Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
Type t = record.getType();
const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
- const CVC4::Record& rec = ((CVC4::DatatypeType)t).getRecord();
- unsigned index = rec.getIndex(field);
+ unsigned index = CVC4::Datatype::indexOf( dt[0].getSelector(field) );
return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record);
}
typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
+Datatype::~Datatype(){
+ delete d_record;
+}
+
const Datatype& Datatype::datatypeOf(Expr item) {
ExprManagerScope ems(item);
TypeNode t = Node::fromExpr(item).getType();
d_involvesUt = true;
}
}
+
+ if( d_isRecord ){
+ std::vector< std::pair<std::string, Type> > fields;
+ for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
+ fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
+ }
+ d_record = new Record(fields);
+ }
}
void Datatype::addConstructor(const DatatypeConstructor& c) {
}
void Datatype::setTuple() {
+ PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
d_isTuple = true;
}
void Datatype::setRecord() {
+ PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
d_isRecord = true;
}
return getSelector().getType();
}
+Type DatatypeConstructorArg::getRangeType() const {
+ return getType().getRangeType();
+}
+
bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
}
*/
SelectorType getType() const;
+ /**
+ * Get the range type of this argument.
+ */
+ Type getRangeType() const;
+
/**
* Get the name of the type of this constructor argument
* (Datatype field). Can be used for not-yet-resolved Datatypes
bool d_isCo;
bool d_isTuple;
bool d_isRecord;
+ Record * d_record;
std::vector<DatatypeConstructor> d_constructors;
bool d_resolved;
Type d_self;
*/
inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false);
+ ~Datatype();
+
/**
* Add a constructor to this Datatype. Constructor names need not
* be unique; they are for convenience and pretty-printing only.
/** is this a record datatype? */
inline bool isRecord() const;
+ /** get the record representation for this datatype */
+ inline Record * getRecord() const;
+
/**
* Return the cardinality of this datatype (the sum of the
* cardinalities of its constructors). The Datatype must be
d_isCo(isCo),
d_isTuple(false),
d_isRecord(false),
+ d_record(NULL),
d_constructors(),
d_resolved(false),
d_self(),
d_isCo(isCo),
d_isTuple(false),
d_isRecord(false),
+ d_record(NULL),
d_constructors(),
d_resolved(false),
d_self(),
return d_isRecord;
}
+inline Record * Datatype::getRecord() const {
+ return d_record;
+}
+
inline bool Datatype::operator!=(const Datatype& other) const throw() {
return !(*this == other);
}
j != j_end;
++j) {
const DatatypeConstructorArg& a = *j;
- Type selectorType = a.getSelector().getType();
+ Type selectorType = a.getType();
Assert(a.isResolved() &&
selectorType.isSelector() &&
SelectorType(selectorType).getDomain() == dtt,
d_operators[i] = Node::null();
}
- d_tupleAndRecordTypes.clear();
+ //d_tupleAndRecordTypes.clear();
+ d_tt_cache.d_children.clear();
+ d_rt_cache.d_children.clear();
Assert(!d_attrManager->inGarbageCollection() );
while(!d_zombies.empty()) {
return TypeNode(mkTypeConst(bounds));
}
+TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
+ if( index==types.size() ){
+ if( d_data.isNull() ){
+ Datatype dt("__cvc4_tuple");
+ dt.setTuple();
+ DatatypeConstructor c("__cvc4_tuple_ctor");
+ for (unsigned i = 0; i < types.size(); ++ i) {
+ std::stringstream ss;
+ ss << "__cvc4_tuple_stor_" << i;
+ c.addArg(ss.str().c_str(), types[i].toType());
+ }
+ dt.addConstructor(c);
+ d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+ Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
+ }
+ return d_data;
+ }else{
+ return d_children[types[index]].getTupleType( nm, types, index+1 );
+ }
+}
+
+TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) {
+ if( index==rec.getNumFields() ){
+ if( d_data.isNull() ){
+ 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);
+ }
+ dt.addConstructor(c);
+ d_data = TypeNode::fromType(nm->toExprManager()->mkDatatypeType(dt));
+ Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
+ }
+ return d_data;
+ }else{
+ return d_children[TypeNode::fromType( rec[index].second )][rec[index].first].getRecordType( nm, rec, index+1 );
+ }
+}
+
TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
std::vector< TypeNode > ts;
Debug("tuprec-debug") << "Make tuple type : ";
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;
+ return d_tt_cache.getTupleType( this, ts );
}
TypeNode NodeManager::mkRecordType(const Record& rec) {
- //index based on type constant
- TypeNode tindex = mkTypeConst(rec);
- TypeNode& dtt = d_tupleAndRecordTypes[tindex];
- if(dtt.isNull()) {
- 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);
- }
- 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;
+ return d_rt_cache.getRecordType( this, rec );
}
void NodeManager::reclaimAllZombies(){
/**
* A map of tuple and record types to their corresponding datatype.
*/
- std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
+ class TupleTypeCache {
+ public:
+ std::map< TypeNode, TupleTypeCache > d_children;
+ TypeNode d_data;
+ TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 );
+ };
+ class RecTypeCache {
+ public:
+ std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children;
+ TypeNode d_data;
+ TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 );
+ };
+ TupleTypeCache d_tt_cache;
+ RecTypeCache d_rt_cache;
/**
* Keep a count of all abstract values produced by this NodeManager.
struct VarNameTag { };
struct GlobalVarTag { };
struct SortArityTag { };
- struct DatatypeTupleTag { };
- struct DatatypeRecordTag { };
struct TypeTag { };
struct TypeCheckedTag { };
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
-/** Attribute true for datatype types that are replacements for tuple types */
-typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr;
-/** Attribute true for datatype types that are replacements for record types */
-typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr;
typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
t.getConst<TypeConstant>() == REAL_TYPE );
}
}
- if(isTuple() || isRecord()) {
- if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
+ if(isTuple() && t.isTuple()) {
+ const Datatype& dt1 = getDatatype();
+ const Datatype& dt2 = t.getDatatype();
+ if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
return false;
}
- if(isTuple()) {
- if(getNumChildren() != t.getNumChildren()) {
+ // r1's fields must be subtypes of r2's, in order
+ for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+ if( !dt1[0][i].getRangeType().isSubtypeOf( dt2[0][i].getRangeType() ) ){
return false;
}
- // children must be subtypes of t's, in order
- for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
- if(!(*i).isSubtypeOf(*j)) {
- return false;
- }
- }
- } else {
- const Record& r1 = getRecord();
- const Record& r2 = t.getRecord();
- if(r1.getNumFields() != r2.getNumFields()) {
- return false;
- }
- const Record::FieldVector& fields1 = r1.getFields();
- const Record::FieldVector& fields2 = r2.getFields();
- // r1's fields must be subtypes of r2's, in order
- // names must match also
- for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) {
- if((*i).first != (*j).first || !(*i).second.isSubtypeOf((*j).second)) {
- return false;
- }
- }
}
return true;
+ }else if( t.isRecord() && t.isRecord() ){
+ //TBD
}
if(isFunction()) {
// A function is a subtype of another if the args are the same type, and
if(isSubtypeOf(NodeManager::currentNM()->realType())) {
return t.isSubtypeOf(NodeManager::currentNM()->realType());
}
- if(isTuple() || isRecord()) {
- if(t.isTuple() || t.isRecord()) {
- if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
+ if(isTuple() && t.isTuple()) {
+ const Datatype& dt1 = getDatatype();
+ const Datatype& dt2 = t.getDatatype();
+ if( dt1[0].getNumArgs()!=dt2[0].getNumArgs() ){
+ return false;
+ }
+ // r1's fields must be subtypes of r2's, in order
+ for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+ if( !dt1[0][i].getRangeType().isComparableTo( dt2[0][i].getRangeType() ) ){
return false;
}
- if(isTuple()) {
- if(getNumChildren() != t.getNumChildren()) {
- return false;
- }
- // children must be comparable to t's, in order
- for(const_iterator i = begin(), j = t.begin(); i != end(); ++i, ++j) {
- if(!(*i).isComparableTo(*j)) {
- return false;
- }
- }
- } else {
- const Record& r1 = getRecord();
- const Record& r2 = t.getRecord();
- if(r1.getNumFields() != r2.getNumFields()) {
- return false;
- }
- // r1's fields must be comparable to r2's, in order
- // names must match also
- const Record::FieldVector& fields1 = r1.getFields();
- const Record::FieldVector& fields2 = r2.getFields();
- for(Record::FieldVector::const_iterator i = fields1.begin(), j = fields2.begin(); i != fields1.end(); ++i, ++j) {
- if((*i).first != (*j).first || !(*i).second.isComparableTo((*j).second)) {
- return false;
- }
- }
- }
- return true;
}
+ return true;
+ }else if( isRecord() && t.isRecord() ){
+ //TBD
} else if(isParametricDatatype() && t.isParametricDatatype()) {
Assert(getKind() == kind::PARAMETRIC_DATATYPE);
Assert(t.getKind() == kind::PARAMETRIC_DATATYPE);
/** Is this a tuple type? */
bool TypeNode::isTuple() const {
- return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeTupleAttr()) ) ||
+ return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) ||
( isPredicateSubtype() && getSubtypeParentType().isTuple() );
}
/** Is this a record type? */
bool TypeNode::isRecord() const {
- return ( getKind() == kind::DATATYPE_TYPE && hasAttribute(expr::DatatypeRecordAttr()) ) ||
+ return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) ||
( isPredicateSubtype() && getSubtypeParentType().isRecord() );
}
Assert(dt.getNumConstructors()==1);
vector<TypeNode> types;
for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
- types.push_back(TypeNode::fromType(((SelectorType)dt[0][i].getSelector().getType()).getRangeType()));
+ types.push_back(TypeNode::fromType(dt[0][i].getRangeType()));
}
return types;
}
const Record& TypeNode::getRecord() const {
Assert(isRecord());
- return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
+ const Datatype & dt = getDatatype();
+ return *(dt.getRecord());
+ //return getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
}
vector<TypeNode> TypeNode::getSExprTypes() const {
Assert(t1.isInteger());
return TypeNode();
}
-/*
- case kind::TUPLE_TYPE: {
- // if the other == this one, we returned already, above
- if(t0.getBaseType() == t1) {
- return t1;
- }
- if(!t1.isTuple() || t0.getNumChildren() != t1.getNumChildren()) {
- // no compatibility between t0, t1
- return TypeNode();
- }
- std::vector<TypeNode> types;
- // construct childwise leastCommonType, if one exists
- for(const_iterator i = t0.begin(), j = t1.begin(); i != t0.end(); ++i, ++j) {
- TypeNode kid = leastCommonTypeNode(*i, *j);
- if(kid.isNull()) {
- // no common supertype: types t0, t1 not compatible
- return TypeNode();
- }
- types.push_back(kid);
- }
- // if we make it here, we constructed the least common type
- return NodeManager::currentNM()->mkTupleType(types);
- }
- case kind::RECORD_TYPE: {
- // if the other == this one, we returned already, above
- if(t0.getBaseType() == t1) {
- return t1;
- }
- const Record& r0 = t0.getConst<Record>();
- if(!t1.isRecord() || r0.getNumFields() != t1.getConst<Record>().getNumFields()) {
- // no compatibility between t0, t1
- return TypeNode();
- }
- std::vector< std::pair<std::string, Type> > fields;
- const Record& r1 = t1.getConst<Record>();
- const Record::FieldVector& fields0 = r0.getFields();
- const Record::FieldVector& fields1 = r1.getFields();
- // construct childwise leastCommonType, if one exists
- for(Record::FieldVector::const_iterator i = fields0.begin(), j = fields1.begin(); i != fields0.end(); ++i, ++j) {
- TypeNode kid = leastCommonTypeNode(TypeNode::fromType((*i).second), TypeNode::fromType((*j).second));
- if((*i).first != (*j).first || kid.isNull()) {
- // if field names differ, or no common supertype, then
- // types t0, t1 not compatible
- return TypeNode();
- }
- fields.push_back(std::make_pair((*i).first, kid.toType()));
- }
- // 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) {
- return t0;
+ if( t0.isTuple() && t1.isTuple() ){
+ const Datatype& dt1 = t0.getDatatype();
+ const Datatype& dt2 = t1.getDatatype();
+ if( dt1[0].getNumArgs()==dt2[0].getNumArgs() ){
+ std::vector< TypeNode > lc_types;
+ for( unsigned i=0; i<dt1[0].getNumArgs(); i++ ){
+ TypeNode tc = leastCommonTypeNode( TypeNode::fromType( dt1[0][i].getRangeType() ), TypeNode::fromType( dt2[0][i].getRangeType() ) );
+ if( tc.isNull() ){
+ return tc;
+ }else{
+ lc_types.push_back( tc );
+ }
+ }
+ return NodeManager::currentNM()->mkTupleType( lc_types );
+ }
+ }else if( t0.isRecord() && t1.isRecord() ){
+ //TBD
}
// otherwise no common ancestor
return TypeNode();
TypeNode in_t = in.getType();
if( processing.find( in_t )==processing.end() ){
processing[in_t] = true;
- if(in.getType().isRecord()) {
- Assert(as.isRecord());
- const Record& inRec = in.getType().getRecord();
- const Record& asRec = as.getRecord();
- Assert(inRec.getNumFields() == asRec.getNumFields());
- const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
- NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
- nb << NodeManager::currentNM()->mkConst(asRec);
- for(size_t i = 0; i < asRec.getNumFields(); ++i) {
- Assert(inRec[i].first == asRec[i].first);
- Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
- if(inRec[i].second != asRec[i].second) {
- arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
- }
- nb << arg;
- }
- Node out = nb;
- processing.erase( in_t );
- return out;
- }
if(in.getType().isDatatype()) {
if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
processing.erase( in_t );
# constructor applications are constant if they are applied only to constants
construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
-## for co-datatypes
-operator MU 2 "a mu operator, first argument is a bound variable, second argument is body"
-typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-# mu applications are constant expressions
-construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-
constant TUPLE_UPDATE_OP \
::CVC4::TupleUpdate \
::CVC4::TupleUpdateHashFunction \
parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index"
typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
-constant RECORD_TYPE \
- ::CVC4::Record \
- ::CVC4::RecordHashFunction \
- "expr/record.h" \
- "record type"
-cardinality RECORD_TYPE \
- "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \
- "theory/datatypes/theory_datatypes_type_rules.h"
-well-founded RECORD_TYPE \
- "::CVC4::theory::datatypes::RecordProperties::isWellFounded(%TYPE%)" \
- "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \
- "theory/datatypes/theory_datatypes_type_rules.h"
-enumerator RECORD_TYPE \
- "::CVC4::theory::datatypes::RecordEnumerator" \
- "theory/datatypes/type_enumerator.h"
-
constant RECORD_UPDATE_OP \
::CVC4::RecordUpdate \
::CVC4::RecordUpdateHashFunction \
return n;
}
- if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
- Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
- Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl;
- if(t.isTuple()) {
- Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl;
- Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl;
- t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()));
- } else {
- Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl;
- Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl;
- t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()));
- }
- }
-
if( in.getKind()==EQUAL ){
Node nn;
std::vector< Node > rew;
}
};/* struct DatatypeAscriptionTypeRule */
-/* For co-datatypes */
-class DatatypeMuTypeRule {
-private:
- //a Mu-expression is constant iff its body is composed of constructors applied to constant expr and bound variables only
- inline static bool computeIsConstNode(TNode n, std::vector< TNode >& fv ){
- if( n.getKind()==kind::MU ){
- fv.push_back( n[0] );
- bool ret = computeIsConstNode( n[1], fv );
- fv.pop_back();
- return ret;
- }else if( n.isConst() || std::find( fv.begin(), fv.end(), n )!=fv.end() ){
- return true;
- }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !computeIsConstNode( n[i], fv ) ){
- return false;
- }
- }
- return true;
- }else{
- return false;
- }
- }
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- if( n[0].getKind()!=kind::BOUND_VARIABLE ) {
- std::stringstream ss;
- ss << "expected a bound var for MU expression, got `"
- << n[0] << "'";
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- return n[1].getType(check);
- }
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
- throw(AssertionException) {
- Assert(n.getKind() == kind::MU);
- NodeManagerScope nms(nodeManager);
- std::vector< TNode > fv;
- return computeIsConstNode( n, fv );
- }
-};
-
-
struct ConstructorProperties {
inline static Cardinality computeCardinality(TypeNode type) {
// Constructors aren't exactly functions, they're like
if(check) {
if(!tupleType.isTuple()) {
throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
- tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
}
if(tu.getIndex() >= tupleType.getTupleLength()) {
std::stringstream ss;
}
};/* struct RecordUpdateTypeRule */
-struct RecordProperties {
- inline static Node mkGroundTerm(TypeNode type) {
- Assert(type.getKind() == kind::RECORD_TYPE);
- return Node::null();
- }
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- return true;
- }
- inline static Cardinality computeCardinality(TypeNode type) {
- Cardinality card(1);
- return card;
- }
- inline static bool isWellFounded(TypeNode type) {
- return true;
- }
-};/* struct RecordProperties */
-
class DtSizeTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
};/* DatatypesEnumerator */
-
-class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
- TypeEnumeratorProperties * d_tep;
- TypeEnumerator** d_enumerators;
-
- /** Allocate and initialize the delegate enumerators */
- void newEnumerators() {
- const Record& rec = getType().getConst<Record>();
- d_enumerators = new TypeEnumerator*[rec.getNumFields()];
- for(size_t i = 0; i < rec.getNumFields(); ++i) {
- d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
- }
- }
-
- void deleteEnumerators() throw() {
- if(d_enumerators != NULL) {
- const Record& rec = getType().getConst<Record>();
- for(size_t i = 0; i < rec.getNumFields(); ++i) {
- delete d_enumerators[i];
- }
- delete [] d_enumerators;
- d_enumerators = NULL;
- }
- }
-
-public:
-
- RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
- TypeEnumeratorBase<RecordEnumerator>(type), d_tep(tep) {
- Assert(type.isRecord());
- newEnumerators();
- }
-
- RecordEnumerator(const RecordEnumerator& re) throw() :
- TypeEnumeratorBase<RecordEnumerator>(re.getType()),
- d_tep(re.d_tep),
- d_enumerators(NULL) {
-
- if(re.d_enumerators != NULL) {
- newEnumerators();
- for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]);
- }
- }
- }
-
- virtual ~RecordEnumerator() throw() {
- deleteEnumerators();
- }
-
- Node operator*() throw(NoMoreValuesException) {
- if(isFinished()) {
- throw NoMoreValuesException(getType());
- }
-
-
- return Node::null();
- }
-
- RecordEnumerator& operator++() throw() {
- if(isFinished()) {
- return *this;
- }
-
- size_t i;
- const Record& rec = getType().getConst<Record>();
- for(i = 0; i < rec.getNumFields(); ++i) {
- if(d_enumerators[i]->isFinished()) {
- *d_enumerators[i] = TypeEnumerator(TypeNode::fromType(rec[i].second));
- } else {
- ++*d_enumerators[i];
- return *this;
- }
- }
-
- deleteEnumerators();
-
- return *this;
- }
-
- bool isFinished() throw() {
- return d_enumerators == NULL;
- }
-
-};/* RecordEnumerator */
-
}/* CVC4::theory::datatypes namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
std::vector< Node > newVars;
for( unsigned j=0; j<c.getNumArgs(); j++ ){
- TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
- tn = tn[1];
+ TypeNode tn = TypeNode::fromType( c[j].getRangeType() );
Node v = NodeManager::currentNM()->mkBoundVar( tn );
newChildren.push_back( v );
newVars.push_back( v );
void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
for( unsigned j=0; j<dc.getNumArgs(); j++ ){
- TypeNode tn = TypeNode::fromType( ((SelectorType)dc[j].getSelector().getType()).getRangeType() );
+ TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
std::vector< Node > ssc;
if( tn==ntn ){
ssc.push_back( n );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode ctn = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() );
+ TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
ret = false;
break;
projects / cvc5.git / commitdiff