diff --git a/dev/sidekick-base/Sidekick_base/Proof/index.html b/dev/sidekick-base/Sidekick_base/Proof/index.html index 87c873a9..a8fc6123 100644 --- a/dev/sidekick-base/Sidekick_base/Proof/index.html +++ b/dev/sidekick-base/Sidekick_base/Proof/index.html @@ -1,2 +1,2 @@ -Proof (sidekick-base.Sidekick_base.Proof)

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
\ No newline at end of file +Proof (sidekick-base.Sidekick_base.Proof)

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

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
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html b/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html index f89ef843..d6b20791 100644 --- a/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html +++ b/dev/sidekick-base/Sidekick_base/Proof_dummy/index.html @@ -1,3 +1,3 @@ Proof_dummy (sidekick-base.Sidekick_base.Proof_dummy)

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.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 := 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 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 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

\ No newline at end of file +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.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 := 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 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 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.

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

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html new file mode 100644 index 00000000..ea5323cd --- /dev/null +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_proof_r1/index.html @@ -0,0 +1,2 @@ + +Step_proof_r1 (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_proof_r1)

Module Proof_ser.Step_proof_r1

type t = {
unit : ID.t;
c : ID.t;
}
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html index a81492f0..b77c7a88 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/Step_view/index.html @@ -1,2 +1,2 @@ -Step_view (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_view)

Module Proof_ser.Step_view

type t =
| Step_input of Step_input.t
| Step_unsat of Step_unsat.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Step_clause_rw of Step_clause_rw.t
| Step_bool_tauto of Step_bool_tauto.t
| Step_bool_c of Step_bool_c.t
| Step_proof_p1 of Step_proof_p1.t
| Step_true of Step_true.t
| Fun_decl of Fun_decl.t
| Expr_def of Expr_def.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file +Step_view (sidekick-base.Sidekick_base_proof_trace.Proof_ser.Step_view)

Module Proof_ser.Step_view

type t =
| Step_input of Step_input.t
| Step_unsat of Step_unsat.t
| Step_rup of Step_rup.t
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
| Step_cc of Step_cc.t
| Step_preprocess of Step_preprocess.t
| Step_clause_rw of Step_clause_rw.t
| Step_bool_tauto of Step_bool_tauto.t
| Step_bool_c of Step_bool_c.t
| Step_proof_p1 of Step_proof_p1.t
| Step_proof_r1 of Step_proof_r1.t
| Step_true of Step_true.t
| Fun_decl of Fun_decl.t
| Expr_def of Expr_def.t
| Expr_bool of Expr_bool.t
| Expr_if of Expr_if.t
| Expr_not of Expr_not.t
| Expr_eq of Expr_eq.t
| Expr_app of Expr_app.t
val decode : Bare.Decode.t -> t
  • raises Bare.Decode.Error

    in case of error.

val encode : Bare.Encode.t -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html index 43450830..e585f896 100644 --- a/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html +++ b/dev/sidekick-base/Sidekick_base_proof_trace/Proof_ser/index.html @@ -1,2 +1,2 @@ -Proof_ser (sidekick-base.Sidekick_base_proof_trace.Proof_ser)

Module Sidekick_base_proof_trace.Proof_ser

module Bare : sig ... end
module ID : sig ... end
module Lit : sig ... end
module Clause : sig ... end
module Step_input : sig ... end
module Step_rup : sig ... end
module Step_bridge_lit_expr : sig ... end
module Step_cc : sig ... end
module Step_preprocess : sig ... end
module Step_clause_rw : sig ... end
module Step_unsat : sig ... end
module Step_proof_p1 : sig ... end
module Step_bool_tauto : sig ... end
module Step_bool_c : sig ... end
module Step_true : sig ... end
module Fun_decl : sig ... end
module Expr_def : sig ... end
module Expr_bool : sig ... end
module Expr_if : sig ... end
module Expr_not : sig ... end
module Expr_eq : sig ... end
module Expr_app : sig ... end
module Step_view : sig ... end
module Step : sig ... end
\ No newline at end of file +Proof_ser (sidekick-base.Sidekick_base_proof_trace.Proof_ser)

Module Sidekick_base_proof_trace.Proof_ser

module Bare : sig ... end
module ID : sig ... end
module Lit : sig ... end
module Clause : sig ... end
module Step_input : sig ... end
module Step_rup : sig ... end
module Step_bridge_lit_expr : sig ... end
module Step_cc : sig ... end
module Step_preprocess : sig ... end
module Step_clause_rw : sig ... end
module Step_unsat : sig ... end
module Step_proof_p1 : sig ... end
module Step_proof_r1 : sig ... end
module Step_bool_tauto : sig ... end
module Step_bool_c : sig ... end
module Step_true : sig ... end
module Fun_decl : sig ... end
module Expr_def : sig ... end
module Expr_bool : sig ... end
module Expr_if : sig ... end
module Expr_not : sig ... end
module Expr_eq : sig ... end
module Expr_app : sig ... end
module Step_view : sig ... end
module Step : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/P/index.html index beef1b8b..852cc2e1 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Solver.P)

Module Solver.P

type proof_step = Solver_arg.proof_step
type lit = Solver_arg.Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Solver.P)

Module Solver.P

type proof_step = Solver_arg.proof_step
type lit = Solver_arg.Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/index.html index c044c59a..8ccbe2b0 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/Solver_internal/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Solver.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/index.html index 61e1c216..22184808 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Th_bool.A.S.P)

Module S.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Th_bool.A.S.P)

Module S.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/index.html index 0c0252f4..7a4aab34 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/P/index.html new file mode 100644 index 00000000..714fc6a7 --- /dev/null +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/P/index.html @@ -0,0 +1,2 @@ + +P (sidekick-base.Sidekick_base_solver.Th_data.A.P)

Module A.P

val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_select_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_isa_split : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.proof_step
val lemma_isa_sel : S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_isa_disj : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.proof_step
val lemma_cstor_inj : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.proof_step
val lemma_cstor_distinct : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/P/index.html index 35ab8e16..b955db3f 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Th_data.A.S.P)

Module S.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Th_data.A.S.P)

Module S.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/P/index.html index a49aa677..34ac424f 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/index.html index 105f9164..13f7df00 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/index.html @@ -1,2 +1,2 @@ -A (sidekick-base.Sidekick_base_solver.Th_data.A)

Module Th_data.A

module S : sig ... end
module Cstor : sig ... end
val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) Sidekick_th_data.data_ty_view
val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit
val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_select_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_isa_split : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.proof_step
val lemma_isa_sel : S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_isa_disj : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.proof_step
val lemma_cstor_inj : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.proof_step
val lemma_cstor_distinct : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step
val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step
\ No newline at end of file +A (sidekick-base.Sidekick_base_solver.Th_data.A)

Module Th_data.A

module S : sig ... end
module Cstor : sig ... end
val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) Sidekick_th_data.data_ty_view
val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit
module P : sig ... end
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/P/index.html index 4c9a2cf8..0548873a 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Th_lra.A.S.P)

Module S.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Th_lra.A.S.P)

Module S.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/P/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/P/index.html index dd6bd31f..4a024110 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/P/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file +P (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal.P)

Module Solver_internal.P

type t = proof
type proof_step = proof_step
type term = T.Term.t
type lit = Lit.t
type proof_rule = t -> proof_step
val lemma_cc : lit Iter.t -> t -> proof_step
module Step_vec : sig ... end
val enabled : t -> bool
val emit_input_clause : lit Iter.t -> proof_rule
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
val emit_unsat_core : lit Iter.t -> proof_rule
val emit_unsat : proof_step -> t -> unit
val del_clause : proof_step -> lit Iter.t -> t -> unit
val define_term : term -> term -> proof_rule
val proof_p1 : proof_step -> proof_step -> proof_rule
val proof_r1 : proof_step -> proof_step -> proof_rule
val with_defs : proof_step -> proof_step Iter.t -> proof_rule
val lemma_true : term -> proof_rule
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html index d3e200d6..6380e5a9 100644 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/P/index.html @@ -1,2 +1,2 @@ -P (sidekick-bin.Sidekick_smtlib.Process.Solver.P)

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

\ No newline at end of file +P (sidekick-bin.Sidekick_smtlib.Process.Solver.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html index a67214b4..3dfcc1ae 100644 --- a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_arith_lra.Make.1-A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_arith_lra.Make.1-A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html index 5c911741..92a0377c 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_arith_lra.ARG.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_arith_lra.ARG.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html index 32242917..1f882fd2 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_arith_lra.S.A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_arith_lra.S.A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html index 60cc1d1c..eb444830 100644 --- a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html +++ b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI.P)

Module SI.P

Proofs

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 = term
type lit = Lit.t
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file +P (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI.P)

Module SI.P

Proofs

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 = term
type lit = Lit.t
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html index 17c2f93e..ab538578 100644 --- a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.MONOID_ARG.SI.P)

Module SI.P

Proofs

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 = term
type lit = Lit.t
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file +P (sidekick.Sidekick_core.MONOID_ARG.SI.P)

Module SI.P

Proofs

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 = term
type lit = Lit.t
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-PROOF/index.html b/dev/sidekick/Sidekick_core/module-type-PROOF/index.html index 8052fb01..eb5f9b47 100644 --- a/dev/sidekick/Sidekick_core/module-type-PROOF/index.html +++ b/dev/sidekick/Sidekick_core/module-type-PROOF/index.html @@ -1,2 +1,2 @@ -PROOF (sidekick.Sidekick_core.PROOF)

Module type Sidekick_core.PROOF

Proofs of unsatisfiability.

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 proof_step

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

type term
type lit
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file +PROOF (sidekick.Sidekick_core.PROOF)

Module type Sidekick_core.PROOF

Proofs of unsatisfiability.

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 proof_step

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

type term
type lit
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html index a8ccc0c1..8e223e36 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.SOLVER.P)

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

\ No newline at end of file +P (sidekick.Sidekick_core.SOLVER.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html index 7bd098ce..44e8b1a8 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_core.SOLVER_INTERNAL.P)

Module SOLVER_INTERNAL.P

Proofs

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 = term
type lit = Lit.t
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file +P (sidekick.Sidekick_core.SOLVER_INTERNAL.P)

Module SOLVER_INTERNAL.P

Proofs

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 = term
type lit = Lit.t
type proof_rule = t -> proof_step
include 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 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).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/P/index.html b/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/P/index.html index da9ad66b..f953abbd 100644 --- a/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/P/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Make/argument-1-A/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_smt_solver.Make.1-A.P)

Module 1-A.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 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).

\ No newline at end of file +P (sidekick.Sidekick_smt_solver.Make.1-A.P)

Module 1-A.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).

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/module-type-ARG/P/index.html b/dev/sidekick/Sidekick_smt_solver/module-type-ARG/P/index.html index 721f9226..5f0ed1cc 100644 --- a/dev/sidekick/Sidekick_smt_solver/module-type-ARG/P/index.html +++ b/dev/sidekick/Sidekick_smt_solver/module-type-ARG/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_smt_solver.ARG.P)

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

\ No newline at end of file +P (sidekick.Sidekick_smt_solver.ARG.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html index a4b14b2d..9b888ff4 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_bool_static.Make.1-A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_bool_static.Make.1-A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html index c9493ed2..972d5f4a 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_bool_static.ARG.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_bool_static.ARG.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html index 60802655..b7e9e31d 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_bool_static.S.A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_bool_static.S.A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html index db5a13d5..404cbfd3 100644 --- a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_cstor.Make.1-A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_cstor.Make.1-A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html index 9208209f..2f763be7 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_cstor.ARG.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_cstor.ARG.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html index aa1dd1fa..755dbbe0 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_cstor.S.A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_cstor.S.A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/P/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/P/index.html new file mode 100644 index 00000000..960b2e48 --- /dev/null +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/P/index.html @@ -0,0 +1,2 @@ + +P (sidekick.Sidekick_th_data.Make.1-A.P)

Module 1-A.P

val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.P.t -> S.P.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 : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step

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

val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html index ba56c15d..fede49a6 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_data.Make.1-A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_data.Make.1-A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html index 9aa53dfd..b4d4e801 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html @@ -1,2 +1,2 @@ -A (sidekick.Sidekick_th_data.Make.1-A)

Parameter Make.1-A

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

Make a constructor application term

Make a is-a term

val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

include PROOF with type proof := S.P.t and type proof_step := S.P.proof_step and type term := S.T.Term.t and type lit := S.Lit.t
val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.P.t -> S.P.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 : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step

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

val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step

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

\ No newline at end of file +A (sidekick.Sidekick_th_data.Make.1-A)

Parameter Make.1-A

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

Make a constructor application term

Make a is-a term

val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

module P : PROOF with type proof := S.P.t and type proof_step := S.P.proof_step and type term := S.T.Term.t and type lit := S.Lit.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/P/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/P/index.html new file mode 100644 index 00000000..91611166 --- /dev/null +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/P/index.html @@ -0,0 +1,2 @@ + +P (sidekick.Sidekick_th_data.ARG.P)

Module ARG.P

val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.P.t -> S.P.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 : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step

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

val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html index d04222e1..4f91d26f 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_data.ARG.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_data.ARG.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html index fac563cc..eeaef950 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html @@ -1,2 +1,2 @@ -ARG (sidekick.Sidekick_th_data.ARG)

Module type Sidekick_th_data.ARG

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

Make a constructor application term

Make a is-a term

val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

include PROOF with type proof := S.P.t and type proof_step := S.P.proof_step and type term := S.T.Term.t and type lit := S.Lit.t
val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.P.t -> S.P.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 : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step

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

val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step

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

\ No newline at end of file +ARG (sidekick.Sidekick_th_data.ARG)

Module type Sidekick_th_data.ARG

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

Make a constructor application term

Make a is-a term

val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

module P : PROOF with type proof := S.P.t and type proof_step := S.P.proof_step and type term := S.T.Term.t and type lit := S.Lit.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/P/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/P/index.html new file mode 100644 index 00000000..2a841114 --- /dev/null +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/P/index.html @@ -0,0 +1,2 @@ + +P (sidekick.Sidekick_th_data.S.A.P)

Module A.P

val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.P.t -> S.P.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 : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step

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

val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html index adffb11f..b8c3c848 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/P/index.html @@ -1,2 +1,2 @@ -P (sidekick.Sidekick_th_data.S.A.S.P)

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

\ No newline at end of file +P (sidekick.Sidekick_th_data.S.A.S.P)

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/index.html index 6de28ed8..15a508ef 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/A/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/index.html @@ -1,2 +1,2 @@ -A (sidekick.Sidekick_th_data.S.A)

Module S.A

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

Make a constructor application term

Make a is-a term

val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

include PROOF with type proof := S.P.t and type proof_step := S.P.proof_step and type term := S.T.Term.t and type lit := S.Lit.t
val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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:S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.Lit.t Iter.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.P.t -> S.P.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 : S.Lit.t -> S.Lit.t -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> int -> S.P.t -> S.P.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 : S.T.Term.t -> S.T.Term.t -> S.P.t -> S.P.proof_step

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

val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.t -> S.P.proof_step

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

\ No newline at end of file +A (sidekick.Sidekick_th_data.S.A)

Module S.A

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

Make a constructor application term

Make a is-a term

val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

module P : PROOF with type proof := S.P.t and type proof_step := S.P.proof_step and type term := S.T.Term.t and type lit := S.Lit.t
\ No newline at end of file