diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-14 22:15:37 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-14 22:15:37 -0700 |
commit | 2060f439c873c8b1928cbd5f54967571176f2aba (patch) | |
tree | 45fab904b632b6174ee66807081465693a5da83f /src/theory | |
parent | c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010 (diff) |
Refactor how assertions are added to decision engine (#2396)
Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 17 |
4 files changed, 19 insertions, 18 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 95a60afac..8c9b39ea4 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -67,10 +67,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) d_check_vts_lemma_lc = false; } -InstStrategyCegqi::~InstStrategyCegqi() -{ - -} +InstStrategyCegqi::~InstStrategyCegqi() {} bool InstStrategyCegqi::needsCheck(Theory::Effort e) { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 92a355348..95ec24df9 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1194,16 +1194,17 @@ bool MatchGen::reset_round(QuantConflictFind* p) d_qni_gterm_rep[it->first] = p->getRepresentative( it->second ); } if( d_type==typ_ground ){ - //int e = p->evaluate( d_n ); - //if( e==1 ){ + // int e = p->evaluate( d_n ); + // if( e==1 ){ // d_ground_eval[0] = p->d_true; //}else if( e==-1 ){ // d_ground_eval[0] = p->d_false; //} - //modified + // modified TermDb* tdb = p->getTermDatabase(); QuantifiersEngine* qe = p->getQuantifiersEngine(); - for( unsigned i=0; i<2; i++ ){ + for (unsigned i = 0; i < 2; i++) + { if (tdb->isEntailed(d_n, i == 0)) { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; @@ -1220,7 +1221,7 @@ bool MatchGen::reset_round(QuantConflictFind* p) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = tdb->getEntailedTerm(d_n[i]); + TNode t = tdb->getEntailedTerm(d_n[i]); if (qe->inConflict()) { return false; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index fe1dc30a4..09525712f 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -307,8 +307,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, } Trace("cegqi-engine") << "...success:" << std::endl; Trace("cegqi-engine") << ss.str(); - Trace("sygus-repair-const") << "Repaired constants in solution : " - << std::endl; + Trace("sygus-repair-const") + << "Repaired constants in solution : " << std::endl; Trace("sygus-repair-const") << ss.str(); return true; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 37276ac5e..b9c3ccc4e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -29,6 +29,7 @@ #include "options/options.h" #include "options/proof_options.h" #include "options/quantifiers_options.h" +#include "preprocessing/assertion_pipeline.h" #include "proof/cnf_proof.h" #include "proof/lemma_proof.h" #include "proof/proof_manager.h" @@ -53,6 +54,7 @@ using namespace std; +using namespace CVC4::preprocessing; using namespace CVC4::theory; namespace CVC4 { @@ -1818,8 +1820,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); } - std::vector<Node> additionalLemmas; - IteSkolemMap iteSkolemMap; + AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe Node ppNode = preprocess ? this->preprocess(node) : Node(node); @@ -1827,9 +1828,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Remove the ITEs Debug("ite") << "Remove ITE from " << ppNode << std::endl; additionalLemmas.push_back(ppNode); - d_tform_remover.run(additionalLemmas, iteSkolemMap); + additionalLemmas.updateRealAssertionsEnd(); + d_tform_remover.run(additionalLemmas.ref(), + additionalLemmas.getIteSkolemMap()); Debug("ite") << "..done " << additionalLemmas[0] << std::endl; - additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + additionalLemmas.replace(0, theory::Rewriter::rewrite(additionalLemmas[0])); if(Debug.isOn("lemma-ites")) { Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; @@ -1846,19 +1849,19 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // assert to prop engine d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); + additionalLemmas.replace(i, theory::Rewriter::rewrite(additionalLemmas[i])); d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. if(negated) { - additionalLemmas[0] = additionalLemmas[0].notNode(); + additionalLemmas.replace(0, additionalLemmas[0].notNode()); negated = false; } // assert to decision engine if(!removable) { - d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap); + d_decisionEngine->addAssertions(additionalLemmas); } // Mark that we added some lemmas |