diff options
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
| -rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index b98088a71..d778a679e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -245,6 +245,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) // now, do instantiation-based merging for each of these terms Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl; //merge all pending equalities + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); while( !d_upendingAdds.empty() ){ Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl; std::vector< Node > pending; @@ -256,7 +257,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl; std::vector< Node > eq_terms; //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine - Node gt = getTermDatabase()->evaluateTerm(t); + Node gt = echeck->evaluateTerm(t); if( !gt.isNull() && gt!=t ){ eq_terms.push_back( gt ); } @@ -1362,7 +1363,8 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode } Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl; //get the representative of rhs with substitution subs - TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true ); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); + TNode grhs = echeck->getEntailedTerm(rhs, subs, true); Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl; if( !grhs.isNull() ){ if( glhs!=grhs ){ |