Hardcaml_verify_kernel.Dimacsval write_problem : Cnf.t -> Stdio.Out_channel.t -> Base.unitWrite a DIMACS formatted CNF file suitable for input into SAT solvers.
val parse_result :
Base.string Base.list ->
Base.int Base.list Sat.t Base.Or_error.tParse the result of a SAT solver. Different solves use different formats, so the parsing is quie relaxed and works with minisat, picosat and z3.
val read_result :
Stdio.In_channel.t ->
Base.int Base.list Sat.t Base.Or_error.tRead the result of a SAT solver.