This commit removes the dead psuedoboolean code.

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 593f3f7159c4f663245af0d0b89d2c8cbf0c7ead..2bcf5e18cb4199b36c362d87b56f4692f6738347 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -890,11 +890,6 @@ inline TypeNode NodeManager::realType() {
   return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
 }
 
-/** Get the (singleton) type for pseudobooleans. */
-inline TypeNode NodeManager::pseudobooleanType() {
-  return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE));
-}
-
 /** Get the (singleton) type for strings. */
 inline TypeNode NodeManager::stringType() {
   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index eaf10ba202b06c8936481cbc3dd4d684577b60f5..df222b684d6ecca9aa8891c8d174b3fe5b69538c 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -224,19 +224,6 @@ Type::operator RealType() const throw(AssertionException) {
   return RealType(*this);
 }
 
-/** Is this the pseudoboolean type? */
-bool Type::isPseudoboolean() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isPseudoboolean();
-}
-
-/** Cast to a pseudoboolean type */
-Type::operator PseudobooleanType() const throw(AssertionException) {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isPseudoboolean());
-  return PseudobooleanType(*this);
-}
-
 /** Is this the string type? */
 bool Type::isString() const {
   NodeManagerScope nms(d_nodeManager);
@@ -509,11 +496,6 @@ RealType::RealType(const Type& t) throw(AssertionException) :
   Assert(isNull() || isReal());
 }
 
-PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
-  Type(t) {
-  Assert(isNull() || isPseudoboolean());
-}
-
 StringType::StringType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isNull() || isString());

diff --git a/src/expr/type.h b/src/expr/type.h
index 76fccb37ba92953ed8d8c6964baa512a5a9d81c3..8e9190ac5a35ff09a85fda81118effd9a1a6678f 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -48,7 +48,6 @@ class NodeTemplate;
 class BooleanType;
 class IntegerType;
 class RealType;
-class PseudobooleanType;
 class StringType;
 class BitVectorType;
 class ArrayType;
@@ -256,18 +255,6 @@ public:
    */
   operator RealType() const throw(AssertionException);
 
-  /**
-   * Is this the pseudoboolean type?
-   * @return true if the type is the pseudoboolean type
-   */
-  bool isPseudoboolean() const;
-
-  /**
-   * Cast this type to a pseudoboolean type
-   * @return the PseudobooleanType
-   */
-  operator PseudobooleanType() const throw(AssertionException);
-
   /**
    * Is this the string type?
    * @return true if the type is the string type
@@ -488,17 +475,6 @@ public:
   RealType(const Type& type = Type()) throw(AssertionException);
 };/* class RealType */
 
-/**
- * Singleton class encapsulating the pseudoboolean type.
- */
-class CVC4_PUBLIC PseudobooleanType : public Type {
-
-public:
-
-  /** Construct from the base type */
-  PseudobooleanType(const Type& type) throw(AssertionException);
-};/* class PseudobooleanType */
-
 /**
  * Singleton class encapsulating the string type.
  */

diff --git a/src/expr/type.i b/src/expr/type.i
index 13ae9663e1611a80af6286bcc134bb8da332a8ad..0646ec8cd363a2ce971c6eadec58f9e7188f29d9 100644 (file)
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -17,7 +17,6 @@
 %rename(toBooleanType) CVC4::Type::operator BooleanType() const;
 %rename(toIntegerType) CVC4::Type::operator IntegerType() const;
 %rename(toRealType) CVC4::Type::operator RealType() const;
-%rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const;
 %rename(toStringType) CVC4::Type::operator StringType() const;
 %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
 %rename(toFunctionType) CVC4::Type::operator FunctionType() const;

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 4ddb01974591232c49b2c60ecacd796c6da4980c..3f5c3a032ab356b3c04d267291773c8cca67c2ca 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -77,10 +77,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
   }
   if(getKind() == kind::TYPE_CONSTANT) {
     switch(getConst<TypeConstant>()) {
-    case PSEUDOBOOLEAN_TYPE:
-      return t.getKind() == kind::TYPE_CONSTANT &&
-        ( t.getConst<TypeConstant>() == BOOLEAN_TYPE ||
-          t.getConst<TypeConstant>() == INTEGER_TYPE );
     case INTEGER_TYPE:
       return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
     default:

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 7fe3bc75ece5f677f33f6f22e663e0d7db6fa9ce..25b5e4bb3130c5ffc573eaed9c9641e64466bd2c 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -465,9 +465,6 @@ public:
   /** Is this the Real type? */
   bool isReal() const;
 
-  /** Is this the Pseudoboolean type? */
-  bool isPseudoboolean() const;
-
   /** Is this the String type? */
   bool isString() const;
 
@@ -792,7 +789,6 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
 inline bool TypeNode::isBoolean() const {
   return
     ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
-      isPseudoboolean() ||
     ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() );
 }
 
@@ -800,7 +796,6 @@ inline bool TypeNode::isInteger() const {
   return
     ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
     isSubrange() ||
-    isPseudoboolean() ||
     ( isPredicateSubtype() && getSubtypeBaseType().isInteger() );
 }
 
@@ -811,20 +806,13 @@ inline bool TypeNode::isReal() const {
     ( isPredicateSubtype() && getSubtypeBaseType().isReal() );
 }
 
-inline bool TypeNode::isPseudoboolean() const {
-  return
-    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ) ||
-    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
-}
-
 inline bool TypeNode::isString() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == STRING_TYPE;
 }
 
 inline bool TypeNode::isArray() const {
-  return getKind() == kind::ARRAY_TYPE ||
-    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+  return getKind() == kind::ARRAY_TYPE;
 }
 
 inline TypeNode TypeNode::getArrayIndexType() const {

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 1f147479ddbfa9b0006fc10b1368daf22b45a8ef..1df59adc491c41952347f791aca65013c40c5657 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -101,11 +101,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       break;
     }
-    case kind::CONST_PSEUDOBOOLEAN: {
-      const Pseudoboolean& num = n.getConst<Pseudoboolean>();
-      out << num;
-      break;
-    }
     case kind::SUBRANGE_TYPE:
       out << '[' << n.getConst<SubrangeBounds>() << ']';
       break;
@@ -123,9 +118,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       case BOOLEAN_TYPE:
         out << "BOOLEAN";
         break;
-      case PSEUDOBOOLEAN_TYPE:
-        out << "PSEUDOBOOLEAN";
-        break;
       case KIND_TYPE:
         out << "TYPE";
         break;

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index d18ec6e69f4f9be8e4e9c33af029e13ceca35577..62d885c062307eecfcc2dd2bc7a19835ed2926e9 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -234,7 +234,7 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
   Assert(!isTranslated(node), "atom already mapped!");
   // boolean variables are not theory literals
-  bool theoryLiteral = node.getKind() != kind::VARIABLE && !node.getType().isPseudoboolean();
+  bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
 
   if(node.getKind() == kind::CONST_BOOLEAN) {

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index e88ec073d97b1abd23567d3f86bc3d1df03d3dcf..5ce27eb46a394d92099bfa2733592281c6bf8274 100644 (file)
--- 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 03402a6f12f8bc1f7e7420a6fc9c672355b2657f..d877339b34846d5562cd71932d670e076644c635 100644 (file)
--- 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 e00d8dc5eac6c3daee09cac3a2bf4056d7ea35fb..8ffe68376283fedcafed557a57a1523908ea1444 100644 (file)
--- 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 6f8a462361b2182ce7188b5b182c825cb5ad9eb6..5fa6e08c6da3010388cbf231b69f3ea8df66d643 100644 (file)
--- 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 4aac76eacb237eeacb13d17aa580991f20544a88..431c82476076ac494c2b906dcf2259b4e8588dec 100644 (file)
--- 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;

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 4787457cf3166f1eafb5f402153dc436373c7abf..cded1e5a34b0b34f4d59587ac99e864a192df745 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -72,8 +72,6 @@ libutil_la_SOURCES = \
        boolean_simplification.cpp \
        ite_removal.h \
        ite_removal.cpp \
-       pseudoboolean.h \
-       pseudoboolean.cpp \
        node_visitor.h \
        index.h
 
@@ -171,7 +169,6 @@ EXTRA_DIST = \
        options.i \
        ascription_type.i \
        rational.i \
-       pseudoboolean.i \
        hash.i
 
 MOSTLYCLEANFILES = \

diff --git a/src/util/pseudoboolean.cpp b/src/util/pseudoboolean.cpp
deleted file mode 100644 (file)
index 655cd82..0000000
--- a/src/util/pseudoboolean.cpp
+++ /dev/null
@@ -1,49 +0,0 @@
-/*********************                                                        */
-/*! \file pseudoboolean.cpp
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute &of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A pseudoboolean constant
- **
- ** A pseudoboolean constant.
- **/
-
-#include "util/pseudoboolean.h"
-
-namespace CVC4 {
-
-Pseudoboolean::Pseudoboolean(bool b) :
-  d_value(b) {
-}
-
-Pseudoboolean::Pseudoboolean(int i) {
-  CheckArgument(i == 0 || i == 1, i);
-  d_value = (i == 1);
-}
-
-Pseudoboolean::Pseudoboolean(const CVC4::Integer& i) {
-  CheckArgument(i == 0 || i == 1, i);
-  d_value = (i == 1);
-}
-
-Pseudoboolean::operator bool() const {
-  return d_value;
-}
-
-Pseudoboolean::operator int() const {
-  return d_value ? 1 : 0;
-}
-
-Pseudoboolean::operator CVC4::Integer() const {
-  return d_value ? 1 : 0;
-}
-
-}/* CVC4 namespace */

diff --git a/src/util/pseudoboolean.h b/src/util/pseudoboolean.h
deleted file mode 100644 (file)
index 03cde2d..0000000
--- a/src/util/pseudoboolean.h
+++ /dev/null
@@ -1,54 +0,0 @@
-/*********************                                                        */
-/*! \file pseudoboolean.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A pseudoboolean constant
- **
- ** A pseudoboolean constant.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PSEUDOBOOLEAN_H
-#define __CVC4__PSEUDOBOOLEAN_H
-
-#include "util/integer.h"
-
-namespace CVC4 {
-
-class Pseudoboolean {
-  bool d_value;
-
-public:
-  Pseudoboolean(bool b);
-  Pseudoboolean(int i);
-  Pseudoboolean(const CVC4::Integer& i);
-
-  operator bool() const;
-  operator int() const;
-  operator CVC4::Integer() const;
-
-};/* class Pseudoboolean */
-
-struct PseudobooleanHashStrategy {
-  static inline size_t hash(CVC4::Pseudoboolean pb) {
-    return int(pb);
-  }
-};/* struct PseudobooleanHashStrategy */
-
-inline std::ostream& operator<<(std::ostream& os, CVC4::Pseudoboolean pb) {
-  return os << int(pb);
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PSEUDOBOOLEAN_H */

diff --git a/src/util/pseudoboolean.i b/src/util/pseudoboolean.i
deleted file mode 100644 (file)
index 78c373a..0000000
--- a/src/util/pseudoboolean.i
+++ /dev/null
@@ -1,11 +0,0 @@
-%{
-#include "util/pseudoboolean.h"
-%}
-
-%rename(toBool) CVC4::Pseudoboolean::operator bool() const;
-%rename(toInt) CVC4::Pseudoboolean::operator int() const;
-%rename(toInteger) CVC4::Pseudoboolean::operator CVC4::Integer() const;
-
-%ignore CVC4::operator<<(std::ostream&, CVC4::Pseudoboolean);
-
-%include "util/pseudoboolean.h"