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; i<q[0].getNumChildren(); i++ ){
- d_match.push_back( TNode::null() );
- d_match_term.push_back( TNode::null() );
- }
//register the variables
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- d_var_num[q[0][i]] = i;
- d_vars.push_back( q[0][i] );
- d_var_types.push_back( q[0][i].getType() );
+ for (size_t i = 0, nvars = d_q[0].getNumChildren(); i < nvars; i++)
+ {
+ Node v = d_q[0][i];
+ d_match.push_back(TNode::null());
+ d_match_term.push_back(TNode::null());
+ d_var_num[v] = i;
+ d_vars.push_back(v);
+ d_var_types.push_back(v.getType());
}
registerNode( qn, true, true );
Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
- d_mg = new MatchGen( this, qn );
+ d_mg.reset(new MatchGen(p, this, qn));
if( d_mg->isValid() ){
- /*
- for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
- if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
- Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
- d_mg->setInvalid();
- break;
- }
- }
- */
- for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+ for (size_t j = q[0].getNumChildren(), nvars = d_vars.size(); j < nvars;
+ j++)
+ {
if( d_vars[j].getKind()!=BOUND_VARIABLE ){
d_var_mg[j] = NULL;
bool is_tsym = false;
d_tsym_vars.push_back( j );
}
if( !is_tsym || options::qcfTConstraint() ){
- d_var_mg[j] = new MatchGen( this, d_vars[j], true );
+ d_var_mg[j] = new MatchGen(p, this, d_vars[j], true);
}
if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
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<size_t> bvars;
+ d_var_mg[j]->determineVariableOrder(bvars);
}
}
}
if( d_mg->isValid() ){
- std::vector< int > bvars;
- d_mg->determineVariableOrder( this, bvars );
+ std::vector<size_t> bvars;
+ d_mg->determineVariableOrder(bvars);
}
}else{
Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
}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; j<vars.size(); j++ ){
- Node v = vars[j];
+ for (TNode v : vars)
+ {
TNode f = p->getTermDatabase()->getMatchOperator( v );
if( !f.isNull() ){
Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
- for( unsigned k=0; k<v.getNumChildren(); k++ ){
+ for (size_t k = 0, vnchild = v.getNumChildren(); k < vnchild; k++)
+ {
Node n = v[k];
- std::map< TNode, int >::iterator itv = d_var_num.find( n );
+ std::map<TNode, size_t>::iterator itv = d_var_num.find(n);
if( itv!=d_var_num.end() ){
+ std::vector<size_t>& 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<TNode>& vars,
+ TNode n,
+ bool pol,
+ std::map<TNode, bool>& visited)
+{
std::map< TNode, bool >::iterator itv = visited.find( n );
if( itv==visited.end() ){
visited[n] = true;
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<Node>& 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 ) ){
}
Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
if( rec ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- getPropagateVars( p, vars, n[i], pol, visited );
+ for (const Node& nc : n)
+ {
+ getPropagateVars(vars, nc, pol, visited);
}
}
}
Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
if (expr::hasBoundVar(n))
{
- if( n.getKind()==BOUND_VARIABLE ){
- d_inMatchConstraint[n] = true;
- }
if( d_var_num.find( n )==d_var_num.end() ){
Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
d_var_num[n] = d_vars.size();
}
}
+int QuantInfo::getVarNum(TNode v) const
+{
+ std::map<TNode, size_t>::const_iterator it = d_var_num.find(v);
+ return it != d_var_num.end() ? static_cast<int>(it->second) : -1;
+}
-bool QuantInfo::reset_round( QuantConflictFind * p ) {
- for( unsigned i=0; i<d_match.size(); i++ ){
+bool QuantInfo::reset_round()
+{
+ for (size_t i = 0, nmatch = d_match.size(); i < nmatch; i++)
+ {
d_match[i] = TNode::null();
d_match_term[i] = TNode::null();
}
d_vars_set.clear();
d_curr_var_deq.clear();
d_tconstraints.clear();
-
- d_mg->reset_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<const size_t, MatchGen*>& 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<TNode, size_t>::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<TNode, size_t>::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<TNode, size_t>::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<size_t, std::map<TNode, size_t> >::iterator itd =
+ d_curr_var_deq.find(v);
+ if (itd == d_curr_var_deq.end())
+ {
+ return true;
+ }
+ for (std::pair<const TNode, size_t>& 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<int>(getCurrentRepVar(static_cast<size_t>(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<size_t>(vn)
+ == getCurrentRepVar(static_cast<size_t>(getVarNum(n)))));
if( polarity ){
- if( vn!=v ){
+ if (vn != static_cast<int>(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<size_t, std::map<TNode, size_t> >::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<const TNode, size_t>& dd : itd->second)
+ {
+ if (dd.second == v)
+ {
+ remDeq.push_back(dd.first);
}
}
- for( unsigned i=0; i<remDeq.size(); i++ ){
- d_curr_var_deq[vn].erase( remDeq[i] );
+ for (TNode rd : remDeq)
+ {
+ itd->second.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;
}
//copy or check disequalities
- std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
+ std::map<size_t, std::map<TNode, size_t> >::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<TNode, size_t>& cvd = d_curr_var_deq[vn];
+ for (const std::pair<const TNode, size_t>& 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 ){
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{
}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<int>(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 );
}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;
}
}
}
-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<size_t, std::map<TNode, size_t> >::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_match.size(); i++ ){
- if( d_match[i]==vv ){
+ }
+ TNode vv = getVar(v);
+ if (std::find(d_match.begin(), d_match.end(), vv) != d_match.end())
+ {
+ return true;
+ }
+ for (const std::pair<const size_t, std::map<TNode, size_t> >& d :
+ d_curr_var_deq)
+ {
+ for (const std::pair<const TNode, size_t>& 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; j<it2->second.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<size_t, std::map<TNode, std::vector<size_t> > >::iterator it =
+ d_var_rel_dom.find(v);
+ if (it != d_var_rel_dom.end())
+ {
+ TermDb* tdb = d_parent->getTermDatabase();
+ for (std::pair<const TNode, std::vector<size_t> >& 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 );
d_match[ v ] = TNode::null();
}
-bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
- for( int i=0; i<getNumVars(); i++ ){
- //std::map< int, TNode >::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;
}
}
return false;
}
-bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
- std::vector<Node>& terms)
+bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
{
if( options::qcfEagerTest() ){
+ EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
//check whether the instantiation evaluates as expected
- EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
std::map<TNode, TNode> subs;
for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
{
<< " " << 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))
{
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; i<terms.size(); i++ ){
- Trace("qcf-instance-check") << " " << terms[i] << std::endl;
- }
+ Trace("qcf-instance-check") << " " << terms << std::endl;
Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
}
// If it is the case that instantiation can be rewritten to a Boolean
}else{
if (Configuration::isDebugBuild())
{
- if (!p->isPropagatingInstance(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
}
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 "
// 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<bool, Node> et = p->getState().getValuation().entailmentCheck(
- options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
- ++(p->d_statistics.d_entailment_checks);
+ std::pair<bool, Node> 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)
return chEnt;
}
-bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
+bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
+{
//assign values for variables that were unassigned (usually not necessary, but handles corner cases)
bool doFail = false;
bool success = true;
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; j<d_vars[index].getNumChildren(); j++ ){
- int vn = getVarNum( d_vars[index][j] );
+ for (const Node& vi : d_vars[index]){
+ int vn = getVarNum( vi );
if( vn!=-1 ){
- TNode vv = getCurrentValue( d_vars[index][j] );
- if( vv==d_vars[index][j] ){
+ TNode vv = getCurrentValue( vi );
+ if( vv==vi ){
//we will assign this
if( slv_v==-1 ){
Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
slv_v = vn;
- if (!p->atConflictEffort()) {
+ 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<size_t>(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;
}
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{
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;
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);
}
}
}
//check what is left to assign
d_unassigned.clear();
d_unassigned_tn.clear();
- std::vector< int > unassigned[2];
+ std::vector<size_t> unassigned[2];
std::vector< TypeNode > unassigned_tn[2];
- for( int i=0; i<getNumVars(); i++ ){
+ for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
+ {
if( d_match[i].isNull() ){
int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
unassigned[rindex].push_back( i );
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_index<d_unassigned_nvar ){
if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
d_una_eqc_count.push_back( -1 );
}else{
- d_var_mg[ d_unassigned[d_una_index] ]->reset( 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_index<d_unassigned_nvar ){
if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
d_una_index++;
- }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( 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<TNode>& eqcs =
+ d_parent->d_eqcs[d_unassigned_tn[d_una_index]];
+ if (d_una_eqc_count[d_una_index] < static_cast<int>(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;
}
}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_unassigned.size(); i++ ){
- int ui = d_unassigned[i];
- if( !d_match[ui].isNull() ){
- Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << 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_unassigned.size(); i++ ){
- int ui = d_unassigned[i];
- if( !d_match[ui].isNull() ){
- Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << 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; i<d_q[0].getNumChildren(); i++ ){
- //Node cv = qi->getCurrentValue( 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{
}
}
-void QuantInfo::revertMatch( QuantConflictFind * p, std::vector< int >& assigned ) {
- for( unsigned i=0; i<assigned.size(); i++ ){
- unsetMatch( p, assigned[i] );
+void QuantInfo::revertMatch(const std::vector<size_t>& assigned)
+{
+ for (size_t a : assigned)
+ {
+ unsetMatch(a);
}
}
-void QuantInfo::debugPrintMatch( const char * c ) {
- for( int i=0; i<getNumVars(); i++ ){
+void QuantInfo::debugPrintMatch(const char* c) const
+{
+ for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
+ {
Trace(c) << " " << d_vars[i] << " -> ";
if( !d_match[i].isNull() ){
Trace(c) << d_match[i];
}else{
Trace(c) << "(unassigned) ";
}
- if( !d_curr_var_deq[i].empty() ){
+ std::map<size_t, std::map<TNode, size_t> >::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<const TNode, size_t>& d : itc->second)
+ {
+ Trace(c) << d.first << " ";
}
Trace(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<const Node, bool>& 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;
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<size_t>(vn);
d_qni_size++;
d_type_not = false;
d_n = n;
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 );
d_type = typ_formula;
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
if( d_n.getKind()!=FORALL || i==1 ){
- d_children.push_back( MatchGen( qi, d_n[i], false ) );
- if( !d_children[d_children.size()-1].isValid() ){
+ std::unique_ptr<MatchGen> mg =
+ std::make_unique<MatchGen>(p, qi, d_n[i], false);
+ if (!mg->isValid())
+ {
setInvalid();
break;
}
+ d_children.push_back(std::move(mg));
}
}
}else{
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<int>& cbvars,
+ std::map<Node, bool>& 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<n.getNumChildren(); i++ ){
- collectBoundVar( qi, n[i], cbvars, visited, hasNested );
+ for (const Node& nc : n)
+ {
+ collectBoundVar(nc, cbvars, visited, hasNested);
}
}
}
-void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
+void MatchGen::determineVariableOrder(std::vector<size_t>& 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 ){
std::map< int, bool > has_nested;
std::vector< bool > assigned;
Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
- for( unsigned i=0; i<d_children.size(); i++ ){
+ for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
+ {
std::map< Node, bool > 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;
}
//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<d_children.size(); i++ ){
+ for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
+ {
if( !assigned[i] ){
Trace("qcf-qregister-debug2") << "Child " << i << " has b/ub : " << vb_count[i] << "/" << vu_count[i] << std::endl;
int score0 = 0;//has_nested[i] ? 0 : 1;
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<min_score0 || ( score0==min_score0 && score<min_score ) ){
min_score0 = score0;
}
}
}
- 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;
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 ){
}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; i<d_children.size(); i++ ){
+ for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
+ {
d_children_order.push_back( i );
- d_children[i].determineVariableOrder( qi, bvars );
+ d_children[i]->determineVariableOrder(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<cvars.size(); j++ ){
if( std::find( bvars.begin(), bvars.end(), cvars[j] )==bvars.end() ){
bvars.push_back( cvars[j] );
}
}
-bool MatchGen::reset_round(QuantConflictFind* p)
+bool MatchGen::reset_round()
{
d_wasSet = false;
- for( unsigned i=0; i<d_children.size(); i++ ){
- if (!d_children[i].reset_round(p))
+ for (std::unique_ptr<MatchGen>& 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())
{
}
}
}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]))
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 );
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<bool>() == 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<size_t>(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<const size_t, size_t>& 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<size_t>(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<int, TNode>::iterator it = d_qni_gterm.find(i);
+ std::map<size_t, TNode>::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<size_t>(vnn));
}
}
bool success;
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{
}
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];
}
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);
}
}
}
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;
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<Node, bool>::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;
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;
--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;
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<size_t, size_t>::iterator itb;
+ for (const std::pair<const size_t, TNode>& 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();
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<const size_t, size_t>& 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();
}
}
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;
}
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<TNode, TNodeTrie>::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()<d_qni_size ){
- d_qn.push_back( &it->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<TNode, TNodeTrie>::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<size_t, size_t>::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<TNode, TNodeTrie>::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()<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());
- 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()<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{
- 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<TNode, TNodeTrie>::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<size_t, size_t>::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<const size_t, size_t>& 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];
}
}
}
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))
{
TermRegistry& tr)
: QuantifiersModule(env, qs, qim, qr, tr),
d_conflict(context(), false),
- d_true(NodeManager::currentNM()->mkConst<bool>(true)),
- d_false(NodeManager::currentNM()->mkConst<bool>(false)),
d_effort(EFFORT_INVALID)
{
}
//-------------------------------------------------- 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(); j<d_qinfo[q].d_vars.size(); j++ ){
- Trace("qcf-qregister") << " ?x" << j << " = ";
- debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
- Trace("qcf-qregister") << std::endl;
- }
+ return;
+ }
+ 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].reset(new QuantInfo(d_env, this, q));
+
+ // debug print
+ if (Trace.isOn("qcf-qregister"))
+ {
+ QuantInfo* qi = d_qinfo[q].get();
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
+ Trace("qcf-qregister") << " ";
+ debugPrintQuantBody("qcf-qregister", q, q[1]);
+ Trace("qcf-qregister") << std::endl;
+ if (qi->d_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 ) {
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
}
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.
// 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())
{
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<int> assigned;
- if (!qi->completeMatch(this, assigned))
+ std::vector<size_t> assigned;
+ if (!qi->completeMatch(assigned))
{
Trace("qcf-inst") << " ... Spurious (cannot assign unassigned vars)"
<< std::endl;
// check whether the match is spurious according to (T-)entailment checks
std::vector<Node> 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)"
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
}
}
// clean up assigned
- qi->revertMatch(this, assigned);
+ qi->revertMatch(assigned);
d_tempCache.clear();
}
Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
//-------------------------------------------------- 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() );
}
}
-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<Node, size_t>::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<n.getNumChildren(); i++ ){
- Trace(c) << " ";
- debugPrintQuantBody( c, q, n[i] );
+ return;
+ }
+ std::map<Node, std::unique_ptr<QuantInfo> >::const_iterator itq =
+ d_qinfo.find(q);
+ if (itq != d_qinfo.end())
+ {
+ const QuantInfo* qi = itq->second.get();
+ std::map<TNode, size_t>::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()
//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<TNodeTrie*> d_qn;
- std::vector<std::map<TNode, TNodeTrie>::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,
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<std::unique_ptr<MatchGen> > d_children;
short d_type;
bool d_type_not;
/** reset round
* 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<size_t>& bvars);
+ void collectBoundVar(Node n,
+ std::vector<int>& cbvars,
+ std::map<Node, bool>& 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<size_t> d_children_order;
+ // current matching information
+ std::vector<TNodeTrie*> d_qn;
+ std::vector<std::map<TNode, TNodeTrie>::iterator> d_qni;
+ // for matching : each index is either a variable or a ground term
+ size_t d_qni_size;
+ std::map<size_t, size_t> d_qni_var_num;
+ std::map<size_t, TNode> d_qni_gterm;
+ std::map<size_t, size_t> d_qni_bound;
+ std::vector<size_t> d_qni_bound_except;
+ std::map<size_t, TNode> d_qni_bound_cons;
+ std::map<size_t, size_t> d_qni_bound_cons_var;
+ std::map<size_t, size_t>::iterator d_binding_it;
+ bool d_matched_basis;
+ bool d_binding;
+ // int getVarBindingVar();
+ std::map<size_t, Node> 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<size_t, MatchGen*> 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<TNode> d_vars;
+ std::vector<TypeNode> d_var_types;
+ std::map<TNode, size_t> d_var_num;
+ std::vector<size_t> 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<Node>& terms);
+ bool entailmentTest(Node lit, bool chEnt = true);
+ bool completeMatch(std::vector<size_t>& assigned, bool doContinue = false);
+ void revertMatch(const std::vector<size_t>& assigned);
+ void debugPrintMatch(const char* c) const;
+ bool isConstrainedVar(size_t v);
void getMatch( std::vector< Node >& terms );
+
+ // current constraints
+ std::vector<TNode> d_match;
+ std::vector<TNode> d_match_term;
+ std::map<size_t, std::map<TNode, size_t> > d_curr_var_deq;
+ std::map<Node, bool> d_tconstraints;
+
+ private:
+ void registerNode(Node n, bool hasPol, bool pol, bool beneathQuant = false);
+ void flatten(Node n, bool beneathQuant);
+ void getPropagateVars(std::vector<TNode>& vars,
+ TNode n,
+ bool pol,
+ std::map<TNode, bool>& visited);
+ /** The parent who owns this class */
+ QuantConflictFind* d_parent;
+ std::unique_ptr<MatchGen> d_mg;
+ Node d_q;
+ VarMgMap d_var_mg;
+ // for completing match
+ std::vector<size_t> d_unassigned;
+ std::vector<TypeNode> d_unassigned_tn;
+ size_t d_unassigned_nvar;
+ size_t d_una_index;
+ std::vector<int> d_una_eqc_count;
+ // optimization: track which arguments variables appear under UF terms in
+ std::map<size_t, std::map<TNode, std::vector<size_t> > > d_var_rel_dom;
+ // optimization: number of variables set, to track when we can stop
+ std::unordered_set<size_t> d_vars_set;
+ std::vector<Node> d_extra_var;
};
class QuantConflictFind : public QuantifiersModule
{
friend class MatchGen;
friend class QuantInfo;
- typedef context::CDHashMap<Node, bool> NodeBoolMap;
-
- private:
- context::CDO< bool > d_conflict;
- std::map<std::pair<TypeNode, Kind>, 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,
/** register quantifier */
void registerQuantifier(Node q) override;
-
- public:
/** needs check */
bool needsCheck(Theory::Effort level) override;
/** reset round */
*/
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:
* 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<Node> d_quants;
+ std::map<Node, size_t> d_quant_id;
+ /** Map from quantified formulas to their info class to compute instances */
+ std::map<Node, std::unique_ptr<QuantInfo> > d_qinfo;
+ /** Map from type -> list(eqc) of that type */
+ std::map<TypeNode, std::vector<TNode> > d_eqcs;
+ /** Are we in conflict? */
+ context::CDO<bool> d_conflict;
+ /** Zeros for (type, kind) pairs */
+ std::map<std::pair<TypeNode, Kind>, 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;
+ /** The current effort */
+ Effort d_effort;
};
std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
projects / cvc5.git / commitdiff