diff options
| author | Tim King <taking@cs.nyu.edu> | 2014-06-25 10:46:40 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-25 10:50:38 -0400 |
| commit | 15a15f5c9fa65df13dfb2fe6b3bf3fc3604ddacc (patch) | |
| tree | d1259217632ff03797926310305029bd2e94656c | |
| parent | edb81bac8370bb09ddc9ff7a85fafb852a8e05ba (diff) | |
Fixing the previous bugfix.smtcomp2014-resubmission
| -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 f6ac951bc..30fc25306 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2146,6 +2146,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()); @@ -2288,6 +2291,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(); @@ -2563,6 +2567,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex SimplexDecisionProcedure& simplex = selectSimplex(true); simplex.findModel(false); + // can change d_qflraStatus d_linEq.stopTrackingBoundCounts(); d_partialModel.startQueueingBoundCounts(); @@ -2964,18 +2969,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())){ |