Decision strategy: incorporate arrays. (#2495)

1 files changed, 29 insertions, 2 deletions

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<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; }