diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-01 09:26:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-01 09:26:26 -0500 |
commit | c1d9bed7f73db9567f635f59cde134795e65c9ba (patch) | |
tree | cec6839b42cc6c691bbb888bd356f627d973e968 /src/theory/quantifiers_engine.h | |
parent | 79881c196e29ef341166e7a31c1183e8b537d069 (diff) |
Move some generic utilities out of quantifiers (#3139)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 61e9053f5..da207c58a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -36,6 +36,10 @@ namespace CVC4 { class TheoryEngine; +namespace expr { +class TermCanonize; +} + namespace theory { class QuantifiersEngine; @@ -47,7 +51,6 @@ namespace quantifiers { class TermDb; class TermDbSygus; class TermUtil; - class TermCanonize; class Instantiate; class Skolemize; class TermEnumeration; @@ -130,7 +133,7 @@ public: /** get term utilities */ quantifiers::TermUtil* getTermUtil() const; /** get term canonizer */ - quantifiers::TermCanonize* getTermCanonize() const; + expr::TermCanonize* getTermCanonize() const; /** get quantifiers attributes */ quantifiers::QuantAttributes* getQuantAttributes() const; /** get instantiate utility */ @@ -345,7 +348,7 @@ public: /** term utilities */ std::unique_ptr<quantifiers::TermUtil> d_term_util; /** term utilities */ - std::unique_ptr<quantifiers::TermCanonize> d_term_canon; + std::unique_ptr<expr::TermCanonize> d_term_canon; /** term database */ std::unique_ptr<quantifiers::TermDb> d_term_db; /** sygus term database */ |