An unsat answer comes with a proof, if the solver was asked to produce one. cvc.lean hands it over as data: each step of the proof can be taken apart into its rule, its premises and its arguments, and the whole proof can be traversed — to find the lemmas a refutation relies on, to see which assertions it uses, or to rebuild it elsewhere.
As for the solver, the rest of this section uses the typed layer; the sort-erased one is the same with sort-erased formulas.
open Cvc Typed
variable [Ω]
A proof is only available where the answer was unsat, so getUnsatProof lives in the unsat mode, and needs cvc5's produce-proofs option.
Cvc.Typed.Solver.getUnsatProof [Cvc.Ω] (s : Cvc.Typed.Solver) (pc : Cvc.Proof.Component := Cvc.Proof.Component.full) : s.EnvUnsat (s.Proofs pc)Cvc.Typed.Solver.getUnsatProof [Cvc.Ω] (s : Cvc.Typed.Solver) (pc : Cvc.Proof.Component := Cvc.Proof.Component.full) : s.EnvUnsat (s.Proofs pc)
The proof of the unsat answer this block stands on, for component pc.
Needs the solver option produce-proofs. The full component, the default, is the whole
refutation, and answers one proof; the others are its parts — preprocessing, the SAT solver's
reasoning, the theory lemmas — and may answer several, one per lemma for theoryLemmas. These are
this layer's proofs, whose conclusions are Term Bool.
A proof produced by solver s for component pc, whose conclusions are formulas, Term Bool.
The same cvc5 proof as the sort-erased Cvc.Untyped.Solver.Proof, under a type of its own: the
sort-erased functions do not accept it, and toUntyped (or relax) and toTyped cross for free.
A proof is indexed by the solver that produced it and by the component it was asked for: the whole refutation (full, the default), or one of its parts — preprocessing, the SAT solver's reasoning, the theory lemmas. Printing a proof in a format other than Proof.Format.no is only legal for full, and the index is what makes that a type obligation.
for step in proof do … visits the distinct steps of a proof:
#eval Env.runIO do
let s ← Solver.new
s.setOpt .smt_produceProofs true
let b ← Term.mkSymbolAs Bool "b"
s.assert b
s.assert (← smt! ¬ b)
let proofs ← s.checkSat
(ifUnsat := s.getUnsatProof)
for p in proofs do
for step in p do
println! "{step.getRule} ⊢ {step.getResult}"
view answers a step as a Solver.ProofView, one constructor per rule:
Cvc.Typed.Solver.Proof.view {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : s.ProofView pcCvc.Typed.Solver.Proof.view {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : s.ProofView pc
The root step of p, taken apart: its rule as a constructor, its premises and arguments.
The two layers' views are one type, Cvc.Proof.View P F T, at each layer's own types: P is a premise, F a formula and T a term of any sort. A typed view's formulas are Term Bool and its other terms sort-erased; a sort-erased view's are all sort-erased:
A step of a typed proof, taken apart: formulas as Term Bool, other terms sort-erased.
Equations
s.ProofView pc =
Cvc.Proof.View (s.Proof pc) (Cvc.Typed.Term Bool) Cvc.Untyped.Term
A step of a sort-erased proof, taken apart: Cvc.Proof.View over sort-erased terms.
Equations
s.ProofView pc =
Cvc.Proof.View (s.Proof pc) Cvc.Untyped.Term Cvc.Untyped.Term
The premise type is a parameter too, so that foldUp (see below) can hand over a step whose premises are values it has already computed rather than proofs. Here is the generic type, with every rule it decodes:
One step of a cvc5 proof: its rule as a constructor, its premises and arguments as fields.
The parameters say what the fields are, so that each layer picks its own, and so that a traversal can hand over a step whose premises are something else entirely:
P is a premise — a proof, or what a bottom-up traversal computed for one;
F is a formula — a sort-erased term, or a typed Term Bool;
T is a term of any sort.
The conclusion is not a field: it is the step's own result. Neither is an argument that only
restates it, such as REORDERING's target clause or THEORY_REWRITE's equality.
A rule is decoded only when its step has the layout cvc5 documents; anything else is other,
holding the step's premises and arguments as cvc5 gives them. So no step is lost, and a layout cvc5
changes degrades to other rather than to a wrong reading. Which rules are decoded can grow, and a
rule moving out of other is the change to expect from one version to the next.
Which rules appear at all depends on cvc5's proof-granularity option. Coarse settings leave
MACRO_… steps, which are other here; dsl-rewrite breaks rewriting down into dslRewrite,
theoryRewrite and the equality rules.
Constructors
Cvc.Proof.View.assume {P F T : Type} (f : F) : Cvc.Proof.View P F T
ASSUME, an open leaf: concludes f, unless an enclosing scope discharges it.
Cvc.Proof.View.scope {P F T : Type} (body : P) (discharged : Array F) : Cvc.Proof.View P F T
SCOPE: discharges discharged from body : F, concluding F₁ ∧ … ∧ Fₙ ⇒ F.
When F is false, the conclusion is ¬(F₁ ∧ … ∧ Fₙ) instead.
Cvc.Proof.View.evaluate {P F T : Type} (t : T) : Cvc.Proof.View P F T
EVALUATE: t = v, v being the value t evaluates to.
Cvc.Proof.View.dslRewrite {P F T : Type} (rule : cvc5.ProofRewriteRule) (premises : Array P) (instantiation : Array T) : Cvc.Proof.View P F T
DSL_REWRITE: an instance of the RARE rule rule, its variables instantiated in order.
The premises are the rule's conditions, instantiated likewise. A variable with list semantics is instantiated with the list of terms it stands for.
Cvc.Proof.View.theoryRewrite {P F T : Type} (rule : cvc5.ProofRewriteRule) : Cvc.Proof.View P F T
THEORY_REWRITE: t = t', the conclusion, by the theory rewrite rule rule.
Cvc.Proof.View.aciNorm {P F T : Type} : Cvc.Proof.View P F T
ACI_NORM: t = s, equal modulo associativity, commutativity, idempotence and identity.
Cvc.Proof.View.absorb {P F T : Type} : Cvc.Proof.View P F T
ABSORB: t = z, z being a zero element t contains beneath its operator.
Cvc.Proof.View.trust {P F T : Type} (id : Nat) (premises : Array P) (extra : Array T) : Cvc.Proof.View P F T
Cvc.Proof.View.trustTheoryRewrite {P F T : Type} (theory method : Nat) : Cvc.Proof.View P F T
TRUST_THEORY_REWRITE: an unchecked theory rewrite, the equality being the conclusion.
theory identifies the theory whose rewriter applied and method the kind of rewriting; both are
cvc5's internal identifiers, which its API does not name.
Cvc.Proof.View.satRefutation {P F T : Type} (premises : Array P) : Cvc.Proof.View P F T
Cvc.Proof.View.resolution {P F T : Type} (left right : P) (polarity : Bool) (pivot : F) : Cvc.Proof.View P F T
Cvc.Proof.View.chainResolution {P F T : Type} (premises : Array P) (steps : Array (Bool × F)) : Cvc.Proof.View P F T
CHAIN_RESOLUTION: resolves premises left to right, step i on steps[i]'s pivot.
Each step is a polarity and a pivot, as in resolution, and there is one step fewer than there
are premises.
Cvc.Proof.View.chainMResolution {P F T : Type} (premises : Array P) (steps : Array (Bool × F)) : Cvc.Proof.View P F T
CHAIN_M_RESOLUTION: chainResolution with factoring and reordering.
The conclusion is the result of the resolution as a set of literals.
Cvc.Proof.View.factoring {P F T : Type} (premise : P) : Cvc.Proof.View P F T
FACTORING: premise's clause, every literal's repetitions dropped.
Cvc.Proof.View.reordering {P F T : Type} (premise : P) : Cvc.Proof.View P F T
REORDERING: premise's clause, its literals in the conclusion's order.
Cvc.Proof.View.split {P F T : Type} (f : F) : Cvc.Proof.View P F T
SPLIT: f ∨ ¬f.
Cvc.Proof.View.eqResolve {P F T : Type} (premise equiv : P) : Cvc.Proof.View P F T
EQ_RESOLVE: F₂ from premise : F₁ and equiv : F₁ = F₂.
Cvc.Proof.View.modusPonens {P F T : Type} (premise implication : P) : Cvc.Proof.View P F T
MODUS_PONENS: F₂ from premise : F₁ and implication : F₁ ⇒ F₂.
Cvc.Proof.View.notNotElim {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_NOT_ELIM: F from ¬¬F.
Cvc.Proof.View.contra {P F T : Type} (premise negation : P) : Cvc.Proof.View P F T
CONTRA: false from premise : F and negation : ¬F.
Cvc.Proof.View.andElim {P F T : Type} (premise : P) (index : Nat) : Cvc.Proof.View P F T
AND_ELIM: the conjunct at index of premise : F₀ ∧ … ∧ Fₙ, counting from zero.
Cvc.Proof.View.andIntro {P F T : Type} (premises : Array P) : Cvc.Proof.View P F T
AND_INTRO: the conjunction of the premises' conclusions.
Cvc.Proof.View.notOrElim {P F T : Type} (premise : P) (index : Nat) : Cvc.Proof.View P F T
NOT_OR_ELIM: ¬Fᵢ from premise : ¬(F₀ ∨ … ∨ Fₙ), i being index, from zero.
Cvc.Proof.View.impliesElim {P F T : Type} (premise : P) : Cvc.Proof.View P F T
IMPLIES_ELIM: ¬F₁ ∨ F₂ from F₁ ⇒ F₂.
Cvc.Proof.View.notImpliesElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_IMPLIES_ELIM1: F₁ from ¬(F₁ ⇒ F₂).
Cvc.Proof.View.notImpliesElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_IMPLIES_ELIM2: ¬F₂ from ¬(F₁ ⇒ F₂).
Cvc.Proof.View.equivElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
EQUIV_ELIM1: ¬F₁ ∨ F₂ from F₁ = F₂.
Cvc.Proof.View.equivElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
EQUIV_ELIM2: F₁ ∨ ¬F₂ from F₁ = F₂.
Cvc.Proof.View.notEquivElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_EQUIV_ELIM1: F₁ ∨ F₂ from F₁ ≠ F₂.
Cvc.Proof.View.notEquivElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_EQUIV_ELIM2: ¬F₁ ∨ ¬F₂ from F₁ ≠ F₂.
Cvc.Proof.View.xorElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
XOR_ELIM1: F₁ ∨ F₂ from F₁ ⊕ F₂.
Cvc.Proof.View.xorElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
XOR_ELIM2: ¬F₁ ∨ ¬F₂ from F₁ ⊕ F₂.
Cvc.Proof.View.notXorElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_XOR_ELIM1: F₁ ∨ ¬F₂ from ¬(F₁ ⊕ F₂).
Cvc.Proof.View.notXorElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_XOR_ELIM2: ¬F₁ ∨ F₂ from ¬(F₁ ⊕ F₂).
Cvc.Proof.View.iteElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
ITE_ELIM1: ¬C ∨ F₁ from ite C F₁ F₂.
Cvc.Proof.View.iteElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
ITE_ELIM2: C ∨ F₂ from ite C F₁ F₂.
Cvc.Proof.View.notIteElim1 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_ITE_ELIM1: ¬C ∨ ¬F₁ from ¬(ite C F₁ F₂).
Cvc.Proof.View.notIteElim2 {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_ITE_ELIM2: C ∨ ¬F₂ from ¬(ite C F₁ F₂).
Cvc.Proof.View.notAnd {P F T : Type} (premise : P) : Cvc.Proof.View P F T
NOT_AND: ¬F₁ ∨ … ∨ ¬Fₙ from ¬(F₁ ∧ … ∧ Fₙ).
Cvc.Proof.View.cnfAndPos {P F T : Type} (f : F) (index : Nat) : Cvc.Proof.View P F T
CNF_AND_POS: ¬f ∨ Fᵢ, f being F₀ ∧ … ∧ Fₙ and i index, counting from zero.
Cvc.Proof.View.cnfAndNeg {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_AND_NEG: f ∨ ¬F₁ ∨ … ∨ ¬Fₙ, f being F₁ ∧ … ∧ Fₙ.
Cvc.Proof.View.cnfOrPos {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_OR_POS: ¬f ∨ F₁ ∨ … ∨ Fₙ, f being F₁ ∨ … ∨ Fₙ.
Cvc.Proof.View.cnfOrNeg {P F T : Type} (f : F) (index : Nat) : Cvc.Proof.View P F T
CNF_OR_NEG: f ∨ ¬Fᵢ, f being F₀ ∨ … ∨ Fₙ and i index, counting from zero.
Cvc.Proof.View.cnfImpliesPos {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_IMPLIES_POS: ¬f ∨ ¬F₁ ∨ F₂, f being F₁ ⇒ F₂.
Cvc.Proof.View.cnfImpliesNeg1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_IMPLIES_NEG1: f ∨ F₁, f being F₁ ⇒ F₂.
Cvc.Proof.View.cnfImpliesNeg2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_IMPLIES_NEG2: f ∨ ¬F₂, f being F₁ ⇒ F₂.
Cvc.Proof.View.cnfEquivPos1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_EQUIV_POS1: ¬f ∨ ¬F₁ ∨ F₂, f being F₁ = F₂.
Cvc.Proof.View.cnfEquivPos2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_EQUIV_POS2: ¬f ∨ F₁ ∨ ¬F₂, f being F₁ = F₂.
Cvc.Proof.View.cnfEquivNeg1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_EQUIV_NEG1: f ∨ F₁ ∨ F₂, f being F₁ = F₂.
Cvc.Proof.View.cnfEquivNeg2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_EQUIV_NEG2: f ∨ ¬F₁ ∨ ¬F₂, f being F₁ = F₂.
Cvc.Proof.View.cnfXorPos1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_XOR_POS1: ¬f ∨ F₁ ∨ F₂, f being F₁ ⊕ F₂.
Cvc.Proof.View.cnfXorPos2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_XOR_POS2: ¬f ∨ ¬F₁ ∨ ¬F₂, f being F₁ ⊕ F₂.
Cvc.Proof.View.cnfXorNeg1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_XOR_NEG1: f ∨ ¬F₁ ∨ F₂, f being F₁ ⊕ F₂.
Cvc.Proof.View.cnfXorNeg2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_XOR_NEG2: f ∨ F₁ ∨ ¬F₂, f being F₁ ⊕ F₂.
Cvc.Proof.View.cnfItePos1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_ITE_POS1: ¬f ∨ ¬C ∨ F₁, f being ite C F₁ F₂.
Cvc.Proof.View.cnfItePos2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_ITE_POS2: ¬f ∨ C ∨ F₂, f being ite C F₁ F₂.
Cvc.Proof.View.cnfItePos3 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_ITE_POS3: ¬f ∨ F₁ ∨ F₂, f being ite C F₁ F₂.
Cvc.Proof.View.cnfIteNeg1 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_ITE_NEG1: f ∨ ¬C ∨ ¬F₁, f being ite C F₁ F₂.
Cvc.Proof.View.cnfIteNeg2 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_ITE_NEG2: f ∨ C ∨ ¬F₂, f being ite C F₁ F₂.
Cvc.Proof.View.cnfIteNeg3 {P F T : Type} (f : F) : Cvc.Proof.View P F T
CNF_ITE_NEG3: f ∨ ¬F₁ ∨ ¬F₂, f being ite C F₁ F₂.
Cvc.Proof.View.refl {P F T : Type} (t : T) : Cvc.Proof.View P F T
REFL: t = t.
Cvc.Proof.View.symm {P F T : Type} (premise : P) : Cvc.Proof.View P F T
SYMM: t₂ = t₁ from t₁ = t₂, or t₂ ≠ t₁ from t₁ ≠ t₂.
Cvc.Proof.View.trans {P F T : Type} (premises : Array P) : Cvc.Proof.View P F T
TRANS: t₁ = tₙ from the chain t₁ = t₂, …, tₙ₋₁ = tₙ.
Cvc.Proof.View.cong {P F T : Type} (premises : Array P) (app : T) : Cvc.Proof.View P F T
CONG: f(t₁, …, tₙ) = f(s₁, …, sₙ) from tᵢ = sᵢ, app being f(t₁, …, tₙ).
Used for operators of fixed arity, indexed ones and uninterpreted functions included.
Cvc.Proof.View.naryCong {P F T : Type} (premises : Array P) (app : T) : Cvc.Proof.View P F T
Cvc.Proof.View.pairwiseCong {P F T : Type} (premises : Array P) (app : T) : Cvc.Proof.View P F T
PAIRWISE_CONG: cong for a variadic, pairwise operator, which today means distinct.
Cvc.Proof.View.trueIntro {P F T : Type} (premise : P) : Cvc.Proof.View P F T
TRUE_INTRO: F = true from F.
Cvc.Proof.View.trueElim {P F T : Type} (premise : P) : Cvc.Proof.View P F T
TRUE_ELIM: F from F = true.
Cvc.Proof.View.falseIntro {P F T : Type} (premise : P) : Cvc.Proof.View P F T
FALSE_INTRO: F = false from ¬F.
Cvc.Proof.View.falseElim {P F T : Type} (premise : P) : Cvc.Proof.View P F T
FALSE_ELIM: ¬F from F = false.
Cvc.Proof.View.other {P F T : Type} (rule : cvc5.ProofRule) (premises : Array P) (args : Array T) : Cvc.Proof.View P F T
Any other step, as cvc5 gives it: a rule not decoded, or a step whose layout was not expected.
Which rules are decoded grows over time, so a pattern .other .SOME_RULE … stops matching
once that rule is decoded: match on the step's rule instead for a rule not decoded.
A typed step's view holds its formulas — an assumption, a pivot, a clause-form input — as Term Bool, so they are operands of the Boolean operators as they are. A term of any other sort stays sort-erased, as the arguments of a proof do: no rule fixes its sort.
def describe {s : Solver} : s.ProofView pc → String
| .assume f => s!"assume {f}"
| .scope _ fs => s!"scope, discharging {fs}"
| .contra .. => "contra"
| v => s!"{v.rule}"
#eval Env.runIO do
let s ← Solver.new
s.setOpt .smt_produceProofs true
let b ← Term.mkSymbolAs Bool "b"
s.assert b
s.assert (← smt! ¬ b)
let proofs ← s.checkSat
(ifUnsat := s.getUnsatProof)
for p in proofs do
for step in p do println! describe step.view
The examples below refute x ≥ 1, x ≤ 1 and f x ≠ f 1: arithmetic decides x = 1 and congruence does the rest, so the proof goes through two theories and through rewriting.
def congruence : Env Solver := do
let s ← Solver.new
s.setOpt .smt_produceProofs true
let f ← Term.mkSymbolAs (Int → Int) "f"
let x ← Term.mkSymbolAs Int "x"
smt! x ≥ 1 >>= s.assert
smt! x ≤ 1 >>= s.assert
smt! f x ≠ f 1 >>= s.assert
return s
A proof is a graph rather than a tree: cvc5 shares a sub-proof between the steps that use it. Every traversal visits a shared step once, telling steps apart by identity.
Cvc.Typed.Solver.Proof.fold.{u_1} {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) {m : Type → Type u_1} {σ : Type} [Monad m] (init : σ) (pre : s.Proof pc → s.ProofView pc → σ → m (Cvc.FoldPre σ) := fun x x_1 s => pure (Cvc.FoldPre.descend s)) (post : s.Proof pc → s.ProofView pc → σ → m (Cvc.FoldPost σ) := fun x x_1 s => pure (Cvc.FoldPost.continue s)) (revisit : Bool := false) : m σCvc.Typed.Solver.Proof.fold.{u_1} {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) {m : Type → Type u_1} {σ : Type} [Monad m] (init : σ) (pre : s.Proof pc → s.ProofView pc → σ → m (Cvc.FoldPre σ) := fun x x_1 s => pure (Cvc.FoldPre.descend s)) (post : s.Proof pc → s.ProofView pc → σ → m (Cvc.FoldPost σ) := fun x x_1 s => pure (Cvc.FoldPost.continue s)) (revisit : Bool := false) : m σ
Folds over the distinct steps of p, depth-first, with early exit, in any monad.
Each step is handed over with its view. pre is called on reaching a step, before its premises,
and can skip them or stop; post on leaving it, once its premises are done, and can stop. Both
default to carrying on.
A step shared by several others is visited once, on the first path that reaches it, unless
revisit is set — which can take exponentially long.
pre can end the fold early. The first resolution step reached is the SAT solver's refutation, and its premises are the clauses it resolved:
#eval Env.runIO do
let s ← congruence
let proofs ← s.checkSat
(ifUnsat := s.getUnsatProof)
for p in proofs do
let clauses : Array (Term Bool) :=
p.fold #[] (m := Id)
(pre := fun _ v acc => return match v with
| .chainMResolution ps _ =>
.stop (ps.map (·.getResult))
| _ => .descend acc)
for c in clauses do println! "- {c}"
The fold runs in the caller's monad, and break ends a for loop over the steps just as stop ends a fold.
Cvc.Typed.Solver.Proof.foldUp.{u_1} {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) {m : Type → Type u_1} {β : Type} [Monad m] (f : s.Proof pc → Cvc.Proof.View β (Cvc.Typed.Term Bool) Cvc.Untyped.Term → m β) : m βCvc.Typed.Solver.Proof.foldUp.{u_1} {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) {m : Type → Type u_1} {β : Type} [Monad m] (f : s.Proof pc → Cvc.Proof.View β (Cvc.Typed.Term Bool) Cvc.Untyped.Term → m β) : m β
Computes a value for every distinct step of p, bottom-up, and answers the root's.
f is handed each step with its view, the premises of which are the values already computed for
them. It is called once per distinct step, so a sub-proof shared by many steps is computed once,
which is what rebuilding a proof elsewhere wants. To end early, throw, in Except for instance.
foldUp hands each step a view whose premises are the values already computed for them — the shape of anything that rebuilds a proof elsewhere. Ending early is the monad's business: here, a rebuild gives up on the first step it has no rule for.
#eval Env.runIO do
let s ← congruence
let proofs ← s.checkSat
(ifUnsat := s.getUnsatProof)
for p in proofs do
let rebuilt : Except String Nat :=
p.foldUp fun q v => match v with
| .other .. =>
throw s!"no rule for {q.getRule}"
| v => return v.premises.foldl (· + ·) 1
match rebuilt with
| .ok n => println! "rebuilt, {n} steps as a tree"
| .error e => println! e
Cvc.Typed.Solver.Proof.freeAssumptions {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : Cvc.Typed.Terms BoolCvc.Typed.Solver.Proof.freeAssumptions {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : Cvc.Typed.Terms Bool
The assumptions p leaves open, in the order they are first reached.
These are the formulas of its ASSUME steps that no enclosing SCOPE discharges.
A proof cvc5 answers for the full component leaves none open, its root scope discharging the
assertions. Below that scope, they are the assertions the refutation actually uses.
A full proof leaves no assumption open, its root scope discharging the assertions. Below that scope, the open assumptions are the assertions the refutation actually uses:
#eval Env.runIO do
let s ← congruence
let proofs ← s.checkSat
(ifUnsat := s.getUnsatProof)
for p in proofs do
if let .scope outer _ := p.view then
if let .scope refutation _ := outer.view then
for f in refutation.freeAssumptions do
println! "- {f}"
The theoryLemmas component answers one proof per theory lemma, whose conclusion is the lemma. Solver.Proofs.fold and Solver.Proofs.foldUp traverse several proofs at once.
#eval Env.runIO do
let s ← congruence
let lemmas ← s.checkSat (ifUnsat :=
s.getUnsatProof .theoryLemmas)
for p in lemmas do
println! "lemma : {p.getResult}"
println! "steps : {p.size}"
Cvc.Typed.Solver.Proof.ruleCounts {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : Array (cvc5.ProofRule × Nat)Cvc.Typed.Solver.Proof.ruleCounts {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : Array (cvc5.ProofRule × Nat)
How many distinct steps of p apply each rule, rules in the order they are first reached.
Cvc.Typed.Solver.Proof.trusted {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : s.Proofs pcCvc.Typed.Solver.Proof.trusted {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : s.Proofs pc
The distinct steps of p that cvc5 does not justify, in the order they are first reached.
These are its TRUST and TRUST_THEORY_REWRITE steps.
Cvc.Typed.Solver.Proof.size {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : NatCvc.Typed.Solver.Proof.size {pc : Cvc.Proof.Component} [Cvc.Ω] {s : Cvc.Typed.Solver} (p : s.Proof pc) : Nat
The number of distinct steps in p.
Each layer has its own proof type. The typed one is the sort-erased one under a type of its own, so toUntyped (or relax) and toTyped cross for free, and a sort-erased function never answers for a typed proof by accident. The two views decode the same steps; they differ only in how formulas are typed.