diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-17 21:24:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-17 21:24:10 -0500 |
commit | 4d2cc845273d078660a0e8f9946516edec93e25e (patch) | |
tree | 9a215c48f420cd2f24bd900fb3767ebc10f6349a /src/theory/theory_engine.cpp | |
parent | 7c249b3efdeeb51fd3dfc2571bc529c55880cf5c (diff) |
(proof-new) Improvements for theory engine (#5292)
Avoids use of macro rules in a few places.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 24 |
1 files changed, 9 insertions, 15 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 863c67a2b..aaa010148 100644 --- 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); |