module Sat_solver_intf:sig
..end
add_clause ~tag ~proof c
adds the constraint c
to the SAT solver,
annotated with proof
. tag
is a unique identifier for this constraint
and must not have been already used.typeproof_step =
Proof.Step.t
typeproof =
Proof.t
type
result =
| |
Sat |
| |
Unsat of |
exception WrongState of string
module type S =sig
..end