diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-26 20:45:26 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-26 20:45:26 -0600 |
| commit | 693ed2fd482791e29e5d86420d0aa2ac835b7260 (patch) | |
| tree | 010caa4fae9f97a62c2d5c3b2afe5ad842281911 /src/theory/quantifiers_engine.cpp | |
| parent | 524c2d9f44a7c4297422dd1356fe3dc377166180 (diff) | |
Use term canonizer utility locally in quantifiers (#5823)
Term canonization was used in two places, which are unrelated and don't need to share the instance.
Also removes a few unnecessary methods from QuantifiersEngine.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 83aafe33a..94f70a2d9 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -44,7 +44,6 @@ QuantifiersEngine::QuantifiersEngine( d_model(nullptr), d_builder(nullptr), d_term_util(new quantifiers::TermUtil), - d_term_canon(new expr::TermCanonize), d_term_db(new quantifiers::TermDb(qstate, qim, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), @@ -150,11 +149,6 @@ OutputChannel& QuantifiersEngine::getOutputChannel() /** get default valuation for the quantifiers engine */ Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); } -const LogicInfo& QuantifiersEngine::getLogicInfo() const -{ - return d_te->getLogicInfo(); -} - EqualityQuery* QuantifiersEngine::getEqualityQuery() const { return d_eq_query.get(); @@ -179,10 +173,6 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const { return d_term_util.get(); } -expr::TermCanonize* QuantifiersEngine::getTermCanonize() const -{ - return d_term_canon.get(); -} quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const { return d_quant_attr.get(); @@ -773,13 +763,6 @@ void QuantifiersEngine::preRegisterQuantifier(Node q) Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl; } -void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { - for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){ - std::set< Node > added; - getTermDatabase()->addTerm( *p, added ); - } -} - void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ if (reduceQuantifier(f)) { |