Module Sidekick_base.Proof

Proofs of unsatisfiability

Proofs are used in sidekick when the problem is found unsatisfiable. A proof collects inferences made by the solver into a list of steps, each with its own kind of justification (e.g. "by congruence"), and outputs it in some kind of format.

Currently we target Quip as an experimental proof backend.

include Sidekick_core.PROOF with type term = Base_types.Term.t and type ty = Base_types.Ty.t
type t

The abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)

type term = Base_types.Term.t
type ty = Base_types.Ty.t
type hres_step

hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation

val r : t -> pivot:term -> hres_step

Resolution step on given pivot term

val r1 : t -> hres_step

Unit resolution; pivot is obvious

val p : t -> lhs:term -> rhs:term -> hres_step

Paramodulation using proof whose conclusion has a literal lhs=rhs

val p1 : t -> hres_step

Unit paramodulation

type lit

Proof representation of literals

val pp_lit : lit Sidekick_core.Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step

define a (new) atomic term

val is_trivial_refl : t -> bool

is this a proof of |- t=t? This can be used to remove some trivial steps that would build on the proof (e.g. rewriting using refl t is useless).

val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t
val hres_l : t -> hres_step list -> t
val res : pivot:term -> t -> t -> t
val res1 : t -> t -> t
val refl : term -> t
val true_is_true : t
val true_neq_false : t
val nn : t -> t
val cc_lemma : lit list -> t
val cc_imply2 : t -> t -> term -> term -> t
val cc_imply_l : t list -> term -> term -> t
val composite_iter : ?⁠assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?⁠assms:(string * lit) list -> composite_step list -> t
val sorry : t
val sorry_c : lit Iter.t -> t
val sorry_c_l : lit list -> t
val default : t
val pp_debug : sharing:bool -> t Sidekick_core.Fmt.printer

Pretty print a proof.

parameter sharing

if true, try to compact the proof by introducing definitions for common terms, clauses, and steps as needed. Safe to ignore.

module Quip : sig ... end
val isa_split : ty -> term Iter.t -> t
val isa_disj : ty -> term -> term -> t
val cstor_inj : Base_types.Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : string -> term list -> t
val ite_true : term -> t
val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t