diff options
Diffstat (limited to 'src/theory/arith')
26 files changed, 264 insertions, 292 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index ea349a383..6b277a10a 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -85,7 +85,9 @@ struct VirtualBound { , d(coeff) , y(bounding) , c(orig) - { Assert(k == kind::LEQ || k == kind::GEQ); } + { + Assert(k == kind::LEQ || k == kind::GEQ); + } }; struct CutScratchPad { @@ -621,8 +623,6 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& v, TreeLog& l, ApproximateStatistic Assert(numRows > 0); Assert(numCols > 0); - - glp_add_rows(d_inputProb, numRows); glp_add_cols(d_inputProb, numCols); @@ -994,7 +994,7 @@ ApproxGLPK::~ApproxGLPK(){ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const { Assert(d_solvedRelaxation); - Assert(!mip || d_solvedMIP); + Assert(!mip || d_solvedMIP); ApproximateSimplex::Solution sol; DenseSet& newBasis = sol.newBasis; @@ -1737,8 +1737,6 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){ } } - - // Node explainSet(const set<ConstraintP>& inp){ // Assert(!inp.empty()); // NodeBuilder<> nb(kind::AND); @@ -2434,7 +2432,7 @@ bool ApproxGLPK::replaceSlacksOnCuts(){ ArithVar x = *iter; SlackReplace rep = d_pad.d_slacks[x]; if(d_vars.isIntegerInput(x)){ - Assert(rep == SlackLB || rep == SlackUB); + Assert(rep == SlackLB || rep == SlackUB); Rational& a = cut.get(x); const DeltaRational& bound = (rep == SlackLB) ? @@ -2835,7 +2833,7 @@ bool ApproxGLPK::gaussianElimConstructTableRow(int nid, int M, const PrimitiveVe // r_p : 0 = -1 * other + sum a_i x_i // rid : 0 = e * other + sum b_i x_i // rid += e * r_p - // : 0 = 0 * other + ... + // : 0 = 0 * other + ... Assert(!e.getCoefficient().isZero()); Rational cp = e.getCoefficient(); diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 454d6c11f..3930d7359 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -390,8 +390,8 @@ Node ArithIteUtils::findIteCnd(TNode tb, TNode fb) const{ bool ArithIteUtils::solveBinOr(TNode binor){ Assert(binor.getKind() == kind::OR); Assert(binor.getNumChildren() == 2); - Assert(binor[0].getKind() == kind::EQUAL); - Assert(binor[1].getKind() == kind::EQUAL); + Assert(binor[0].getKind() == kind::EQUAL); + Assert(binor[1].getKind() == kind::EQUAL); //Node n = Node n = applySubstitutions(binor); @@ -411,8 +411,8 @@ bool ArithIteUtils::solveBinOr(TNode binor){ TNode l = n[0]; TNode r = n[1]; - Assert(l.getKind() == kind::EQUAL); - Assert(r.getKind() == kind::EQUAL); + Assert(l.getKind() == kind::EQUAL); + Assert(r.getKind() == kind::EQUAL); Debug("arith::ite") << "bin or " << n << endl; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 86e5b3195..c8a03fab1 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -50,7 +50,7 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){ } RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ - Assert(t.getKind()== kind::MINUS); + Assert(t.getKind() == kind::MINUS); if(pre){ if(t[0] == t[1]){ @@ -70,7 +70,7 @@ RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ } RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ - Assert(t.getKind()== kind::UMINUS); + Assert(t.getKind() == kind::UMINUS); if(t[0].getKind() == kind::CONST_RATIONAL){ Rational neg = -(t[0].getConst<Rational>()); @@ -143,8 +143,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return RewriteResponse(REWRITE_DONE, t); case kind::PI: return RewriteResponse(REWRITE_DONE, t); - default: - Unhandled(k); + default: Unhandled() << k; } } } @@ -263,7 +262,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ RewriteResponse ArithRewriter::preRewriteMult(TNode t){ - Assert(t.getKind()== kind::MULT || t.getKind()== kind::NONLINEAR_MULT); + Assert(t.getKind() == kind::MULT || t.getKind() == kind::NONLINEAR_MULT); if(t.getNumChildren() == 2){ if(t[0].getKind() == kind::CONST_RATIONAL @@ -321,7 +320,7 @@ static Node flatten(Kind k, TNode t){ } RewriteResponse ArithRewriter::preRewritePlus(TNode t){ - Assert(t.getKind()== kind::PLUS); + Assert(t.getKind() == kind::PLUS); if(canFlatten(kind::PLUS, t)){ return RewriteResponse(REWRITE_DONE, flatten(kind::PLUS, t)); @@ -331,7 +330,7 @@ RewriteResponse ArithRewriter::preRewritePlus(TNode t){ } RewriteResponse ArithRewriter::postRewritePlus(TNode t){ - Assert(t.getKind()== kind::PLUS); + Assert(t.getKind() == kind::PLUS); std::vector<Monomial> monomials; std::vector<Polynomial> polynomials; @@ -357,7 +356,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t){ } RewriteResponse ArithRewriter::postRewriteMult(TNode t){ - Assert(t.getKind()== kind::MULT || t.getKind()==kind::NONLINEAR_MULT); + Assert(t.getKind() == kind::MULT || t.getKind() == kind::NONLINEAR_MULT); Polynomial res = Polynomial::mkOne(); @@ -462,7 +461,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { pi_factor, nm->mkNode(kind::MULT, ntwo, ra_div_two)); }else{ - Assert( r.sgn()==-1 ); + Assert(r.sgn() == -1); new_pi_factor = nm->mkNode(kind::PLUS, pi_factor, @@ -671,7 +670,7 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ } RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){ - Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind()== kind::DIVISION); + Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind() == kind::DIVISION); Node left = t[0]; Node right = t[1]; diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 2138b513e..e17605ead 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -163,8 +163,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ if(t == cleft && e == cright){ // t == cleft && e == cright - Assert( t == cleft ); - Assert( e == cright ); + Assert(t == cleft); + Assert(e == cright); switch(k){ case LT: // (ite (< x y) x y) case LEQ: { // (ite (<= x y) x y) @@ -270,9 +270,7 @@ void ArithStaticLearner::addBound(TNode n) { Debug("arith::static") << "adding bound " << n << endl; } break; - default: - Unhandled(k); - break; + default: Unhandled() << k; break; } } diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 4588a5848..d737fefeb 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -207,10 +207,8 @@ inline Node negateConjunctionAsClause(TNode conjunction){ } inline Node maybeUnaryConvert(NodeBuilder<>& builder){ - Assert(builder.getKind() == kind::OR || - builder.getKind() == kind::AND || - builder.getKind() == kind::PLUS || - builder.getKind() == kind::MULT); + Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND + || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT); Assert(builder.getNumChildren() >= 1); if(builder.getNumChildren() == 1){ return builder[0]; diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index f269847de..8173f2cea 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -138,7 +138,7 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) return Result::UNSAT; } } - Assert( d_conflictVariables.empty() ); + Assert(d_conflictVariables.empty()); if(d_errorSet.errorEmpty()){ return Result::SAT; diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 7bd69190e..43fa4e437 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -20,7 +20,7 @@ #include <stdint.h> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "theory/arith/arithvar.h" #include "util/dense_map.h" @@ -66,7 +66,7 @@ public: } inline BoundCounts operator-(BoundCounts bc) const { - Assert( *this >= bc ); + Assert(*this >= bc); return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount, d_upperBoundCount - bc.d_upperBoundCount); } diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index a11dd729b..158a81e8d 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -93,13 +93,13 @@ void FarkasConflictBuilder::reset(){ /* Adds a constraint to the constraint under construction. */ void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){ - Assert(!PROOF_ON() || - (!underConstruction() && d_constraints.empty() && d_farkas.empty()) || - (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); + Assert( + !PROOF_ON() + || (!underConstruction() && d_constraints.empty() && d_farkas.empty()) + || (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); Assert(PROOF_ON() || d_farkas.empty()); Assert(c->isTrue()); - if(d_consequent == NullConstraint){ d_consequent = c; } else { @@ -136,7 +136,7 @@ void FarkasConflictBuilder::makeLastConsequent(){ d_consequentSet = true; } - Assert(! d_consequent->negationHasProof() ); + Assert(!d_consequent->negationHasProof()); Assert(d_consequentSet); } @@ -144,9 +144,10 @@ void FarkasConflictBuilder::makeLastConsequent(){ ConstraintCP FarkasConflictBuilder::commitConflict(){ Assert(underConstruction()); Assert(!d_constraints.empty()); - Assert(!PROOF_ON() || - (!underConstruction() && d_constraints.empty() && d_farkas.empty()) || - (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); + Assert( + !PROOF_ON() + || (!underConstruction() && d_constraints.empty() && d_farkas.empty()) + || (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); Assert(PROOF_ON() || d_farkas.empty()); Assert(d_consequentSet); @@ -156,7 +157,7 @@ ConstraintCP FarkasConflictBuilder::commitConflict(){ reset(); Assert(!underConstruction()); - Assert( not_c->inConflict() ); + Assert(not_c->inConflict()); Assert(!d_consequentSet); return not_c; } diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index ce45141ef..5a6bf6f31 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -489,7 +489,7 @@ bool ArithCongruenceManager::fixpointInfer() { explain( eq_exp, assumptions ); }else{ //eq_exp should be true - Assert( eq_exp==d_true ); + Assert(eq_exp == d_true); } Node req_exp; if( assumptions.empty() ){ diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index c7251d4c4..e7b1289a4 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -63,8 +63,7 @@ ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){ return Equality; case DISTINCT: return Disequality; - default: - Unhandled(k); + default: Unhandled() << k; } } @@ -322,20 +321,11 @@ void ValueCollection::add(ConstraintP c){ ConstraintP ValueCollection::getConstraintOfType(ConstraintType t) const{ switch(t){ - case LowerBound: - Assert(hasLowerBound()); - return d_lowerBound; - case Equality: - Assert(hasEquality()); - return d_equality; - case UpperBound: - Assert(hasUpperBound()); - return d_upperBound; - case Disequality: - Assert(hasDisequality()); - return d_disequality; - default: - Unreachable(); + case LowerBound: Assert(hasLowerBound()); return d_lowerBound; + case Equality: Assert(hasEquality()); return d_equality; + case UpperBound: Assert(hasUpperBound()); return d_upperBound; + case Disequality: Assert(hasDisequality()); return d_disequality; + default: Unreachable(); } } @@ -613,7 +603,7 @@ void ConstraintRule::print(std::ostream& out) const { out << "_"; } out << " * (" << *antecedent << ")" << std::endl; - + Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0); --p; coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffIterator-1 : 0; @@ -862,7 +852,8 @@ ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, cons pair<SortedConstraintMapIterator, bool> negInsertAttempt; negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection())); Assert(negInsertAttempt.second - || ! negInsertAttempt.first->second.hasConstraintOfType(negC->getType())); + || !negInsertAttempt.first->second.hasConstraintOfType( + negC->getType())); negPos = negInsertAttempt.first; } @@ -1108,7 +1099,7 @@ void Constraint::setAssumption(bool nowInConflict){ Assert(assertedToTheTheory()); d_database->pushConstraintRule(ConstraintRule(this, AssumeAP)); - + Assert(inConflict() == nowInConflict); if(Debug.isOn("constraint::conflictCommit") && inConflict()){ Debug("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl; @@ -1149,7 +1140,6 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){ Assert(imp->hasProof()); Assert(negationHasProof() == nowInConflict); - d_database->d_antecedents.push_back(NullConstraint); d_database->d_antecedents.push_back(imp); @@ -1283,7 +1273,7 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef Assert(negationHasProof() == nowInConflict); Assert(allHaveProof(a)); - Assert( PROOF_ON() == (coeffs != RationalVectorCPSentinel) ); + Assert(PROOF_ON() == (coeffs != RationalVectorCPSentinel)); // !PROOF_ON() => coeffs == RationalVectorCPSentinel // PROOF_ON() => coeffs->size() == a.size() + 1 Assert(!PROOF_ON() || coeffs->size() == a.size() + 1); @@ -1404,7 +1394,8 @@ void Constraint::assertionFringe(ConstraintCPVec& v){ v[writePos] = vi; writePos++; }else{ - Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof() || vi->hasIntHoleProof() ); + Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof() + || vi->hasIntHoleProof()); AntecedentId p = vi->getEndAntecedent(); ConstraintCP antecedent = antecedents[p]; @@ -1561,7 +1552,7 @@ ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool assert ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const { Assert(variableDatabaseIsSetup(v)); - Assert(t == UpperBound || t == LowerBound); + Assert(t == UpperBound || t == LowerBound); SortedConstraintMap& scm = getVariableSCM(v); if(t == UpperBound){ diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 831c631f8..7fd4e2031 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -21,8 +21,8 @@ #include <ostream> +#include "base/check.h" #include "base/exception.h" -#include "base/cvc4_assert.h" #include "util/integer.h" #include "util/rational.h" diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index b30dc515b..11cf55354 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -279,7 +279,6 @@ void DioSolver::enqueueInputConstraints(){ void DioSolver::moveMinimumByAbsToQueueFront(){ Assert(!queueEmpty()); - //Select the minimum element. size_t indexInQueue = 0; Monomial minMonomial = d_trail[d_currentF[indexInQueue]].d_minimalMonomial; @@ -399,7 +398,12 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ Debug("arith::dio") << "extendedReduction combine" << endl; TrailIndex next = combineEqAtIndexes(current, s, inQueue, t); - Assert(d_trail[next].d_eq.getPolynomial().getCoefficient(vl).getValue().getNumerator() == g); + Assert(d_trail[next] + .d_eq.getPolynomial() + .getCoefficient(vl) + .getValue() + .getNumerator() + == g); current = next; currentCoeff = g; @@ -633,7 +637,8 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::solveIndex(DioS d_subs.push_back(Substitution(Node::null(), var, ci)); Debug("arith::dio") << "after solveIndex " << d_trail[ci].d_eq.getNode() << " for " << av.getNode() << endl; - Assert(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl) == Constant::mkConstant(-1)); + Assert(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl) + == Constant::mkConstant(-1)); return make_pair(subBy, i); } @@ -690,7 +695,8 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex( Debug("arith::dio") << "Decompose ci(" << ci <<":" << d_trail[ci].d_eq.getNode() << ") for " << d_trail[i].d_minimalMonomial.getNode() << endl; - Assert(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl) == Constant::mkConstant(-1)); + Assert(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl) + == Constant::mkConstant(-1)); SumPair newFact = r + fresh_a; @@ -717,7 +723,10 @@ DioSolver::TrailIndex DioSolver::applySubstitution(DioSolver::SubIndex si, DioSo if(!a.isZero()){ Integer one(1); TrailIndex afterSub = combineEqAtIndexes(ti, one, subIndex, a.getValue().getNumerator()); - Assert(d_trail[afterSub].d_eq.getPolynomial().getCoefficient(VarList(var)).isZero()); + Assert(d_trail[afterSub] + .d_eq.getPolynomial() + .getCoefficient(VarList(var)) + .isZero()); return afterSub; }else{ return ti; diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 0c26f9c55..fa6c08696 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -74,7 +74,8 @@ private: NodeToInputConstraintIndexMap d_varToInputConstraintMap; Node proofVariableToReason(const Variable& v) const{ - Assert(d_varToInputConstraintMap.find(v.getNode()) != d_varToInputConstraintMap.end()); + Assert(d_varToInputConstraintMap.find(v.getNode()) + != d_varToInputConstraintMap.end()); InputConstraintIndex pos = (*(d_varToInputConstraintMap.find(v.getNode()))).second; Assert(pos < d_inputConstraints.size()); return d_inputConstraints[pos].d_reason; diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 8839739a2..9e3e7c630 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -152,8 +152,16 @@ public: inline ArithVar getVariable() const { return d_variable; } bool isRelaxed() const { return d_relaxed; } - void setRelaxed(){ Assert(!d_relaxed); d_relaxed = true; } - void setUnrelaxed(){ Assert(d_relaxed); d_relaxed = false; } + void setRelaxed() + { + Assert(!d_relaxed); + d_relaxed = true; + } + void setUnrelaxed() + { + Assert(d_relaxed); + d_relaxed = false; + } inline int sgn() const { return d_sgn; } diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 827323302..29177d3f4 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -118,8 +118,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ }else if(d_errorSet.errorEmpty()){ //if(verbose){ Message() << "fcFindModel("<< instance <<") fixed itself" << endl; } Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; - if(verbose) - Assert(!d_errorSet.moreSignals()); + if (verbose) Assert(!d_errorSet.moreSignals()); Assert(d_conflictVariables.empty()); return Result::SAT; } @@ -264,7 +263,7 @@ WitnessImprovement FCSimplexDecisionProcedure::adjustFocusShrank(const ArithVarV WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){ // uint32_t newErrorSize = d_errorSet.errorSize(); // uint32_t newFocusSize = d_errorSet.focusSize(); - Assert(d_focusSize == d_errorSet.focusSize()); + Assert(d_focusSize == d_errorSet.focusSize()); Assert(d_focusSize > 1); Assert(d_errorSet.inFocus(v)); @@ -558,7 +557,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit int prevFocusSgn = d_errorSet.popSignal(); if(d_tableau.isBasic(updated)){ - Assert(!d_variables.assignmentIsConsistent(updated) == d_errorSet.inError(updated)); + Assert(!d_variables.assignmentIsConsistent(updated) + == d_errorSet.inError(updated)); if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);} if(!d_variables.assignmentIsConsistent(updated)){ if(checkBasicForConflict(updated)){ @@ -582,7 +582,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } - Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize())); + Assert( + debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize())); adjustFocusAndError(selected, focusChanges); } @@ -729,7 +730,6 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ Assert(d_conflictVariables.empty()); Assert(d_focusErrorVar == ARITHVAR_SENTINEL); - d_scores.purge(); d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); @@ -752,8 +752,8 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ d_focusSize = d_errorSet.focusSize(); - Assert( d_errorSize == d_focusSize); - Assert( d_errorSize >= 1 ); + Assert(d_errorSize == d_focusSize); + Assert(d_errorSize >= 1); d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer); @@ -795,7 +795,8 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ if(verbose){ debugDualLike(w, Message(), instance, prevFocusSize, prevErrorSize); } - Assert(debugDualLike(w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); + Assert(debugDualLike( + w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize)); } diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 7f729751b..8c7d22088 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -365,7 +365,6 @@ void LinearEqualityModule::debugCheckTracking(){ << "computed " << computed << " tracking " << d_btracking[ridx] << endl; Assert(computed == d_btracking[ridx]); - } } } @@ -574,12 +573,10 @@ void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bo Assert(sgn != 0); bool selectUb = rowUp ? (sgn > 0) : (sgn < 0); - Assert( nonbasic != v || - ( rowUp && a_ij.sgn() > 0 && c->isLowerBound()) || - ( rowUp && a_ij.sgn() < 0 && c->isUpperBound()) || - (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) || - (!rowUp && a_ij.sgn() < 0 && c->isLowerBound()) - ); + Assert(nonbasic != v || (rowUp && a_ij.sgn() > 0 && c->isLowerBound()) + || (rowUp && a_ij.sgn() < 0 && c->isUpperBound()) + || (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) + || (!rowUp && a_ij.sgn() < 0 && c->isLowerBound())); if(Debug.isOn("arith::propagateRow")){ if(nonbasic == v){ @@ -743,7 +740,7 @@ ConstraintCP LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithV fcs.addConstraint(c, coeff, adjustSgn); if(basicVar == v){ - Assert(! c->negationHasProof() ); + Assert(!c->negationHasProof()); fcs.makeLastConsequent(); } } @@ -1400,8 +1397,8 @@ void LinearEqualityModule::pop_block(BorderHeap& heap, int& brokenInBlock, int& heap.pop_heap(); }else{ // does not belong to the block - Assert((heap.direction() > 0) ? - (blockValue < top.d_diff) : (blockValue > top.d_diff)); + Assert((heap.direction() > 0) ? (blockValue < top.d_diff) + : (blockValue > top.d_diff)); break; } } diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 02b8dc194..c845ccb05 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -478,7 +478,6 @@ protected: Assert(newEntry.getCoefficient() != 0); - ++d_entriesInUse; d_rows[row].insert(newId); @@ -650,7 +649,6 @@ public: Assert(mult != 0); - RowIterator i = getRow(to).begin(); RowIterator i_end = getRow(to).end(); while(i != i_end){ @@ -710,7 +708,6 @@ public: Assert(mult != 0); - RowIterator i = getRow(to).begin(); RowIterator i_end = getRow(to).end(); while(i != i_end){ diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 4747727c8..839520c0b 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -975,7 +975,7 @@ bool NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s) { Trace("nl-ext-model") << "...ERROR: already has value." << std::endl; // this should never happen since substitutions should be applied eagerly - Assert( false ); + Assert(false); return false; } // if we previously had an approximate bound, the exact bound should be in its @@ -1876,8 +1876,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, /* //mark processed if has a "one" factor (will look at reduced monomial) std::map< Node, std::map< Node, unsigned > >::iterator itme = - d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node, - unsigned >::iterator itme2 = itme->second.begin(); itme2 != + d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< + Node, unsigned >::iterator itme2 = itme->second.begin(); itme2 != itme->second.end(); ++itme2 ){ Node v = itme->first; Assert( d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if( mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true; @@ -1957,7 +1957,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } else { - Assert( false ); + Assert(false); } } // initialize pi if necessary @@ -2669,7 +2669,7 @@ void NonlinearExtension::printModelValue(const char* c, int NonlinearExtension::compare_value(Node i, Node j, unsigned orderType) const { Assert(orderType >= 0 && orderType <= 3); - Assert( i.isConst() && j.isConst() ); + Assert(i.isConst() && j.isConst()); Trace("nl-ext-debug") << "compare value " << i << " " << j << ", o = " << orderType << std::endl; int ret; @@ -2725,8 +2725,8 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, Node av = d_m_vlist[a][a_index]; unsigned aexp = d_m_exp[a][av]; // take current sign in model - Assert( d_mv[1].find(av) != d_mv[0].end() ); - Assert( d_mv[1][av].isConst() ); + Assert(d_mv[1].find(av) != d_mv[0].end()); + Assert(d_mv[1][av].isConst()); int sgn = d_mv[1][av].getConst<Rational>().sgn(); Trace("nl-ext-debug") << "Process var " << av << "^" << aexp << ", model sign = " << sgn << std::endl; @@ -3032,7 +3032,7 @@ std::vector<Node> NonlinearExtension::checkMonomialMagnitude( unsigned c ) { // compare magnitude against variables for (unsigned k = 0; k < d_ms_vars.size(); k++) { Node v = d_ms_vars[k]; - Assert( d_mv[0].find( v )!=d_mv[0].end() ); + Assert(d_mv[0].find(v) != d_mv[0].end()); if( d_mv[0][v].isConst() ){ std::vector<Node> exp; NodeMultiset a_exp_proc; @@ -3185,7 +3185,7 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { Node curr_v = p<=1 ? a_v_c : b_v_c; if( prevRefine ){ Node pt_v = d_tangent_val_bound[p][a][b]; - Assert( !pt_v.isNull() ); + Assert(!pt_v.isNull()); if( curr_v!=pt_v ){ Node do_extend = nm->mkNode((p == 1 || p == 3) ? GT : LT, curr_v, pt_v); @@ -3424,8 +3424,8 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( Kind type = itcr->second; for (unsigned j = 0; j < itm->second.size(); j++) { Node y = itm->second[j]; - Assert(d_m_contain_mult[x].find(y) != - d_m_contain_mult[x].end()); + Assert(d_m_contain_mult[x].find(y) + != d_m_contain_mult[x].end()); Node mult = d_m_contain_mult[x][y]; // x <k> t => m*x <k'> t where y = m*x // get the sign of mult @@ -3583,7 +3583,7 @@ std::vector<Node> NonlinearExtension::checkFactoring( poly.push_back(NodeManager::currentNM()->mkNode(MULT, x, kf)); std::map<Node, std::vector<Node> >::iterator itfo = factor_to_mono_orig.find(x); - Assert( itfo!=factor_to_mono_orig.end() ); + Assert(itfo != factor_to_mono_orig.end()); for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ if( std::find( itfo->second.begin(), itfo->second.end(), itm->first )==itfo->second.end() ){ poly.push_back(ArithMSum::mkCoeffTerm( @@ -3781,7 +3781,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() { Kind k = tfl.first; for (const Node& t : tfl.second) { - Assert( d_mv[1].find( t )!=d_mv[1].end() ); + Assert(d_mv[1].find(t) != d_mv[1].end()); //initial refinements if( d_tf_initial_refine.find( t )==d_tf_initial_refine.end() ){ d_tf_initial_refine[t] = true; @@ -3921,10 +3921,10 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { for (unsigned i = 0; i < sorted_tf_args[k].size(); i++) { Node targ = sorted_tf_args[k][i]; - Assert( d_mv[1].find( targ )!=d_mv[1].end() ); + Assert(d_mv[1].find(targ) != d_mv[1].end()); Trace("nl-ext-tf-mono") << " " << targ << " -> " << d_mv[1][targ] << std::endl; Node t = tf_arg_to_term[k][targ]; - Assert( d_mv[1].find( t )!=d_mv[1].end() ); + Assert(d_mv[1].find(t) != d_mv[1].end()); Trace("nl-ext-tf-mono") << " f-val : " << d_mv[1][t] << std::endl; } std::vector< Node > mpoints; @@ -3947,7 +3947,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { Node mpv; if( !mpoints[i].isNull() ){ mpv = computeModelValue( mpoints[i], 1 ); - Assert( mpv.isConst() ); + Assert(mpv.isConst()); } mpoints_vals.push_back( mpv ); } @@ -3959,14 +3959,14 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { for (unsigned i = 0, size = sorted_tf_args[k].size(); i < size; i++) { Node sarg = sorted_tf_args[k][i]; - Assert( d_mv[1].find( sarg )!=d_mv[1].end() ); + Assert(d_mv[1].find(sarg) != d_mv[1].end()); Node sargval = d_mv[1][sarg]; - Assert( sargval.isConst() ); + Assert(sargval.isConst()); Node s = tf_arg_to_term[k][ sarg ]; - Assert( d_mv[1].find( s )!=d_mv[1].end() ); + Assert(d_mv[1].find(s) != d_mv[1].end()); Node sval = d_mv[1][s]; - Assert( sval.isConst() ); - + Assert(sval.isConst()); + //increment to the proper monotonicity region bool increment = true; while (increment && mdir_index < mpoints.size()) @@ -3976,7 +3976,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { increment = true; }else{ Node pval = mpoints_vals[mdir_index]; - Assert( pval.isConst() ); + Assert(pval.isConst()); if( sargval.getConst<Rational>() < pval.getConst<Rational>() ){ increment = true; Trace("nl-ext-tf-mono") << "...increment at " << sarg << " since model value is less than " << mpoints[mdir_index] << std::endl; @@ -4017,7 +4017,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { } if( !mono_lem.isNull() ){ if( !mono_bounds[0].isNull() ){ - Assert( !mono_bounds[1].isNull() ); + Assert(!mono_bounds[1].isNull()); mono_lem = NodeManager::currentNM()->mkNode( IMPLIES, NodeManager::currentNM()->mkNode( diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index ee298bc66..c0658b9af 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -69,11 +69,7 @@ bool Variable::isLeafMember(Node n){ (Theory::isLeafOf(n, theory::THEORY_ARITH)); } -VarList::VarList(Node n) - : NodeWrapper(n) -{ - Assert(isSorted(begin(), end())); -} +VarList::VarList(Node n) : NodeWrapper(n) { Assert(isSorted(begin(), end())); } bool Variable::isDivMember(Node n){ switch(n.getKind()){ @@ -275,11 +271,13 @@ Monomial Monomial::operator*(const Monomial& mono) const { return Monomial::mkMonomial(newConstant, newVL); } -// vector<Monomial> Monomial::sumLikeTerms(const std::vector<Monomial> & monos) { +// vector<Monomial> Monomial::sumLikeTerms(const std::vector<Monomial> & monos) +// { // Assert(isSorted(monos)); // vector<Monomial> outMonomials; // typedef vector<Monomial>::const_iterator iterator; -// for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;) { +// for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;) +// { // Rational constant = (*rangeIter).getConstant().getValue(); // VarList varList = (*rangeIter).getVarList(); // ++rangeIter; @@ -334,7 +332,7 @@ void Monomial::combineAdjacentMonomials(std::vector<Monomial>& monos) { writePos++; } } - Assert(rangeEnd>readPos); + Assert(rangeEnd > readPos); readPos = rangeEnd; } if(writePos > 0 ){ @@ -526,7 +524,7 @@ Integer Polynomial::numeratorGCD() const { //We'll use the standardization that gcd(0, 0) = 0 //So that the gcd of the zero polynomial is gcd{0} = 0 iterator i=begin(), e=end(); - Assert(i!=e); + Assert(i != e); Integer d = (*i).getConstant().getValue().getNumerator().abs(); if(d.isOne()){ @@ -683,13 +681,7 @@ SumPair SumPair::mkSumPair(const Polynomial& p){ } } -Comparison::Comparison(TNode n) - : NodeWrapper(n) -{ - Assert(isNormalForm()); -} - - +Comparison::Comparison(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); } SumPair Comparison::toSumPair() const { Kind cmpKind = comparisonKind(); @@ -727,8 +719,7 @@ SumPair Comparison::toSumPair() const { return SumPair(left - right, Constant::mkZero()); } } - default: - Unhandled(cmpKind); + default: Unhandled() << cmpKind; } } @@ -766,8 +757,7 @@ Polynomial Comparison::normalizedVariablePart() const { } } } - default: - Unhandled(cmpKind); + default: Unhandled() << cmpKind; } } @@ -816,8 +806,7 @@ DeltaRational Comparison::normalizedDeltaRational() const { return DeltaRational(0, 0); } } - default: - Unhandled(cmpKind); + default: Unhandled() << cmpKind; } } @@ -834,8 +823,7 @@ Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r) { case kind::GEQ: case kind::GT: return NodeManager::currentNM()->mkNode(k, l.getNode(), r.getNode()); - default: - Unhandled(k); + default: Unhandled() << k; } } @@ -875,9 +863,7 @@ size_t Comparison::getComplexity() const{ case kind::GT: case kind::GEQ: return getLeft().getComplexity() + getRight().getComplexity(); - default: - Unhandled(comparisonKind()); - return -1; + default: Unhandled() << comparisonKind(); return -1; } } @@ -895,8 +881,7 @@ Polynomial Comparison::getLeft() const { case kind::GEQ: left = getNode()[0]; break; - default: - Unhandled(k); + default: Unhandled() << k; } return Polynomial::parsePolynomial(left); } @@ -915,8 +900,7 @@ Polynomial Comparison::getRight() const { case kind::GEQ: right = getNode()[1]; break; - default: - Unhandled(k); + default: Unhandled() << k; } return Polynomial::parsePolynomial(right); } @@ -1290,8 +1274,7 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& l, const Polynomia result = isInteger ? mkIntInequality(k, diff) : mkRatInequality(k, diff); break; - default: - Unhandled(k); + default: Unhandled() << k; } Assert(!result.isNull()); if(result.getKind() == kind::NOT && result[0].getKind() == kind::CONST_BOOLEAN){ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index a3d173cc7..8099339ae 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -224,48 +224,44 @@ public: class Variable : public NodeWrapper { public: - Variable(Node n) : NodeWrapper(n) { - Assert(isMember(getNode())); - } - - // TODO: check if it's a theory leaf also - static bool isMember(Node n) { - Kind k = n.getKind(); - switch(k){ - case kind::CONST_RATIONAL: - return false; - case kind::INTS_DIVISION: - case kind::INTS_MODULUS: - case kind::DIVISION: - case kind::INTS_DIVISION_TOTAL: - case kind::INTS_MODULUS_TOTAL: - case kind::DIVISION_TOTAL: - return isDivMember(n); - case kind::EXPONENTIAL: - case kind::SINE: - case kind::COSINE: - case kind::TANGENT: - case kind::COSECANT: - case kind::SECANT: - case kind::COTANGENT: - case kind::ARCSINE: - case kind::ARCCOSINE: - case kind::ARCTANGENT: - case kind::ARCCOSECANT: - case kind::ARCSECANT: - case kind::ARCCOTANGENT: - case kind::SQRT: - case kind::PI: - return isTranscendentalMember(n); - case kind::ABS: - case kind::TO_INTEGER: - // Treat to_int as a variable; it is replaced in early preprocessing - // by a variable. - return true; - default: - return isLeafMember(n); - } - } + Variable(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); } + + // TODO: check if it's a theory leaf also + static bool isMember(Node n) + { + Kind k = n.getKind(); + switch (k) + { + case kind::CONST_RATIONAL: return false; + case kind::INTS_DIVISION: + case kind::INTS_MODULUS: + case kind::DIVISION: + case kind::INTS_DIVISION_TOTAL: + case kind::INTS_MODULUS_TOTAL: + case kind::DIVISION_TOTAL: return isDivMember(n); + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: + case kind::COSECANT: + case kind::SECANT: + case kind::COTANGENT: + case kind::ARCSINE: + case kind::ARCCOSINE: + case kind::ARCTANGENT: + case kind::ARCCOSECANT: + case kind::ARCSECANT: + case kind::ARCCOTANGENT: + case kind::SQRT: + case kind::PI: return isTranscendentalMember(n); + case kind::ABS: + case kind::TO_INTEGER: + // Treat to_int as a variable; it is replaced in early preprocessing + // by a variable. + return true; + default: return isLeafMember(n); + } + } static bool isLeafMember(Node n); static bool isDivMember(Node n); @@ -306,7 +302,7 @@ public: if(n < m){ return -1; }else{ - Assert( n != m ); + Assert(n != m); return 1; } }else{ @@ -339,20 +335,17 @@ public: class Constant : public NodeWrapper { public: - Constant(Node n) : NodeWrapper(n) { - Assert(isMember(getNode())); - } + Constant(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); } - static bool isMember(Node n) { - return n.getKind() == kind::CONST_RATIONAL; - } + static bool isMember(Node n) { return n.getKind() == kind::CONST_RATIONAL; } - bool isNormalForm() { return isMember(getNode()); } + bool isNormalForm() { return isMember(getNode()); } - static Constant mkConstant(Node n) { - Assert(n.getKind() == kind::CONST_RATIONAL); - return Constant(n); - } + static Constant mkConstant(Node n) + { + Assert(n.getKind() == kind::CONST_RATIONAL); + return Constant(n); + } static Constant mkConstant(const Rational& rat); @@ -597,8 +590,8 @@ private: Monomial(Node n, const Constant& c, const VarList& vl): NodeWrapper(n), constant(c), varList(vl) { - Assert(!c.isZero() || vl.empty() ); - Assert( c.isZero() || !vl.empty() ); + Assert(!c.isZero() || vl.empty()); + Assert(c.isZero() || !vl.empty()); Assert(!c.isOne() || !multStructured(n)); } @@ -623,15 +616,15 @@ private: Monomial(const VarList& vl): NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl) { - Assert( !varList.empty() ); + Assert(!varList.empty()); } Monomial(const Constant& c, const VarList& vl): NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl) { - Assert( !c.isZero() ); - Assert( !c.isOne() ); - Assert( !varList.empty() ); + Assert(!c.isZero()); + Assert(!c.isOne()); + Assert(!varList.empty()); Assert(multStructured(getNode())); } @@ -843,8 +836,8 @@ public: Polynomial(const std::vector<Monomial>& m): NodeWrapper(makePlusNode(m)), d_singleton(false) { - Assert( m.size() >= 2); - Assert( Monomial::isStrictlySorted(m) ); + Assert(m.size() >= 2); + Assert(Monomial::isStrictlySorted(m)); } static Polynomial mkPolynomial(const Constant& c){ @@ -901,7 +894,7 @@ public: } Polynomial getTail() const { - Assert(! singleton()); + Assert(!singleton()); iterator tailStart = begin(); ++tailStart; @@ -1097,14 +1090,9 @@ private: return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode()); } - SumPair(TNode n) : - NodeWrapper(n) - { - Assert(isNormalForm()); - } - -public: + SumPair(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); } + public: SumPair(const Polynomial& p): NodeWrapper(toNode(p, Constant::mkConstant(0))) { diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 77872fb55..bf27af36a 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -57,8 +57,7 @@ SimplexDecisionProcedure::~SimplexDecisionProcedure(){ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) { TimerStat::CodeTimer codeTimer(timer); - Assert( d_conflictVariables.empty() ); - + Assert(d_conflictVariables.empty()); while(d_errorSet.moreSignals()){ ArithVar curr = d_errorSet.topSignal(); @@ -99,7 +98,6 @@ void SimplexDecisionProcedure::reportConflict(ArithVar basic){ } ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const { - Assert(d_tableau.isBasic(basic)); Assert(checkBasicForConflict(basic)); @@ -198,7 +196,7 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time TimerStat::CodeTimer codeTimer(timer); Assert(!d_errorSet.focusEmpty()); Assert(debugIsASet(set)); - + ArithVar inf = requestVariable(); Assert(inf != ARITHVAR_SENTINEL); diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index cfd00ac30..b1153d36f 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -257,7 +257,7 @@ public: /** Sets the focusDirection. */ void setFocusDirection(int fd){ - Assert(-1 <= fd && fd <= 1); + Assert(-1 <= fd && fd <= 1); d_focusDirection = fd; updateWitness(); } diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index e23273a09..e50d9d060 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -405,7 +405,8 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes int prevFocusSgn = d_errorSet.popSignal(); if(d_tableau.isBasic(updated)){ - Assert(!d_variables.assignmentIsConsistent(updated) == d_errorSet.inError(updated)); + Assert(!d_variables.assignmentIsConsistent(updated) + == d_errorSet.inError(updated)); if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);} if(!d_variables.assignmentIsConsistent(updated)){ if(checkBasicForConflict(updated)){ @@ -642,7 +643,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ if(d_errorSize <= 2){ ArithVarVec inError; d_errorSet.pushFocusInto(inError); - + Assert(debugIsASet(inError)); subsets.push_back(inError); return subsets; @@ -712,7 +713,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ if(hasParticipated.isMember(v)){ continue; } hasParticipated.add(v); - + Assert(d_soiVar == ARITHVAR_SENTINEL); //d_soiVar's row = \sumofinfeasibilites underConstruction ArithVarVec underConstruction; @@ -770,7 +771,6 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){ // } } - Assert(d_soiVar == ARITHVAR_SENTINEL); Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl; return subsets; @@ -781,7 +781,7 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset); Assert(!subset.empty()); Assert(!d_conflictBuilder->underConstruction()); - + Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl; bool success = false; @@ -791,7 +791,6 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ ConstraintP violated = d_errorSet.getViolated(e); Assert(violated != NullConstraint); - int sgn = d_errorSet.getSgn(e); const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne; Debug("arith::generateSOIConflict") << "basic error var: " @@ -815,7 +814,7 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ // pick a violated constraint arbitrarily. any of them may be selected for the conflict Assert(d_conflictBuilder->underConstruction()); Assert(d_conflictBuilder->consequentIsSet()); - + for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){ const Tableau::Entry& entry = *i; ArithVar v = entry.getColVar(); @@ -864,7 +863,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ generateSOIConflict(d_qeConflict); }else{ vector<ArithVarVec> subsets = greedyConflictSubsets(); - Assert( d_soiVar == ARITHVAR_SENTINEL); + Assert(d_soiVar == ARITHVAR_SENTINEL); bool anySuccess = false; Assert(!subsets.empty()); for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){ @@ -879,7 +878,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ } Assert(anySuccess); } - Assert( d_soiVar == ARITHVAR_SENTINEL); + Assert(d_soiVar == ARITHVAR_SENTINEL); d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization); //reportConflict(conf); do not do this. We need a custom explanations! @@ -965,7 +964,6 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ Assert(d_conflictVariables.empty()); Assert(d_soiVar == ARITHVAR_SENTINEL); - //d_scores.purge(); d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiFocusConstructionTimer); diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index aa4c3d454..82b46bf30 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -102,7 +102,7 @@ void Tableau::addRow(ArithVar basic, { Assert(basic < getNumColumns()); Assert(debugIsASet(variables)); - Assert(coefficients.size() == variables.size() ); + Assert(coefficients.size() == variables.size()); Assert(!isBasic(basic)); RowIndex newRow = Matrix<Rational>::addRow(coefficients, variables); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c775a2611..62be1fcc1 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -691,7 +691,6 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){ Assert(constraint->isLowerBound()); Assert(constraint->isTrue()); Assert(!constraint->negationHasProof()); - ArithVar x_i = constraint->getVariable(); const DeltaRational& c_i = constraint->getValue(); @@ -733,7 +732,6 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){ const ValueCollection& vc = constraint->getValueCollection(); if(vc.hasEquality()){ - Assert(vc.hasDisequality()); ConstraintP eq = vc.getEquality(); ConstraintP diseq = vc.getDisequality(); @@ -828,7 +826,7 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){ Assert(constraint->isUpperBound()); Assert(constraint->isTrue()); Assert(!constraint->negationHasProof()); - + ArithVar x_i = constraint->getVariable(); const DeltaRational& c_i = constraint->getValue(); @@ -1001,7 +999,6 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){ Assert(cmpToLB >= 0); Assert(cmpToUB < 0 || cmpToLB > 0); - if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); Debug("dio::push") << "dio::push " << x_i << endl; @@ -1211,7 +1208,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { case kind::INTS_MODULUS: case kind::DIVISION: // these should be removed during expand definitions - Assert( false ); + Assert(false); break; case kind::INTS_DIVISION_TOTAL: @@ -1433,8 +1430,8 @@ ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){ bestRowLength = rowLength; } } - Assert(bestBasic == ARITHVAR_SENTINEL || - bestRowLength < std::numeric_limits<uint32_t>::max()); + Assert(bestBasic == ARITHVAR_SENTINEL + || bestRowLength < std::numeric_limits<uint32_t>::max()); return bestBasic; } @@ -1528,7 +1525,8 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ } Node vnode = v.getNode(); - Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion + Assert( + isSetup(vnode)); // Otherwise there is some invariant breaking recursion Polynomial m = Polynomial::parsePolynomial(vnode[0]); Polynomial n = Polynomial::parsePolynomial(vnode[1]); @@ -1541,7 +1539,7 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){ case INTS_DIVISION: case INTS_MODULUS: // these should be removed during expand definitions - Assert( false ); + Assert(false); break; case DIVISION_TOTAL: lem = axiomIteForTotalDivision(vnode); @@ -1743,7 +1741,7 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){ throw LogicException(ss.str()); } Assert(!d_partialModel.hasArithVar(x)); - Assert(x.getType().isReal()); // real or integer + Assert(x.getType().isReal()); // real or integer ArithVar max = d_partialModel.getNumberOfVariables(); ArithVar varX = d_partialModel.allocate(x, aux); @@ -1897,7 +1895,6 @@ Node TheoryArithPrivate::callDioSolver(){ Assert(isInteger(v)); Assert(d_partialModel.boundsAreEqual(v)); - ConstraintP lb = d_partialModel.getLowerBoundConstraint(v); ConstraintP ub = d_partialModel.getUpperBoundConstraint(v); @@ -1937,7 +1934,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){ Kind simpleKind = Comparison::comparisonKind(assertion); ConstraintP constraint = d_constraintDatabase.lookup(assertion); if(constraint == NullConstraint){ - Assert(simpleKind == EQUAL || simpleKind == DISTINCT ); + Assert(simpleKind == EQUAL || simpleKind == DISTINCT); bool isDistinct = simpleKind == DISTINCT; Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion; Assert(!isSetup(eq)); @@ -1945,8 +1942,8 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){ if(reEq.getKind() == CONST_BOOLEAN){ if(reEq.getConst<bool>() == isDistinct){ // if is (not true), or false - Assert((reEq.getConst<bool>() && isDistinct) || - (!reEq.getConst<bool>() && !isDistinct)); + Assert((reEq.getConst<bool>() && isDistinct) + || (!reEq.getConst<bool>() && !isDistinct)); raiseBlackBoxConflict(assertion); } return NullConstraint; @@ -2209,7 +2206,8 @@ void TheoryArithPrivate::outputLemma(TNode lem) { // void TheoryArithPrivate::branchVector(const std::vector<ArithVar>& lemmas){ // //output the lemmas -// for(vector<ArithVar>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){ +// for(vector<ArithVar>::const_iterator i = lemmas.begin(); i != lemmas.end(); +// ++i){ // ArithVar v = *i; // Assert(!d_cutInContext.contains(v)); // d_cutInContext.insert(v); @@ -2343,7 +2341,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const D << " " << rhs << endl; - Assert( k == kind::LEQ || k == kind::GEQ ); + Assert(k == kind::LEQ || k == kind::GEQ); Node comparison = NodeManager::currentNM()->mkNode(k, sum, mkRationalNode(rhs)); Node rewritten = Rewriter::rewrite(comparison); @@ -2508,7 +2506,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc pair<ConstraintP, ArithVar> p = replayGetConstraint(bci); Assert(p.second == ARITHVAR_SENTINEL); ConstraintP bc = p.first; - Assert(bc != NullConstraint); + Assert(bc != NullConstraint); if(bc->hasProof()){ return; } @@ -2538,7 +2536,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc conflicts.push_back(ConstraintCPVec()); intHoleConflictToVector(d_conflicts[i], conflicts.back()); Constraint::assertionFringe(conflicts.back()); - + // ConstraintCP conflicting = d_conflicts[i]; // ConstraintCP negConflicting = conflicting->getNegation(); // Assert(conflicting->hasProof()); @@ -2891,7 +2889,6 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex } Assert(d_acTmp.empty()); - /* Garbage collect the constraints from this call */ while(d_replayConstraints.size() > rpcons_size){ ConstraintP c = d_replayConstraints.back(); @@ -3165,11 +3162,12 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if(mipRes == MipClosed){ d_likelyIntegerInfeasible = true; replayLog(approx); - AlwaysAssert(anyConflict() || d_qflraStatus != Result::SAT); + AlwaysAssert(anyConflict() || d_qflraStatus != Result::SAT); - if(!anyConflict()){ - solveRealRelaxation(effortLevel); - } + if (!anyConflict()) + { + solveRealRelaxation(effortLevel); + } } if(!(anyConflict() || !d_approxCuts.empty())){ turnOffApproxFor(options::replayNumericFailurePenalty()); @@ -3749,8 +3747,8 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ d_currentPropagationList.pop_front(); ConstraintType t = curr->getType(); - Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation"); - + Assert(t != Disequality) + << "Disequalities are not allowed in d_currentPropagation"; switch(t){ case LowerBound: @@ -3776,8 +3774,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB); break; } - default: - Unhandled(curr->getType()); + default: Unhandled() << curr->getType(); } } @@ -3796,7 +3793,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); d_currentPropagationList.clear(); } - Assert( d_currentPropagationList.empty()); + Assert(d_currentPropagationList.empty()); Debug("arith::ems") << "ems: " << emmittedConflictOrSplit << "post unate" << endl; @@ -3903,7 +3900,7 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const { const Rational& i = d.getInfinitesimalPart(); Trace("integers") << "integers: assignment to [[" << d_partialModel.asNode(x) << "]] is " << r << "[" << i << "]" << endl; - Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0)); + Assert(!(r.getDenominator() == 1 && i.getNumerator() == 0)); Assert(!d.isIntegral()); TNode var = d_partialModel.asNode(x); Integer floor_d = d.floor(); @@ -4134,7 +4131,9 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { Debug("arith::prop") << c->getNegation()->externalExplainByAssertions() << endl; } - Assert(!c->negationHasProof(), "A constraint has been propagated on the constraint propagation queue, but the negation has been set to true. Contact Tim now!"); + Assert(!c->negationHasProof()) + << "A constraint has been propagated on the constraint propagation " + "queue, but the negation has been set to true. Contact Tim now!"; if(!c->assertedToTheTheory()){ Node literal = c->getLiteral(); @@ -4302,7 +4301,7 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) { - AlwaysAssert(d_qflraStatus == Result::SAT); + AlwaysAssert(d_qflraStatus == Result::SAT); //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); if(Debug.isOn("arith::collectModelInfo")){ @@ -4463,8 +4462,7 @@ void TheoryArithPrivate::presolve(){ d_constraintDatabase.outputUnateInequalityLemmas(lemmas); d_constraintDatabase.outputUnateEqualityLemmas(lemmas); break; - default: - Unhandled(options::arithUnateLemmaMode()); + default: Unhandled() << options::arithUnateLemmaMode(); } } @@ -4525,10 +4523,14 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound if(bestImplied != NullConstraint){ //This should be stronger Assert(!upperBound || bound <= bestImplied->getValue()); - Assert(!upperBound || d_partialModel.lessThanUpperBound(basic, bestImplied->getValue())); - - Assert( upperBound || bound >= bestImplied->getValue()); - Assert( upperBound || d_partialModel.greaterThanLowerBound(basic, bestImplied->getValue())); + Assert( + !upperBound + || d_partialModel.lessThanUpperBound(basic, bestImplied->getValue())); + + Assert(upperBound || bound >= bestImplied->getValue()); + Assert(upperBound + || d_partialModel.greaterThanLowerBound(basic, + bestImplied->getValue())); //slightly changed // ConstraintP c = d_constraintDatabase.lookup(bestImplied); @@ -5152,7 +5154,8 @@ Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest, return skolem; } -// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){ +// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const +// InferBoundsParameters& param){ // Node t = Rewriter::rewrite(term); // Assert(Polynomial::isMember(t)); // Polynomial p = Polynomial::parsePolynomial(t); @@ -5168,8 +5171,8 @@ Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest, // if(res.foundBound()){ // DeltaRational newBound = res.getValue() + c.getValue(); // if(tail.isIntegral()){ -// Integer asInt = (param.findLowerBound()) ? newBound.ceiling() : newBound.floor(); -// newBound = DeltaRational(asInt); +// Integer asInt = (param.findLowerBound()) ? newBound.ceiling() : +// newBound.floor(); newBound = DeltaRational(asInt); // } // res.setBound(newBound, res.getExplanation()); // } @@ -5202,14 +5205,16 @@ Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest, // { // InferBoundsResult lookup = inferUpperBoundLookup(t, param); // if(lookup.foundBound()){ -// if(param.getEffort() == InferBoundsParameters::LookupAndSimplexOnFailure || +// if(param.getEffort() == +// InferBoundsParameters::LookupAndSimplexOnFailure || // lookup.boundIsOptimal()){ // return lookup; // } // } // InferBoundsResult simplex = inferUpperBoundSimplex(t, param); // if(lookup.foundBound() && simplex.foundBound()){ -// return (lookup.getValue() <= simplex.getValue()) ? lookup : simplex; +// return (lookup.getValue() <= simplex.getValue()) ? lookup : +// simplex; // }else if(lookup.foundBound()){ // return lookup; // }else{ @@ -5223,7 +5228,6 @@ Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest, // } // } - std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ using namespace inferbounds; @@ -5351,7 +5355,8 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith << " <= " << primDir << "*" << dm << "*" << bestPrimDiff.second << " <= " << primDir << "*" << sep << endl << " by " << bestPrimDiff.first << endl; - Assert(bestPrimDiff.second * (Rational(primDir)* dm) <= (sep * Rational(primDir))); + Assert(bestPrimDiff.second * (Rational(primDir) * dm) + <= (sep * Rational(primDir))); return make_pair(true, bestPrimDiff.first); } } @@ -5842,7 +5847,8 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg } } -// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const inferbounds::InferBoundAlgorithm& param){ +// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const +// inferbounds::InferBoundAlgorithm& param){ // Assert(param.findUpperBound()); // if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){ @@ -5907,7 +5913,8 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg // // TODO improve upon bland's // ArithVar entering = ARITHVAR_SENTINEL; // const Tableau::Entry* enteringEntry = NULL; -// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ +// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); +// !ri.atEnd(); ++ri){ // const Tableau::Entry& entry = *ri; // ArithVar v = entry.getColVar(); // if(v != optVar){ @@ -5975,7 +5982,6 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg // } // } - // if(leaving == ARITHVAR_SENTINEL){ // finalState = NoBound; // break; @@ -6003,7 +6009,8 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg // case Inferred: // { // NodeBuilder<> nb(kind::AND); -// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ +// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); +// !ri.atEnd(); ++ri){ // const Tableau::Entry& e =*ri; // ArithVar colVar = e.getColVar(); // if(colVar != optVar){ diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index 5c6bf63ce..bb1612928 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -36,8 +36,8 @@ class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> { RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) : TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0) { - Assert(type.getKind() == kind::TYPE_CONSTANT && - type.getConst<TypeConstant>() == REAL_TYPE); + Assert(type.getKind() == kind::TYPE_CONSTANT + && type.getConst<TypeConstant>() == REAL_TYPE); } Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); } @@ -77,8 +77,8 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> { IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) : TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0) { - Assert(type.getKind() == kind::TYPE_CONSTANT && - type.getConst<TypeConstant>() == INTEGER_TYPE); + Assert(type.getKind() == kind::TYPE_CONSTANT + && type.getConst<TypeConstant>() == INTEGER_TYPE); } Node operator*() override |