(proof-new) Minor documentation sync (#6592)

5 files changed, 26 insertions, 28 deletions

diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 3146160bb..215c61210 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -76,7 +76,8 @@ class ProofNodeUpdaterCallback
  * (ProofNodeUpdaterCallback::shouldUpdate)
  * and overwrites them based on the update procedure of the callback
  * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that
- * should be filled in the callback for each ProofNode to update.
+ * should be filled in the callback for each ProofNode to update. This update
+ * process is applied in a *pre-order* traversal.
  */
 class ProofNodeUpdater
 {
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index c2a6a30f6..f4e8078dc 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -52,6 +52,7 @@ const char* toString(PfRule id)
     case PfRule::FACTORING: return "FACTORING";
     case PfRule::REORDERING: return "REORDERING";
     case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION";
+    case PfRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST";
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
     case PfRule::MODUS_PONENS: return "MODUS_PONENS";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index e4c33a840..9771dda31 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -41,6 +41,10 @@ namespace cvc5 {
  * (2) SCOPE, which closes the scope of assumptions.
  * The core rules additionally correspond to generic operations that are done
  * internally on nodes, e.g. calling Rewriter::rewrite.
+ *
+ * Rules with prefix MACRO_ are those that can be defined in terms of other
+ * rules. These exist for convienience. We provide their definition in the line
+ * "Macro:".
  */
 enum class PfRule : uint32_t
 {
@@ -181,7 +185,6 @@ enum class PfRule : uint32_t
   // where F' and G' are the result of each side of the equation above. Here,
   // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
   MACRO_SR_PRED_TRANSFORM,
-
   //================================================= Processing rules
   // ======== Remove Term Formulas Axiom
   // Children: none
@@ -214,7 +217,7 @@ enum class PfRule : uint32_t
   // the quantifiers rewriter involves constructing new bound variables that are
   // not guaranteed to be consistent on each call.
   THEORY_REWRITE,
-  // The rules in this section have the signature of a "trusted rule":
+  // The remaining rules in this section have the signature of a "trusted rule":
   //
   // Children: none
   // Arguments: (F)
@@ -907,8 +910,8 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
   // where
-  //   r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))),
-  //   r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))).
+  //   r_t = (skolem (suf t1 (str.len s1)))),
+  //   r_s = (skolem (suf s1 (str.len t1)))).
   //
   // or the reverse form of the above:
   //
@@ -918,9 +921,8 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
   // where
-  //   r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
-  //   s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2)
-  //   (str.len t2))))).
+  //   r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))),
+  //   r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))).
   //
   // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
   // (pre x n) is shorthand for (str.substr x 0 n).
@@ -932,7 +934,7 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (= t1 (str.++ c r))
   // where
-  //   r = (witness ((z String)) (= z (suf t1 1))).
+  //   r = (skolem (suf t1 1)).
   //
   // or the reverse form of the above:
   //
@@ -942,7 +944,7 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (= t2 (str.++ r c))
   // where
-  //   r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))).
+  //   r = (skolem (pre t2 (- (str.len t2) 1))).
   CONCAT_CSPLIT,
   // ======== Concat length propagate
   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
@@ -951,7 +953,7 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (= t1 (str.++ s1 r_t))
   // where
-  //   r_t = (witness ((z String)) (= z (suf t1 (str.len s1))))
+  //   r_t = (skolem (suf t1 (str.len s1)))
   //
   // or the reverse form of the above:
   //
@@ -961,8 +963,7 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (= t2 (str.++ r_t s2))
   // where
-  //   r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
-  //   s2))))).
+  //   r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))).
   CONCAT_LPROP,
   // ======== Concat constant propagate
   // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
@@ -975,7 +976,7 @@ enum class PfRule : uint32_t
   //   w3 is (pre w2 p),
   //   w4 is (suf w2 p),
   //   p = Word::overlap((suf w2 1), w1),
-  //   r = (witness ((z String)) (= z (suf t1 (str.len w3)))).
+  //   r = (skolem (suf t1 (str.len w3))).
   // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
   // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
   //
@@ -991,7 +992,7 @@ enum class PfRule : uint32_t
   //   w3 is (suf w2 (- (str.len w2) p)),
   //   w4 is (pre w2 (- (str.len w2) p)),
   //   p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
-  //   r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))).
+  //   r = (skolem (pre t2 (- (str.len t2) (str.len w3)))).
   // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
   // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
   // be contained in t2.
@@ -1007,14 +1008,14 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
   // where
-  //   w1 is (witness ((z String)) (= z (pre t n)))
-  //   w2 is (witness ((z String)) (= z (suf t n)))
+  //   w1 is (skolem (pre t n))
+  //   w2 is (skolem (suf t n))
   STRING_DECOMPOSE,
   // ======== Length positive
   // Children: none
   // Arguments: (t)
   // ---------------------
-  // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0)))
+  // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
   STRING_LENGTH_POS,
   // ======== Length non-empty
   // Children: (P1:(not (= t "")))
@@ -1030,15 +1031,15 @@ enum class PfRule : uint32_t
   // Conclusion: (and R (= t w))
   // where w = strings::StringsPreprocess::reduce(t, R, ...).
   // In other words, R is the reduction predicate for extended term t, and w is
-  //   (witness ((z T)) (= z t))
+  //   (skolem t)
   // Notice that the free variables of R are w and the free variables of t.
   STRING_REDUCTION,
   // ======== Eager Reduction
   // Children: none
-  // Arguments: (t, id?)
+  // Arguments: (t)
   // ---------------------
   // Conclusion: R
-  // where R = strings::TermRegistry::eagerReduce(t, id).
+  // where R = strings::TermRegistry::eagerReduce(t).
   STRING_EAGER_REDUCTION,
   //======================== Regular expressions
   // ======== Regular expression intersection
@@ -1141,7 +1142,6 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (<= i greatestIntLessThan(c)})
   INT_TIGHT_UB,
-
   // ======== Tightening Strict Integer Lower Bounds
   // Children: (P:(> i c))
   //         where i has integer type.
@@ -1149,7 +1149,6 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (>= i leastIntGreaterThan(c)})
   INT_TIGHT_LB,
-
   // ======== Trichotomy of the reals
   // Children: (A B)
   // Arguments: (C)
@@ -1161,14 +1160,12 @@ enum class PfRule : uint32_t
   //                 note that "not" here denotes arithmetic negation, flipping
   //                 >= to <, etc.
   ARITH_TRICHOTOMY,
-
   // ======== Arithmetic operator elimination
   // Children: none
   // Arguments: (t)
   // ---------------------
   // Conclusion: arith::OperatorElim::getAxiomFor(t)
   ARITH_OP_ELIM_AXIOM,
-
   // ======== Int Trust
   // Children: (P1 ... Pn)
   // Arguments: (Q)
@@ -1223,7 +1220,6 @@ enum class PfRule : uint32_t
   // Conclusion: (and (>= real.pi l) (<= real.pi u))
   // Where l (u) is a valid lower (upper) bound on pi.
   ARITH_TRANS_PI,
-
   //======== Exp at negative values
   // Children: none
   // Arguments: (t)
@@ -1289,7 +1285,6 @@ enum class PfRule : uint32_t
   // exponential function is the following:
   //   e^x = \sum_{n=0}^{\infty} x^n / n!
   ARITH_TRANS_EXP_APPROX_BELOW,
-
   //======== Sine is always between -1 and 1
   // Children: none
   // Arguments: (t)
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 53633a123..0968aa1f9 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -66,6 +66,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
     d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM);
     d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST);
     d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION);
+    d_pfpp->setEliminateRule(PfRule::MACRO_ARITH_SCALE_SUM_UB);
     if (options::proofGranularityMode()
         != options::ProofGranularityMode::REWRITE)
     {
diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
index 1606fbb50..c0b368e6e 100644
--- a/src/theory/eager_proof_generator.h
+++ b/src/theory/eager_proof_generator.h
@@ -130,7 +130,7 @@ class EagerProofGenerator : public ProofGenerator
    * @param isConflict Whether the returned trust node is a conflict (otherwise
    * it is a lemma),
    * @return The trust node corresponding to the fact that this generator has
-   * a proof of (children => exp), or of exp if children is empty.
+   * a proof of (exp => conc), or of conc if exp is empty.
    */
   TrustNode mkTrustNode(Node conc,
                         PfRule id,