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.cpp | |
| parent | 79881c196e29ef341166e7a31c1183e8b537d069 (diff) | |
Move some generic utilities out of quantifiers (#3139)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f86d82874..0281f50ec 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers_engine.h" +#include "expr/term_canonize.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" #include "smt/smt_statistics_registry.h" @@ -49,7 +50,6 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_canonize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" @@ -81,7 +81,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_builder(nullptr), d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), - d_term_canon(new quantifiers::TermCanonize), + d_term_canon(new expr::TermCanonize), d_term_db(new quantifiers::TermDb(c, u, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), @@ -330,7 +330,7 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const { return d_term_util.get(); } -quantifiers::TermCanonize* QuantifiersEngine::getTermCanonize() const +expr::TermCanonize* QuantifiersEngine::getTermCanonize() const { return d_term_canon.get(); } |