From cd5cc65fed2c850100a6f00067d102b48d262742 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 1 Apr 2016 16:42:56 -0500 Subject: [PATCH] Improvements to equality inference module: add missing cases for solvable variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort. --- src/options/quantifiers_options | 2 + src/theory/quantifiers/equality_infer.cpp | 316 +++++++++++++++++----- src/theory/quantifiers/equality_infer.h | 24 +- src/theory/quantifiers/quant_util.cpp | 12 +- src/theory/quantifiers_engine.cpp | 37 ++- src/theory/quantifiers_engine.h | 4 +- 6 files changed, 307 insertions(+), 88 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 04b6e6813..5f23a02e0 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -66,6 +66,8 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false consider ground terms within bodies of quantified formulas for matching option inferArithTriggerEq --infer-arith-trigger-eq bool :default false infer equalities for trigger terms based on solving arithmetic equalities +option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false + record explanations for inferArithTriggerEq option smartTriggers --smart-triggers bool :default true enable smart triggers diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index f1dbb32fa..e4dbb9c43 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -26,13 +26,17 @@ using namespace std; namespace CVC4 { -EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_rep_exp(c) { +EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_solved( c, false ), d_master(c) +//, d_rep_exp(c), d_uselist(c) +{ } EqualityInference::EqualityInference( context::Context* c, bool trackExp ) : -d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){ +d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), +d_rep_to_eqc( c ), d_rep_exp( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){ d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + d_true = NodeManager::currentNM()->mkConst( true ); } EqualityInference::~EqualityInference(){ @@ -41,6 +45,86 @@ EqualityInference::~EqualityInference(){ } } +void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) { + if( std::find( exp.begin(), exp.end(), e )==exp.end() ){ + Trace("eq-infer-debug2") << "......add to explanation " << e << std::endl; + exp.push_back( e ); + } +} + +void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) { + NodeListMap::iterator re_i = d_rep_exp.find( eqc ); + if( re_i!=d_rep_exp.end() ){ + for( unsigned i=0; i<(*re_i).second->size(); i++ ){ + addToExplanation( exp, (*(*re_i).second)[i] ); + } + } + //for( unsigned i=0; id_rep_exp.size(); i++ ){ + // addToExplanation( exp, d_eqci[n]->d_rep_exp[i] ); + //} +} + +void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) { + NodeListMap::iterator re_i = d_rep_exp.find( eqc ); + NodeList* re; + if( re_i != d_rep_exp.end() ){ + re = (*re_i).second; + }else{ + re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator(d_c->getCMM()) ); + d_rep_exp.insertDataFromContextMemory( eqc, re ); + } + for( unsigned i=0; ipush_back( exp_to_add[i] ); + } + //for( unsigned i=0; id_rep_exp.push_back( exp_to_add[i] ); + //} +} + +Node EqualityInference::getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m ) { + if( !eqc->d_master.get().isNull() ){ + if( eqc->d_master.get()==t ){ + if( !new_m.isNull() && t!=new_m ){ + eqc->d_master = new_m; + updated = true; + return new_m; + }else{ + return t; + } + }else{ + Assert( d_eqci.find( eqc->d_master.get() )!=d_eqci.end() ); + EqcInfo * eqc_m = d_eqci[eqc->d_master.get()]; + Node m = getMaster( eqc->d_master.get(), eqc_m, updated, new_m ); + eqc->d_master = m; + return m; + } + }else{ + return Node::null(); + } +} + +//update the internal "master" representative of the equivalence class, return true if the merge was non-redundant +bool EqualityInference::updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ) { + bool updated = false; + Node m1 = getMaster( t1, eqc1, updated ); + if( m1.isNull() ){ + eqc1->d_master = t2; + if( eqc2->d_master.get().isNull() ){ + eqc2->d_master = t2; + } + return true; + }else{ + updated = false; + Node m2 = getMaster( t2, eqc2, updated, m1); + if( m2.isNull() ){ + eqc2->d_master = m1; + return true; + }else{ + return updated; + } + } +} + void EqualityInference::eqNotifyNewClass(TNode t) { if( t.getType().isReal() ){ Trace("eq-infer") << "Notify equivalence class : " << t << std::endl; @@ -52,56 +136,74 @@ void EqualityInference::eqNotifyNewClass(TNode t) { }else{ eqci = itec->second; } - std::map< Node, Node > msum; - if( QuantArith::getMonomialSum( t, msum ) ){ - eqci->d_valid = true; - bool changed = false; - std::vector< Node > children; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { - Node n = it->first; - if( !n.isNull() ){ - NodeMap::const_iterator itv = d_elim_vars.find( n ); - if( itv!=d_elim_vars.end() ){ - changed = true; - n = (*itv).second; - } - if( it->second.isNull() ){ - children.push_back( n ); + Assert( !eqci->d_valid.get() ); + if( !eqci->d_solved.get() ){ + //somewhat strange: t may not be in rewritten form + Node r = Rewriter::rewrite( t ); + std::map< Node, Node > msum; + if( QuantArith::getMonomialSum( r, msum ) ){ + Trace("eq-infer-debug2") << "...process monomial sum, size = " << msum.size() << std::endl; + eqci->d_valid = true; + bool changed = false; + std::vector< Node > exp; + std::vector< Node > children; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { + Trace("eq-infer-debug2") << "...process child " << it->first << ", " << it->second << std::endl; + if( !it->first.isNull() ){ + Node n = it->first; + BoolMap::const_iterator itv = d_elim_vars.find( n ); + if( itv!=d_elim_vars.end() ){ + changed = true; + Assert( d_eqci.find( n )!=d_eqci.end() ); + Assert( n!=t ); + Assert( d_eqci[n]->d_solved.get() ); + Trace("eq-infer-debug2") << "......its solved form is " << d_eqci[n]->d_rep.get() << std::endl; + if( d_trackExplain ){ + //track the explanation: justified by explanation for each substitution + addToExplanationEqc( exp, n ); + } + n = d_eqci[n]->d_rep; + Assert( !n.isNull() ); + } + if( it->second.isNull() ){ + children.push_back( n ); + }else{ + children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) ); + } }else{ - children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) ); + Assert( !it->second.isNull() ); + children.push_back( it->second ); } - }else{ - children.push_back( it->second ); } - } - Node r; - bool mvalid = true; - if( changed ){ - r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); - r = Rewriter::rewrite( r ); - msum.clear(); - if( !QuantArith::getMonomialSum( r, msum ) ){ - mvalid = false; + Trace("eq-infer-debug2") << "...children size = " << children.size() << std::endl; + bool mvalid = true; + if( changed ){ + r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); + Trace("eq-infer-debug2") << "...pre-rewrite : " << r << std::endl; + r = Rewriter::rewrite( r ); + msum.clear(); + if( !QuantArith::getMonomialSum( r, msum ) ){ + mvalid = false; + } + } + Trace("eq-infer") << "...value is " << r << std::endl; + setEqcRep( t, r, exp, eqci ); + if( mvalid ){ + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( !it->first.isNull() ){ + addToUseList( it->first, t ); + } + } } }else{ - r = t; - } - Trace("eq-infer") << "...value is " << r << std::endl; - setEqcRep( t, r, eqci ); - if( mvalid ){ - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( !it->first.isNull() ){ - addToUseList( it->first, t ); - } - } + eqci->d_valid = false; } - }else{ - eqci->d_valid = false; } } } void EqualityInference::addToUseList( Node used, Node eqc ) { +#if 1 NodeListMap::iterator ul_i = d_uselist.find( used ); NodeList* ul; if( ul_i != d_uselist.end() ){ @@ -111,26 +213,53 @@ void EqualityInference::addToUseList( Node used, Node eqc ) { d_uselist.insertDataFromContextMemory( used, ul ); } Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl; - (*ul).push_back( eqc ); + (*ul).push_back( eqc ); +#else + std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used ); + EqcInfo * eqci_used; + if( itu==d_eqci.end() ){ + eqci_used = new EqcInfo( d_c ); + d_eqci[used] = eqci_used; + }else{ + eqci_used = itu->second; + } + Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl; + eqci_used->d_uselist.push_back( eqc ); +#endif } -void EqualityInference::setEqcRep( Node t, Node r, EqcInfo * eqci ) { +void EqualityInference::setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ) { eqci->d_rep = r; - NodeMap::const_iterator itr = d_rep_to_eqc.find( r ); - if( itr==d_rep_to_eqc.end() ){ - d_rep_to_eqc[r] = t; - }else{ - //merge two equivalence classes - Node t2 = (*itr).second; - //check if it is valid - std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 ); - if( itc!=d_eqci.end() && itc->second->d_valid ){ - Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl; - Trace("eq-infer") << " since they both normalize to : " << r << std::endl; - d_pending_merges.push_back( t.eqNode( t2 ) ); - if( d_trackExplain ){ - //TODO - d_pending_merge_exp.push_back( t.eqNode( t2 ) ); + if( d_trackExplain ){ + addToExplanationEqc( t, exp_to_add ); + } + //if this is an active equivalence class + if( eqci->d_valid.get() ){ + Trace("eq-infer-debug") << "Set eqc rep " << t << " -> " << r << std::endl; + NodeMap::const_iterator itr = d_rep_to_eqc.find( r ); + if( itr==d_rep_to_eqc.end() ){ + d_rep_to_eqc[r] = t; + }else{ + //merge two equivalence classes + Node t2 = (*itr).second; + //check if it is valid + std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 ); + if( itc!=d_eqci.end() && itc->second->d_valid.get() ){ + //if we haven't already determined they should be merged + if( updateMaster( t, t2, eqci, itc->second ) ){ + Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl; + Trace("eq-infer") << " since they both normalize to : " << r << std::endl; + d_pending_merges.push_back( t.eqNode( t2 ) ); + if( d_trackExplain ){ + std::vector< Node > exp; + for( unsigned j=0; j<2; j++ ){ + addToExplanationEqc( exp, j==0 ? t : t2 ); + } + Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( AND, exp ) ); + Trace("eq-infer") << " explanation : " << exp_n << std::endl; + d_pending_merge_exp.push_back( exp_n ); + } + } } } } @@ -154,13 +283,30 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { if( QuantArith::getMonomialSumLit( eq, msum ) ){ Node v_solve; //solve for variables with no coefficient + if( Trace.isOn("eq-infer-debug2") ){ + Trace("eq-infer-debug2") << "Monomial sum : " << std::endl; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { + Trace("eq-infer-debug2") << " " << it->first << " * " << it->second << std::endl; + } + } for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) { Node n = it->first; - if( !n.isNull() && it->second.isNull() ){ - v_solve = n; - break; + if( !n.isNull() ){ + bool canSolve = false; + if( it->second.isNull() ){ + canSolve = true; + }else{ + //Assert( it->second.isConst() ); + Rational r = it->second.getConst(); + canSolve = r.isOne() || r.isNegativeOne(); + } + if( canSolve ){ + v_solve = n; + break; + } } } + Trace("eq-infer-debug") << "solve for variable : " << v_solve << std::endl; if( !v_solve.isNull() ){ //solve for v_solve Node veq; @@ -168,28 +314,61 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { Node v_value = veq[1]; Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl; Assert( d_elim_vars.find( v_solve )==d_elim_vars.end() ); - d_elim_vars[v_solve] = v_value; - + d_elim_vars[v_solve] = true; + //store value in eqc info + EqcInfo * eqci_solved; + std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( v_solve ); + if( itec==d_eqci.end() ){ + eqci_solved = new EqcInfo( d_c ); + d_eqci[v_solve] = eqci_solved; + }else{ + eqci_solved = itec->second; + } + eqci_solved->d_solved = true; + eqci_solved->d_rep = v_value; + //track the explanation + std::vector< Node > exp; + if( d_trackExplain ){ + //explanation is t1 = t2 + their explanations + exp.push_back( t1.eqNode( t2 ) ); + for( unsigned i=0; i<2; i++ ){ + addToExplanationEqc( exp, i==0 ? t1 : t2 ); + } + if( Trace.isOn("eq-infer-debug") ){ + Trace("eq-infer-debug") << " explanation for solving " << v_solve << " is "; + for( unsigned i=0; i new_use; for( std::map< Node, Node >::iterator itmm = msum.begin(); itmm != msum.end(); ++itmm ){ Node n = itmm->first; if( !n.isNull() && n!=v_solve ){ new_use.push_back( n ); + addToUseList( n, v_solve ); } } //go through all equivalence classes that may refer to v_solve std::map< Node, bool > processed; + processed[v_solve] = true; NodeListMap::iterator ul_i = d_uselist.find( v_solve ); if( ul_i != d_uselist.end() ){ NodeList* ul = (*ul_i).second; Trace("eq-infer-debug") << " use list size = " << ul->size() << std::endl; for( unsigned j=0; jsize(); j++ ){ Node r = (*ul)[j]; + //Trace("eq-infer-debug") << " use list size = " << eqci_solved->d_uselist.size() << std::endl; + //for( unsigned j=0; jd_uselist.size(); j++ ){ + // Node r = eqci_solved->d_uselist[j]; if( processed.find( r )==processed.end() ){ processed[r] = true; std::map< Node, EqcInfo * >::iterator itt = d_eqci.find( r ); - if( itt!=d_eqci.end() && itt->second->d_valid ){ + if( itt!=d_eqci.end() && ( itt->second->d_valid || itt->second->d_solved ) ){ std::map< Node, Node > msum2; if( QuantArith::getMonomialSum( itt->second->d_rep.get(), msum2 ) ){ std::map< Node, Node >::iterator itm = msum2.find( v_solve ); @@ -206,7 +385,7 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { Node rr = QuantArith::mkNode( msum2 ); rr = Rewriter::rewrite( rr ); Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl; - setEqcRep( itt->first, rr, itt->second ); + setEqcRep( itt->first, rr, exp, itt->second ); //update use list for( unsigned i=0; i d_rep; + //whether the eqc of this info is a representative and d_rep can been computed successfully context::CDO< bool > d_valid; - //explanation for why d_rep is how it is - NodeList d_rep_exp; + //whether the eqc of this info is a solved variable + context::CDO< bool > d_solved; + //master equivalence class (a union find) + context::CDO< Node > d_master; + //a vector of equalities t1=t2 for which eqNotifyMerge(t1,t2) was called that explains d_rep + //NodeList d_rep_exp; + //the list of other eqc where this variable may be appear + //NodeList d_uselist; }; /** track explanations */ bool d_trackExplain; /** information necessary for equivalence classes */ - NodeMap d_elim_vars; + BoolMap d_elim_vars; std::map< Node, EqcInfo * > d_eqci; NodeMap d_rep_to_eqc; + NodeListMap d_rep_exp; /** set eqc rep */ - void setEqcRep( Node t, Node r, EqcInfo * eqci ); + void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ); /** use list */ NodeListMap d_uselist; void addToUseList( Node used, Node eqc ); /** pending merges */ NodeList d_pending_merges; NodeList d_pending_merge_exp; + /** add to explanation */ + void addToExplanation( std::vector< Node >& exp, Node e ); + void addToExplanationEqc( std::vector< Node >& exp, Node eqc ); + void addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ); + /** for setting master/slave */ + Node getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m = Node::null() ); + bool updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ); public: //second argument is whether explanations should be tracked EqualityInference(context::Context* c, bool trackExp = false); diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index eb92b0f70..5344c0e88 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -33,16 +33,16 @@ bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ } } bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) { - if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ - if( msum.find(n[1])==msum.end() ){ - msum[n[1]] = n[0]; - return true; - } - }else if( n.isConst() ){ + if( n.isConst() ){ if( msum.find(Node::null())==msum.end() ){ msum[Node::null()] = n; return true; } + }else if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ + if( msum.find(n[1])==msum.end() ){ + msum[n[1]] = n[0]; + return true; + } }else{ if( msum.find(n)==msum.end() ){ msum[n] = Node::null(); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 01229a171..9e26abfd7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -417,7 +417,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ debugPrintEqualityEngine( "quant-engine-ee-pre" ); } Trace("quant-engine-debug2") << "Reset equality engine..." << std::endl; - d_eq_query->reset( e ); + if( !d_eq_query->reset( e ) ){ + flushLemmas(); + return; + } if( Trace.isOn("quant-engine-assert") ){ Trace("quant-engine-assert") << "Assertions : " << std::endl; @@ -1298,7 +1301,7 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){ if( options::inferArithTriggerEq() ){ - d_eq_inference = new quantifiers::EqualityInference( c ); + d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() ); }else{ d_eq_inference = NULL; } @@ -1308,28 +1311,44 @@ EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){ delete d_eq_inference; } -void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ +bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ d_int_rep.clear(); d_reset_count++; - processInferences( e ); + return processInferences( e ); } -void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { +bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { if( options::inferArithTriggerEq() ){ eq::EqualityEngine* ee = getEngine(); //updated implementation while( d_eqi_counter.get()getNumPendingMerges() ){ Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() ); + Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() ); Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl; + Trace("quant-engine-ee-proc") << " explanation : " << eq_exp << std::endl; Assert( ee->hasTerm( eq[0] ) ); Assert( ee->hasTerm( eq[1] ) ); - Assert( !ee->areDisequal( eq[0], eq[1], false ) ); - //just use itself as an explanation for now (should never be used, since equality engine should be consistent) - ee->assertEquality( eq, true, eq ); - d_eqi_counter = d_eqi_counter.get() + 1; + if( ee->areDisequal( eq[0], eq[1], false ) ){ + Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl; + if( Trace.isOn("term-db-lemma") ){ + Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl; + if( !d_qe->getTheoryEngine()->needCheck() ){ + Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl; + //this should really never happen (implies arithmetic is incomplete when sharing is enabled) + Assert( false ); + } + Trace("term-db-lemma") << " add split on : " << eq << std::endl; + } + d_qe->addSplit( eq ); + return false; + }else{ + ee->assertEquality( eq, true, eq_exp ); + d_eqi_counter = d_eqi_counter.get() + 1; + } } Assert( ee->consistent() ); } + return true; } bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index afde8c996..06b1c312b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -413,7 +413,7 @@ private: int d_reset_count; /** processInferences : will merge equivalence classes in master equality engine, if possible */ - void processInferences( Theory::Effort e ); + bool processInferences( Theory::Effort e ); /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map& cache ); /** get score */ @@ -422,7 +422,7 @@ public: EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ); virtual ~EqualityQueryQuantifiersEngine(); /** reset */ - void reset( Theory::Effort e ); + bool reset( Theory::Effort e ); /** general queries about equality */ bool hasTerm( Node a ); Node getRepresentative( Node a ); -- 2.30.2