diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-18 20:20:58 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-18 20:20:58 +0000 |
commit | 3b93d45dab9513195d5604a069423ed13e173f49 (patch) | |
tree | 96497114c06755a14efe0d30c680703c9aa5380b /src/theory/arith | |
parent | 76b8bdc51693af0867de94fe6002e8a8bec9e5f9 (diff) |
This commit removes the dead psuedoboolean code.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 38 | ||||
-rw-r--r-- | src/theory/arith/arith_static_learner.h | 2 | ||||
-rw-r--r-- | src/theory/arith/kinds | 12 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 215 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 14 |
5 files changed, 4 insertions, 277 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index e88ec073d..5ce27eb46 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -199,21 +199,6 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet } } -void ArithStaticLearner::replaceWithPseudoboolean(TNode var) { - AssertArgument(var.getMetaKind() == kind::metakind::VARIABLE, var); - // [MGD 10/21/2011] disable pseudobooleans for now (as discussed in today's meeting) - /* - TypeNode pbType = NodeManager::currentNM()->pseudobooleanType(); - Node pbVar = NodeManager::currentNM()->mkVar(string("PB[") + var.toString() + ']', pbType); - d_pbSubstitutions.addSubstitution(var, pbVar); - - if(Debug.isOn("pb")) { - Expr::printtypes::Scope pts(Debug("pb"), true); - Debug("pb") << "will replace " << var << " with " << pbVar << endl; - } - */ -} - void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ Assert(n.getKind() == kind::ITE); Assert(n[0].getKind() != EQUAL); @@ -399,27 +384,6 @@ void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuild } } -void ArithStaticLearner::checkBoundsForPseudobooleanReplacement(TNode n) { - NodeToMinMaxMap::iterator minFind = d_minMap.find(n); - NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n); - - if( n.getType().isInteger() && - minFind != d_minMap.end() && - maxFind != d_maxMap.end() && - ( ( (*minFind).second.getNoninfinitesimalPart() == 1 && - (*minFind).second.getInfinitesimalPart() == 0 ) || - ( (*minFind).second.getNoninfinitesimalPart() == 0 && - (*minFind).second.getInfinitesimalPart() > 0 ) ) && - ( ( (*maxFind).second.getNoninfinitesimalPart() == 1 && - (*maxFind).second.getInfinitesimalPart() == 0 ) || - ( (*maxFind).second.getNoninfinitesimalPart() == 2 && - (*maxFind).second.getInfinitesimalPart() < 0 ) ) ) { - // eligible for pseudoboolean replacement - Debug("pb") << "eligible for pseudoboolean replacement: " << n << endl; - replaceWithPseudoboolean(n); - } -} - void ArithStaticLearner::addBound(TNode n) { NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]); @@ -436,7 +400,6 @@ void ArithStaticLearner::addBound(TNode n) { if (maxFind == d_maxMap.end() || maxFind->second > bound) { d_maxMap[n[0]] = bound; Debug("arith::static") << "adding bound " << n << endl; - checkBoundsForPseudobooleanReplacement(n[0]); } break; case kind::GT: @@ -446,7 +409,6 @@ void ArithStaticLearner::addBound(TNode n) { if (minFind == d_minMap.end() || minFind->second < bound) { d_minMap[n[0]] = bound; Debug("arith::static") << "adding bound " << n << endl; - checkBoundsForPseudobooleanReplacement(n[0]); } break; default: diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 03402a6f1..d877339b3 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -78,13 +78,11 @@ private: void postProcess(NodeBuilder<>& learned); - void replaceWithPseudoboolean(TNode var); void iteMinMax(TNode n, NodeBuilder<>& learned); void iteConstant(TNode n, NodeBuilder<>& learned); void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned); - void checkBoundsForPseudobooleanReplacement(TNode n); /** These fields are designed to be accessable to ArithStaticLearner methods. */ class Statistics { diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index e00d8dc5e..8ffe68376 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -34,12 +34,6 @@ sort INTEGER_TYPE \ "NodeManager::currentNM()->mkConst(Rational(0))" \ "expr/node_manager.h" \ "Integer type" -sort PSEUDOBOOLEAN_TYPE \ - 2 \ - well-founded \ - "NodeManager::currentNM()->mkConst(Pseudoboolean(0))" \ - "expr/node_manager.h" \ - "Pseudoboolean type" constant SUBRANGE_TYPE \ ::CVC4::SubrangeBounds \ @@ -60,12 +54,6 @@ constant CONST_RATIONAL \ "util/rational.h" \ "a multiple-precision rational constant" -constant CONST_PSEUDOBOOLEAN \ - ::CVC4::Pseudoboolean \ - ::CVC4::PseudobooleanHashStrategy \ - "util/pseudoboolean.h" \ - "a pseudoboolean constant" - operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" 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: diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 4aac76eac..431c82476 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -112,31 +112,25 @@ private: /** * (For the moment) the type hierarchy goes as: - * PsuedoBoolean <: Integer <: Real + * Integer <: Real * The type number of a variable is an integer representing the most specific * type of the variable. The possible values of type number are: */ enum ArithType { ATReal = 0, - ATInteger = 1, - ATPsuedoBoolean = 2 + ATInteger = 1 }; std::vector<ArithType> d_variableTypes; inline ArithType nodeToArithType(TNode x) const { - return x.getType().isPseudoboolean() ? ATPsuedoBoolean : - (x.getType().isInteger() ? ATInteger : ATReal); + return (x.getType().isInteger() ? ATInteger : ATReal); } - /** Returns true if x is of type Integer or PsuedoBoolean. */ + /** Returns true if x is of type Integer. */ inline bool isInteger(ArithVar x) const { return d_variableTypes[x] >= ATInteger; } - /** Returns true if x is of type PsuedoBoolean. */ - inline bool isPsuedoBoolean(ArithVar x) const { - return d_variableTypes[x] == ATPsuedoBoolean; - } /** This is the set of variables initially introduced as slack variables. */ std::vector<bool> d_slackVars; |