package hardcaml_verify

  1. Overview
  2. Docs
type run_solver = dimacs_in:Base.string -> result_out:Base.string -> Base.unit -> Base.unit Base.Or_error.t
val minisat : run_solver

Minisat solver

val picosat : run_solver

Picosat solver

val z3 : ?seed:Base.int -> parallel:Base.bool -> Base.unit -> run_solver

Z3 solver in DIMACs mode. parallel:true enableds parallel solving, however, as of V4.8.5 Z3 does not return a proper model.

type 'a result = 'a Base.list Sat.t Base.Or_error.t
val sexp_of_result : ('a -> Sexplib0.Sexp.t) -> 'a result -> Sexplib0.Sexp.t
val solve_with_model : ?solver:run_solver -> ?print_model:Base.bool -> (module Cnf.Model with type input = 'input) -> Cnf.t -> 'input result

Create intermediate files, run the given solver and return a model if satisfiable.

val solve : ?solver:run_solver -> ?print_model:Base.bool -> Cnf.t -> Cnf.Model_with_vectors.input result