Module Sidekick_base.Proof_dummy

Dummy proof module that does nothing.

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

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 = private unit

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

type term = Base_types.Term.t
type lit = Lit.t
include Sidekick_core.SAT_PROOF with type t := t and type lit := lit and type proof_step := proof_step and type proof_rule := t -> proof_step

A vector of steps

val enabled : t -> bool

Returns true if proof production is enabled

val emit_input_clause : lit Iter.t -> t -> proof_step

Emit an input clause.

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

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

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 lemma_cc : lit Iter.t -> t -> proof_step

lemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.

val define_term : term -> term -> t -> proof_step

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

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

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 proof_res : pivot:term -> proof_step -> proof_step -> t -> proof_step

proof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.

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

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

val lemma_true : term -> t -> proof_step

lemma_true (true) p asserts the clause (true)

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

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

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).

type proof_rule = t -> proof_step
val create : unit -> t
val lemma_lra : Lit.t Iter.t -> proof_rule
include Sidekick_th_data.PROOF with type proof := t and type proof_step := proof_step and type lit := Lit.t and type term := Base_types.Term.t
val lemma_isa_cstor : cstor_t:Base_types.Term.t -> Base_types.Term.t -> t -> proof_step

lemma_isa_cstor (d …) (is-c t) returns the clause (c …) = t |- is-c t or (d …) = t |- ¬ (is-c t)

val lemma_select_cstor : cstor_t:Base_types.Term.t -> Base_types.Term.t -> t -> proof_step

lemma_select_cstor (c t1…tn) (sel-c-i t) returns a proof of t = c t1…tn |- (sel-c-i t) = ti

val lemma_isa_split : Base_types.Term.t -> Lit.t Iter.t -> t -> proof_step

lemma_isa_split t lits is the proof of is-c1 t \/ is-c2 t \/ … \/ is-c_n t

val lemma_isa_sel : Base_types.Term.t -> t -> proof_step

lemma_isa_sel (is-c t) is the proof of is-c t |- t = c (sel-c-1 t)…(sel-c-n t)

val lemma_isa_disj : Lit.t -> Lit.t -> t -> proof_step

lemma_isa_disj (is-c t) (is-d t) is the proof of ¬ (is-c t) \/ ¬ (is-c t)

val lemma_cstor_inj : Base_types.Term.t -> Base_types.Term.t -> int -> t -> proof_step

lemma_cstor_inj (c t1…tn) (c u1…un) i is the proof of c t1…tn = c u1…un |- ti = ui

val lemma_cstor_distinct : Base_types.Term.t -> Base_types.Term.t -> t -> proof_step

lemma_isa_distinct (c …) (d …) is the proof of the unit clause |- (c …) ≠ (d …)

val lemma_acyclicity : (Base_types.Term.t * Base_types.Term.t) Iter.t -> t -> proof_step

lemma_acyclicity pairs is a proof of t1=u1, …, tn=un |- false by acyclicity.

include Sidekick_th_bool_static.PROOF with type proof := t and type proof_step := proof_step and type lit := Lit.t and type term := Base_types.Term.t
val lemma_bool_tauto : Lit.t Iter.t -> t -> proof_step

Boolean tautology lemma (clause)

val lemma_bool_c : string -> Base_types.Term.t list -> t -> proof_step

Basic boolean logic lemma for a clause |- c. proof_bool_c b name cs is the rule designated by name.

val lemma_bool_equiv : Base_types.Term.t -> Base_types.Term.t -> t -> proof_step

Boolean tautology lemma (equivalence)

val lemma_ite_true : ite:Base_types.Term.t -> t -> proof_step

lemma a ==> ite a b c = b

val lemma_ite_false : ite:Base_types.Term.t -> t -> proof_step

lemma ¬a ==> ite a b c = c