smt_scope/items/proof.rs
1use std::{str::FromStr, sync::OnceLock};
2
3#[cfg(feature = "mem_dbg")]
4use mem_dbg::{MemDbg, MemSize};
5use strum::{EnumIter, IntoEnumIterator};
6
7use crate::{BoxSlice, FxHashMap, IString, StringTable};
8
9use super::{ProofIdx, StackIdx, TermId, TermIdx};
10
11/// A Z3 proof step and associated data. Represents a single step where z3
12/// proved a boolean expression. These steps have dependencies which combine to
13/// build up a proof tree. Parts of this tree may be under hypotheses in which
14/// case the solver tries to do a proof by contradiction (and the proved terms
15/// are only valid under these hypotheses).
16#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
17#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
18#[derive(Debug)]
19pub struct ProofStep {
20 /// The parsed term id of the proof step itself (corresponds to `ProofIdx`).
21 /// Only useful for debugging.
22 pub id: TermId,
23 /// The kind of proof step. Which logical rule was used to derive the
24 /// result.
25 pub kind: ProofStepKind,
26 /// The (boolean) term which this step proves. This might not necessarily be
27 /// a "full" proof if this step (transitively) depends on any hypotheses!
28 pub result: TermIdx,
29 /// The antecedents of this proof step.
30 pub prerequisites: BoxSlice<ProofIdx>,
31 /// The frame in which this proof step was created. The proof is forgotten
32 /// (and may be repeated later) when the frame is popped.
33 pub frame: StackIdx,
34}
35
36#[allow(non_camel_case_types)]
37#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
38#[cfg_attr(feature = "mem_dbg", copy_type)]
39#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
40#[derive(Debug, Clone, Copy, PartialEq, Eq, EnumIter)]
41/// Taken from
42/// [z3-sys](https://docs.rs/z3-sys/0.8.1/src/z3_sys/lib.rs.html#451). Update
43/// from there if more cases are added. A few marked cases were renamed to
44/// match z3's
45/// [ast.cpp](https://github.com/Z3Prover/z3/blob/54d30f26f72ce62f5dcb5a5258f632f84858714f/src/ast/ast.cpp#L778-L821).
46pub enum ProofStepKind {
47 /// Undef/Null proof object.
48 PR_UNDEF,
49 /// Proof for the expression 'true'.
50 ///
51 /// *Renamed from `PR_TRUE`*
52 PR_TRUE_AXIOM,
53 /// Proof for a fact asserted by the user.
54 PR_ASSERTED,
55 /// Proof for a fact (tagged as goal) asserted by the user.
56 PR_GOAL,
57 /// Given a proof for p and a proof for (implies p q), produces a proof for q.
58 ///
59 /// ```text
60 /// T1: p
61 /// T2: (implies p q)
62 /// [mp T1 T2]: q
63 /// ```
64 ///
65 /// The second antecedents may also be a proof for `(iff p q)`.
66 ///
67 /// *Renamed from `PR_MODUS_PONENS`*
68 PR_MP,
69 /// A proof for `(R t t)`, where `R` is a reflexive relation.
70 ///
71 /// This proof object has no antecedents.
72 ///
73 /// The only reflexive relations that are used are
74 /// equivalence modulo namings, equality and equivalence.
75 /// That is, `R` is either `~`, `=` or `iff`.
76 ///
77 /// *Renamed from `PR_REFLEXIVITY`*
78 PR_REFL,
79 /// Given an symmetric relation `R` and a proof for `(R t s)`,
80 /// produces a proof for `(R s t)`.
81 ///
82 /// ```text
83 /// T1: (R t s)
84 /// [symmetry T1]: (R s t)
85 /// ```
86 ///
87 /// `T1` is the antecedent of this proof object.
88 ///
89 /// *Renamed from `PR_SYMMETRY`*
90 PR_SYMM,
91 /// Given a transitive relation `R`, and proofs for `(R t s)` and
92 /// `(R s u)`, produces a proof for `(R t u)`.
93 ///
94 /// ```text
95 /// T1: (R t s)
96 /// T2: (R s u)
97 /// [trans T1 T2]: (R t u)
98 /// ```
99 ///
100 /// *Renamed from `PR_TRANSITIVITY`*
101 PR_TRANS,
102 /// Condensed transitivity proof.
103 ///
104 /// It combines several symmetry and transitivity proofs.
105 ///
106 /// Example:
107 ///
108 /// ```text
109 /// T1: (R a b)
110 /// T2: (R c b)
111 /// T3: (R c d)
112 /// [trans* T1 T2 T3]: (R a d)
113 /// ```
114 ///
115 /// `R` must be a symmetric and transitive relation.
116 ///
117 /// Assuming that this proof object is a proof for `(R s t)`, then
118 /// a proof checker must check if it is possible to prove `(R s t)`
119 /// using the antecedents, symmetry and transitivity. That is,
120 /// if there is a path from `s` to `t`, if we view every
121 /// antecedent `(R a b)` as an edge between `a` and `b`.
122 ///
123 /// *Renamed from `PR_TRANSITIVITY_STAR`*
124 PR_TRANS_STAR,
125 /// Monotonicity proof object.
126 ///
127 /// ```text
128 /// T1: (R t_1 s_1)
129 /// ...
130 /// Tn: (R t_n s_n)
131 /// [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))
132 /// ```
133 ///
134 /// Remark: if `t_i == s_i`, then the antecedent `Ti` is suppressed.
135 /// That is, reflexivity proofs are suppressed to save space.
136 PR_MONOTONICITY,
137 /// Given a proof for `(~ p q)`, produces a proof for
138 /// `(~ (forall (x) p) (forall (x) q))`.
139 ///
140 /// ```text
141 /// T1: (~ p q)
142 /// [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
143 /// ```
144 PR_QUANT_INTRO,
145
146 /// Given a proof `p`, produces a proof of `lambda x . p`, where `x` are free
147 /// variables in `p`.
148 ///
149 /// ```text
150 /// T1: f
151 /// [proof-bind T1] forall (x) f
152 /// ```
153 ///
154 /// *Renamed from `PR_BIND`*
155 PR_PROOF_BIND,
156 /// Distributivity proof object.
157 ///
158 /// Given that `f (= or)` distributes over `g (= and)`, produces a proof for
159 ///
160 /// ```text
161 /// (= (f a (g c d))
162 /// (g (f a c) (f a d)))
163 /// ```
164 ///
165 /// If `f` and `g` are associative, this proof also justifies the following equality:
166 ///
167 /// ```text
168 /// (= (f (g a b) (g c d))
169 /// (g (f a c) (f a d) (f b c) (f b d)))
170 /// ```
171 ///
172 /// where each `f` and `g` can have arbitrary number of arguments.
173 ///
174 /// This proof object has no antecedents.
175 ///
176 /// Remark: This rule is used by the CNF conversion pass and
177 /// instantiated by `f,
178 PR_DISTRIBUTIVITY,
179 /// Given a proof for `(and l_1 ... l_n)`, produces a proof
180 /// for `l_i`.
181 ///
182 /// ```text
183 /// T1: (and l_1 ... l_n)
184 /// [and-elim T1]: l_i
185 /// ```
186 PR_AND_ELIM,
187 /// Given a proof for `(not (or l_1 ... l_n))`, produces a
188 /// proof for `(not l_i)`.
189 ///
190 /// ```text
191 /// T1: (not (or l_1 ... l_n))
192 /// [not-or-elim T1]: (not l_i)
193 /// ```
194 PR_NOT_OR_ELIM,
195 /// A proof for a local rewriting step `(= t s)`.
196 ///
197 /// The head function symbol of `t` is interpreted.
198 ///
199 /// This proof object has no antecedents.
200 ///
201 /// The conclusion of a rewrite rule is either an equality `(= t s)`,
202 /// an equivalence `(iff t s)`, or equi-satisfiability `(~ t s)`.
203 ///
204 /// Remark: if `f` is `bool`, then `=` is `iff`.
205 ///
206 /// Examples:
207 ///
208 /// ```text
209 /// (= (+ x 0) x)
210 /// (= (+ x 1 2) (+ 3 x))
211 /// (iff (or x false) x)
212 /// ```
213 PR_REWRITE,
214 /// A proof for rewriting an expression `t` into an expression `s`.
215 ///
216 /// This proof object can have `n` antecedents. The antecedents are
217 /// proofs for equalities used as substitution rules.
218 ///
219 /// The object is also used in a few cases. The cases are:
220 ///
221 /// - When applying contextual simplification `(CONTEXT_SIMPLIFIER=true)`.
222 /// - When converting bit-vectors to Booleans `(BIT2BOOL=true)`.
223 PR_REWRITE_STAR,
224 /// A proof for `(iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r)))`.
225 ///
226 /// This proof object has no antecedents.
227 PR_PULL_QUANT,
228 /// A proof for:
229 ///
230 /// ```text
231 /// (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
232 /// (and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
233 /// ...
234 /// (forall (x_1 ... x_m) p_n[x_1 ... x_m])))
235 /// ```
236 ///
237 /// This proof object has no antecedents.
238 PR_PUSH_QUANT,
239 /// A proof for
240 ///
241 /// ```text
242 /// (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
243 /// (forall (x_1 ... x_n) p[x_1 ... x_n]))
244 /// ```
245 ///
246 /// It is used to justify the elimination of unused variables.
247 ///
248 /// This proof object has no antecedents.
249 ///
250 /// *Renamed from `PR_ELIM_UNUSED_VARS`*
251 PR_ELIM_UNUSED,
252 /// A proof for destructive equality resolution:
253 ///
254 /// ```text
255 /// (iff (forall (x) (or (not (= x t)) P[x])) P[t])
256 /// ```
257 ///
258 /// if `x` does not occur in `t`.
259 ///
260 /// This proof object has no antecedents.
261 ///
262 /// Several variables can be eliminated simultaneously.
263 PR_DER,
264 /// A proof of `(or (not (forall (x) (P x))) (P a))`.
265 PR_QUANT_INST,
266 /// Mark a hypothesis in a natural deduction style proof.
267 PR_HYPOTHESIS,
268 /// ```text
269 /// T1: false
270 /// [lemma T1]: (or (not l_1) ... (not l_n))
271 /// ```
272 ///
273 /// This proof object has one antecedent: a hypothetical proof for false.
274 ///
275 /// It converts the proof in a proof for `(or (not l_1) ... (not l_n))`,
276 /// when `T1` contains the open hypotheses: `l_1, ..., l_n`.
277 ///
278 /// The hypotheses are closed after an application of a lemma.
279 ///
280 /// Furthermore, there are no other open hypotheses in the subtree covered by
281 /// the lemma.
282 PR_LEMMA,
283 /// ```text
284 /// T1: (or l_1 ... l_n l_1' ... l_m')
285 /// T2: (not l_1)
286 /// ...
287 /// T(n+1): (not l_n)
288 /// [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
289 /// ```
290 PR_UNIT_RESOLUTION,
291 /// ```text
292 /// T1: p
293 /// [iff-true T1]: (iff p true)
294 /// ```
295 PR_IFF_TRUE,
296 /// ```text
297 /// T1: (not p)
298 /// [iff-false T1]: (iff p false)
299 /// ```
300 PR_IFF_FALSE,
301 /// ```text
302 /// [comm]: (= (f a b) (f b a))
303 /// ```
304 ///
305 /// `f` is a commutative operator.
306 ///
307 /// This proof object has no antecedents.
308 ///
309 /// Remark: if `f` is `bool`, then `=` is `iff`.
310 PR_COMMUTATIVITY,
311 /// Proof object used to justify Tseitin's like axioms:
312 ///
313 /// ```text
314 /// (or (not (and p q)) p)
315 /// (or (not (and p q)) q)
316 /// (or (not (and p q r)) p)
317 /// (or (not (and p q r)) q)
318 /// (or (not (and p q r)) r)
319 /// ...
320 /// (or (and p q) (not p) (not q))
321 /// (or (not (or p q)) p q)
322 /// (or (or p q) (not p))
323 /// (or (or p q) (not q))
324 /// (or (not (iff p q)) (not p) q)
325 /// (or (not (iff p q)) p (not q))
326 /// (or (iff p q) (not p) (not q))
327 /// (or (iff p q) p q)
328 /// (or (not (ite a b c)) (not a) b)
329 /// (or (not (ite a b c)) a c)
330 /// (or (ite a b c) (not a) (not b))
331 /// (or (ite a b c) a (not c))
332 /// (or (not (not a)) (not a))
333 /// (or (not a) a)
334 /// ```
335 ///
336 /// This proof object has no antecedents.
337 ///
338 /// Note: all axioms are propositional tautologies.
339 /// Note also that `and` and `or` can take multiple arguments.
340 /// You can recover the propositional tautologies by
341 /// unfolding the Boolean connectives in the axioms a small
342 /// bounded number of steps `(=3)`.
343 PR_DEF_AXIOM,
344 /// Introduces a name for a formula/term.
345 ///
346 /// Suppose `e` is an expression with free variables `x`, and
347 /// `def-intro` introduces the name `n(x)`. The possible cases are:
348 ///
349 /// When e is of Boolean type:
350 ///
351 /// ```text
352 /// [def-intro]: (and (or n (not e)) (or (not n) e))
353 /// ```
354 ///
355 /// or:
356 ///
357 /// ```text
358 /// [def-intro]: (or (not n) e)
359 /// ```
360 ///
361 /// when e only occurs positively.
362 ///
363 /// When e is of the form `(ite cond th el)`:
364 ///
365 /// ```text
366 /// [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
367 /// ```
368 ///
369 /// Otherwise:
370 ///
371 /// ```text
372 /// [def-intro]: (= n e)
373 /// ```
374 ///
375 /// *Renamed from `PR_DEF_INTRO`*
376 PR_INTRO_DEF,
377 /// ```text
378 /// [apply-def T1]: F ~ n
379 /// ```
380 ///
381 /// `F` is 'equivalent' to `n`, given that `T1` is a proof that
382 /// `n` is a name for `F`.
383 PR_APPLY_DEF,
384 /// ```text
385 /// T1: (iff p q)
386 /// [iff~ T1]: (~ p q)
387 /// ```
388 PR_IFF_OEQ,
389 /// Proof for a (positive) NNF step. Example:
390 ///
391 /// ```text
392 /// T1: (not s_1) ~ r_1
393 /// T2: (not s_2) ~ r_2
394 /// T3: s_1 ~ r_1'
395 /// T4: s_2 ~ r_2'
396 /// [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2)
397 /// (and (or r_1 r_2') (or r_1' r_2)))
398 /// ```
399 ///
400 /// The negation normal form steps `NNF_POS` and `NNF_NEG` are used in the
401 /// following cases:
402 ///
403 /// - When creating the NNF of a positive force quantifier.
404 /// The quantifier is retained (unless the bound variables are eliminated).
405 /// Example:
406 /// ```text
407 /// T1: q ~ q_new
408 /// [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
409 /// ```
410 /// - When recursively creating NNF over Boolean formulas, where the top-level
411 /// connective is changed during NNF conversion. The relevant Boolean connectives
412 /// for `NNF_POS` are `implies`, `iff`, `xor`, `ite`.
413 /// `NNF_NEG` furthermore handles the case where negation is pushed
414 /// over Boolean connectives `and` and `or`.
415 PR_NNF_POS,
416 /// Proof for a (negative) NNF step. Examples:
417 ///
418 /// ```text
419 /// T1: (not s_1) ~ r_1
420 /// ...
421 /// Tn: (not s_n) ~ r_n
422 /// [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
423 /// ```
424 ///
425 /// and
426 ///
427 /// ```text
428 /// T1: (not s_1) ~ r_1
429 /// ...
430 /// Tn: (not s_n) ~ r_n
431 /// [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
432 /// ```
433 ///
434 /// and
435 ///
436 /// ```text
437 /// T1: (not s_1) ~ r_1
438 /// T2: (not s_2) ~ r_2
439 /// T3: s_1 ~ r_1'
440 /// T4: s_2 ~ r_2'
441 /// [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
442 /// (and (or r_1 r_2) (or r_1' r_2')))
443 /// ```
444 PR_NNF_NEG,
445 /// Proof for:
446 ///
447 /// ```text
448 /// [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
449 /// [sk]: (~ (exists x (p x y)) (p (sk y) y))
450 /// ```
451 ///
452 /// This proof object has no antecedents.
453 ///
454 /// *Renamed from `PR_SKOLEMIZE`*
455 PR_SK,
456 /// Modus ponens style rule for equi-satisfiability.
457 ///
458 /// ```text
459 /// T1: p
460 /// T2: (~ p q)
461 /// [mp~ T1 T2]: q
462 /// ```
463 ///
464 /// *Renamed from `PR_MODUS_PONENS_OEQ`*
465 PR_MP_OEQ,
466 /// Generic proof for theory lemmas.
467 ///
468 /// The theory lemma function comes with one or more parameters.
469 ///
470 /// The first parameter indicates the name of the theory.
471 ///
472 /// For the theory of arithmetic, additional parameters provide hints for
473 /// checking the theory lemma.
474 ///
475 /// The hints for arithmetic are:
476 ///
477 /// - `farkas` - followed by rational coefficients. Multiply the coefficients to the
478 /// inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
479 /// - `triangle-eq` - Indicates a lemma related to the equivalence:
480 /// ```text
481 /// (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
482 /// ```
483 /// - `gcd-test` - Indicates an integer linear arithmetic lemma that uses a gcd test.
484 PR_TH_LEMMA,
485 /// Hyper-resolution rule.
486 ///
487 /// The premises of the rules is a sequence of clauses.
488 /// The first clause argument is the main clause of the rule.
489 /// with a literal from the first (main) clause.
490 ///
491 /// Premises of the rules are of the form
492 ///
493 /// ```text
494 /// (or l0 l1 l2 .. ln)
495 /// ```
496 ///
497 /// or
498 ///
499 /// ```text
500 /// (=> (and l1 l2 .. ln) l0)
501 /// ```
502 ///
503 /// or in the most general (ground) form:
504 ///
505 /// ```text
506 /// (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))
507 /// ```
508 ///
509 /// In other words we use the following (Prolog style) convention for Horn
510 /// implications:
511 ///
512 /// - the head of a Horn implication is position 0,
513 /// - the first conjunct in the body of an implication is position 1
514 /// - the second conjunct in the body of an implication is position 2
515 ///
516 /// For general implications where the head is a disjunction, the
517 /// first n positions correspond to the n disjuncts in the head.
518 /// The next m positions correspond to the m conjuncts in the body.
519 ///
520 /// The premises can be universally quantified so that the most
521 /// general non-ground form is:
522 ///
523 /// ```text
524 /// (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))
525 /// ```
526 ///
527 /// The hyper-resolution rule takes a sequence of parameters.
528 /// The parameters are substitutions of bound variables separated by pairs
529 /// of literal positions from the main clause and side clause.
530 PR_HYPER_RESOLVE,
531
532 /// Unrecognised proof step was encountered.
533 OTHER(IString),
534}
535
536impl ProofStepKind {
537 pub fn to_z3_string(self) -> Result<String, IString> {
538 let kind_str = format!("{self:?}");
539 let kind_str = kind_str.strip_prefix("PR_").ok_or_else(|| {
540 let Self::OTHER(istr) = self else {
541 unreachable!("The variant `ProofStepKind::{self:?}` does not start with \"PR_\"!");
542 };
543 istr
544 })?;
545 let kind_str = kind_str
546 .replace("_STAR", "*")
547 .replace("_OEQ", "~")
548 .replace('_', "-")
549 .to_ascii_lowercase();
550 Ok(kind_str)
551 }
552
553 pub fn is_trivial(self) -> bool {
554 use ProofStepKind::*;
555 matches!(
556 self,
557 PR_MP
558 | PR_REWRITE
559 | PR_MONOTONICITY
560 | PR_TRANS
561 | PR_REFL
562 | PR_COMMUTATIVITY
563 | PR_IFF_TRUE
564 | PR_IFF_FALSE
565 | PR_SYMM
566 )
567 }
568
569 pub fn is_hypothesis(self) -> bool {
570 matches!(self, ProofStepKind::PR_HYPOTHESIS)
571 }
572
573 pub fn is_asserted(self) -> bool {
574 matches!(self, ProofStepKind::PR_ASSERTED)
575 }
576
577 pub fn is_quant_inst(self) -> bool {
578 matches!(self, ProofStepKind::PR_QUANT_INST)
579 }
580
581 pub fn is_lemma(self) -> bool {
582 matches!(self, ProofStepKind::PR_LEMMA)
583 }
584}
585
586static SEARCH_MAP: OnceLock<FxHashMap<String, ProofStepKind>> = OnceLock::new();
587
588impl FromStr for ProofStepKind {
589 type Err = ();
590 fn from_str(s: &str) -> Result<Self, Self::Err> {
591 let map = SEARCH_MAP.get_or_init(|| {
592 let mut map = FxHashMap::default();
593 for kind in ProofStepKind::iter() {
594 let Ok(kind_str) = kind.to_z3_string() else {
595 continue;
596 };
597 map.insert(kind_str, kind);
598 }
599 map
600 });
601 map.get(s).copied().ok_or(())
602 }
603}
604
605impl ProofStepKind {
606 pub fn parse_existing(strings: &StringTable, value: &str) -> Option<Self> {
607 match ProofStepKind::from_str(value) {
608 Ok(kind) => Some(kind),
609 Err(_) => strings.get(value).map(IString).map(ProofStepKind::OTHER),
610 }
611 }
612}