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