#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
namespace CVC4 {
namespace theory {
}
InstMatchGenerator::InstMatchGenerator( Node pat ){
- d_cg = NULL;
+ d_cg = nullptr;
d_needsReset = true;
d_active_add = true;
Assert(quantifiers::TermUtil::hasInstConstAttr(pat));
d_pattern = pat;
d_match_pattern = pat;
d_match_pattern_type = pat.getType();
- d_next = NULL;
+ d_next = nullptr;
d_independent_gen = false;
}
InstMatchGenerator::InstMatchGenerator() {
- d_cg = NULL;
+ d_cg = nullptr;
d_needsReset = true;
d_active_add = true;
- d_next = NULL;
+ d_next = nullptr;
d_independent_gen = false;
}
void InstMatchGenerator::setActiveAdd(bool val){
d_active_add = val;
- if( d_next!=NULL ){
+ if (d_next != nullptr)
+ {
d_next->setActiveAdd(val);
}
}
unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
return ngtt;
-// }else if( d_match_pattern_getKind()==EQUAL ){
-
- }else{
- return -1;
}
+ return -1;
}
-void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
- if( !d_pattern.isNull() ){
- Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
- if( d_match_pattern.getKind()==NOT ){
- Assert(d_pattern.getKind() == NOT);
- //we want to add the children of the NOT
- d_match_pattern = d_match_pattern[0];
- }
+void InstMatchGenerator::initialize(Node q,
+ QuantifiersEngine* qe,
+ std::vector<InstMatchGenerator*>& gens)
+{
+ if (d_pattern.isNull())
+ {
+ gens.insert(gens.end(), d_children.begin(), d_children.end());
+ return;
+ }
+ Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern
+ << std::endl;
+ if (d_match_pattern.getKind() == NOT)
+ {
+ Assert(d_pattern.getKind() == NOT);
+ // we want to add the children of the NOT
+ d_match_pattern = d_match_pattern[0];
+ }
- if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
- && d_match_pattern[0].getKind() == INST_CONSTANT
- && d_match_pattern[1].getKind() == INST_CONSTANT)
- {
- // special case: disequalities between variables x != y will match ground
- // disequalities.
- }
- else if (d_match_pattern.getKind() == EQUAL
- || d_match_pattern.getKind() == GEQ)
+ if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
+ && d_match_pattern[0].getKind() == INST_CONSTANT
+ && d_match_pattern[1].getKind() == INST_CONSTANT)
+ {
+ // special case: disequalities between variables x != y will match ground
+ // disequalities.
+ }
+ else if (d_match_pattern.getKind() == EQUAL
+ || d_match_pattern.getKind() == GEQ)
+ {
+ // We are one of the following cases:
+ // f(x)~a, f(x)~y, x~a, x~y
+ // If we are the first or third case, we ensure that f(x)/x is on the left
+ // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
+ // d_eq_class_rel (indicating the equivalence class that we are related
+ // to) is set to a.
+ for (size_t i = 0; i < 2; i++)
{
- // We are one of the following cases:
- // f(x)~a, f(x)~y, x~a, x~y
- // If we are the first or third case, we ensure that f(x)/x is on the left
- // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
- // d_eq_class_rel (indicating the equivalence class that we are related
- // to) is set to a.
- for( unsigned i=0; i<2; i++ ){
- Node mp = d_match_pattern[i];
- Node mpo = d_match_pattern[1 - i];
- // If this side has free variables, and the other side does not or
- // it is a free variable, then we will match on this side of the
- // relation.
- if (quantifiers::TermUtil::hasInstConstAttr(mp)
- && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
- || mpo.getKind() == INST_CONSTANT))
+ Node mp = d_match_pattern[i];
+ Node mpo = d_match_pattern[1 - i];
+ // If this side has free variables, and the other side does not or
+ // it is a free variable, then we will match on this side of the
+ // relation.
+ if (quantifiers::TermUtil::hasInstConstAttr(mp)
+ && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
+ || mpo.getKind() == INST_CONSTANT))
+ {
+ if (i == 1)
{
- if (i == 1)
+ if (d_match_pattern.getKind() == GEQ)
{
- if (d_match_pattern.getKind() == GEQ)
- {
- d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
- d_pattern = d_pattern.negate();
- }
- else
- {
- d_pattern = NodeManager::currentNM()->mkNode(
- d_match_pattern.getKind(), mp, mpo);
- }
+ d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
+ d_pattern = d_pattern.negate();
+ }
+ else
+ {
+ d_pattern = NodeManager::currentNM()->mkNode(
+ d_match_pattern.getKind(), mp, mpo);
}
- d_eq_class_rel = mpo;
- d_match_pattern = mp;
- // we won't find a term in the other direction
- break;
}
+ d_eq_class_rel = mpo;
+ d_match_pattern = mp;
+ // we won't find a term in the other direction
+ break;
}
}
- d_match_pattern_type = d_match_pattern.getType();
- Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
- d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+ }
+ d_match_pattern_type = d_match_pattern.getType();
+ Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
+ << d_match_pattern << std::endl;
+ d_match_pattern_op = qe->getTermDatabase()->getMatchOperator(d_match_pattern);
- //now, collect children of d_match_pattern
- Kind mpk = d_match_pattern.getKind();
- if (mpk == INST_CONSTANT)
- {
- d_children_types.push_back(
- d_match_pattern.getAttribute(InstVarNumAttribute()));
- }
- else
+ // now, collect children of d_match_pattern
+ Kind mpk = d_match_pattern.getKind();
+ if (mpk == INST_CONSTANT)
+ {
+ d_children_types.push_back(
+ d_match_pattern.getAttribute(InstVarNumAttribute()));
+ }
+ else
+ {
+ for (size_t i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
{
- for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size;
- i++)
+ Node pat = d_match_pattern[i];
+ Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
+ if (!qa.isNull())
{
- Node pat = d_match_pattern[i];
- Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
- if (!qa.isNull())
+ if (pat.getKind() == INST_CONSTANT && qa == q)
+ {
+ d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
+ }
+ else
{
- if (pat.getKind() == INST_CONSTANT && qa == q)
+ InstMatchGenerator* cimg = getInstMatchGenerator(q, pat);
+ if (cimg)
{
- d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
+ d_children.push_back(cimg);
+ d_children_index.push_back(i);
+ d_children_types.push_back(-2);
}
else
{
- InstMatchGenerator* cimg = getInstMatchGenerator(q, pat);
- if (cimg)
- {
- d_children.push_back(cimg);
- d_children_index.push_back(i);
- d_children_types.push_back(-2);
- }
- else
- {
- d_children_types.push_back(-1);
- }
+ d_children_types.push_back(-1);
}
}
- else
- {
- d_children_types.push_back(-1);
- }
+ }
+ else
+ {
+ d_children_types.push_back(-1);
}
}
+ }
- //create candidate generator
- if (mpk == APPLY_SELECTOR)
- {
- // candidates for apply selector are a union of correctly and incorrectly
- // applied selectors
- d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
- }
- else if (Trigger::isAtomicTriggerKind(mpk))
+ // create candidate generator
+ if (mpk == APPLY_SELECTOR)
+ {
+ // candidates for apply selector are a union of correctly and incorrectly
+ // applied selectors
+ d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
+ }
+ else if (Trigger::isAtomicTriggerKind(mpk))
+ {
+ if (mpk == APPLY_CONSTRUCTOR)
{
- if (mpk == APPLY_CONSTRUCTOR)
- {
- // 1-constructors have a trivial way of generating candidates in a
- // given equivalence class
- const DType& dt = d_match_pattern.getType().getDType();
- if (dt.getNumConstructors() == 1)
- {
- d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
- }
- }
- if (d_cg == nullptr)
+ // 1-constructors have a trivial way of generating candidates in a
+ // given equivalence class
+ const DType& dt = d_match_pattern.getType().getDType();
+ if (dt.getNumConstructors() == 1)
{
- CandidateGeneratorQE* cg =
- new CandidateGeneratorQE(qe, d_match_pattern);
- // we will be scanning lists trying to find ground terms whose operator
- // is the same as d_match_operator's.
- d_cg = cg;
- // if matching on disequality, inform the candidate generator not to
- // match on eqc
- if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
- {
- cg->excludeEqc(d_eq_class_rel);
- d_eq_class_rel = Node::null();
- }
+ d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
}
}
- else if (mpk == INST_CONSTANT)
+ if (d_cg == nullptr)
{
- if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
- Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
- size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
- const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
- const DTypeConstructor& c = dt[selectorIndex];
- Node cOp = c.getConstructor();
- Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
- d_cg = new inst::CandidateGeneratorQE( qe, cOp );
- }else{
- d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
+ CandidateGeneratorQE* cg = new CandidateGeneratorQE(qe, d_match_pattern);
+ // we will be scanning lists trying to find ground terms whose operator
+ // is the same as d_match_operator's.
+ d_cg = cg;
+ // if matching on disequality, inform the candidate generator not to
+ // match on eqc
+ if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
+ {
+ cg->excludeEqc(d_eq_class_rel);
+ d_eq_class_rel = Node::null();
}
}
- else if (mpk == EQUAL)
+ }
+ else if (mpk == INST_CONSTANT)
+ {
+ if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
{
- //we will be producing candidates via literal matching heuristics
- if (d_pattern.getKind() == NOT)
- {
- // candidates will be all disequalities
- d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
- }
+ Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+ size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
+ const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
+ const DTypeConstructor& c = dt[selectorIndex];
+ Node cOp = c.getConstructor();
+ Trace("inst-match-gen")
+ << "Purify dt trigger " << d_pattern << ", will match terms of op "
+ << cOp << std::endl;
+ d_cg = new inst::CandidateGeneratorQE(qe, cOp);
}else{
- Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+ d_cg = new CandidateGeneratorQEAll(qe, d_match_pattern);
}
}
+ else if (mpk == EQUAL)
+ {
+ // we will be producing candidates via literal matching heuristics
+ if (d_pattern.getKind() == NOT)
+ {
+ // candidates will be all disequalities
+ d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
+ }
+ }
+ else
+ {
+ Trace("inst-match-gen-warn")
+ << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+ }
gens.insert( gens.end(), d_children.begin(), d_children.end() );
}
{
Trace("matching-fail") << "Internal error for match generator." << std::endl;
return -2;
- }else{
- EqualityQuery* q = qe->getEqualityQuery();
- bool success = true;
- //save previous match
- //InstMatch prev( &m );
- std::vector< int > prev;
- //if t is null
- Assert(!t.isNull());
- Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
- // notice that t may have a different kind or operator from our match
- // pattern, e.g. for APPLY_SELECTOR triggers.
- //first, check if ground arguments are not equal, or a match is in conflict
- Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
- for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
+ }
+ EqualityQuery* q = qe->getEqualityQuery();
+ bool success = true;
+ std::vector<int> prev;
+ // if t is null
+ Assert(!t.isNull());
+ Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
+ // notice that t may have a different kind or operator from our match
+ // pattern, e.g. for APPLY_SELECTOR triggers.
+ // first, check if ground arguments are not equal, or a match is in conflict
+ Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
+ for (size_t i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
+ {
+ int64_t ct = d_children_types[i];
+ if (ct >= 0)
{
- int ct = d_children_types[i];
- if (ct >= 0)
+ Trace("matching-debug2")
+ << "Setting " << ct << " to " << t[i] << "..." << std::endl;
+ bool addToPrev = m.get(ct).isNull();
+ if (!m.set(q, ct, t[i]))
{
- Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..."
- << std::endl;
- bool addToPrev = m.get(ct).isNull();
- if (!m.set(q, ct, t[i]))
- {
- //match is in conflict
- Trace("matching-fail") << "Match fail: " << m.get(ct) << " and "
- << t[i] << std::endl;
- success = false;
- break;
- }else if( addToPrev ){
- Trace("matching-debug2") << "Success." << std::endl;
- prev.push_back(ct);
- }
+ // match is in conflict
+ Trace("matching-fail")
+ << "Match fail: " << m.get(ct) << " and " << t[i] << std::endl;
+ success = false;
+ break;
}
- else if (ct == -1)
+ else if (addToPrev)
{
- if( !q->areEqual( d_match_pattern[i], t[i] ) ){
- Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
- //ground arguments are not equal
- success = false;
- break;
- }
+ Trace("matching-debug2") << "Success." << std::endl;
+ prev.push_back(ct);
}
}
- Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl;
- //for variable matching
- if( d_match_pattern.getKind()==INST_CONSTANT ){
- bool addToPrev = m.get(d_children_types[0]).isNull();
- if (!m.set(q, d_children_types[0], t))
+ else if (ct == -1)
+ {
+ if (!q->areEqual(d_match_pattern[i], t[i]))
{
+ Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i]
+ << " and " << t[i] << std::endl;
+ // ground arguments are not equal
success = false;
- }else{
- if( addToPrev ){
- prev.push_back(d_children_types[0]);
- }
+ break;
}
}
- //for relational matching
- if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
+ }
+ Trace("matching-debug2") << "Done setting immediate matches, success = "
+ << success << "." << std::endl;
+ // for variable matching
+ if (d_match_pattern.getKind() == INST_CONSTANT)
+ {
+ bool addToPrev = m.get(d_children_types[0]).isNull();
+ if (!m.set(q, d_children_types[0], t))
{
- int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
- //also must fit match to equivalence class
- bool pol = d_pattern.getKind()!=NOT;
- Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
- Node t_match;
- if( pol ){
- if( pat.getKind()==GT ){
- t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermUtil()->d_one);
- }else{
- t_match = t;
- }
+ success = false;
+ }
+ else
+ {
+ if (addToPrev)
+ {
+ prev.push_back(d_children_types[0]);
+ }
+ }
+ }
+ // for relational matching
+ if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
+ // also must fit match to equivalence class
+ bool pol = d_pattern.getKind() != NOT;
+ Node pat = d_pattern.getKind() == NOT ? d_pattern[0] : d_pattern;
+ Node t_match;
+ if (pol)
+ {
+ if (pat.getKind() == GT)
+ {
+ t_match = nm->mkNode(MINUS, t, nm->mkConst(Rational(1)));
}else{
- if( pat.getKind()==EQUAL ){
- if( t.getType().isBoolean() ){
- t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) );
- }else{
- Assert(t.getType().isReal());
- t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
- }
- }else if( pat.getKind()==GEQ ){
- t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
- }else if( pat.getKind()==GT ){
- t_match = t;
- }
+ t_match = t;
}
- if( !t_match.isNull() ){
- bool addToPrev = m.get( v ).isNull();
- if (!m.set(q, v, t_match))
+ }
+ else
+ {
+ if (pat.getKind() == EQUAL)
+ {
+ if (t.getType().isBoolean())
+ {
+ t_match = nm->mkConst(!q->areEqual(nm->mkConst(true), t));
+ }
+ else
{
- success = false;
- }else if( addToPrev ){
- prev.push_back( v );
+ Assert(t.getType().isReal());
+ t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
}
}
+ else if (pat.getKind() == GEQ)
+ {
+ t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
+ }
+ else if (pat.getKind() == GT)
+ {
+ t_match = t;
+ }
}
- int ret_val = -1;
- if( success ){
- Trace("matching-debug2") << "Reset children..." << std::endl;
- //now, fit children into match
- //we will be requesting candidates for matching terms for each child
- for (unsigned i = 0, size = d_children.size(); i < size; i++)
+ if (!t_match.isNull())
+ {
+ bool addToPrev = m.get(v).isNull();
+ if (!m.set(q, v, t_match))
{
- if( !d_children[i]->reset( t[ d_children_index[i] ], qe ) ){
- success = false;
- break;
- }
+ success = false;
}
- if( success ){
- Trace("matching-debug2") << "Continue next " << d_next << std::endl;
- ret_val = continueNextMatch(f, m, qe, tparent);
+ else if (addToPrev)
+ {
+ prev.push_back(v);
}
}
- if( ret_val<0 ){
- for (int& pv : prev)
+ }
+ int ret_val = -1;
+ if (success)
+ {
+ Trace("matching-debug2") << "Reset children..." << std::endl;
+ // now, fit children into match
+ // we will be requesting candidates for matching terms for each child
+ for (size_t i = 0, size = d_children.size(); i < size; i++)
+ {
+ if (!d_children[i]->reset(t[d_children_index[i]], qe))
{
- m.d_vals[pv] = Node::null();
+ success = false;
+ break;
}
}
- return ret_val;
+ if (success)
+ {
+ Trace("matching-debug2") << "Continue next " << d_next << std::endl;
+ ret_val = continueNextMatch(f, m, qe, tparent);
+ }
+ }
+ if (ret_val < 0)
+ {
+ for (int& pv : prev)
+ {
+ m.d_vals[pv] = Node::null();
+ }
}
+ return ret_val;
}
-int InstMatchGenerator::continueNextMatch(Node f,
+int InstMatchGenerator::continueNextMatch(Node q,
InstMatch& m,
QuantifiersEngine* qe,
Trigger* tparent)
{
if( d_next!=NULL ){
- return d_next->getNextMatch(f, m, qe, tparent);
- }else{
- if( d_active_add ){
- return sendInstantiation(tparent, m) ? 1 : -1;
- }else{
- return 1;
- }
+ return d_next->getNextMatch(q, m, qe, tparent);
+ }
+ if (d_active_add)
+ {
+ return sendInstantiation(tparent, m) ? 1 : -1;
}
+ return 1;
}
/** reset instantiation round */
return success;
}
-int InstMatchGenerator::addInstantiations(Node f,
- QuantifiersEngine* qe,
- Trigger* tparent)
+uint64_t InstMatchGenerator::addInstantiations(Node f,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
{
//try to add instantiation for each match produced
- int addedLemmas = 0;
+ uint64_t addedLemmas = 0;
InstMatch m( f );
while (getNextMatch(f, m, qe, tparent) > 0)
{
Assert(gens.size() == pats.size());
std::vector< Node > patsn;
std::map< Node, InstMatchGenerator * > pat_map_init;
- for( unsigned i=0; i<gens.size(); i++ ){
- Node pn = gens[i]->d_match_pattern;
+ for (InstMatchGenerator* g : gens)
+ {
+ Node pn = g->d_match_pattern;
patsn.push_back( pn );
- pat_map_init[pn] = gens[i];
+ pat_map_init[pn] = g;
}
//return mkInstMatchGenerator( q, patsn, qe, pat_map_init );
imgm->d_next = mkInstMatchGenerator( q, patsn, qe, pat_map_init );
q, pat, var_contains[pat]);
}
std::map< Node, std::vector< Node > > var_to_node;
- for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
- for( unsigned i=0; i<it->second.size(); i++ ){
- var_to_node[ it->second[i] ].push_back( it->first );
+ for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
+ {
+ for (const Node& n : vc.second)
+ {
+ var_to_node[n].push_back(vc.first);
}
}
std::vector< Node > pats_ordered;
std::vector< bool > pats_ordered_independent;
std::map< Node, bool > var_bound;
- while( pats_ordered.size()<pats.size() ){
+ size_t patsSize = pats.size();
+ while (pats_ordered.size() < patsSize)
+ {
// score is lexographic ( bound vars, shared vars )
int score_max_1 = -1;
int score_max_2 = -1;
unsigned score_index = 0;
bool set_score_index = false;
- for( unsigned i=0; i<pats.size(); i++ ){
+ for (size_t i = 0; i < patsSize; i++)
+ {
Node p = pats[i];
if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){
int score_1 = 0;
Assert(set_score_index);
//update the variable bounds
Node mp = pats[score_index];
- for( unsigned i=0; i<var_contains[mp].size(); i++ ){
- var_bound[var_contains[mp][i]] = true;
+ std::vector<Node>& vcm = var_contains[mp];
+ for (const Node& vc : vcm)
+ {
+ var_bound[vc] = true;
}
pats_ordered.push_back( mp );
pats_ordered_independent.push_back( score_max_1==0 );
}
Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl;
- for( unsigned i=0; i<pats_ordered.size(); i++ ){
- Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl;
- InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]);
- Assert(cimg != NULL);
+ for (size_t i = 0, poSize = pats_ordered.size(); i < poSize; i++)
+ {
+ Node po = pats_ordered[i];
+ Trace("multi-trigger-linear") << "...make for " << po << std::endl;
+ InstMatchGenerator* cimg = getInstMatchGenerator(q, po);
+ Assert(cimg != nullptr);
d_children.push_back( cimg );
- if( i==0 ){ //TODO : improve
+ // this could be improved
+ if (i == 0)
+ {
cimg->setIndependent();
}
}
}
int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
- for( unsigned i=0; i<d_children.size(); i++ ){
- if( !d_children[i]->reset( Node::null(), qe ) ){
+ for (InstMatchGenerator* c : d_children)
+ {
+ if (!c->reset(Node::null(), qe))
+ {
return -2;
}
}
Assert(eqc.isNull());
if( options::multiTriggerLinear() ){
return true;
- }else{
- return resetChildren( qe )>0;
}
+ return resetChildren(qe) > 0;
}
int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
}
}
Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
- Assert(d_next != NULL);
+ Assert(d_next != nullptr);
int ret_val = continueNextMatch(q, m, qe, tparent);
if( ret_val>0 ){
Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl;
if( options::multiTriggerLinear() ){
// now, restrict everyone
- for( unsigned i=0; i<d_children.size(); i++ ){
+ for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+ {
Node mi = d_children[i]->getCurrentMatch();
Trace("multi-trigger-linear") << " child " << i << " match : " << mi << std::endl;
d_children[i]->excludeMatch( mi );
q, pat, var_contains[pat]);
}
//convert to indicies
- for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
- Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: ";
- for( int i=0; i<(int)it->second.size(); i++ ){
- Trace("multi-trigger-cache") << it->second[i] << " ";
- int index = it->second[i].getAttribute(InstVarNumAttribute());
- d_var_contains[ it->first ].push_back( index );
- d_var_to_node[ index ].push_back( it->first );
+ for (std::pair<const Node, std::vector<Node> >& vc : var_contains)
+ {
+ Trace("multi-trigger-cache") << "Pattern " << vc.first << " contains: ";
+ for (const Node& vcn : vc.second)
+ {
+ Trace("multi-trigger-cache") << vcn << " ";
+ uint64_t index = vcn.getAttribute(InstVarNumAttribute());
+ d_var_contains[vc.first].push_back(index);
+ d_var_to_node[index].push_back(vc.first);
}
Trace("multi-trigger-cache") << std::endl;
}
- for( unsigned i=0; i<pats.size(); i++ ){
+ size_t patsSize = pats.size();
+ for (size_t i = 0; i < patsSize; i++)
+ {
Node n = pats[i];
//make the match generator
InstMatchGenerator* img =
img->setActiveAdd(false);
d_children.push_back(img);
//compute unique/shared variables
- std::vector< int > unique_vars;
- std::map< int, bool > shared_vars;
- int numSharedVars = 0;
- for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
- if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
- Trace("multi-trigger-cache") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
- unique_vars.push_back( d_var_contains[n][j] );
+ std::vector<uint64_t> unique_vars;
+ std::map<uint64_t, bool> shared_vars;
+ unsigned numSharedVars = 0;
+ std::vector<uint64_t>& vctn = d_var_contains[n];
+ for (size_t j = 0, vctnSize = vctn.size(); j < vctnSize; j++)
+ {
+ if (d_var_to_node[vctn[j]].size() == 1)
+ {
+ Trace("multi-trigger-cache")
+ << "Var " << vctn[j] << " is unique to " << pats[i] << std::endl;
+ unique_vars.push_back(vctn[j]);
}else{
- shared_vars[ d_var_contains[n][j] ] = true;
+ shared_vars[vctn[j]] = true;
numSharedVars++;
}
}
//we use the latest shared variables, then unique variables
- std::vector< int > vars;
- unsigned index = i==0 ? pats.size()-1 : (i-1);
+ std::vector<uint64_t> vars;
+ size_t index = i == 0 ? pats.size() - 1 : (i - 1);
while( numSharedVars>0 && index!=i ){
- for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
- if( it->second ){
- if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
- d_var_contains[ pats[index] ].end() ){
- vars.push_back( it->first );
- shared_vars[ it->first ] = false;
+ for (std::pair<const uint64_t, bool>& sv : shared_vars)
+ {
+ if (sv.second)
+ {
+ std::vector<uint64_t>& vctni = d_var_contains[pats[index]];
+ if (std::find(vctni.begin(), vctni.end(), sv.first) != vctni.end())
+ {
+ vars.push_back(sv.first);
+ shared_vars[sv.first] = false;
numSharedVars--;
}
}
}
- index = index==0 ? (int)(pats.size()-1) : (index-1);
+ index = index == 0 ? patsSize - 1 : (index - 1);
}
vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
- Trace("multi-trigger-cache") << " Index[" << i << "]: ";
- for( unsigned j=0; j<vars.size(); j++ ){
- Trace("multi-trigger-cache") << vars[j] << " ";
+ if (Trace.isOn("multi-trigger-cache"))
+ {
+ Trace("multi-trigger-cache") << " Index[" << i << "]: ";
+ for (uint64_t v : vars)
+ {
+ Trace("multi-trigger-cache") << v << " ";
+ }
+ Trace("multi-trigger-cache") << std::endl;
}
- Trace("multi-trigger-cache") << std::endl;
//make ordered inst match trie
d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
{
- for( unsigned i=0; i<d_children.size(); i++ ){
+ for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+ {
delete d_children[i];
}
- for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
- delete it->second;
+ for (std::pair<const size_t, InstMatchTrie::ImtIndexOrder*>& i : d_imtio)
+ {
+ delete i.second;
}
}
/** reset instantiation round (call this whenever equivalence classes have changed) */
void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
- for( unsigned i=0; i<d_children.size(); i++ ){
- d_children[i]->resetInstantiationRound( qe );
+ for (InstMatchGenerator* c : d_children)
+ {
+ c->resetInstantiationRound(qe);
}
}
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
- for( unsigned i=0; i<d_children.size(); i++ ){
- if( !d_children[i]->reset( eqc, qe ) ){
- //return false;
+ for (InstMatchGenerator* c : d_children)
+ {
+ if (!c->reset(eqc, qe))
+ {
+ // do not return false here
}
}
return true;
}
-int InstMatchGeneratorMulti::addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent)
+uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
{
- int addedLemmas = 0;
+ uint64_t addedLemmas = 0;
Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
- for( unsigned i=0; i<d_children.size(); i++ ){
+ for (size_t i = 0, csize = d_children.size(); i < csize; i++)
+ {
Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
std::vector< InstMatch > newMatches;
InstMatch m( q );
m.clear();
}
Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
- for( unsigned j=0; j<newMatches.size(); j++ ){
+ for (size_t j = 0, nmatches = newMatches.size(); j < nmatches; j++)
+ {
Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
if( qe->inConflict() ){
void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
Trigger* tparent,
InstMatch& m,
- int fromChildIndex,
- int& addedLemmas)
+ size_t fromChildIndex,
+ uint64_t& addedLemmas)
{
//see if these produce new matches
d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
// we can safely skip the following lines, even when we have already produced this match.
Trace("multi-trigger-cache-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl;
//process new instantiations
- int childIndex = (fromChildIndex+1)%(int)d_children.size();
+ size_t childIndex = (fromChildIndex + 1) % d_children.size();
processNewInstantiations(qe,
tparent,
m,
void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
Trigger* tparent,
InstMatch& m,
- int& addedLemmas,
+ uint64_t& addedLemmas,
InstMatchTrie* tr,
- int trieIndex,
- int childIndex,
- int endChildIndex,
+ size_t trieIndex,
+ size_t childIndex,
+ size_t endChildIndex,
bool modEq)
{
Assert(!qe->inConflict());
Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m
<< std::endl;
}
- }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
- int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
+ return;
+ }
+ InstMatchTrie::ImtIndexOrder* iio = d_children_trie[childIndex].getOrdering();
+ if (trieIndex < iio->d_order.size())
+ {
+ size_t curr_index = iio->d_order[trieIndex];
// Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
// curr_index );
Node n = m.get( curr_index );
endChildIndex,
modEq);
}
- if (modEq)
+ if (!modEq)
+ {
+ return;
+ }
+ eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
+ // check modulo equality for other possible instantiations
+ if (!ee->hasTerm(n))
+ {
+ return;
+ }
+ eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
+ while (!eqc.isFinished())
{
- // check modulo equality for other possible instantiations
- if (qe->getEqualityQuery()->getEngine()->hasTerm(n))
+ Node en = (*eqc);
+ if (en != n)
{
- eq::EqClassIterator eqc(
- qe->getEqualityQuery()->getEngine()->getRepresentative(n),
- qe->getEqualityQuery()->getEngine());
- while (!eqc.isFinished())
+ std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
+ if (itc != tr->d_data.end())
{
- Node en = (*eqc);
- if (en != n)
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ &(itc->second),
+ trieIndex + 1,
+ childIndex,
+ endChildIndex,
+ modEq);
+ if (qe->inConflict())
{
- std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
- if (itc != tr->d_data.end())
- {
- processNewInstantiations(qe,
- tparent,
- m,
- addedLemmas,
- &(itc->second),
- trieIndex + 1,
- childIndex,
- endChildIndex,
- modEq);
- if (qe->inConflict())
- {
- break;
- }
- }
+ break;
}
- ++eqc;
}
}
+ ++eqc;
}
}else{
- int newChildIndex = (childIndex+1)%(int)d_children.size();
+ size_t newChildIndex = (childIndex + 1) % d_children.size();
processNewInstantiations(qe,
tparent,
m,
Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
}
Assert(Trigger::isSimpleTrigger(d_match_pattern));
- for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
+ for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
+ {
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
if( !options::cegqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
}
-int InstMatchGeneratorSimple::addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent)
+uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
{
- int addedLemmas = 0;
+ uint64_t addedLemmas = 0;
TNodeTrie* tat;
if( d_eqc.isNull() ){
tat = qe->getTermDatabase()->getTermArgTrie( d_op );
void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
QuantifiersEngine* qe,
- int& addedLemmas,
- unsigned argIndex,
+ uint64_t& addedLemmas,
+ size_t argIndex,
TNodeTrie* tat)
{
Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
TNode t = tat->getData();
Debug("simple-trigger") << "Actual term is " << t << std::endl;
//convert to actual used terms
- for (std::map<unsigned, int>::iterator it = d_var_num.begin();
- it != d_var_num.end();
- ++it)
+ for (const std::pair<unsigned, int>& v : d_var_num)
{
- if( it->second>=0 ){
- Assert(it->first < t.getNumChildren());
- Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
- m.setValue( it->second, t[it->first] );
+ if (v.second >= 0)
+ {
+ Assert(v.first < t.getNumChildren());
+ Debug("simple-trigger")
+ << "...set " << v.second << " " << t[v.first] << std::endl;
+ m.setValue(v.second, t[v.first]);
}
}
// we do not need the trigger parent for simple triggers (no post-processing
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
}
- }else{
- if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
- int v = d_var_num[argIndex];
- if( v!=-1 ){
- for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+ return;
+ }
+ if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
+ {
+ int v = d_var_num[argIndex];
+ if (v != -1)
+ {
+ for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+ {
+ Node t = tt.first;
+ Node prev = m.get(v);
+ // using representatives, just check if equal
+ Assert(t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
+ if (prev.isNull() || prev == t)
{
- Node t = tt.first;
- Node prev = m.get( v );
- //using representatives, just check if equal
- Assert(
- t.getType().isComparableTo(d_match_pattern_arg_types[argIndex]));
- if( prev.isNull() || prev==t ){
- m.setValue( v, t);
- addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
- m.setValue( v, prev);
- if( qe->inConflict() ){
- break;
- }
+ m.setValue(v, t);
+ addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
+ m.setValue(v, prev);
+ if (qe->inConflict())
+ {
+ break;
}
}
- return;
}
- //inst constant from another quantified formula, treat as ground term TODO: remove this?
- }
- Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
- std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
- if( it!=tat->d_data.end() ){
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+ return;
}
+ // inst constant from another quantified formula, treat as ground term TODO:
+ // remove this?
+ }
+ Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
+ std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
+ if (it != tat->d_data.end())
+ {
+ addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second));
}
}
int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
- unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+ size_t ngt = qe->getTermDatabase()->getNumGroundTerms(f);
Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl;
- return ngt;
+ return static_cast<int>(ngt);
}
projects / cvc5.git / commitdiff