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 = ProofStep.t

type proof = ProofStep.of_

type result =

`\|`	`Sat`
`\|`	`Unsat of proof`

exception WrongState of string

module type S = sig .. end