diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
commit | b122cec27ca27d0b48e786191448e0053be78ed0 (patch) | |
tree | 615981d8623e830894f02fc528b173ac7461f934 /src/expr/node_manager.h | |
parent | 3da16da97df7cd2efd4b113db3bfef8b9c138ebe (diff) |
Tuples and records merge. Resolves bug 270.
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.)
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 64 |
1 files changed, 47 insertions, 17 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ea733e771..6e08a9bc2 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -53,10 +53,16 @@ class TypeChecker; 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 */ @@ -71,8 +77,8 @@ public: 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 { @@ -82,8 +88,8 @@ 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>&); @@ -158,6 +164,11 @@ class NodeManager { 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" * NodeValue. In particular, "non-inlined" constants are permitted @@ -288,12 +299,12 @@ class NodeManager { * 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: @@ -413,7 +424,8 @@ 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 */ /** @@ -717,6 +729,14 @@ public: 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 * elements. @@ -780,6 +800,12 @@ public: throw(TypeCheckingExceptionPrivate); /** + * Given a tuple or record type, get the internal datatype used for + * it. Makes the DatatypeType if necessary. + */ + TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType); + + /** * Get the type for the given node and optionally do type checking. * * Initial type computation will be near-constant time if @@ -1067,6 +1093,10 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { 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) { @@ -1456,25 +1486,25 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, } -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; } @@ -1492,22 +1522,22 @@ inline Node* NodeManager::mkBoundVarPtr(const std::string& name, 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; } |