diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-17 12:26:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-17 12:26:03 -0500 |
| commit | 2bb23eca6e3a239c33f5f4eb2dd0056de0738686 (patch) | |
| tree | ffc149ba83f4ad739676859417451f34b69e54c7 /src/theory/quantifiers_engine.h | |
| parent | a983ec175a7b7a2c247274735b9740c417114d94 (diff) | |
Encapsulate relevant domain (#3293)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index e1fc742af..323158404 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -32,7 +32,6 @@ #include "theory/quantifiers/quant_epr.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" @@ -104,10 +103,6 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() const; //---------------------- end utilities - //---------------------- utilities (TODO move these utilities #1163) - /** get relevant domain */ - quantifiers::RelevantDomain* getRelevantDomain() const; - //---------------------- end utilities private: /** * Maps quantified formulas to the module that owns them, if any module has @@ -314,8 +309,6 @@ public: std::unique_ptr<inst::TriggerTrie> d_tr_trie; /** extended model object */ std::unique_ptr<quantifiers::FirstOrderModel> d_model; - /** relevant domain */ - std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; /** model builder */ std::unique_ptr<quantifiers::QModelBuilder> d_builder; /** utility for effectively propositional logic */ |