Module `Sidekick_base.Proof_stub`

Dummy proof module that does nothing.

include Sidekick_core.PROOF with type lit = Lit.t and type term = Base_types.Term.t

type t: 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 = Base_types.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.

val create : unit -> t
val lemma_bool_tauto : Lit.t Iter.t -> t -> unit
val lemma_bool_c : string -> term list -> t -> unit
val lemma_bool_equiv : term -> term -> t -> unit
val lemma_ite_true : a:term -> ite:term -> t -> unit
val lemma_ite_false : a:term -> ite:term -> t -> unit
val lemma_lra : Lit.t Iter.t -> t -> unit
val lemma_isa_split : Lit.t Iter.t -> t -> unit
val lemma_isa_disj : Lit.t Iter.t -> t -> unit
val lemma_cstor_inj : Lit.t Iter.t -> t -> unit