This commit removes the dead psuedoboolean code.

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;