diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-04 03:03:34 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-04 03:03:34 +0000 |
commit | 3d1c57e0506b2454aa815c3c1cb634d96ade1d7c (patch) | |
tree | 1805ae7dae1f9e9b04c2d344ce252a969fc4e7a8 /src/theory/arith/simplex.cpp | |
parent | 1433806056059339dd16ae8e431feaae23553150 (diff) |
- This fixes a problem where simplex produced the same conflict in the single check call.
- This increases the number of substitutions that ppAssert can solve on integer equations.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index d3092c044..31187afd1 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -34,6 +34,7 @@ static const bool CHECK_AFTER_PIVOT = true; static const uint32_t VARORDER_CHECK_PERIOD = 200; SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) : + d_conflictVariable(ARITHVAR_SENTINEL), d_linEq(linEq), d_partialModel(d_linEq.getPartialModel()), d_tableau(d_linEq.getTableau()), @@ -203,6 +204,7 @@ Node betterConflict(TNode x, TNode y){ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime); + Assert(d_successes.empty()); switch(type){ case BeforeDiffSearch: ++(d_statistics.d_attemptBeforeDiffSearch); break; @@ -212,21 +214,20 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { case AfterVarOrderSearch: ++(d_statistics.d_attemptAfterVarOrderSearch); break; } - bool success = false; ArithPriorityQueue::const_iterator i = d_queue.begin(); ArithPriorityQueue::const_iterator end = d_queue.end(); for(; i != end; ++i){ ArithVar x_i = *i; - if(d_tableau.isBasic(x_i)){ + if(x_i != d_conflictVariable && d_tableau.isBasic(x_i) && !d_successes.isMember(x_i)){ Node possibleConflict = checkBasicForConflict(x_i); if(!possibleConflict.isNull()){ - success = true; + d_successes.add(x_i); reportConflict(possibleConflict); } } } - if(success){ + if(!d_successes.empty()){ switch(type){ case BeforeDiffSearch: ++(d_statistics.d_successBeforeDiffSearch); break; case DuringDiffSearch: ++(d_statistics.d_successDuringDiffSearch); break; @@ -234,11 +235,16 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break; case AfterVarOrderSearch: ++(d_statistics.d_successAfterVarOrderSearch); break; } + d_successes.purge(); + return true; + }else{ + return false; } - return success; } bool SimplexDecisionProcedure::findModel(){ + Assert(d_conflictVariable == ARITHVAR_SENTINEL); + if(d_queue.empty()){ return false; } @@ -293,6 +299,7 @@ bool SimplexDecisionProcedure::findModel(){ // means that the assignment we can always empty these queues. d_queue.clear(); d_pivotsInRound.purge(); + d_conflictVariable = ARITHVAR_SENTINEL; Assert(!d_queue.inCollectionMode()); d_queue.transitionToCollectionMode(); @@ -363,6 +370,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); Node conflict = generateConflictBelowLowerBound(x_i); //unsat + d_conflictVariable = x_i; reportConflict(conflict); return true; } @@ -374,6 +382,8 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); Node conflict = generateConflictAboveUpperBound(x_i); //unsat + + d_conflictVariable = x_i; reportConflict(conflict); return true; } @@ -386,6 +396,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(CHECK_AFTER_PIVOT){ Node possibleConflict = checkBasicForConflict(x_j); if(!possibleConflict.isNull()){ + d_conflictVariable = x_j; reportConflict(possibleConflict); return true; // unsat } |