summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am3
-rw-r--r--src/expr/expr_manager_template.cpp39
-rw-r--r--src/expr/expr_manager_template.h4
-rw-r--r--src/expr/node_manager.cpp45
-rw-r--r--src/expr/node_manager.h25
-rw-r--r--src/expr/predicate.cpp99
-rw-r--r--src/expr/predicate.h72
-rw-r--r--src/expr/predicate.i12
-rw-r--r--src/expr/type.cpp33
-rw-r--r--src/expr/type.h4
-rw-r--r--src/expr/type_node.cpp124
-rw-r--r--src/expr/type_node.h78
12 files changed, 20 insertions, 518 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index e45c765c0..859d5a312 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -61,8 +61,6 @@ libexpr_la_SOURCES = \
variable_type_map.h \
datatype.h \
datatype.cpp \
- predicate.h \
- predicate.cpp \
record.cpp \
record.h \
uninterpreted_constant.cpp \
@@ -103,7 +101,6 @@ EXTRA_DIST = \
kind.i \
expr.i \
record.i \
- predicate.i \
variable_type_map.i \
uninterpreted_constant.i
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 735d531e1..d6249d6fd 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -842,43 +842,6 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
}
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return PredicateSubtype(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-*/
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return PredicateSubtype(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-*/
-
-Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return SubrangeType(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
/**
* Get the type for the given Expr and optionally do type checking.
*
@@ -1062,8 +1025,6 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
return to->mkTypeConst(n.getConst<TypeConstant>());
} else if(n.getKind() == kind::BITVECTOR_TYPE) {
return to->mkBitVectorType(n.getConst<BitVectorSize>());
- } else if(n.getKind() == kind::SUBRANGE_TYPE) {
- return to->mkSubrangeType(n.getSubrangeBounds());
}
Type from_t = from->toType(n);
Type& to_t = vmap.d_typeMap[from_t];
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 07dc88fd3..8719d8ef4 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -461,8 +461,8 @@ public:
/**
* Make an integer subrange type as defined by the argument.
*/
- Type mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingException);
+ //Type mkSubrangeType(const SubrangeBounds& bounds)
+ // throw(TypeCheckingException);
/** Get the type of an expression */
Type getType(Expr e, bool check = false)
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index b746e0de9..f7a1d98d6 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -506,51 +506,6 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
}
-TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingExceptionPrivate) {
-
- Node lambdan = Node::fromExpr(lambda);
-
- if(lambda.isNull()) {
- throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
- }
-
- TypeNode tn = lambdan.getType();
- if(! tn.isPredicateLike() ||
- tn.getArgTypes().size() != 1) {
- stringstream ss;
- ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
- throw TypeCheckingExceptionPrivate(lambdan, ss.str());
- }
-
- return TypeNode(mkTypeConst(Predicate(lambda)));
-}
-
-TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingExceptionPrivate) {
-
- Node lambdan = Node::fromExpr(lambda);
-
- if(lambda.isNull()) {
- throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
- }
-
- TypeNode tn = lambdan.getType();
- if(! tn.isPredicateLike() ||
- tn.getArgTypes().size() != 1) {
- stringstream ss;
- ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
- throw TypeCheckingExceptionPrivate(lambdan, ss.str());
- }
-
- return TypeNode(mkTypeConst(Predicate(lambda, witness)));
-}
-
-TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingExceptionPrivate) {
- return TypeNode(mkTypeConst(bounds));
-}
-
TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
if( index==types.size() ){
if( d_data.isNull() ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1d1150842..44c116558 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -875,31 +875,6 @@ public:
TypeNode mkSortConstructor(const std::string& name, size_t arity);
/**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression. A TypeCheckingExceptionPrivate can be thrown if
- * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
- * proving that the resulting predicate subtype is inhabited.
- */
- TypeNode mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression and whose non-emptiness is witnessed by the given
- * witness. A TypeCheckingExceptionPrivate can be thrown if lambda
- * is not a LAMBDA, or is ill-typed, or if the witness is not a
- * witness or ill-typed.
- */
- TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Make an integer subrange type as defined by the argument.
- */
- TypeNode mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingExceptionPrivate);
-
- /**
* Get the type for the given node and optionally do type checking.
*
* Initial type computation will be near-constant time if
diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
deleted file mode 100644
index eaf587110..000000000
--- a/src/expr/predicate.cpp
+++ /dev/null
@@ -1,99 +0,0 @@
-/********************* */
-/*! \file predicate.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Representation of predicates for predicate subtyping
- **
- ** Simple class to represent predicates for predicate subtyping.
- ** Instances of this class are carried as the payload of
- ** the CONSTANT-metakinded SUBTYPE_TYPE types.
- **/
-#include "expr/predicate.h"
-
-#include "base/cvc4_assert.h"
-#include "expr/expr.h"
-
-
-using namespace std;
-
-namespace CVC4 {
-
-Predicate::Predicate(const Predicate& p)
- : d_predicate(new Expr(p.getExpression()))
- , d_witness(new Expr(p.getWitness()))
-{}
-
-Predicate::Predicate(const Expr& e) throw(IllegalArgumentException)
- : d_predicate(new Expr(e))
- , d_witness(new Expr())
-{
- PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
- PrettyCheckArgument(e.getType().isPredicate(), e,
- "Expression given is not predicate");
- PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
- "Expression given is not predicate of a single argument");
-}
-
-Predicate::Predicate(const Expr& e, const Expr& w)
- throw(IllegalArgumentException)
- : d_predicate(new Expr(e))
- , d_witness(new Expr(w))
-{
- PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
- PrettyCheckArgument(e.getType().isPredicate(), e,
- "Expression given is not predicate");
- PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
- "Expression given is not predicate of a single argument");
-}
-
-Predicate::~Predicate() {
- delete d_predicate;
- delete d_witness;
-}
-
-Predicate& Predicate::operator=(const Predicate& p){
- (*d_predicate) = p.getExpression();
- (*d_witness) = p.getWitness();
- return *this;
-}
-
-
-// Predicate::operator Expr() const {
-// return d_predicate;
-// }
-
-const Expr& Predicate::getExpression() const {
- return *d_predicate;
-}
-
-const Expr& Predicate::getWitness() const {
- return *d_witness;
-}
-
-bool Predicate::operator==(const Predicate& p) const {
- return getExpression() == p.getExpression() &&
- getWitness() == p.getWitness();
-}
-
-std::ostream& operator<<(std::ostream& out, const Predicate& p) {
- out << p.getExpression();
- const Expr& witness = p.getWitness();
- if(! witness.isNull()) {
- out << " : " << witness;
- }
- return out;
-}
-
-size_t PredicateHashFunction::operator()(const Predicate& p) const {
- ExprHashFunction h;
- return h(p.getWitness()) * 5039 + h(p.getExpression());
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/predicate.h b/src/expr/predicate.h
deleted file mode 100644
index 99e589fcd..000000000
--- a/src/expr/predicate.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/********************* */
-/*! \file predicate.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Representation of predicates for predicate subtyping
- **
- ** Simple class to represent predicates for predicate subtyping.
- ** Instances of this class are carried as the payload of
- ** the CONSTANT-metakinded SUBTYPE_TYPE types.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PREDICATE_H
-#define __CVC4__PREDICATE_H
-
-#include "base/exception.h"
-
-namespace CVC4 {
-
-class Predicate;
-
-std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
-
-struct CVC4_PUBLIC PredicateHashFunction {
- size_t operator()(const Predicate& p) const;
-};/* class PredicateHashFunction */
-
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-class CVC4_PUBLIC Expr;
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-class CVC4_PUBLIC Predicate {
-public:
-
- Predicate(const Expr& e) throw(IllegalArgumentException);
- Predicate(const Expr& e, const Expr& w) throw(IllegalArgumentException);
-
- Predicate(const Predicate& p);
- ~Predicate();
- Predicate& operator=(const Predicate& p);
-
- //operator Expr() const;
-
- const Expr& getExpression() const;
- const Expr& getWitness() const;
-
- bool operator==(const Predicate& p) const;
-
- friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p);
- friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
-
-private:
- Expr* d_predicate;
- Expr* d_witness;
-};/* class Predicate */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PREDICATE_H */
diff --git a/src/expr/predicate.i b/src/expr/predicate.i
deleted file mode 100644
index aa80a98b5..000000000
--- a/src/expr/predicate.i
+++ /dev/null
@@ -1,12 +0,0 @@
-%{
-#include "expr/predicate.h"
-%}
-
-%rename(equals) CVC4::Predicate::operator==(const Predicate&) const;
-%rename(toExpr) CVC4::Predicate::operator Expr() const;
-
-%rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const;
-
-%ignore CVC4::operator<<(std::ostream&, const Predicate&);
-
-%include "expr/predicate.h"
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index bb3ce0f58..8bcb0f8d5 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -329,20 +329,6 @@ bool Type::isSortConstructor() const {
return d_typeNode->isSortConstructor();
}
-/** Is this a predicate subtype */
-/* - not in release 1.0
-bool Type::isPredicateSubtype() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->isPredicateSubtype();
-}
-*/
-
-/** Is this an integer subrange */
-bool Type::isSubrange() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->isSubrange();
-}
-
size_t FunctionType::getArity() const {
return d_typeNode->getNumChildren() - 1;
}
@@ -505,20 +491,6 @@ SortConstructorType::SortConstructorType(const Type& t)
PrettyCheckArgument(isNull() || isSortConstructor(), this);
}
-/* - not in release 1.0
-PredicateSubtype::PredicateSubtype(const Type& t)
- throw(IllegalArgumentException) :
- Type(t) {
- PrettyCheckArgument(isNull() || isPredicateSubtype(), this);
-}
-*/
-
-SubrangeType::SubrangeType(const Type& t)
- throw(IllegalArgumentException) :
- Type(t) {
- PrettyCheckArgument(isNull() || isSubrange(), this);
-}
-
unsigned BitVectorType::getSize() const {
return d_typeNode->getBitVectorSize();
}
@@ -666,11 +638,6 @@ Type PredicateSubtype::getParentType() const {
}
*/
-SubrangeBounds SubrangeType::getSubrangeBounds() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getSubrangeBounds();
-}
-
size_t TypeHashFunction::operator()(const Type& t) const {
return TypeNodeHashFunction()(NodeManager::fromType(t));
}
diff --git a/src/expr/type.h b/src/expr/type.h
index 04b2907ff..25f0c5436 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -372,7 +372,7 @@ public:
* Is this an integer subrange type?
* @return true if this is an integer subrange type
*/
- bool isSubrange() const;
+ //bool isSubrange() const;
/**
* Outputs a string representation of this type to the stream.
@@ -584,7 +584,6 @@ public:
Type getParentType() const;
};/* class PredicateSubtype */
-#endif /* 0 */
/**
* Class encapsulating an integer subrange type.
@@ -600,6 +599,7 @@ public:
SubrangeBounds getSubrangeBounds() const;
};/* class SubrangeType */
+#endif /* 0 */
/**
* Class encapsulating the bit-vector type.
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 6e16ee9fa..383a31dd0 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -106,15 +106,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
return false;
}
}
- if(isSubrange()) {
- if(t.isSubrange()) {
- return t.getSubrangeBounds() <= getSubrangeBounds();
- } else {
- return t.getKind() == kind::TYPE_CONSTANT &&
- ( t.getConst<TypeConstant>() == INTEGER_TYPE ||
- t.getConst<TypeConstant>() == REAL_TYPE );
- }
- }
if(isTuple() && t.isTuple()) {
const Datatype& dt1 = getDatatype();
const Datatype& dt2 = t.getDatatype();
@@ -151,9 +142,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
}
return true;
}
- if(isPredicateSubtype()) {
- return getSubtypeParentType().isSubtypeOf(t);
- }
if(isSet() && t.isSet()) {
return getSetElementType().isSubtypeOf(t.getSetElementType());
}
@@ -205,28 +193,13 @@ bool TypeNode::isComparableTo(TypeNode t) const {
if(isArray() && t.isArray()) {
return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
}
- //if(isPredicateSubtype()) {
- // return t.isComparableTo(getSubtypeParentType());
- //}
return false;
}
-Node TypeNode::getSubtypePredicate() const {
- Assert(isPredicateSubtype());
- return Node::fromExpr(getConst<Predicate>().getExpression());
-}
-
-TypeNode TypeNode::getSubtypeParentType() const {
- Assert(isPredicateSubtype());
- return getSubtypePredicate().getType().getArgTypes()[0];
-}
-
TypeNode TypeNode::getBaseType() const {
TypeNode realt = NodeManager::currentNM()->realType();
if (isSubtypeOf(realt)) {
return realt;
- } else if (isPredicateSubtype()) {
- return getSubtypeParentType().getBaseType();
} else if (isParametricDatatype()) {
vector<Type> v;
for(size_t i = 1; i < getNumChildren(); ++i) {
@@ -264,14 +237,12 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
/** Is this a tuple type? */
bool TypeNode::isTuple() const {
- return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
+ return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() );
}
/** Is this a record type? */
bool TypeNode::isRecord() const {
- return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
+ return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() );
}
size_t TypeNode::getTupleLength() const {
@@ -375,11 +346,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
return TypeNode(); // null type
}
default:
- //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
- // return t0; // t0 is a constant type
- //} else {
- return TypeNode(); // null type
- //}
+ return TypeNode(); // null type
}
} else if(t1.getKind() == kind::TYPE_CONSTANT) {
return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
@@ -394,11 +361,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
case kind::CONSTRUCTOR_TYPE:
case kind::SELECTOR_TYPE:
case kind::TESTER_TYPE:
- //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
- // return t0;
- //} else {
- return TypeNode();
- //}
+ return TypeNode();
case kind::FUNCTION_TYPE:
return TypeNode(); // Not sure if this is right
case kind::SET_TYPE: {
@@ -423,47 +386,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
case kind::SEXPR_TYPE:
Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
return TypeNode();
- case kind::SUBTYPE_TYPE:
- //if(t1.isPredicateSubtype()){
- // // This is the case where both t0 and t1 are predicate subtypes.
- // return leastCommonPredicateSubtype(t0, t1);
- //}else{ // t0 is a predicate subtype and t1 is not
- // return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases
- //}
- return TypeNode();
- case kind::SUBRANGE_TYPE:
- /*
- if(t1.isSubrange()) {
- const SubrangeBounds& t0SR = t0.getSubrangeBounds();
- const SubrangeBounds& t1SR = t1.getSubrangeBounds();
- if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) {
- SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR);
- return NodeManager::currentNM()->mkSubrangeType(j);
- } else {
- return NodeManager::currentNM()->integerType();
- }
- } else if(t1.isPredicateSubtype()) {
- // t0 is a subrange
- // t1 is not a subrange
- // t1 is a predicate subtype
- if(t1.isInteger()) {
- return NodeManager::currentNM()->integerType();
- } else if(t1.isReal()) {
- return NodeManager::currentNM()->realType();
- } else {
- return TypeNode();
- }
- } else {
- // t0 is a subrange
- // t1 is not a subrange
- // t1 is not a type constant && is not a predicate subtype
- // t1 cannot be real subtype or integer.
- Assert(t1.isReal());
- Assert(t1.isInteger());
- return TypeNode();
- }
-*/
- return TypeNode();
case kind::DATATYPE_TYPE:
if( t0.isTuple() && t1.isTuple() ){
const Datatype& dt1 = t0.getDatatype();
@@ -490,9 +412,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
if(!t1.isParametricDatatype()) {
return TypeNode();
}
- while(t1.getKind() != kind::PARAMETRIC_DATATYPE) {
- t1 = t1.getSubtypeParentType();
- }
if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) {
return TypeNode();
}
@@ -508,38 +427,6 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
}
}
-TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){
- Assert(t0.isPredicateSubtype());
- Assert(t1.isPredicateSubtype());
-
- std::vector<TypeNode> t0stack;
- t0stack.push_back(t0);
- while(t0stack.back().isPredicateSubtype()){
- t0stack.push_back(t0stack.back().getSubtypeParentType());
- }
- std::vector<TypeNode> t1stack;
- t1stack.push_back(t1);
- while(t1stack.back().isPredicateSubtype()){
- t1stack.push_back(t1stack.back().getSubtypeParentType());
- }
-
- Assert(!t0stack.empty());
- Assert(!t1stack.empty());
-
- if(t0stack.back() == t1stack.back()){
- TypeNode mostGeneral = t1stack.back();
- t0stack.pop_back(); t1stack.pop_back();
- while(!t0stack.empty() && t1stack.empty() && t0stack.back() == t1stack.back()){
- mostGeneral = t0stack.back();
- t0stack.pop_back(); t1stack.pop_back();
- }
- return mostGeneral;
- }else{
- return leastCommonTypeNode(t0stack.back(), t1stack.back());
- }
-}
-
-
Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
TypeNode ntn = n.getType();
Assert( ntn.isComparableTo( tn ) );
@@ -581,8 +468,7 @@ Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
/** Is this a sort kind */
bool TypeNode::isSort() const {
- return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isSort() );
+ return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
}
/** Is this a sort constructor kind */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1a8bb14ed..8dd80bc37 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -620,27 +620,9 @@ public:
/** Is this a sort constructor kind */
bool isSortConstructor() const;
- /** Is this a subtype predicate */
- bool isPredicateSubtype() const;
-
- /** Get the predicate defining this subtype */
- Node getSubtypePredicate() const;
-
- /**
- * Get the parent type of this subtype; note that it could be
- * another subtype.
- */
- TypeNode getSubtypeParentType() const;
-
/** Get the most general base type of the type */
TypeNode getBaseType() const;
- /** Is this a subrange */
- bool isSubrange() const;
-
- /** Get the bounds defining this subrange */
- const SubrangeBounds& getSubrangeBounds() const;
-
/**
* Returns the leastUpperBound in the extended type lattice of the two types.
* If this is \top, i.e. there is no inhabited type that contains both,
@@ -657,13 +639,7 @@ public:
static Node getEnsureTypeCondition( Node n, TypeNode tn );
private:
static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
-
- /**
- * Returns the leastUpperBound in the extended type lattice of two
- * predicate subtypes.
- */
- static TypeNode leastCommonPredicateSubtype(TypeNode t0, TypeNode t1);
-
+
/**
* Indents the given stream a given amount of spaces.
*
@@ -852,22 +828,18 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
inline bool TypeNode::isBoolean() const {
return
- ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isBoolean() );
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE );
}
inline bool TypeNode::isInteger() const {
return
- ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
- isSubrange() ||
- ( isPredicateSubtype() && getSubtypeParentType().isInteger() );
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE );
}
inline bool TypeNode::isReal() const {
return
( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
- isInteger() ||
- ( isPredicateSubtype() && getSubtypeParentType().isReal() );
+ isInteger();
}
inline bool TypeNode::isString() const {
@@ -944,43 +916,27 @@ inline TypeNode TypeNode::getRangeType() const {
/** Is this a symbolic expression type? */
inline bool TypeNode::isSExpr() const {
- return getKind() == kind::SEXPR_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isSExpr() );
-}
-
-/** Is this a predicate subtype */
-inline bool TypeNode::isPredicateSubtype() const {
- return getKind() == kind::SUBTYPE_TYPE;
-}
-
-/** Is this a subrange type */
-inline bool TypeNode::isSubrange() const {
- return getKind() == kind::SUBRANGE_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isSubrange() );
+ return getKind() == kind::SEXPR_TYPE;
}
/** Is this a floating-point type */
inline bool TypeNode::isFloatingPoint() const {
- return getKind() == kind::FLOATINGPOINT_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() );
+ return getKind() == kind::FLOATINGPOINT_TYPE;
}
/** Is this a bit-vector type */
inline bool TypeNode::isBitVector() const {
- return getKind() == kind::BITVECTOR_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isBitVector() );
+ return getKind() == kind::BITVECTOR_TYPE;
}
/** Is this a datatype type */
inline bool TypeNode::isDatatype() const {
- return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
+ return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE;
}
/** Is this a parametric datatype type */
inline bool TypeNode::isParametricDatatype() const {
- return getKind() == kind::PARAMETRIC_DATATYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() );
+ return getKind() == kind::PARAMETRIC_DATATYPE;
}
/** Is this a codatatype type */
@@ -1013,15 +969,13 @@ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
return
( getKind() == kind::FLOATINGPOINT_TYPE &&
getConst<FloatingPointSize>().exponent() == exp &&
- getConst<FloatingPointSize>().significand() == sig ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) );
+ getConst<FloatingPointSize>().significand() == sig );
}
/** Is this a bit-vector type of size <code>size</code> */
inline bool TypeNode::isBitVector(unsigned size) const {
return
- ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) );
+ ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size );
}
/** Get the datatype specification from a datatype type */
@@ -1054,16 +1008,6 @@ inline unsigned TypeNode::getBitVectorSize() const {
return getConst<BitVectorSize>();
}
-inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
- Assert(isSubrange());
- if(getKind() == kind::SUBRANGE_TYPE){
- return getConst<SubrangeBounds>();
- }else{
- Assert(isPredicateSubtype());
- return getSubtypeParentType().getSubrangeBounds();
- }
-}
-
#ifdef CVC4_DEBUG
/**
* Pretty printer for use within gdb. This is not intended to be used
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback