summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_manager.h5
-rw-r--r--src/expr/type.cpp18
-rw-r--r--src/expr/type.h24
-rw-r--r--src/expr/type.i1
-rw-r--r--src/expr/type_node.cpp4
-rw-r--r--src/expr/type_node.h14
-rw-r--r--src/printer/cvc/cvc_printer.cpp8
-rw-r--r--src/prop/cnf_stream.cpp2
-rw-r--r--src/theory/arith/arith_static_learner.cpp38
-rw-r--r--src/theory/arith/arith_static_learner.h2
-rw-r--r--src/theory/arith/kinds12
-rw-r--r--src/theory/arith/normal_form.cpp215
-rw-r--r--src/theory/arith/theory_arith.h14
-rw-r--r--src/util/Makefile.am3
-rw-r--r--src/util/pseudoboolean.cpp49
-rw-r--r--src/util/pseudoboolean.h54
-rw-r--r--src/util/pseudoboolean.i11
17 files changed, 6 insertions, 468 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 593f3f715..2bcf5e18c 100644
--- 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 eaf10ba20..df222b684 100644
--- 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 76fccb37b..8e9190ac5 100644
--- 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;
@@ -257,18 +256,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
*/
@@ -489,17 +476,6 @@ public:
};/* 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.
*/
class CVC4_PUBLIC StringType : public Type {
diff --git a/src/expr/type.i b/src/expr/type.i
index 13ae9663e..0646ec8cd 100644
--- 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 4ddb01974..3f5c3a032 100644
--- 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 7fe3bc75e..25b5e4bb3 100644
--- 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 1f147479d..1df59adc4 100644
--- 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 d18ec6e69..62d885c06 100644
--- 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 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;
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 4787457cf..cded1e5a3 100644
--- 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
index 655cd8277..000000000
--- 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
index 03cde2d98..000000000
--- 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
index 78c373aa1..000000000
--- 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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback