diff options
| author | Tim King <taking@cs.nyu.edu> | 2014-06-25 10:46:40 -0400 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2014-06-25 10:46:40 -0400 |
| commit | b1e7d97356e2926d67a4208168e7b6017d7f77ed (patch) | |
| tree | 45d9160738d9d4263b5d10f15a4da12fd4d31e76 | |
| parent | 7e5245639848594e5ff72a5104c340defe4aac7c (diff) | |
Fixing the previous bugfix.
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0fa9e79f2..d3178c34f 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2147,6 +2147,9 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){ d_currentPropagationList.resize(enteringPropN); } + /* It is not clear what the d_qflraStatus is at this point */ + d_qflraStatus = Result::SAT_UNKNOWN; + Assert(d_replayVariables.empty()); Assert(d_replayConstraints.empty()); @@ -2289,6 +2292,7 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc SimplexDecisionProcedure& simplex = selectSimplex(true); simplex.findModel(false); + // Can change d_qflraStatus d_linEq.stopTrackingBoundCounts(); d_partialModel.startQueueingBoundCounts(); @@ -2564,6 +2568,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex SimplexDecisionProcedure& simplex = selectSimplex(true); simplex.findModel(false); + // can change d_qflraStatus d_linEq.stopTrackingBoundCounts(); d_partialModel.startQueueingBoundCounts(); @@ -2965,18 +2970,10 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if(mipRes == MipClosed){ d_likelyIntegerInfeasible = true; replayLog(approx); + AlwaysAssert(anyConflict() || d_qflraStatus != Result::SAT); if(!anyConflict()){ - //start up simplex - d_partialModel.stopQueueingBoundCounts(); - UpdateTrackingCallback utcb(&d_linEq); - d_partialModel.processBoundsQueue(utcb); - d_linEq.startTrackingBoundCounts(); - //call simplex - solveRelaxationOrPanic(effortLevel); - // shutdown simplex - d_linEq.stopTrackingBoundCounts(); - d_partialModel.startQueueingBoundCounts(); + solveRealRelaxation(effortLevel); } } if(!(anyConflict() || !d_approxCuts.empty())){ |