summaryrefslogtreecommitdiff
path: root/src/theory/arith/attempt_solution_simplex.cpp
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2013-05-03 21:55:40 -0400
committerTim King <taking@cs.nyu.edu>2013-05-05 14:24:45 -0400
commitf5a9b1de720d6c77815ebb0ea9d6e911905885d1 (patch)
tree7a7f8e77a09fc3c28e2334e040cd32827b700981 /src/theory/arith/attempt_solution_simplex.cpp
parent5a20ba9f1f843fe066bbc8268f511a71902b88cb (diff)
Adding cut offs for likely integer infeasible paths.
Diffstat (limited to 'src/theory/arith/attempt_solution_simplex.cpp')
-rw-r--r--src/theory/arith/attempt_solution_simplex.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index c8d5b6f68..9db56ff68 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -103,12 +103,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
Assert(toAdd != ARITHVAR_SENTINEL);
Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
- Message() << toRemove << " " << toAdd << endl;
+ //Message() << toRemove << " " << toAdd << endl;
d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
- Message() << needsToBeAdded.size() << "to go" << endl;
+ //Message() << needsToBeAdded.size() << "to go" << endl;
needsToBeAdded.remove(toAdd);
bool conflict = processSignals();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback