From 20957db27201d594a83e0e5abe77875ed4932faf Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 7 Jan 2018 16:46:16 -0800 Subject: Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Removes RationalFromDoubleException. Replaces this with an explicit Maybe datatype. Makes Maybe CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex. --- src/theory/arith/linear_equality.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'src/theory/arith/linear_equality.cpp') 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); } -- cgit v1.2.3