diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-07 22:06:07 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-07 22:06:07 +0000 |
commit | 9f18a444d5c926cffa0532995a3a50cf74a98769 (patch) | |
tree | d4e9bca2bc79b063c26795d28f03fc624174e57d /src/theory | |
parent | c4a96dc3a0ace41e5f746207847a57ce1c6d4d33 (diff) |
Fixes a sign bug in the DioSolver.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 613ce8368..28fe86c70 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -375,6 +375,7 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ //For the rest of the equations keep reducing until the coefficient is one for(; iter != end; ++iter){ + Debug("arith::dio") << "next round : " << currentCoeff << " " << currentGcd << endl; TrailIndex inQueue = *iter; Constant iqc = d_trail[inQueue].d_eq.getPolynomial().getCoefficient(vl); if(!iqc.isZero()){ @@ -385,9 +386,9 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ // g = a*s + b*t Integer::extendedGcd(g, s, t, currentCoeff, inQueueCoeff); - Debug("arith::dio") << "extendedReduction" << endl; + Debug("arith::dio") << "extendedReduction : " << endl; Debug("arith::dio") << g << " = " << s <<"*"<< currentCoeff << " + " << t <<"*"<< inQueueCoeff << endl; - + Assert(g <= currentGcd); if(g < currentGcd){ if(s.sgn() == 0){ @@ -395,10 +396,10 @@ DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){ Assert(inQueueCoeff.divides(currentGcd)); current = *iter; currentCoeff = inQueueCoeff; - currentGcd = inQueueCoeff; + currentGcd = inQueueCoeff.abs(); }else{ + Debug("arith::dio") << "extendedReduction combine" << endl; - TrailIndex next = combineEqAtIndexes(current, s, inQueue, t); Assert(d_trail[next].d_eq.getPolynomial().getCoefficient(vl).getValue().getNumerator() == g); |