diff options
Diffstat (limited to 'src/theory')
63 files changed, 862 insertions, 736 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 11cf55354..438e11511 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -513,8 +513,8 @@ SumPair DioSolver::purifyIndex(TrailIndex i){ Constant negOne = Constant::mkConstant(-1); for(uint32_t revIter = d_subs.size(); revIter > 0; --revIter){ - uint32_t i = revIter - 1; - Node freshNode = d_subs[i].d_fresh; + uint32_t i2 = revIter - 1; + Node freshNode = d_subs[i2].d_fresh; if(freshNode.isNull()){ continue; }else{ @@ -523,7 +523,7 @@ SumPair DioSolver::purifyIndex(TrailIndex i){ Constant a = vsum.getCoefficient(VarList(var)); if(!a.isZero()){ - const SumPair& sj = d_trail[d_subs[i].d_constraint].d_eq; + const SumPair& sj = d_trail[d_subs[i2].d_constraint].d_eq; Assert(sj.getPolynomial().getCoefficient(VarList(var)).isOne()); SumPair newSi = (curr * negOne) + (sj * a); Assert(newSi.getPolynomial().getCoefficient(VarList(var)).isZero()); diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 3c1d5f1e9..d09a138fe 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -45,9 +45,9 @@ void NlModel::reset(TheoryModel* m, std::map<Node, Node>& arithModel) d_arithVal.clear(); // process arithModel std::map<Node, Node>::iterator it; - for (const std::pair<const Node, Node>& m : arithModel) + for (const std::pair<const Node, Node>& m2 : arithModel) { - d_arithVal[m.first] = m.second; + d_arithVal[m2.first] = m2.second; } } @@ -700,14 +700,14 @@ bool NlModel::solveEqualitySimple(Node eq, Assert(m_var.isConst()); for (unsigned r = 0; r < 2; r++) { - for (unsigned b = 0; b < 2; b++) + for (unsigned b2 = 0; b2 < 2; b2++) { - Node val = b == 0 ? l : u; + Node val = b2 == 0 ? l : u; // (-b +- approx_sqrt( b^2 - 4ac ))/2a Node approx = nm->mkNode( MULT, coeffa, nm->mkNode(r == 0 ? MINUS : PLUS, negb, val)); approx = Rewriter::rewrite(approx); - bounds[r][b] = approx; + bounds[r][b2] = approx; Assert(approx.isConst()); } if (bounds[r][0].getConst<Rational>() > bounds[r][1].getConst<Rational>()) @@ -776,13 +776,13 @@ bool NlModel::simpleCheckModelLit(Node lit) // x = a is ( x >= a ^ x <= a ) for (unsigned i = 0; i < 2; i++) { - Node lit = nm->mkNode(GEQ, atom[i], atom[1 - i]); + Node lit2 = nm->mkNode(GEQ, atom[i], atom[1 - i]); if (!pol) { - lit = lit.negate(); + lit2 = lit2.negate(); } - lit = Rewriter::rewrite(lit); - bool success = simpleCheckModelLit(lit); + lit2 = Rewriter::rewrite(lit2); + bool success = simpleCheckModelLit(lit2); if (success != pol) { // false != true -> one conjunct of equality is false, we fail @@ -1167,7 +1167,7 @@ bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol) } // must over/under approximate based on vc_set_lower, computed above Node vb = vc_set_lower ? l : u; - for (unsigned i = 0; i < vcfact; i++) + for (unsigned i2 = 0; i2 < vcfact; i2++) { vbs.push_back(vb); } @@ -1317,7 +1317,7 @@ void NlModel::getModelValueRepair( Node v = cb.first; if (l != u) { - Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); + pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); Trace("nl-model") << v << " approximated as " << pred << std::endl; Node witness; if (options::modelWitnessChoice()) diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 2d530d602..cd9352b3a 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -3828,9 +3828,9 @@ std::pair<Node, Node> NonlinearExtension::getTfModelBounds(Node tf, unsigned d) std::vector<Node> bounds; TNode tfv = d_taylor_real_fv; TNode tfs = tf[0]; - for (unsigned d = 0; d < 2; d++) + for (unsigned d2 = 0; d2 < 2; d2++) { - int index = d == 0 ? (isNeg ? 1 : 0) : (isNeg ? 3 : 2); + int index = d2 == 0 ? (isNeg ? 1 : 0) : (isNeg ? 3 : 2); Node pab = pbounds[index]; if (!pab.isNull()) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0ddded6bf..037f0892a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1329,7 +1329,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o Comparison cmp = Comparison::parseNormalForm(in); Polynomial left = cmp.getLeft(); - Polynomial right = cmp.getRight(); Monomial m = left.getHead(); if (m.getVarList().singleton()){ @@ -2173,11 +2172,11 @@ void TheoryArithPrivate::outputConflicts(){ // // Anyways, we reverse the children in `conflict` here. NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND); - for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; - ++i) + for (size_t j = 0, nchildren = conflict.getNumChildren(); j < nchildren; + ++j) { conflictInFarkasCoefficientOrder - << conflict[conflict.getNumChildren() - i - 1]; + << conflict[conflict.getNumChildren() - j - 1]; } if (Debug.isOn("arith::pf::tree")) { @@ -3103,7 +3102,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if(!safeToCallApprox()) { return; } Assert(safeToCallApprox()); - TimerStat::CodeTimer codeTimer(d_statistics.d_solveIntTimer); + TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer); ++(d_statistics.d_solveIntCalls); d_statistics.d_inSolveInteger.setData(1); @@ -3145,7 +3144,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if( relaxRes == LinFeasible ){ MipResult mipRes = MipUnknown; { - TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer); + TimerStat::CodeTimer codeTimer1(d_statistics.d_mipTimer); mipRes = approx->solveMIP(false); } @@ -3183,7 +3182,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ /* All integer branches closed */ approx->setPivotLimit(2*mipLimit); { - TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer); + TimerStat::CodeTimer codeTimer2(d_statistics.d_mipTimer); mipRes = approx->solveMIP(true); } @@ -3215,7 +3214,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ approx->setPivotLimit(2*mipLimit); approx->setBranchingDepth(2); { - TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer); + TimerStat::CodeTimer codeTimer3(d_statistics.d_mipTimer); mipRes = approx->solveMIP(true); } replayLemmas(approx); @@ -3316,7 +3315,7 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){ } bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ - TimerStat::CodeTimer codeTimer(d_statistics.d_solveRealRelaxTimer); + TimerStat::CodeTimer codeTimer0(d_statistics.d_solveRealRelaxTimer); Assert(d_qflraStatus != Result::SAT); d_partialModel.stopQueueingBoundCounts(); @@ -3370,7 +3369,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ ApproximateSimplex::Solution relaxSolution; LinResult relaxRes = LinUnknown; { - TimerStat::CodeTimer codeTimer(d_statistics.d_lpTimer); + TimerStat::CodeTimer codeTimer1(d_statistics.d_lpTimer); relaxRes = approxSolver->solveRelaxation(); } Debug("solveRealRelaxation") << "solve relaxation? " << endl; @@ -3770,7 +3769,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ || options::arithPropagationMode() == options::ArithPropagationMode::BOTH_PROP)) { - TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime); Assert(d_qflraStatus != Result::UNSAT); while(!d_currentPropagationList.empty() && !anyConflict()){ @@ -3823,7 +3822,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ } else { - TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + TimerStat::CodeTimer codeTimer1(d_statistics.d_newPropTime); d_currentPropagationList.clear(); } Assert(d_currentPropagationList.empty()); @@ -5810,11 +5809,11 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg const Tableau::Entry& entry = *ri; ArithVar v = entry.getColVar(); if(v != optVar){ - int sgn = entry.getCoefficient().sgn(); - Assert(sgn != 0); - bool candidate = (sgn > 0) - ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) - : (d_partialModel.cmpAssignmentLowerBound(v) != 0); + int sgn1 = entry.getCoefficient().sgn(); + Assert(sgn1 != 0); + bool candidate = (sgn1 > 0) + ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) + : (d_partialModel.cmpAssignmentLowerBound(v) != 0); if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ entering = v; enteringEntry = &entry; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d721b7e7a..dcf82e6b4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1476,18 +1476,21 @@ void TheoryArrays::check(Effort e) { mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]); iRep = d_equalityEngine.getRepresentative(r[1]); std::pair<TNode, TNode> key(mayRep, iRep); - ReadBucketMap::iterator it = d_readBucketTable.find(key); - if (it == d_readBucketTable.end()) { + ReadBucketMap::iterator rbm_it = d_readBucketTable.find(key); + if (rbm_it == d_readBucketTable.end()) + { bucketList = new(true) CTNodeList(d_readTableContext); d_readBucketAllocations.push_back(bucketList); d_readBucketTable[key] = bucketList; } else { - bucketList = it->second; + bucketList = rbm_it->second; } - CTNodeList::const_iterator it2 = bucketList->begin(), iend = bucketList->end(); - for (; it2 != iend; ++it2) { - const TNode& r2 = *it2; + CTNodeList::const_iterator ctnl_it = bucketList->begin(), + ctnl_iend = bucketList->end(); + for (; ctnl_it != ctnl_iend; ++ctnl_it) + { + const TNode& r2 = *ctnl_it; Assert(r2.getKind() == kind::SELECT); Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0])); Assert(iRep == d_equalityEngine.getRepresentative(r2[1])); diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index d3aeb5c37..f2f12a548 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -95,10 +95,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, // we did not change anything return false; } - NodeNodeMap seen; + NodeNodeMap seen_rev; for (unsigned i = 0; i < new_assertions.size(); ++i) { - new_assertions[i] = reverseAbstraction(new_assertions[i], seen); + new_assertions[i] = reverseAbstraction(new_assertions[i], seen_rev); } // we undo the abstraction functions so the logic is QF_BV still return true; @@ -235,13 +235,15 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) // enumerate arguments assignments std::vector<Node> or_assignments; - for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) + for (const ArgsVec& av : args) + // for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); + // ++it) { NodeBuilder<> arg_assignment(kind::AND); - ArgsVec& args = *it; - for (unsigned k = 0; k < args.size(); ++k) + // ArgsVec& args = *it; + for (unsigned k = 0; k < av.size(); ++k) { - Node eq = nm->mkNode(kind::EQUAL, args[k], skolem_args[k]); + Node eq = nm->mkNode(kind::EQUAL, av[k], skolem_args[k]); arg_assignment << eq; } or_assignments.push_back(arg_assignment); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 14753deec..de8a0e11e 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -984,10 +984,9 @@ Node mergeExplanations(const std::vector<Node>& expls) { TNode expl = expls[i]; Assert(expl.getType().isBoolean()); if (expl.getKind() == kind::AND) { - for (unsigned i = 0; i < expl.getNumChildren(); ++i) { - TNode child = expl[i]; - if (child == utils::mkTrue()) - continue; + for (const TNode& child : expl) + { + if (child == utils::mkTrue()) continue; literals.insert(child); } } else if (expl != utils::mkTrue()) { diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 42f4d3e06..77cb45f36 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -32,21 +32,21 @@ namespace datatypes { RewriteResponse DatatypesRewriter::postRewrite(TNode in) { Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; - Kind k = in.getKind(); + Kind kind = in.getKind(); NodeManager* nm = NodeManager::currentNM(); - if (k == kind::APPLY_CONSTRUCTOR) + if (kind == kind::APPLY_CONSTRUCTOR) { return rewriteConstructor(in); } - else if (k == kind::APPLY_SELECTOR_TOTAL || k == kind::APPLY_SELECTOR) + else if (kind == kind::APPLY_SELECTOR_TOTAL || kind == kind::APPLY_SELECTOR) { return rewriteSelector(in); } - else if (k == kind::APPLY_TESTER) + else if (kind == kind::APPLY_TESTER) { return rewriteTester(in); } - else if (k == kind::DT_SIZE) + else if (kind == kind::DT_SIZE) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { @@ -72,7 +72,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (k == kind::DT_HEIGHT_BOUND) + else if (kind == kind::DT_HEIGHT_BOUND) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { @@ -106,7 +106,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (k == kind::DT_SIZE_BOUND) + else if (kind == kind::DT_SIZE_BOUND) { if (in[0].isConst()) { @@ -114,7 +114,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (k == DT_SYGUS_EVAL) + else if (kind == DT_SYGUS_EVAL) { // sygus evaluation function Node ev = in[0]; @@ -134,7 +134,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, ret); } } - else if (k == MATCH) + else if (kind == MATCH) { Trace("dt-rewrite-match") << "Rewrite match: " << in << std::endl; Node h = in[0]; @@ -223,7 +223,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, ret); } - if (k == kind::EQUAL) + if (kind == kind::EQUAL) { if (in[0] == in[1]) { diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 95b73b2fe..76832e369 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -271,9 +271,10 @@ void SygusExtension::assertTesterInternal( int tindex, TNode n, Node exp, std::v if( xa==a ){ IntMap::const_iterator ittv = d_testers.find( x ); Assert(ittv != d_testers.end()); - int tindex = (*ittv).second; + int tidx = (*ittv).second; const DType& dti = x.getType().getDType(); - if( dti[tindex].getNumArgs()>0 ){ + if (dti[tidx].getNumArgs() > 0) + { NodeMap::const_iterator itt = d_testers_exp.find( x ); Assert(itt != d_testers_exp.end()); conflict.push_back( (*itt).second ); diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index 21fb71bf7..06f1ea79c 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -178,8 +178,8 @@ bool SygusSimpleSymBreak::considerArgKind( // the argument types of the child must be the parent's type for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++) { - TypeNode tn = dt[c].getArgType(i); - if (tn != tnp) + TypeNode type = dt[c].getArgType(i); + if (type != tnp) { return true; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 141c9476f..fc8dedbd3 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -226,20 +226,20 @@ void TheoryDatatypes::check(Effort e) { //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one, // infer the equality. for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){ - TypeNode tn = dt.getRecursiveSingletonArgType(tt, i); + TypeNode type = dt.getRecursiveSingletonArgType(tt, i); if( getQuantifiersEngine() ){ // under the assumption that the cardinality of this type is one - Node a = getSingletonLemma( tn, true ); + Node a = getSingletonLemma(type, true); assumptions.push_back( a.negate() ); }else{ success = false; // assert that the cardinality of this type is more than one - getSingletonLemma( tn, false ); + getSingletonLemma(type, false); } } if( success ){ - Node eq = n.eqNode( itrs->second ); - assumptions.push_back( eq ); + Node assumption = n.eqNode(itrs->second); + assumptions.push_back(assumption); Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions ); Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl; doSendLemma( lemma ); @@ -414,8 +414,9 @@ void TheoryDatatypes::flushPendingFacts(){ lem = fact; }else{ std::vector< Node > children; - for( unsigned i=0; i<assumptions.size(); i++ ){ - children.push_back( assumptions[i].negate() ); + for (const TNode& assumption : assumptions) + { + children.push_back(assumption.negate()); } children.push_back( fact ); lem = NodeManager::currentNM()->mkNode( OR, children ); @@ -1341,19 +1342,19 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { } if( use_s!=rrs ){ Node eq = use_s.eqNode( rrs ); - Node eq_exp; + Node peq; if( options::dtRefIntro() ){ - eq_exp = d_true; + peq = d_true; }else{ - eq_exp = c.eqNode( s[0] ); + peq = c.eqNode(s[0]); } Trace("datatypes-infer") << "DtInfer : collapse sel"; //Trace("datatypes-infer") << ( wrong ? " wrong" : ""); - Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; + Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl; d_pending.push_back( eq ); - d_pending_exp[ eq ] = eq_exp; + d_pending_exp[eq] = peq; d_infer.push_back( eq ); - d_infer_exp.push_back( eq_exp ); + d_infer_exp.push_back(peq); } } } @@ -2039,14 +2040,18 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, if( visited.find( nn ) == visited.end() ) { Trace("datatypes-cycle-check2") << " visit : " << nn << std::endl; visited[nn] = true; - TNode ncons = getEqcConstructor( nn ); - if( ncons.getKind()==APPLY_CONSTRUCTOR ) { - for( unsigned i=0; i<ncons.getNumChildren(); i++ ) { - TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false ); + TNode nncons = getEqcConstructor(nn); + if (nncons.getKind() == APPLY_CONSTRUCTOR) + { + for (unsigned i = 0; i < nncons.getNumChildren(); i++) + { + TNode cn = + searchForCycle(nncons[i], on, visited, proc, explanation, false); if( cn==on ) { //add explanation for why the constructor is connected - if( n != ncons ) { - explainEquality( n, ncons, true, explanation ); + if (n != nncons) + { + explainEquality(n, nncons, true, explanation); } return on; }else if( !cn.isNull() ){ diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index cb9ab1e30..13cc8fc19 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -501,8 +501,8 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args) if (!svarsInit) { svarsInit = true; - TypeNode tn = cur.getType(); - Node varList = tn.getDType().getSygusVarList(); + TypeNode type = cur.getType(); + Node varList = type.getDType().getSygusVarList(); for (const Node& v : varList) { svars.push_back(v); diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index e4e485fd9..665635c38 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -731,10 +731,10 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract( return symbolicBitVector<isSigned>(construct); } -floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t) - : FloatingPointSize(t.getConst<FloatingPointSize>()) +floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type) + : FloatingPointSize(type.getConst<FloatingPointSize>()) { - PRECONDITION(t.isFloatingPoint()); + PRECONDITION(type.isFloatingPoint()); } floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig) : FloatingPointSize(exp, sig) @@ -751,14 +751,14 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const } } -FpConverter::FpConverter(context::UserContext *user) +FpConverter::FpConverter(context::UserContext* user) : #ifdef CVC4_USE_SYMFPU - f(user), - r(user), - b(user), - u(user), - s(user), + d_fpMap(user), + d_rmMap(user), + d_boolMap(user), + d_ubvMap(user), + d_sbvMap(user), #endif d_additionalAssertions(user) { @@ -863,9 +863,9 @@ Node FpConverter::convert(TNode node) if (t.isRoundingMode()) { - rmMap::const_iterator i(r.find(current)); + rmMap::const_iterator i(d_rmMap.find(current)); - if (i == r.end()) + if (i == d_rmMap.end()) { if (Theory::isLeafOf(current, THEORY_FP)) { @@ -875,14 +875,20 @@ Node FpConverter::convert(TNode node) switch (current.getConst<RoundingMode>()) { case roundNearestTiesToEven: - r.insert(current, traits::RNE()); + d_rmMap.insert(current, traits::RNE()); break; case roundNearestTiesToAway: - r.insert(current, traits::RNA()); + d_rmMap.insert(current, traits::RNA()); + break; + case roundTowardPositive: + d_rmMap.insert(current, traits::RTP()); + break; + case roundTowardNegative: + d_rmMap.insert(current, traits::RTN()); + break; + case roundTowardZero: + d_rmMap.insert(current, traits::RTZ()); break; - case roundTowardPositive: r.insert(current, traits::RTP()); break; - case roundTowardNegative: r.insert(current, traits::RTN()); break; - case roundTowardZero: r.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; } } @@ -890,7 +896,7 @@ Node FpConverter::convert(TNode node) { /******** Variables ********/ rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current)); - r.insert(current, tmp); + d_rmMap.insert(current, tmp); d_additionalAssertions.push_back(tmp.valid()); } } @@ -903,23 +909,23 @@ Node FpConverter::convert(TNode node) } else if (t.isFloatingPoint()) { - fpMap::const_iterator i(f.find(current)); + fpMap::const_iterator i(d_fpMap.find(current)); - if (i == f.end()) + if (i == d_fpMap.end()) { if (Theory::isLeafOf(current, THEORY_FP)) { if (current.getKind() == kind::CONST_FLOATINGPOINT) { /******** Constants ********/ - f.insert(current, - symfpu::unpackedFloat<traits>( - current.getConst<FloatingPoint>().getLiteral())); + d_fpMap.insert(current, + symfpu::unpackedFloat<traits>( + current.getConst<FloatingPoint>().getLiteral())); } else { /******** Variables ********/ - f.insert(current, buildComponents(current)); + d_fpMap.insert(current, buildComponents(current)); } } else @@ -937,9 +943,9 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_ABS: case kind::FLOATINGPOINT_NEG: { - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -949,14 +955,14 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_ABS: - f.insert(current, - symfpu::absolute<traits>(fpt(current.getType()), - (*arg1).second)); + d_fpMap.insert(current, + symfpu::absolute<traits>( + fpt(current.getType()), (*arg1).second)); break; case kind::FLOATINGPOINT_NEG: - f.insert(current, - symfpu::negate<traits>(fpt(current.getType()), - (*arg1).second)); + d_fpMap.insert(current, + symfpu::negate<traits>(fpt(current.getType()), + (*arg1).second)); break; default: Unreachable() << "Unknown unary floating-point function"; @@ -968,18 +974,19 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_SQRT: case kind::FLOATINGPOINT_RTI: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -989,13 +996,13 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_SQRT: - f.insert(current, - symfpu::sqrt<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second)); + d_fpMap.insert(current, + symfpu::sqrt<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second)); break; case kind::FLOATINGPOINT_RTI: - f.insert( + d_fpMap.insert( current, symfpu::roundToIntegral<traits>(fpt(current.getType()), (*mode).second, @@ -1011,25 +1018,26 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_REM: { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - f.insert( + d_fpMap.insert( current, symfpu::remainder<traits>( fpt(current.getType()), (*arg1).second, (*arg2).second)); @@ -1039,20 +1047,21 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_MIN_TOTAL: case kind::FLOATINGPOINT_MAX_TOTAL: { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); // current[2] is a bit-vector so we do not need to recurse down it - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1062,19 +1071,19 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_MAX_TOTAL: - f.insert(current, - symfpu::max<traits>(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); + d_fpMap.insert(current, + symfpu::max<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); break; case kind::FLOATINGPOINT_MIN_TOTAL: - f.insert(current, - symfpu::min<traits>(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); + d_fpMap.insert(current, + symfpu::min<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); break; default: @@ -1090,24 +1099,25 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_MULT: case kind::FLOATINGPOINT_DIV: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - fpMap::const_iterator arg2(f.find(current[2])); - bool recurseNeeded = - (mode == r.end()) || (arg1 == f.end()) || (arg2 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + fpMap::const_iterator arg2(d_fpMap.find(current[2])); + bool recurseNeeded = (mode == d_rmMap.end()) + || (arg1 == d_fpMap.end()) + || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[2]); } @@ -1117,12 +1127,12 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_PLUS: - f.insert(current, - symfpu::add<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - prop(true))); + d_fpMap.insert(current, + symfpu::add<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + prop(true))); break; case kind::FLOATINGPOINT_SUB: @@ -1133,22 +1143,23 @@ Node FpConverter::convert(TNode node) break; case kind::FLOATINGPOINT_MULT: - f.insert(current, - symfpu::multiply<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); + d_fpMap.insert( + current, + symfpu::multiply<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); break; case kind::FLOATINGPOINT_DIV: - f.insert(current, - symfpu::divide<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); + d_fpMap.insert(current, + symfpu::divide<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); break; case kind::FLOATINGPOINT_REM: /* - f.insert(current, + d_fpMap.insert(current, symfpu::remainder<traits>(fpt(current.getType()), (*mode).second, (*arg1).second, @@ -1169,66 +1180,68 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_FMA: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - fpMap::const_iterator arg2(f.find(current[2])); - fpMap::const_iterator arg3(f.find(current[3])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()) - || (arg2 == f.end() || (arg3 == f.end())); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + fpMap::const_iterator arg2(d_fpMap.find(current[2])); + fpMap::const_iterator arg3(d_fpMap.find(current[3])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()) + || (arg2 == d_fpMap.end() || (arg3 == d_fpMap.end())); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[2]); } - if (arg3 == f.end()) + if (arg3 == d_fpMap.end()) { workStack.push_back(current[3]); } continue; // i.e. recurse! } - f.insert(current, - symfpu::fma<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - (*arg3).second)); + d_fpMap.insert(current, + symfpu::fma<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + (*arg3).second)); } break; /******** Conversions ********/ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - f.insert( + d_fpMap.insert( current, symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()), fpt(current.getType()), @@ -1241,27 +1254,28 @@ Node FpConverter::convert(TNode node) { Node IEEEBV(nm->mkNode( kind::BITVECTOR_CONCAT, current[0], current[1], current[2])); - f.insert(current, - symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); + d_fpMap.insert( + current, + symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); } break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - f.insert(current, - symfpu::unpack<traits>(fpt(current.getType()), - ubv(current[0]))); + d_fpMap.insert(current, + symfpu::unpack<traits>(fpt(current.getType()), + ubv(current[0]))); break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: { - rmMap::const_iterator mode(r.find(current[0])); - bool recurseNeeded = (mode == r.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + bool recurseNeeded = (mode == d_rmMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } @@ -1271,7 +1285,7 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - f.insert( + d_fpMap.insert( current, symfpu::convertSBVToFloat<traits>(fpt(current.getType()), (*mode).second, @@ -1279,7 +1293,7 @@ Node FpConverter::convert(TNode node) break; case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - f.insert( + d_fpMap.insert( current, symfpu::convertUBVToFloat<traits>(fpt(current.getType()), (*mode).second, @@ -1296,7 +1310,7 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_FP_REAL: { - f.insert(current, buildComponents(current)); + d_fpMap.insert(current, buildComponents(current)); // Rely on the real theory and theory combination // to handle the value } @@ -1316,9 +1330,9 @@ Node FpConverter::convert(TNode node) } else if (t.isBoolean()) { - boolMap::const_iterator i(b.find(current)); + boolMap::const_iterator i(d_boolMap.find(current)); - if (i == b.end()) + if (i == d_boolMap.end()) { switch (current.getKind()) { @@ -1329,49 +1343,52 @@ Node FpConverter::convert(TNode node) if (childType.isFloatingPoint()) { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - b.insert(current, - symfpu::smtlibEqual<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::smtlibEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); } else if (childType.isRoundingMode()) { - rmMap::const_iterator arg1(r.find(current[0])); - rmMap::const_iterator arg2(r.find(current[1])); - bool recurseNeeded = (arg1 == r.end()) || (arg2 == r.end()); + rmMap::const_iterator arg1(d_rmMap.find(current[0])); + rmMap::const_iterator arg2(d_rmMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_rmMap.end()) || (arg2 == d_rmMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == r.end()) + if (arg1 == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg2 == r.end()) + if (arg2 == d_rmMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - b.insert(current, (*arg1).second == (*arg2).second); + d_boolMap.insert(current, (*arg1).second == (*arg2).second); } else { @@ -1386,18 +1403,19 @@ Node FpConverter::convert(TNode node) { TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1407,15 +1425,17 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_LEQ: - b.insert(current, - symfpu::lessThanOrEqual<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::lessThanOrEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); break; case kind::FLOATINGPOINT_LT: - b.insert(current, - symfpu::lessThan<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::lessThan<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); break; default: @@ -1434,9 +1454,9 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_ISPOS: { TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -1446,42 +1466,43 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_ISN: - b.insert( + d_boolMap.insert( current, symfpu::isNormal<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISSN: - b.insert(current, - symfpu::isSubnormal<traits>(fpt(childType), - (*arg1).second)); + d_boolMap.insert(current, + symfpu::isSubnormal<traits>(fpt(childType), + (*arg1).second)); break; case kind::FLOATINGPOINT_ISZ: - b.insert( + d_boolMap.insert( current, symfpu::isZero<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISINF: - b.insert( + d_boolMap.insert( current, symfpu::isInfinite<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISNAN: - b.insert(current, - symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); + d_boolMap.insert( + current, + symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISPOS: - b.insert( + d_boolMap.insert( current, symfpu::isPositive<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISNEG: - b.insert( + d_boolMap.insert( current, symfpu::isNegative<traits>(fpt(childType), (*arg1).second)); break; @@ -1513,7 +1534,7 @@ Node FpConverter::convert(TNode node) break; } - i = b.find(current); + i = d_boolMap.find(current); } result = (*i).second; @@ -1526,22 +1547,23 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_UBV_TOTAL: { TypeNode childType(current[1].getType()); - ubvMap::const_iterator i(u.find(current)); + ubvMap::const_iterator i(d_ubvMap.find(current)); - if (i == u.end()) + if (i == d_ubvMap.end()) { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1551,13 +1573,13 @@ Node FpConverter::convert(TNode node) FloatingPointToUBVTotal info = current.getOperator().getConst<FloatingPointToUBVTotal>(); - u.insert(current, - symfpu::convertFloatToUBV<traits>(fpt(childType), - (*mode).second, - (*arg1).second, - info.bvs, - ubv(current[2]))); - i = u.find(current); + d_ubvMap.insert(current, + symfpu::convertFloatToUBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + ubv(current[2]))); + i = d_ubvMap.find(current); } result = (*i).second; @@ -1567,22 +1589,23 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_SBV_TOTAL: { TypeNode childType(current[1].getType()); - sbvMap::const_iterator i(s.find(current)); + sbvMap::const_iterator i(d_sbvMap.find(current)); - if (i == s.end()) + if (i == d_sbvMap.end()) { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1592,14 +1615,14 @@ Node FpConverter::convert(TNode node) FloatingPointToSBVTotal info = current.getOperator().getConst<FloatingPointToSBVTotal>(); - s.insert(current, - symfpu::convertFloatToSBV<traits>(fpt(childType), - (*mode).second, - (*arg1).second, - info.bvs, - sbv(current[2]))); + d_sbvMap.insert(current, + symfpu::convertFloatToSBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + sbv(current[2]))); - i = s.find(current); + i = d_sbvMap.find(current); } result = (*i).second; @@ -1639,9 +1662,9 @@ Node FpConverter::convert(TNode node) // (via auxiliary constraints) TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -1689,9 +1712,9 @@ Node FpConverter::getValue(Valuation &val, TNode var) if (t.isRoundingMode()) { - rmMap::const_iterator i(r.find(var)); + rmMap::const_iterator i(d_rmMap.find(var)); - if (i == r.end()) + if (i == d_rmMap.end()) { Unreachable() << "Asking for the value of an unregistered expression"; } @@ -1703,9 +1726,9 @@ Node FpConverter::getValue(Valuation &val, TNode var) } else if (t.isFloatingPoint()) { - fpMap::const_iterator i(f.find(var)); + fpMap::const_iterator i(d_fpMap.find(var)); - if (i == f.end()) + if (i == d_fpMap.end()) { Unreachable() << "Asking for the value of an unregistered expression"; } diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 8ff5293e2..344dcf926 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -318,11 +318,11 @@ class FpConverter typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap; typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap; - fpMap f; - rmMap r; - boolMap b; - ubvMap u; - sbvMap s; + fpMap d_fpMap; + rmMap d_rmMap; + boolMap d_boolMap; + ubvMap d_ubvMap; + sbvMap d_sbvMap; /* These functions take a symfpu object and convert it to a node. * These should ensure that constant folding it will give a diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp index 729a18ee4..4a3426222 100644 --- a/src/theory/idl/idl_model.cpp +++ b/src/theory/idl/idl_model.cpp @@ -22,42 +22,52 @@ using namespace theory; using namespace idl; IDLModel::IDLModel(context::Context* context) -: d_model(context) -, d_reason(context) -{} + : d_model(context), d_reason(context) +{ +} -Integer IDLModel::getValue(TNode var) const { +Integer IDLModel::getValue(TNode var) const +{ model_value_map::const_iterator find = d_model.find(var); - if (find != d_model.end()) { + if (find != d_model.end()) + { return (*find).second; - } else { + } + else + { return 0; } } -void IDLModel::setValue(TNode var, Integer value, IDLReason reason) { - Assert(!reason.constraint.isNull()); +void IDLModel::setValue(TNode var, Integer value, IDLReason reason) +{ + Assert(!reason.d_constraint.isNull()); d_model[var] = value; d_reason[var] = reason; } -void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) { +void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) +{ TNode current = var; - do { + do + { Debug("theory::idl::model") << "processing: " << var << std::endl; Assert(d_reason.find(current) != d_reason.end()); IDLReason reason = d_reason[current]; - Debug("theory::idl::model") << "adding reason: " << reason.constraint << std::endl; - reasons.push_back(reason.constraint); - current = reason.x; + Debug("theory::idl::model") + << "adding reason: " << reason.d_constraint << std::endl; + reasons.push_back(reason.d_constraint); + current = reason.d_x; } while (current != var); } -void IDLModel::toStream(std::ostream& out) const { +void IDLModel::toStream(std::ostream& out) const +{ model_value_map::const_iterator it = d_model.begin(); model_value_map::const_iterator it_end = d_model.end(); out << "Model[" << std::endl; - for (; it != it_end; ++ it) { + for (; it != it_end; ++it) + { out << (*it).first << " -> " << (*it).second << std::endl; } out << "]"; diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h index 87e67edea..610b90695 100644 --- a/src/theory/idl/idl_model.h +++ b/src/theory/idl/idl_model.h @@ -17,8 +17,8 @@ #pragma once -#include "expr/node.h" #include "context/cdhashmap.h" +#include "expr/node.h" namespace CVC4 { namespace theory { @@ -30,14 +30,14 @@ namespace idl { * value of x is 0, then the variable x and the constraint (y > 0) are a reason * for the y taking the value 1. */ -struct IDLReason { +struct IDLReason +{ /** The variable of the reason */ - TNode x; + TNode d_x; /** The constraint of the reason */ - TNode constraint; + TNode d_constraint; - IDLReason(TNode x, TNode constraint) - : x(x), constraint(constraint) {} + IDLReason(TNode x, TNode constraint) : d_x(x), d_constraint(constraint) {} IDLReason() {} }; @@ -45,10 +45,11 @@ struct IDLReason { * A model maps variables to integer values and backs them up with reasons. * Default values (if not set with setValue) for all variables are 0. */ -class IDLModel { - +class IDLModel +{ typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map; - typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> model_reason_map; + typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> + model_reason_map; /** Values assigned to individual variables */ model_value_map d_model; @@ -56,8 +57,7 @@ class IDLModel { /** Reasons constraining the individual variables */ model_reason_map d_reason; -public: - + public: IDLModel(context::Context* context); /** Get the model value of the variable */ @@ -71,14 +71,14 @@ public: /** Output to the given stream */ void toStream(std::ostream& out) const; - }; -inline std::ostream& operator << (std::ostream& out, const IDLModel& model) { +inline std::ostream& operator<<(std::ostream& out, const IDLModel& model) +{ model.toStream(out); return out; } -} -} -} +} // namespace idl +} // namespace theory +} // namespace CVC4 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) diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index e5d6748aa..765c2b4c8 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -52,33 +52,33 @@ struct RewriteStackElement { * Construct a fresh stack element. */ RewriteStackElement(TNode node, TheoryId theoryId) - : node(node), - original(node), - theoryId(theoryId), - originalTheoryId(theoryId), - nextChild(0) + : d_node(node), + d_original(node), + d_theoryId(theoryId), + d_originalTheoryId(theoryId), + d_nextChild(0) { } - TheoryId getTheoryId() { return static_cast<TheoryId>(theoryId); } + TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); } TheoryId getOriginalTheoryId() { - return static_cast<TheoryId>(originalTheoryId); + return static_cast<TheoryId>(d_originalTheoryId); } /** The node we're currently rewriting */ - Node node; + Node d_node; /** Original node */ - Node original; + Node d_original; /** Id of the theory that's currently rewriting this node */ - unsigned theoryId : 8; + unsigned d_theoryId : 8; /** Id of the original theory that started the rewrite */ - unsigned originalTheoryId : 8; + unsigned d_originalTheoryId : 8; /** Index of the child this node is done rewriting */ - unsigned nextChild : 32; + unsigned d_nextChild : 32; /** Builder for this node */ - NodeBuilder<> builder; + NodeBuilder<> d_builder; }; Node Rewriter::rewrite(TNode node) { @@ -140,71 +140,73 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Trace("rewriter") << "Rewriter::rewriting: " << rewriteStackTop.getTheoryId() << "," - << rewriteStackTop.node << std::endl; + << rewriteStackTop.d_node << std::endl; // Before rewriting children we need to do a pre-rewrite of the node - if (rewriteStackTop.nextChild == 0) { - + if (rewriteStackTop.d_nextChild == 0) + { // Check if the pre-rewrite has already been done (it's in the cache) - Node cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), - rewriteStackTop.node); + cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), + rewriteStackTop.d_node); if (cached.isNull()) { // Rewrite until fix-point is reached for(;;) { // Perform the pre-rewrite RewriteResponse response = d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite( - rewriteStackTop.node); + rewriteStackTop.d_node); // Put the rewritten node to the top of the stack - rewriteStackTop.node = response.d_node; - TheoryId newTheory = theoryOf(rewriteStackTop.node); + rewriteStackTop.d_node = response.d_node; + TheoryId newTheory = theoryOf(rewriteStackTop.d_node); // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite if (newTheory == rewriteStackTop.getTheoryId() && response.d_status == REWRITE_DONE) { break; } - rewriteStackTop.theoryId = newTheory; + rewriteStackTop.d_theoryId = newTheory; } // Cache the rewrite setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(), - rewriteStackTop.original, - rewriteStackTop.node); + rewriteStackTop.d_original, + rewriteStackTop.d_node); } // Otherwise we're have already been pre-rewritten (in pre-rewrite cache) else { // Continue with the cached version - rewriteStackTop.node = cached; - rewriteStackTop.theoryId = theoryOf(cached); + rewriteStackTop.d_node = cached; + rewriteStackTop.d_theoryId = theoryOf(cached); } } - rewriteStackTop.original =rewriteStackTop.node; + rewriteStackTop.d_original = rewriteStackTop.d_node; // Now it's time to rewrite the children, check if this has already been done - Node cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), - rewriteStackTop.node); + cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), + rewriteStackTop.d_node); // If not, go through the children if(cached.isNull()) { // The child we need to rewrite - unsigned child = rewriteStackTop.nextChild++; + unsigned child = rewriteStackTop.d_nextChild++; // To build the rewritten expression we set up the builder if(child == 0) { - if (rewriteStackTop.node.getNumChildren() > 0) { + if (rewriteStackTop.d_node.getNumChildren() > 0) + { // The children will add themselves to the builder once they're done - rewriteStackTop.builder << rewriteStackTop.node.getKind(); - kind::MetaKind metaKind = rewriteStackTop.node.getMetaKind(); + rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind(); + kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind(); if (metaKind == kind::metakind::PARAMETERIZED) { - rewriteStackTop.builder << rewriteStackTop.node.getOperator(); + rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator(); } } } // Process the next child - if(child < rewriteStackTop.node.getNumChildren()) { + if (child < rewriteStackTop.d_node.getNumChildren()) + { // The child node - Node childNode = rewriteStackTop.node[child]; + Node childNode = rewriteStackTop.d_node[child]; // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now) rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode))); // Go on with the rewriting @@ -212,10 +214,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } // Incorporate the children if necessary - if (rewriteStackTop.node.getNumChildren() > 0) { - Node rewritten = rewriteStackTop.builder; - rewriteStackTop.node = rewritten; - rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node); + if (rewriteStackTop.d_node.getNumChildren() > 0) + { + Node rewritten = rewriteStackTop.d_builder; + rewriteStackTop.d_node = rewritten; + rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node); } // Done with all pre-rewriting, so let's do the post rewrite @@ -223,14 +226,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Do the post-rewrite RewriteResponse response = d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite( - rewriteStackTop.node); + rewriteStackTop.d_node); // We continue with the response we got TheoryId newTheoryId = theoryOf(response.d_node); if (newTheoryId != rewriteStackTop.getTheoryId() || response.d_status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite - Assert(response.d_node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.d_node); //TODO: this is not thread-safe - should make this assertion dependent on sequential build #ifdef CVC4_ASSERTIONS Assert(d_rewriteStack->find(response.d_node) @@ -238,7 +241,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_rewriteStack->insert(response.d_node); #endif Node rewritten = rewriteTo(newTheoryId, response.d_node); - rewriteStackTop.node = rewritten; + rewriteStackTop.d_node = rewritten; #ifdef CVC4_ASSERTIONS d_rewriteStack->erase(response.d_node); #endif @@ -251,36 +254,36 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); Assert(r2.d_node == response.d_node); #endif - rewriteStackTop.node = response.d_node; + rewriteStackTop.d_node = response.d_node; break; } // Check for trivial rewrite loops of size 1 or 2 - Assert(response.d_node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.d_node); Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()] ->postRewrite(response.d_node) .d_node - != rewriteStackTop.node); - rewriteStackTop.node = response.d_node; + != rewriteStackTop.d_node); + rewriteStackTop.d_node = response.d_node; } // We're done with the post rewrite, so we add to the cache setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), - rewriteStackTop.original, - rewriteStackTop.node); + rewriteStackTop.d_original, + rewriteStackTop.d_node); } else { // We were already in cache, so just remember it - rewriteStackTop.node = cached; - rewriteStackTop.theoryId = theoryOf(cached); + rewriteStackTop.d_node = cached; + rewriteStackTop.d_theoryId = theoryOf(cached); } // If this is the last node, just return if (rewriteStack.size() == 1) { - Assert(!isEquality || rewriteStackTop.node.getKind() == kind::EQUAL - || rewriteStackTop.node.isConst()); - return rewriteStackTop.node; + Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL + || rewriteStackTop.d_node.isConst()); + return rewriteStackTop.d_node; } // We're done with this node, append it to the parent - rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node; + rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node; rewriteStack.pop_back(); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 1a798414e..866c80863 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -304,24 +304,25 @@ bool TheorySetsPrivate::assertFact(Node fact, Node exp) Node s = e->d_singleton; if (!s.isNull()) { - Node exp = NodeManager::currentNM()->mkNode( + Node pexp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode(s)); - d_keep.insert(exp); + d_keep.insert(pexp); if (s.getKind() == kind::SINGLETON) { if (s[0] != atom[0]) { - Trace("sets-prop") << "Propagate mem-eq : " << exp << std::endl; + Trace("sets-prop") + << "Propagate mem-eq : " << pexp << std::endl; Node eq = s[0].eqNode(atom[0]); d_keep.insert(eq); - assertFact(eq, exp); + assertFact(eq, pexp); } } else { Trace("sets-prop") - << "Propagate mem-eq conflict : " << exp << std::endl; - d_state.setConflict(exp); + << "Propagate mem-eq conflict : " << pexp << std::endl; + d_state.setConflict(pexp); } } } @@ -774,8 +775,8 @@ void TheorySetsPrivate::checkUpwardsClosure() std::vector<Node> exp; exp.push_back(itm2m.second); d_state.addEqualityToExp(term[1], itm2m.second[1], exp); - Node k = d_state.getProxy(term); - Node fact = nm->mkNode(kind::MEMBER, x, k); + Node r = d_state.getProxy(term); + Node fact = nm->mkNode(kind::MEMBER, x, r); d_im.assertInference(fact, exp, "upc2"); if (d_state.isInConflict()) { diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 135175665..a1fc67385 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -21,6 +21,7 @@ #include <map> #include <memory> #include <vector> + #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/variable_type_map.h" diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 343f6e4f8..c23041914 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -155,19 +155,19 @@ void BaseSolver::checkInit() std::vector<Node> exp; // explain empty components bool foundNEmpty = false; - for (const Node& nc : n) + for (const Node& nnc : n) { - if (d_state.areEqual(nc, d_emptyString)) + if (d_state.areEqual(nnc, d_emptyString)) { - if (nc != d_emptyString) + if (nnc != d_emptyString) { - exp.push_back(nc.eqNode(d_emptyString)); + exp.push_back(nnc.eqNode(d_emptyString)); } } else { Assert(!foundNEmpty); - ns = nc; + ns = nnc; foundNEmpty = true; } } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 723520b67..5414c9b98 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -485,10 +485,10 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< if( eqc==d_emptyString ){ //for empty eqc, ensure all components are empty if( nr!=d_emptyString ){ - std::vector< Node > exp; - exp.push_back( n.eqNode( d_emptyString ) ); + std::vector<Node> exps; + exps.push_back(n.eqNode(d_emptyString)); d_im.sendInference( - exp, n[i].eqNode(d_emptyString), "I_CYCLE_E"); + exps, n[i].eqNode(d_emptyString), "I_CYCLE_E"); return Node::null(); } }else{ @@ -1576,9 +1576,9 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, } Node split_eq; - for (unsigned r = 0; r < 2; r++) + for (unsigned i = 0; i < 2; i++) { - Node t = r == 0 ? veci[loop_index] : t_yz; + Node t = i == 0 ? veci[loop_index] : t_yz; split_eq = t.eqNode(d_emptyString); Node split_eqr = Rewriter::rewrite(split_eq); // the equality could rewrite to false diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index b04b88b31..af114e361 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -570,16 +570,16 @@ void ExtfSolver::checkExtfInference(Node n, { bool do_infer = false; conc = conc.negate(); - bool pol = conc.getKind() != NOT; - Node lit = pol ? conc : conc[0]; + bool pol2 = conc.getKind() != NOT; + Node lit = pol2 ? conc : conc[0]; if (lit.getKind() == EQUAL) { - do_infer = pol ? !d_state.areEqual(lit[0], lit[1]) - : !d_state.areDisequal(lit[0], lit[1]); + do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1]) + : !d_state.areDisequal(lit[0], lit[1]); } else { - do_infer = !d_state.areEqual(lit, pol ? d_true : d_false); + do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false); } if (do_infer) { diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 1942938c3..86995736e 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -303,15 +303,15 @@ Node RegExpElimination::eliminateConcat(Node atom) // process the non-greedy find variables if (!non_greedy_find_vars.empty()) { - std::vector<Node> children; + std::vector<Node> children2; for (const Node& v : non_greedy_find_vars) { Node bound = nm->mkNode( AND, nm->mkNode(LEQ, d_zero, v), nm->mkNode(LT, v, lenx)); - children.push_back(bound); + children2.push_back(bound); } - children.push_back(res); - Node body = nm->mkNode(AND, children); + children2.push_back(res); + Node body = nm->mkNode(AND, children2); Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars); res = nm->mkNode(EXISTS, bvl, body); } diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0e8347281..530564a35 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -772,8 +772,8 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) firstChars(r[i], cset, vset); Node n = r[i]; Node exp; - int r = delta( n, exp ); - if(r != 1) { + if (delta(n, exp) != 1) + { break; } } @@ -826,15 +826,15 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) if(Trace.isOn("regexp-fset")) { Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {"; - for (std::set<unsigned>::const_iterator itr = pcset.begin(); - itr != pcset.end(); - ++itr) + for (std::set<unsigned>::const_iterator it = pcset.begin(); + it != pcset.end(); + ++it) { - if (itr != pcset.begin()) + if (it != pcset.begin()) { Trace("regexp-fset") << ","; } - Trace("regexp-fset") << (*itr); + Trace("regexp-fset") << (*it); } Trace("regexp-fset") << "}" << std::endl; } @@ -1191,7 +1191,6 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } else if(r[0].getKind() == kind::REGEXP_SIGMA) { conc = d_true; } else { - NodeManager* nm = NodeManager::currentNM(); Node se = s.eqNode(d_emptyString); Node sinr = nm->mkNode(kind::STRING_IN_REGEXP, s, r[0]); Node sk1 = nm->mkSkolem( @@ -1495,24 +1494,25 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > } if(Trace.isOn("regexp-int-debug")) { Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {"; - for (std::vector<unsigned>::const_iterator itr = cset.begin(); - itr != cset.end(); - ++itr) + for (std::vector<unsigned>::const_iterator it = cset.begin(); + it != cset.end(); + ++it) { - if(itr != cset.begin()) { + if (it != cset.begin()) + { Trace("regexp-int-debug") << ", "; } - Trace("regexp-int-debug") << ( *itr ); + Trace("regexp-int-debug") << (*it); } Trace("regexp-int-debug") << std::endl; } std::map< PairNodes, Node > cacheX; - for (std::vector<unsigned>::const_iterator itr = cset.begin(); - itr != cset.end(); - ++itr) + for (std::vector<unsigned>::const_iterator it = cset.begin(); + it != cset.end(); + ++it) { std::vector<unsigned> cvec; - cvec.push_back(String::convertCodeToUnsignedInt(*itr)); + cvec.push_back(String::convertCodeToUnsignedInt(*it)); String c(cvec); Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl; Node r1l = derivativeSingle(r1, c); diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 5b41feacb..9d9c66ec2 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -100,15 +100,15 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) Trace("regexp-process") << "Checking Memberships ... " << std::endl; for (const std::pair<const Node, std::vector<Node> >& mr : mems) { - std::vector<Node> mems = mr.second; + std::vector<Node> mems2 = mr.second; Trace("regexp-process") << "Memberships(" << mr.first << ") = " << mr.second << std::endl; - if (!checkEqcInclusion(mems)) + if (!checkEqcInclusion(mems2)) { // conflict discovered, return return; } - if (!checkEqcIntersect(mems)) + if (!checkEqcIntersect(mems2)) { // conflict discovered, return return; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 26721229f..f05c9165b 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -195,8 +195,9 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, std::reverse( mchildren_ss.begin(), mchildren_ss.end() ); std::reverse( children_ss.begin(), children_ss.end() ); } - Node ret = simpleRegexpConsume( mchildren_ss, children_ss, t ); - if( ret.isNull() ){ + if (simpleRegexpConsume(mchildren_ss, children_ss, t) + .isNull()) + { can_skip = true; } } @@ -1252,10 +1253,13 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } case kind::REGEXP_STAR: { if( s.size() != index_start ) { - for(unsigned k=s.size() - index_start; k>0; --k) { - CVC4::String t = s.substr(index_start, k); + for (unsigned i = s.size() - index_start; i > 0; --i) + { + CVC4::String t = s.substr(index_start, i); if( testConstStringInRegExp( t, 0, r[0] ) ) { - if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) { + if (index_start + i == s.size() + || testConstStringInRegExp(s, index_start + i, r)) + { return true; } } @@ -1409,8 +1413,8 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { { nb << nm->mkNode(STRING_IN_REGEXP, xc, r); } - Node retNode = nb.constructNode(); - return returnRewrite(node, retNode, "re-in-dist-char-star"); + return returnRewrite( + node, nb.constructNode(), "re-in-dist-char-star"); } } } @@ -2245,19 +2249,19 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { if (nc2.size() > 1) { Node emp = nm->mkConst(CVC4::String("")); - NodeBuilder<> nb(kind::AND); + NodeBuilder<> nb2(kind::AND); for (const Node& n2 : nc2) { if (n2 == n) { - nb << nm->mkNode(kind::EQUAL, node[0], node[1]); + nb2 << nm->mkNode(kind::EQUAL, node[0], node[1]); } else { - nb << nm->mkNode(kind::EQUAL, emp, n2); + nb2 << nm->mkNode(kind::EQUAL, emp, n2); } } - ret = nb.constructNode(); + ret = nb2.constructNode(); } else { @@ -2770,14 +2774,14 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.replace( str.++( x, "ab" ), "a", y ) ---> // str.++( str.replace( str.++( x, "a" ), "a", y ), "b" ) // this is independent of whether the second argument may be empty - std::vector<Node> cc; - cc.push_back(NodeManager::currentNM()->mkNode( + std::vector<Node> scc; + scc.push_back(NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, utils::mkConcat(STRING_CONCAT, children0), node[1], node[2])); - cc.insert(cc.end(), ce.begin(), ce.end()); - Node ret = utils::mkConcat(STRING_CONCAT, cc); + scc.insert(scc.end(), ce.begin(), ce.end()); + Node ret = utils::mkConcat(STRING_CONCAT, scc); return returnRewrite(node, ret, "rpl-cctn"); } } @@ -2968,8 +2972,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return returnRewrite(node, node[0], "repl-repl2-inv-id"); } bool dualReplIteSuccess = false; - Node cmp_con = checkEntailContains(node[1][0], node[1][2]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { // str.contains( x, z ) ---> false // implies @@ -2983,11 +2987,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // implies // str.replace( x, str.replace( x, y, z ), w ) ---> // ite( str.contains( x, y ), x, w ) - cmp_con = checkEntailContains(node[1][1], node[1][2]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + cmp_con2 = checkEntailContains(node[1][1], node[1][2]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { - cmp_con = checkEntailContains(node[1][2], node[1][1]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + cmp_con2 = checkEntailContains(node[1][2], node[1][1]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { dualReplIteSuccess = true; } @@ -3016,8 +3020,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.contains(y, z) ----> false and ( y == w or x == w ) implies // implies // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w) - Node cmp_con = checkEntailContains(node[1][0], node[1][2]); - invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>(); + Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]); + invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>(); } } else @@ -3025,11 +3029,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.contains(x, z) ----> false and str.contains(x, w) ----> false // implies // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u) - Node cmp_con = checkEntailContains(node[0], node[1][1]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + Node cmp_con2 = checkEntailContains(node[0], node[1][1]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { - cmp_con = checkEntailContains(node[0], node[1][2]); - invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>(); + cmp_con2 = checkEntailContains(node[0], node[1][2]); + invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>(); } } if (invSuccess) @@ -3044,8 +3048,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { // str.contains( z, w ) ----> false implies // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z ) - Node cmp_con = checkEntailContains(node[1], node[2][0]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + Node cmp_con2 = checkEntailContains(node[1], node[2][0]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]); diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index c16fab4a9..21862a251 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -194,15 +194,15 @@ bool SubstitutionMinimize::findInternal(Node n, { if (cur.isVar()) { - const std::vector<Node>::const_iterator& it = + const std::vector<Node>::const_iterator& iit = std::find(vars.begin(), vars.end(), cur); - if (it == vars.end()) + if (iit == vars.end()) { value[cur] = cur; } else { - ptrdiff_t pos = std::distance(vars.begin(), it); + ptrdiff_t pos = std::distance(vars.begin(), iit); value[cur] = subs[pos]; } } diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 333f09d2d..7728456a7 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -24,10 +24,11 @@ namespace CVC4 { namespace theory { struct substitution_stack_element { - TNode node; - bool children_added; - substitution_stack_element(TNode node) - : node(node), children_added(false) {} + TNode d_node; + bool d_children_added; + substitution_stack_element(TNode node) : d_node(node), d_children_added(false) + { + } };/* struct substitution_stack_element */ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { @@ -46,7 +47,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { { // The current node we are processing substitution_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl; @@ -77,7 +78,8 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { } // Not yet substituted, so process - if (stackHead.children_added) { + if (stackHead.d_children_added) + { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -109,10 +111,12 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl; cache[current] = result; toVisit.pop_back(); - } else { + } + else + { // Mark that we have added the children if any if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the operator, if any if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { TNode opNode = current.getOperator(); diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 6a404104f..2b6a847dc 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -88,9 +88,9 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { // The current theory has already visited it, so now it depends on the parent and the type if (Theory::setContains(parentTheoryId, visitedTheories)) { if (useType) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); - d_theories = Theory::setInsert(typeTheoryId, d_theories); - return Theory::setContains(typeTheoryId, visitedTheories); + TheoryId typeTheoryId2 = Theory::theoryOf(current.getType()); + d_theories = Theory::setInsert(typeTheoryId2, d_theories); + return Theory::setContains(typeTheoryId2, visitedTheories); } else { return true; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e15641bb4..a39c014a6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -470,17 +470,22 @@ void TheoryEngine::printAssertions(const char* tag) { if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { Trace(tag) << "--------------------------------------------" << endl; Trace(tag) << "Assertions of " << theory->getId() << ": " << endl; - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - if ((*it).d_isPreregistered) - { - Trace(tag) << "[" << i << "]: "; - } - else + { + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), + it_end = + theory->facts_end(); + for (unsigned i = 0; it != it_end; ++it, ++i) { - Trace(tag) << "(" << i << "): "; + if ((*it).d_isPreregistered) + { + Trace(tag) << "[" << i << "]: "; + } + else + { + Trace(tag) << "(" << i << "): "; + } + Trace(tag) << (*it).d_assertion << endl; } - Trace(tag) << (*it).d_assertion << endl; } if (d_logicInfo.isSharingEnabled()) { @@ -1146,8 +1151,7 @@ void TheoryEngine::preprocessStart() struct preprocess_stack_element { TNode node; bool children_added; - preprocess_stack_element(TNode node) - : node(node), children_added(false) {} + preprocess_stack_element(TNode n) : node(n), children_added(false) {} };/* struct preprocess_stack_element */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 399695131..bf0a82a20 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -267,9 +267,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // choice z. P(z). Node v = nm->mkBoundVar(n.getType()); Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - Node ret = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); - d_modelCache[n] = ret; - return ret; + Node answer = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); + d_modelCache[n] = answer; + return answer; } // must rewrite the term at this point ret = Rewriter::rewrite(n); @@ -315,11 +315,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const { if (d_enableFuncModels) { - std::map<Node, Node>::const_iterator it = d_uf_models.find(n); - if (it != d_uf_models.end()) + std::map<Node, Node>::const_iterator entry = d_uf_models.find(n); + if (entry != d_uf_models.end()) { // Existing function - ret = it->second; + ret = entry->second; d_modelCache[n] = ret; return ret; } @@ -327,7 +327,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // constant in the enumeration of the range type vector<TypeNode> argTypes = t.getArgTypes(); vector<Node> args; - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = argTypes.size(); i < size; ++i) { args.push_back(nm->mkBoundVar(argTypes[i])); diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index a96f29ada..68ad25490 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -736,7 +736,6 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } #endif - set<Node>* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); if (!assignOne) { @@ -755,6 +754,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) bool assignable, evaluable CVC4_UNUSED; std::map<Node, Assigner>::iterator itAssigner; std::map<Node, Node>::iterator itAssignerM; + set<Node>* repSet = typeRepSet.getSet(t); for (i = noRepSet.begin(); i != noRepSet.end();) { i2 = i; @@ -928,11 +928,10 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { set<Node>& noRepSet = TypeSet::getSet(it); - set<Node>::iterator i; - for (i = noRepSet.begin(); i != noRepSet.end(); ++i) + for (const Node& node : noRepSet) { - tm->d_reps[*i] = *i; - tm->d_rep_set.add((*i).getType(), *i); + tm->d_reps[node] = node; + tm->d_rep_set.add(node.getType(), node); } } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 63aa81097..479e3400d 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1002,15 +1002,22 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { std::vector<std::shared_ptr<EqProof>> orderedChildren; bool nullCongruenceFound = false; - for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { - if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && - eqpc->d_children[i]->d_node.isNull()) { + for (const auto& child : eqpc->d_children) + { + if (child->d_id == eq::MERGED_THROUGH_CONGRUENCE + && child->d_node.isNull()) + { nullCongruenceFound = true; - Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; - orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); - orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); - } else { - orderedChildren.push_back(eqpc->d_children[i]); + Debug("pf::ee") + << "Have congruence with empty d_node. Splitting..." + << std::endl; + orderedChildren.insert(orderedChildren.begin(), + child->d_children[0]); + orderedChildren.push_back(child->d_children[1]); + } + else + { + orderedChildren.push_back(child); } } @@ -1935,11 +1942,12 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; - Theory::Set tags = newSetTags; + Theory::Set tags2 = newSetTags; TheoryId current; - while ((current = Theory::setPop(tags)) != THEORY_LAST) { + while ((current = Theory::setPop(tags2)) != THEORY_LAST) + { // Remove from the tags - tags = Theory::setRemove(current, tags); + tags2 = Theory::setRemove(current, tags2); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = current == tag ? eqNodeId : triggerSet.d_triggers[i++]; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 6d6f49c7f..23b7b9217 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -336,8 +336,8 @@ unsigned HoExtension::checkAppCompletion() { if (n[k].getType().isFunction()) { - TNode rop = ee->getRepresentative(n[k]); - curr_rops[rop] = true; + TNode rop2 = ee->getRepresentative(n[k]); + curr_rops[rop2] = true; } } } diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 49ceebfd6..27d045120 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -400,18 +400,17 @@ void SymmetryBreaker::assertFormula(TNode phi) { } } unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); - for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); - i != ps.end(); - ++i) { - Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; - set<TNode>& p = (*i).second; + for (auto& kv : ps) + { + Debug("ufsymm") << "UFSYMM partition*: " << kv.first; + set<TNode>& p = kv.second; for(set<TNode>::iterator j = p.begin(); j != p.end(); ++j) { Debug("ufsymm") << " " << *j; } Debug("ufsymm") << endl; - p.insert((*i).first); + p.insert(kv.first); Permutations::iterator pi = d_permutations.find(p); if(pi == d_permutations.end()) { d_permutations.insert(p); @@ -473,11 +472,9 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { } } - for(Permutations::iterator i = d_permutations.begin(); - i != d_permutations.end(); - ++i) { + for (const Permutation& p : d_permutations) + { ++(d_stats.d_permutationSetsConsidered); - const Permutation& p = *i; Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; size_t n = p.size() - 1; if(invariantByPermutations(p)) { @@ -529,11 +526,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { if(i != p.end() || p.size() != cts.size()) { Debug("ufsymm") << "UFSYMM cts != p" << endl; NodeBuilder<> disj(kind::OR); - for(set<Node>::const_iterator i = cts.begin(); - i != cts.end(); - ++i) { - if(t != *i) { - disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i); + NodeManager* nm = NodeManager::currentNM(); + for (const Node& nn : cts) + { + if (t != nn) + { + disj << nm->mkNode(kind::EQUAL, t, nn); } } Node d; @@ -596,20 +594,29 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.push_back(p1); repls.push_back(p1); repls.push_back(p0); - for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { - Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + for (const Node nn : d_phi) + { + Node s = + nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); Node n = norm(s); - if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { - Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl - << "UFSYMM because this node: " << *i << endl - << "UFSYMM rewrite-norms to : " << n << endl - << "UFSYMM which is not in our set of normalized assertions" << endl; + if (nn != n && d_phiSet.find(n) == d_phiSet.end()) + { + Debug("ufsymm") + << "UFSYMM P_swap is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << nn << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; return false; - } else if(Debug.isOn("ufsymm:p")) { - if(*i == s) { - Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl; - } else { - Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl + } + else if (Debug.isOn("ufsymm:p")) + { + if (nn == s) + { + Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << nn << endl; + } + else + { + Debug("ufsymm:p") << "UFSYMM P_swap passes: " << nn << endl << "UFSYMM rewrites: " << s << endl << "UFSYMM norms: " << n << endl; } @@ -622,30 +629,41 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.clear(); repls.clear(); bool first = true; - for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) { - subs.push_back(*i); + for (const Node& nn : p) + { + subs.push_back(nn); if(!first) { - repls.push_back(*i); + repls.push_back(nn); } else { first = false; } } repls.push_back(*p.begin()); Assert(subs.size() == repls.size()); - for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { - Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + for (const Node& nn : d_phi) + { + Node s = + nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); Node n = norm(s); - if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { - Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl - << "UFSYMM because this node: " << *i << endl - << "UFSYMM rewrite-norms to : " << n << endl - << "UFSYMM which is not in our set of normalized assertions" << endl; + if (nn != n && d_phiSet.find(n) == d_phiSet.end()) + { + Debug("ufsymm") + << "UFSYMM P_circ is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << nn << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" + << endl; return false; - } else if(Debug.isOn("ufsymm:p")) { - if(*i == s) { - Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl; - } else { - Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl + } + else if (Debug.isOn("ufsymm:p")) + { + if (nn == s) + { + Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << nn << endl; + } + else + { + Debug("ufsymm:p") << "UFSYMM P_circ passes: " << nn << endl << "UFSYMM rewrites: " << s << endl << "UFSYMM norms: " << n << endl; } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index ffe3730c4..d667aea7e 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -153,14 +153,20 @@ void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ } } //now see if any children can be removed, and simplify the ones that cannot - for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( !it->first.isNull() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( it->first ); - }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); - if( it->second.isEmpty() ){ - eraseData.push_back( it->first ); + for (auto& kv : d_data) + { + if (!kv.first.isNull()) + { + if (!defaultVal.isNull() && kv.second.d_value == defaultVal) + { + eraseData.push_back(kv.first); + } + else + { + kv.second.simplify(op, defaultVal, argIndex + 1); + if (kv.second.isEmpty()) + { + eraseData.push_back(kv.first); } } } |