summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/approx_simplex.cpp116
-rw-r--r--src/theory/arith/attempt_solution_simplex.cpp4
-rw-r--r--src/theory/arith/constraint.cpp5
-rw-r--r--src/theory/arith/dio_solver.cpp4
-rw-r--r--src/theory/arith/dual_simplex.cpp40
-rw-r--r--src/theory/arith/fc_simplex.cpp57
-rw-r--r--src/theory/arith/linear_equality.cpp4
-rw-r--r--src/theory/arith/soi_simplex.cpp47
-rw-r--r--src/theory/arith/theory_arith_private.cpp15
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);
// }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback