Module Mc2_dimacs
Main for dimacs
module Plugin_sat : sig ... end
val plugin : Mc2_core.Plugin.Factory.t
val k_atom : (int -> Mc2_core.atom) Mc2_core.Service.Key.t
Key to build atoms
val parse : Mc2_core.Service.Registry.t -> string -> Mc2_core.atom list list or_error
Parse a file into a list of clauses.
- parameter registry
used to build atoms from integers, see
k_atom
val solve : Mc2_core.Solver.t -> Mc2_core.Solver.res or_error
Solve a problem
val process : ?gc:bool -> ?restarts:bool -> ?dot_proof:string -> ?pp_model:bool -> ?check:bool -> ?time:float -> ?memory:float -> ?progress:bool -> ?switch:Mc2_core.Util.Switch.t -> Mc2_core.Solver.t -> Mc2_core.atom list list -> unit or_error
Add clauses to solver, solve, and prints the results.
- parameter check
check proof/model
- parameter progress
print progress bar
- parameter dot_proof
file into which to print the proof