Decision strategy: incorporate arrays. (#2495)

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 2ae658e6b29f835e55b48ce07376694ef3ee1af5..1adbdb0b22782e0b702094d2a784dca7b121e85f 100644 (file)
--- 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 4407d45d8f1e2acdc3f1767c1c3c9961ccf029c1..c21fda4306f64efb195f73e9c644f05992373f79 100644 (file)
--- 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 363ad16fffa16d3db65b3993b00327436141c8a2..e0f187e33e40a8f9d4c7520131b488ae892942fb 100644 (file)
--- 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<TheoryArraysDecisionStrategy> 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; }