Mc2_dimacs (p.mc2.0.1.doc.mc2.dimacs.Mc2

Main for dimacs

This library provides a parser for DIMACS files, to represent SAT problems.

http://www.satcompetition.org/2009/format-benchmarks2009.html

Sourcemodule Plugin_sat : sig ... end

Sourcetype 'a or_error = ('a, string) CCResult.t

Sourceval plugin : Mc2_core.Plugin.Factory.t

Sourceval k_atom : (int -> Mc2_core.atom) Mc2_core.Service.Key.t

Key to build atoms

Source

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

Sourceval solve : Mc2_core.Solver.t -> Mc2_core.Solver.res or_error

Solve a problem

Source

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