diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-01 16:42:56 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-01 16:42:56 -0500 |
commit | cd5cc65fed2c850100a6f00067d102b48d262742 (patch) | |
tree | 6999501b3e6a34cfcac344165e92e83f5727389a /src/theory/quantifiers/equality_infer.cpp | |
parent | ccc9cd5aad5248b4a2c86b617d76bc98063a7ea2 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers/equality_infer.cpp')
-rw-r--r-- | src/theory/quantifiers/equality_infer.cpp | 316 |
1 files changed, 249 insertions, 67 deletions
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; i<d_eqci[n]->d_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<TNode>(d_c->getCMM()) ); + d_rep_exp.insertDataFromContextMemory( eqc, re ); + } + for( unsigned i=0; i<exp_to_add.size(); i++ ){ + re->push_back( exp_to_add[i] ); + } + //for( unsigned i=0; i<exp_to_add.size(); i++ ){ + // eqci->d_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<Rational>(); + 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<exp.size(); i++ ){ + Trace("eq-infer-debug") << exp[i] << " "; + } + Trace("eq-infer-debug") << std::endl; + } + addToExplanationEqc( v_solve, exp ); + } + std::vector< Node > 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; j<ul->size(); j++ ){ Node r = (*ul)[j]; + //Trace("eq-infer-debug") << " use list size = " << eqci_solved->d_uselist.size() << std::endl; + //for( unsigned j=0; j<eqci_solved->d_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<new_use.size(); i++ ){ addToUseList( new_use[i], r ); @@ -238,8 +417,11 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { } Node EqualityInference::getPendingMergeExplanation( unsigned i ) { - Assert( d_trackExplain ); - return d_pending_merge_exp[i]; + if( d_trackExplain ){ + return d_pending_merge_exp[i]; + }else{ + return d_pending_merges[i]; + } } } |