diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/approx_simplex.cpp | 116 | ||||
-rw-r--r-- | src/theory/arith/attempt_solution_simplex.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/constraint.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/dual_simplex.cpp | 40 | ||||
-rw-r--r-- | src/theory/arith/fc_simplex.cpp | 57 | ||||
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/soi_simplex.cpp | 47 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 15 |
9 files changed, 185 insertions, 107 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 7c89a9e39..2432e6945 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -630,9 +630,10 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& v, TreeLog& l, ApproximateStatistic for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){ ArithVar v = *vi; - if(s_verbosity >= 2){ - //Message() << v << " "; - //d_vars.printModel(v, Message()); + if (s_verbosity >= 2) + { + // CVC4Message() << v << " "; + // d_vars.printModel(v, CVC4Message()); } int type; @@ -763,9 +764,10 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ for(ArithVariables::var_iterator vi = d_vars.var_begin(), vi_end = d_vars.var_end(); vi != vi_end; ++vi){ ArithVar v = *vi; - if(s_verbosity >= 2){ - Message() << v << " "; - d_vars.printModel(v, Message()); + if (s_verbosity >= 2) + { + CVC4Message() << v << " "; + d_vars.printModel(v, CVC4Message()); } int type; @@ -865,9 +867,11 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ int dir = guessDir(r); if(len >= rowLengthReq){ - if(s_verbosity >= 1){ - Message() << "high row " << r << " " << len << " " << avgRowLength << " " << dir<< endl; - d_vars.printModel(r, Message()); + if (s_verbosity >= 1) + { + CVC4Message() << "high row " << r << " " << len << " " << avgRowLength + << " " << dir << endl; + d_vars.printModel(r, CVC4Message()); } ret.push_back(ArithRatPair(r, Rational(dir))); } @@ -885,9 +889,11 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{ double ubScore = double(bc.upperBoundCount()) / maxCount; double lbScore = double(bc.lowerBoundCount()) / maxCount; if(ubScore >= .9 || lbScore >= .9){ - if(s_verbosity >= 1){ - Message() << "high col " << c << " " << bc << " " << ubScore << " " << lbScore << " " << dir << endl; - d_vars.printModel(c, Message()); + if (s_verbosity >= 1) + { + CVC4Message() << "high col " << c << " " << bc << " " << ubScore + << " " << lbScore << " " << dir << endl; + d_vars.printModel(c, CVC4Message()); } ret.push_back(ArithRatPair(c, Rational(c))); } @@ -1009,22 +1015,26 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const int status = isAux ? glp_get_row_stat(prob, glpk_index) : glp_get_col_stat(prob, glpk_index); - if(s_verbosity >= 2){ - Message() << "assignment " << vi << endl; + if (s_verbosity >= 2) + { + CVC4Message() << "assignment " << vi << endl; } bool useDefaultAssignment = false; switch(status){ case GLP_BS: - //Message() << "basic" << endl; + // CVC4Message() << "basic" << endl; newBasis.add(vi); useDefaultAssignment = true; break; case GLP_NL: case GLP_NS: if(!mip){ - if(s_verbosity >= 2){ Message() << "non-basic lb" << endl; } + if (s_verbosity >= 2) + { + CVC4Message() << "non-basic lb" << endl; + } newValues.set(vi, d_vars.getLowerBound(vi)); }else{// intentionally fall through otherwise useDefaultAssignment = true; @@ -1032,7 +1042,10 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const break; case GLP_NU: if(!mip){ - if(s_verbosity >= 2){ Message() << "non-basic ub" << endl; } + if (s_verbosity >= 2) + { + CVC4Message() << "non-basic ub" << endl; + } newValues.set(vi, d_vars.getUpperBound(vi)); }else {// intentionally fall through otherwise useDefaultAssignment = true; @@ -1046,7 +1059,10 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const } if(useDefaultAssignment){ - if(s_verbosity >= 2){ Message() << "non-basic other" << endl; } + if (s_verbosity >= 2) + { + CVC4Message() << "non-basic other" << endl; + } double newAssign; if(mip){ @@ -1058,24 +1074,35 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const } const DeltaRational& oldAssign = d_vars.getAssignment(vi); - - if(d_vars.hasLowerBound(vi) && - roughlyEqual(newAssign, d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))){ - //Message() << " to lb" << endl; + if (d_vars.hasLowerBound(vi) + && roughlyEqual(newAssign, + d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA))) + { + // CVC4Message() << " to lb" << endl; newValues.set(vi, d_vars.getLowerBound(vi)); - }else if(d_vars.hasUpperBound(vi) && - roughlyEqual(newAssign, d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))){ + } + else if (d_vars.hasUpperBound(vi) + && roughlyEqual( + newAssign, + d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA))) + { newValues.set(vi, d_vars.getUpperBound(vi)); - // Message() << " to ub" << endl; - }else{ - + // CVC4Message() << " to ub" << endl; + } + else + { double rounded = round(newAssign); - if(roughlyEqual(newAssign, rounded)){ - // Message() << "roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl; + if (roughlyEqual(newAssign, rounded)) + { + // CVC4Message() << "roughly equal " << rounded << " " << newAssign << + // " " << oldAssign << endl; newAssign = rounded; - }else{ - // Message() << "not roughly equal " << rounded << " " << newAssign << " " << oldAssign << endl; + } + else + { + // CVC4Message() << "not roughly equal " << rounded << " " << + // newAssign << " " << oldAssign << endl; } DeltaRational proposal; @@ -1089,20 +1116,29 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const proposal = d_vars.getAssignment(vi); } - if(roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))){ - // Message() << " to prev value" << newAssign << " " << oldAssign << endl; + if (roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA))) + { + // CVC4Message() << " to prev value" << newAssign << " " << oldAssign + // << endl; proposal = d_vars.getAssignment(vi); } - - if(d_vars.strictlyLessThanLowerBound(vi, proposal)){ - //Message() << " round to lb " << d_vars.getLowerBound(vi) << endl; + if (d_vars.strictlyLessThanLowerBound(vi, proposal)) + { + // CVC4Message() << " round to lb " << d_vars.getLowerBound(vi) << + // endl; proposal = d_vars.getLowerBound(vi); - }else if(d_vars.strictlyGreaterThanUpperBound(vi, proposal)){ - //Message() << " round to ub " << d_vars.getUpperBound(vi) << endl; + } + else if (d_vars.strictlyGreaterThanUpperBound(vi, proposal)) + { + // CVC4Message() << " round to ub " << d_vars.getUpperBound(vi) << + // endl; proposal = d_vars.getUpperBound(vi); - }else{ - //Message() << " use proposal" << proposal << " " << oldAssign << endl; + } + else + { + // CVC4Message() << " use proposal" << proposal << " " << oldAssign + // << endl; } newValues.set(vi, proposal); } diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index b8e08add8..22802b558 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -122,12 +122,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - //Message() << toRemove << " " << toAdd << endl; + // CVC4Message() << toRemove << " " << toAdd << endl; d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - //Message() << needsToBeAdded.size() << "to go" << endl; + // CVC4Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); bool conflict = processSignals(); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index b0be108f7..03d9c50e9 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -179,10 +179,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){ return o; } -void Constraint::debugPrint() const { - Message() << *this << endl; -} - +void Constraint::debugPrint() const { CVC4Message() << *this << endl; } ValueCollection::ValueCollection() : d_lowerBound(NullConstraint), diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 15d6b9f50..15faf58bf 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -784,8 +784,8 @@ void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{ const SumPair& eq = d_trail[i].d_eq; const Polynomial& proof = d_trail[i].d_proof; - Message() << "d_trail["<<i<<"].d_eq = " << eq.getNode() << endl; - Message() << "d_trail["<<i<<"].d_proof = " << proof.getNode() << endl; + CVC4Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl; + CVC4Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl; } void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){ diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 3d6e92283..4ac3034ff 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -107,13 +107,19 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ } } - if(verbose && numDifferencePivots > 0){ - if(result == Result::UNSAT){ - Message() << "diff order found unsat" << endl; - }else if(d_errorSet.errorEmpty()){ - Message() << "diff order found model" << endl; - }else{ - Message() << "diff order missed" << endl; + if (verbose && numDifferencePivots > 0) + { + if (result == Result::UNSAT) + { + CVC4Message() << "diff order found unsat" << endl; + } + else if (d_errorSet.errorEmpty()) + { + CVC4Message() << "diff order found model" << endl; + } + else + { + CVC4Message() << "diff order missed" << endl; } } } @@ -133,13 +139,19 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){ result = Result::UNSAT; } - if(verbose){ - if(result == Result::UNSAT){ - Message() << "restricted var order found unsat" << endl; - }else if(d_errorSet.errorEmpty()){ - Message() << "restricted var order found model" << endl; - }else{ - Message() << "restricted var order missed" << endl; + if (verbose) + { + if (result == Result::UNSAT) + { + CVC4Message() << "restricted var order found unsat" << endl; + } + else if (d_errorSet.errorEmpty()) + { + CVC4Message() << "restricted var order found model" << endl; + } + else + { + CVC4Message() << "restricted var order missed" << endl; } } } diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 7b482b314..33f01eba1 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -98,7 +98,10 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl; Assert(d_conflictVariables.empty()); - //if(verbose){ Message() << "fcFindModel("<< instance <<") trivial" << endl; } + //if (verbose) + //{ + // CVC4Message() << "fcFindModel(" << instance << ") trivial" << endl; + //} return Result::SAT; } @@ -110,12 +113,18 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(initialProcessSignals()){ d_conflictVariables.purge(); - if(verbose){ Message() << "fcFindModel("<< instance <<") early conflict" << endl; } + if (verbose) + { + CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl; + } Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; }else if(d_errorSet.errorEmpty()){ - //if(verbose){ Message() << "fcFindModel("<< instance <<") fixed itself" << endl; } + //if (verbose) + //{ + // CVC4Message() << "fcFindModel(" << instance << ") fixed itself" << endl; + //} Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl; if (verbose) Assert(!d_errorSet.moreSignals()); Assert(d_conflictVariables.empty()); @@ -142,17 +151,27 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){ if(result == Result::UNSAT){ ++(d_statistics.d_fcFoundUnsat); - if(verbose){ Message() << "fc found unsat";} + if (verbose) + { + CVC4Message() << "fc found unsat"; + } }else if(d_errorSet.errorEmpty()){ ++(d_statistics.d_fcFoundSat); - if(verbose){ Message() << "fc found model"; } + if (verbose) + { + CVC4Message() << "fc found model"; + } }else{ ++(d_statistics.d_fcMissed); - if(verbose){ Message() << "fc missed"; } + if (verbose) + { + CVC4Message() << "fc missed"; + } } } - if(verbose){ - Message() << "(" << instance << ") pivots " << d_pivots << endl; + if (verbose) + { + CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl; } Assert(!d_errorSet.moreSignals()); @@ -524,12 +543,10 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit } if(degenerate(w) && selected.describesPivot()){ ArithVar leaving = selected.leaving(); - Message() - << "degenerate " << leaving - << ", atBounds " << d_linEq.basicsAtBounds(selected) - << ", len " << d_tableau.basicRowLength(leaving) - << ", bc " << d_linEq.debugBasicAtBoundCount(leaving) - << endl; + CVC4Message() << "degenerate " << leaving << ", atBounds " + << d_linEq.basicsAtBounds(selected) << ", len " + << d_tableau.basicRowLength(leaving) << ", bc " + << d_linEq.debugBasicAtBoundCount(leaving) << endl; } } @@ -575,9 +592,10 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit } } - if(verbose){ - Message() << "conflict variable " << selected << endl; - Message() << ss.str(); + if (verbose) + { + CVC4Message() << "conflict variable " << selected << endl; + CVC4Message() << ss.str(); } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } @@ -791,8 +809,9 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){ Assert(d_focusSize == d_errorSet.focusSize()); Assert(d_errorSize == d_errorSet.errorSize()); - if(verbose){ - debugDualLike(w, Message(), instance, prevFocusSize, prevErrorSize); + if (verbose) + { + debugDualLike(w, CVC4Message(), 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 32d2714e8..765061e8d 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -184,12 +184,12 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){ Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - Message() << toRemove << " " << toAdd << endl; + CVC4Message() << toRemove << " " << toAdd << endl; d_tableau.pivot(toRemove, toAdd, d_trackCallback); d_basicVariableUpdates(toAdd); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - Message() << needsToBeAdded.size() << "to go" << endl; + CVC4Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); } } diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index ecac3d749..3f2fca50f 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -121,7 +121,10 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ if(initialProcessSignals()){ d_conflictVariables.purge(); - if(verbose){ Message() << "fcFindModel("<< instance <<") early conflict" << endl; } + if (verbose) + { + CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl; + } Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl; Assert(d_conflictVariables.empty()); return Result::UNSAT; @@ -152,17 +155,27 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){ if(result == Result::UNSAT){ ++(d_statistics.d_soiFoundUnsat); - if(verbose){ Message() << "fc found unsat";} + if (verbose) + { + CVC4Message() << "fc found unsat"; + } }else if(d_errorSet.errorEmpty()){ ++(d_statistics.d_soiFoundSat); - if(verbose){ Message() << "fc found model"; } + if (verbose) + { + CVC4Message() << "fc found model"; + } }else{ ++(d_statistics.d_soiMissed); - if(verbose){ Message() << "fc missed"; } + if (verbose) + { + CVC4Message() << "fc missed"; + } } } - if(verbose){ - Message() << "(" << instance << ") pivots " << d_pivots << endl; + if (verbose) + { + CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl; } Assert(!d_errorSet.moreSignals()); @@ -373,12 +386,10 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes } if(degenerate(w) && selected.describesPivot()){ ArithVar leaving = selected.leaving(); - Message() - << "degenerate " << leaving - << ", atBounds " << d_linEq.basicsAtBounds(selected) - << ", len " << d_tableau.basicRowLength(leaving) - << ", bc " << d_linEq.debugBasicAtBoundCount(leaving) - << endl; + CVC4Message() << "degenerate " << leaving << ", atBounds " + << d_linEq.basicsAtBounds(selected) << ", len " + << d_tableau.basicRowLength(leaving) << ", bc " + << d_linEq.debugBasicAtBoundCount(leaving) << endl; } } @@ -424,9 +435,10 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes } } - if(verbose){ - Message() << "conflict variable " << selected << endl; - Message() << ss.str(); + if (verbose) + { + CVC4Message() << "conflict variable " << selected << endl; + CVC4Message() << ss.str(); } if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); } @@ -982,8 +994,9 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ Assert(d_errorSize == d_errorSet.errorSize()); - if(verbose){ - debugSOI(w, Message(), instance); + if (verbose) + { + debugSOI(w, CVC4Message(), instance); } Assert(debugSOI(w, Debug("dualLike"), instance)); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 153b8e379..74f2bdbd3 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3193,7 +3193,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // int maxDepth = // d_likelyIntegerInfeasible ? 1 : options::arithMaxBranchDepth(); - // if(d_likelyIntegerInfeasible){ // d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution); // }else{ @@ -3203,7 +3202,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // mipRes = approxSolver->solveMIP(true); // } // d_errorSet.reduceToSignals(); -// //Message() << "here" << endl; +// //CVC4Message() << "here" << endl; // if(mipRes == ApproximateSimplex::ApproxSat){ // mipSolution = approxSolver->extractMIP(); // d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution); @@ -3219,13 +3218,15 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // } // } // options::arithStandardCheckVarOrderPivots.set(pass2Limit); -// if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); } -// //Message() << "done" << endl; +// if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = +// simplex.findModel(false); } +// //CVC4Message() << "done" << endl; // } // break; // case ApproximateSimplex::ApproxUnsat: // { -// ApproximateSimplex::Solution sol = approxSolver->extractRelaxation(); +// ApproximateSimplex::Solution sol = +// approxSolver->extractRelaxation(); // d_qflraStatus = d_attemptSolSimplex.attempt(sol); // options::arithStandardCheckVarOrderPivots.set(pass2Limit); @@ -3245,13 +3246,13 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ // }else{ // if(d_qflraStatus == Result::SAT_UNKNOWN){ -// //Message() << "got sat unknown" << endl; +// //CVC4Message() << "got sat unknown" << endl; // vector<ArithVar> toCut = cutAllBounded(); // if(toCut.size() > 0){ // //branchVector(toCut); // emmittedConflictOrSplit = true; // }else{ -// //Message() << "splitting" << endl; +// //CVC4Message() << "splitting" << endl; // d_qflraStatus = simplex.findModel(noPivotLimit); // } |