From: Tim King Date: Fri, 18 May 2012 20:20:58 +0000 (+0000) Subject: This commit removes the dead psuedoboolean code. X-Git-Tag: cvc5-1.0.0~8153 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b93d45dab9513195d5604a069423ed13e173f49;p=cvc5.git This commit removes the dead psuedoboolean code. --- 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(REAL_TYPE)); } -/** Get the (singleton) type for pseudobooleans. */ -inline TypeNode NodeManager::pseudobooleanType() { - return TypeNode(mkTypeConst(PSEUDOBOOLEAN_TYPE)); -} - /** Get the (singleton) type for strings. */ inline TypeNode NodeManager::stringType() { return TypeNode(mkTypeConst(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; @@ -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 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()) { - case PSEUDOBOOLEAN_TYPE: - return t.getKind() == kind::TYPE_CONSTANT && - ( t.getConst() == BOOLEAN_TYPE || - t.getConst() == INTEGER_TYPE ); case INTEGER_TYPE: return t.getKind() == kind::TYPE_CONSTANT && t.getConst() == 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() == BOOLEAN_TYPE ) || - isPseudoboolean() || ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() ); } @@ -800,7 +796,6 @@ inline bool TypeNode::isInteger() const { return ( getKind() == kind::TYPE_CONSTANT && getConst() == 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() == PSEUDOBOOLEAN_TYPE ) || - ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() ); -} - inline bool TypeNode::isString() const { return getKind() == kind::TYPE_CONSTANT && getConst() == 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(); - out << num; - break; - } case kind::SUBRANGE_TYPE: out << '[' << n.getConst() << ']'; 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& 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& 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(); -// const Rational& rConst = right.getNode().getConst(); -// bool res = evaluateConstantPredicate(k, lConst, rConst); -// return Comparison(res); -// } - -// if(left.getNode().getType().isPseudoboolean()) { -// bool result; -// if(pbComparison(k, left.getNode(), right.getNode().getConst(), 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 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 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"