diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-09 14:33:35 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-09 16:31:11 -0400 |
commit | 588468e4800d790aecd35725c123d21f3e7a86ae (patch) | |
tree | 3732e3bb7a6d7a8cad818651b3b18a15a55256ff /src/theory/arith | |
parent | 85377f73a331b334437aa0d50d15c81e905869c1 (diff) |
Changing the integer normal form to increase matching.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/normal_form.cpp | 33 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 9 |
2 files changed, 34 insertions, 8 deletions
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 8454ca210..1ebbe49e0 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -745,9 +745,8 @@ bool Comparison::isNormalGEQ() const { return false; }else{ if(left.isIntegral()){ - return left.denominatorLCMIsOne() && left.numeratorGCDIsOne(); + return left.signNormalizedReducedSum(); }else{ - Debug("nf::tmp") << "imme sdfhkdjfh "<< left.leadingCoefficientIsAbsOne() << endl; return left.leadingCoefficientIsAbsOne(); } } @@ -768,7 +767,7 @@ bool Comparison::isNormalLT() const { return false; }else{ if(left.isIntegral()){ - return left.denominatorLCMIsOne() && left.numeratorGCDIsOne(); + return left.signNormalizedReducedSum(); }else{ return left.leadingCoefficientIsAbsOne(); } @@ -889,6 +888,7 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){ Polynomial left = sp.getPolynomial(); Rational right = - (sp.getConstant().getValue()); + Monomial m = left.getHead(); Assert(!m.isConstant()); @@ -899,16 +899,31 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){ Polynomial newLeft = left * mult; Rational rightMult = right * mult; + bool negateResult = false; + if(!newLeft.leadingCoefficientIsPositive()){ + // multiply by -1 + // a: left >= right or b: left > right + // becomes + // a: -left <= -right or b: -left < -right + // a: not (-left > -right) or b: (not -left >= -right) + newLeft = -newLeft; + rightMult = -rightMult; + k = (kind::GT == k) ? kind::GEQ : kind::GT; + negateResult = true; + // the later stages handle: + // a: not (-left >= -right + 1) or b: (not -left >= -right) + } + Node result = Node::null(); if(rightMult.isIntegral()){ if(k == kind::GT){ // (> p z) // (>= p (+ z 1)) Constant rightMultPlusOne = Constant::mkConstant(rightMult + 1); - return toNode(kind::GEQ, newLeft, rightMultPlusOne); + result = toNode(kind::GEQ, newLeft, rightMultPlusOne); }else{ Constant newRight = Constant::mkConstant(rightMult); - return toNode(kind::GEQ, newLeft, newRight); + result = toNode(kind::GEQ, newLeft, newRight); } }else{ //(>= l (/ n d)) @@ -916,7 +931,13 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){ //This also hold for GT as (ceil (/ n d)) > (/ n d) Integer ceilr = rightMult.ceiling(); Constant ceilRight = Constant::mkConstant(ceilr); - return toNode(kind::GEQ, newLeft, ceilRight); + result = toNode(kind::GEQ, newLeft, ceilRight); + } + Assert(!result.isNull()); + if(negateResult){ + return result.notNode(); + }else{ + return result; } } diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index bcf9cbfa4..c6af7010f 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -76,12 +76,13 @@ namespace arith { * (exists realMonomial (monomialList qpolynomial)) * abs(monomialCoefficient (head (monomialList qpolynomial))) == 1 * - * integer_cmp := (<= zpolynomial constant) + * integer_cmp := (>= zpolynomial constant) * where * not (exists constantMonomial (monomialList zpolynomial)) * (forall integerMonomial (monomialList zpolynomial)) * the gcd of all numerators of coefficients is 1 * the denominator of all coefficients and the constant is 1 + * the leading coefficient is positive * * rational_eq := (= qvarlist qpolynomial) * where @@ -939,6 +940,10 @@ public: bool denominatorLCMIsOne() const; bool numeratorGCDIsOne() const; + bool signNormalizedReducedSum() const { + return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne(); + } + /** * Returns the Least Common Multiple of the denominators of the coefficients * of the monomials. @@ -1265,7 +1270,7 @@ private: * Creates a comparison equivalent to (k l 0). * k is either GT or GEQ. * It is not the case that all variables in l are integral. - */ + */ static Node mkRatInequality(Kind k, const Polynomial& l); public: |