if( d_nodes.size()==1 ){
if( isSimpleTrigger( d_nodes[0] ) ){
d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
+ ++(qe->d_statistics.d_triggers);
}else{
d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe);
+ ++(qe->d_statistics.d_simple_triggers);
}
}else{
if( options::multiTriggerCache() ){
}else{
d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe);
}
- }
- if( d_nodes.size()==1 ){
- if( isSimpleTrigger( d_nodes[0] ) ){
- ++(qe->d_statistics.d_triggers);
- }else{
- ++(qe->d_statistics.d_simple_triggers);
- }
- }else{
- Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
- for( unsigned i=0; i<d_nodes.size(); i++ ){
- Trace("multi-trigger") << " " << d_nodes[i] << std::endl;
+ if (Trace.isOn("multi-trigger"))
+ {
+ Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
+ for (const Node& nc : d_nodes)
+ {
+ Trace("multi-trigger") << " " << nc << std::endl;
+ }
}
++(qe->d_statistics.d_multi_triggers);
}
d_mg->reset( eqc, d_quantEngine );
}
-Node Trigger::getInstPattern(){
+bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; }
+
+Node Trigger::getInstPattern() const
+{
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
}
-int Trigger::addInstantiations()
+uint64_t Trigger::addInstantiations()
{
- int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
- if( addedLemmas>0 ){
- if (Debug.isOn("inst-trigger"))
+ uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
+ if (Debug.isOn("inst-trigger"))
+ {
+ if (addedLemmas > 0)
{
Debug("inst-trigger") << "Added " << addedLemmas
- << " lemmas, trigger was ";
- for (unsigned i = 0; i < d_nodes.size(); i++)
- {
- Debug("inst-trigger") << d_nodes[i] << " ";
- }
- Debug("inst-trigger") << std::endl;
+ << " lemmas, trigger was " << d_nodes << std::endl;
}
}
return addedLemmas;
return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
}
-bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
+bool Trigger::mkTriggerTerms(Node q,
+ std::vector<Node>& nodes,
+ size_t nvars,
+ std::vector<Node>& trNodes)
+{
//only take nodes that contribute variables to the trigger when added
std::vector< Node > temp;
temp.insert( temp.begin(), nodes.begin(), nodes.end() );
quantifiers::TermUtil::computeInstConstContainsForQuant(
q, pat, varContains[pat]);
}
- for( unsigned i=0; i<temp.size(); i++ ){
+ for (const Node& t : temp)
+ {
+ const std::vector<Node>& vct = varContains[t];
bool foundVar = false;
- for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
- Node v = varContains[ temp[i] ][j];
+ for (const Node& v : vct)
+ {
Assert(quantifiers::TermUtil::getInstConstAttr(v) == q);
if( vars.find( v )==vars.end() ){
varCount++;
}
}
if( foundVar ){
- trNodes.push_back( temp[i] );
- for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
- Node v = varContains[ temp[i] ][j];
- patterns[ v ].push_back( temp[i] );
+ trNodes.push_back(t);
+ for (const Node& v : vct)
+ {
+ patterns[v].push_back(t);
}
}
- if( varCount==n_vars ){
+ if (varCount == nvars)
+ {
break;
}
}
- if( varCount<n_vars ){
+ if (varCount < nvars)
+ {
Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
- for( unsigned i=0; i<nodes.size(); i++) {
- Trace("trigger-debug") << nodes[i] << " ";
- }
- Trace("trigger-debug") << std::endl;
-
+ Trace("trigger-debug") << nodes << std::endl;
//do not generate multi-trigger if it does not contain all variables
return false;
- }else{
- //now, minimize the trigger
- for( unsigned i=0; i<trNodes.size(); i++ ){
- bool keepPattern = false;
- Node n = trNodes[i];
- for( unsigned j=0; j<varContains[ n ].size(); j++ ){
- Node v = varContains[ n ][j];
- if( patterns[v].size()==1 ){
- keepPattern = true;
- break;
- }
+ }
+ // now, minimize the trigger
+ for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
+ {
+ bool keepPattern = false;
+ Node n = trNodes[i];
+ const std::vector<Node>& vcn = varContains[n];
+ for (const Node& v : vcn)
+ {
+ if (patterns[v].size() == 1)
+ {
+ keepPattern = true;
+ break;
}
- if( !keepPattern ){
- //remove from pattern vector
- for( unsigned j=0; j<varContains[ n ].size(); j++ ){
- Node v = varContains[ n ][j];
- for( unsigned k=0; k<patterns[v].size(); k++ ){
- if( patterns[v][k]==n ){
- patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
- break;
- }
+ }
+ if (!keepPattern)
+ {
+ // remove from pattern vector
+ for (const Node& v : vcn)
+ {
+ std::vector<Node>& pv = patterns[v];
+ for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
+ {
+ if (pv[k] == n)
+ {
+ pv.erase(pv.begin() + k, pv.begin() + k + 1);
+ break;
}
}
- //remove from trigger nodes
- trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
- i--;
}
+ // remove from trigger nodes
+ trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
+ i--;
}
}
return true;
}
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
+Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& nodes,
+ bool keepAll,
+ int trOption,
+ size_t useNVars)
+{
std::vector< Node > trNodes;
if( !keepAll ){
- unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
- if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
- return NULL;
+ size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars;
+ if (!mkTriggerTerms(f, nodes, nvars, trNodes))
+ {
+ return nullptr;
}
}else{
trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
//just return old trigger
return t;
}else{
- return NULL;
+ return nullptr;
}
}
}
return t;
}
-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
+Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+ Node f,
+ Node n,
+ bool keepAll,
+ int trOption,
+ size_t useNVars)
+{
std::vector< Node > nodes;
nodes.push_back( n );
- return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
+ return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars);
}
bool Trigger::isUsable( Node n, Node q ){
- if( quantifiers::TermUtil::getInstConstAttr(n)==q ){
- if( isAtomicTrigger( n ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !isUsable( n[i], q ) ){
- return false;
- }
- }
- return true;
- }else if( n.getKind()==INST_CONSTANT ){
- return true;
- }else{
- std::map< Node, Node > coeffs;
- if (options::purifyTriggers())
+ if (quantifiers::TermUtil::getInstConstAttr(n) != q)
+ {
+ return true;
+ }
+ if (isAtomicTrigger(n))
+ {
+ for (const Node& nc : n)
+ {
+ if (!isUsable(nc, q))
{
- Node x = getInversionVariable( n );
- if( !x.isNull() ){
- return true;
- }
+ return false;
}
}
- return false;
- }else{
return true;
}
+ else if (n.getKind() == INST_CONSTANT)
+ {
+ return true;
+ }
+ std::map<Node, Node> coeffs;
+ if (options::purifyTriggers())
+ {
+ Node x = getInversionVariable(n);
+ if (!x.isNull())
+ {
+ return true;
+ }
+ }
+ return false;
}
Node Trigger::getIsUsableEq( Node q, Node n ) {
Assert(isRelationalTrigger(n));
- for( unsigned i=0; i<2; i++) {
+ for (size_t i = 0; i < 2; i++)
+ {
if( isUsableEqTerms( q, n[i], n[1-i] ) ){
if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
pol = !pol;
n = n[0];
}
+ NodeManager* nm = NodeManager::currentNM();
if( n.getKind()==INST_CONSTANT ){
- return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
}else if( isRelationalTrigger( n ) ){
Node rtr = getIsUsableEq( q, n );
if( rtr.isNull() && n[0].getType().isReal() ){
Trace("relational-trigger") << " return : " << rtr2 << std::endl;
return rtr2;
}
- }else{
- Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
- if( isUsableAtomicTrigger( n, q ) ){
- return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
- }
+ return Node::null();
+ }
+ Trace("trigger-debug") << n << " usable : "
+ << (quantifiers::TermUtil::getInstConstAttr(n) == q)
+ << " " << isAtomicTrigger(n) << " " << isUsable(n, q)
+ << std::endl;
+ if (isUsableAtomicTrigger(n, q))
+ {
+ return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
}
return Node::null();
}
t = t[0];
}
}
- if( isAtomicTrigger( t ) ){
- for( unsigned i=0; i<t.getNumChildren(); i++ ){
- if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermUtil::hasInstConstAttr(t[i]) ){
- return false;
- }
- }
- if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+ if (!isAtomicTrigger(t))
+ {
+ return false;
+ }
+ for (const Node& tc : t)
+ {
+ if (tc.getKind() != INST_CONSTANT
+ && quantifiers::TermUtil::hasInstConstAttr(tc))
{
return false;
}
- return true;
}
- return false;
+ if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+ {
+ return false;
+ }
+ return true;
}
//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
bool knowIsUsable)
{
std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
- if( itv==visited.end() ){
- visited[ n ].clear();
- Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
- if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
- Node nu;
- bool nu_single = false;
- if( knowIsUsable ){
- nu = n;
- }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
- nu = getIsUsableTrigger( n, q );
- if( !nu.isNull() && nu!=n ){
- collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
- // copy to n
- visited[n].insert( visited[n].end(), added.begin(), added.end() );
- return;
- }
+ if (itv != visited.end())
+ {
+ // already visited
+ for (const Node& t : itv->second)
+ {
+ if (std::find(added.begin(), added.end(), t) == added.end())
+ {
+ added.push_back(t);
}
- if( !nu.isNull() ){
- Assert(nu == n);
- Assert(nu.getKind() != NOT);
- Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
- Node reqEq;
- if( nu.getKind()==EQUAL ){
- if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){
- if( hasPol ){
- reqEq = nu[1];
- }
- nu = nu[0];
- }
+ }
+ return;
+ }
+ visited[n].clear();
+ Trace("auto-gen-trigger-debug2")
+ << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
+ << " " << hasEPol << std::endl;
+ Kind nk = n.getKind();
+ if (nk == FORALL || nk == INST_CONSTANT)
+ {
+ // do not traverse beneath quantified formulas
+ return;
+ }
+ Node nu;
+ bool nu_single = false;
+ if (knowIsUsable)
+ {
+ nu = n;
+ }
+ else if (nk != NOT
+ && std::find(exclude.begin(), exclude.end(), n) == exclude.end())
+ {
+ nu = getIsUsableTrigger(n, q);
+ if (!nu.isNull() && nu != n)
+ {
+ collectPatTerms2(q,
+ nu,
+ visited,
+ tinfo,
+ tstrt,
+ exclude,
+ added,
+ pol,
+ hasPol,
+ epol,
+ hasEPol,
+ true);
+ // copy to n
+ visited[n].insert(visited[n].end(), added.begin(), added.end());
+ return;
+ }
+ }
+ if (!nu.isNull())
+ {
+ Assert(nu == n);
+ Assert(nu.getKind() != NOT);
+ Trace("auto-gen-trigger-debug2")
+ << "...found usable trigger : " << nu << std::endl;
+ Node reqEq;
+ if (nu.getKind() == EQUAL)
+ {
+ if (isAtomicTrigger(nu[0])
+ && !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
+ {
+ if (hasPol)
+ {
+ reqEq = nu[1];
}
- Assert(reqEq.isNull()
- || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
- Assert(isUsableTrigger(nu, q));
- //tinfo.find( nu )==tinfo.end()
- Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
- tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
- nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
+ nu = nu[0];
}
- Node nrec = nu.isNull() ? n : nu;
- std::vector< Node > added2;
- for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
- bool newHasPol, newPol;
- bool newHasEPol, newEPol;
- QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
- QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
- collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
- }
- // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
- if( !nu.isNull() ){
- bool rm_nu = false;
- for( unsigned i=0; i<added2.size(); i++ ){
- Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
- Assert(added2[i] != nu);
- // if child was not already removed
- if( tinfo.find( added2[i] )!=tinfo.end() ){
- if (tstrt == options::TriggerSelMode::MAX
- || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX
- && !nu_single))
- {
- // discard all subterms
- // do not remove if it has smaller weight
- if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
- {
- Trace("auto-gen-trigger-debug2")
- << "......remove it." << std::endl;
- visited[added2[i]].clear();
- tinfo.erase(added2[i]);
- }
- }
- else
- {
- if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
- if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
- {
- // discard if we added a subterm as a trigger with all
- // variables that nu has
- Trace("auto-gen-trigger-debug2")
- << "......subsumes parent " << tinfo[nu].d_weight << " "
- << tinfo[added2[i]].d_weight << "." << std::endl;
- rm_nu = true;
- }
- }
- if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
- added.push_back( added2[i] );
- }
- }
- }
- }
- if (rm_nu
- && (tstrt == options::TriggerSelMode::MIN
- || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL
- && nu_single)))
+ }
+ Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
+ Assert(isUsableTrigger(nu, q));
+ // tinfo.find( nu )==tinfo.end()
+ Trace("auto-gen-trigger-debug2")
+ << "...add usable trigger : " << nu << std::endl;
+ tinfo[nu].init(q, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
+ nu_single = tinfo[nu].d_fv.size() == q[0].getNumChildren();
+ }
+ Node nrec = nu.isNull() ? n : nu;
+ std::vector<Node> added2;
+ for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
+ {
+ bool newHasPol, newPol;
+ bool newHasEPol, newEPol;
+ QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
+ QuantPhaseReq::getEntailPolarity(
+ nrec, i, hasEPol, epol, newHasEPol, newEPol);
+ collectPatTerms2(q,
+ nrec[i],
+ visited,
+ tinfo,
+ tstrt,
+ exclude,
+ added2,
+ newPol,
+ newHasPol,
+ newEPol,
+ newHasEPol);
+ }
+ // if this is not a usable trigger, don't worry about caching the results,
+ // since triggers do not contain non-usable subterms
+ if (nu.isNull())
+ {
+ return;
+ }
+ bool rm_nu = false;
+ for (size_t i = 0, asize = added2.size(); i < asize; i++)
+ {
+ Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
+ << " : " << added2[i] << std::endl;
+ Assert(added2[i] != nu);
+ // if child was not already removed
+ if (tinfo.find(added2[i]) != tinfo.end())
+ {
+ if (tstrt == options::TriggerSelMode::MAX
+ || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
+ {
+ // discard all subterms
+ // do not remove if it has smaller weight
+ if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
{
- tinfo.erase( nu );
+ Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
+ visited[added2[i]].clear();
+ tinfo.erase(added2[i]);
}
- else
+ }
+ else
+ {
+ if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
{
- if( std::find( added.begin(), added.end(), nu )==added.end() ){
- added.push_back( nu );
+ if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
+ {
+ // discard if we added a subterm as a trigger with all
+ // variables that nu has
+ Trace("auto-gen-trigger-debug2")
+ << "......subsumes parent " << tinfo[nu].d_weight << " "
+ << tinfo[added2[i]].d_weight << "." << std::endl;
+ rm_nu = true;
}
}
- visited[n].insert( visited[n].end(), added.begin(), added.end() );
- }
- }
- }else{
- for( unsigned i=0; i<itv->second.size(); ++i ){
- Node t = itv->second[i];
- if( std::find( added.begin(), added.end(), t )==added.end() ){
- added.push_back( t );
+ if (std::find(added.begin(), added.end(), added2[i]) == added.end())
+ {
+ added.push_back(added2[i]);
+ }
}
}
}
-}
-
-bool Trigger::isPureTheoryTrigger( Node n ) {
- if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
- return false;
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !isPureTheoryTrigger( n[i] ) ){
- return false;
- }
+ if (rm_nu
+ && (tstrt == options::TriggerSelMode::MIN
+ || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
+ {
+ tinfo.erase(nu);
+ }
+ else
+ {
+ if (std::find(added.begin(), added.end(), nu) == added.end())
+ {
+ added.push_back(nu);
}
- return true;
}
+ visited[n].insert(visited[n].end(), added.begin(), added.end());
}
int Trigger::getTriggerWeight( Node n ) {
return 2;
}
-bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
- if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
- if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
- bool hasVar = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()==INST_CONSTANT ){
- hasVar = true;
- if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
- vars.push_back( n[i] );
- }else{
- //do not allow duplicate variables
- return false;
- }
- }else{
- //do not allow nested function applications
- return false;
- }
- }
- if( hasVar ){
- patTerms.push_back( n );
- }
- }
- }else{
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
- return false;
- }
- }
- }
- return true;
-}
-
void Trigger::collectPatTerms(Node q,
Node n,
std::vector<Node>& patTerms,
}
std::vector< Node > added;
collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
- for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
- patTerms.push_back( it->first );
+ for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
+ {
+ patTerms.push_back(t.first);
}
}
int Trigger::isTriggerInstanceOf(Node n1,
Node n2,
- std::vector<Node>& fv1,
- std::vector<Node>& fv2)
+ const std::vector<Node>& fv1,
+ const std::vector<Node>& fv2)
{
Assert(n1 != n2);
int status = 0;
{
cur = visit.back();
visit.pop_back();
- if (visited.find(cur) == visited.end())
+ if (visited.find(cur) != visited.end())
{
- visited.insert(cur);
- cur1 = cur.first;
- cur2 = cur.second;
- Assert(cur1 != cur2);
- // recurse if they have the same operator
- if (cur1.hasOperator() && cur2.hasOperator()
- && cur1.getNumChildren() == cur2.getNumChildren()
- && cur1.getOperator() == cur2.getOperator()
- && cur1.getOperator().getKind()!=INST_CONSTANT)
+ continue;
+ }
+ visited.insert(cur);
+ cur1 = cur.first;
+ cur2 = cur.second;
+ Assert(cur1 != cur2);
+ // recurse if they have the same operator
+ if (cur1.hasOperator() && cur2.hasOperator()
+ && cur1.getNumChildren() == cur2.getNumChildren()
+ && cur1.getOperator() == cur2.getOperator()
+ && cur1.getOperator().getKind() != INST_CONSTANT)
+ {
+ visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
+ for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
{
- visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
- for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++)
+ if (cur1[i] != cur2[i])
{
- if (cur1[i] != cur2[i])
- {
- visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
- }
- else if (cur1[i].getKind() == INST_CONSTANT)
+ visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
+ }
+ else if (cur1[i].getKind() == INST_CONSTANT)
+ {
+ if (subs_vars.find(cur1[i]) != subs_vars.end())
{
- if (subs_vars.find(cur1[i]) != subs_vars.end())
- {
- return 0;
- }
- // the variable must map to itself in the substitution
- subs_vars.insert(cur1[i]);
+ return 0;
}
+ // the variable must map to itself in the substitution
+ subs_vars.insert(cur1[i]);
}
}
- else
+ continue;
+ }
+ bool success = false;
+ // check if we are in a unifiable instance case
+ // must be only this case
+ for (unsigned r = 0; r < 2; r++)
+ {
+ if (status == 0 || ((status == 1) == (r == 0)))
{
- bool success = false;
- // check if we are in a unifiable instance case
- // must be only this case
- for (unsigned r = 0; r < 2; r++)
+ TNode curi = r == 0 ? cur1 : cur2;
+ if (curi.getKind() == INST_CONSTANT
+ && subs_vars.find(curi) == subs_vars.end())
{
- if (status == 0 || ((status == 1) == (r == 0)))
+ TNode curj = r == 0 ? cur2 : cur1;
+ // RHS must be a simple trigger
+ if (getTriggerWeight(curj) == 0)
{
- TNode curi = r == 0 ? cur1 : cur2;
- if (curi.getKind() == INST_CONSTANT
- && subs_vars.find(curi) == subs_vars.end())
+ // must occur in the free variables in the other
+ const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
+ if (std::find(free_vars.begin(), free_vars.end(), curi)
+ != free_vars.end())
{
- TNode curj = r == 0 ? cur2 : cur1;
- // RHS must be a simple trigger
- if (getTriggerWeight(curj) == 0)
- {
- // must occur in the free variables in the other
- std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
- if (std::find(free_vars.begin(), free_vars.end(), curi)
- != free_vars.end())
- {
- status = r == 0 ? 1 : -1;
- subs_vars.insert(curi);
- success = true;
- break;
- }
- }
+ status = r == 0 ? 1 : -1;
+ subs_vars.insert(curi);
+ success = true;
+ break;
}
}
}
- if (!success)
- {
- return 0;
- }
}
}
+ if (!success)
+ {
+ return 0;
+ }
} while (!visit.empty());
return status;
}
void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
{
std::map<unsigned, std::vector<Node> > fvs;
- for (unsigned i = 0, size = nodes.size(); i < size; i++)
+ for (size_t i = 0, size = nodes.size(); i < size; i++)
{
quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
}
std::vector<bool> active;
active.resize(nodes.size(), true);
- for (unsigned i = 0, size = nodes.size(); i < size; i++)
+ for (size_t i = 0, size = nodes.size(); i < size; i++)
{
std::vector<Node>& fvsi = fvs[i];
- if (active[i])
+ if (!active[i])
{
- for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++)
+ continue;
+ }
+ for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
+ {
+ if (!active[j])
{
- if (active[j])
- {
- int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
- if (result == 1)
- {
- Trace("filter-instances") << nodes[j] << " is an instance of "
- << nodes[i] << std::endl;
- active[i] = false;
- break;
- }
- else if (result == -1)
- {
- Trace("filter-instances") << nodes[i] << " is an instance of "
- << nodes[j] << std::endl;
- active[j] = false;
- }
- }
+ continue;
+ }
+ int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
+ if (result == 1)
+ {
+ Trace("filter-instances")
+ << nodes[j] << " is an instance of " << nodes[i] << std::endl;
+ active[i] = false;
+ break;
+ }
+ else if (result == -1)
+ {
+ Trace("filter-instances")
+ << nodes[i] << " is an instance of " << nodes[j] << std::endl;
+ active[j] = false;
}
}
}
std::vector<Node> temp;
- for (unsigned i = 0; i < nodes.size(); i++)
+ for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
{
if (active[i])
{
}
Node Trigger::getInversionVariable( Node n ) {
- if( n.getKind()==INST_CONSTANT ){
+ Kind nk = n.getKind();
+ if (nk == INST_CONSTANT)
+ {
return n;
- }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+ }
+ else if (nk == PLUS || nk == MULT)
+ {
Node ret;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
+ for (const Node& nc : n)
+ {
+ if (quantifiers::TermUtil::hasInstConstAttr(nc))
+ {
if( ret.isNull() ){
- ret = getInversionVariable( n[i] );
+ ret = getInversionVariable(nc);
if( ret.isNull() ){
Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
return Node::null();
}else{
return Node::null();
}
- }else if( n.getKind()==MULT ){
- if( !n[i].isConst() ){
+ }
+ else if (nk == MULT)
+ {
+ if (!nc.isConst())
+ {
Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
return Node::null();
}
- /*
- else if( n.getType().isInteger() ){
- Rational r = n[i].getConst<Rational>();
- if( r!=Rational(-1) && r!=Rational(1) ){
- Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
- return Node::null();
- }
- }
- */
}
}
return ret;
- }else{
- Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl;
}
+ Trace("var-trigger-debug")
+ << "No : unsupported operator " << n << "." << std::endl;
return Node::null();
}
Node Trigger::getInversion( Node n, Node x ) {
- if( n.getKind()==INST_CONSTANT ){
+ Kind nk = n.getKind();
+ if (nk == INST_CONSTANT)
+ {
return x;
- }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+ }
+ else if (nk == PLUS || nk == MULT)
+ {
+ NodeManager* nm = NodeManager::currentNM();
int cindex = -1;
bool cindexSet = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
- if( n.getKind()==PLUS ){
- x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
- }else if( n.getKind()==MULT ){
- Assert(n[i].isConst());
+ for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+ {
+ Node nc = n[i];
+ if (!quantifiers::TermUtil::hasInstConstAttr(nc))
+ {
+ if (nk == PLUS)
+ {
+ x = nm->mkNode(MINUS, x, nc);
+ }
+ else if (nk == MULT)
+ {
+ Assert(nc.isConst());
if( x.getType().isInteger() ){
- Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
- if( !n[i].getConst<Rational>().abs().isOne() ){
- x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
+ Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
+ if (!nc.getConst<Rational>().abs().isOne())
+ {
+ x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
}
- if( n[i].getConst<Rational>().sgn()<0 ){
- x = NodeManager::currentNM()->mkNode( UMINUS, x );
+ if (nc.getConst<Rational>().sgn() < 0)
+ {
+ x = nm->mkNode(UMINUS, x);
}
}else{
- Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
- x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+ Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
+ x = nm->mkNode(MULT, x, coeff);
}
}
x = Rewriter::rewrite( x );
return d_mg->getActiveScore( d_quantEngine );
}
+void Trigger::debugPrint(const char* c) const
+{
+ Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl;
+}
+
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff