diff options
author | Tim King <taking@cs.nyu.edu> | 2012-06-12 19:57:23 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-06-12 19:57:23 +0000 |
commit | 883b975204c9d08d3c6eeae56c9eb0191f850438 (patch) | |
tree | 420920a9b1fa4ddb2f692e393dc77ad359ca4e3c /src/theory | |
parent | 73e4e0b71e7c535b1005fe02d2303c9ed8cb3c62 (diff) |
Fix to yesterday's change in arithmetic.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/delta_rational.h | 4 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 22 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 4 |
3 files changed, 26 insertions, 4 deletions
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 12110fab4..ed256faa1 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -93,6 +93,10 @@ public: return *(this) + (a * negOne); } + DeltaRational operator-() const{ + return DeltaRational(-c, -k); + } + DeltaRational operator/(const Rational& a) const{ CVC4::Rational tmpC = c/a; CVC4::Rational tmpK = k/a; diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 986df5f80..c90be63b9 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -532,10 +532,26 @@ DeltaRational Comparison::normalizedDeltaRational() const { case kind::EQUAL: case kind::DISTINCT: { - Monomial firstRight = getRight().getHead(); + Polynomial right = getRight(); + Monomial firstRight = right.getHead(); if(firstRight.isConstant()){ - return DeltaRational(firstRight.getConstant().getValue(), 0); - }else{ + DeltaRational c = DeltaRational(firstRight.getConstant().getValue(), 0); + Polynomial left = getLeft(); + if(!left.allIntegralVariables()){ + return c; + //this is a qpolynomial and the sign of the leading + //coefficient will not change after the diff below + } else{ + // the polynomial may be a z polynomial in which case + // taking the diff is the simplest and obviously correct means + Polynomial diff = right.singleton() ? left : left - right.getTail(); + if(diff.leadingCoefficientIsPositive()){ + return c; + }else{ + return -c; + } + } + }else{ // The constant is 0 sign cannot change return DeltaRational(0, 0); } } diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index b5475586a..8fb99a9ae 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -493,7 +493,9 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar const Rational& coeff = entry.getCoefficient(); bool weakening = false; Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar); - Debug("weak") << "weak : " << weakening << " " << c->assertedToTheTheory() + Debug("weak") << "weak : " << weakening << " " + << c->assertedToTheTheory() << " " + << d_partialModel.getAssignment(v) << " " << c << endl << c->explainForConflict() << endl; anyWeakenings = anyWeakenings || weakening; |