Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) {
CVC4::Type t = recordType(field, expr.getType());
- return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr);
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+ return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr);
}
Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
const std::string& field1, const Expr& expr1) {
CVC4::Type t = recordType(field0, expr0.getType(),
field1, expr1.getType());
- return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1);
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+ return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr0, expr1);
}
Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0,
CVC4::Type t = recordType(field0, expr0.getType(),
field1, expr1.getType(),
field2, expr2.getType());
- return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1, expr2);
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+ return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), expr0, expr1, expr2);
}
Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
types.push_back(exprs[i].getType());
}
CVC4::Type t = recordType(fields, types);
- return d_em->mkExpr(d_em->mkConst(CVC4::RecordType(t).getRecord()), *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs));
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+ return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs));
}
Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
- return d_em->mkExpr(d_em->mkConst(CVC4::RecordSelect(field)), record);
+ Type t = record.getType();
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+ const CVC4::Record& rec = t.getRecord();
+ unsigned index = rec.getIndex(field);
+ return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record);
}
Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field,
}
Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) {
- const vector<CVC4::Expr>& v =
- *reinterpret_cast<const vector<CVC4::Expr>*>(&exprs);
- return d_em->mkExpr(CVC4::kind::TUPLE, v);
+ std::vector< Type > types;
+ std::vector<CVC4::Expr> v;
+ for( unsigned i=0; i<exprs.size(); i++ ){
+ types.push_back( exprs[i].getType() );
+ v.push_back( exprs[i] );
+ }
+ Type t = tupleType( types );
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
+ v.insert( v.begin(), dt[0].getConstructor() );
+ return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, v);
}
Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) {
- CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(),
+ CompatCheckArgument(index >= 0 && index < tuple.getType().getTupleLength(),
"invalid index in tuple select");
- return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple);
+ const CVC4::Datatype& dt = ((CVC4::DatatypeType)tuple.getType()).getDatatype();
+ return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), tuple);
}
Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
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");
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
*/
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;
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 */
/**
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;
*/
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();
/** 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
d_name(name),
d_params(),
d_isCo(isCo),
+ d_isTuple(false),
+ d_isRecord(false),
d_constructors(),
d_resolved(false),
d_self(),
d_name(name),
d_params(params),
d_isCo(isCo),
+ d_isTuple(false),
+ d_isRecord(false),
d_constructors(),
d_resolved(false),
d_self(),
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);
}
#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"
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) {
* <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
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;
* @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.
* @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
TypeNode mkSubrangeType(const SubrangeBounds& bounds)
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.
*
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) {
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);
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;
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);
class SelectorType;
class TesterType;
class FunctionType;
-class TupleType;
-class RecordType;
class SExprType;
class SortType;
class SortConstructorType;
*/
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
};/* 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 {
}
}
if(isTuple() || isRecord()) {
- if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
- return true;
- }
if(isTuple() != t.isTuple() || isRecord() != t.isRecord()) {
return false;
}
}
}
} 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;
}
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;
}
}
}
} 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;
}
}
}
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);
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()) {
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 {
Assert(t1.isInteger());
return TypeNode();
}
+/*
case kind::TUPLE_TYPE: {
// if the other == this one, we returned already, above
if(t0.getBaseType() == 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) {
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 ||
/** 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() );
}
/** 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 */
: restrictedTypePossiblyFunctionLHS[t,check,lhs]
{ if(lhs) {
assert(t.isTuple());
- args = TupleType(t).getTypes();
+ args = t.getTupleTypes();
} else {
args.push_back(t);
}
if(! t.isTuple()) {
PARSER_STATE->parseError("tuple-update applied to non-tuple");
}
- size_t length = TupleType(t).getLength();
+ size_t length = t.getTupleLength();
if(k >= length) {
std::stringstream ss;
ss << "tuple is of length " << length << "; cannot update index " << k;
PARSER_STATE->parseError(ss.str());
}
- f2 = MK_EXPR(MK_CONST(TupleSelect(k)), f);
+ std::vector<Expr> args;
+ const Datatype & dt = ((DatatypeType)t).getDatatype();
+ args.push_back( dt[0][k].getSelector() );
+ args.push_back( f );
+ f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
<< "its type: " << t;
PARSER_STATE->parseError(ss.str());
}
- const Record& rec = RecordType(t).getRecord();
+ const Record& rec = t.getRecord();
if(! rec.contains(id)) {
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
- f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f);
+ std::vector<Expr> args;
+ const Datatype & dt = ((DatatypeType)t).getDatatype();
+ args.push_back( dt[0][id].getSelector() );
+ args.push_back( f );
+ f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
if(! t.isRecord()) {
PARSER_STATE->parseError("record-select applied to non-record");
}
- const Record& rec = RecordType(t).getRecord();
+ const Record& rec = t.getRecord();
if(!rec.contains(id)){
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
- f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
+ const Datatype & dt = ((DatatypeType)t).getDatatype();
+ std::vector<Expr> sargs;
+ sargs.push_back( dt[0][id].getSelector() );
+ sargs.push_back( f );
+ f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs);
}
| k=numeral
{ Type t = f.getType();
if(! t.isTuple()) {
PARSER_STATE->parseError("tuple-select applied to non-tuple");
}
- size_t length = TupleType(t).getLength();
+ size_t length = t.getTupleLength();
if(k >= length) {
std::stringstream ss;
ss << "tuple is of length " << length << "; cannot access index " << k;
PARSER_STATE->parseError(ss.str());
}
- f = MK_EXPR(MK_CONST(TupleSelect(k)), f);
+ const Datatype & dt = ((DatatypeType)t).getDatatype();
+ std::vector<Expr> sargs;
+ sargs.push_back( dt[0][k].getSelector() );
+ sargs.push_back( f );
+ f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs);
}
)
)*
for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
types.push_back((*i).getType());
}
- TupleType t = EXPR_MANAGER->mkTupleType(types);
- f = MK_EXPR(kind::TUPLE, args);
+ DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+ const Datatype& dt = t.getDatatype();
+ args.insert( args.begin(), dt[0].getConstructor() );
+ f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
}
}
/* empty tuple literal */
| LPAREN RPAREN
- { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); }
+ { std::vector<Type> types;
+ DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+ const Datatype& dt = t.getDatatype();
+ f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); }
/* empty record literal */
| PARENHASH HASHPAREN
- { RecordType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >());
- f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>());
+ { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >());
+ const Datatype& dt = t.getDatatype();
+ f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor());
}
-
/* empty set literal */
| LBRACE RBRACE
{ f = MK_CONST(EmptySet(Type())); }
for(unsigned i = 0; i < names.size(); ++i) {
typeIds.push_back(std::make_pair(names[i], args[i].getType()));
}
- RecordType t = EXPR_MANAGER->mkRecordType(typeIds);
- f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args);
+ DatatypeType t = EXPR_MANAGER->mkRecordType(typeIds);
+ const Datatype& dt = t.getDatatype();
+ args.insert( args.begin(), dt[0].getConstructor() );
+ f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
}
/* variable / zero-ary constructor application */
}
break;
- case kind::DATATYPE_TYPE:
- out << n.getConst<Datatype>().getName();
+ case kind::DATATYPE_TYPE: {
+ const Datatype& dt = n.getConst<Datatype>();
+ if( dt.isTuple() ){
+ out << '[';
+ for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
+ if (i > 0) {
+ out << ", ";
+ }
+ Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
+ out << t;
+ }
+ out << ']';
+ }else if( dt.isRecord() ){
+ out << "[# ";
+ for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
+ if (i > 0) {
+ out << ", ";
+ }
+ Type t = ((SelectorType)dt[0][i].getSelector().getType()).getRangeType();
+ out << dt[0][i].getSelector() << ":" << t;
+ }
+ out << " #]";
+ }else{
+ out << dt.getName();
+ }
+ }
break;
case kind::EMPTYSET:
out << " ENDIF";
return;
break;
- case kind::TUPLE_TYPE:
case kind::SEXPR_TYPE:
out << '[';
for (unsigned i = 0; i < n.getNumChildren(); ++ i) {
}
return;
break;
- case kind::APPLY_CONSTRUCTOR:
+ case kind::APPLY_CONSTRUCTOR: {
+ TypeNode t = n.getType();
+ if( t.isTuple() ){
+ //no-op
+ }else if( t.isRecord() ){
+ const Record& rec = t.getRecord();
+ out << "(# ";
+ TNode::iterator i = n.begin();
+ bool first = true;
+ const Record::FieldVector& fields = rec.getFields();
+ for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
+ if(!first) {
+ out << ", ";
+ }
+ out << (*j).first << " := ";
+ toStream(out, *i, depth, types, false);
+ first = false;
+ }
+ out << " #)";
+ return;
+ }else{
+ toStream(op, n.getOperator(), depth, types, false);
+ }
+ }
+ break;
case kind::APPLY_SELECTOR:
- case kind::APPLY_SELECTOR_TOTAL:
+ case kind::APPLY_SELECTOR_TOTAL: {
+ TypeNode t = n.getType();
+ if( t.isTuple() ){
+ toStream(out, n[0], depth, types, true);
+ out << '.' << Datatype::indexOf( n.getOperator().toExpr() );
+ }else if( t.isRecord() ){
+ toStream(out, n[0], depth, types, true);
+ const Record& rec = t.getRecord();
+ unsigned index = Datatype::indexOf( n.getOperator().toExpr() );
+ std::pair<std::string, Type> fld = rec[index];
+ out << '.' << fld.first;
+ }else{
+ toStream(op, n.getOperator(), depth, types, false);
+ }
+ }
+ break;
case kind::APPLY_TESTER:
toStream(op, n.getOperator(), depth, types, false);
break;
out << " -> BOOLEAN";
return;
break;
- case kind::TUPLE_SELECT:
- toStream(out, n[0], depth, types, true);
- out << '.' << n.getOperator().getConst<TupleSelect>().getIndex();
- return;
- break;
- case kind::RECORD_SELECT:
- toStream(out, n[0], depth, types, true);
- out << '.' << n.getOperator().getConst<RecordSelect>().getField();
- return;
- break;
case kind::TUPLE_UPDATE:
toStream(out, n[0], depth, types, true);
out << " WITH ." << n.getOperator().getConst<TupleUpdate>().getIndex() << " := ";
toStream(out, n[1], depth, types, true);
return;
break;
- case kind::TUPLE:
- // no-op
- break;
- case kind::RECORD: {
- // (# _a := 2, _b := 2 #)
- const Record& rec = n.getOperator().getConst<Record>();
- out << "(# ";
- TNode::iterator i = n.begin();
- bool first = true;
- const Record::FieldVector& fields = rec.getFields();
- for(Record::FieldVector::const_iterator j = fields.begin(); j != fields.end(); ++i, ++j) {
- if(!first) {
- out << ", ";
- }
- out << (*j).first << " := ";
- toStream(out, *i, depth, types, false);
- first = false;
- }
- out << " #)";
- return;
- break;
- }
// ARRAYS
case kind::ARRAY_TYPE:
static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() {
if(c->getArity() > 0) {
+ //TODO?
out << "ERROR: Don't know how to print parameterized type declaration "
- "in CVC language:" << endl << c->toString() << endl;
+ "in CVC language." << endl;
} else {
out << c->getSymbol() << " : TYPE;";
}
}
firstSelector = false;
const DatatypeConstructorArg& selector = *k;
- out << selector.getName() << ": " << SelectorType(selector.getType()).getRangeType();
+ Type t = SelectorType(selector.getType()).getRangeType();
+ if( t.isDatatype() ){
+ const Datatype & sdt = ((DatatypeType)t).getDatatype();
+ out << selector.getName() << ": " << sdt.getName();
+ }else{
+ out << selector.getName() << ": " << t;
+ }
}
out << ')';
}
case kind::EQUAL:
case kind::DISTINCT: out << smtKindString(k) << " "; break;
case kind::CHAIN: break;
- case kind::TUPLE: break;
case kind::FUNCTION_TYPE:
for(size_t i = 0; i < n.getNumChildren() - 1; ++i) {
if(i > 0) {
case kind::EQUAL: return "=";
case kind::DISTINCT: return "distinct";
case kind::CHAIN: break;
- case kind::TUPLE: break;
case kind::SEXPR: break;
// bool theory
processing[in_t] = true;
if(in.getType().isRecord()) {
Assert(as.isRecord());
- const Record& inRec = in.getType().getConst<Record>();
- const Record& asRec = as.getConst<Record>();
+ const Record& inRec = in.getType().getRecord();
+ const Record& asRec = as.getRecord();
Assert(inRec.getNumFields() == asRec.getNumFields());
- NodeBuilder<> nb(kind::RECORD);
+ 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(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in);
+ 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);
}
processing.erase( in_t );
return out;
}
- if(in.getType().isTuple()) {
- Assert(as.isTuple());
- Assert(in.getType().getNumChildren() == as.getNumChildren());
- NodeBuilder<> nb(kind::TUPLE);
- for(size_t i = 0; i < as.getNumChildren(); ++i) {
- Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in);
- if(in.getType()[i] != as[i]) {
- arg = rewriteAs(arg, as[i], 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 );
} else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
return out;
}
- if(type.isRecord()) {
- const Record& rec = type.getConst<Record>();
- const Record::FieldVector& fields = rec.getFields();
- vector< pair<string, Type> > flds;
- for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
- TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
- if(TypeNode::fromType((*i).second) != converted) {
- flds.push_back(make_pair((*i).first, converted.toType()));
- } else {
- flds.push_back(*i);
- }
- }
- TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
- Debug("tuprec") << "converted " << type << " to " << newRec << endl;
- if(newRec != type) {
- outNode = newRec;// cache it
- }
- return newRec;
- }
if(!type.isSort() && type.getNumChildren() > 0) {
Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
// This should handle tuples and arrays ok.
stack< triple<TNode, theory::TheoryId, bool> > worklist;
worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
stack< NodeBuilder<> > result;
- result.push(NodeBuilder<>(kind::TUPLE));
+ //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder. Since TUPLE is no longer a kind, replacing this with "AND".
+ //result.push(NodeBuilder<>(kind::TUPLE));
+ result.push(NodeBuilder<>(kind::AND));
NodeManager* nm = NodeManager::currentNM();
result.top() << top;
worklist.pop();
goto next_worklist;
- } else if(t.isTuple() || t.isRecord()) {
- TypeNode newType = convertType(t, true);
- if(t != newType) {
- Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
- newType, "a tuple/record variable introduced by Boolean-term conversion",
- NodeManager::SKOLEM_EXACT_NAME);
- top.setAttribute(BooleanTermAttr(), n);
- n.setAttribute(BooleanTermAttr(), top);
- Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
- d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
- Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
- d_varCache[top] = n;
- result.top() << n;
- worklist.pop();
- goto next_worklist;
- }
- d_varCache[top] = Node::null();
- result.top() << top;
- worklist.pop();
- goto next_worklist;
} else if(t.isDatatype() || t.isParametricDatatype()) {
Debug("boolean-terms") << "found a var of datatype type" << endl;
TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
Debug("bt") << "looking at: " << top << endl;
// rewrite the operator, as necessary
if(mk == kind::metakind::PARAMETERIZED) {
- if(k == kind::RECORD) {
- result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
- } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+ if(k == kind::APPLY_TYPE_ASCRIPTION) {
Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
result.top() << asc;
Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
asc.setAttribute(BooleanTermAttr(), top.getOperator());
} else if(kindToTheoryId(k) != THEORY_BV &&
- k != kind::TUPLE_SELECT &&
k != kind::TUPLE_UPDATE &&
- k != kind::RECORD_SELECT &&
k != kind::RECORD_UPDATE &&
k != kind::DIVISIBLE &&
// Theory parametric functions go here
} else {
Node n = result.top();
result.pop();
- Debug("boolean-terms") << "constructed: " << n << endl;
+ Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl;
if(parentTheory == theory::THEORY_BOOL) {
if(n.getType().isBitVector() &&
n.getType().getBitVectorSize() == 1) {
return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
}
}
- if(n.getType().isRecord() && asType.isRecord()) {
- Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
- const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
- const Record& asRec = asType.getConst<Record>();
- Assert(rec.getNumFields() == asRec.getNumFields());
- Assert(n.getNumChildren() == asRec.getNumFields());
- NodeBuilder<> b(n.getKind());
- b << asType;
- for(size_t i = 0; i < n.getNumChildren(); ++i) {
- b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second));
- }
- Node out = b;
- Debug("boolean-terms") << "+++ returning record " << out << endl;
- return out;
- }
Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
if(n.getType().isArray()) {
Assert(asType.isArray());
Debug("tuprec") << "visiting " << current << endl;
Assert(!alreadyVisited(current, TNode::null()));
bool rewriteChildren = false;
- if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
- if(current.getKind() == kind::APPLY_CONSTRUCTOR){
- TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
- NodeBuilder<> b(kind::TUPLE);
- TypeNode::iterator t = expectType.begin();
- for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
- Assert(alreadyVisited(*i, TNode::null()));
- Assert(t != expectType.end());
- TNode n = d_nodes[*i];
- n = n.isNull() ? *i : n;
- if(!n.getType().isSubtypeOf(*t)) {
- Assert(n.getType().isBitVector(1u) ||
- (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
- Assert(n.isConst());
- Assert((*t).isBoolean());
- if(n.getType().isBitVector(1u)) {
- b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
- } else {
- // we assume (by construction) false is first; see boolean_terms.cpp
- b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
- }
- } else {
- b << n;
- }
- }
- Assert(t == expectType.end());
- d_nodes[current] = b;
- Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
- // The assert below is too strong---we might be returning a model value but
- // expect a type that still uses datatypes for tuples/records. If it's
- // really not the right type we should catch it in SmtEngine anyway.
- // Assert(d_nodes[current].getType() == expectType);
- return;
- }else{
- rewriteChildren = true;
- }
- } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
- if(current.getKind() == kind::APPLY_CONSTRUCTOR){
- //Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
- TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
- const Record& expectRec = expectType.getConst<Record>();
- NodeBuilder<> b(kind::RECORD);
- b << current.getType().getAttribute(expr::DatatypeRecordAttr());
- const Record::FieldVector& fields = expectRec.getFields();
- Record::FieldVector::const_iterator t = fields.begin();
- for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
- Assert(alreadyVisited(*i, TNode::null()));
- Assert(t != fields.end());
- TNode n = d_nodes[*i];
- n = n.isNull() ? *i : n;
- if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
- Assert(n.getType().isBitVector(1u) ||
- (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
- Assert(n.isConst());
- Assert((*t).second.isBoolean());
- if(n.getType().isBitVector(1u)) {
- b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
- } else {
- // we assume (by construction) false is first; see boolean_terms.cpp
- b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
- }
- } else {
- b << n;
- }
- }
- Assert(t == fields.end());
- d_nodes[current] = b;
- Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
- Assert(d_nodes[current].getType() == expectType);
- return;
- }else{
- rewriteChildren = true;
- }
- } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
+ if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
( current.getOperator().hasAttribute(BooleanTermAttr()) ||
( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
+ for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+ Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
+ }
if(d_propagatorNeedsFinish) {
d_propagator.finish();
return false;
}
+
+ Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl;
// No conflict, go through the literals and solve them
SubstitutionMap constantPropagations(d_smt.d_context);
SubstitutionMap newSubstitutions(d_smt.d_context);
Node learnedLiteral = d_nonClausalLearnedLiterals[i];
Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
+ Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
if (learnedLiteral != learnedLiteralNew) {
learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
}
+ Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl;
for (;;) {
learnedLiteralNew = constantPropagations.apply(learnedLiteral);
if (learnedLiteralNew == learnedLiteral) {
++d_smt.d_stats->d_numConstantProps;
learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
}
+ Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl;
// It might just simplify to a constant
if (learnedLiteral.isConst()) {
if (learnedLiteral.getConst<bool>()) {
#endif /* CVC4_ASSERTIONS */
}
// Resize the learnt
+ Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
d_nonClausalLearnedLiterals.resize(j);
hash_set<TNode, TNodeHashFunction> s;
}
}
}
- if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
- return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
- }
- if(in.getKind() == kind::RECORD_SELECT && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
- const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
- return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
- }
- if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
- (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) {
- // These strange (half-tuple-converted) terms can be created by
- // the system if you have something like "foo.1" for a tuple
- // term foo. The select is rewritten to "select_1(foo)". If
- // foo gets a value in the model from the TypeEnumerator, you
- // then have a select of a tuple, and we should flatten that
- // here. Ditto for records, below.
- Expr selectorExpr = in.getOperator().toExpr();
- const Datatype& dt CVC4_UNUSED = Datatype::datatypeOf(selectorExpr);
- TypeNode dtt CVC4_UNUSED = TypeNode::fromType(dt.getDatatypeType());
- size_t selectorIndex = Datatype::indexOf(selectorExpr);
- Debug("tuprec") << "looking at " << in << ", got selector index " << selectorIndex << std::endl;
-#ifdef CVC4_ASSERTIONS
- // sanity checks: tuple- and record-converted datatypes should have one constructor
- Assert(NodeManager::currentNM()->getDatatypeForTupleRecord(in[0].getType()) == dtt);
- if(in[0].getKind() == kind::TUPLE) {
- Assert(dtt.hasAttribute(expr::DatatypeTupleAttr()));
- Assert(dtt.getAttribute(expr::DatatypeTupleAttr()) == in[0].getType());
- } else {
- Assert(dtt.hasAttribute(expr::DatatypeRecordAttr()));
- Assert(dtt.getAttribute(expr::DatatypeRecordAttr()) == in[0].getType());
- }
- Assert(dt.getNumConstructors() == 1);
- Assert(dt[0].getNumArgs() > selectorIndex);
- Assert(dt[0][selectorIndex].getSelector() == selectorExpr);
-#endif /* CVC4_ASSERTIONS */
- Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl;
- return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
- }
if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
// Have to be careful not to rewrite well-typed expressions
// where the selector doesn't match the constructor,
return RewriteResponse(REWRITE_AGAIN_FULL, res );
}
}
- if(in.getKind() == kind::TUPLE_SELECT &&
- in[0].getKind() == kind::TUPLE) {
- return RewriteResponse(REWRITE_DONE, in[0][in.getOperator().getConst<TupleSelect>().getIndex()]);
- }
- if(in.getKind() == kind::TUPLE_UPDATE &&
- in[0].getKind() == kind::TUPLE) {
- size_t ix = in.getOperator().getConst<TupleUpdate>().getIndex();
- NodeBuilder<> b(kind::TUPLE);
- for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) {
- if(ix == 0) {
- b << in[1];
- } else {
- b << *i;
- }
- }
- Node n = b;
- Assert(n.getType().isSubtypeOf(in.getType()));
- return RewriteResponse(REWRITE_DONE, n);
- }
- if(in.getKind() == kind::RECORD_SELECT &&
- in[0].getKind() == kind::RECORD) {
- return RewriteResponse(REWRITE_DONE, in[0][in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
- }
- if(in.getKind() == kind::RECORD_UPDATE &&
- in[0].getKind() == kind::RECORD) {
- size_t ix = in[0].getOperator().getConst<Record>().getIndex(in.getOperator().getConst<RecordUpdate>().getField());
- NodeBuilder<> b(kind::RECORD);
- b << in[0].getOperator();
- for(TNode::const_iterator i = in[0].begin(); i != in[0].end(); ++i, --ix) {
- if(ix == 0) {
- b << in[1];
- } else {
- b << *i;
- }
- }
- Node n = b;
- Assert(n.getType().isSubtypeOf(in.getType()));
- return RewriteResponse(REWRITE_DONE, n);
- }
if(in.getKind() == kind::EQUAL && in[0] == in[1]) {
return RewriteResponse(REWRITE_DONE,
static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) {
Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl;
- if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
- (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
- (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
- //n1.getKind()==kind::APPLY_CONSTRUCTOR
+ if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
if( n1.getOperator() != n2.getOperator() ) {
Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl;
return true;
/** is this term a datatype */
static bool isTermDatatype( TNode n ){
TypeNode tn = n.getType();
- return tn.isDatatype() || tn.isParametricDatatype() ||
- tn.isTuple() || tn.isRecord();
+ return tn.isDatatype() || tn.isParametricDatatype();
}
static bool isTypeDatatype( TypeNode tn ){
- return tn.isDatatype() || tn.isParametricDatatype() ||
- tn.isTuple() || tn.isRecord();
+ return tn.isDatatype() || tn.isParametricDatatype();
}
private:
static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending,
# mu applications are constant expressions
construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-operator TUPLE_TYPE 0: "tuple type"
-cardinality TUPLE_TYPE \
- "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
- "theory/datatypes/theory_datatypes_type_rules.h"
-well-founded TUPLE_TYPE \
- "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%TYPE%)" \
- "::CVC4::theory::datatypes::TupleProperties::mkGroundTerm(%TYPE%)" \
- "theory/datatypes/theory_datatypes_type_rules.h"
-enumerator TUPLE_TYPE \
- "::CVC4::theory::datatypes::TupleEnumerator" \
- "theory/datatypes/type_enumerator.h"
-
-operator TUPLE 0: "a tuple (N-ary)"
-typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
-construle TUPLE ::CVC4::theory::datatypes::TupleProperties
-
-constant TUPLE_SELECT_OP \
- ::CVC4::TupleSelect \
- ::CVC4::TupleSelectHashFunction \
- "util/tuple.h" \
- "operator for a tuple select; payload is an instance of the CVC4::TupleSelect class"
-parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple"
-typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule
-
constant TUPLE_UPDATE_OP \
::CVC4::TupleUpdate \
::CVC4::TupleUpdateHashFunction \
"expr/record.h" \
"record type"
cardinality RECORD_TYPE \
- "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
+ "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \
"theory/datatypes/theory_datatypes_type_rules.h"
well-founded RECORD_TYPE \
- "::CVC4::theory::datatypes::TupleProperties::isWellFounded(%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"
-parameterized RECORD RECORD_TYPE 0: "a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order"
-typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
-construle RECORD ::CVC4::theory::datatypes::RecordProperties
-
-constant RECORD_SELECT_OP \
- ::CVC4::RecordSelect \
- ::CVC4::RecordSelectHashFunction \
- "expr/record.h" \
- "operator for a record select; payload is an instance CVC4::RecordSelect class"
-parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from"
-typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule
-
constant RECORD_UPDATE_OP \
::CVC4::RecordUpdate \
::CVC4::RecordUpdateHashFunction \
"expr/record.h" \
- "operator for a record update; payload is an instance CVC4::RecordSelect class"
+ "operator for a record update; payload is an instance CVC4::RecordUpdate class"
parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field"
typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
// extra debug check to make sure that the rewriter did its job correctly
Assert( atom.getKind() != kind::EQUAL ||
- ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE &&
- atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD &&
- atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
- atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE &&
- atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT &&
- atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ),
+ ( atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
+ atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE),
"tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
//assert the fact
Node TheoryDatatypes::ppRewrite(TNode in) {
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
- if(in.getKind() == kind::TUPLE_SELECT) {
- TypeNode t = in[0].getType();
- if(t.hasAttribute(expr::DatatypeTupleAttr())) {
- t = t.getAttribute(expr::DatatypeTupleAttr());
- }
- TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
- const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
- return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
- } else if(in.getKind() == kind::RECORD_SELECT) {
- TypeNode t = in[0].getType();
- if(t.hasAttribute(expr::DatatypeRecordAttr())) {
- t = t.getAttribute(expr::DatatypeRecordAttr());
- }
- TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
- const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
- return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
- }
-
TypeNode t = in.getType();
- // we only care about tuples and records here
- if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
- in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
- 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 " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
- if(t.isTuple()) {
- Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
- Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
- NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
- } else {
- Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
- Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
- NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
- }
- }
-
- if( in.getKind()==EQUAL ){
- Node nn;
- std::vector< Node > rew;
- if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
- nn = NodeManager::currentNM()->mkConst(false);
- }else{
- nn = rew.size()==0 ? d_true :
- ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
- }
- return nn;
- }
-
- // nothing to do
- return in;
- }
-
- if(t.hasAttribute(expr::DatatypeTupleAttr())) {
- t = t.getAttribute(expr::DatatypeTupleAttr());
- } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
- t = t.getAttribute(expr::DatatypeRecordAttr());
- }
-
- // if the type doesn't have an associated datatype, then make one for it
- TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t;
-
- const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-
- // now rewrite the expression
- Node n;
- if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) {
- NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
- b << Node::fromExpr(dt[0].getConstructor());
- b.append(in.begin(), in.end());
- n = b;
- } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
+ if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
+ Assert( t.isDatatype() );
+ const Datatype& dt = DatatypeType(t.toType()).getDatatype();
NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
b << Node::fromExpr(dt[0].getConstructor());
size_t size, updateIndex;
if(in.getKind() == kind::TUPLE_UPDATE) {
- size = t.getNumChildren();
+ Assert( t.isTuple() );
+ size = t.getTupleLength();
updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
} else { // kind::RECORD_UPDATE
- const Record& record = t.getConst<Record>();
+ Assert( t.isRecord() );
+ const Record& record = t.getRecord();
size = record.getNumFields();
updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
}
}
}
Debug("tuprec") << "builder says " << b << std::endl;
- n = b;
+ Node n = b;
+ return n;
}
- Assert(!n.isNull());
+ 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;
+ if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
+ nn = NodeManager::currentNM()->mkConst(false);
+ }else{
+ nn = rew.size()==0 ? d_true :
+ ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+ }
+ return nn;
+ }
- Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
+ // nothing to do
+ return in;
- return n;
}
void TheoryDatatypes::addSharedTerm(TNode t) {
}
bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
- if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
- (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
- (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
+ if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
if( n1.getOperator() != n2.getOperator() ) {
return true;
} else {
}
};/* struct ConstructorProperties */
-struct TupleTypeRule {
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- Assert(n.getKind() == kind::TUPLE);
- std::vector<TypeNode> types;
- for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
- child_it != child_it_end;
- ++child_it) {
- types.push_back((*child_it).getType(check));
- }
- return nodeManager->mkTupleType(types);
- }
-};/* struct TupleTypeRule */
-
-struct TupleSelectTypeRule {
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- Assert(n.getKind() == kind::TUPLE_SELECT);
- if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) {
- throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator");
- }
- const TupleSelect& ts = n.getOperator().getConst<TupleSelect>();
- TypeNode tupleType = n[0].getType(check);
- if(!tupleType.isTuple()) {
- if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
- throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple");
- }
- tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
- }
- if(ts.getIndex() >= tupleType.getNumChildren()) {
- std::stringstream ss;
- ss << "Tuple-select expression index `" << ts.getIndex()
- << "' is not a valid index; tuple type only has "
- << tupleType.getNumChildren() << " fields";
- throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
- }
- return tupleType[ts.getIndex()];
- }
-};/* struct TupleSelectTypeRule */
-
struct TupleUpdateTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
Assert(n.getKind() == kind::TUPLE_UPDATE);
TypeNode newValue = n[1].getType(check);
if(check) {
if(!tupleType.isTuple()) {
- if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
- throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
- }
+ throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
}
- if(tu.getIndex() >= tupleType.getNumChildren()) {
+ if(tu.getIndex() >= tupleType.getTupleLength()) {
std::stringstream ss;
ss << "Tuple-update expression index `" << tu.getIndex()
<< "' is not a valid index; tuple type only has "
- << tupleType.getNumChildren() << " fields";
+ << tupleType.getTupleLength() << " fields";
throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
}
}
}
};/* struct TupleUpdateTypeRule */
-struct TupleProperties {
- inline static Cardinality computeCardinality(TypeNode type) {
- // Don't assert this; allow other theories to use this cardinality
- // computation.
- //
- // Assert(type.getKind() == kind::TUPLE_TYPE);
-
- Cardinality card(1);
- for(TypeNode::iterator i = type.begin(),
- i_end = type.end();
- i != i_end;
- ++i) {
- card *= (*i).getCardinality();
- }
-
- return card;
- }
-
- inline static bool isWellFounded(TypeNode type) {
- // Don't assert this; allow other theories to use this
- // wellfoundedness computation.
- //
- // Assert(type.getKind() == kind::TUPLE_TYPE);
-
- for(TypeNode::iterator i = type.begin(),
- i_end = type.end();
- i != i_end;
- ++i) {
- if(! (*i).isWellFounded()) {
- return false;
- }
- }
-
- return true;
- }
-
- inline static Node mkGroundTerm(TypeNode type) {
- Assert(type.getKind() == kind::TUPLE_TYPE);
-
- std::vector<Node> children;
- for(TypeNode::iterator i = type.begin(),
- i_end = type.end();
- i != i_end;
- ++i) {
- children.push_back((*i).mkGroundTerm());
- }
-
- return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
- }
-
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::TUPLE);
- NodeManagerScope nms(nodeManager);
-
- for(TNode::iterator i = n.begin(),
- i_end = n.end();
- i != i_end;
- ++i) {
- if(! (*i).isConst()) {
- return false;
- }
- }
-
- return true;
- }
-};/* struct TupleProperties */
-
-struct RecordTypeRule {
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- Assert(n.getKind() == kind::RECORD);
- NodeManagerScope nms(nodeManager);
- const Record& rec = n.getOperator().getConst<Record>();
- const Record::FieldVector& fields = rec.getFields();
- if(check) {
- Record::FieldVector::const_iterator i = fields.begin();
- for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
- child_it != child_it_end;
- ++child_it, ++i) {
- if(i == fields.end()) {
- throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
- }
- if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
- std::stringstream ss;
- ss << "record description types differ from record literal types\nDescription type: " << (*child_it).getType() << "\nLiteral type: " << (*i).second;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- if(i != fields.end()) {
- throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
- }
- }
- return nodeManager->mkRecordType(rec);
- }
-};/* struct RecordTypeRule */
-
-struct RecordSelectTypeRule {
- inline static Record::FieldVector::const_iterator record_find(const Record::FieldVector& fields, std::string name){
- for(Record::FieldVector::const_iterator i = fields.begin(), i_end = fields.end(); i != i_end; ++i){
- if((*i).first == name) {
- return i;
- }
- }
- return fields.end();
- }
-
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- Assert(n.getKind() == kind::RECORD_SELECT);
- NodeManagerScope nms(nodeManager);
- if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) {
- throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator");
- }
- const RecordSelect& rs = n.getOperator().getConst<RecordSelect>();
- TypeNode recordType = n[0].getType(check);
- if(!recordType.isRecord()) {
- if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) {
- throw TypeCheckingExceptionPrivate(n, "Record-select expression formed over non-record");
- }
- recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
- }
- const Record& rec = recordType.getRecord();
- const Record::FieldVector& fields = rec.getFields();
- Record::FieldVector::const_iterator field = record_find(fields, rs.getField());
- if(field == fields.end()) {
- std::stringstream ss;
- ss << "Record-select field `" << rs.getField()
- << "' is not a valid field name for the record type";
- throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
- }
- return TypeNode::fromType((*field).second);
- }
-};/* struct RecordSelectTypeRule */
-
struct RecordUpdateTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
Assert(n.getKind() == kind::RECORD_UPDATE);
TypeNode newValue = n[1].getType(check);
if(check) {
if(!recordType.isRecord()) {
- if(!recordType.hasAttribute(expr::DatatypeRecordAttr())) {
- throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record");
- }
- recordType = recordType.getAttribute(expr::DatatypeRecordAttr());
+ throw TypeCheckingExceptionPrivate(n, "Record-update expression formed over non-record");
}
const Record& rec = recordType.getRecord();
if(!rec.contains(ru.getField())) {
struct RecordProperties {
inline static Node mkGroundTerm(TypeNode type) {
Assert(type.getKind() == kind::RECORD_TYPE);
-
- const Record& rec = type.getRecord();
- const Record::FieldVector& fields = rec.getFields();
- std::vector<Node> children;
- for(Record::FieldVector::const_iterator i = fields.begin(),
- i_end = fields.end();
- i != i_end;
- ++i) {
- children.push_back((*i).second.mkGroundTerm());
- }
-
- return NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(rec), children);
+ return Node::null();
}
-
inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::RECORD);
- NodeManagerScope nms(nodeManager);
-
- for(TNode::iterator i = n.begin(),
- i_end = n.end();
- i != i_end;
- ++i) {
- if(! (*i).isConst()) {
- return false;
- }
- }
-
+ return true;
+ }
+ inline static Cardinality computeCardinality(TypeNode type) {
+ Cardinality card(1);
+ return card;
+ }
+ inline static bool isWellFounded(TypeNode type) {
return true;
}
};/* struct RecordProperties */
++*this; //increment( d_ctor );
AlwaysAssert( !isFinished() );
}
+
};/* DatatypesEnumerator */
-class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
- TypeEnumeratorProperties * d_tep;
- TypeEnumerator** d_enumerators;
-
- /** Allocate and initialize the delegate enumerators */
- void newEnumerators() {
- d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
- for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- d_enumerators[i] = new TypeEnumerator(getType()[i], d_tep);
- }
- }
-
- void deleteEnumerators() throw() {
- if(d_enumerators != NULL) {
- for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- delete d_enumerators[i];
- }
- delete [] d_enumerators;
- d_enumerators = NULL;
- }
- }
-
-public:
-
- TupleEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
- TypeEnumeratorBase<TupleEnumerator>(type), d_tep(tep) {
- Assert(type.isTuple());
- newEnumerators();
- }
-
- TupleEnumerator(const TupleEnumerator& te) throw() :
- TypeEnumeratorBase<TupleEnumerator>(te.getType()),
- d_tep(te.d_tep),
- d_enumerators(NULL) {
-
- if(te.d_enumerators != NULL) {
- newEnumerators();
- for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]);
- }
- }
- }
-
- virtual ~TupleEnumerator() throw() {
- deleteEnumerators();
- }
-
- Node operator*() throw(NoMoreValuesException) {
- if(isFinished()) {
- throw NoMoreValuesException(getType());
- }
-
- NodeBuilder<> nb(kind::TUPLE);
- for(size_t i = 0; i < getType().getNumChildren(); ++i) {
- nb << **d_enumerators[i];
- }
- return Node(nb);
- }
-
- TupleEnumerator& operator++() throw() {
- if(isFinished()) {
- return *this;
- }
-
- size_t i;
- for(i = 0; i < getType().getNumChildren(); ++i) {
- if(d_enumerators[i]->isFinished()) {
- *d_enumerators[i] = TypeEnumerator(getType()[i], d_tep);
- } else {
- ++*d_enumerators[i];
- return *this;
- }
- }
-
- deleteEnumerators();
-
- return *this;
- }
-
- bool isFinished() throw() {
- return d_enumerators == NULL;
- }
-
-};/* TupleEnumerator */
class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
TypeEnumeratorProperties * d_tep;
throw NoMoreValuesException(getType());
}
- NodeBuilder<> nb(kind::RECORD);
- Debug("te") << "record enumerator: creating record of type " << getType() << std::endl;
- nb << getType();
- const Record& rec = getType().getConst<Record>();
- for(size_t i = 0; i < rec.getNumFields(); ++i) {
- Debug("te") << " - " << i << " " << std::flush << "=> " << **d_enumerators[i] << std::endl;
- nb << **d_enumerators[i];
- }
- return Node(nb);
+
+ return Node::null();
}
RecordEnumerator& operator++() throw() {
continue;
}
TypeNode t = TypeSet::getType(it);
- if(t.isTuple() || t.isRecord()) {
- t = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
- }
//get properties of this type
bool isCorecursive = false;
void testMkAssociativeBadKind() {
std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
- TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException);
+ TS_ASSERT_THROWS( d_exprManager->mkAssociative(LEQ,vars), IllegalArgumentException);
}
};
projects / cvc5.git / commitdiff