diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 13:27:27 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-28 13:27:27 -0600 |
| commit | 3234db430074e278258e6d687c07146a59769a92 (patch) | |
| tree | 17db55e1ff335c3998e1c4e172d174dc9f6e3b21 /src/theory/quantifiers_engine.h | |
| parent | 4cd2d73366aba081a38900ddc2f4f172ce9ed2f8 (diff) | |
Use standard equality engine information in quantifiers state (#5824)
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 126fca01f..74f432585 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -73,12 +73,12 @@ class QuantifiersEngine { OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ Valuation& getValuation(); + /** The quantifiers state object */ + quantifiers::QuantifiersState& getState(); + /** The quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& getInferenceManager(); //---------------------- end external interface //---------------------- utilities - /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine() const; - /** get equality query */ - EqualityQuery* getEqualityQuery() const; /** get the model builder */ quantifiers::QModelBuilder* getModelBuilder() const; /** get model */ @@ -110,11 +110,8 @@ class QuantifiersEngine { * * @param te The theory engine * @param dm The decision manager of the theory engine - * @param mee The master equality engine of the theory engine */ - void finishInit(TheoryEngine* te, - DecisionManager* dm, - eq::EqualityEngine* mee); + void finishInit(TheoryEngine* te, DecisionManager* dm); //---------------------- end private initialization /** * Maps quantified formulas to the module that owns them, if any module has @@ -227,8 +224,6 @@ public: void markRelevant(Node q); /** has added lemma */ bool hasAddedLemma() const; - /** is in conflict */ - bool inConflict() const; /** get current q effort */ QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } /** get number of waiting lemmas */ @@ -343,8 +338,6 @@ public: TheoryEngine* d_te; /** Reference to the decision manager of the theory engine */ DecisionManager* d_decManager; - /** Pointer to the master equality engine */ - eq::EqualityEngine* d_masterEqualityEngine; /** vector of utilities for quantifiers */ std::vector<QuantifiersUtil*> d_util; /** vector of modules for quantifiers */ |