diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 31 |
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; } |