Module Sidekick_base.Proof

Proof representation

module Config : sig ... end

Configuration of proofs

Main Proof API

type t

A container for the whole proof

type proof_step

A proof step in the trace.

The proof will store all steps, and at the end when we find the empty clause we can filter them to keep only the relevant ones.

include Sidekick_core.PROOF with type t := t and type proof_step := proof_step and type lit = Lit.t and type term = Base_types.Term.t
type term = Base_types.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 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).

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

Creation

val create : ?config:Config.t -> unit -> t

Create new proof.

  • parameter config

    modifies the proof behavior

val empty : t

Empty proof, stores nothing

val disable : t -> unit

Disable proof, even if the config would enable it

Use the proof

val iter_steps_backward : t -> Base_types.Proof_ser.Step.t Iter.t

Iterates on all the steps of the proof, from the end.

This will yield nothing if the proof was disabled or used a dummy backend.

module Unsafe_ : sig ... end