Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
}
+RecordType ExprManager::mkRecordType(const Record& rec) {
+ NodeManagerScope nms(d_nodeManager);
+ return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+}
+
SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
NodeManagerScope nms(d_nodeManager);
std::vector<TypeNode> typeNodes;
return t;
}
-Expr ExprManager::mkVar(const std::string& name, Type type) {
+Expr ExprManager::mkVar(const std::string& name, Type type, bool isGlobal) {
Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
NodeManagerScope nms(d_nodeManager);
- Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
+ Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, isGlobal);
Debug("nm") << "set " << name << " on " << *n << std::endl;
INC_STAT_VAR(type, false);
return Expr(this, n);
}
-Expr ExprManager::mkVar(Type type) {
+Expr ExprManager::mkVar(Type type, bool isGlobal) {
Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
NodeManagerScope nms(d_nodeManager);
INC_STAT_VAR(type, false);
- return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
+ return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, isGlobal));
}
Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
*/
TupleType mkTupleType(const std::vector<Type>& types);
+ /**
+ * Make a record type with types from the rec parameter.
+ */
+ RecordType mkRecordType(const Record& rec);
+
/**
* Make a symbolic expressiontype with types from
* <code>types[0..types.size()-1]</code>. <code>types</code> may
throw(TypeCheckingException);
// variables are special, because duplicates are permitted
- Expr mkVar(const std::string& name, Type type);
- Expr mkVar(Type type);
+ Expr mkVar(const std::string& name, Type type, bool isGlobal = false);
+ Expr mkVar(Type type, bool isGlobal = false);
Expr mkBoundVar(const std::string& name, Type type);
Expr mkBoundVar(Type type);
lineno=${BASH_LINENO[0]}
check_theory_seen
typerules="${typerules}
+#line $lineno \"$kf\"
case kind::$1:
+#line $lineno \"$kf\"
typeNode = $2::computeType(nodeManager, n, check);
break;
"
lineno=${BASH_LINENO[0]}
check_theory_seen
construles="${construles}
+#line $lineno \"$kf\"
case kind::$1:
+#line $lineno \"$kf\"
return $2::computeIsConst(nodeManager, n);
"
}
std::string message) throw() :
Exception(message),
d_node(new Node(node)) {
+#ifdef CVC4_DEBUG
+ s_debugLastException = toString().c_str();
+#endif /* CVC4_DEBUG */
}
TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
/** The node responsible for the failure */
NodeTemplate<true>* d_node;
-protected:
-
- TypeCheckingExceptionPrivate() throw() : Exception() {}
-
public:
/**
}
if((flags & SKOLEM_NO_NOTIFY) == 0) {
for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewSkolem(n, comment);
+ (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL);
}
}
return n;
return TypeNode(mkTypeConst(bounds));
}
+TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
+ Assert(t.isTuple() || t.isRecord());
+
+ // if the type doesn't have an associated datatype, then make one for it
+ TypeNode& dtt = d_tupleAndRecordTypes[t];
+ 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;
+ } else {
+ const Record& rec = t.getRecord();
+ Datatype dt("__cvc4_record");
+ DatatypeConstructor c("__cvc4_record_ctor");
+ for(Record::const_iterator i = rec.begin(); i != rec.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(), t);
+ } else {
+ Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl;
+ }
+ Assert(!dtt.isNull());
+ return dtt;
+}
+
}/* CVC4 namespace */
namespace attr {
struct VarNameTag { };
struct SortArityTag { };
+ struct DatatypeTupleTag { };
+ struct DatatypeRecordTag { };
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
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;
}/* CVC4::expr namespace */
virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
- virtual void nmNotifyNewVar(TNode n) { }
- virtual void nmNotifyNewSkolem(TNode n, const std::string& comment) { }
+ virtual void nmNotifyNewVar(TNode n, bool isGlobal) { }
+ virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { }
};/* class NodeManagerListener */
class NodeManager {
friend class expr::TypeChecker;
// friends so they can access mkVar() here, which is private
- friend Expr ExprManager::mkVar(const std::string&, Type);
- friend Expr ExprManager::mkVar(Type);
+ friend Expr ExprManager::mkVar(const std::string&, Type, bool isGlobal);
+ friend Expr ExprManager::mkVar(Type, bool isGlobal);
// friend so it can access NodeManager's d_listeners and notify clients
friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
*/
std::vector<NodeManagerListener*> d_listeners;
+ /**
+ * A map of tuple and record types to their corresponding datatype.
+ */
+ std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
+
/**
* Look up a NodeValue in the pool associated to this NodeManager.
* The NodeValue argument need not be a "completely-constructed"
* version of this is private to avoid internal uses of mkVar() from
* within CVC4. Such uses should employ mkSkolem() instead.
*/
- Node mkVar(const std::string& name, const TypeNode& type);
- Node* mkVarPtr(const std::string& name, const TypeNode& type);
+ Node mkVar(const std::string& name, const TypeNode& type, bool isGlobal = false);
+ Node* mkVarPtr(const std::string& name, const TypeNode& type, bool isGlobal = false);
/** Create a variable with the given type. */
- Node mkVar(const TypeNode& type);
- Node* mkVarPtr(const TypeNode& type);
+ Node mkVar(const TypeNode& type, bool isGlobal = false);
+ Node* mkVarPtr(const TypeNode& type, bool isGlobal = false);
public:
enum SkolemFlags {
SKOLEM_DEFAULT = 0, /**< default behavior */
SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
- SKOLEM_EXACT_NAME = 2 /**< do not make the name unique by adding the id */
+ SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
+ SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */
};/* enum SkolemFlags */
/**
*/
inline 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);
+
/**
* Make a symbolic expression type with types from
* <code>types</code>. <code>types</code> may have any number of
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::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) {
}
-inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
+inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bool isGlobal) {
Node n = NodeBuilder<0>(this, kind::VARIABLE);
setAttribute(n, TypeAttr(), type);
setAttribute(n, TypeCheckedAttr(), true);
setAttribute(n, expr::VarNameAttr(), name);
for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewVar(n);
+ (*i)->nmNotifyNewVar(n, isGlobal);
}
return n;
}
inline Node* NodeManager::mkVarPtr(const std::string& name,
- const TypeNode& type) {
+ const TypeNode& type, bool isGlobal) {
Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
setAttribute(*n, TypeAttr(), type);
setAttribute(*n, TypeCheckedAttr(), true);
setAttribute(*n, expr::VarNameAttr(), name);
for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewVar(*n);
+ (*i)->nmNotifyNewVar(*n, isGlobal);
}
return n;
}
return n;
}
-inline Node NodeManager::mkVar(const TypeNode& type) {
+inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) {
Node n = NodeBuilder<0>(this, kind::VARIABLE);
setAttribute(n, TypeAttr(), type);
setAttribute(n, TypeCheckedAttr(), true);
for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewVar(n);
+ (*i)->nmNotifyNewVar(n, isGlobal);
}
return n;
}
-inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
+inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) {
Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
setAttribute(*n, TypeAttr(), type);
setAttribute(*n, TypeCheckedAttr(), true);
for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewVar(*n);
+ (*i)->nmNotifyNewVar(*n, isGlobal);
}
return n;
}
return TupleType(*this);
}
+/** Is this a record type? */
+bool Type::isRecord() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isRecord();
+}
+
+/** Cast to a record type */
+Type::operator RecordType() const throw(IllegalArgumentException) {
+ NodeManagerScope nms(d_nodeManager);
+ CheckArgument(isNull() || isRecord(), this);
+ return RecordType(*this);
+}
+
/** 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;
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;
CheckArgument(isNull() || isTuple(), this);
}
+RecordType::RecordType(const Type& t) throw(IllegalArgumentException) :
+ Type(t) {
+ CheckArgument(isNull() || isRecord(), this);
+}
+
SExprType::SExprType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
CheckArgument(isNull() || isSExpr(), this);
}
const Datatype& DatatypeType::getDatatype() const {
+ NodeManagerScope nms(d_nodeManager);
if( d_typeNode->isParametricDatatype() ) {
CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
return dt;
} else {
- return d_typeNode->getConst<Datatype>();
+ return d_typeNode->getDatatype();
}
}
class SmtEngine;
class Datatype;
+class Record;
template <bool ref_count>
class NodeTemplate;
class TesterType;
class FunctionType;
class TupleType;
+class RecordType;
class SExprType;
class SortType;
class SortConstructorType;
*/
operator TupleType() const throw(IllegalArgumentException);
+ /**
+ * Is this a record type?
+ * @return true if the type is a record type
+ */
+ bool isRecord() const;
+
+ /**
+ * Cast this type to a record type
+ * @return the RecordType
+ */
+ operator RecordType() const throw(IllegalArgumentException);
+
/**
* Is this a symbolic expression type?
* @return true if the type is a symbolic expression type
/** 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.
*/
t.getConst<TypeConstant>() == REAL_TYPE );
}
}
+ if(isTuple() || isRecord()) {
+ if(t == NodeManager::currentNM()->getDatatypeForTupleRecord(*this)) {
+ return true;
+ }
+ if(isTuple() != t.isTuple() || isRecord() != t.isRecord() ||
+ getNumChildren() != t.getNumChildren()) {
+ 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;
+ }
+ }
+ return true;
+ }
if(isPredicateSubtype()) {
return getSubtypeParentType().isSubtypeOf(t);
}
if(isSubtypeOf(NodeManager::currentNM()->realType())) {
return t.isSubtypeOf(NodeManager::currentNM()->realType());
}
+ if(t.isDatatype() && (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() ||
+ 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;
+ }
+ }
+ 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);
+ }
if(isPredicateSubtype()) {
return t.isComparableTo(getSubtypeParentType());
}
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();
}
return params;
}
+size_t TypeNode::getTupleLength() const {
+ Assert(isTuple());
+ return getNumChildren();
+}
+
vector<TypeNode> TypeNode::getTupleTypes() const {
Assert(isTuple());
vector<TypeNode> types;
return types;
}
+const Record& TypeNode::getRecord() const {
+ Assert(isRecord());
+ return getConst<Record>();
+}
+
vector<TypeNode> TypeNode::getSExprTypes() const {
Assert(isSExpr());
vector<TypeNode> types;
Assert(!t0.isNull());
Assert(!t1.isNull());
- if(EXPECT_TRUE(t0 == t1)){
+ if(EXPECT_TRUE(t0 == t1)) {
return t0;
- }else{ // t0 != t1
- if(t0.getKind()== kind::TYPE_CONSTANT){
+ } else { // t0 != t1
+ if(t0.getKind()== kind::TYPE_CONSTANT) {
switch(t0.getConst<TypeConstant>()) {
case INTEGER_TYPE:
- if(t1.isInteger()){
+ if(t1.isInteger()) {
// t0 == IntegerType && t1.isInteger()
return t0; //IntegerType
- }else if(t1.isReal()){
+ } else if(t1.isReal()) {
// t0 == IntegerType && t1.isReal() && !t1.isInteger()
return NodeManager::currentNM()->realType(); // RealType
- }else{
- return TypeNode(); //null type
+ } else {
+ return TypeNode(); // null type
}
case REAL_TYPE:
- if(t1.isReal()){
+ if(t1.isReal()) {
return t0; // RealType
- }else{
+ } else {
return TypeNode(); // null type
}
default:
- if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){
+ if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
return t0; // t0 is a constant type
- }else{
+ } else {
return TypeNode(); // null type
}
}
- }else if(t1.getKind() == kind::TYPE_CONSTANT){
+ } else if(t1.getKind() == kind::TYPE_CONSTANT) {
return leastCommonTypeNode(t1, t0); //decrease the number of special cases
- }else{
+ } else {
// t0 != t1 &&
// t0.getKind() == kind::TYPE_CONSTANT &&
// t1.getKind() == kind::TYPE_CONSTANT
- switch(t0.getKind()){
+ switch(t0.getKind()) {
case kind::ARRAY_TYPE:
case kind::BITVECTOR_TYPE:
case kind::SORT_TYPE:
case kind::CONSTRUCTOR_TYPE:
case kind::SELECTOR_TYPE:
case kind::TESTER_TYPE:
- if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)){
+ if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
return t0;
- }else{
+ } else {
return TypeNode();
}
case kind::FUNCTION_TYPE:
case kind::SEXPR_TYPE:
Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
return TypeNode(); // Not sure if this is right
- case kind::TUPLE_TYPE:
- Unimplemented("haven't implemented leastCommonType for tuples yet");
- return TypeNode(); // Not sure if this is right
case kind::SUBTYPE_TYPE:
if(t1.isPredicateSubtype()){
// This is the case where both t0 and t1 are predicate subtypes.
return leastCommonPredicateSubtype(t0, t1);
- }else{ //t0 is a predicate subtype and t1 is not
+ }else{ // t0 is a predicate subtype and t1 is not
return leastCommonTypeNode(t1, t0); //decrease the number of special cases
}
case kind::SUBRANGE_TYPE:
- if(t1.isSubrange()){
- const SubrangeBounds& t0SR= t0.getSubrangeBounds();
+ if(t1.isSubrange()) {
+ const SubrangeBounds& t0SR = t0.getSubrangeBounds();
const SubrangeBounds& t1SR = t1.getSubrangeBounds();
- if(SubrangeBounds::joinIsBounded(t0SR, t1SR)){
+ if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) {
SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR);
return NodeManager::currentNM()->mkSubrangeType(j);
- }else{
+ } else {
return NodeManager::currentNM()->integerType();
}
- }else if(t1.isPredicateSubtype()){
- //t0 is a subrange
- //t1 is not a subrange
- //t1 is a predicate subtype
- if(t1.isInteger()){
+ } else if(t1.isPredicateSubtype()) {
+ // t0 is a subrange
+ // t1 is not a subrange
+ // t1 is a predicate subtype
+ if(t1.isInteger()) {
return NodeManager::currentNM()->integerType();
- }else if(t1.isReal()){
+ } else if(t1.isReal()) {
return NodeManager::currentNM()->realType();
- }else{
+ } else {
return TypeNode();
}
- }else{
- //t0 is a subrange
- //t1 is not a subrange
+ } else {
+ // t0 is a subrange
+ // t1 is not a subrange
// t1 is not a type constant && is not a predicate subtype
// t1 cannot be real subtype or integer.
Assert(t1.isReal());
Assert(t1.isInteger());
return TypeNode();
}
+ 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>();
+ // construct childwise leastCommonType, if one exists
+ for(Record::const_iterator i = r0.begin(), j = r1.begin(); i != r0.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:
- // two datatypes that aren't == have no common ancestors
+ // t1 might be a subtype tuple or record
+ if(t1.getBaseType() == t0) {
+ return t0;
+ }
+ // otherwise no common ancestor
return TypeNode();
default:
Unimplemented("don't have a leastCommonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str());
/** Is this a tuple type? */
bool isTuple() const;
+ /** Get the length of a tuple type */
+ size_t getTupleLength() const;
+
/** Get the constituent types of a tuple type */
std::vector<TypeNode> getTupleTypes() const;
+ /** Is this a record type? */
+ bool isRecord() const;
+
+ /** Get the description of the record type */
+ const Record& getRecord() const;
+
/** Is this a symbolic expression type? */
bool isSExpr() const;
/** Is this a tester type */
bool isTester() const;
+ /** Get the Datatype specification from a datatype type */
+ const Datatype& getDatatype() const;
+
/** Get the size of this bit-vector type */
unsigned getBitVectorSize() const;
( 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() );
}
( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) );
}
+/** 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>();
+ }
+}
+
/** Get the size of this bit-vector type */
inline unsigned TypeNode::getBitVectorSize() const {
Assert(isBitVector());
**
** \brief Parser for CVC presentation input language
**
- ** Parser for CVC input language.
+ ** Parser for CVC presentation input language.
**/
grammar Cvc;
// NOTE: do not clear the vectors here!
}
: identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED]
- { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t);
+ { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t, false);
terms.insert(terms.end(), vars.begin(), vars.end());
for(unsigned i = 0; i < vars.size(); ++i) {
types.push_back(t);
}
} else {
Debug("parser") << " " << *i << " not declared" << std::endl;
- Expr func = PARSER_STATE->mkVar(*i, t);
+ Expr func = PARSER_STATE->mkVar(*i, t, true);
if(topLevel) {
Command* decl = new DeclareFunctionCommand(*i, func, t);
seq->addCommand(decl);
i != i_end;
++i) {
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
- Expr func = EXPR_MANAGER->mkVar(*i, t);
+ Expr func = EXPR_MANAGER->mkVar(*i, t, true);
PARSER_STATE->defineFunction(*i, f);
Command* decl = new DefineFunctionCommand(*i, func, f);
seq->addCommand(decl);
}
} else {
// tuple type [ T, U, V... ]
- t = PARSER_STATE->mkTupleType(types);
+ t = EXPR_MANAGER->mkTupleType(types);
}
}
/* record types */
| SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ
- { t = PARSER_STATE->mkRecordType(typeIds); }
+ { t = EXPR_MANAGER->mkRecordType(typeIds); }
/* bitvector types */
| BITVECTOR_TOK LPAREN k=numeral RPAREN
boundVarDecl[ids,t] RPAREN COLON formula[f]
{ PARSER_STATE->popScope();
UNSUPPORTED("array literals not supported yet");
- f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()));
+ f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), true);
}
;
: k=numeral ASSIGN_TOK uminusTerm[f2]
{
Type t = f.getType();
- if(! t.isDatatype()) {
+ if(! t.isTuple()) {
PARSER_STATE->parseError("tuple-update applied to non-tuple");
}
- Datatype tuple = DatatypeType(f.getType()).getDatatype();
- if(tuple.getName() != "__cvc4_tuple") {
- PARSER_STATE->parseError("tuple-update applied to non-tuple");
- }
- if(k < tuple[0].getNumArgs()) {
- std::vector<Expr> args;
- for(unsigned i = 0; i < tuple[0].getNumArgs(); ++i) {
- if(i == k) {
- args.push_back(f2);
- } else {
- Expr selectorOp = tuple[0][i].getSelector();
- Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- args.push_back(select);
- }
- }
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, tuple[0].getConstructor(), args);
- } else {
+ size_t length = TupleType(t).getLength();
+ if(k >= length) {
std::stringstream ss;
- ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot update index " << k;
+ ss << "tuple is of length " << length << "; cannot update index " << k;
PARSER_STATE->parseError(ss.str());
}
+ f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2);
}
;
: identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
{
Type t = f.getType();
- if(! t.isDatatype()) {
- PARSER_STATE->parseError("record-update applied to non-record");
- }
- Datatype record = DatatypeType(f.getType()).getDatatype();
- if(record.getName() != "__cvc4_record") {
+ if(! t.isRecord()) {
PARSER_STATE->parseError("record-update applied to non-record");
}
- const DatatypeConstructorArg* updateArg = 0;
- try {
- updateArg = &record[0][id];
- } catch(IllegalArgumentException& e) {
+ const Record& rec = RecordType(t).getRecord();
+ Record::const_iterator fld = rec.find(id);
+ if(fld == rec.end()) {
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
- std::vector<Expr> args;
- for(unsigned i = 0; i < record[0].getNumArgs(); ++i) {
- const DatatypeConstructorArg* thisArg = &record[0][i];
- if(thisArg == updateArg) {
- args.push_back(f2);
- } else {
- Expr selectorOp = record[0][i].getSelector();
- Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- args.push_back(select);
- }
- }
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, record[0].getConstructor(), args);
+ f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2);
}
;
| DOT
( identifier[id,CHECK_NONE,SYM_VARIABLE]
{ Type t = f.getType();
- if(! t.isDatatype()) {
+ if(! t.isRecord()) {
PARSER_STATE->parseError("record-select applied to non-record");
}
- Datatype record = DatatypeType(f.getType()).getDatatype();
- if(record.getName() != "__cvc4_record") {
- PARSER_STATE->parseError("record-select applied to non-record");
- }
- try {
- Expr selectorOp = record[0][id].getSelector();
- f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- } catch(IllegalArgumentException& e) {
+ const Record& rec = RecordType(t).getRecord();
+ Record::const_iterator fld = rec.find(id);
+ if(fld == rec.end()) {
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
+ f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
}
| k=numeral
{ Type t = f.getType();
- if(! t.isDatatype()) {
- PARSER_STATE->parseError("tuple-select applied to non-tuple");
- }
- Datatype tuple = DatatypeType(f.getType()).getDatatype();
- if(tuple.getName() != "__cvc4_tuple") {
+ if(! t.isTuple()) {
PARSER_STATE->parseError("tuple-select applied to non-tuple");
}
- try {
- Expr selectorOp = tuple[0][k].getSelector();
- f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- } catch(IllegalArgumentException& e) {
+ size_t length = TupleType(t).getLength();
+ if(k >= length) {
std::stringstream ss;
- ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot access index " << k;
+ ss << "tuple is of length " << length << "; cannot access index " << k;
PARSER_STATE->parseError(ss.str());
}
+ f = MK_EXPR(MK_CONST(TupleSelect(k)), f);
}
)
)*
for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
types.push_back((*i).getType());
}
- DatatypeType t = PARSER_STATE->mkTupleType(types);
- f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args);
+ TupleType t = EXPR_MANAGER->mkTupleType(types);
+ f = MK_EXPR(kind::TUPLE, args);
}
}
for(unsigned i = 0; i < names.size(); ++i) {
typeIds.push_back(std::make_pair(names[i], args[i].getType()));
}
- DatatypeType t = PARSER_STATE->mkRecordType(typeIds);
- f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args);
+ RecordType t = EXPR_MANAGER->mkRecordType(typeIds);
+ f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args);
}
/* variable / zero-ary constructor application */
Expr
Parser::mkVar(const std::string& name, const Type& type,
bool levelZero) {
- Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
- Expr expr = d_exprManager->mkVar(name, type);
+ Debug("parser") << "mkVar(" << name << ", " << type << ", " << levelZero << ")" << std::endl;
+ Expr expr = d_exprManager->mkVar(name, type, levelZero);
defineVar(name, expr, levelZero);
return expr;
}
Parser::mkFunction(const std::string& name, const Type& type,
bool levelZero) {
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
- Expr expr = d_exprManager->mkVar(name, type);
+ Expr expr = d_exprManager->mkVar(name, type, levelZero);
defineFunction(name, expr, levelZero);
return expr;
}
return types;
}
-DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds) {
- DatatypeType& dtt = d_recordTypes[typeIds];
- if(dtt.isNull()) {
- Datatype dt("__cvc4_record");
-Debug("datatypes") << "make new record_ctor" << std::endl;
- DatatypeConstructor c("__cvc4_record_ctor");
- for(std::vector< std::pair<std::string, Type> >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) {
- c.addArg((*i).first, (*i).second);
- }
- dt.addConstructor(c);
- dtt = d_exprManager->mkDatatypeType(dt);
- } else {
-Debug("datatypes") << "use old record_ctor" << std::endl;
-}
- return dtt;
-}
-
-DatatypeType Parser::mkTupleType(const std::vector<Type>& types) {
- DatatypeType& dtt = d_tupleTypes[types];
- if(dtt.isNull()) {
- Datatype dt("__cvc4_tuple");
- DatatypeConstructor c("__cvc4_tuple_ctor");
- for(std::vector<Type>::const_iterator i = types.begin(); i != types.end(); ++i) {
- c.addArg("__cvc4_tuple_stor", *i);
- }
- dt.addConstructor(c);
- dtt = d_exprManager->mkDatatypeType(dt);
- }
- return dtt;
-}
-
bool Parser::isDeclared(const std::string& name, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
/** Are we only parsing? */
bool d_parseOnly;
- /**
- * We might see the same record type multiple times; we have
- * to match always to the same Type. This map contains all the
- * record types we have.
- */
- std::map<std::vector< std::pair<std::string, Type> >, DatatypeType> d_recordTypes;
-
- /**
- * We might see the same tuple type multiple times; we have
- * to match always to the same Type. This map contains all the
- * tuple types we have.
- */
- std::map<std::vector<Type>, DatatypeType> d_tupleTypes;
-
/** The set of operators available in the current logic. */
std::set<Kind> d_logicOperators;
std::vector<DatatypeType>
mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
- /**
- * Create a record type, or if there's already a matching one, return that one.
- */
- DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds);
-
- /**
- * Create a tuple type, or if there's already a matching one, return that one.
- */
- DatatypeType mkTupleType(const std::vector<Type>& types);
-
/**
* Add an operator to the current legal set.
*
out << ']';
return;
break;
- case kind::TUPLE:
case kind::SEXPR:
// no-op
break;
break;
// DATATYPES
+ case kind::APPLY_TYPE_ASCRIPTION: {
+ toStream(out, n[0], depth, types, false);
+ out << "::";
+ TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
+ out << (t.isFunctionLike() ? t.getRangeType() : t);
+ }
+ return;
+ break;
case kind::APPLY_CONSTRUCTOR:
case kind::APPLY_SELECTOR:
case kind::APPLY_TESTER:
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::RECORD_UPDATE:
+ toStream(out, n[0], depth, types, true);
+ out << " WITH ." << n.getOperator().getConst<RecordUpdate>().getField() << " := ";
+ 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;
+ for(Record::const_iterator j = rec.begin(); j != rec.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:
op << ">=";
opType = INFIX;
break;
+ case kind::PARAMETRIC_DATATYPE:
+ out << n[0].getConst<Datatype>().getName();
+ break;
// BITVECTORS
case kind::BITVECTOR_XOR:
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
if( tn.isSort() ){
- //print the cardinality
+ // print the cardinality
if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
}
}
out << c << std::endl;
if( tn.isSort() ){
- //print the representatives
+ // print the representatives
if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
}else{
out << tn;
}
- out << " = " << tm.getValue( n ) << ";" << std::endl;
+ out << " = " << tm.getValue(n.toExpr()) << ";" << std::endl;
/*
//for table format (work in progress)
}
static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
- out << "% (get-value ( ";
const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
- out << " ))";
+ Assert(!terms.empty());
+ out << "GET_VALUE ";
+ copy(terms.begin(), terms.end() - 1, ostream_iterator<Expr>(out, ";\nGET_VALUE "));
+ out << terms.back() << ";";
}
static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
break;
// datatypes
+ case kind::APPLY_TYPE_ASCRIPTION: {
+ out << "as ";
+ toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
+ out << ' ';
+ TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
+ out << (t.isFunctionLike() ? t.getRangeType() : t);
+ stillNeedToPrintParams = false;
+ }
+ break;
case kind::APPLY_TESTER:
case kind::APPLY_CONSTRUCTOR:
case kind::APPLY_SELECTOR:
libsmt_la_SOURCES = \
smt_engine.cpp \
smt_engine.h \
+ model_postprocessor.cpp \
+ model_postprocessor.h \
smt_engine_scope.cpp \
smt_engine_scope.h \
command_list.cpp \
--- /dev/null
+/********************* */
+/*! \file model_postprocessor.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief
+ **
+ **
+ **/
+
+#include "smt/model_postprocessor.h"
+
+using namespace CVC4;
+using namespace CVC4::smt;
+
+void ModelPostprocessor::visit(TNode current, TNode parent) {
+ Debug("tuprec") << "visiting " << current << std::endl;
+ Assert(!alreadyVisited(current, TNode::null()));
+ if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
+ Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+ NodeBuilder<> b(kind::TUPLE);
+ for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+ Assert(alreadyVisited(*i, TNode::null()));
+ TNode n = d_nodes[*i];
+ b << (n.isNull() ? *i : n);
+ }
+ d_nodes[current] = b;
+ Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+ } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
+ Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+ NodeBuilder<> b(kind::RECORD);
+ b << current.getType().getAttribute(expr::DatatypeRecordAttr());
+ for(TNode::iterator i = current.begin(); i != current.end(); ++i) {
+ Assert(alreadyVisited(*i, TNode::null()));
+ TNode n = d_nodes[*i];
+ b << (n.isNull() ? *i : n);
+ }
+ d_nodes[current] = b;
+ Debug("tuprec") << "returning " << d_nodes[current] << std::endl;
+ } else {
+ Debug("tuprec") << "returning self" << std::endl;
+ // rewrite to self
+ d_nodes[current] = Node::null();
+ }
+}/* ModelPostprocessor::visit() */
+
--- /dev/null
+/********************* */
+/*! \file model_postprocessor.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief
+ **
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MODEL_POSTPROCESSOR_H
+#define __CVC4__MODEL_POSTPROCESSOR_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace smt {
+
+class ModelPostprocessor {
+public:
+ typedef Node return_type;
+ std::hash_map<TNode, Node, TNodeHashFunction> d_nodes;
+
+ bool alreadyVisited(TNode current, TNode parent) {
+ return d_nodes.find(current) != d_nodes.end();
+ }
+
+ void visit(TNode current, TNode parent);
+
+ void start(TNode n) { }
+
+ Node done(TNode n) {
+ Assert(alreadyVisited(n, TNode::null()));
+ TNode retval = d_nodes[n];
+ return retval.isNull() ? n : retval;
+ }
+};/* class ModelPostprocessor */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MODEL_POSTPROCESSOR_H */
#include "smt/modal_exception.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
+#include "smt/model_postprocessor.h"
#include "theory/theory_engine.h"
#include "theory/bv/theory_bv_rewriter.h"
#include "proof/proof_manager.h"
#include "util/proof.h"
#include "util/boolean_simplification.h"
+#include "util/node_visitor.h"
#include "util/configuration.h"
#include "util/exception.h"
#include "smt/command_list.h"
d_smt.addToModelCommandAndDump(c);
}
- void nmNotifyNewVar(TNode n) {
+ void nmNotifyNewVar(TNode n, bool isGlobal) {
DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
n.toExpr(),
n.getType().toType());
- d_smt.addToModelCommandAndDump(c);
+ d_smt.addToModelCommandAndDump(c, isGlobal);
}
- void nmNotifyNewSkolem(TNode n, const std::string& comment) {
+ void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) {
std::string id = n.getAttribute(expr::VarNameAttr());
DeclareFunctionCommand c(id,
n.toExpr(),
if(Dump.isOn("skolems") && comment != "") {
Dump("skolems") << CommentCommand(id + " is " + comment);
}
- d_smt.addToModelCommandAndDump(c, false, "skolems");
+ d_smt.addToModelCommandAndDump(c, isGlobal, false, "skolems");
}
Node applySubstitutions(TNode node) const {
d_definedFunctions(NULL),
d_assertionList(NULL),
d_assignments(NULL),
+ d_modelGlobalCommands(),
d_modelCommands(NULL),
d_dumpCommands(),
d_logic(),
return false;
}
-
void SmtEnginePrivate::processAssertions() {
Assert(d_smt.d_fullyInited);
Assert(d_smt.d_pendingPops == 0);
// Add the formula
d_problemExtended = true;
+ if(d_assertionList != NULL) {
+ d_assertionList->push_back(e.notExpr());
+ }
d_private->addFormula(e.getNode().notNode());
// Run the check
return quickCheck().asValidityResult();
}
+Node SmtEngine::postprocess(TNode node) {
+ ModelPostprocessor mpost;
+ NodeVisitor<ModelPostprocessor> visitor;
+ return visitor.run(mpost, node);
+}
+
Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
// Make sure all preprocessing is done
d_private->processAssertions();
- return d_private->simplify(Node::fromExpr(e)).toExpr();
+ Node n = d_private->simplify(Node::fromExpr(e));
+ n = postprocess(n);
+ return n.toExpr();
}
Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) {
Dump("benchmark") << ExpandDefinitionsCommand(e);
}
hash_map<Node, Node, NodeHashFunction> cache;
- return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
+ Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+ n = postprocess(n);
+ return n.toExpr();
}
Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
Trace("smt") << "--- getting value of " << n << endl;
TheoryModel* m = d_theoryEngine->getModel();
Node resultNode;
- if( m ){
- resultNode = m->getValue( n );
+ if(m != NULL) {
+ resultNode = m->getValue(n);
}
Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
+ resultNode = postprocess(resultNode);
+ Trace("smt") << "--- model-post returned " << resultNode << endl;
// type-check the result we got
Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType()));
return SExpr(sexprs);
}
-void SmtEngine::addToModelCommandAndDump(const Command& c, bool userVisible, const char* dumpTag) {
+void SmtEngine::addToModelCommandAndDump(const Command& c, bool isGlobal, bool userVisible, const char* dumpTag) {
Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
SmtScope smts(this);
// If we aren't yet fully inited, the user might still turn on
// and expects to find their cardinalities in the model.
if(/* userVisible && */ (!d_fullyInited || options::produceModels())) {
doPendingPops();
- d_modelCommands->push_back(c.clone());
+ if(isGlobal) {
+ d_modelGlobalCommands.push_back(c.clone());
+ } else {
+ d_modelCommands->push_back(c.clone());
+ }
}
if(Dump.isOn(dumpTag)) {
if(d_fullyInited) {
typedef context::CDList<Command*, CommandCleanup> CommandList;
}/* CVC4::smt namespace */
+namespace theory {
+ class TheoryModel;
+}/* CVC4::theory namespace */
+
namespace stats {
StatisticsRegistry* getStatisticsRegistry(SmtEngine*);
}/* CVC4::stats namespace */
AssignmentSet* d_assignments;
/**
- * A list of commands that should be in the Model. Only maintained
- * if produce-models option is on.
+ * A list of commands that should be in the Model globally (i.e.,
+ * regardless of push/pop). Only maintained if produce-models option
+ * is on.
+ */
+ std::vector<Command*> d_modelGlobalCommands;
+
+ /**
+ * A list of commands that should be in the Model locally (i.e.,
+ * it is context-dependent on push/pop). Only maintained if
+ * produce-models option is on.
*/
smt::CommandList* d_modelCommands;
*/
void checkModel(bool hardFailure = true);
+ /**
+ * Postprocess a value for output to the user. Involves doing things
+ * like turning datatypes back into tuples, length-1-bitvectors back
+ * into booleans, etc.
+ */
+ Node postprocess(TNode n);
+
/**
* This is something of an "init" procedure, but is idempotent; call
* as often as you like. Should be called whenever the final options
friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
// to access d_modelCommands
friend class ::CVC4::Model;
+ friend class ::CVC4::theory::TheoryModel;
// to access getModel(), which is private (for now)
friend class GetModelCommand;
* Add to Model command. This is used for recording a command
* that should be reported during a get-model call.
*/
- void addToModelCommandAndDump(const Command& c, bool userVisible = true, const char* dumpTag = "declarations");
+ void addToModelCommandAndDump(const Command& c, bool isGlobal = false, bool userVisible = true, const char* dumpTag = "declarations");
/**
* Get the model (only if immediately preceded by a SAT
variable VARIABLE "variable"
variable BOUND_VARIABLE "bound variable"
variable SKOLEM "skolem var"
-operator TUPLE 1: "a tuple"
operator SEXPR 0: "a symbolic expression"
operator LAMBDA 2 "lambda"
"::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
well-founded FUNCTION_TYPE false
-operator TUPLE_TYPE 1: "tuple type"
-cardinality TUPLE_TYPE \
- "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
- "theory/builtin/theory_builtin_type_rules.h"
-well-founded TUPLE_TYPE \
- "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
- "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
- "theory/builtin/theory_builtin_type_rules.h"
operator SEXPR_TYPE 0: "symbolic expression type"
cardinality SEXPR_TYPE \
"::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
-typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
}
};/* class DistinctTypeRule */
-class TupleTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
- 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);
- }
-};/* class TupleTypeRule */
-
class SExprTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
}
};/* class FuctionProperties */
-class TupleProperties {
-public:
- 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);
- }
-};/* class TupleProperties */
-
class SExprProperties {
public:
inline static Cardinality computeCardinality(TypeNode type) {
}
}
}
+ 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 &&
+ (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 &&
in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
// Have to be careful not to rewrite well-typed expressions
}
}
}
+ 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.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 inline void shutdown() {}
static bool checkClash( Node n1, Node n2 ) {
- if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
+ 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.getOperator() != n2.getOperator() ) {
return true;
} else {
/** is this term a datatype */
static bool isTermDatatype( Node n ){
TypeNode tn = n.getType();
- return tn.isDatatype() || tn.isParametricDatatype();
+ return tn.isDatatype() || tn.isParametricDatatype() ||
+ tn.isTuple() || tn.isRecord();
}
};/* class DatatypesRewriter */
# constructor applications are constant if they are applied only to constants
construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
+operator TUPLE_TYPE 1: "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 1: "a tuple"
+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"
+parameterized TUPLE_SELECT TUPLE_SELECT_OP 1 "tuple select"
+typerule TUPLE_SELECT ::CVC4::theory::datatypes::TupleSelectTypeRule
+
+constant TUPLE_UPDATE_OP \
+ ::CVC4::TupleUpdate \
+ ::CVC4::TupleUpdateHashFunction \
+ "util/tuple.h" \
+ "operator for a tuple update"
+parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update"
+typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
+
+constant RECORD_TYPE \
+ ::CVC4::Record \
+ "::CVC4::RecordHashFunction" \
+ "util/record.h" \
+ "record type"
+cardinality RECORD_TYPE \
+ "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
+ "theory/datatypes/theory_datatypes_type_rules.h"
+well-founded RECORD_TYPE \
+ "::CVC4::theory::datatypes::TupleProperties::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 1: "a record"
+typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule
+construle RECORD ::CVC4::theory::datatypes::RecordProperties
+
+constant RECORD_SELECT_OP \
+ ::CVC4::RecordSelect \
+ ::CVC4::RecordSelectHashFunction \
+ "util/record.h" \
+ "operator for a record select"
+parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select"
+typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule
+
+constant RECORD_UPDATE_OP \
+ ::CVC4::RecordUpdate \
+ ::CVC4::RecordUpdateHashFunction \
+ "util/record.h" \
+ "operator for a record update"
+parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update"
+typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule
+
endtheory
#include "util/cvc4_assert.h"
#include "theory/datatypes/theory_datatypes_instantiator.h"
#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "theory/model.h"
#include "smt/options.h"
Assertion assertion = get();
TNode fact = assertion.assertion;
Trace("datatypes-assert") << "Assert " << fact << std::endl;
+
+ TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
+
+ // 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 ),
+ "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
+
//assert the fact
assertFact( fact, fact );
flushPendingFacts();
Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
}
+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, 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, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
+ }
+
+ // 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) {
+ // nothing to do
+ return in;
+ }
+
+ TypeNode t = in.getType();
+
+ 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) {
+ NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
+ b << Node::fromExpr(dt[0].getConstructor());
+ size_t size, updateIndex;
+ if(in.getKind() == kind::TUPLE_UPDATE) {
+ size = t.getNumChildren();
+ updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
+ } else { // kind::RECORD_UPDATE
+ const Record& record = t.getConst<Record>();
+ size = record.getNumFields();
+ updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
+ }
+ Debug("tuprec") << "expr is " << in << std::endl;
+ Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
+ Debug("tuprec") << "t is " << t << std::endl;
+ Debug("tuprec") << "t has arity " << size << std::endl;
+ for(size_t i = 0; i < size; ++i) {
+ if(i == updateIndex) {
+ b << in[1];
+ Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
+ } else {
+ b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]);
+ Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
+ }
+ }
+ Debug("tuprec") << "builder says " << b << std::endl;
+ n = b;
+ }
+
+ Assert(!n.isNull());
+
+ Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
+
+ return n;
+}
+
void TheoryDatatypes::addSharedTerm(TNode t) {
Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
<< t << endl;
Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
collectTerms( n_ic );
//add type ascription for ambiguous constructor types
- if( n_ic.getType()!=n.getType() ){
+ if(!n_ic.getType().isComparableTo(n.getType())) {
Assert( dt.isParametric() );
Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
/** inferences */
NodeList d_infer;
NodeList d_infer_exp;
+
private:
//notification class for equality engine
class NotifyClass : public eq::EqualityEngineNotify {
void check(Effort e);
void preRegisterTerm(TNode n);
+ Node ppRewrite(TNode n);
void presolve();
void addSharedTerm(TNode t);
EqualityStatus getEqualityStatus(TNode a, TNode b);
#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
#include "util/matcher.h"
+#include "expr/attribute.h"
namespace CVC4 {
TypeNode childType = (*child_it).getType(check);
Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl;
TypeNode argumentType = *tchild_it;
- if(!childType.isSubtypeOf(argumentType)) {
+ if(!childType.isComparableTo(argumentType)) {
std::stringstream ss;
ss << "bad type for constructor argument:\nexpected: " << argumentType << "\ngot : " << childType;
throw TypeCheckingExceptionPrivate(n, ss.str());
Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
Debug("typecheck-idt") << "sel type: " << selType << std::endl;
TypeNode childType = n[0].getType(check);
- if(selType[0] != childType) {
+ if(!selType[0].isComparableTo(childType)) {
Debug("typecheck-idt") << "ERROR: " << selType[0].getKind() << " " << childType.getKind() << std::endl;
throw TypeCheckingExceptionPrivate(n, "bad type for selector argument");
}
Type t = testType[0].toType();
Assert( t.isDatatype() );
DatatypeType dt = DatatypeType(t);
- if( dt.isParametric() ){
+ if(dt.isParametric()) {
Debug("typecheck-idt") << "typecheck parameterized tester: " << n << std::endl;
Matcher m( dt );
if( !m.doMatching( testType[0], childType ) ){
throw TypeCheckingExceptionPrivate(n, "matching failed for tester argument of parameterized datatype");
}
- }else{
+ } else {
Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
Debug("typecheck-idt") << "test type: " << testType << std::endl;
- if(testType[0] != childType) {
+ if(!testType[0].isComparableTo(childType)) {
throw TypeCheckingExceptionPrivate(n, "bad type for tester argument");
}
}
}
};/* 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);
+ const TupleSelect& ts = n.getOperator().getConst<TupleSelect>();
+ TypeNode tupleType = n[0].getType(check);
+ if(!tupleType.isTuple()) {
+ if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) {
+ 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);
+ const TupleUpdate& tu = n.getOperator().getConst<TupleUpdate>();
+ TypeNode tupleType = n[0].getType(check);
+ TypeNode newValue = n[1].getType(check);
+ if(check) {
+ if(!tupleType.isTuple()) {
+ if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) {
+ throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
+ }
+ tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
+ }
+ if(tu.getIndex() >= tupleType.getNumChildren()) {
+ std::stringstream ss;
+ ss << "Tuple-update expression index `" << tu.getIndex()
+ << "' is not a valid index; tuple type only has "
+ << tupleType.getNumChildren() << " fields";
+ throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
+ }
+ }
+ return tupleType;
+ }
+};/* 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>();
+ if(check) {
+ Record::iterator i = rec.begin();
+ for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+ child_it != child_it_end;
+ ++child_it, ++i) {
+ if(i == rec.end()) {
+ throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
+ }
+ if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
+ throw TypeCheckingExceptionPrivate(n, "record description types differ from record literal types");
+ }
+ }
+ if(i != rec.end()) {
+ throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
+ }
+ }
+ return nodeManager->mkRecordType(rec);
+ }
+};/* struct RecordTypeRule */
+
+struct RecordSelectTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+ Assert(n.getKind() == kind::RECORD_SELECT);
+ NodeManagerScope nms(nodeManager);
+ 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();
+ Record::const_iterator field = rec.find(rs.getField());
+ if(field == rec.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);
+ NodeManagerScope nms(nodeManager);
+ const RecordUpdate& ru = n.getOperator().getConst<RecordUpdate>();
+ TypeNode recordType = n[0].getType(check);
+ 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());
+ }
+ const Record& rec = recordType.getRecord();
+ Record::const_iterator field = rec.find(ru.getField());
+ if(field == rec.end()) {
+ std::stringstream ss;
+ ss << "Record-update field `" << ru.getField()
+ << "' is not a valid field name for the record type";
+ throw TypeCheckingExceptionPrivate(n, ss.str().c_str());
+ }
+ }
+ return recordType;
+ }
+};/* struct RecordUpdateTypeRule */
+
+struct RecordProperties {
+ inline static Node mkGroundTerm(TypeNode type) {
+ Unimplemented();
+ }
+
+ 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;
+ }
+};/* struct RecordProperties */
+
}/* CVC4::theory::datatypes namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
};/* DatatypesEnumerator */
+class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
+ TypeEnumerator** d_enumerators;
+
+ 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) throw() :
+ TypeEnumeratorBase<TupleEnumerator>(type) {
+ Assert(type.isTuple());
+ d_enumerators = new TypeEnumerator*[type.getNumChildren()];
+ for(size_t i = 0; i < type.getNumChildren(); ++i) {
+ d_enumerators[i] = new TypeEnumerator(type[i]);
+ }
+ }
+
+ ~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]);
+ } else {
+ ++*d_enumerators[i];
+ return *this;
+ }
+ }
+
+ deleteEnumerators();
+
+ return *this;
+ }
+
+ bool isFinished() throw() {
+ return d_enumerators == NULL;
+ }
+
+};/* TupleEnumerator */
+
+class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
+ TypeEnumerator** d_enumerators;
+
+ 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:
+
+ RecordEnumerator(TypeNode type) throw() :
+ TypeEnumeratorBase<RecordEnumerator>(type) {
+ Assert(type.isRecord());
+ const Record& rec = getType().getConst<Record>();
+ Debug("te") << "creating record enumerator for " << type << std::endl;
+ d_enumerators = new TypeEnumerator*[rec.getNumFields()];
+ for(size_t i = 0; i < rec.getNumFields(); ++i) {
+ Debug("te") << " - sub-enumerator for " << rec[i].second << std::endl;
+ d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
+ }
+ }
+
+ ~RecordEnumerator() throw() {
+ deleteEnumerators();
+ }
+
+ Node operator*() throw(NoMoreValuesException) {
+ if(isFinished()) {
+ 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);
+ }
+
+ 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 */
#include "theory/theory_engine.h"
#include "theory/type_enumerator.h"
#include "smt/options.h"
+#include "smt/smt_engine.h"
#include "theory/uf/theory_uf_model.h"
using namespace std;
Expr TheoryModel::getValue( Expr expr ) const{
Node n = Node::fromExpr( expr );
Node ret = getValue( n );
- return ret.toExpr();
+ return d_smt.postprocess(ret).toExpr();
}
/** get cardinality for sort */
~TypeEnumerator() { delete d_te; }
- bool isFinished() throw() { return d_te->isFinished(); }
- Node operator*() throw(NoMoreValuesException) { return **d_te; }
+ bool isFinished() throw() {
+#ifdef CVC4_ASSERTIONS
+ if(d_te->isFinished()) {
+ try {
+ **d_te;
+ Assert(false, "expected an NoMoreValuesException to be thrown");
+ } catch(NoMoreValuesException&) {
+ // ignore the exception, we're just asserting that it would be thrown
+ }
+ } else {
+ try {
+ **d_te;
+ } catch(NoMoreValuesException&) {
+ Assert(false, "didn't expect a NoMoreValuesException to be thrown");
+ }
+ }
+#endif /* CVC4_ASSERTIONS */
+ return d_te->isFinished();
+ }
+ Node operator*() throw(NoMoreValuesException) {
+#ifdef CVC4_ASSERTIONS
+ try {
+ Node n = **d_te;
+ Assert(n.isConst());
+ Assert(! isFinished());
+ return n;
+ } catch(NoMoreValuesException&) {
+ Assert(isFinished());
+ throw;
+ }
+#else /* CVC4_ASSERTIONS */
+ return **d_te;
+#endif /* CVC4_ASSERTIONS */
+ }
TypeEnumerator& operator++() throw() { ++*d_te; return *this; }
TypeEnumerator operator++(int) throw() { TypeEnumerator te = *this; ++*d_te; return te; }
array.h \
datatype.h \
datatype.cpp \
+ tuple.h \
+ record.h \
+ record.cpp \
matcher.h \
gmp_util.h \
sexpr.h \
Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ ExprManagerScope ems(d_constructor);
const Datatype& dt = Datatype::datatypeOf(d_constructor);
CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
DatatypeType dtt = dt.getDatatypeType();
void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
try {
if(s.find_first_not_of('0') == std::string::npos) {
- // string of all zeroes, CLN has a bug for these inputs
+ // String of all zeroes, CLN has a bug for these inputs up to and
+ // including CLN v1.3.2.
+ // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
d_value = read_integer(flags, "0", NULL, NULL);
} else {
d_value = read_integer(flags, s.c_str(), NULL, NULL);
--- /dev/null
+/********************* */
+/*! \file record.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a record definition
+ **
+ ** A class representing a record definition.
+ **/
+
+#include "util/record.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& os, const Record& r) {
+ os << "[# ";
+ bool first = true;
+ for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+ if(!first) {
+ os << ", ";
+ }
+ os << (*i).first << ":" << (*i).second;
+ first = false;
+ }
+ os << " #]";
+
+ return os;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file record.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a Record definition
+ **
+ ** A class representing a Record definition.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RECORD_H
+#define __CVC4__RECORD_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <utility>
+#include "util/hash.h"
+
+namespace CVC4 {
+
+class Record;
+
+// operators for record select and update
+
+class CVC4_PUBLIC RecordSelect {
+ std::string d_field;
+public:
+ RecordSelect(const std::string& field) throw() : d_field(field) { }
+ std::string getField() const throw() { return d_field; }
+ bool operator==(const RecordSelect& t) const throw() { return d_field == t.d_field; }
+ bool operator!=(const RecordSelect& t) const throw() { return d_field != t.d_field; }
+};/* class RecordSelect */
+
+class CVC4_PUBLIC RecordUpdate {
+ std::string d_field;
+public:
+ RecordUpdate(const std::string& field) throw() : d_field(field) { }
+ std::string getField() const throw() { return d_field; }
+ bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; }
+ bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; }
+};/* class RecordUpdate */
+
+struct CVC4_PUBLIC RecordSelectHashFunction {
+ inline size_t operator()(const RecordSelect& t) const {
+ return StringHashFunction()(t.getField());
+ }
+};/* struct RecordSelectHashFunction */
+
+struct CVC4_PUBLIC RecordUpdateHashFunction {
+ inline size_t operator()(const RecordUpdate& t) const {
+ return StringHashFunction()(t.getField());
+ }
+};/* struct RecordUpdateHashFunction */
+
+std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
+
+inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
+ return out << "[" << t.getField() << "]";
+}
+
+inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
+ return out << "[" << t.getField() << "]";
+}
+
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+
+namespace CVC4 {
+
+// now an actual record definition
+
+class CVC4_PUBLIC Record {
+ std::vector< std::pair<std::string, Type> > d_fields;
+
+public:
+
+ typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator;
+ typedef const_iterator iterator;
+
+ Record(const std::vector< std::pair<std::string, Type> >& fields) :
+ d_fields(fields) {
+ CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty");
+ }
+
+ const_iterator find(std::string name) const {
+ const_iterator i;
+ for(i = begin(); i != end(); ++i) {
+ if((*i).first == name) {
+ break;
+ }
+ }
+ return i;
+ }
+
+ size_t getIndex(std::string name) const {
+ const_iterator i = find(name);
+ CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str());
+ return i - begin();
+ }
+
+ size_t getNumFields() const {
+ return d_fields.size();
+ }
+
+ const_iterator begin() const {
+ return d_fields.begin();
+ }
+
+ const_iterator end() const {
+ return d_fields.end();
+ }
+
+ std::pair<std::string, Type> operator[](size_t index) const {
+ CheckArgument(index < d_fields.size(), index, "index out of bounds for record type");
+ return d_fields[index];
+ }
+
+ bool operator==(const Record& r) const {
+ return d_fields == r.d_fields;
+ }
+
+ bool operator!=(const Record& r) const {
+ return !(*this == r);
+ }
+
+};/* class Record */
+
+struct CVC4_PUBLIC RecordHashFunction {
+ inline size_t operator()(const Record& r) const {
+ size_t n = 0;
+ for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+ n = (n << 3) ^ TypeHashFunction()((*i).second);
+ }
+ return n;
+ }
+};/* struct RecordHashFunction */
+
+std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RECORD_H */
--- /dev/null
+%{
+#include "util/record.h"
+%}
+
+%include "util/record.h"
--- /dev/null
+/********************* */
+/*! \file tuple.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Tuple operators
+ **
+ ** Tuple operators.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TUPLE_H
+#define __CVC4__TUPLE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <utility>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC TupleSelect {
+ unsigned d_index;
+public:
+ TupleSelect(unsigned index) throw() : d_index(index) { }
+ unsigned getIndex() const throw() { return d_index; }
+ bool operator==(const TupleSelect& t) const throw() { return d_index == t.d_index; }
+ bool operator!=(const TupleSelect& t) const throw() { return d_index != t.d_index; }
+};/* class TupleSelect */
+
+class CVC4_PUBLIC TupleUpdate {
+ unsigned d_index;
+public:
+ TupleUpdate(unsigned index) throw() : d_index(index) { }
+ unsigned getIndex() const throw() { return d_index; }
+ bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; }
+ bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; }
+};/* class TupleUpdate */
+
+struct CVC4_PUBLIC TupleSelectHashFunction {
+ inline size_t operator()(const TupleSelect& t) const {
+ return t.getIndex();
+ }
+};/* struct TupleSelectHashFunction */
+
+struct CVC4_PUBLIC TupleUpdateHashFunction {
+ inline size_t operator()(const TupleUpdate& t) const {
+ return t.getIndex();
+ }
+};/* struct TupleUpdateHashFunction */
+
+std::ostream& operator<<(std::ostream& out, const TupleSelect& t) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) CVC4_PUBLIC;
+
+inline std::ostream& operator<<(std::ostream& out, const TupleSelect& t) {
+ return out << "[" << t.getIndex() << "]";
+}
+
+inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) {
+ return out << "[" << t.getIndex() << "]";
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TUPLE_H */
--- /dev/null
+%{
+#include "util/tuple.h"
+%}
+
+%include "util/tuple.h"
}
size_t Model::getNumCommands() const {
- return d_smt.d_modelCommands->size();
+ return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
}
const Command* Model::getCommand(size_t i) const {
- return (*d_smt.d_modelCommands)[i];
+ Assert(i < getNumCommands());
+ // index the global commands first, then the locals
+ if(i < d_smt.d_modelGlobalCommands.size()) {
+ return d_smt.d_modelGlobalCommands[i];
+ } else {
+ return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
+ }
}
}/* CVC4 namespace */
friend std::ostream& operator<<(std::ostream&, Model&);
protected:
- /** The SmtEngine we're associated to */
- const SmtEngine& d_smt;
+ /** The SmtEngine we're associated with */
+ SmtEngine& d_smt;
/** construct the base class; users cannot do this, only CVC4 internals */
Model();
size_t getNumCommands() const;
/** get command */
const Command* getCommand(size_t i) const;
+ /** get the smt engine that this model is hooked up to */
+ SmtEngine* getSmtEngine() { return &d_smt; }
public:
/** get value for expression */
wrong-sel-simp.cvc
FAILING_TESTS = \
+ bug438.cvc \
datatype-dump.cvc
EXTRA_DIST = $(TESTS)
--- /dev/null
+% EXPECT: sat
+% EXIT: 10
+DATATYPE list[T] = cons(car:T, cdr:list[T]) | nil END;
+x : list[REAL];
+ASSERT x = cons(1.0,nil::list[REAL])::list[REAL];
+CHECKSAT;
projects / cvc5.git / commitdiff