diff options
Diffstat (limited to 'src/theory/arith/normal_form.cpp')
-rw-r--r-- | src/theory/arith/normal_form.cpp | 215 |
1 files changed, 0 insertions, 215 deletions
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 6f8a46236..5fa6e08c6 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -984,28 +984,6 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& l, const Polynomia } } -// Comparison Comparison::normalize(Comparison c) { -// if(c.isConstant()){ -// return c.evaluateConstant(); -// }else{ -// Comparison c0 = c.constantInLefthand() ? c.cancelLefthandConstant() : c; -// Comparison c1 = c0.normalizeLeadingCoefficientPositive(); -// if(c1.allIntegralVariables()){ -// //All Integer Variable Case -// Comparison integer0 = c1.multiplyByDenominatorLCM(); -// Comparison integer1 = integer0.divideByLefthandGCD(); -// Comparison integer2 = integer1.tightenIntegralConstraint(); -// Assert(integer2.isBoolean() || integer2.isIntegerNormalForm()); -// return integer2; -// }else{ -// //Mixed case -// Comparison mixed = c1.divideByLeadingCoefficient(); -// Assert(mixed.isMixedNormalForm()); -// return mixed; -// } -// } -// } - bool Comparison::isBoolean() const { return getNode().getKind() == kind::CONST_BOOLEAN; } @@ -1015,199 +993,6 @@ bool Comparison::debugIsIntegral() const{ return getLeft().isIntegral() && getRight().isIntegral(); } -// Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) { -// Assert(isRelationOperator(k)); -// if(left.isConstant()) { -// const Rational& lConst = left.getNode().getConst<Rational>(); -// const Rational& rConst = right.getNode().getConst<Rational>(); -// bool res = evaluateConstantPredicate(k, lConst, rConst); -// return Comparison(res); -// } - -// if(left.getNode().getType().isPseudoboolean()) { -// bool result; -// if(pbComparison(k, left.getNode(), right.getNode().getConst<Rational>(), result)) { -// return Comparison(result); -// } -// } - -// return Comparison(toNode(k, left, right), k, left, right); -// } - -// Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Polynomial& right) { -// Assert(isRelationOperator(k)); -// return Comparison(toNode(k, left, right), k, left, right); -// } - - -// bool Comparison::constantInLefthand() const{ -// return getLeft().containsConstant(); -// } - -// Comparison Comparison::cancelLefthandConstant() const { -// if(constantInLefthand()){ -// Monomial constantHead = getLeft().getHead(); -// Assert(constantHead.isConstant()); - -// Constant constant = constantHead.getConstant(); -// Constant negativeConstantHead = -constant; -// return addConstant(negativeConstantHead); -// }else{ -// return *this; -// } -// } - -// Integer OrderedPolynomialPair::denominatorLCM() const { -// // Get the coefficients to be all integers. -// Integer firstDenominatorLCM = getFirst().denominatorLCM(); -// Integer secondDenominatorLCM = getSecond().denominatorLCM(); -// Integer denominatorLCM = secondDenominatorLCM.lcm(secondDenominatorLCM); -// Assert(denominatorLCM.sgn() > 0); -// return denominatorLCM; -// } - -// bool Comparison::isIntegral() const { -// return getRight().isIntegral() && getLeft().isIntegral(); -// } - -// bool OrderedPolynomialPair::isConstant() const { -// return getFirst().isConstant() && getSecond().isConstant(); -// } - -// bool OrderedPolynomialPair::evaluateConstant(Kind k) const { -// Assert(getFirst().isConstant()); -// Assert(getSecond().isConstant()); - -// const Rational& firstConst = getFirst().asConstant(); -// const Rational& secondConst = getSecond().asConstant(); - -// return evaluateConstantPredicate(k, firstConst, secondConst); -// } - -// OrderedPolynomialPair OrderedPolynomialPair::divideByGCD() const { -// Assert(isIntegral()); - -// Integer fGcd = getFirst().gcd(); -// Integer sGcd = getSecond().gcd(); - -// Integer gcd = fGcd.gcd(sGcd); -// Polynomial newFirst = getFirst().exactDivide(gcd); -// Polynomial newSecond = getSecond().exactDivide(gcd); - -// return OrderedPolynomialPair(newFirst, newSecond); -// } - -// OrderedPolynomialPair OrderedPolynomialPair::divideByLeadingFirstCoefficient() const { -// //Handle the rational/mixed case -// Monomial head = getFirst().getHead(); -// Constant leadingCoefficient = head.getConstant(); -// Assert(!leadingCoefficient.isZero()); - -// Constant inverse = leadingCoefficient.inverse(); - -// return multiplyConstant(inverse); -// } - -// OrderedPolynomialPair OrderedPolynomialPair::multiplyConstant(const Constant& c) const { -// return OrderedPolynomialPair(getFirst() * c, getSecond() * c); -// } - -// Comparison Comparison::divideByLeadingCoefficient() const { -// //Handle the rational/mixed case -// Monomial head = getLeft().getHead(); -// Constant leadingCoefficient = head.getConstant(); -// Assert(!leadingCoefficient.isZero()); - -// Constant inverse = leadingCoefficient.inverse(); - -// return multiplyConstant(inverse); -// } - - - -// Comparison Comparison::tightenIntegralConstraint() const { -// Assert(getLeft().isIntegral()); - -// if(getRight().isIntegral()){ -// return *this; -// }else{ -// switch(getKind()){ -// case kind::EQUAL: -// //If the gcd of the left hand side does not cleanly divide the right hand side, -// //this is unsatisfiable in the theory of Integers. -// return Comparison(false); -// case kind::GEQ: -// case kind::GT: -// { -// //(>= l (/ n d)) -// //(>= l (ceil (/ n d))) -// //This also hold for GT as (ceil (/ n d)) > (/ n d) -// Integer ceilr = getRight().getValue().ceiling(); -// Constant newRight = Constant::mkConstant(ceilr); -// return Comparison(toNode(kind::GEQ, getLeft(), newRight),kind::GEQ, getLeft(),newRight); -// } -// case kind::LEQ: -// case kind::LT: -// { -// //(<= l (/ n d)) -// //(<= l (floor (/ n d))) -// //This also hold for LT as (floor (/ n d)) < (/ n d) -// Integer floor = getRight().getValue().floor(); -// Constant newRight = Constant::mkConstant(floor); -// return Comparison(toNode(kind::LEQ, getLeft(), newRight),kind::LEQ, getLeft(),newRight); -// } -// default: -// Unreachable(); -// } -// } -// } - -// bool Comparison::isIntegerNormalForm() const{ -// if(constantInLefthand()){ return false; } -// else if(getLeft().getHead().getConstant().isNegative()){ return false; } -// else if(!isIntegral()){ return false; } -// else { -// return getLeft().gcd() == 1; -// } -// } -// bool Comparison::isMixedNormalForm() const { -// if(constantInLefthand()){ return false; } -// else if(allIntegralVariables()) { return false; } -// else{ -// return getLeft().getHead().getConstant().getValue() == 1; -// } -// } - -// Comparison Comparison::normalize(Comparison c) { -// if(c.isConstant()){ -// return c.evaluateConstant(); -// }else{ -// Comparison c0 = c.constantInLefthand() ? c.cancelLefthandConstant() : c; -// Comparison c1 = c0.normalizeLeadingCoefficientPositive(); -// if(c1.allIntegralVariables()){ -// //All Integer Variable Case -// Comparison integer0 = c1.multiplyByDenominatorLCM(); -// Comparison integer1 = integer0.divideByLefthandGCD(); -// Comparison integer2 = integer1.tightenIntegralConstraint(); -// Assert(integer2.isBoolean() || integer2.isIntegerNormalForm()); -// return integer2; -// }else{ -// //Mixed case -// Comparison mixed = c1.divideByLeadingCoefficient(); -// Assert(mixed.isMixedNormalForm()); -// return mixed; -// } -// } -// } - -// Comparison Comparison::mkNormalComparison(Kind k, const Polynomial& left, const Constant& right) { -// Comparison cmp = mkComparison(k,left,right); -// Comparison normalized = cmp.normalize(cmp); -// Assert(normalized.isNormalForm()); -// return normalized; -// } - - Kind Comparison::comparisonKind(TNode literal){ switch(literal.getKind()){ case kind::CONST_BOOLEAN: |