diff options
author | Tim King <taking@cs.nyu.edu> | 2018-01-07 16:46:16 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-07 16:46:16 -0800 |
commit | 20957db27201d594a83e0e5abe77875ed4932faf (patch) | |
tree | 47c665493a2a26d9ad50d2f53de310a7ce8193e0 /src/theory/arith/linear_equality.cpp | |
parent | 8497910df4d1c254b26f09c3dc5ee6191c970b12 (diff) |
Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)
* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 9d414fcd7..c97ed9714 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -1074,11 +1074,15 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr Assert(nbSgn != 0); if(nbSgn > 0){ - if(d_upperBoundDifference.nothing() || nbDiff <= d_upperBoundDifference){ + if (d_upperBoundDifference.nothing() + || nbDiff <= d_upperBoundDifference.value()) + { return false; } }else{ - if(d_lowerBoundDifference.nothing() || nbDiff >= d_lowerBoundDifference){ + if (d_lowerBoundDifference.nothing() + || nbDiff >= d_lowerBoundDifference.value()) + { return false; } } @@ -1162,14 +1166,14 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& if(d_variables.hasUpperBound(nb)){ ConstraintP ub = d_variables.getUpperBoundConstraint(nb); d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb); - Border border(ub, d_upperBoundDifference, false, NULL, true); + Border border(ub, d_upperBoundDifference.value(), false, NULL, true); Debug("handleBorders") << "push back increasing " << border << endl; d_increasing.push_back(border); } if(d_variables.hasLowerBound(nb)){ ConstraintP lb = d_variables.getLowerBoundConstraint(nb); d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb); - Border border(lb, d_lowerBoundDifference, false, NULL, false); + Border border(lb, d_lowerBoundDifference.value(), false, NULL, false); Debug("handleBorders") << "push back decreasing " << border << endl; d_decreasing.push_back(border); } |