(proof-new) Improvements for theory engine (#5292)

Avoids use of macro rules in a few places.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 863c67a2b4ab174ce04587d813963d5b86c6d0ea..aaa0101483e85c9a413c8801390d08b3d25ca58b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1468,15 +1468,12 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
                                    PfRule::PREPROCESS_LEMMA);
           // ---------- from d_lazyProof -------------- from theory preprocess
           // lemma                       lemma = lemmap
-          // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
+          // ------------------------------------------ EQ_RESOLVE
           // lemmap
           std::vector<Node> pfChildren;
           pfChildren.push_back(lemma);
           pfChildren.push_back(tplemma.getProven());
-          std::vector<Node> pfArgs;
-          pfArgs.push_back(lemmap);
-          d_lazyProof->addStep(
-              lemmap, PfRule::MACRO_SR_PRED_TRANSFORM, pfChildren, pfArgs);
+          d_lazyProof->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
         }
       }
       tlemma = TrustNode::mkTrustLemma(lemmap, d_lazyProof.get());
@@ -1630,8 +1627,8 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
         {
           // ------------------------- explained  ---------- from theory
           // fullConflict => conflict              ~conflict
-          // --------------------------------------------
-          // MACRO_SR_PRED_TRANSFORM ~fullConflict
+          // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
+          // ~fullConflict
           children.push_back(conflict.notNode());
           args.push_back(mkMethodId(MethodId::SB_LITERAL));
           d_lazyProof->addStep(
@@ -1928,9 +1925,9 @@ theory::TrustNode TheoryEngine::getExplanation(
         Trace("te-proof-exp") << "...trivial" << std::endl;
         continue;
       }
-      // ------------- Via theory
-      // tExp => tConc              tExp
-      // ---------------------------------MACRO_SR_PRED_TRANSFORM
+      //       ------------- Via theory
+      // tExp  tExp => tConc
+      // ---------------------------------MODUS_PONENS
       // tConc
       if (trn.getGenerator() != nullptr)
       {
@@ -1945,12 +1942,9 @@ theory::TrustNode TheoryEngine::getExplanation(
         lcp->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
       }
       std::vector<Node> pfChildren;
-      pfChildren.push_back(proven);
       pfChildren.push_back(trn.getNode());
-      std::vector<Node> pfArgs;
-      pfArgs.push_back(tConc);
-      pfArgs.push_back(mkMethodId(MethodId::SB_FORMULA));
-      lcp->addStep(tConc, PfRule::MACRO_SR_PRED_TRANSFORM, pfChildren, pfArgs);
+      pfChildren.push_back(proven);
+      lcp->addStep(tConc, PfRule::MODUS_PONENS, pfChildren, {});
     }
     // store in the proof generator
     TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index fd6d1af27305d0934eb4b8cfdfd2cb6d30925acb..3626b623ad35c898ad42693f4aa3ac9587a60786 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -38,11 +38,11 @@
 #include "theory/interrupted.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
-#include "theory/substitutions.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
 #include "theory/trust_node.h"
+#include "theory/trust_substitutions.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"