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/pseudoboolean_proc.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/pseudoboolean_proc.cpp')
-rw-r--r-- | src/theory/arith/pseudoboolean_proc.cpp | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp index 230cfb7ca..1cdb90e20 100644 --- a/src/theory/arith/pseudoboolean_proc.cpp +++ b/src/theory/arith/pseudoboolean_proc.cpp @@ -15,10 +15,11 @@ ** \todo document this file **/ +#include "theory/arith/pseudoboolean_proc.h" + #include "base/output.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" -#include "theory/arith/pseudoboolean_proc.h" #include "theory/rewriter.h" namespace CVC4 { @@ -58,24 +59,30 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){ Polynomial p = Polynomial::parsePolynomial(l); clear(); - if(negated){ + if (negated) + { // (not (>= p r)) // (< p r) // (> (-p) (-r)) // (>= (-p) (-r +1)) d_off = (-r.getConst<Rational>()); - if(d_off.constValue().isIntegral()){ - d_off = d_off.constValue() + Rational(1) ; - }else{ - d_off = Rational(d_off.constValue().ceiling()); + if (d_off.value().isIntegral()) + { + d_off = d_off.value() + Rational(1); } - }else{ + else + { + d_off = Rational(d_off.value().ceiling()); + } + } + else + { // (>= p r) d_off = r.getConst<Rational>(); - d_off = Rational(d_off.constValue().ceiling()); + d_off = Rational(d_off.value().ceiling()); } - Assert(d_off.constValue().isIntegral()); + Assert(d_off.value().isIntegral()); int adj = negated ? -1 : 1; for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){ @@ -247,8 +254,8 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){ Debug("pbs::rewrites") << "failed " << std::endl; return; } - Assert(d_off.constValue().isIntegral()); - Integer off = d_off.constValue().ceiling(); + Assert(d_off.value().isIntegral()); + Integer off = d_off.value().ceiling(); // \sum pos >= \sum neg + off @@ -323,4 +330,3 @@ void PseudoBooleanProcessor::clear() { }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - |