From 4a0637be2548b2ee4c29873c045246cb36e8d122 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Sep 2018 11:17:27 -0500 Subject: [PATCH] Decision strategy: incorporate arrays. (#2495) --- src/theory/arrays/kinds | 2 +- src/theory/arrays/theory_arrays.cpp | 59 ++++++++++++++++++++--------- src/theory/arrays/theory_arrays.h | 31 ++++++++++++++- 3 files changed, 72 insertions(+), 20 deletions(-) diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 2ae658e6b..1adbdb0b2 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -8,7 +8,7 @@ theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_ typechecker "theory/arrays/theory_arrays_type_rules.h" properties polite stable-infinite parametric -properties check propagate presolve getNextDecisionRequest +properties check propagate presolve rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4407d45d8..c21fda430 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -56,21 +56,30 @@ const bool d_solveWrite2 = false; //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, std::string name) +TheoryArrays::TheoryArrays(context::Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + std::string name) : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name), d_numRow(name + "theory::arrays::number of Row lemmas", 0), d_numExt(name + "theory::arrays::number of Ext lemmas", 0), d_numProp(name + "theory::arrays::number of propagations", 0), d_numExplain(name + "theory::arrays::number of explanations", 0), - d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", 0), - d_numSharedArrayVarSplits(name + "theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits(name + "theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts(name + "theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits(name + "theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts(name + "theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, name + "theory::arrays::pp" , true), + d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", + 0), + d_numSharedArrayVarSplits( + name + "theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits( + name + "theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts( + name + "theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits( + name + "theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts( + name + "theory::arrays::number of setModelVal conflicts", 0), + d_ppEqualityEngine(u, name + "theory::arrays::pp", true), d_ppFacts(u), // d_ppCache(u), d_literalsToPropagate(c), @@ -102,7 +111,8 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, d_readTableContext(new context::Context()), d_arrayMerges(c), d_inCheckModel(false), - d_proofReconstruction(&d_equalityEngine) + d_proofReconstruction(&d_equalityEngine), + d_dstrat(new TheoryArraysDecisionStrategy(this)) { smtStatisticsRegistry()->registerStat(&d_numRow); smtStatisticsRegistry()->registerStat(&d_numExt); @@ -171,7 +181,6 @@ void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } - ///////////////////////////////////////////////////////////////////////////// // PREPROCESSING ///////////////////////////////////////////////////////////////////////////// @@ -1243,6 +1252,9 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m) void TheoryArrays::presolve() { Trace("arrays")<<"Presolving \n"; + // add the decision strategy + getDecisionManager()->registerStrategy(DecisionManager::STRAT_ARRAYS, + d_dstrat.get()); } @@ -2133,16 +2145,14 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } } - -Node TheoryArrays::getNextDecisionRequest( unsigned& priority ) { +Node TheoryArrays::getNextDecisionRequest() +{ if(! d_decisionRequests.empty()) { Node n = d_decisionRequests.front(); d_decisionRequests.pop(); - priority = 2; return n; - } else { - return Node::null(); } + return Node::null(); } @@ -2268,6 +2278,21 @@ void TheoryArrays::conflict(TNode a, TNode b) { d_conflict = true; } +TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy( + TheoryArrays* ta) + : d_ta(ta) +{ +} +void TheoryArrays::TheoryArraysDecisionStrategy::initialize() {} +Node TheoryArrays::TheoryArraysDecisionStrategy::getNextDecisionRequest() +{ + return d_ta->getNextDecisionRequest(); +} +std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const +{ + return std::string("th_arrays_dec"); +} + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 363ad16ff..e0f187e33 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -249,8 +249,6 @@ class TheoryArrays : public Theory { // NOTIFICATIONS ///////////////////////////////////////////////////////////////////////////// - public: - Node getNextDecisionRequest(unsigned& priority) override; void presolve() override; void shutdown() override {} @@ -455,6 +453,35 @@ class TheoryArrays : public Theory { /** An equality-engine callback for proof reconstruction */ ArrayProofReconstruction d_proofReconstruction; + /** + * The decision strategy for the theory of arrays, which calls the + * getNextDecisionEngineRequest function below. + */ + class TheoryArraysDecisionStrategy : public DecisionStrategy + { + public: + TheoryArraysDecisionStrategy(TheoryArrays* ta); + /** initialize */ + void initialize() override; + /** get next decision request */ + Node getNextDecisionRequest() override; + /** identify */ + std::string identify() const override; + + private: + /** pointer to the theory of arrays */ + TheoryArrays* d_ta; + }; + /** an instance of the above decision strategy */ + std::unique_ptr d_dstrat; + /** get the next decision request + * + * If the "arrays-eager-index" option is enabled, then whenever a + * read-over-write lemma is generated, a decision request is also generated + * for the comparison between the indexes that appears in the lemma. + */ + Node getNextDecisionRequest(); + public: eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } -- 2.30.2