summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/datatype.cpp8
-rw-r--r--src/expr/datatype.h31
-rw-r--r--src/expr/expr_manager_template.cpp9
-rw-r--r--src/expr/expr_manager_template.h4
-rw-r--r--src/expr/node_manager.cpp123
-rw-r--r--src/expr/node_manager.h24
-rw-r--r--src/expr/type.cpp54
-rw-r--r--src/expr/type.h45
-rw-r--r--src/expr/type_node.cpp51
-rw-r--r--src/expr/type_node.h19
10 files changed, 161 insertions, 207 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index b9870afb4..32c0bb6dd 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -151,6 +151,13 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
d_sygus_allow_all = allow_all;
}
+void Datatype::setTuple() {
+ d_isTuple = true;
+}
+
+void Datatype::setRecord() {
+ d_isRecord = true;
+}
Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
@@ -663,7 +670,6 @@ void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >&
d_sygus_num_let_input_args = num_let_input_args;
}
-
void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 5f80c54f7..625fbb5d4 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -237,9 +237,6 @@ public:
*/
DatatypeConstructor(std::string name, std::string tester);
- /** set sygus */
- void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
-
/**
* Add an argument (i.e., a data field) of the given name and type
* to this Datatype constructor. Selector names need not be unique;
@@ -382,6 +379,8 @@ public:
bool involvesExternalType() const;
bool involvesUninterpretedType() const;
+ /** set sygus */
+ void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus );
};/* class DatatypeConstructor */
/**
@@ -473,6 +472,8 @@ private:
std::string d_name;
std::vector<Type> d_params;
bool d_isCo;
+ bool d_isTuple;
+ bool d_isRecord;
std::vector<DatatypeConstructor> d_constructors;
bool d_resolved;
Type d_self;
@@ -565,6 +566,12 @@ public:
*/
void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
+ /** set tuple */
+ void setTuple();
+
+ /** set tuple */
+ void setRecord();
+
/** Get the name of this Datatype. */
inline std::string getName() const throw();
@@ -589,6 +596,12 @@ public:
/** is this a sygus datatype? */
inline bool isSygus() const;
+ /** is this a tuple datatype? */
+ inline bool isTuple() const;
+
+ /** is this a record datatype? */
+ inline bool isRecord() const;
+
/**
* Return the cardinality of this datatype (the sum of the
* cardinalities of its constructors). The Datatype must be
@@ -757,6 +770,8 @@ inline Datatype::Datatype(std::string name, bool isCo) :
d_name(name),
d_params(),
d_isCo(isCo),
+ d_isTuple(false),
+ d_isRecord(false),
d_constructors(),
d_resolved(false),
d_self(),
@@ -771,6 +786,8 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params, boo
d_name(name),
d_params(params),
d_isCo(isCo),
+ d_isTuple(false),
+ d_isRecord(false),
d_constructors(),
d_resolved(false),
d_self(),
@@ -819,6 +836,14 @@ inline bool Datatype::isSygus() const {
return !d_sygus_type.isNull();
}
+inline bool Datatype::isTuple() const {
+ return d_isTuple;
+}
+
+inline bool Datatype::isRecord() const {
+ return d_isRecord;
+}
+
inline bool Datatype::operator!=(const Datatype& other) const throw() {
return !(*this == other);
}
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 0b9557cc8..ce7a92b48 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -20,6 +20,7 @@
#include "expr/node_manager.h"
#include "expr/variable_type_map.h"
+#include "expr/node_manager_attributes.h"
#include "options/options.h"
#include "util/statistics_registry.h"
@@ -596,18 +597,18 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
}
-TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
+DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) {
NodeManagerScope nms(d_nodeManager);
std::vector<TypeNode> typeNodes;
for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
typeNodes.push_back(*types[i].d_typeNode);
}
- return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
+ return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
}
-RecordType ExprManager::mkRecordType(const Record& rec) {
+DatatypeType ExprManager::mkRecordType(const Record& rec) {
NodeManagerScope nms(d_nodeManager);
- return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+ return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
}
SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index e65cfc358..37ef128f4 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -341,12 +341,12 @@ public:
* <code>types[0..types.size()-1]</code>. <code>types</code> must
* have at least one element.
*/
- TupleType mkTupleType(const std::vector<Type>& types);
+ DatatypeType mkTupleType(const std::vector<Type>& types);
/**
* Make a record type with types from the rec parameter.
*/
- RecordType mkRecordType(const Record& rec);
+ DatatypeType mkRecordType(const Record& rec);
/**
* Make a symbolic expressiontype with types from
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e52776fce..e6e44928d 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -461,79 +461,66 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
return TypeNode(mkTypeConst(bounds));
}
-TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
- Assert(t.isTuple() || t.isRecord());
-
- //AJR: not sure why .getBaseType() was used in two cases below,
- // disabling this, which is necessary to fix bug 605/667,
- // which involves records of INT which were mapped to records of REAL below.
- TypeNode tOrig = t;
- if(t.isTuple()) {
- vector<TypeNode> v;
- bool changed = false;
- for(size_t i = 0; i < t.getNumChildren(); ++i) {
- TypeNode tn = t[i];
- TypeNode base;
- if(tn.isTuple() || tn.isRecord()) {
- base = getDatatypeForTupleRecord(tn);
- } else {
- base = tn;//.getBaseType();
- }
- changed = changed || (tn != base);
- v.push_back(base);
- }
- if(changed) {
- t = mkTupleType(v);
- }
- } else {
- const Record& r = t.getRecord();
- std::vector< std::pair<std::string, Type> > v;
- bool changed = false;
- const Record::FieldVector& fields = r.getFields();
- for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
- Type tn = (*i).second;
- Type base;
- if(tn.isTuple() || tn.isRecord()) {
- base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType();
- } else {
- base = tn;//.getBaseType();
- }
- changed = changed || (tn != base);
- v.push_back(std::make_pair((*i).first, base));
- }
- if(changed) {
- t = mkRecordType(Record(v));
+TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
+ std::vector< TypeNode > ts;
+ Debug("tuprec-debug") << "Make tuple type : ";
+ for (unsigned i = 0; i < types.size(); ++ i) {
+ CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples");
+ ts.push_back( types[i] );
+ Debug("tuprec-debug") << types[i] << " ";
+ }
+ Debug("tuprec-debug") << std::endl;
+ //index based on function type
+ TypeNode tindex;
+ if( types.empty() ){
+ //do nothing (will index on null type)
+ }else if( types.size()==1 ){
+ tindex = types[0];
+ }else{
+ TypeNode tt = ts.back();
+ ts.pop_back();
+ tindex = mkFunctionType( ts, tt );
+ ts.push_back( tt );
+ }
+ TypeNode& dtt = d_tupleAndRecordTypes[tindex];
+ if(dtt.isNull()) {
+ Datatype dt("__cvc4_tuple");
+ dt.setTuple();
+ DatatypeConstructor c("__cvc4_tuple_ctor");
+ for (unsigned i = 0; i < ts.size(); ++ i) {
+ std::stringstream ss;
+ ss << "__cvc4_tuple_stor_" << i;
+ c.addArg(ss.str().c_str(), ts[i].toType());
}
+ dt.addConstructor(c);
+ dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
+ dtt.setAttribute(DatatypeTupleAttr(), tindex);
+ Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
+ }else{
+ Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
}
+ Assert(!dtt.isNull());
+ return dtt;
+}
- // if the type doesn't have an associated datatype, then make one for it
- TypeNode& dtt = d_tupleAndRecordTypes[t];
+TypeNode NodeManager::mkRecordType(const Record& rec) {
+ //index based on type constant
+ TypeNode tindex = mkTypeConst(rec);
+ TypeNode& dtt = d_tupleAndRecordTypes[tindex];
if(dtt.isNull()) {
- if(t.isTuple()) {
- Datatype dt("__cvc4_tuple");
- DatatypeConstructor c("__cvc4_tuple_ctor");
- for(TypeNode::const_iterator i = t.begin(); i != t.end(); ++i) {
- c.addArg("__cvc4_tuple_stor", (*i).toType());
- }
- dt.addConstructor(c);
- dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
- Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
- dtt.setAttribute(DatatypeTupleAttr(), tOrig);
- } else {
- const Record& rec = t.getRecord();
- const Record::FieldVector& fields = rec.getFields();
- Datatype dt("__cvc4_record");
- DatatypeConstructor c("__cvc4_record_ctor");
- for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
- c.addArg((*i).first, (*i).second);
- }
- dt.addConstructor(c);
- dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
- Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl;
- dtt.setAttribute(DatatypeRecordAttr(), tOrig);
+ const Record::FieldVector& fields = rec.getFields();
+ Datatype dt("__cvc4_record");
+ dt.setRecord();
+ DatatypeConstructor c("__cvc4_record_ctor");
+ for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
+ c.addArg((*i).first, (*i).second);
}
- } else {
- Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
+ dt.addConstructor(c);
+ dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt));
+ dtt.setAttribute(DatatypeRecordAttr(), tindex);
+ Debug("tuprec-debug") << "Return type : " << dtt << std::endl;
+ }else{
+ Debug("tuprec-debug") << "Return cached type : " << dtt << std::endl;
}
Assert(!dtt.isNull());
return dtt;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1ae9f1e8e..45c9afbde 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -756,7 +756,7 @@ public:
* @param types a vector of types
* @returns the tuple type (types[0], ..., types[n])
*/
- inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
+ TypeNode mkTupleType(const std::vector<TypeNode>& types);
/**
* Make a record type with the description from rec.
@@ -764,7 +764,7 @@ public:
* @param rec a description of the record
* @returns the record type
*/
- inline TypeNode mkRecordType(const Record& rec);
+ TypeNode mkRecordType(const Record& rec);
/**
* Make a symbolic expression type with types from
@@ -839,12 +839,6 @@ public:
throw(TypeCheckingExceptionPrivate);
/**
- * Given a tuple or record type, get the internal datatype used for
- * it. Makes the DatatypeType if necessary.
- */
- TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
-
- /**
* Get the type for the given node and optionally do type checking.
*
* Initial type computation will be near-constant time if
@@ -1063,20 +1057,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
}
-inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
- std::vector<TypeNode> typeNodes;
- for (unsigned i = 0; i < types.size(); ++ i) {
- CheckArgument(!types[i].isFunctionLike(), types,
- "cannot put function-like types in tuples");
- typeNodes.push_back(types[i]);
- }
- return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
-}
-
-inline TypeNode NodeManager::mkRecordType(const Record& rec) {
- return mkTypeConst(rec);
-}
-
inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
std::vector<TypeNode> typeNodes;
for (unsigned i = 0; i < types.size(); ++ i) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 99d04d658..6a8e6609c 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -292,6 +292,29 @@ bool Type::isRecord() const {
return d_typeNode->isRecord();
}
+/** Get the length of a tuple type */
+size_t Type::getTupleLength() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->getTupleLength();
+}
+
+/** Get the constituent types of a tuple type */
+std::vector<Type> Type::getTupleTypes() const {
+ NodeManagerScope nms(d_nodeManager);
+ std::vector< TypeNode > vec = d_typeNode->getTupleTypes();
+ std::vector< Type > vect;
+ for( unsigned i=0; i<vec.size(); i++ ){
+ vect.push_back( vec[i].toType() );
+ }
+ return vect;
+}
+
+/** Get the description of the record type */
+const Record& Type::getRecord() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->getRecord();
+}
+
/** Is this a symbolic expression type? */
bool Type::isSExpr() const {
NodeManagerScope nms(d_nodeManager);
@@ -358,27 +381,6 @@ Type FunctionType::getRangeType() const {
return makeType(d_typeNode->getRangeType());
}
-size_t TupleType::getLength() const {
- return d_typeNode->getTupleLength();
-}
-
-vector<Type> TupleType::getTypes() const {
- NodeManagerScope nms(d_nodeManager);
- vector<Type> types;
- vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
- vector<TypeNode>::iterator it = typeNodes.begin();
- vector<TypeNode>::iterator it_end = typeNodes.end();
- for(; it != it_end; ++ it) {
- types.push_back(makeType(*it));
- }
- return types;
-}
-
-const Record& RecordType::getRecord() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getRecord();
-}
-
vector<Type> SExprType::getTypes() const {
NodeManagerScope nms(d_nodeManager);
vector<Type> types;
@@ -488,16 +490,6 @@ FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException)
PrettyCheckArgument(isNull() || isFunction(), this);
}
-TupleType::TupleType(const Type& t) throw(IllegalArgumentException)
- : Type(t) {
- PrettyCheckArgument(isNull() || isTuple(), this);
-}
-
-RecordType::RecordType(const Type& t) throw(IllegalArgumentException)
- : Type(t) {
- PrettyCheckArgument(isNull() || isRecord(), this);
-}
-
SExprType::SExprType(const Type& t) throw(IllegalArgumentException)
: Type(t) {
PrettyCheckArgument(isNull() || isSExpr(), this);
diff --git a/src/expr/type.h b/src/expr/type.h
index 0f2118c44..b7ea14f78 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -56,8 +56,6 @@ class ConstructorType;
class SelectorType;
class TesterType;
class FunctionType;
-class TupleType;
-class RecordType;
class SExprType;
class SortType;
class SortConstructorType;
@@ -302,6 +300,15 @@ public:
*/
bool isRecord() const;
+ /** Get the length of a tuple type */
+ size_t getTupleLength() const;
+
+ /** Get the constituent types of a tuple type */
+ std::vector<Type> getTupleTypes() const;
+
+ /** Get the description of the record type */
+ const Record& getRecord() const;
+
/**
* Is this a symbolic expression type?
* @return true if the type is a symbolic expression type
@@ -459,39 +466,7 @@ public:
};/* class FunctionType */
/**
- * Class encapsulating a tuple type.
- */
-class CVC4_PUBLIC TupleType : public Type {
-
-public:
-
- /** Construct from the base type */
- TupleType(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the length of the tuple. The same as getTypes().size(). */
- size_t getLength() const;
-
- /** Get the constituent types */
- std::vector<Type> getTypes() const;
-
-};/* class TupleType */
-
-/**
- * Class encapsulating a record type.
- */
-class CVC4_PUBLIC RecordType : public Type {
-
-public:
-
- /** Construct from the base type */
- RecordType(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the constituent types */
- const Record& getRecord() const;
-};/* class RecordType */
-
-/**
- * Class encapsulating a tuple type.
+ * Class encapsulating a sexpr type.
*/
class CVC4_PUBLIC SExprType : public Type {
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index ea185f98b..755b16e46 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -94,9 +94,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
}
}
if(isTuple() || isRecord()) {
- if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
- return true;
- }
if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
return false;
}
@@ -111,8 +108,8 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
}
}
} else {
- const Record& r1 = getConst<Record>();
- const Record& r2 = t.getConst<Record>();
+ const Record& r1 = getRecord();
+ const Record& r2 = t.getRecord();
if(r1.getNumFields() != r2.getNumFields()) {
return false;
}
@@ -166,12 +163,8 @@ bool TypeNode::isComparableTo(TypeNode t) const {
if(isSubtypeOf(NodeManager::currentNM()->realType())) {
return t.isSubtypeOf(NodeManager::currentNM()->realType());
}
- if(t.isDatatype() && (isTuple() || isRecord())) {
+ if(isTuple() || isRecord()) {
if(t.isTuple() || t.isRecord()) {
- if(NodeManager::currentNM()->getDatatypeForTupleRecord(t) ==
- NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
- return true;
- }
if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
return false;
}
@@ -186,8 +179,8 @@ bool TypeNode::isComparableTo(TypeNode t) const {
}
}
} else {
- const Record& r1 = getConst<Record>();
- const Record& r2 = t.getConst<Record>();
+ const Record& r1 = getRecord();
+ const Record& r2 = t.getRecord();
if(r1.getNumFields() != r2.getNumFields()) {
return false;
}
@@ -202,12 +195,7 @@ bool TypeNode::isComparableTo(TypeNode t) const {
}
}
return true;
- } else {
- return t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this);
}
- } else if(isDatatype() && (t.isTuple() || t.isRecord())) {
- Assert(!isTuple() && !isRecord());// should have been handled above
- return *this == NodeManager::currentNM()->getDatatypeForTupleRecord(t);
} else if(isParametricDatatype() && t.isParametricDatatype()) {
Assert(getKind() == kind::PARAMETRIC_DATATYPE);
Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
@@ -244,8 +232,6 @@ TypeNode TypeNode::getBaseType() const {
TypeNode realt = NodeManager::currentNM()->realType();
if (isSubtypeOf(realt)) {
return realt;
- } else if (isTuple() || isRecord()) {
- return NodeManager::currentNM()->getDatatypeForTupleRecord(*this);
} else if (isPredicateSubtype()) {
return getSubtypeParentType().getBaseType();
} else if (isParametricDatatype()) {
@@ -282,23 +268,40 @@ std::vector<TypeNode> TypeNode::getParamTypes() const {
return params;
}
+
+/** Is this a tuple type? */
+bool TypeNode::isTuple() const {
+ return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) ||
+ ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
+}
+
+/** Is this a record type? */
+bool TypeNode::isRecord() const {
+ return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) ) ||
+ ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
+}
+
size_t TypeNode::getTupleLength() const {
Assert(isTuple());
- return getNumChildren();
+ const Datatype& dt = getConst<Datatype>();
+ Assert(dt.getNumConstructors()==1);
+ return dt[0].getNumArgs();
}
vector<TypeNode> TypeNode::getTupleTypes() const {
Assert(isTuple());
+ const Datatype& dt = getConst<Datatype>();
+ Assert(dt.getNumConstructors()==1);
vector<TypeNode> types;
- for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
- types.push_back((*this)[i]);
+ for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
+ types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType()));
}
return types;
}
const Record& TypeNode::getRecord() const {
Assert(isRecord());
- return getConst<Record>();
+ return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
}
vector<TypeNode> TypeNode::getSExprTypes() const {
@@ -446,6 +449,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
Assert(t1.isInteger());
return TypeNode();
}
+/*
case kind::TUPLE_TYPE: {
// if the other == this one, we returned already, above
if(t0.getBaseType() == t1) {
@@ -495,6 +499,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
// if we make it here, we constructed the least common type
return NodeManager::currentNM()->mkRecordType(Record(fields));
}
+*/
case kind::DATATYPE_TYPE:
// t1 might be a subtype tuple or record
if(t1.getBaseType() == t0) {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 59f602f09..4c48cc3ca 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -929,18 +929,6 @@ inline TypeNode TypeNode::getRangeType() const {
return (*this)[getNumChildren() - 1];
}
-/** Is this a tuple type? */
-inline bool TypeNode::isTuple() const {
- return getKind() == kind::TUPLE_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
-}
-
-/** Is this a record type? */
-inline bool TypeNode::isRecord() const {
- return getKind() == kind::RECORD_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
-}
-
/** Is this a symbolic expression type? */
inline bool TypeNode::isSExpr() const {
return getKind() == kind::SEXPR_TYPE ||
@@ -973,7 +961,6 @@ inline bool TypeNode::isBitVector() const {
/** Is this a datatype type */
inline bool TypeNode::isDatatype() const {
return getKind() == kind::DATATYPE_TYPE ||
- getKind() == kind::TUPLE_TYPE || getKind() == kind::RECORD_TYPE ||
( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
}
@@ -1027,11 +1014,7 @@ inline bool TypeNode::isBitVector(unsigned size) const {
/** Get the datatype specification from a datatype type */
inline const Datatype& TypeNode::getDatatype() const {
Assert(isDatatype());
- if(getKind() == kind::DATATYPE_TYPE) {
- return getConst<Datatype>();
- } else {
- return NodeManager::currentNM()->getDatatypeForTupleRecord(*this).getConst<Datatype>();
- }
+ return getConst<Datatype>();
}
/** Get the exponent size of this floating-point type */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback