diff options
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 */ - |