Module Sat_solver_intf

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.

type proof_step = Logtk.Proof.Step.t 
type proof = Logtk.Proof.t 
type result = 
| Sat
| Unsat of proof
exception WrongState of string
module type S = sig .. end