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/conjecture_generator.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/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 280c8c511..cd363eb70 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -312,7 +312,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) } Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { - return d_quantEngine->getTermCanonize()->getCanonicalFreeVar(tn, i); + return d_termCanon.getCanonicalFreeVar(tn, i); } bool ConjectureGenerator::isHandledTerm( TNode n ){ @@ -545,7 +545,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) if( d_tge.isRelevantTerm( eq ) ){ //make it canonical Trace("sg-proc-debug") << "get canonical " << eq << std::endl; - eq = d_quantEngine->getTermCanonize()->getCanonicalTerm(eq); + eq = d_termCanon.getCanonicalTerm(eq); }else{ eq = Node::null(); } @@ -700,8 +700,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) sum += it->second; for( unsigned i=0; i<it->second; i++ ){ gsubs_vars.push_back( - d_quantEngine->getTermCanonize()->getCanonicalFreeVar( - it->first, i)); + d_termCanon.getCanonicalFreeVar(it->first, i)); } } } |