summaryrefslogtreecommitdiff
path: root/src/theory/arith/normal_form.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/normal_form.cpp')
-rw-r--r--src/theory/arith/normal_form.cpp215
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback