Module `Solver.P`

type t = proof: The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = T.Term.t
type lit = Lit.t

include Sidekick_core.CC_PROOF with type t := t and type lit := lit

type t
type lit

val lemma_cc : lit Iter.t -> t -> unit: lemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.

include Sidekick_core.SAT_PROOF with type t := t and type lit := lit

type t: The stored proof (possibly nil, possibly on disk, possibly in memory)

type lit: A boolean literal for the proof trace

type dproof = t -> unit: A delayed proof, used to produce proofs on demand from theories.

val with_proof : t -> (t -> unit) -> unit: If proof is enabled, call f on it to emit steps. if proof is disabled, the callback won't even be called.

val emit_input_clause : lit Iter.t -> t -> unit: Emit an input clause.

val emit_redundant_clause : lit Iter.t -> t -> unit: Emit a clause deduced by the SAT solver, redundant wrt axioms. The clause must be RUP wrt previous clauses.

val del_clause : lit Iter.t -> t -> unit: Forget a clause. Only useful for performance considerations.

val begin_subproof : t -> unit: Begins a subproof. The result of this will only be the clause with which end_subproof is called; all other intermediate steps will be discarded.

val end_subproof : t -> unit: end_subproof p ends the current active subproof, the last result of which is kept.

val define_term : term -> term -> t -> unit: define_term p cst u defines the new constant cst as being equal to u.

val lemma_true : term -> t -> unit: lemma_true p (true) asserts the clause (true)

val lemma_preprocess : term -> term -> t -> unit: lemma_preprocess p t u asserts that t = u is a tautology and that t has been preprocessed into u. From now on, t and u will be used interchangeably.