From: Andrew Reynolds Date: Wed, 26 Jan 2022 19:07:56 +0000 (-0600) Subject: Initial refactoring of conflict-based instantiation (#7380) X-Git-Tag: cvc5-1.0.0~501 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e42644dd87d217b98ec88207c2c7f30ef54261a;p=cvc5.git Initial refactoring of conflict-based instantiation (#7380) This done an initial pass at refactoring conflict-based instantiation (the code has been largely unchanged since it was written in early 2014). This code is a bottleneck on some Facebook benchmarks and needs revisiting. This changes the style so the parent modules are made data members instead of passed to methods. Otherwise, it changes int -> size_t wherever applicable, although int is often used to denote possibly valid indices where -1 means invalid. It updates to use range-based for loops and mostly organizes the order of data members in classes to meet style guidelines. Followup PRs will make more significant refactoring, e.g. to split the classes into multiple utilities. --- diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index d39212ddc..dbe141c66 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -37,54 +37,38 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QuantInfo::QuantInfo() - : d_unassigned_nvar(0), d_una_index(0), d_parent(nullptr), d_mg(nullptr) +QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q) + : EnvObj(env), + d_parent(p), + d_mg(nullptr), + d_q(q), + d_unassigned_nvar(0), + d_una_index(0) { -} - -QuantInfo::~QuantInfo() { - delete d_mg; - for(std::map< int, MatchGen * >::iterator i = d_var_mg.begin(), - iend=d_var_mg.end(); i != iend; ++i) { - MatchGen* currentMatchGenerator = (*i).second; - delete currentMatchGenerator; - } - d_var_mg.clear(); -} - -void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { - d_parent = p; - d_q = q; + Node qn = d_q[1]; d_extra_var.clear(); - for( unsigned i=0; iisValid() ){ - /* - for( unsigned j=0; jsetInvalid(); - break; - } - } - */ - for( unsigned j=q[0].getNumChildren(); jisValid() ){ Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl; d_mg->setInvalid(); break; }else{ - std::vector< int > bvars; - d_var_mg[j]->determineVariableOrder( this, bvars ); + std::vector bvars; + d_var_mg[j]->determineVariableOrder(bvars); } } } if( d_mg->isValid() ){ - std::vector< int > bvars; - d_mg->determineVariableOrder( this, bvars ); + std::vector bvars; + d_mg->determineVariableOrder(bvars); } }else{ Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl; @@ -125,29 +109,46 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { }else{ //get all variables that are always relevant std::map< TNode, bool > visited; - getPropagateVars( p, vars, q[1], false, visited ); + getPropagateVars(vars, q[1], false, visited); } - for( unsigned j=0; jgetTermDatabase()->getMatchOperator( v ); if( !f.isNull() ){ Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl; - for( unsigned k=0; k::iterator itv = d_var_num.find( n ); + std::map::iterator itv = d_var_num.find(n); if( itv!=d_var_num.end() ){ + std::vector& vrd = d_var_rel_dom[itv->second][f]; Trace("qcf-opt") << " arg " << k << " is var #" << itv->second << std::endl; - if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){ - d_var_rel_dom[itv->second][f].push_back( k ); + if (std::find(vrd.begin(), vrd.end(), k) == vrd.end()) + { + vrd.push_back(k); } } } } - } + } } } -void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){ +QuantInfo::~QuantInfo() {} + +Node QuantInfo::getQuantifiedFormula() const { return d_q; } + +QuantifiersInferenceManager& QuantInfo::getInferenceManager() +{ + Assert(d_parent != nullptr); + return d_parent->getInferenceManager(); +} + +void QuantInfo::getPropagateVars(std::vector& vars, + TNode n, + bool pol, + std::map& visited) +{ std::map< TNode, bool >::iterator itv = visited.find( n ); if( itv==visited.end() ){ visited[n] = true; @@ -156,10 +157,12 @@ void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& v if( d_var_num.find( n )!=d_var_num.end() ){ Assert(std::find(vars.begin(), vars.end(), n) == vars.end()); vars.push_back( n ); - TNode f = p->getTermDatabase()->getMatchOperator( n ); + TNode f = d_parent->getTermDatabase()->getMatchOperator(n); if( !f.isNull() ){ - if( std::find( p->d_func_rel_dom[f].begin(), p->d_func_rel_dom[f].end(), d_q )==p->d_func_rel_dom[f].end() ){ - p->d_func_rel_dom[f].push_back( d_q ); + std::vector& rd = d_parent->d_func_rel_dom[f]; + if (std::find(rd.begin(), rd.end(), d_q) == rd.end()) + { + rd.push_back(d_q); } } }else if( MatchGen::isHandledBoolConnective( n ) ){ @@ -168,8 +171,9 @@ void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& v } Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl; if( rec ){ - for( unsigned i=0; i::const_iterator it = d_var_num.find(v); + return it != d_var_num.end() ? static_cast(it->second) : -1; +} -bool QuantInfo::reset_round( QuantConflictFind * p ) { - for( unsigned i=0; ireset_round( p ); - for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){ - if (!it->second->reset_round(p)) + + d_mg->reset_round(); + for (const std::pair& vg : d_var_mg) + { + if (!vg.second->reset_round()) { return false; } } //now, reset for matching - d_mg->reset( p, false, this ); + d_mg->reset(false); return true; } -int QuantInfo::getCurrentRepVar( int v ) { - if( v!=-1 && !d_match[v].isNull() ){ - int vn = getVarNum( d_match[v] ); - if( vn!=-1 ){ - //int vr = getCurrentRepVar( vn ); - //d_match[v] = d_vars[vr]; - //return vr; - return getCurrentRepVar( vn ); +size_t QuantInfo::getCurrentRepVar(size_t v) +{ + Assert(v < d_match.size()); + TNode m = d_match[v]; + if (!m.isNull()) + { + std::map::const_iterator it = d_var_num.find(m); + if (it != d_var_num.end()) + { + return getCurrentRepVar(it->second); } } return v; } TNode QuantInfo::getCurrentValue( TNode n ) { - int v = getVarNum( n ); - if( v==-1 ){ + std::map::const_iterator it = d_var_num.find(n); + if (it == d_var_num.end()) + { + return n; + } + Node m = d_match[it->second]; + if (m.isNull()) + { return n; - }else{ - if( d_match[v].isNull() ){ - return n; - }else{ - Assert(getVarNum(d_match[v]) != v); - return getCurrentValue( d_match[v] ); - } } + return getCurrentValue(m); } TNode QuantInfo::getCurrentExpValue( TNode n ) { - int v = getVarNum( n ); - if( v==-1 ){ + std::map::const_iterator it = d_var_num.find(n); + if (it == d_var_num.end()) + { return n; - }else{ - if( d_match[v].isNull() ){ - return n; - }else{ - Assert(getVarNum(d_match[v]) != v); - if( d_match_term[v].isNull() ){ - return getCurrentValue( d_match[v] ); - }else{ - return d_match_term[v]; - } - } } + Node m = d_match[it->second]; + if (m.isNull()) + { + return n; + } + Assert(m != n); + Node mt = d_match_term[it->second]; + if (mt.isNull()) + { + return getCurrentValue(m); + } + return mt; } -bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) { +bool QuantInfo::getCurrentCanBeEqual(size_t v, TNode n, bool chDiseq) +{ //check disequalities - std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v ); - if( itd!=d_curr_var_deq.end() ){ - for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){ - Node cv = getCurrentValue( it->first ); - Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl; - if( cv==n ){ + std::map >::iterator itd = + d_curr_var_deq.find(v); + if (itd == d_curr_var_deq.end()) + { + return true; + } + for (std::pair& dd : itd->second) + { + Node cv = getCurrentValue(dd.first); + Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl; + if (cv == n) + { + return false; + } + else if (chDiseq && !isVar(n) && !isVar(cv)) + { + // they must actually be disequal if we are looking for conflicts + if (!d_parent->areDisequal(n, cv)) + { + // TODO : check for entailed disequal return false; - }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){ - //they must actually be disequal if we are looking for conflicts - if( !p->areDisequal( n, cv ) ){ - //TODO : check for entailed disequal - - return false; - } } } } + return true; } -int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) { +int QuantInfo::addConstraint(size_t v, TNode n, bool polarity) +{ v = getCurrentRepVar( v ); int vn = getVarNum( n ); - vn = vn==-1 ? -1 : getCurrentRepVar( vn ); + if (vn != -1) + { + vn = static_cast(getCurrentRepVar(static_cast(vn))); + } n = getCurrentValue( n ); - return addConstraint( p, v, n, vn, polarity, false ); + return addConstraint(v, n, vn, polarity, false); } -int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) { +int QuantInfo::addConstraint( + size_t v, TNode n, int vn, bool polarity, bool doRemove) +{ + Assert(v < d_match.size()); //for handling equalities between variables, and disequalities involving variables Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")"; Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl; Assert(doRemove || n == getCurrentValue(n)); Assert(doRemove || v == getCurrentRepVar(v)); - Assert(doRemove || vn == getCurrentRepVar(getVarNum(n))); + Assert(doRemove || (vn == -1 && getVarNum(n) == -1) + || (vn >= 0 + && static_cast(vn) + == getCurrentRepVar(static_cast(getVarNum(n))))); if( polarity ){ - if( vn!=v ){ + if (vn != static_cast(v)) + { if( doRemove ){ if( vn!=-1 ){ //if set to this in the opposite direction, clean up opposite instead // std::map< int, TNode >::iterator itmn = d_match.find( vn ); if( d_match[vn]==d_vars[v] ){ - return addConstraint( p, vn, d_vars[v], v, true, true ); + return addConstraint(vn, d_vars[v], v, true, true); }else{ //unsetting variables equal - std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn ); + std::map >::iterator itd = + d_curr_var_deq.find(vn); if( itd!=d_curr_var_deq.end() ){ //remove disequalities owned by this std::vector< TNode > remDeq; - for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){ - if( it->second==v ){ - remDeq.push_back( it->first ); + for (const std::pair& dd : itd->second) + { + if (dd.second == v) + { + remDeq.push_back(dd.first); } } - for( unsigned i=0; isecond.erase(rd); } } } } - unsetMatch( p, v ); + unsetMatch(v); return 1; }else{ - //std::map< int, TNode >::iterator itm = d_match.find( v ); bool isGroundRep = false; bool isGround = false; if( vn!=-1 ){ Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl; - //std::map< int, TNode >::iterator itmn = d_match.find( vn ); if( d_match[v].isNull() ){ //setting variables equal bool alreadySet = false; @@ -408,20 +443,25 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo } //copy or check disequalities - std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v ); + std::map >::iterator itd = + d_curr_var_deq.find(v); if( itd!=d_curr_var_deq.end() ){ - for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){ - Node dv = getCurrentValue( it->first ); + std::map& cvd = d_curr_var_deq[vn]; + for (const std::pair& dd : itd->second) + { + Node dv = getCurrentValue(dd.first); if( !alreadySet ){ - if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){ - d_curr_var_deq[vn][dv] = v; - } - }else{ - if( !p->areMatchDisequal( d_match[vn], dv ) ){ - Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; - return -1; + if (cvd.find(dv) == cvd.end()) + { + cvd[dv] = v; } } + else if (d_match[vn] == dv) + { + Debug("qcf-match-debug") + << " -> fail, conflicting disequality" << std::endl; + return -1; + } } } if( alreadySet ){ @@ -431,11 +471,11 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo if( d_match[vn].isNull() ){ Debug("qcf-match-debug") << " ...Reverse direction" << std::endl; //set the opposite direction - return addConstraint( p, vn, d_vars[v], v, true, false ); + return addConstraint(vn, d_vars[v], v, true, false); }else{ Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl; //are they currently equal - return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1; + return d_match[v] == d_match[vn] ? 0 : -1; } } }else{ @@ -446,26 +486,34 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo }else{ //compare ground values Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl; - return p->areMatchEqual( d_match[v], n ) ? 0 : -1; + return d_match[v] == n ? 0 : -1; } } - if( setMatch( p, v, n, isGroundRep, isGround ) ){ + if (setMatch(v, n, isGroundRep, isGround)) + { Debug("qcf-match-debug") << " -> success" << std::endl; return 1; - }else{ + } + else + { Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; return -1; } } - }else{ + } + else + { Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl; return 0; } }else{ - if( vn==v ){ + if (vn == static_cast(v)) + { Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl; return -1; - }else{ + } + else + { if( doRemove ){ Assert(d_curr_var_deq[v].find(n) != d_curr_var_deq[v].end()); d_curr_var_deq[v].erase( n ); @@ -473,10 +521,10 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo }else{ if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){ //check if it respects equality - //std::map< int, TNode >::iterator itm = d_match.find( v ); if( !d_match[v].isNull() ){ TNode nv = getCurrentValue( n ); - if( !p->areMatchDisequal( nv, d_match[v] ) ){ + if (nv == d_match[v]) + { Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; return -1; } @@ -493,60 +541,84 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo } } -bool QuantInfo::isConstrainedVar( int v ) { - if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){ +bool QuantInfo::isConstrainedVar(size_t v) +{ + std::map >::const_iterator it = + d_curr_var_deq.find(v); + if (it != d_curr_var_deq.end() && !it->second.empty()) + { return true; - }else{ - Node vv = getVar( v ); - //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){ - for( unsigned i=0; i >& d : + d_curr_var_deq) + { + for (const std::pair& dd : d.second) + { + if (dd.first == vv) + { return true; } } - for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){ - for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - if( it2->first==vv ){ - return true; - } - } - } - return false; } + return false; } -bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround ) { - if( getCurrentCanBeEqual( p, v, n ) ){ - if( isGroundRep ){ - //fail if n does not exist in the relevant domain of each of the argument positions - std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v ); - if( it!=d_var_rel_dom.end() ){ - for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - for( unsigned j=0; jsecond.size(); j++ ){ - Debug("qcf-match-debug2") << n << " in relevant domain " << it2->first << "." << it2->second[j] << "?" << std::endl; - if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){ - Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl; - return false; - } +bool QuantInfo::setMatch(size_t v, TNode n, bool isGroundRep, bool isGround) +{ + if (!getCurrentCanBeEqual(v, n)) + { + return false; + } + if (isGroundRep) + { + // fail if n does not exist in the relevant domain of each of the argument + // positions + std::map > >::iterator it = + d_var_rel_dom.find(v); + if (it != d_var_rel_dom.end()) + { + TermDb* tdb = d_parent->getTermDatabase(); + for (std::pair >& rd : it->second) + { + for (size_t index : rd.second) + { + Debug("qcf-match-debug2") << n << " in relevant domain " << rd.first + << "." << index << "?" << std::endl; + if (!tdb->inRelevantDomain(rd.first, index, n)) + { + Debug("qcf-match-debug") + << " -> fail, since " << n << " is not in relevant domain of " + << rd.first << "." << index << std::endl; + return false; } } } } - Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl; - if( isGround ){ - if( d_vars[v].getKind()==BOUND_VARIABLE ){ - d_vars_set[v] = true; - Debug("qcf-match-debug") << "---- now bound " << d_vars_set.size() << " / " << d_q[0].getNumChildren() << " base variables." << std::endl; - } + } + Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " + << d_curr_var_deq[v].size() << " disequalities" + << std::endl; + if (isGround) + { + if (d_vars[v].getKind() == BOUND_VARIABLE) + { + d_vars_set.insert(v); + Debug("qcf-match-debug") + << "---- now bound " << d_vars_set.size() << " / " + << d_q[0].getNumChildren() << " base variables." << std::endl; } - d_match[v] = n; - return true; - }else{ - return false; } + d_match[v] = n; + return true; } -void QuantInfo::unsetMatch( QuantConflictFind * p, int v ) { +void QuantInfo::unsetMatch(size_t v) +{ Debug("qcf-match-debug") << "-- unbind : " << v << std::endl; if( d_vars[v].getKind()==BOUND_VARIABLE && d_vars_set.find( v )!=d_vars_set.end() ){ d_vars_set.erase( v ); @@ -554,11 +626,13 @@ void QuantInfo::unsetMatch( QuantConflictFind * p, int v ) { d_match[ v ] = TNode::null(); } -bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { - for( int i=0; i::iterator it = d_match.find( i ); +bool QuantInfo::isMatchSpurious() +{ + for (size_t i = 0, nvars = getNumVars(); i < nvars; i++) + { if( !d_match[i].isNull() ){ - if (!getCurrentCanBeEqual(p, i, d_match[i], p->atConflictEffort())) { + if (!getCurrentCanBeEqual(i, d_match[i], d_parent->atConflictEffort())) + { return true; } } @@ -566,12 +640,11 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false; } -bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, - std::vector& terms) +bool QuantInfo::isTConstraintSpurious(const std::vector& terms) { if( options::qcfEagerTest() ){ + EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck(); //check whether the instantiation evaluates as expected - EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); std::map subs; for (size_t i = 0, tsize = terms.size(); i < tsize; i++) { @@ -585,7 +658,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, << " " << d_extra_var[i] << " -> " << n << std::endl; subs[d_extra_var[i]] = n; } - if (p->atConflictEffort()) { + if (d_parent->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; if (!echeck->isEntailed(d_q[1], subs, false, false)) { @@ -600,9 +673,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, d_q[1], subs, false, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; - for( unsigned i=0; iisPropagatingInstance(inst_eval)) + if (!d_parent->isPropagatingInstance(inst_eval)) { // Notice that this can happen in cases where: // (1) x = -1*y is rewritten to y = -1*x, and @@ -638,23 +709,25 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, } if( !d_tconstraints.empty() ){ //check constraints + QuantifiersRegistry& qr = d_parent->getQuantifiersRegistry(); for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ //apply substitution to the tconstraint - Node cons = p->getQuantifiersRegistry().substituteBoundVariables( - it->first, d_q, terms); + Node cons = qr.substituteBoundVariables(it->first, d_q, terms); cons = it->second ? cons : cons.negate(); - if (!entailmentTest(p, cons, p->atConflictEffort())) { + if (!entailmentTest(cons, d_parent->atConflictEffort())) + { return true; } } } // spurious if quantifiers engine is in conflict - return p->d_qstate.isInConflict(); + return d_parent->d_qstate.isInConflict(); } -bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { +bool QuantInfo::entailmentTest(Node lit, bool chEnt) +{ Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl; - Node rew = Rewriter::rewrite(lit); + Node rew = rewrite(lit); if (rew.isConst()) { Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to " @@ -665,14 +738,15 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { // constraint is (not) entailed if (!chEnt) { - rew = Rewriter::rewrite(rew.negate()); + rew = rewrite(rew.negate()); } // check if it is entailed Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; - std::pair et = p->getState().getValuation().entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew); - ++(p->d_statistics.d_entailment_checks); + std::pair et = + d_parent->getState().getValuation().entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew); + ++(d_parent->d_statistics.d_entailment_checks); Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl; if (!et.first) @@ -684,7 +758,8 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { return chEnt; } -bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) { +bool QuantInfo::completeMatch(std::vector& assigned, bool doContinue) +{ //assign values for variables that were unassigned (usually not necessary, but handles corner cases) bool doFail = false; bool success = true; @@ -708,24 +783,27 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){ Kind k = d_vars[index].getKind(); std::vector< TNode > children; - for( unsigned j=0; jatConflictEffort()) { + if (!d_parent->atConflictEffort()) + { break; } }else{ - Node z = p->getZero(d_vars[index].getType(), k); + Node z = d_parent->getZero(d_vars[index].getType(), k); if( !z.isNull() ){ + size_t vni = static_cast(vn); Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl; - assigned.push_back( vn ); - if( !setMatch( p, vn, z, false, true ) ){ + assigned.push_back(vni); + if (!setMatch(vni, z, false, true)) + { success = false; break; } @@ -736,15 +814,15 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign children.push_back( vv ); } }else{ - Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl; - children.push_back( d_vars[index][j] ); + Trace("qcf-tconstraint-debug") << "...sum " << vi << std::endl; + children.push_back( vi ); } } if( success ){ if( slv_v!=-1 ){ Node lhs; if( children.empty() ){ - lhs = p->getZero(d_vars[index].getType(), k); + lhs = d_parent->getZero(d_vars[index].getType(), k); }else if( children.size()==1 ){ lhs = children[0]; }else{ @@ -754,7 +832,8 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( v==d_vars[index] ){ sum = lhs; }else{ - if (p->atConflictEffort()) { + if (d_parent->atConflictEffort()) + { Kind kn = k; if( d_vars[index].getKind()==PLUS ){ kn = MINUS; @@ -767,19 +846,21 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( !sum.isNull() ){ assigned.push_back( slv_v ); Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl; - if( !setMatch( p, slv_v, sum, false, true ) ){ + if (!setMatch(slv_v, sum, false, true)) + { success = false; } - p->d_tempCache.push_back( sum ); + d_parent->d_tempCache.push_back(sum); } }else{ //must show that constraint is met Node sum = NodeManager::currentNM()->mkNode( k, children ); Node eq = sum.eqNode( v ); - if( !entailmentTest( p, eq ) ){ + if (!entailmentTest(eq)) + { success = false; } - p->d_tempCache.push_back( sum ); + d_parent->d_tempCache.push_back(sum); } } } @@ -792,9 +873,10 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign //check what is left to assign d_unassigned.clear(); d_unassigned_tn.clear(); - std::vector< int > unassigned[2]; + std::vector unassigned[2]; std::vector< TypeNode > unassigned_tn[2]; - for( int i=0; i& assign Trace("qcf-check-unassign") << "Failure, try again..." << std::endl; } bool invalidMatch = false; - while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){ + while ((success && d_una_index < d_unassigned.size()) || invalidMatch + || doFail) + { invalidMatch = false; - if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){ + if (!doFail && d_una_index == d_una_eqc_count.size()) + { //check if it has now been assigned if( d_una_indexreset( p, true, this ); + d_var_mg[d_unassigned[d_una_index]]->reset(true); d_una_eqc_count.push_back( 0 ); } }else{ d_una_eqc_count.push_back( 0 ); } - }else{ + } + else + { bool failed = false; if( !doFail ){ if( d_una_indexgetNextMatch( p, this ) ){ + } + else if (d_var_mg[d_unassigned[d_una_index]]->getNextMatch()) + { Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl; d_una_index++; - }else{ + } + else + { failed = true; Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl; } }else{ - Assert(doFail || d_una_index == (int)d_una_eqc_count.size() - 1); - if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){ + Assert(doFail || d_una_index + 1 == d_una_eqc_count.size()); + const std::vector& eqcs = + d_parent->d_eqcs[d_unassigned_tn[d_una_index]]; + if (d_una_eqc_count[d_una_index] < static_cast(eqcs.size())) + { int currIndex = d_una_eqc_count[d_una_index]; d_una_eqc_count[d_una_index]++; - Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl; - if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true, true ) ){ + Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" + << eqcs[currIndex] << std::endl; + if (setMatch( + d_unassigned[d_una_index], eqcs[currIndex], true, true)) + { d_match_term[d_unassigned[d_una_index]] = TNode::null(); Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl; d_una_index++; - }else{ + } + else + { Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl; invalidMatch = true; } - }else{ + } + else + { failed = true; Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl; } @@ -874,46 +975,59 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign }else{ doFail = false; } + if (d_una_index == 0) + { + success = false; + break; + } d_una_index--; - }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 ); + } while (d_una_eqc_count[d_una_index] == -1); } } } - success = d_una_index>=0; if( success ){ doFail = true; Trace("qcf-check-unassign") << " Try: " << std::endl; - for( unsigned i=0; i " << d_match[ui] << std::endl; + if (Trace.isOn("qcf-check")) + { + for (int ui : d_unassigned) + { + if (!d_match[ui].isNull()) + { + Trace("qcf-check-unassign") + << " Assigned #" << ui << " : " << d_vars[ui] << " -> " + << d_match[ui] << std::endl; + } } } } - }while( success && isMatchSpurious( p ) ); + } while (success && isMatchSpurious()); Trace("qcf-check") << "done assigning." << std::endl; } if( success ){ - for( unsigned i=0; i " << d_match[ui] << std::endl; + if (Trace.isOn("qcf-check")) + { + for (int ui : d_unassigned) + { + if (!d_match[ui].isNull()) + { + Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui] + << " -> " << d_match[ui] << std::endl; + } } } return true; - }else{ - revertMatch( p, assigned ); - assigned.clear(); - return false; } + revertMatch(assigned); + assigned.clear(); + return false; } void QuantInfo::getMatch( std::vector< Node >& terms ){ - for( unsigned i=0; igetCurrentValue( qi->d_match[i] ); - int repVar = getCurrentRepVar( i ); + for (size_t i = 0, nvars = d_q[0].getNumChildren(); i < nvars; i++) + { + size_t repVar = getCurrentRepVar(i); Node cv; - //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar ); if( !d_match_term[repVar].isNull() ){ cv = d_match_term[repVar]; }else{ @@ -924,24 +1038,32 @@ void QuantInfo::getMatch( std::vector< Node >& terms ){ } } -void QuantInfo::revertMatch( QuantConflictFind * p, std::vector< int >& assigned ) { - for( unsigned i=0; i& assigned) +{ + for (size_t a : assigned) + { + unsetMatch(a); } } -void QuantInfo::debugPrintMatch( const char * c ) { - for( int i=0; i "; if( !d_match[i].isNull() ){ Trace(c) << d_match[i]; }else{ Trace(c) << "(unassigned) "; } - if( !d_curr_var_deq[i].empty() ){ + std::map >::const_iterator itc = + d_curr_var_deq.find(i); + if (!itc->second.empty()) + { Trace(c) << ", DEQ{ "; - for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){ - Trace(c) << it->first << " "; + for (const std::pair& d : itc->second) + { + Trace(c) << d.first << " "; } Trace(c) << "}"; } @@ -952,37 +1074,24 @@ void QuantInfo::debugPrintMatch( const char * c ) { } if( !d_tconstraints.empty() ){ Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl; - for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ - Trace(c) << " " << it->first << " -> " << it->second << std::endl; + for (const std::pair& tc : d_tconstraints) + { + Trace(c) << " " << tc.first << " -> " << tc.second << std::endl; } } } -MatchGen::MatchGen() - : d_matched_basis(), - d_binding(), - d_tgt(), - d_tgt_orig(), - d_wasSet(), - d_n(), - d_type( typ_invalid ), - d_type_not() -{ - d_qni_size = 0; - d_child_counter = -1; - d_use_children = true; -} - - -MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) - : d_matched_basis(), - d_binding(), - d_tgt(), - d_tgt_orig(), - d_wasSet(), - d_n(), - d_type(), - d_type_not() +MatchGen::MatchGen(QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar) + : d_tgt(), + d_tgt_orig(), + d_wasSet(), + d_n(), + d_type(), + d_type_not(), + d_parent(p), + d_qi(qi), + d_matched_basis(), + d_binding() { //initialize temporary d_child_counter = -1; @@ -1000,7 +1109,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type = typ_invalid; }else{ d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym; - d_qni_var_num[0] = qi->getVarNum( n ); + int vn = qi->getVarNum(n); + Assert(vn >= 0); + d_qni_var_num[0] = static_cast(vn); d_qni_size++; d_type_not = false; d_n = n; @@ -1009,7 +1120,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) Node nn = d_n[j]; Trace("qcf-qregister-debug") << " " << d_qni_size; if( qi->isVar( nn ) ){ - int v = qi->d_var_num[nn]; + size_t v = qi->d_var_num[nn]; Trace("qcf-qregister-debug") << " is var #" << v << std::endl; d_qni_var_num[d_qni_size] = v; //qi->addFuncParent( v, f, j ); @@ -1035,11 +1146,14 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type = typ_formula; for( unsigned i=0; i mg = + std::make_unique(p, qi, d_n[i], false); + if (!mg->isValid()) + { setInvalid(); break; } + d_children.push_back(std::move(mg)); } } }else{ @@ -1085,27 +1199,32 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = "; debugPrintType( "qcf-qregister-debug", d_type, true ); Trace("qcf-qregister-debug") << std::endl; - //Assert( d_children.size()==d_children_order.size() ); } -void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested ) { +void MatchGen::collectBoundVar(Node n, + std::vector& cbvars, + std::map& visited, + bool& hasNested) +{ if( visited.find( n )==visited.end() ){ visited[n] = true; if( n.getKind()==FORALL ){ hasNested = true; } - int v = qi->getVarNum( n ); + int v = d_qi->getVarNum(n); if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){ cbvars.push_back( v ); } - for( unsigned i=0; i& bvars ) { +void MatchGen::determineVariableOrder(std::vector& bvars) +{ Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl; bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL ); if( isComm ){ @@ -1116,10 +1235,12 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars std::map< int, bool > has_nested; std::vector< bool > assigned; Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl; - for( unsigned i=0; i visited; has_nested[i] = false; - collectBoundVar( qi, d_children[i].d_n, c_to_vars[i], visited, has_nested[i] ); + collectBoundVar( + d_children[i]->getNode(), c_to_vars[i], visited, has_nested[i]); assigned.push_back( false ); vb_count[i] = 0; vu_count[i] = 0; @@ -1135,11 +1256,13 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars } //children that bind no unbound variable, then the most number of bound, unbound variables go first Trace("qcf-qregister-vo") << "Variable order for " << d_n << " : " << std::endl; + size_t nqvars = d_qi->d_vars.size(); do { int min_score0 = -1; int min_score = -1; int min_score_index = -1; - for( unsigned i=0; i& bvars if( !options::qcfVoExp() ){ score = vu_count[i]; }else{ - score = vu_count[i]==0 ? 0 : ( 1 + qi->d_vars.size()*( qi->d_vars.size() - vb_count[i] ) + ( qi->d_vars.size() - vu_count[i] ) ); + score = vu_count[i] == 0 ? 0 + : (1 + nqvars * (nqvars - vb_count[i]) + + (nqvars - vu_count[i])); } if( min_score==-1 || score0& bvars } } } - Trace("qcf-qregister-vo") << " " << d_children_order.size()+1 << ": " << d_children[min_score_index].d_n << " : "; + Trace("qcf-qregister-vo") + << " " << d_children_order.size() + 1 << ": " + << d_children[min_score_index]->getNode() << " : "; Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl; Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl; Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl; @@ -1165,7 +1292,7 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars d_children_order.push_back( min_score_index ); assigned[min_score_index] = true; //determine order internal to children - d_children[min_score_index].determineVariableOrder( qi, bvars ); + d_children[min_score_index]->determineVariableOrder(bvars); Trace("qcf-qregister-debug") << "...bind variables" << std::endl; //now, make it a bound variable if( vu_count[min_score_index]>0 ){ @@ -1185,14 +1312,15 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars }while( d_children_order.size()!=d_children.size() ); Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl; }else{ - for( unsigned i=0; idetermineVariableOrder(bvars); //now add to bvars std::map< Node, bool > visited; std::vector< int > cvars; bool has_nested = false; - collectBoundVar( qi, d_children[i].d_n, cvars, visited, has_nested ); + collectBoundVar(d_children[i]->getNode(), cvars, visited, has_nested); for( unsigned j=0; j& bvars } } -bool MatchGen::reset_round(QuantConflictFind* p) +bool MatchGen::reset_round() { d_wasSet = false; - for( unsigned i=0; i& mg : d_children) + { + if (!mg->reset_round()) { return false; } } if( d_type==typ_ground ){ - // int e = p->evaluate( d_n ); - // if( e==1 ){ - // d_ground_eval[0] = p->d_true; - //}else if( e==-1 ){ - // d_ground_eval[0] = p->d_false; - //} - // modified - EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); - QuantifiersState& qs = p->getState(); + EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck(); + QuantifiersState& qs = d_parent->getState(); for (unsigned i = 0; i < 2; i++) { if (echeck->isEntailed(d_n, i == 0)) { - d_ground_eval[0] = i==0 ? p->d_true : p->d_false; + d_ground_eval[0] = NodeManager::currentNM()->mkConst(i == 0); } if (qs.isInConflict()) { @@ -1233,8 +1355,8 @@ bool MatchGen::reset_round(QuantConflictFind* p) } } }else if( d_type==typ_eq ){ - EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); - QuantifiersState& qs = p->getState(); + EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck(); + QuantifiersState& qs = d_parent->getState(); for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) @@ -1261,7 +1383,8 @@ bool MatchGen::reset_round(QuantConflictFind* p) return true; } -void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { +void MatchGen::reset(bool tgt) +{ d_tgt = d_type_not ? !tgt : tgt; Debug("qcf-match") << " Reset for : " << d_n << ", type : "; debugPrintType( "qcf-match", d_type ); @@ -1278,77 +1401,103 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_use_children = false; }else if( d_type==typ_ground ){ d_use_children = false; - if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){ + if (d_ground_eval[0].isConst() + && d_ground_eval[0].getConst() == d_tgt) + { d_child_counter = 0; } - }else if( qi->isBaseMatchComplete() && options::qcfEagerTest() ){ + } + else if (d_qi->isBaseMatchComplete() && options::qcfEagerTest()) + { d_use_children = false; d_child_counter = 0; - }else if( d_type==typ_bool_var ){ + } + else if (d_type == typ_bool_var) + { //get current value of the variable - TNode n = qi->getCurrentValue( d_n ); - int vn = qi->getCurrentRepVar( qi->getVarNum( n ) ); - if( vn==-1 ){ - EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + TNode n = d_qi->getCurrentValue(d_n); + int vnn = d_qi->getVarNum(n); + if (vnn == -1) + { + // evaluate the value, see if it is compatible + EntailmentCheck* echeck = + d_parent->getTermRegistry().getEntailmentCheck(); if (echeck->isEntailed(n, d_tgt)) { d_child_counter = 0; } - }else{ + } + else + { + size_t vn = d_qi->getCurrentRepVar(static_cast(vnn)); //unassigned, set match to true/false d_qni_bound[0] = vn; - qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false, true ); + d_qi->setMatch(vn, NodeManager::currentNM()->mkConst(d_tgt), false, true); d_child_counter = 0; } if( d_child_counter==0 ){ d_qn.push_back( NULL ); } - }else if( d_type==typ_var ){ + } + else if (d_type == typ_var) + { Assert(isHandledUfTerm(d_n)); - TNode f = getMatchOperator( p, d_n ); + TNode f = d_parent->getTermDatabase()->getMatchOperator(d_n); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; - TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f); + TNodeTrie* qni = + d_parent->getTermDatabase()->getTermArgTrie(Node::null(), f); if (qni == nullptr || qni->empty()) { //inform irrelevant quantifiers - p->setIrrelevantFunction( f ); + d_parent->setIrrelevantFunction(f); } else { d_qn.push_back(qni); } d_matched_basis = false; - }else if( d_type==typ_tsym || d_type==typ_tconstraint ){ - for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){ - int repVar = qi->getCurrentRepVar( it->second ); - if( qi->d_match[repVar].isNull() ){ - Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl; - d_qni_bound[it->first] = repVar; + } + else if (d_type == typ_tsym || d_type == typ_tconstraint) + { + for (std::pair& qvn : d_qni_var_num) + { + size_t repVar = d_qi->getCurrentRepVar(qvn.second); + if (d_qi->d_match[repVar].isNull()) + { + Debug("qcf-match-debug") << "Force matching on child #" << qvn.first + << ", which is var #" << repVar << std::endl; + d_qni_bound[qvn.first] = repVar; } } d_qn.push_back( NULL ); - }else if( d_type==typ_pred || d_type==typ_eq ){ + } + else if (d_type == typ_pred || d_type == typ_eq) + { //add initial constraint Node nn[2]; int vn[2]; if( d_type==typ_pred ){ - nn[0] = qi->getCurrentValue( d_n ); - vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) ); - nn[1] = d_tgt ? p->d_true : p->d_false; + nn[0] = d_qi->getCurrentValue(d_n); + int vnn = d_qi->getVarNum(nn[0]); + vn[0] = + vnn == -1 ? vnn : d_qi->getCurrentRepVar(static_cast(vnn)); + nn[1] = NodeManager::currentNM()->mkConst(d_tgt); vn[1] = -1; d_tgt = true; }else{ for( unsigned i=0; i<2; i++ ){ TNode nc; - std::map::iterator it = d_qni_gterm.find(i); + std::map::iterator it = d_qni_gterm.find(i); if (it != d_qni_gterm.end()) { nc = it->second; }else{ nc = d_n[i]; } - nn[i] = qi->getCurrentValue( nc ); - vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) ); + nn[i] = d_qi->getCurrentValue(nc); + int vnn = d_qi->getVarNum(nn[i]); + vn[i] = + vnn == -1 ? vnn : d_qi->getCurrentRepVar(static_cast(vnn)); } } bool success; @@ -1357,12 +1506,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl; //just compare values if( d_tgt ){ - success = p->areMatchEqual( nn[0], nn[1] ); + success = nn[0] == nn[1]; }else{ - if (p->atConflictEffort()) { - success = p->areDisequal( nn[0], nn[1] ); - }else{ - success = p->areMatchDisequal( nn[0], nn[1] ); + if (d_parent->atConflictEffort()) + { + success = d_parent->areDisequal(nn[0], nn[1]); + } + else + { + success = (nn[0] != nn[1]); } } }else{ @@ -1377,12 +1529,13 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { } Debug("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl; //add some constraint - int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false ); + int addc = d_qi->addConstraint(vn[0], nn[1], vn[1], d_tgt, false); success = addc!=-1; //if successful and non-redundant, store that we need to cleanup this if( addc==1 ){ //Trace("qcf-explain") << " reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl; - for( unsigned i=0; i<2; i++ ){ + for (size_t i = 0; i < 2; i++) + { if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){ d_qni_bound[vn[i]] = vn[i]; } @@ -1395,20 +1548,26 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { if( success ){ d_qn.push_back( NULL ); } - }else{ + } + else + { if( d_children.empty() ){ //add dummy d_qn.push_back( NULL ); }else{ if( d_tgt && d_n.getKind()==FORALL ){ //fail - } else if (d_n.getKind() == FORALL && p->atConflictEffort() && - !options::qcfNestedConflict()) { + } + else if (d_n.getKind() == FORALL && d_parent->atConflictEffort() + && !options::qcfNestedConflict()) + { //fail - }else{ + } + else + { //reset the first child to d_tgt d_child_counter = 0; - getChild( d_child_counter )->reset( p, d_tgt, qi ); + getChild(d_child_counter)->reset(d_tgt); } } } @@ -1417,7 +1576,8 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl; } -bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { +bool MatchGen::getNextMatch() +{ Debug("qcf-match") << " Get next match for : " << d_n << ", type = "; debugPrintType( "qcf-match", d_type ); Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl; @@ -1436,24 +1596,30 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { bool doReset = false; bool doFail = false; if( !d_binding ){ - if( doMatching( p, qi ) ){ + if (doMatching()) + { Debug("qcf-match-debug") << " - Matching succeeded" << std::endl; d_binding = true; d_binding_it = d_qni_bound.begin(); doReset = true; //for tconstraint, add constraint if( d_type==typ_tconstraint ){ - std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n ); - if( it==qi->d_tconstraints.end() ){ - qi->d_tconstraints[d_n] = d_tgt; + std::map::iterator it = d_qi->d_tconstraints.find(d_n); + if (it == d_qi->d_tconstraints.end()) + { + d_qi->d_tconstraints[d_n] = d_tgt; //store that we added this constraint d_qni_bound_cons[0] = d_n; - }else if( d_tgt!=it->second ){ + } + else if (d_tgt != it->second) + { success = false; terminate = true; } } - }else{ + } + else + { Debug("qcf-match-debug") << " - Matching failed" << std::endl; success = false; terminate = true; @@ -1472,14 +1638,16 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { QuantInfo::VarMgMap::const_iterator itm; if( !doFail ){ Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl; - itm = qi->var_mg_find( d_binding_it->second ); + itm = d_qi->var_mg_find(d_binding_it->second); } - if( doFail || ( d_binding_it->first!=0 && itm != qi->var_mg_end() ) ){ + if (doFail || (d_binding_it->first != 0 && itm != d_qi->var_mg_end())) + { Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl; if( doReset ){ - itm->second->reset( p, true, qi ); + itm->second->reset(true); } - if( doFail || !itm->second->getNextMatch( p, qi ) ){ + if (doFail || !itm->second->getNextMatch()) + { do { if( d_binding_it==d_qni_bound.begin() ){ Debug("qcf-match-debug") << " failed." << std::endl; @@ -1488,17 +1656,21 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { --d_binding_it; Debug("qcf-match-debug") << " decrement..." << std::endl; } - }while( success && - ( d_binding_it->first==0 || - (!qi->containsVarMg(d_binding_it->second)))); + } while (success + && (d_binding_it->first == 0 + || (!d_qi->containsVarMg(d_binding_it->second)))); doReset = false; doFail = false; - }else{ + } + else + { Debug("qcf-match-debug") << " increment..." << std::endl; ++d_binding_it; doReset = true; } - }else{ + } + else + { Debug("qcf-match-debug") << " skip..." << d_binding_it->second << std::endl; ++d_binding_it; doReset = true; @@ -1518,13 +1690,17 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { if( !success ){ if( d_type==typ_eq || d_type==typ_pred ){ //clean up the constraints you added - for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){ - if( !it->second.isNull() ){ - Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl; - std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first ); + std::map::iterator itb; + for (const std::pair& qb : d_qni_bound_cons) + { + if (!qb.second.isNull()) + { + Debug("qcf-match") + << " Clean up bound var " << qb.first + << (d_tgt ? "!" : "") << " = " << qb.second << std::endl; + itb = d_qni_bound_cons_var.find(qb.first); int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1; - //Trace("qcf-explain") << " cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl; - qi->addConstraint( p, it->first, it->second, vn, d_tgt, true ); + d_qi->addConstraint(qb.first, qb.second, vn, d_tgt, true); } } d_qni_bound_cons.clear(); @@ -1532,18 +1708,20 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_qni_bound.clear(); }else{ //clean up the matches you set - for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){ - Debug("qcf-match") << " Clean up bound var " << it->second << std::endl; - Assert(it->second < qi->getNumVars()); - qi->unsetMatch( p, it->second ); - qi->d_match_term[ it->second ] = TNode::null(); + for (const std::pair& qb : d_qni_bound) + { + Debug("qcf-match") + << " Clean up bound var " << qb.second << std::endl; + Assert(qb.second < d_qi->getNumVars()); + d_qi->unsetMatch(qb.second); + d_qi->d_match_term[qb.second] = TNode::null(); } d_qni_bound.clear(); } if( d_type==typ_tconstraint ){ //remove constraint if applicable if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){ - qi->d_tconstraints.erase( d_n ); + d_qi->d_tconstraints.erase(d_n); d_qni_bound_cons.clear(); } } @@ -1566,90 +1744,111 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { if( d_n.getKind()==OR || d_n.getKind()==AND ){ if( (d_n.getKind()==AND)==d_tgt ){ //all children must match simultaneously - if( getChild( d_child_counter )->getNextMatch( p, qi ) ){ + if (getChild(d_child_counter)->getNextMatch()) + { if( d_child_counter<(int)(getNumChildren()-1) ){ d_child_counter++; Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl; - getChild( d_child_counter )->reset( p, d_tgt, qi ); + getChild(d_child_counter)->reset(d_tgt); }else{ success = true; } - }else{ - //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){ - // d_child_counter--; - //}else{ + } + else + { d_child_counter--; - //} } }else{ //one child must match - if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){ + if (!getChild(d_child_counter)->getNextMatch()) + { if( d_child_counter<(int)(getNumChildren()-1) ){ d_child_counter++; Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl; - getChild( d_child_counter )->reset( p, d_tgt, qi ); + getChild(d_child_counter)->reset(d_tgt); }else{ d_child_counter = -1; } - }else{ + } + else + { success = true; } } }else if( d_n.getKind()==EQUAL ){ //construct match based on both children if( d_child_counter%2==0 ){ - if( getChild( 0 )->getNextMatch( p, qi ) ){ + if (getChild(0)->getNextMatch()) + { d_child_counter++; - getChild( 1 )->reset( p, d_child_counter==1, qi ); - }else{ + getChild(1)->reset(d_child_counter == 1); + } + else + { if( d_child_counter==0 ){ d_child_counter = 2; - getChild( 0 )->reset( p, !d_tgt, qi ); + getChild(0)->reset(!d_tgt); }else{ d_child_counter = -1; } } } if( d_child_counter>=0 && d_child_counter%2==1 ){ - if( getChild( 1 )->getNextMatch( p, qi ) ){ + if (getChild(1)->getNextMatch()) + { success = true; - }else{ + } + else + { d_child_counter--; } } }else if( d_n.getKind()==ITE ){ if( d_child_counter%2==0 ){ int index1 = d_child_counter==4 ? 1 : 0; - if( getChild( index1 )->getNextMatch( p, qi ) ){ + if (getChild(index1)->getNextMatch()) + { d_child_counter++; - getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi ); - }else{ + getChild(d_child_counter == 5 + ? 2 + : (d_tgt == (d_child_counter == 1) ? 1 : 2)) + ->reset(d_tgt); + } + else + { if (d_child_counter == 4) { d_child_counter = -1; }else{ d_child_counter +=2; - getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi ); + getChild(d_child_counter == 2 ? 0 : 1) + ->reset(d_child_counter == 2 ? !d_tgt : d_tgt); } } } if( d_child_counter>=0 && d_child_counter%2==1 ){ int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2); - if( getChild( index2 )->getNextMatch( p, qi ) ){ + if (getChild(index2)->getNextMatch()) + { success = true; - }else{ + } + else + { d_child_counter--; } } }else if( d_n.getKind()==FORALL ){ - if( getChild( d_child_counter )->getNextMatch( p, qi ) ){ + if (getChild(d_child_counter)->getNextMatch()) + { success = true; - }else{ + } + else + { d_child_counter = -1; } } } - d_wasSet = success; + d_wasSet = success; Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl; return success; } @@ -1658,128 +1857,178 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { return false; } -bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { - if( !d_qn.empty() ){ - if( d_qn[0]==NULL ){ - d_qn.clear(); - return true; - }else{ - Assert(d_type == typ_var); - Assert(d_qni_size > 0); - bool invalidMatch; - do { - invalidMatch = false; - Debug("qcf-match-debug") << " Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl; - if( d_qn.size()==d_qni.size()+1 ) { - int index = (int)d_qni.size(); - //initialize - TNode val; - std::map< int, int >::iterator itv = d_qni_var_num.find( index ); - if( itv!=d_qni_var_num.end() ){ - //get the representative variable this variable is equal to - int repVar = qi->getCurrentRepVar( itv->second ); - Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl; - //get the value the rep variable - //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar ); - if( !qi->d_match[repVar].isNull() ){ - val = qi->d_match[repVar]; - Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl; - }else{ - //binding a variable - d_qni_bound[index] = repVar; - std::map::iterator it = - d_qn[index]->d_data.begin(); - if( it != d_qn[index]->d_data.end() ) { - d_qni.push_back( it ); - //set the match - if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true, true ) ){ - Debug("qcf-match-debug") << " Binding variable" << std::endl; - if( d_qn.size()second ); - } - }else{ - Debug("qcf-match") << " Binding variable, currently fail." << std::endl; - invalidMatch = true; - } - }else{ - Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl; - d_qn.pop_back(); - } - } - }else{ - Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl; - Assert(d_qni_gterm.find(index) != d_qni_gterm.end()); - val = d_qni_gterm[index]; - Assert(!val.isNull()); - } - if( !val.isNull() ){ - Node valr = p->getRepresentative(val); - //constrained by val - std::map::iterator it = - d_qn[index]->d_data.find(valr); - if( it!=d_qn[index]->d_data.end() ){ - Debug("qcf-match-debug") << " Match" << std::endl; - d_qni.push_back( it ); +bool MatchGen::doMatching() +{ + if (d_qn.empty()) + { + return false; + } + if (d_qn[0] == NULL) + { + d_qn.clear(); + return true; + } + Assert(d_type == typ_var); + Assert(d_qni_size > 0); + bool invalidMatch; + do + { + invalidMatch = false; + Debug("qcf-match-debug") << " Do matching " << d_n << " " + << d_qn.size() << " " << d_qni.size() << std::endl; + if (d_qn.size() == d_qni.size() + 1) + { + size_t index = d_qni.size(); + // initialize + TNode val; + std::map::iterator itv = d_qni_var_num.find(index); + if (itv != d_qni_var_num.end()) + { + // get the representative variable this variable is equal to + size_t repVar = d_qi->getCurrentRepVar(itv->second); + Debug("qcf-match-debug") + << " Match " << index << " is a variable " << itv->second + << ", which is repVar " << repVar << std::endl; + // get the value the rep variable + if (!d_qi->d_match[repVar].isNull()) + { + val = d_qi->d_match[repVar]; + Debug("qcf-match-debug") + << " Variable is already bound to " << val << std::endl; + } + else + { + // binding a variable + d_qni_bound[index] = repVar; + std::map::iterator it = d_qn[index]->d_data.begin(); + if (it != d_qn[index]->d_data.end()) + { + d_qni.push_back(it); + // set the match + if (it->first.getType().isComparableTo(d_qi->d_var_types[repVar]) + && d_qi->setMatch(d_qni_bound[index], it->first, true, true)) + { + Debug("qcf-match-debug") + << " Binding variable" << std::endl; if( d_qn.size()second ); } - }else{ - Debug("qcf-match-debug") << " Failed to match" << std::endl; - d_qn.pop_back(); } - } - }else{ - Assert(d_qn.size() == d_qni.size()); - int index = d_qni.size()-1; - //increment if binding this variable - bool success = false; - std::map< int, int >::iterator itb = d_qni_bound.find( index ); - if( itb!=d_qni_bound.end() ){ - d_qni[index]++; - if( d_qni[index]!=d_qn[index]->d_data.end() ){ - success = true; - if( qi->setMatch( p, itb->second, d_qni[index]->first, true, true ) ){ - Debug("qcf-match-debug") << " Bind next variable" << std::endl; - if( d_qn.size()second ); - } - }else{ - Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl; - invalidMatch = true; - } - }else{ - qi->unsetMatch( p, itb->second ); - qi->d_match_term[ itb->second ] = TNode::null(); - Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl; + else + { + Debug("qcf-match") + << " Binding variable, currently fail." << std::endl; + invalidMatch = true; } - }else{ - //TODO : if it equal to something else, also try that } - //if not incrementing, move to next - if( !success ){ + else + { + Debug("qcf-match-debug") + << " Binding variable, fail, no more variables to bind" + << std::endl; d_qn.pop_back(); - d_qni.pop_back(); } } - }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch ); - if( d_qni.size()==d_qni_size ){ - //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() ); - //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl; - Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty()); - TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first; - Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl; - qi->d_match_term[d_qni_var_num[0]] = t; - //set the match terms - for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){ - Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl; - //if( it->second<(int)qi->d_q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term - if( it->first>0 ){ - Assert(!qi->d_match[it->second].isNull()); - Assert(p->areEqual(t[it->first - 1], qi->d_match[it->second])); - qi->d_match_term[it->second] = t[it->first-1]; + } + else + { + Debug("qcf-match-debug") + << " Match " << index << " is ground term" << std::endl; + Assert(d_qni_gterm.find(index) != d_qni_gterm.end()); + val = d_qni_gterm[index]; + Assert(!val.isNull()); + } + if (!val.isNull()) + { + Node valr = d_parent->getRepresentative(val); + // constrained by val + std::map::iterator it = + d_qn[index]->d_data.find(valr); + if (it != d_qn[index]->d_data.end()) + { + Debug("qcf-match-debug") << " Match" << std::endl; + d_qni.push_back(it); + if (d_qn.size() < d_qni_size) + { + d_qn.push_back(&it->second); + } + } + else + { + Debug("qcf-match-debug") << " Failed to match" << std::endl; + d_qn.pop_back(); + } + } + } + else + { + Assert(d_qn.size() == d_qni.size()); + size_t index = d_qni.size() - 1; + // increment if binding this variable + bool success = false; + std::map::iterator itb = d_qni_bound.find(index); + if (itb != d_qni_bound.end()) + { + d_qni[index]++; + if (d_qni[index] != d_qn[index]->d_data.end()) + { + success = true; + if (d_qi->setMatch(itb->second, d_qni[index]->first, true, true)) + { + Debug("qcf-match-debug") + << " Bind next variable" << std::endl; + if (d_qn.size() < d_qni_size) + { + d_qn.push_back(&d_qni[index]->second); + } + } + else + { + Debug("qcf-match-debug") + << " Bind next variable, currently fail" << std::endl; + invalidMatch = true; } - //} } + else + { + d_qi->unsetMatch(itb->second); + d_qi->d_match_term[itb->second] = TNode::null(); + Debug("qcf-match-debug") + << " Bind next variable, no more variables to bind" + << std::endl; + } + } + else + { + // TODO : if it equal to something else, also try that + } + // if not incrementing, move to next + if (!success) + { + d_qn.pop_back(); + d_qni.pop_back(); + } + } + } while ((!d_qn.empty() && d_qni.size() != d_qni_size) || invalidMatch); + if (d_qni.size() == d_qni_size) + { + Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty()); + TNode t = d_qni[d_qni.size() - 1]->second.d_data.begin()->first; + Debug("qcf-match-debug") + << " " << d_n << " matched " << t << std::endl; + d_qi->d_match_term[d_qni_var_num[0]] = t; + // set the match terms + Node q = d_qi->getQuantifiedFormula(); + for (const std::pair& qb : d_qni_bound) + { + Debug("qcf-match-debug") + << " position " << qb.first << " bounded " << qb.second << " / " + << q[0].getNumChildren() << std::endl; + if (qb.first > 0) + { + Assert(!d_qi->d_match[qb.second].isNull()); + Assert(d_parent->areEqual(t[qb.first - 1], d_qi->d_match[qb.second])); + d_qi->d_match_term[qb.second] = t[qb.first - 1]; } } } @@ -1827,14 +2076,6 @@ bool MatchGen::isHandledUfTerm( TNode n ) { return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind()); } -Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) { - if( isHandledUfTerm( n ) ){ - return p->getTermDatabase()->getMatchOperator( n ); - }else{ - return Node::null(); - } -} - bool MatchGen::isHandled( TNode n ) { if (n.getKind() != BOUND_VARIABLE && expr::hasBoundVar(n)) { @@ -1857,8 +2098,6 @@ QuantConflictFind::QuantConflictFind(Env& env, TermRegistry& tr) : QuantifiersModule(env, qs, qim, qr, tr), d_conflict(context(), false), - d_true(NodeManager::currentNM()->mkConst(true)), - d_false(NodeManager::currentNM()->mkConst(false)), d_effort(EFFORT_INVALID) { } @@ -1866,54 +2105,48 @@ QuantConflictFind::QuantConflictFind(Env& env, //-------------------------------------------------- registration void QuantConflictFind::registerQuantifier( Node q ) { - if (d_qreg.hasOwnership(q, this)) + if (!d_qreg.hasOwnership(q, this)) { - d_quants.push_back( q ); - d_quant_id[q] = d_quants.size(); - if( Trace.isOn("qcf-qregister") ){ - Trace("qcf-qregister") << "Register "; - debugPrintQuant( "qcf-qregister", q ); - Trace("qcf-qregister") << " : " << q << std::endl; - } - //make QcfNode structure - Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl; - d_qinfo[q].initialize( this, q, q[1] ); - - //debug print - if( Trace.isOn("qcf-qregister") ){ - Trace("qcf-qregister") << "- Flattened structure is :" << std::endl; - Trace("qcf-qregister") << " "; - debugPrintQuantBody( "qcf-qregister", q, q[1] ); - Trace("qcf-qregister") << std::endl; - if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){ - Trace("qcf-qregister") << " with additional constraints : " << std::endl; - for( unsigned j=q[0].getNumChildren(); jd_vars.size() > q[0].getNumChildren()) + { + Trace("qcf-qregister") << " with additional constraints : " << std::endl; + for (size_t j = q[0].getNumChildren(), nvars = qi->d_vars.size(); + j < nvars; + j++) + { + Trace("qcf-qregister") << " ?x" << j << " = "; + debugPrintQuantBody("qcf-qregister", q, qi->d_vars[j], false); + Trace("qcf-qregister") << std::endl; } - Trace("qcf-qregister") << "Done registering quantifier." << std::endl; } + Trace("qcf-qregister") << "Done registering quantifier." << std::endl; } } -bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) { - //if( d_effort==QuantConflictFind::effort_mc ){ - // return n1==n2 || !areDisequal( n1, n2 ); - //}else{ - return n1==n2; - //} -} - -bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { - // if( d_effort==QuantConflictFind::Effort::Conflict ){ - // return areDisequal( n1, n2 ); - //}else{ - return n1!=n2; - //} -} - //-------------------------------------------------- check function bool QuantConflictFind::needsCheck( Theory::Effort level ) { @@ -2094,8 +2327,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas) { - QuantInfo* qi = &d_qinfo[q]; Assert(d_qinfo.find(q) != d_qinfo.end()); + QuantInfo* qi = d_qinfo[q].get(); if (!qi->matchGeneratorIsValid()) { // quantified formula is not properly set up for matching @@ -2109,7 +2342,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, } Trace("qcf-check-debug") << "Reset round..." << std::endl; - if (!qi->reset_round(this)) + if (!qi->reset_round()) { // it is typically the case that another conflict (e.g. in the term // database) was discovered if we fail here. @@ -2118,7 +2351,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, // try to make a matches making the body false or propagating Trace("qcf-check-debug") << "Get next match..." << std::endl; Instantiate* qinst = d_qim.getInstantiate(); - while (qi->getNextMatch(this)) + while (qi->getNextMatch()) { if (d_qstate.isInConflict()) { @@ -2136,15 +2369,15 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, Trace("qcf-inst") << std::endl; } // check whether internal match constraints are satisfied - if (qi->isMatchSpurious(this)) + if (qi->isMatchSpurious()) { Trace("qcf-inst") << " ... Spurious (match is inconsistent)" << std::endl; continue; } // check whether match can be completed - std::vector assigned; - if (!qi->completeMatch(this, assigned)) + std::vector assigned; + if (!qi->completeMatch(assigned)) { Trace("qcf-inst") << " ... Spurious (cannot assign unassigned vars)" << std::endl; @@ -2153,7 +2386,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, // check whether the match is spurious according to (T-)entailment checks std::vector terms; qi->getMatch(terms); - bool tcs = qi->isTConstraintSpurious(this, terms); + bool tcs = qi->isTConstraintSpurious(terms); if (tcs) { Trace("qcf-inst") << " ... Spurious (match is T-inconsistent)" @@ -2168,8 +2401,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, Node inst = qinst->getInstantiation(q, terms); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert(!getTermRegistry().getEntailmentCheck()->isEntailed(inst, true)); - Assert(getTermRegistry().getEntailmentCheck()->isEntailed(inst, false) + Assert(!d_treg.getEntailmentCheck()->isEntailed(inst, true)); + Assert(d_treg.getEntailmentCheck()->isEntailed(inst, false) || d_effort > EFFORT_CONFLICT); } // Process the lemma: either add an instantiation or specific lemmas @@ -2217,7 +2450,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, } } // clean up assigned - qi->revertMatch(this, assigned); + qi->revertMatch(assigned); d_tempCache.clear(); } Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; @@ -2225,7 +2458,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, //-------------------------------------------------- debugging -void QuantConflictFind::debugPrint( const char * c ) { +void QuantConflictFind::debugPrint(const char* c) const +{ //print the equivalance classes Trace(c) << "----------EQ classes" << std::endl; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); @@ -2248,28 +2482,53 @@ void QuantConflictFind::debugPrint( const char * c ) { } } -void QuantConflictFind::debugPrintQuant( const char * c, Node q ) { - Trace(c) << "Q" << d_quant_id[q]; +void QuantConflictFind::debugPrintQuant(const char* c, Node q) const +{ + std::map::const_iterator it = d_quant_id.find(q); + if (it == d_quant_id.end()) + { + Trace(c) << q; + return; + } + Trace(c) << "Q" << it->second; } -void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) { +void QuantConflictFind::debugPrintQuantBody(const char* c, + Node q, + Node n, + bool doVarNum) const +{ if( n.getNumChildren()==0 ){ Trace(c) << n; - }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){ - Trace(c) << "?x" << d_qinfo[q].d_var_num[n]; - }else{ - Trace(c) << "("; - if( n.getKind()==APPLY_UF ){ - Trace(c) << n.getOperator(); - }else{ - Trace(c) << n.getKind(); - } - for( unsigned i=0; i >::const_iterator itq = + d_qinfo.find(q); + if (itq != d_qinfo.end()) + { + const QuantInfo* qi = itq->second.get(); + std::map::const_iterator itv = qi->d_var_num.find(n); + if (doVarNum && itv != qi->d_var_num.end()) + { + Trace(c) << "?x" << itv->second; + return; } - Trace(c) << ")"; } + Trace(c) << "("; + if (n.getKind() == APPLY_UF) + { + Trace(c) << n.getOperator(); + } + else + { + Trace(c) << n.getKind(); + } + for (const Node& nc : n) + { + Trace(c) << " "; + debugPrintQuantBody(c, q, nc); + } + Trace(c) << ")"; } QuantConflictFind::Statistics::Statistics() diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 82a925d3b..c9cce84b9 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -36,37 +36,10 @@ class QuantInfo; //match generator class MatchGen { friend class QuantInfo; -private: - //current children information - int d_child_counter; - bool d_use_children; - //children of this object - std::vector< int > d_children_order; - unsigned getNumChildren() { return d_children.size(); } - MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; } - //MatchGen * getChild( int i ) { return &d_children[i]; } - //current matching information - std::vector d_qn; - std::vector::iterator> d_qni; - bool doMatching( QuantConflictFind * p, QuantInfo * qi ); - //for matching : each index is either a variable or a ground term - unsigned d_qni_size; - std::map< int, int > d_qni_var_num; - std::map< int, TNode > d_qni_gterm; - std::map< int, int > d_qni_bound; - std::vector< int > d_qni_bound_except; - std::map< int, TNode > d_qni_bound_cons; - std::map< int, int > d_qni_bound_cons_var; - std::map< int, int >::iterator d_binding_it; - //std::vector< int > d_independent; - bool d_matched_basis; - bool d_binding; - //int getVarBindingVar(); - std::map< int, Node > d_ground_eval; - //determine variable order - void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ); - void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested ); -public: + + public: + MatchGen(QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar = false); + //type of the match generator enum { typ_invalid, @@ -80,14 +53,12 @@ public: typ_tsym, }; void debugPrintType( const char * c, short typ, bool isTrace = false ); -public: - MatchGen(); - MatchGen( QuantInfo * qi, Node n, bool isVar = false ); + bool d_tgt; bool d_tgt_orig; bool d_wasSet; Node d_n; - std::vector< MatchGen > d_children; + std::vector > d_children; short d_type; bool d_type_not; /** reset round @@ -96,146 +67,140 @@ public: * processing this match generator. This method returns false if the reset * failed, e.g. if a conflict was encountered during term indexing. */ - bool reset_round(QuantConflictFind* p); - void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ); - bool getNextMatch( QuantConflictFind * p, QuantInfo * qi ); - bool isValid() { return d_type!=typ_invalid; } + bool reset_round(); + void reset(bool tgt); + bool getNextMatch(); + bool isValid() const { return d_type != typ_invalid; } void setInvalid(); + Node getNode() const { return d_n; } // is this term treated as UF application? static bool isHandledBoolConnective( TNode n ); static bool isHandledUfTerm( TNode n ); - static Node getMatchOperator( QuantConflictFind * p, Node n ); //can this node be handled by the algorithm static bool isHandled( TNode n ); -}; - -//info for quantifiers -class QuantInfo { -private: - void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false ); - void flatten( Node n, bool beneathQuant ); -private: //for completing match - std::vector< int > d_unassigned; - std::vector< TypeNode > d_unassigned_tn; - int d_unassigned_nvar; - int d_una_index; - std::vector< int > d_una_eqc_count; - //optimization: track which arguments variables appear under UF terms in - std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom; - void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ); - //optimization: number of variables set, to track when we can stop - std::map< int, bool > d_vars_set; - std::vector< Node > d_extra_var; -public: - bool isBaseMatchComplete(); -public: - QuantInfo(); - ~QuantInfo(); - std::vector< TNode > d_vars; - std::vector< TypeNode > d_var_types; - std::map< TNode, int > d_var_num; - std::vector< int > d_tsym_vars; - std::map< TNode, bool > d_inMatchConstraint; - int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; } - bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); } - int getNumVars() { return (int)d_vars.size(); } - TNode getVar( int i ) { return d_vars[i]; } - typedef std::map< int, MatchGen * > VarMgMap; private: + // determine variable order + void determineVariableOrder(std::vector& bvars); + void collectBoundVar(Node n, + std::vector& cbvars, + std::map& visited, + bool& hasNested); + size_t getNumChildren() const { return d_children.size(); } + MatchGen* getChild(size_t i) const + { + return d_children[d_children_order[i]].get(); + } + bool doMatching(); /** The parent who owns this class */ QuantConflictFind* d_parent; - MatchGen * d_mg; - VarMgMap d_var_mg; + /** Quantifier info of the parent */ + QuantInfo* d_qi; + // current children information + int d_child_counter; + bool d_use_children; + // children of this object + std::vector d_children_order; + // current matching information + std::vector d_qn; + std::vector::iterator> d_qni; + // for matching : each index is either a variable or a ground term + size_t d_qni_size; + std::map d_qni_var_num; + std::map d_qni_gterm; + std::map d_qni_bound; + std::vector d_qni_bound_except; + std::map d_qni_bound_cons; + std::map d_qni_bound_cons_var; + std::map::iterator d_binding_it; + bool d_matched_basis; + bool d_binding; + // int getVarBindingVar(); + std::map d_ground_eval; +}; + +//info for quantifiers +class QuantInfo : protected EnvObj +{ public: - VarMgMap::const_iterator var_mg_find(int i) const { return d_var_mg.find(i); } + typedef std::map VarMgMap; + QuantInfo(Env& env, QuantConflictFind* p, Node q); + ~QuantInfo(); + /** get quantified formula */ + Node getQuantifiedFormula() const; + bool isBaseMatchComplete(); + /** Get quantifiers inference manager */ + QuantifiersInferenceManager& getInferenceManager(); + std::vector d_vars; + std::vector d_var_types; + std::map d_var_num; + std::vector d_tsym_vars; + int getVarNum(TNode v) const; + bool isVar(TNode v) const { return d_var_num.find(v) != d_var_num.end(); } + size_t getNumVars() const { return d_vars.size(); } + TNode getVar(size_t i) const { return d_vars[i]; } + VarMgMap::const_iterator var_mg_find(size_t i) const + { + return d_var_mg.find(i); + } VarMgMap::const_iterator var_mg_end() const { return d_var_mg.end(); } - bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); } - + bool containsVarMg(size_t i) const { return var_mg_find(i) != var_mg_end(); } bool matchGeneratorIsValid() const { return d_mg->isValid(); } - bool getNextMatch( QuantConflictFind * p ) { - return d_mg->getNextMatch(p, this); - } - - Node d_q; - bool reset_round( QuantConflictFind * p ); -public: - //initialize - void initialize( QuantConflictFind * p, Node q, Node qn ); - //current constraints - std::vector< TNode > d_match; - std::vector< TNode > d_match_term; - std::map< int, std::map< TNode, int > > d_curr_var_deq; - std::map< Node, bool > d_tconstraints; - int getCurrentRepVar( int v ); + bool getNextMatch() { return d_mg->getNextMatch(); } + bool reset_round(); + size_t getCurrentRepVar(size_t v); TNode getCurrentValue( TNode n ); TNode getCurrentExpValue( TNode n ); - bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false ); - int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ); - int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ); - bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround ); - void unsetMatch( QuantConflictFind * p, int v ); - bool isMatchSpurious( QuantConflictFind * p ); - bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ); - bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true ); - bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false ); - void revertMatch( QuantConflictFind * p, std::vector< int >& assigned ); - void debugPrintMatch( const char * c ); - bool isConstrainedVar( int v ); -public: + bool getCurrentCanBeEqual(size_t v, TNode n, bool chDiseq = false); + int addConstraint(size_t v, TNode n, bool polarity); + int addConstraint(size_t v, TNode n, int vn, bool polarity, bool doRemove); + bool setMatch(size_t v, TNode n, bool isGroundRep, bool isGround); + void unsetMatch(size_t v); + bool isMatchSpurious(); + bool isTConstraintSpurious(const std::vector& terms); + bool entailmentTest(Node lit, bool chEnt = true); + bool completeMatch(std::vector& assigned, bool doContinue = false); + void revertMatch(const std::vector& assigned); + void debugPrintMatch(const char* c) const; + bool isConstrainedVar(size_t v); void getMatch( std::vector< Node >& terms ); + + // current constraints + std::vector d_match; + std::vector d_match_term; + std::map > d_curr_var_deq; + std::map d_tconstraints; + + private: + void registerNode(Node n, bool hasPol, bool pol, bool beneathQuant = false); + void flatten(Node n, bool beneathQuant); + void getPropagateVars(std::vector& vars, + TNode n, + bool pol, + std::map& visited); + /** The parent who owns this class */ + QuantConflictFind* d_parent; + std::unique_ptr d_mg; + Node d_q; + VarMgMap d_var_mg; + // for completing match + std::vector d_unassigned; + std::vector d_unassigned_tn; + size_t d_unassigned_nvar; + size_t d_una_index; + std::vector d_una_eqc_count; + // optimization: track which arguments variables appear under UF terms in + std::map > > d_var_rel_dom; + // optimization: number of variables set, to track when we can stop + std::unordered_set d_vars_set; + std::vector d_extra_var; }; class QuantConflictFind : public QuantifiersModule { friend class MatchGen; friend class QuantInfo; - typedef context::CDHashMap NodeBoolMap; - - private: - context::CDO< bool > d_conflict; - std::map, Node> d_zero; - //for storing nodes created during t-constraint solving (prevents memory leaks) - std::vector< Node > d_tempCache; - //optimization: list of quantifiers that depend on ground function applications - std::map< TNode, std::vector< Node > > d_func_rel_dom; - std::map< TNode, bool > d_irr_func; - std::map< Node, bool > d_irr_quant; - void setIrrelevantFunction( TNode f ); -private: - std::map< Node, Node > d_op_node; - std::map< Node, int > d_fid; -public: //for ground terms - Node d_true; - Node d_false; - TNode getZero(TypeNode tn, Kind k); - - private: - std::map< Node, QuantInfo > d_qinfo; -private: //for equivalence classes - // type -> list(eqc) - std::map< TypeNode, std::vector< TNode > > d_eqcs; - - public: - enum Effort : unsigned { - EFFORT_CONFLICT, - EFFORT_PROP_EQ, - EFFORT_INVALID, - }; - void setEffort(Effort e) { d_effort = e; } - - inline bool atConflictEffort() const { - return d_effort == QuantConflictFind::EFFORT_CONFLICT; - } - - private: - Effort d_effort; - - public: - bool areMatchEqual( TNode n1, TNode n2 ); - bool areMatchDisequal( TNode n1, TNode n2 ); - public: QuantConflictFind(Env& env, QuantifiersState& qs, @@ -245,8 +210,6 @@ private: //for equivalence classes /** register quantifier */ void registerQuantifier(Node q) override; - - public: /** needs check */ bool needsCheck(Theory::Effort level) override; /** reset round */ @@ -259,29 +222,6 @@ private: //for equivalence classes */ void check(Theory::Effort level, QEffort quant_e) override; - private: - /** check quantified formula - * - * This method is called by the above check method for each quantified - * formula q. It attempts to find a conflicting or propagating instance for - * q, depending on the effort level (d_effort). - * - * isConflict: this is set to true if we discovered a conflicting instance. - * This flag may be set instead of d_conflict if --qcf-all-conflict is true, - * in which we continuing adding all conflicts. - * addedLemmas: tracks the total number of lemmas added, and is incremented by - * this method when applicable. - */ - void checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas); - - private: - void debugPrint( const char * c ); - //for debugging - std::vector< Node > d_quants; - std::map< Node, int > d_quant_id; - void debugPrintQuant( const char * c, Node q ); - void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true ); -public: /** statistics class */ class Statistics { public: @@ -308,6 +248,64 @@ public: * algorithm performed by this class. */ bool isPropagatingInstance(Node n) const; + + enum Effort : unsigned + { + EFFORT_CONFLICT, + EFFORT_PROP_EQ, + EFFORT_INVALID, + }; + void setEffort(Effort e) { d_effort = e; } + + bool atConflictEffort() const + { + return d_effort == QuantConflictFind::EFFORT_CONFLICT; + } + + TNode getZero(TypeNode tn, Kind k); + + private: + /** check quantified formula + * + * This method is called by the above check method for each quantified + * formula q. It attempts to find a conflicting or propagating instance for + * q, depending on the effort level (d_effort). + * + * isConflict: this is set to true if we discovered a conflicting instance. + * This flag may be set instead of d_conflict if --qcf-all-conflict is true, + * in which we continuing adding all conflicts. + * addedLemmas: tracks the total number of lemmas added, and is incremented by + * this method when applicable. + */ + void checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas); + void debugPrint(const char* c) const; + void debugPrintQuant(const char* c, Node q) const; + void debugPrintQuantBody(const char* c, + Node q, + Node n, + bool doVarNum = true) const; + void setIrrelevantFunction(TNode f); + // for debugging + std::vector d_quants; + std::map d_quant_id; + /** Map from quantified formulas to their info class to compute instances */ + std::map > d_qinfo; + /** Map from type -> list(eqc) of that type */ + std::map > d_eqcs; + /** Are we in conflict? */ + context::CDO d_conflict; + /** Zeros for (type, kind) pairs */ + std::map, Node> d_zero; + // for storing nodes created during t-constraint solving (prevents memory + // leaks) + std::vector d_tempCache; + // optimization: list of quantifiers that depend on ground function + // applications + std::map > d_func_rel_dom; + std::map d_irr_func; + std::map d_irr_quant; + /** The current effort */ + Effort d_effort; }; std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);