diff options
author | Tim King <taking@cs.nyu.edu> | 2012-02-16 00:54:12 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-02-16 00:54:12 +0000 |
commit | 67c6e89c904f76a268f9297b7589559a262583e0 (patch) | |
tree | 931766422986af03259c2c3c75221fb61be523e9 /src/theory/arith/dio_solver.cpp | |
parent | 9a0a59d5c85c4a1d2469f43e9d2b433e156810ba (diff) |
Last commit accidentally lacked r2778 and r2779 from integer2. I have manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.
Diffstat (limited to 'src/theory/arith/dio_solver.cpp')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index dead34807..1e47d6cdd 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -238,7 +238,7 @@ void DioSolver::enqueueInputConstraints(){ TrailIndex i = d_inputConstraints[curr].d_trailPos; TrailIndex j = applyAllSubstitutionsToIndex(i); - if(!(triviallySat(j) || anyCoefficientExceedsMaximum(j))){ + if(!triviallySat(j)){ if(triviallyUnsat(j)){ raiseConflict(j); }else{ @@ -247,7 +247,7 @@ void DioSolver::enqueueInputConstraints(){ if(!inConflict()){ if(triviallyUnsat(k)){ raiseConflict(k); - }else if(!triviallySat(k)){ + }else if(!(triviallySat(k) || anyCoefficientExceedsMaximum(k))){ pushToQueueBack(k); } } @@ -772,10 +772,10 @@ void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){ if(triviallyUnsat(nextTI)){ raiseConflict(nextTI); - }else if(!(triviallySat(nextTI) || anyCoefficientExceedsMaximum(nextTI))){ + }else if(!triviallySat(nextTI)){ TrailIndex nextNextTI = reduceByGCD(nextTI); - if(!inConflict()){ + if(!(inConflict() || anyCoefficientExceedsMaximum(nextNextTI))){ Assert(queueConditions(nextNextTI)); d_currentF[writeIter] = nextNextTI; ++writeIter; |