[proof-new] Optimizing sat proof (#6324)

For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.

2 files changed, 19 insertions, 6 deletions

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 7f14adc38..5e638b55f 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -67,7 +67,7 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
                      std::vector<std::shared_ptr<ProofNode>>,
                      NodeHashFunction>
       assumptionsToExpand;
-  // invariant of the loop below, the first iteration notwhistanding:
+  // invariant of the loop below, the first iteration notwithstanding:
   //   visit = domain(assumptionsToExpand) \ domain(toConnect)
   std::vector<Node> visit{fact};
   std::unordered_map<Node, bool, NodeHashFunction> visited;
@@ -121,13 +121,22 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
       expr::getFreeAssumptionsMap(curPfn, famap);
       if (Trace.isOn("lazy-cdproofchain"))
       {
+        unsigned alreadyToVisit = 0;
         Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: free assumptions:\n";
+            << "LazyCDProofChain::getProofFor: " << famap.size()
+            << " free assumptions:\n";
         for (auto fap : famap)
         {
           Trace("lazy-cdproofchain")
               << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
+          alreadyToVisit +=
+              std::find(visit.begin(), visit.end(), fap.first) != visit.end()
+                  ? 1
+                  : 0;
         }
+        Trace("lazy-cdproofchain")
+            << "LazyCDProofChain::getProofFor: " << alreadyToVisit
+            << " already to visit\n";
       }
       // mark for post-traversal if we are controlling cycles
       if (d_cyclic)
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 7e0fc31fe..cec85cc99 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -320,6 +320,8 @@ enum class PfRule : uint32_t
   //   The result of the chain resolution is C, which is equal, in its set
   //   representation, to C_n'
   MACRO_RESOLUTION,
+  // As above but not checked
+  MACRO_RESOLUTION_TRUST,
 
   // ======== Split
   // Children: none
@@ -1048,8 +1050,9 @@ enum class PfRule : uint32_t
   //    its ki is negative). >< is always one of <, <=
   //    NB: this implies that lower bounds must have negative ki,
   //                      and upper bounds must have positive ki.
-  //    t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * poly_n)
-  //    t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n * const_n)
+  //    t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
+  //    poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
+  //    * const_n)
   ARITH_SCALE_SUM_UPPER_BOUNDS,
 
   // ======== Sum Upper Bounds
@@ -1134,8 +1137,9 @@ enum class PfRule : uint32_t
   // Arguments: (t, x, y, a, b, sgn)
   // ---------------------
   // Conclusion:
-  //   sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b)))
-  //   sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b)))
+  //   sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y
+  //   b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a)
+  //   (>= y b)))
   // Where x,y are real terms (variables or extended terms), t = (* x y)
   // (possibly under rewriting), a,b are real constants, and sgn is either -1
   // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b