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 proof_step = proof_step

Identifier for a proof proof_rule (like a unique ID for a clause previously added/proved)

type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
include Sidekick_core.CC_PROOF with type t := t and type lit := lit and type proof_step := proof_step
val lemma_cc : lit Iter.t -> t -> proof_step

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 and type proof_step := proof_step and type proof_rule := proof_rule

A vector of steps

val enabled : t -> bool

Returns true if proof production is enabled

val emit_input_clause : lit Iter.t -> proof_rule

Emit an input clause.

val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule

Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.

val emit_unsat_core : lit Iter.t -> proof_rule

Produce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?

val emit_unsat : proof_step -> t -> unit

Signal "unsat" result at the given proof

val del_clause : proof_step -> lit Iter.t -> t -> unit

Forget a clause. Only useful for performance considerations.

val define_term : term -> term -> proof_rule

define_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u

val proof_p1 : proof_step -> proof_step -> proof_rule

proof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.

val proof_r1 : proof_step -> proof_step -> proof_rule

proof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.

val with_defs : proof_step -> proof_step Iter.t -> proof_rule

with_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.

val lemma_true : term -> proof_rule

lemma_true (true) p asserts the clause (true)

val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule

lemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.

The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.

From now on, t and u will be used interchangeably.

  • returns

    a proof_rule ID for the clause (t=u).

val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule

lemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).