Module Mc2_dimacs

Main for dimacs

module Plugin_sat : sig ... end
type 'a or_error = ('a, string) CCResult.t
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