diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 21:15:39 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-17 21:15:39 -0600 |
| commit | 0bd5ef36d2b773912c3049f8f3fed62eaf0fa68b (patch) | |
| tree | 10885ad08d1a3b7d311b21a8223183e8cfe611d1 /src/theory/quantifiers_engine.h | |
| parent | 7ca17deba3b0f0308bda304ac739caf43e9536c0 (diff) | |
Eliminate non-static members in term util (#5919)
This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.
This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2fbf6b70f..f8f92f2e9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -90,8 +90,6 @@ class QuantifiersEngine { quantifiers::TermDb* getTermDatabase() const; /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; - /** get term utilities */ - quantifiers::TermUtil* getTermUtil() const; /** get quantifiers attributes */ quantifiers::QuantAttributes* getQuantAttributes() const; /** get instantiate utility */ @@ -294,8 +292,6 @@ public: std::unique_ptr<quantifiers::FirstOrderModel> d_model; /** model builder */ std::unique_ptr<quantifiers::QModelBuilder> d_builder; - /** term utilities */ - std::unique_ptr<quantifiers::TermUtil> d_term_util; /** term database */ std::unique_ptr<quantifiers::TermDb> d_term_db; /** equality query class */ |