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 = Proof.Step.t 

type proof = Proof.t 

type result = 

exception WrongState of string

module type S = sig .. end