diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-22 16:35:20 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-22 16:35:20 -0600 |
| commit | 4479383c2fd8a3b81ab63d66f843b09b5c9d0cd3 (patch) | |
| tree | f4bf404bac05fd8592a09fda981061311692e8e2 /src/theory/quantifiers_engine.h | |
| parent | 71d72df0437607723256bbd7b4f28cd6c89fe40f (diff) | |
Move quantifiers attributes to quantifiers registry (#5929)
This moves the utility class beneath quantifiers registry.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f8f92f2e9..f01158ee2 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -30,7 +30,6 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/skolemize.h" @@ -90,8 +89,6 @@ class QuantifiersEngine { quantifiers::TermDb* getTermDatabase() const; /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; - /** get quantifiers attributes */ - quantifiers::QuantAttributes* getQuantAttributes() const; /** get instantiate utility */ quantifiers::Instantiate* getInstantiate() const; /** get skolemize utility */ @@ -298,8 +295,6 @@ public: std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query; /** sygus term database */ std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb; - /** quantifiers attributes */ - std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; /** instantiate utility */ std::unique_ptr<quantifiers::Instantiate> d_instantiate; /** skolemize utility */ |