diff options
Diffstat (limited to 'src/theory/quantifiers')
27 files changed, 228 insertions, 191 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 9e6e4842f..f9bf9335e 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -39,31 +39,40 @@ Node AlphaEquivalenceNode::registerNode(Node q, Node t) std::map< Node, bool > visited; while( !tt.empty() ){ if( tt.size()==arg_index.size()+1 ){ - Node t = tt.back(); + Node tb = tt.back(); Node op; - if( t.hasOperator() ){ - if( visited.find( t )==visited.end() ){ - visited[t] = true; - op = t.getOperator(); + if (tb.hasOperator()) + { + if (visited.find(tb) == visited.end()) + { + visited[tb] = true; + op = tb.getOperator(); arg_index.push_back( 0 ); - }else{ - op = t; + } + else + { + op = tb; arg_index.push_back( -1 ); } - }else{ - op = t; + } + else + { + op = tb; arg_index.push_back( 0 ); } Trace("aeq-debug") << op << " "; - aen = &(aen->d_children[op][t.getNumChildren()]); + aen = &(aen->d_children[op][tb.getNumChildren()]); }else{ - Node t = tt.back(); + Node tb = tt.back(); int i = arg_index.back(); - if( i==-1 || i==(int)t.getNumChildren() ){ + if (i == -1 || i == (int)tb.getNumChildren()) + { tt.pop_back(); arg_index.pop_back(); - }else{ - tt.push_back( t[i] ); + } + else + { + tt.push_back(tb[i]); arg_index[arg_index.size()-1]++; } } diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index cdb15b349..5604d5760 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -229,10 +229,10 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool std::vector< Node > outer_vars; std::vector< Node > inner_vars; - Node q = quants[0]; - for (unsigned i = 0, size = d_ask_types[q].size(); i < size; i++) + Node q0 = quants[0]; + for (unsigned i = 0, size = d_ask_types[q0].size(); i < size; i++) { - Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] ); + Node v = NodeManager::currentNM()->mkBoundVar(d_ask_types[q0][i]); Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl; outer_vars.push_back( v ); } diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 24e3a85b5..c349e05b0 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -150,7 +150,7 @@ Node BvInverter::getPathToPv( { children.push_back(lit.getOperator()); } - for (size_t j = 0, num = lit.getNumChildren(); j < num; j++) + for (size_t j = 0, num2 = lit.getNumChildren(); j < num2; j++) { children.push_back(j == ii ? litc : lit[j]); } diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 8db0501f5..43edb89bf 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -248,9 +248,9 @@ bool CandidateRewriteFilter::notify(Node s, #endif // must convert the inferred substitution to original form std::vector<Node> esubs; - for (const Node& s : subs) + for (const Node& sb : subs) { - esubs.push_back(d_drewrite->toExternal(s)); + esubs.push_back(d_drewrite->toExternal(sb)); } Assert(it != d_pairs.end()); for (const Node& nr : it->second) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index bdab6810c..b82b958af 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -265,24 +265,32 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { if( !eq_terms.empty() ){ Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl; //add equivalent terms as equalities to universal engine - for( unsigned i=0; i<eq_terms.size(); i++ ){ - Trace("thm-ee-add") << " " << eq_terms[i] << std::endl; + for (const Node& eqt : eq_terms) + { + Trace("thm-ee-add") << " " << eqt << std::endl; bool assertEq = false; - if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){ + if (d_urelevant_terms.find(eqt) != d_urelevant_terms.end()) + { assertEq = true; - }else{ - Assert(eq_terms[i].getType() == tn); - registerPattern( eq_terms[i], tn ); - if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){ - setUniversalRelevant( eq_terms[i] ); + } + else + { + Assert(eqt.getType() == tn); + registerPattern(eqt, tn); + if (isUniversalLessThan(eqt, t) + || (options::conjectureUeeIntro() + && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt])) + { + setUniversalRelevant(eqt); assertEq = true; } } if( assertEq ){ Node exp; - d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp ); + d_uequalityEngine.assertEquality(t.eqNode(eqt), true, exp); }else{ - Trace("thm-ee-no-add") << "Do not add : " << t << " == " << eq_terms[i] << std::endl; + Trace("thm-ee-no-add") + << "Do not add : " << t << " == " << eqt << std::endl; } } }else{ @@ -467,8 +475,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) if( n.hasOperator() ){ Trace("sg-gen-eqc") << " (" << n.getOperator(); getTermDatabase()->computeArgReps( n ); - for( unsigned i=0; i<getTermDatabase()->d_arg_reps[n].size(); i++ ){ - Trace("sg-gen-eqc") << " e" << d_em[getTermDatabase()->d_arg_reps[n][i]]; + for (TNode ar : getTermDatabase()->d_arg_reps[n]) + { + Trace("sg-gen-eqc") << " e" << d_em[ar]; } Trace("sg-gen-eqc") << ") :: " << n << std::endl; }else{ @@ -549,16 +558,20 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) inEe = d_ee_conjectures.find( q[1] )!=d_ee_conjectures.end(); if( !inEe ){ //add to universal equality engine - Node nl = getUniversalRepresentative( eq[0], true ); - Node nr = getUniversalRepresentative( eq[1], true ); - if( areUniversalEqual( nl, nr ) ){ + Node nlu = getUniversalRepresentative(eq[0], true); + Node nru = getUniversalRepresentative(eq[1], true); + if (areUniversalEqual(nlu, nru)) + { isSubsume = true; //set inactive (will be ignored by other modules) d_quantEngine->getModel()->setQuantifierActive( q, false ); - }else{ + } + else + { Node exp; d_ee_conjectures[q[1]] = true; - d_uequalityEngine.assertEquality( nl.eqNode( nr ), true, exp ); + d_uequalityEngine.assertEquality( + nlu.eqNode(nru), true, exp); } } Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume ? " and subsumed" : ""); @@ -589,8 +602,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) std::vector< Node > ce; for (unsigned j = 0; j < skolems.size(); j++) { - TNode k = skolems[j]; - TNode rk = getRepresentative( k ); + TNode rk = getRepresentative(skolems[j]); std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk ); //check if it is a ground term if( git==d_ground_eqc_map.end() ){ @@ -613,8 +625,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) } if( disproven ){ Trace("sg-conjecture") << "disproven : " << q << " : "; - for( unsigned i=0; i<ce.size(); i++ ){ - Trace("sg-conjecture") << q[0][i] << " -> " << ce[i] << " "; + for (unsigned j = 0, ceSize = ce.size(); j < ceSize; j++) + { + Trace("sg-conjecture") << q[0][j] << " -> " << ce[j] << " "; } Trace("sg-conjecture") << std::endl; } @@ -900,9 +913,9 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in for (const std::pair<TypeNode, unsigned>& lhs_pattern : d_pattern_var_id[lhs]) { - for (unsigned i = 0; i <= lhs_pattern.second; i++) + for (unsigned j = 0; j <= lhs_pattern.second; j++) { - bvs.push_back(getFreeVar(lhs_pattern.first, i)); + bvs.push_back(getFreeVar(lhs_pattern.first, j)); } } Node rsg; @@ -1159,9 +1172,10 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< children.push_back( nn ); } children.push_back( lc ); - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl; - terms.push_back( n ); + Node nenum = NodeManager::currentNM()->mkNode(APPLY_UF, children); + Trace("sg-gt-enum") + << "Ground term enumerate : " << nenum << std::endl; + terms.push_back(nenum); } // pop the index for the last child vec.pop_back(); diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index b01d5e1df..953121167 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -112,7 +112,7 @@ void HigherOrderTrigger::collectHoVarApplyTerms( bool curWithinApply = withinApply[cur]; visited[cur] = Node::null(); visit.push_back(cur); - for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++) + for (unsigned j = 0, sizec = cur.getNumChildren(); j < sizec; j++) { withinApply[cur[j]] = curWithinApply && j == 0; visit.push_back(cur[j]); @@ -486,7 +486,7 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() // for each function type suffix of the type of f, for example if // f : (Int -> (Int -> Int)) // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int) - for (unsigned a = 0, size = argTypes.size(); a < size; a++) + for (unsigned a = 0, arg_size = argTypes.size(); a < arg_size; a++) { std::vector<TypeNode> sargts; sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end()); diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 4625e762a..08d7f40b1 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -20,6 +20,7 @@ #include <map> #include <memory> #include <vector> + #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/variable_type_map.h" diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 9e924f34d..44d3666e8 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1254,7 +1254,7 @@ Node ExtendedRewriter::extendedRewriteEqChain( // x = ( y & x ) ---> y | ~x // x = ( y & ~x ) ---> ~y & ~x std::vector<Node> new_children; - for (unsigned k = 0, nchild = c.getNumChildren(); k < nchild; k++) + for (unsigned k = 0, nchildc = c.getNumChildren(); k < nchildc; k++) { if (j != k) { @@ -1515,10 +1515,10 @@ Node ExtendedRewriter::partialSubstitute(Node n, if (it == visited.end()) { - std::map<Node, Node>::iterator it = assign.find(cur); - if (it != assign.end()) + std::map<Node, Node>::iterator ita = assign.find(cur); + if (ita != assign.end()) { - visited[cur] = it->second; + visited[cur] = ita->second; } else { diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 2bcb154a0..601452c1f 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -437,11 +437,13 @@ void BoundedIntegers::checkOwnership(Node f) } }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){ Trace("bound-int") << " " << v << " in { "; - for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){ - Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " "; + for (TNode fnr : d_fixed_set_ngr_range[f][v]) + { + Trace("bound-int") << fnr << " "; } - for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){ - Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " "; + for (TNode fgr : d_fixed_set_gr_range[f][v]) + { + Trace("bound-int") << fgr << " "; } Trace("bound-int") << "}" << std::endl; }else if( d_bound_type[f][v]==BOUND_FINITE ){ @@ -705,9 +707,9 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va for( int i=0; i<vindex; i++) { Assert(d_set_nums[q][d_set[q][i]] == i); Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl; - int v = rsi->getVariableOrder( i ); - Assert(q[0][v] == d_set[q][i]); - Node t = rsi->getCurrentTerm(v, true); + int vo = rsi->getVariableOrder(i); + Assert(q[0][vo] == d_set[q][i]); + Node t = rsi->getCurrentTerm(vo, true); Trace("bound-int-rsi") << "term : " << t << std::endl; vars.push_back( d_set[q][i] ); subs.push_back( t ); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 206c8f9dd..3e5d36a7d 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -431,8 +431,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ children.push_back(op); entry_children.push_back(op); bool hasNonStar = false; - for( unsigned i=0; i<c.getNumChildren(); i++) { - Node ri = fm->getRepresentative( c[i] ); + for (const Node& ci : c) + { + Node ri = fm->getRepresentative(ci); children.push_back(ri); bool isStar = false; if (fm->isModelBasisTerm(ri)) @@ -445,7 +446,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ hasNonStar = true; } if( !isStar && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Trace("fmc-warn") << "Warning : model for " << op + << " has non-constant argument in model " << ri + << " (from " << ci << ")" << std::endl; Assert(false); } entry_children.push_back(ri); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index a6e1a369c..5ae05f2a7 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -64,8 +64,9 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { if( fm->isQuantifierActive( q ) ){ //check if any of these quantified formulas can be set inactive if( options::fmfEmptySorts() ){ - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); + for (const Node& var : q[0]) + { + TypeNode tn = var.getType(); //we are allowed to assume the type is empty if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index c2baf8be6..0b48b3995 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -187,9 +187,9 @@ Node FunDefEvaluator::evaluate(Node n) const { Trace("fd-eval-debug2") << "FunDefEvaluator: evaluation with args:\n"; - for (const Node& child : children) + for (const Node& ch : children) { - Trace("fd-eval-debug2") << "..." << child << "\n"; + Trace("fd-eval-debug2") << "..." << ch << "\n"; } Trace("fd-eval-debug2") << "FunDefEvaluator: results in " << sbody << "\n"; diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index fecefb8e1..0339b54f5 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -33,6 +33,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { std::vector< int > fd_assertions; std::map< int, Node > subs_head; //first pass : find defined functions, transform quantifiers + NodeManager* nm = NodeManager::currentNM(); for( unsigned i=0; i<assertions.size(); i++ ){ Node n = QuantAttributes::getFunDefHead( assertions[i] ); if( !n.isNull() ){ @@ -62,9 +63,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { //create functions f1...fn mapping from this sort to concrete elements for( unsigned j=0; j<n.getNumChildren(); j++ ){ TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); - std::stringstream ss; - ss << f << "_arg_" << j; - d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); + std::stringstream ssf; + ssf << f << "_arg_" << j; + d_input_arg_inj[f].push_back( + nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf")); } //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index aed2ae429..1607dc0dc 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -474,14 +474,14 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body, { bool doRewrite = options::iteLiftQuant() == options::IteLiftQuantMode::ALL; - std::vector<Node> children; - children.push_back(ret[i][0]); + std::vector<Node> childrenIte; + childrenIte.push_back(ret[i][0]); for (size_t j = 1; j <= 2; j++) { // check if it rewrites to a constant Node nn = nm->mkNode(EQUAL, no, ret[i][j]); nn = Rewriter::rewrite(nn); - children.push_back(nn); + childrenIte.push_back(nn); if (nn.isConst()) { doRewrite = true; @@ -489,7 +489,7 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body, } if (doRewrite) { - ret = nm->mkNode(ITE, children); + ret = nm->mkNode(ITE, childrenIte); break; } } @@ -1588,6 +1588,7 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA } } if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){ + NodeManager* nm = NodeManager::currentNM(); Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl; Trace("clause-split-debug") << " Ground literals: " << std::endl; for( size_t i=0; i<lits.size(); i++) { @@ -1607,8 +1608,9 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA } Trace("clause-split-debug") << std::endl; Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, eqc_to_var[eqc]); - Node body = it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode( OR, it->second ); - Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); + Node bd = + it->second.size() == 1 ? it->second[0] : nm->mkNode(OR, it->second); + Node fa = nm->mkNode(FORALL, bvl, bd); lits.push_back(fa); } Assert(!lits.empty()); diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 6c7a06ebe..a0e25b756 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -243,7 +243,6 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, } std::map<Node, Node> subs_map; std::map<Node, Node> subs_map_rev; - std::vector<Node> funcs; // normalize the invocations if (!terms.empty()) { @@ -314,8 +313,8 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, // rename bound variables with maximal overlap with si_vars std::unordered_set<Node, NodeHashFunction> fvs; expr::getFreeVariables(cr, fvs); - std::vector<Node> terms; - std::vector<Node> subs; + std::vector<Node> termsNs; + std::vector<Node> subsNs; for (const Node& v : fvs) { TypeNode tn = v.getType(); @@ -325,11 +324,11 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, { if (tn == d_arg_types[k]) { - if (std::find(subs.begin(), subs.end(), d_si_vars[k]) - == subs.end()) + if (std::find(subsNs.begin(), subsNs.end(), d_si_vars[k]) + == subsNs.end()) { - terms.push_back(v); - subs.push_back(d_si_vars[k]); + termsNs.push_back(v); + subsNs.push_back(d_si_vars[k]); Trace("si-prt-debug") << " ...use " << d_si_vars[k] << std::endl; break; @@ -337,9 +336,9 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, } } } - Assert(terms.size() == subs.size()); - cr = - cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end()); + Assert(termsNs.size() == subsNs.size()); + cr = cr.substitute( + termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end()); } cr = Rewriter::rewrite(cr); Trace("si-prt") << ".....got si=" << singleInvocation diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 8c664fec5..5e1bf54f4 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -89,9 +89,9 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) else { Options& nodeManagerOptions = nm->getOptions(); - std::ostream* out = nodeManagerOptions.getOut(); - (*out) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")" - << std::endl; + std::ostream* nodeManagerOut = nodeManagerOptions.getOut(); + (*nodeManagerOut) << "; (filtered " << (d_isStrong ? s : s.negate()) + << ")" << std::endl; } } d_curr_sols.clear(); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 113da2acb..908dde528 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -158,16 +158,19 @@ Node CegSingleInvSol::reconstructSolution(Node sol, do { std::vector< TypeNode > to_erase; for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){ - TypeNode stn = it->first; - Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(stn, index); + TypeNode tn = it->first; + Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(tn, index); if( ns.isNull() ){ - to_erase.push_back( stn ); + to_erase.push_back(tn); }else{ - Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn ); - Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false ); - Trace("csi-rcons-debug2") << " - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl; - std::map< Node, int >::iterator itt = d_rcons_to_id[stn].find( nr ); - if (itt != d_rcons_to_id[stn].end()) + Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin(ns, tn); + Node nr = Rewriter::rewrite(nb); // d_qe->getTermDatabaseSygus()->getNormalized( + // tn, nb, false, false ); + Trace("csi-rcons-debug2") + << " - try " << ns << " -> " << nr << " for " << tn << " " + << nr.getKind() << std::endl; + std::map<Node, int>::iterator itt = d_rcons_to_id[tn].find(nr); + if (itt != d_rcons_to_id[tn].end()) { // if it is not already reconstructed if (d_reconstruct.find(itt->second) == d_reconstruct.end()) diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index cae5cd823..cc6c051cd 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -209,8 +209,8 @@ bool CegisCoreConnective::processInitialize(Node conj, SygusTypeInfo& gti = d_tds->getTypeInfo(gt); for (unsigned r = 0; r < 2; r++) { - Node f = prePost[r]; - if (f.isConst()) + Node node = prePost[r]; + if (node.isConst()) { // this direction is trivial, ignore continue; @@ -225,7 +225,7 @@ bool CegisCoreConnective::processInitialize(Node conj, Trace("sygus-ccore-init") << " will do " << (r == 0 ? "pre" : "post") << "condition." << std::endl; Node cons = gdt[i].getConstructor(); - c.initialize(f, cons); + c.initialize(node, cons); // Register the symmetry breaking lemma: do not do top-level solutions // with this constructor (e.g. we want to enumerate literals, not // conjunctions). @@ -667,8 +667,7 @@ Node CegisCoreConnective::evaluate(Node n, Node cn = d_eval.eval(n, d_vars, mvs); if (cn.isNull()) { - Node cn = - n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end()); + cn = n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end()); cn = Rewriter::rewrite(cn); } if (!id.isNull()) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 3923361b1..5a3df28f5 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -74,17 +74,17 @@ void SygusEnumerator::initialize(Node e) { sblc.push_back(slem); } - for (const Node& sbl : sblc) + for (const Node& sblemma : sblc) { Trace("sygus-enum") - << " symmetry breaking lemma : " << sbl << std::endl; + << " symmetry breaking lemma : " << sblemma << std::endl; // if its a negation of a unit top-level tester, then this specifies // that we should not enumerate terms whose top symbol is that // constructor - if (sbl.getKind() == NOT) + if (sblemma.getKind() == NOT) { Node a; - int tst = datatypes::utils::isTester(sbl[0], a); + int tst = datatypes::utils::isTester(sblemma[0], a); if (tst >= 0) { if (a == e) @@ -205,8 +205,8 @@ void SygusEnumerator::TermCache::initialize(SygusStatistics* s, // record type information for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) { - TypeNode tn = dt[i].getArgType(j); - argTypes[i].push_back(tn); + TypeNode type = dt[i].getArgType(j); + argTypes[i].push_back(type); } } NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 0cc57e0ec..9d327bfe1 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -122,9 +122,9 @@ void SygusEvalUnfold::registerModelValue(Node a, Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl; std::vector<Node> vars; Node var_list = dt.getSygusVarList(); - for (const Node& v : var_list) + for (const Node& var : var_list) { - vars.push_back(v); + vars.push_back(var); } // evaluation children std::vector<Node> eval_children; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a1b46f1ac..259f9c642 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -562,12 +562,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::string dbname = ssb.str(); sdts.push_back(SygusDatatypeGenerator(dbname)); unsigned boolIndex = types.size(); - TypeNode btype = nm->booleanType(); + TypeNode bool_type = nm->booleanType(); TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres); - types.push_back(btype); + types.push_back(bool_type); unres_types.push_back(unres_bt); - type_to_unres[btype] = unres_bt; - sygus_to_builtin[unres_bt] = btype; + type_to_unres[bool_type] = unres_bt; + sygus_to_builtin[unres_bt] = bool_type; // We ensure an ordering on types such that parametric types are processed // before their consitituents. Since parametric types were added before their @@ -689,13 +689,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { // Add PLUS, MINUS Kind kinds[2] = {PLUS, MINUS}; - for (const Kind k : kinds) + for (const Kind kind : kinds) { - Trace("sygus-grammar-def") << "...add for " << k << std::endl; + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; std::vector<TypeNode> cargsOp; cargsOp.push_back(unres_t); cargsOp.push_back(unres_t); - sdts[i].addConstructor(k, cargsOp); + sdts[i].addConstructor(kind, cargsOp); } if (!types[i].isInteger()) { @@ -716,22 +716,22 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<TypeNode> cargsEmpty; sdts.back().addConstructor(nm->mkConst(Rational(1)), "1", cargsEmpty); /* Add operator PLUS */ - Kind k = PLUS; + Kind kind = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; std::vector<TypeNode> cargsPlus; cargsPlus.push_back(unresPosInt); cargsPlus.push_back(unresPosInt); - sdts.back().addConstructor(k, cargsPlus); + sdts.back().addConstructor(kind, cargsPlus); sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true); Trace("sygus-grammar-def") << " ...built datatype " << sdts.back().d_sdt.getDatatype() << " "; /* Adding division at root */ - k = DIVISION; - Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; + kind = DIVISION; + Trace("sygus-grammar-def") << "\t...add for " << kind << std::endl; std::vector<TypeNode> cargsDiv; cargsDiv.push_back(unres_t); cargsDiv.push_back(unresPosInt); - sdts[i].addConstructor(k, cargsDiv); + sdts[i].addConstructor(kind, cargsDiv); } } else if (types[i].isBitVector()) @@ -740,10 +740,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<Kind> un_kinds = {BITVECTOR_NOT, BITVECTOR_NEG}; std::vector<TypeNode> cargsUnary; cargsUnary.push_back(unres_t); - for (const Kind k : un_kinds) + for (const Kind kind : un_kinds) { - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdts[i].addConstructor(k, cargsUnary); + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdts[i].addConstructor(kind, cargsUnary); } // binary apps std::vector<Kind> bin_kinds = {BITVECTOR_AND, @@ -762,10 +762,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<TypeNode> cargsBinary; cargsBinary.push_back(unres_t); cargsBinary.push_back(unres_t); - for (const Kind k : bin_kinds) + for (const Kind kind : bin_kinds) { - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdts[i].addConstructor(k, cargsBinary); + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdts[i].addConstructor(kind, cargsBinary); } } else if (types[i].isString()) @@ -828,11 +828,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...add for constructors" << std::endl; const DType& dt = types[i].getDType(); - for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + for (unsigned l = 0, size_l = dt.getNumConstructors(); l < size_l; ++l) { - Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl; - Node cop = dt[k].getConstructor(); - if (dt[k].getNumArgs() == 0) + Trace("sygus-grammar-def") << "...for " << dt[l].getName() << std::endl; + Node cop = dt[l].getConstructor(); + if (dt[l].getNumArgs() == 0) { // Nullary constructors are interpreted as terms, not operators. // Thus, we apply them to no arguments here. @@ -840,11 +840,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } std::vector<TypeNode> cargsCons; Trace("sygus-grammar-def") << "...add for selectors" << std::endl; - for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j) + for (unsigned j = 0, size_j = dt[l].getNumArgs(); j < size_j; ++j) { Trace("sygus-grammar-def") - << "...for " << dt[k][j].getName() << std::endl; - TypeNode crange = dt[k][j].getRangeType(); + << "...for " << dt[l][j].getName() << std::endl; + TypeNode crange = dt[l][j].getRangeType(); Assert(type_to_unres.find(crange) != type_to_unres.end()); cargsCons.push_back(type_to_unres[crange]); // add to the selector type the selector operator @@ -852,15 +852,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Assert(std::find(types.begin(), types.end(), crange) != types.end()); unsigned i_selType = std::distance( types.begin(), std::find(types.begin(), types.end(), crange)); - TypeNode arg_type = dt[k][j].getType(); + TypeNode arg_type = dt[l][j].getType(); arg_type = arg_type.getSelectorDomainType(); Assert(type_to_unres.find(arg_type) != type_to_unres.end()); std::vector<TypeNode> cargsSel; cargsSel.push_back(type_to_unres[arg_type]); - Node sel = dt[k][j].getSelector(); - sdts[i_selType].addConstructor(sel, dt[k][j].getName(), cargsSel); + Node sel = dt[l][j].getSelector(); + sdts[i_selType].addConstructor(sel, dt[l][j].getName(), cargsSel); } - sdts[i].addConstructor(cop, dt[k].getName(), cargsCons); + sdts[i].addConstructor(cop, dt[l].getName(), cargsCons); } } else if (types[i].isSort() || types[i].isFunction()) @@ -1047,9 +1047,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // use a print callback since we do not want to print the lambda std::shared_ptr<SygusPrintCallback> spc; std::vector<Expr> opLArgsExpr; - for (unsigned i = 0, nvars = opLArgs.size(); i < nvars; i++) + for (unsigned j = 0, nvars = opLArgs.size(); j < nvars; j++) { - opLArgsExpr.push_back(opLArgs[i].toExpr()); + opLArgsExpr.push_back(opLArgs[j].toExpr()); } spc = std::make_shared<printer::SygusExprPrintCallback>( monomial.toExpr(), opLArgsExpr); @@ -1076,9 +1076,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops); std::shared_ptr<SygusPrintCallback> spc; std::vector<Expr> lambdaVarsExpr; - for (unsigned i = 0, nvars = lambdaVars.size(); i < nvars; i++) + for (unsigned j = 0, nvars = lambdaVars.size(); j < nvars; j++) { - lambdaVarsExpr.push_back(lambdaVars[i].toExpr()); + lambdaVarsExpr.push_back(lambdaVars[j].toExpr()); } spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(), lambdaVarsExpr); @@ -1118,7 +1118,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } //------ make Boolean type SygusDatatypeGenerator& sdtBool = sdts[boolIndex]; - Trace("sygus-grammar-def") << "Make grammar for " << btype << std::endl; + Trace("sygus-grammar-def") << "Make grammar for " << bool_type << std::endl; //add variables for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) { @@ -1133,7 +1133,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } // add constants std::vector<Node> consts; - mkSygusConstantsForType(btype, consts); + mkSygusConstantsForType(bool_type, consts); for (unsigned i = 0, size = consts.size(); i < size; ++i) { std::stringstream ss; @@ -1170,15 +1170,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // type specific predicates if (types[i].isReal()) { - Kind k = LEQ; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdtBool.addConstructor(k, cargsBinary); + Kind kind = LEQ; + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdtBool.addConstructor(kind, cargsBinary); } else if (types[i].isBitVector()) { - Kind k = BITVECTOR_ULT; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdtBool.addConstructor(k, cargsBinary); + Kind kind = BITVECTOR_ULT; + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdtBool.addConstructor(kind, cargsBinary); } else if (types[i].isDatatype()) { @@ -1187,13 +1187,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( const DType& dt = types[i].getDType(); std::vector<TypeNode> cargsTester; cargsTester.push_back(unres_types[iuse]); - for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + for (unsigned kind = 0, size_k = dt.getNumConstructors(); kind < size_k; + ++kind) { Trace("sygus-grammar-def") - << "...for " << dt[k].getTester() << std::endl; + << "...for " << dt[kind].getTester() << std::endl; std::stringstream sst; - sst << dt[k].getTester(); - sdtBool.addConstructor(dt[k].getTester(), sst.str(), cargsTester); + sst << dt[kind].getTester(); + sdtBool.addConstructor(dt[kind].getTester(), sst.str(), cargsTester); } } } @@ -1225,10 +1226,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdtBool.addConstructor(k, cargs); } } - if( range==btype ){ + if (range == bool_type) + { startIndex = boolIndex; } - sdtBool.d_sdt.initializeDatatype(btype, bvl, true, true); + sdtBool.d_sdt.initializeDatatype(bool_type, bvl, true, true); Trace("sygus-grammar-def") << "...built datatype for Bool " << sdtBool.d_sdt.getDatatype() << " "; Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 5874104ce..df41672e2 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -106,7 +106,6 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, Node query, bool& needExport) { - NodeManager* nm = NodeManager::currentNM(); if (options::sygusRepairConstTimeout.wasSetByUser()) { // To support a separate timeout for the subsolver, we need to create diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index e3e94ba44..dc21107b1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1343,9 +1343,9 @@ Node SygusUnifIo::constructSol( if (snode.d_strats[i]->d_this == strat_ITE) { // flip the two - EnumTypeInfoStrat* etis = snode.d_strats[i]; + EnumTypeInfoStrat* etis_i = snode.d_strats[i]; snode.d_strats[i] = snode.d_strats[0]; - snode.d_strats[0] = etis; + snode.d_strats[0] = etis_i; break; } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 2b85595cd..1bdae0b20 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -79,11 +79,12 @@ Node SygusUnifRl::purifyLemma(Node n, BoolNodePairMap& cache) { Trace("sygus-unif-rl-purify") << "PurifyLemma : " << n << "\n"; - BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n)); - if (it != cache.end()) + BoolNodePairMap::const_iterator it0 = + cache.find(BoolNodePair(ensureConst, n)); + if (it0 != cache.end()) { Trace("sygus-unif-rl-purify-debug") << "... already visited " << n << "\n"; - return it->second; + return it0->second; } // Recurse unsigned size = n.getNumChildren(); @@ -105,14 +106,14 @@ Node SygusUnifRl::purifyLemma(Node n, // occurring under a unification function-to-synthesize if (ensureConst) { - std::map<Node, Node>::iterator it = d_cand_to_sol.find(n[0]); + std::map<Node, Node>::iterator it1 = d_cand_to_sol.find(n[0]); // if function-to-synthesize, retrieve its built solution to replace in // the application before computing the model value - AlwaysAssert(!u_fapp || it != d_cand_to_sol.end()); - if (it != d_cand_to_sol.end()) + AlwaysAssert(!u_fapp || it1 != d_cand_to_sol.end()); + if (it1 != d_cand_to_sol.end()) { TNode cand = n[0]; - Node tmp = n.substitute(cand, it->second); + Node tmp = n.substitute(cand, it1->second); // should be concrete, can just use the rewriter nv = Rewriter::rewrite(tmp); Trace("sygus-unif-rl-purify") @@ -174,8 +175,8 @@ Node SygusUnifRl::purifyLemma(Node n, if (u_fapp) { Node np; - std::map<Node, Node>::const_iterator it = d_app_to_purified.find(nb); - if (it == d_app_to_purified.end()) + std::map<Node, Node>::const_iterator it2 = d_app_to_purified.find(nb); + if (it2 == d_app_to_purified.end()) { // Build purified head with fresh skolem and recreate node std::stringstream ss; @@ -210,7 +211,7 @@ Node SygusUnifRl::purifyLemma(Node n, } else { - np = it->second; + np = it2->second; } Trace("sygus-unif-rl-purify") << "PurifyLemma : purified head and transformed " << nb << " into " @@ -1069,10 +1070,10 @@ void SygusUnifRl::DecisionTreeInfo::buildDtInfoGain(std::vector<Node>& hds, unsigned picked_cond = 0; std::vector<std::pair<std::vector<Node>, std::vector<Node>>> splits; double current_set_entropy = getEntropy(hds, hd_mv, ind); - for (unsigned i = 0, size = conds.size(); i < size; ++i) + for (unsigned j = 0, conds_size = conds.size(); j < conds_size; ++j) { std::pair<std::vector<Node>, std::vector<Node>> split = - evaluateCond(hds, conds[i]); + evaluateCond(hds, conds[j]); splits.push_back(split); Assert(hds.size() == split.first.size() + split.second.size()); double gain = @@ -1083,12 +1084,12 @@ void SygusUnifRl::DecisionTreeInfo::buildDtInfoGain(std::vector<Node>& hds, indent("sygus-unif-dt-debug", ind); Trace("sygus-unif-dt-debug") << "..gain of " - << d_unif->d_tds->sygusToBuiltin(conds[i], conds[i].getType()) << " is " + << d_unif->d_tds->sygusToBuiltin(conds[j], conds[j].getType()) << " is " << gain << "\n"; if (gain > maxgain) { maxgain = gain; - picked_cond = i; + picked_cond = j; } } // add picked condition diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 052546c0e..c2448abb4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -870,8 +870,8 @@ void SygusUnifStrategy::staticLearnRedundantOps( } if (op.getKind() == kind::BUILTIN) { - Kind k = NodeManager::operatorToKind(op); - if (k == NOT || k == OR || k == AND || k == ITE) + Kind kind = NodeManager::operatorToKind(op); + if (kind == NOT || kind == OR || kind == AND || kind == ITE) { // can eliminate if their argument types are simple loops to this type bool type_ok = true; diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index a77d3681b..978e31545 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -159,9 +159,9 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << "Compute single invocation for " << q << "..." << std::endl; quantifiers::SingleInvocationPartition sip; - std::vector<Node> funcs; - funcs.insert(funcs.end(), q[0].begin(), q[0].end()); - sip.init(funcs, body); + std::vector<Node> funcs0; + funcs0.insert(funcs0.end(), q[0].begin(), q[0].end()); + sip.init(funcs0, body); Trace("cegqi-qep") << "...finished, got:" << std::endl; sip.debugPrint("cegqi-qep"); @@ -204,11 +204,11 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; } - std::vector<Node> funcs; - sip.getFunctions(funcs); - for (unsigned i = 0, size = funcs.size(); i < size; i++) + std::vector<Node> funcs1; + sip.getFunctions(funcs1); + for (unsigned i = 0, size = funcs1.size(); i < size; i++) { - Node f = funcs[i]; + Node f = funcs1[i]; Node fi = sip.getFunctionInvocationFor(f); Node fv = sip.getFirstOrderVariableForFunction(f); Assert(!fi.isNull()); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 0b3428c9d..a1b250142 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -404,17 +404,17 @@ void TermDbSygus::registerEnumerator(Node e, SygusTypeInfo& sti = getTypeInfo(stn); const DType& dt = stn.getDType(); int anyC = sti.getAnyConstantConsNum(); - for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { - bool isAnyC = static_cast<int>(i) == anyC; + bool isAnyC = static_cast<int>(j) == anyC; if (anyC != -1 && !isAnyC) { // if we are using the any constant constructor, do not use any // concrete constant - Node c_op = sti.getConsNumConst(i); + Node c_op = sti.getConsNumConst(j); if (!c_op.isNull()) { - rm_indices.push_back(i); + rm_indices.push_back(j); } } } @@ -844,10 +844,10 @@ bool TermDbSygus::canConstructKind(TypeNode tn, { bool success = true; std::vector<TypeNode> disj_types[2]; - for (unsigned c = 0; c < 2; c++) + for (unsigned cc = 0; cc < 2; cc++) { - if (!canConstructKind(conj_types[c], OR, disj_types[c], true) - || disj_types[c].size() != 2) + if (!canConstructKind(conj_types[cc], OR, disj_types[cc], true) + || disj_types[cc].size() != 2) { success = false; break; @@ -865,8 +865,8 @@ bool TermDbSygus::canConstructKind(TypeNode tn, if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1) { TypeNode ntn = ntypes[0]; - for (unsigned dd = 0, size = disj_types[1 - r].size(); - dd < size; + for (unsigned dd = 0, inner_size = disj_types[1 - r].size(); + dd < inner_size; dd++) { if (disj_types[1 - r][dd] == ntn) |