diff options
46 files changed, 1272 insertions, 635 deletions
@@ -19,7 +19,7 @@ <folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath=""> <toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base"> <targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/> -<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="false" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base"> +<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base"> <outputEntries> <entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/> </outputEntries> @@ -1,6 +1,6 @@ <?xml version="1.0" encoding="UTF-8"?> <projectDescription> - <name>cvc4-antlr3</name> + <name>cvc4</name> <comment></comment> <projects> </projects> @@ -32,7 +32,7 @@ </dictionary> <dictionary> <key>org.eclipse.cdt.make.core.buildArguments</key> - <value></value> + <value>-j</value> </dictionary> <dictionary> <key>org.eclipse.cdt.make.core.buildCommand</key> diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 4621d7fc5..9be4de19b 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -208,6 +208,20 @@ public: Debug("gc") << "done emptying trash for " << this << std::endl; } + void clear() throw(AssertionException) { + Debug("gc") << "cdmap " << this + << " disappearing, destroying..." << std::endl; + for(typename table_type::iterator i = d_map.begin(); + i != d_map.end(); + ++i) { + (*i).second->deleteSelf(); + } + d_map.clear(); + emptyTrash(); + Debug("gc") << "done emptying trash for " << this << std::endl; + } + + // The usual operators of map size_t size() const { diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index a9480723f..0abeebb9e 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -26,7 +26,8 @@ libexpr_la_SOURCES = \ command.h \ command.cpp \ declaration_scope.h \ - declaration_scope.cpp + declaration_scope.cpp \ + expr_manager_scope.h EXTRA_DIST = \ @srcdir@/kind.h \ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 1eeec68af..e5a50591f 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -28,7 +28,8 @@ namespace attr { void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_bools.erase(nv); deleteFromTable(d_ints, nv); - deleteFromTable(d_exprs, nv); + deleteFromTable(d_tnodes, nv); + deleteFromTable(d_nodes, nv); deleteFromTable(d_strings, nv); deleteFromTable(d_ptrs, nv); @@ -40,7 +41,10 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_cdints.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) { - d_cdexprs.obliterate(std::make_pair(id, nv)); + d_cdtnodes.obliterate(std::make_pair(id, nv)); + } + for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) { + d_cdnodes.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) { d_cdstrings.obliterate(std::make_pair(id, nv)); @@ -50,6 +54,24 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { } } +void AttributeManager::deleteAllAttributes() { + d_bools.clear(); + deleteAllFromTable(d_ints); + deleteAllFromTable(d_tnodes); + deleteAllFromTable(d_nodes); + deleteAllFromTable(d_strings); + deleteAllFromTable(d_ptrs); + + // FIXME CD-bools in optimized table + d_cdbools.clear(); + d_cdints.clear(); + d_cdtnodes.clear(); + d_cdnodes.clear(); + d_cdstrings.clear(); + d_cdptrs.clear(); +} + + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 27cddf299..4250bb3ef 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -29,7 +29,6 @@ #include "context/cdmap.h" #include "expr/node.h" -#include "expr/type.h" #include "util/output.h" // include supporting templates @@ -57,7 +56,9 @@ class AttributeManager { /** Underlying hash table for integral-valued attributes */ AttrHash<uint64_t> d_ints; /** Underlying hash table for node-valued attributes */ - AttrHash<TNode> d_exprs; + AttrHash<TNode> d_tnodes; + /** Underlying hash table for node-valued attributes */ + AttrHash<Node> d_nodes; /** Underlying hash table for string-valued attributes */ AttrHash<std::string> d_strings; /** Underlying hash table for pointer-valued attributes */ @@ -71,7 +72,9 @@ class AttributeManager { /** Underlying hash table for context-dependent integral-valued attributes */ CDAttrHash<uint64_t> d_cdints; /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<TNode> d_cdexprs; + CDAttrHash<TNode> d_cdtnodes; + /** Underlying hash table for context-dependent node-valued attributes */ + CDAttrHash<Node> d_cdnodes; /** Underlying hash table for context-dependent string-valued attributes */ CDAttrHash<std::string> d_cdstrings; /** Underlying hash table for context-dependent pointer-valued attributes */ @@ -80,6 +83,9 @@ class AttributeManager { template <class T> void deleteFromTable(AttrHash<T>& table, NodeValue* nv); + template <class T> + void deleteAllFromTable(AttrHash<T>& table); + /** * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. @@ -93,7 +99,8 @@ public: AttributeManager(context::Context* ctxt) : d_cdbools(ctxt), d_cdints(ctxt), - d_cdexprs(ctxt), + d_cdtnodes(ctxt), + d_cdnodes(ctxt), d_cdstrings(ctxt), d_cdptrs(ctxt) { } @@ -166,6 +173,11 @@ public: * @param nv the node from which to delete attributes */ void deleteAllAttributes(NodeValue* nv); + + /** + * Remove all attributes from the tables. + */ + void deleteAllAttributes(); }; }/* CVC4::expr::attr namespace */ @@ -205,15 +217,27 @@ struct getTable<uint64_t, false> { } }; -/** Access the "d_exprs" member of AttributeManager. */ +/** Access the "d_tnodes" member of AttributeManager. */ template <> struct getTable<TNode, false> { typedef AttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { - return am.d_exprs; + return am.d_tnodes; } static inline const table_type& get(const AttributeManager& am) { - return am.d_exprs; + return am.d_tnodes; + } +}; + +/** Access the "d_nodes" member of AttributeManager. */ +template <> +struct getTable<Node, false> { + typedef AttrHash<Node> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_nodes; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_nodes; } }; @@ -277,15 +301,27 @@ struct getTable<uint64_t, true> { } }; -/** Access the "d_cdexprs" member of AttributeManager. */ +/** Access the "d_tnodes" member of AttributeManager. */ template <> struct getTable<TNode, true> { typedef CDAttrHash<TNode> table_type; static inline table_type& get(AttributeManager& am) { - return am.d_cdexprs; + return am.d_cdtnodes; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdtnodes; + } +}; + +/** Access the "d_nodes" member of AttributeManager. */ +template <> +struct getTable<Node, true> { + typedef CDAttrHash<Node> table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdnodes; } static inline const table_type& get(const AttributeManager& am) { - return am.d_cdexprs; + return am.d_cdnodes; } }; @@ -499,6 +535,27 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table, } } +/** + * Remove all attributes from the table calling the cleanup function if one is defined. + */ +template <class T> +inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { + for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) { + typedef AttributeTraits<T, false> traits_t; + typedef AttrHash<T> hash_t; + if(traits_t::cleanup[id] != NULL) { + typename hash_t::iterator it = table.begin(); + typename hash_t::iterator it_end = table.end(); + while (it != it_end) { + traits_t::cleanup[id]((*it).second); + ++ it; + } + } + table.clear(); + } +} + + }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 0ae2cdc22..4ac89afec 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -341,6 +341,13 @@ public: super::erase(nv); } + /** + * Clear the hash table. + */ + void clear() { + super::clear(); + } + };/* class AttrHash<bool> */ /** diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index c4eb3af1c..eb41c788e 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -120,3 +120,11 @@ operator DISTINCT 2: "disequality" variable SKOLEM "skolem var" variable VARIABLE "variable" operator TUPLE 2: "a tuple" + +constant TYPE_CONSTANT \ + ::CVC4::TypeConstant \ + ::CVC4::TypeConstantHashStrategy \ + "expr/type_constant.h" \ + "basic types" +operator FUNCTION_TYPE 2: "function type" +variable SORT_TYPE "sort type" diff --git a/src/expr/command.h b/src/expr/command.h index 6a4bb67ed..bb295a662 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -27,6 +27,7 @@ #include <vector> #include "expr/expr.h" +#include "expr/type.h" #include "util/result.h" namespace CVC4 { @@ -92,10 +93,11 @@ public: class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { public: - DeclarationCommand(const std::vector<std::string>& ids, const Type* t); + DeclarationCommand(const std::vector<std::string>& ids, const Type& t); void toStream(std::ostream& out) const; protected: std::vector<std::string> d_declaredSymbols; + Type d_type; }; class CVC4_PUBLIC CheckSatCommand : public Command { @@ -257,8 +259,10 @@ inline void CommandSequence::addCommand(Command* cmd) { /* class DeclarationCommand */ -inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type* t) : - d_declaredSymbols(ids) { +inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type& t) : + d_declaredSymbols(ids), + d_type(t) +{ } /* class SetBenchmarkStatusCommand */ diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index c326817ad..6dc9453d2 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -27,11 +27,12 @@ using namespace context; DeclarationScope::DeclarationScope() : d_context(new Context()), d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)), - d_typeMap(new (true) CDMap<std::string,Type*,StringHashFunction>(d_context)) { + d_typeMap(new (true) CDMap<std::string,Type,StringHashFunction>(d_context)) { } DeclarationScope::~DeclarationScope() { d_exprMap->deleteSelf(); + d_typeMap->deleteSelf(); delete d_context; } @@ -47,7 +48,7 @@ Expr DeclarationScope::lookup(const std::string& name) const throw () { return (*d_exprMap->find(name)).second; } -void DeclarationScope::bindType(const std::string& name, Type* t) throw () { +void DeclarationScope::bindType(const std::string& name, const Type& t) throw () { d_typeMap->insert(name,t); } @@ -55,7 +56,7 @@ bool DeclarationScope::isBoundType(const std::string& name) const throw () { return d_typeMap->find(name) != d_typeMap->end(); } -Type* DeclarationScope::lookupType(const std::string& name) const throw () { +Type DeclarationScope::lookupType(const std::string& name) const throw () { return (*d_typeMap->find(name)).second; } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index e08c25173..7d0f2b787 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -56,7 +56,7 @@ class CVC4_PUBLIC DeclarationScope { context::CDMap<std::string,Expr,StringHashFunction> *d_exprMap; /** A map for types. */ - context::CDMap<std::string,Type*,StringHashFunction> *d_typeMap; + context::CDMap<std::string,Type,StringHashFunction> *d_typeMap; public: /** Create a declaration scope. */ @@ -85,7 +85,7 @@ public: * @param name an identifier * @param t the type to bind to <code>name</code> */ - void bindType(const std::string& name, Type* t) throw (); + void bindType(const std::string& name, const Type& t) throw (); /** Check whether a name is bound to an expression. * @@ -113,7 +113,7 @@ public: * @param name the identifier to lookup * @returns the type bound to <code>name</code> in the current scope. */ - Type* lookupType(const std::string& name) const throw (); + Type lookupType(const std::string& name) const throw (); /** Pop a scope level. Deletes all bindings since the last call to * <code>pushScope</code>. Calls to <code>pushScope</code> and diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h new file mode 100644 index 000000000..38f8fc787 --- /dev/null +++ b/src/expr/expr_manager_scope.h @@ -0,0 +1,52 @@ +/* + * expr_manager_scope.h + * + * Created on: Apr 7, 2010 + * Author: dejan + */ + +#ifndef __CVC4__EXPR_MANAGER_SCOPE_H +#define __CVC4__EXPR_MANAGER_SCOPE_H + +#include "expr/expr.h" +#include "expr/node_manager.h" + +namespace CVC4 { + +/** + * Creates a <code>NodeManagerScope</code> with the underlying + * <code>NodeManager</code> of a given <code>Expr</code> or + * <code>ExprManager</code>. The <code>NodeManagerScope</code> is + * destroyed when the <code>ExprManagerScope</code> is destroyed. See + * <code>NodeManagerScope</code> for more information. + */ +// NOTE: Here, it seems ExprManagerScope is redundant, since we have +// NodeManagerScope already. However, without this class, we'd need +// Expr to be a friend of ExprManager, because in the implementation +// of Expr functions, it needs to set the current NodeManager +// correctly (and to do that it needs access to +// ExprManager::getNodeManager()). So, we make ExprManagerScope a +// friend of ExprManager's, since its implementation is simple to +// read and understand (and verify that it doesn't do any mischief). +// +// ExprManager::getNodeManager() can't just be made public, since +// ExprManager is exposed to clients of the library and NodeManager is +// not. Similarly, ExprManagerScope shouldn't go in expr_manager.h, +// since that's a public header. +class ExprManagerScope { + NodeManagerScope d_nms; +public: + inline ExprManagerScope(const Expr& e) : + d_nms(e.getExprManager() == NULL + ? NodeManager::currentNM() + : e.getExprManager()->getNodeManager()) { + } + inline ExprManagerScope(const ExprManager& exprManager) : + d_nms(exprManager.getNodeManager()) { + } +}; + +} + + +#endif /* __CVC4__EXPR_MANAGER_SCOPE_H */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index a8d957c91..7407043d2 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -46,12 +46,12 @@ ExprManager::~ExprManager() { delete d_ctxt; } -BooleanType* ExprManager::booleanType() const { +BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); return d_nodeManager->booleanType(); } -KindType* ExprManager::kindType() const { +KindType ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); return d_nodeManager->kindType(); } @@ -64,7 +64,7 @@ Expr ExprManager::mkExpr(Kind kind) { kind::kindToString(kind).c_str(), minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkNode(kind))); + return Expr(this, d_nodeManager->mkNodePtr(kind)); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { @@ -75,7 +75,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { kind::kindToString(kind).c_str(), minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode()))); + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode())); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { @@ -86,8 +86,8 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { kind::kindToString(kind).c_str(), minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(), - child2.getNode()))); + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), + child2.getNode())); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, @@ -99,8 +99,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, kind::kindToString(kind).c_str(), minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(), - child2.getNode(), child3.getNode()))); + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode(), child3.getNode())); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, @@ -112,9 +111,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, kind::kindToString(kind).c_str(), minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(), + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode(), child3.getNode(), - child4.getNode()))); + child4.getNode())); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, @@ -127,9 +126,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, kind::kindToString(kind).c_str(), minArity(kind), maxArity(kind), n); NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(), + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode(), child3.getNode(), - child5.getNode()))); + child5.getNode())); } Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { @@ -149,49 +148,52 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) { nodes.push_back(it->getNode()); ++it; } - return Expr(this, new Node(d_nodeManager->mkNode(kind, nodes))); + return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); } /** Make a function type from domain to range. */ -FunctionType* ExprManager::mkFunctionType(Type* domain, - Type* range) { +FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) { NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkFunctionType(domain, range); } /** Make a function type with input types from argTypes. */ -FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes, - Type* range) { +FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) { Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkFunctionType(argTypes, range); } -FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& sorts) { +FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { Assert( sorts.size() >= 2 ); NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkFunctionType(sorts); } -FunctionType* ExprManager::mkPredicateType(const std::vector<Type*>& sorts) { +FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { Assert( sorts.size() >= 1 ); NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkPredicateType(sorts); } -Type* ExprManager::mkSort(const std::string& name) { +SortType ExprManager::mkSort(const std::string& name) { NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkSort(name); } -Expr ExprManager::mkVar(const std::string& name, Type* type) { +Type ExprManager::getType(const Expr& e) { NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkVar(name, type))); + return d_nodeManager->getType(e.getNode()); } -Expr ExprManager::mkVar(Type* type) { +Expr ExprManager::mkVar(const std::string& name, const Type& type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkVar(type))); + return Expr(this, d_nodeManager->mkVarPtr(name, type)); +} + +Expr ExprManager::mkVar(const Type& type) { + NodeManagerScope nms(d_nodeManager); + return Expr(this, d_nodeManager->mkVarPtr(type)); } unsigned ExprManager::minArity(Kind kind) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 82698732c..df5190af6 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -85,10 +85,10 @@ public: ~ExprManager(); /** Get the type for booleans */ - BooleanType* booleanType() const; + BooleanType booleanType() const; /** Get the type for sorts. */ - KindType* kindType() const; + KindType kindType() const; /** * Make a unary expression of a given kind (TRUE, FALSE,...). @@ -162,15 +162,13 @@ public: Expr mkConst(const T&); /** Make a function type from domain to range. */ - FunctionType* mkFunctionType(Type* domain, - Type* range); + FunctionType mkFunctionType(const Type& domain, const Type& range); /** * Make a function type with input types from argTypes. * <code>argTypes</code> must have at least one element. */ - FunctionType* mkFunctionType(const std::vector<Type*>& argTypes, - Type* range); + FunctionType mkFunctionType(const std::vector<Type>& argTypes, const Type& range); /** * Make a function type with input types from @@ -178,7 +176,7 @@ public: * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have * at least 2 elements. */ - FunctionType* mkFunctionType(const std::vector<Type*>& sorts); + FunctionType mkFunctionType(const std::vector<Type>& sorts); /** * Make a predicate type with input types from @@ -186,14 +184,17 @@ public: * <code>BOOLEAN</code>. <code>sorts</code> must have at least one * element. */ - FunctionType* mkPredicateType(const std::vector<Type*>& sorts); + FunctionType mkPredicateType(const std::vector<Type>& sorts); /** Make a new sort with the given name. */ - Type* mkSort(const std::string& name); + SortType mkSort(const std::string& name); + + /** Get the type of an expression */ + Type getType(const Expr& e); // 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, const Type& type); + Expr mkVar(const Type& type); /** Returns the minimum arity of the given kind. */ static unsigned minArity(Kind kind); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 7c723d338..ba7032e34 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -18,6 +18,7 @@ #include "util/Assert.h" #include "util/output.h" +#include "expr/expr_manager_scope.h" ${includes} @@ -25,7 +26,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 29 "${template}" +#line 30 "${template}" using namespace CVC4::kind; @@ -128,10 +129,10 @@ Expr Expr::getOperator() const { return Expr(d_exprManager, new Node(d_node->getOperator())); } -Type* Expr::getType() const { +Type Expr::getType() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - return d_node->getType(); + return d_exprManager->getType(*this); } std::string Expr::toString() const { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 2fa10ceb8..0e960358f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -144,7 +144,7 @@ public: /** Returns the type of the expression, if it has been computed. * Returns NULL if the type of the expression is not known. */ - Type* getType() const; + Type getType() const; /** * Returns the string representation of the expression. diff --git a/src/expr/node.h b/src/expr/node.h index 3a2aca571..27756da5b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -28,7 +28,6 @@ #include "expr/kind.h" #include "expr/metakind.h" -#include "expr/type.h" #include "util/Assert.h" #include "util/output.h" @@ -248,7 +247,7 @@ public: * Returns the type of this node. * @return the type */ - Type* getType() const; + Type getType() const; /** * Returns the kind of this node. @@ -640,7 +639,7 @@ NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) { if(ref_count) { d_nv->dec(); } else { - Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted(), + Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted() || NodeManager::currentNM()->inDestruction(), "TNode pointing to an expired NodeValue at destruction time"); } } @@ -815,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { } template <bool ref_count> -Type* NodeTemplate<ref_count>::getType() const { +Type NodeTemplate<ref_count>::getType() const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index c854b6b80..a093fc954 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -537,7 +537,26 @@ public: return static_cast<Builder&>(*this); } +private: + + /** Construct the node value out of the node builder */ + expr::NodeValue* constructNV(); + expr::NodeValue* constructNV() const; + +public: + + /** Construct the Node out of the node builder */ + Node constructNode(); + Node constructNode() const; + + /** Construct a Node on the heap out of the node builder */ + Node* constructNodePtr(); + Node* constructNodePtr() const; + + // two versions, so we can support extraction from (const) + // NodeBuilders which are temporaries appearing as rvalues operator Node(); + operator Node() const; inline void toStream(std::ostream& out, int depth = -1) const { Assert(!isUsed(), "NodeBuilder is one-shot only; " @@ -1227,7 +1246,17 @@ void NodeBuilderBase<Builder>::decrRefCounts() { } template <class Builder> -NodeBuilderBase<Builder>::operator Node() { +Node* NodeBuilderBase<Builder>::constructNodePtr() { + return new Node(constructNV()); +} + +template <class Builder> +Node* NodeBuilderBase<Builder>::constructNodePtr() const { + return new Node(constructNV()); +} + +template <class Builder> +expr::NodeValue* NodeBuilderBase<Builder>::constructNV() { Assert(!isUsed(), "NodeBuilder is one-shot only; " "attempt to access it after conversion"); Assert(getKind() != kind::UNDEFINED_KIND, @@ -1265,7 +1294,7 @@ NodeBuilderBase<Builder>::operator Node() { setUsed(); Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: " << nv->toString() << "\n"; - return Node(nv); + return nv; } // check that there are the right # of children for this kind @@ -1309,7 +1338,7 @@ NodeBuilderBase<Builder>::operator Node() { decrRefCounts(); d_inlineNv.d_nchildren = 0; setUsed(); - return Node(poolNv); + return poolNv; } else { /* Subcase (b): The Node under construction is NOT already in * the NodeManager's pool. */ @@ -1347,7 +1376,7 @@ NodeBuilderBase<Builder>::operator Node() { d_nm->poolInsert(nv); Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: " << *nv << "\n"; - return Node(nv); + return nv; } } else { /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger @@ -1369,7 +1398,7 @@ NodeBuilderBase<Builder>::operator Node() { dealloc(); setUsed(); - return Node(poolNv); + return poolNv; } else { /* Subcase (b) The Node under construction is NOT already in the * NodeManager's pool. */ @@ -1392,11 +1421,198 @@ NodeBuilderBase<Builder>::operator Node() { d_nm->poolInsert(nv); Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: " << *nv << "\n"; - return Node(nv); + return nv; } } } +// CONST VERSION OF NODE EXTRACTOR +template <class Builder> +expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); + Assert(getKind() != kind::UNDEFINED_KIND, + "Can't make an expression of an undefined kind!"); + + // NOTE: The comments in this function refer to the cases in the + // file comments at the top of this file. + + // Case 0: If a VARIABLE + if(getMetaKind() == kind::metakind::VARIABLE) { + /* 0. If a VARIABLE, treat similarly to 1(b), except that we know + * there are no children (no reference counts to reason about), + * and we don't keep VARIABLE-kinded Nodes in the NodeManager + * pool. */ + + Assert( ! nvIsAllocated(), + "internal NodeBuilder error: " + "VARIABLE-kinded NodeBuilder is heap-allocated !?" ); + Assert( d_inlineNv.d_nchildren == 0, + "improperly-formed VARIABLE-kinded NodeBuilder: " + "no children permitted" ); + + // we have to copy the inline NodeValue out + expr::NodeValue* nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue)); + if(nv == NULL) { + throw std::bad_alloc(); + } + // there are no children, so we don't have to worry about + // reference counts in this case. + nv->d_nchildren = 0; + nv->d_kind = d_nv->d_kind; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << *nv << "\n"; + return nv; + } + + // check that there are the right # of children for this kind + Assert(getMetaKind() != kind::metakind::CONSTANT, + "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"); + Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()), + "Nodes with kind %s must have at least %u children (the one under " + "construction has %u)", + kind::kindToString(getKind()).c_str(), + kind::metakind::getLowerBoundForKind(getKind()), + getNumChildren()); + Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()), + "Nodes with kind %s must have at most %u children (the one under " + "construction has %u)", + kind::kindToString(getKind()).c_str(), + kind::metakind::getUpperBoundForKind(getKind()), + getNumChildren()); + + // Implementation differs depending on whether the NodeValue was + // malloc'ed or not and whether or not it's in the already-been-seen + // NodeManager pool of Nodes. See implementation notes at the top + // of this file. + + if(EXPECT_TRUE( ! nvIsAllocated() )) { + /** Case 1. d_nv points to d_inlineNv: it is the backing store + ** supplied by the user (or derived class) **/ + + // Lookup the expression value in the pool we already have + expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); + // If something else is there, we reuse it + if(poolNv != NULL) { + /* Subcase (a): The Node under construction already exists in + * the NodeManager's pool. */ + + /* 1(a). The existing NodeManager pool entry is returned; we + * leave child reference counts alone and get them at + * NodeBuilder destruction time. */ + + return poolNv; + } else { + /* Subcase (b): The Node under construction is NOT already in + * the NodeManager's pool. */ + + /* 1(b). A new heap-allocated NodeValue must be constructed and + * all settings and children from d_inlineNv copied into it. + * This new NodeValue is put into the NodeManager's pool. The + * NodeBuilder cannot be marked as "used", so we increment all + * child reference counts (which will be decremented to match on + * destruction of the NodeBuilder). We return a Node wrapper + * for this new NodeValue, which increments its reference + * count. */ + + // create the canonical expression value for this node + expr::NodeValue* nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } + nv->d_nchildren = d_inlineNv.d_nchildren; + nv->d_kind = d_inlineNv.d_kind; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + nv->d_children); + + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + (*i)->inc(); + } + + //poolNv = nv; + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << *nv << "\n"; + return nv; + } + } else { + /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger + ** buffer that was heap-allocated by this NodeBuilder. **/ + + // Lookup the expression value in the pool we already have (with insert) + expr::NodeValue* poolNv = d_nm->poolLookup(d_nv); + // If something else is there, we reuse it + if(poolNv != NULL) { + /* Subcase (a): The Node under construction already exists in + * the NodeManager's pool. */ + + /* 2(a). The existing NodeManager pool entry is returned; we + * leave child reference counts alone and get them at + * NodeBuilder destruction time. */ + + return poolNv; + } else { + /* Subcase (b) The Node under construction is NOT already in the + * NodeManager's pool. */ + + /* 2(b). The heap-allocated d_nv cannot be "cropped" to the + * correct size; we create a copy, increment child reference + * counts, place this copy into the NodeManager pool, and return + * a Node wrapper around it. The child reference counts will be + * decremented to match at NodeBuilder destruction time. */ + + // create the canonical expression value for this node + expr::NodeValue* nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + + ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } + nv->d_nchildren = d_nv->d_nchildren; + nv->d_kind = d_nv->d_kind; + nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading + nv->d_rc = 0; + + std::copy(d_nv->d_children, + d_nv->d_children + d_nv->d_nchildren, + nv->d_children); + + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + (*i)->inc(); + } + + //poolNv = nv; + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: " << *nv << "\n"; + return nv; + } + } +} + +template <class Builder> +NodeBuilderBase<Builder>::operator Node() { + return Node(constructNV()); +} + +template <class Builder> +NodeBuilderBase<Builder>::operator Node() const { + return Node(constructNV()); +} + template <unsigned nchild_thresh> template <unsigned N> void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 708bd16b2..4f0e0ff76 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -27,55 +27,23 @@ namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; -NodeManager::NodeManager(context::Context* ctxt) : - d_attrManager(ctxt), - d_nodeUnderDeletion(NULL), - d_reclaiming(false) { - poolInsert( &expr::NodeValue::s_null ); - - for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { - Kind k = Kind(i); - - if(hasOperator(k)) { - d_operators[i] = mkConst(Kind(k)); - } - } -} - -NodeManager::~NodeManager() { - // have to ensure "this" is the current NodeManager during - // destruction of operators, because they get GCed. - - NodeManagerScope nms(this); - - for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { - d_operators[i] = Node::null(); - } - - while(!d_zombies.empty()) { - reclaimZombies(); - } - - poolRemove( &expr::NodeValue::s_null ); -} - /** * This class ensures that NodeManager::d_reclaiming gets set to false * even on exceptional exit from NodeManager::reclaimZombies(). */ -struct Reclaim { - bool& d_reclaimField; +struct ScopedBool { + bool& d_value; - Reclaim(bool& reclaim) : - d_reclaimField(reclaim) { + ScopedBool(bool& reclaim) : + d_value(reclaim) { Debug("gc") << ">> setting RECLAIM field\n"; - d_reclaimField = true; + d_value = true; } - ~Reclaim() { + ~ScopedBool() { Debug("gc") << "<< clearing RECLAIM field\n"; - d_reclaimField = false; + d_value = false; } }; @@ -98,17 +66,57 @@ struct NVReclaim { } }; + +NodeManager::NodeManager(context::Context* ctxt) : + d_attrManager(ctxt), + d_nodeUnderDeletion(NULL), + d_dontGC(false), + d_inDestruction(false) { + poolInsert( &expr::NodeValue::s_null ); + + for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { + Kind k = Kind(i); + + if(hasOperator(k)) { + d_operators[i] = mkConst(Kind(k)); + } + } +} + +NodeManager::~NodeManager() { + // have to ensure "this" is the current NodeManager during + // destruction of operators, because they get GCed. + + NodeManagerScope nms(this); + ScopedBool inDestruction(d_inDestruction); + + { + ScopedBool dontGC(d_dontGC); + d_attrManager.deleteAllAttributes(); + } + + for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { + d_operators[i] = Node::null(); + } + + while(!d_zombies.empty()) { + reclaimZombies(); + } + + poolRemove( &expr::NodeValue::s_null ); +} + void NodeManager::reclaimZombies() { // FIXME multithreading Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; // during reclamation, reclaimZombies() is never supposed to be called - Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!"); + Assert(! d_dontGC, "NodeManager::reclaimZombies() not re-entrant!"); // whether exit is normal or exceptional, the Reclaim dtor is called // and ensures that d_reclaiming is set back to false. - Reclaim r(d_reclaiming); + ScopedBool r(d_dontGC); // We copy the set away and clear the NodeManager's set of zombies. // This is because reclaimZombie() decrements the RC of the diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c3f5238d6..3a6b6e15a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,7 +30,6 @@ #include "expr/kind.h" #include "expr/metakind.h" -#include "expr/expr.h" #include "expr/node_value.h" #include "context/context.h" #include "expr/type.h" @@ -86,7 +85,12 @@ class NodeManager { * NodeValues, but these shouldn't trigger a (recursive) call to * reclaimZombies(). */ - bool d_reclaiming; + bool d_dontGC; + + /** + * Marks that we are in the Destructor currently. + */ + bool d_inDestruction; /** * The set of zombie nodes. We may want to revisit this design, as @@ -164,11 +168,11 @@ class NodeManager { // reclaimZombies(), because it's already running. Debug("gc") << "zombifying node value " << nv << " [" << nv->d_id << "]: " << *nv - << (d_reclaiming ? " [CURRENTLY-RECLAIMING]" : "") + << (d_dontGC ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; d_zombies.insert(nv);// FIXME multithreading - if(!d_reclaiming) {// FIXME multithreading + if(!d_dontGC) {// FIXME multithreading // for now, collect eagerly. can add heuristic here later.. reclaimZombies(); } @@ -202,9 +206,7 @@ class NodeManager { // NodeManager's attributes. These aren't exposed outside of this // class; use the getters. - typedef expr::ManagedAttribute<TypeTag, - CVC4::Type*, - expr::attr::TypeCleanupStrategy> TypeAttr; + typedef expr::Attribute<TypeTag, Node> TypeAttr; typedef expr::Attribute<AtomicTag, bool> AtomicAttr; /** @@ -239,6 +241,11 @@ public: NodeManager(context::Context* ctxt); ~NodeManager(); + /** + * Return true if we are in destruction. + */ + bool inDestruction() const { return d_inDestruction; } + /** The node manager in the current context. */ static NodeManager* currentNM() { return s_current; } @@ -246,37 +253,49 @@ public: /** Create a node with no children. */ Node mkNode(Kind kind); + Node* mkNodePtr(Kind kind); /** Create a node with one child. */ Node mkNode(Kind kind, TNode child1); + Node* mkNodePtr(Kind kind, TNode child1); /** Create a node with two children. */ Node mkNode(Kind kind, TNode child1, TNode child2); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2); /** Create a node with three children. */ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3); /** Create a node with four children. */ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4); /** Create a node with five children. */ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); /** Create a node with an arbitrary number of children. */ template <bool ref_count> Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children); + template <bool ref_count> + Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children); /** * Create a variable with the given name and type. NOTE that no * lookup is done on the name. If you mkVar("a", type) and then * mkVar("a", type) again, you have two variables. */ - Node mkVar(const std::string& name, Type* type); + Node mkVar(const std::string& name, const Type& type); + Node* mkVarPtr(const std::string& name, const Type& type); /** Create a variable with the given type. */ - Node mkVar(Type* type); + Node mkVar(const Type& type); + Node* mkVarPtr(const Type& type); /** * Create a constant of type T. It will have the appropriate @@ -414,14 +433,10 @@ public: const typename AttrKind::value_type& value); /** Get the (singleton) type for booleans. */ - inline BooleanType* booleanType() const { - return BooleanType::getInstance(); - } + inline BooleanType booleanType(); /** Get the (singleton) type for sorts. */ - inline KindType* kindType() const { - return KindType::getInstance(); - } + inline KindType kindType(); /** * Make a function type from domain to range. @@ -430,7 +445,7 @@ public: * @param range the range type * @returns the functional type domain -> range */ - inline FunctionType* mkFunctionType(Type* domain, Type* range) const; + inline Type mkFunctionType(const Type& domain, const Type& range); /** * Make a function type with input types from @@ -440,8 +455,7 @@ public: * @param range the range type * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ - inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes, - Type* range) const; + inline Type mkFunctionType(const std::vector<Type>& argTypes, const Type& range); /** * Make a function type with input types from @@ -449,7 +463,7 @@ public: * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have * at least 2 elements. */ - inline FunctionType* mkFunctionType(const std::vector<Type*>& sorts) const; + inline Type mkFunctionType(const std::vector<Type>& sorts); /** * Make a predicate type with input types from @@ -457,16 +471,15 @@ public: * <code>BOOLEAN</code>. <code>sorts</code> must have at least one * element. */ - inline FunctionType* mkPredicateType(const std::vector<Type*>& sorts) const; + inline Type mkPredicateType(const std::vector<Type>& sorts); /** Make a new sort with the given name. */ - inline Type* mkSort(const std::string& name) const; + inline Type mkSort(const std::string& name); - /** Get the type for the given node. - * - * TODO: Does this call compute the type if it's not already available? + /** + * Get the type for the given node. */ - inline Type* getType(TNode n) const; + inline Type getType(TNode n); /** * Returns true if this node is atomic (has no more Boolean structure) @@ -518,38 +531,6 @@ public: } }; -/** - * Creates a <code>NodeManagerScope</code> with the underlying - * <code>NodeManager</code> of a given <code>Expr</code> or - * <code>ExprManager</code>. The <code>NodeManagerScope</code> is - * destroyed when the <code>ExprManagerScope</code> is destroyed. See - * <code>NodeManagerScope</code> for more information. - */ -// NOTE: Here, it seems ExprManagerScope is redundant, since we have -// NodeManagerScope already. However, without this class, we'd need -// Expr to be a friend of ExprManager, because in the implementation -// of Expr functions, it needs to set the current NodeManager -// correctly (and to do that it needs access to -// ExprManager::getNodeManager()). So, we make ExprManagerScope a -// friend of ExprManager's, since its implementation is simple to -// read and understand (and verify that it doesn't do any mischief). -// -// ExprManager::getNodeManager() can't just be made public, since -// ExprManager is exposed to clients of the library and NodeManager is -// not. Similarly, ExprManagerScope shouldn't go in expr_manager.h, -// since that's a public header. -class ExprManagerScope { - NodeManagerScope d_nms; -public: - inline ExprManagerScope(const Expr& e) : - d_nms(e.getExprManager() == NULL - ? NodeManager::currentNM() - : e.getExprManager()->getNodeManager()) { - } - inline ExprManagerScope(const ExprManager& exprManager) : - d_nms(exprManager.getNodeManager()) { - } -}; template <class AttrKind> inline typename AttrKind::value_type @@ -603,45 +584,61 @@ NodeManager::setAttribute(TNode n, const AttrKind&, d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } + +/** Get the (singleton) type for booleans. */ +inline BooleanType NodeManager::booleanType() { + return Type(this, new Node(mkConst<TypeConstant>(BOOLEAN_TYPE))); +} + +/** Get the (singleton) type for sorts. */ +inline KindType NodeManager::kindType() { + return Type(this, new Node(mkConst<TypeConstant>(KIND_TYPE))); +} + /** Make a function type from domain to range. * TODO: Function types should be unique for this manager. */ -inline FunctionType* NodeManager::mkFunctionType(Type* domain, - Type* range) const { - std::vector<Type*> argTypes; - argTypes.push_back(domain); - return new FunctionType(argTypes, range); +inline Type NodeManager::mkFunctionType(const Type& domain, const Type& range) { + return Type(this, mkNodePtr(kind::FUNCTION_TYPE, *domain.d_typeNode, *range.d_typeNode)); } -/** Make a function type with input types from argTypes. - * TODO: Function types should be unique for this manager. */ -inline FunctionType* -NodeManager::mkFunctionType(const std::vector<Type*>& argTypes, - Type* range) const { - Assert( argTypes.size() > 0 ); - return new FunctionType(argTypes, range); +inline Type NodeManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) { + Assert(argTypes.size() >= 1); + std::vector<Type> sorts(argTypes); + sorts.push_back(range); + return mkFunctionType(sorts); } -inline FunctionType* -NodeManager::mkFunctionType(const std::vector<Type*>& sorts) const { - Assert( sorts.size() >= 2 ); - std::vector<Type*> argTypes(sorts); - Type* rangeType = argTypes.back(); - argTypes.pop_back(); - return mkFunctionType(argTypes,rangeType); + +inline Type +NodeManager::mkFunctionType(const std::vector<Type>& sorts) { + Assert(sorts.size() >= 2); + std::vector<Node> sortNodes; + for (unsigned i = 0; i < sorts.size(); ++ i) { + sortNodes.push_back(*(sorts[i].d_typeNode)); + } + return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes)); } -inline FunctionType* -NodeManager::mkPredicateType(const std::vector<Type*>& sorts) const { - Assert( sorts.size() >= 1 ); - return mkFunctionType(sorts,booleanType()); +inline Type +NodeManager::mkPredicateType(const std::vector<Type>& sorts) { + Assert(sorts.size() >= 1); + std::vector<Node> sortNodes; + for (unsigned i = 0; i < sorts.size(); ++ i) { + sortNodes.push_back(*(sorts[i].d_typeNode)); + } + sortNodes.push_back(*(booleanType().d_typeNode)); + return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes)); } -inline Type* NodeManager::mkSort(const std::string& name) const { - return new SortType(name); +inline Type NodeManager::mkSort(const std::string& name) { + return Type(this, mkVarPtr(name, kindType())); } -inline Type* NodeManager::getType(TNode n) const { - return getAttribute(n, TypeAttr()); +inline Type NodeManager::getType(TNode n) { + Node* typeNode = new Node; + getAttribute(n, TypeAttr(), *typeNode); + // TODO: Type computation + return Type(this, typeNode); } inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { @@ -731,33 +728,71 @@ inline bool NodeManager::hasOperator(Kind k) { } inline Node NodeManager::mkNode(Kind kind) { - return NodeBuilder<>(this, kind); + return NodeBuilder<0>(this, kind); +} + +inline Node* NodeManager::mkNodePtr(Kind kind) { + NodeBuilder<0> nb(this, kind); + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1) { - return NodeBuilder<>(this, kind) << child1; + return NodeBuilder<1>(this, kind) << child1; +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) { + NodeBuilder<1> nb(this, kind); + nb << child1; + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { - return NodeBuilder<>(this, kind) << child1 << child2; + return NodeBuilder<2>(this, kind) << child1 << child2; +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) { + NodeBuilder<2> nb(this, kind); + nb << child1 << child2; + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { - return NodeBuilder<>(this, kind) << child1 << child2 << child3; + return NodeBuilder<3>(this, kind) << child1 << child2 << child3; +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<3> nb(this, kind); + nb << child1 << child2 << child3; + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { - return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; + return NodeBuilder<4>(this, kind) << child1 << child2 << child3 << child4; +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<4> nb(this, kind); + nb << child1 << child2 << child3 << child4; + return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 + return NodeBuilder<5>(this, kind) << child1 << child2 << child3 << child4 << child5; } +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<5> nb(this, kind); + nb << child1 << child2 << child3 << child4 << child5; + return nb.constructNodePtr(); +} + // N-ary version template <bool ref_count> inline Node NodeManager::mkNode(Kind kind, @@ -766,16 +801,34 @@ inline Node NodeManager::mkNode(Kind kind, return NodeBuilder<>(this, kind).append(children); } -inline Node NodeManager::mkVar(const std::string& name, Type* type) { +template <bool ref_count> +inline Node* NodeManager::mkNodePtr(Kind kind, + const std::vector<NodeTemplate<ref_count> >& + children) { + return NodeBuilder<>(this, kind).append(children).constructNodePtr(); +} + +inline Node NodeManager::mkVar(const std::string& name, const Type& type) { Node n = mkVar(type); n.setAttribute(expr::VarNameAttr(), name); return n; } -inline Node NodeManager::mkVar(Type* type) { - Node n = Node(NodeBuilder<>(this, kind::VARIABLE)); - type->inc();// reference-count the type - n.setAttribute(TypeAttr(), type); +inline Node* NodeManager::mkVarPtr(const std::string& name, const Type& type) { + Node* n = mkVarPtr(type); + n->setAttribute(expr::VarNameAttr(), name); + return n; +} + +inline Node NodeManager::mkVar(const Type& type) { + Node n = NodeBuilder<0>(this, kind::VARIABLE); + n.setAttribute(TypeAttr(), *type.d_typeNode); + return n; +} + +inline Node* NodeManager::mkVarPtr(const Type& type) { + Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); + n->setAttribute(TypeAttr(), *type.d_typeNode); return n; } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 851c440b6..63d270ac1 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -15,6 +15,7 @@ #include "expr/node_manager.h" #include "expr/type.h" +#include "expr/type_constant.h" #include "util/Assert.h" #include <string> @@ -25,106 +26,187 @@ std::ostream& operator<<(std::ostream& out, const Type& e) { return out; } -Type::Type() : - d_name(std::string("<undefined>")), - d_rc(0) { +Type Type::makeType(NodeTemplate<false> typeNode) const +{ + return Type(d_nodeManager, new Node(typeNode)); } -Type::Type(std::string name) : - d_name(name), - d_rc(0) { +Type::Type(NodeManager* nm, NodeTemplate<true>* node) +: d_typeNode(node), + d_nodeManager(nm) +{ } -std::string Type::getName() const { - return d_name; +Type::~Type() { + NodeManagerScope nms(d_nodeManager); + delete d_typeNode; } -BooleanType BooleanType::s_instance; +Type::Type() +: d_typeNode(new Node()), + d_nodeManager(NULL) +{ +} -BooleanType::BooleanType() : - Type(std::string("BOOLEAN")) { - d_rc = RC_MAX;// singleton, not heap-allocated +Type::Type(uintptr_t n) +: d_typeNode(new Node()), + d_nodeManager(NULL) { + AlwaysAssert(n == 0); } -BooleanType::~BooleanType() { +Type::Type(const Type& t) +: d_typeNode(new Node(*t.d_typeNode)), + d_nodeManager(t.d_nodeManager) +{ } -BooleanType* BooleanType::getInstance() { - return &s_instance; +bool Type::isNull() const { + return d_typeNode->isNull(); } -bool BooleanType::isBoolean() const { - return true; +Type& Type::operator=(const Type& t) { + NodeManagerScope nms(d_nodeManager); + if (this != &t) { + *d_typeNode = *t.d_typeNode; + d_nodeManager = t.d_nodeManager; + } + return *this; } -FunctionType::FunctionType(const std::vector<Type*>& argTypes, - Type* range) : - d_argTypes(argTypes), - d_rangeType(range) { +bool Type::operator==(const Type& t) const { + return *d_typeNode == *t.d_typeNode; +} - Assert( argTypes.size() > 0 ); +bool Type::operator!=(const Type& t) const { + return *d_typeNode != *t.d_typeNode; } -// FIXME: What becomes of argument types? -FunctionType::~FunctionType() { +void Type::toStream(std::ostream& out) const { + NodeManagerScope nms(d_nodeManager); + // Do the cast by hand + if (isBoolean()) { out << (BooleanType)*this; return; } + if (isFunction()) { out << (FunctionType)*this; return; } + if (isKind()) { out << (KindType)*this; return; } + if (isSort()) { out << (SortType)*this; return; } + // We should not get here + Unreachable("Type not implemented completely"); } -const std::vector<Type*> FunctionType::getArgTypes() const { - return d_argTypes; +/** Is this the Boolean type? */ +bool Type::isBoolean() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getKind() == kind::TYPE_CONSTANT + && d_typeNode->getConst<TypeConstant>() == BOOLEAN_TYPE; } -Type* FunctionType::getRangeType() const { - return d_rangeType; +/** Cast to a Boolean type */ +Type::operator BooleanType() const { + NodeManagerScope nms(d_nodeManager); + Assert(isBoolean()); + return BooleanType(*this); } -bool FunctionType::isFunction() const { - return true; +/** Is this a function type? */ +bool Type::isFunction() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getKind() == kind::FUNCTION_TYPE; } -bool FunctionType::isPredicate() const { - return d_rangeType->isBoolean(); +/** Is this a predicate type? NOTE: all predicate types are also + function types. */ +bool Type::isPredicate() const { + NodeManagerScope nms(d_nodeManager); + return isFunction() && ((FunctionType)*this).getRangeType().isBoolean(); } -void FunctionType::toStream(std::ostream& out) const { - if( d_argTypes.size() > 1 ) { - out << "("; - } - for( unsigned int i=0; i < d_argTypes.size(); ++i ) { - if( i > 0 ) { - out << ","; - } - d_argTypes[i]->toStream(out); - } - if( d_argTypes.size() > 1 ) { - out << ")"; - } - out << " -> "; - d_rangeType->toStream(out); +/** Cast to a function type */ +Type::operator FunctionType() const { + NodeManagerScope nms(d_nodeManager); + Assert(isFunction()); + return FunctionType(*this); +} + +/** Is this a sort kind */ +bool Type::isSort() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getKind() == kind::VARIABLE && + d_typeNode->getType().isKind(); +} + +/** Cast to a sort type */ +Type::operator SortType() const { + NodeManagerScope nms(d_nodeManager); + Assert(isSort()); + return SortType(*this); } -KindType KindType::s_instance; +/** Is this a kind type (i.e., the type of a type)? */ +bool Type::isKind() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getKind() == kind::TYPE_CONSTANT + && d_typeNode->getConst<TypeConstant>() == KIND_TYPE; +} + +/** Cast to a kind type */ +Type::operator KindType() const { + NodeManagerScope nms(d_nodeManager); + Assert(isKind()); + return KindType(*this); +} -KindType::KindType() : - Type(std::string("KIND")) { - d_rc = RC_MAX;// singleton, not heap-allocated +std::vector<Type> FunctionType::getArgTypes() const { + NodeManagerScope nms(d_nodeManager); + std::vector<Type> args; + for (unsigned i = 0, i_end = d_typeNode->getNumChildren() - 1; i < i_end; ++ i) { + args.push_back(makeType((*d_typeNode)[i])); + } + return args; } -KindType::~KindType() { +Type FunctionType::getRangeType() const { + NodeManagerScope nms(d_nodeManager); + return makeType((*d_typeNode)[d_typeNode->getNumChildren()-1]); } -bool KindType::isKind() const { - return true; +void BooleanType::toStream(std::ostream& out) const { + out << "BOOLEAN"; } -KindType* KindType::getInstance() { - return &s_instance; +std::string SortType::getName() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getAttribute(expr::VarNameAttr()); } -SortType::SortType(std::string name) : - Type(name) { +void SortType::toStream(std::ostream& out) const { + NodeManagerScope nms(d_nodeManager); + out << getName(); } -SortType::~SortType() { +void FunctionType::toStream(std::ostream& out) const { + NodeManagerScope nms(d_nodeManager); + unsigned arity = d_typeNode->getNumChildren(); + + if(arity > 2) { + out << "("; + } + unsigned int i; + for(i=0; i < arity - 1; ++i) { + if(i > 0) { + out << ","; + } + out << makeType((*d_typeNode)[i]); + } + if(arity > 2) { + out << ")"; + } + out << " -> "; + (*d_typeNode)[i].toStream(out); } +BooleanType::BooleanType(const Type& t) : Type(t) {} +FunctionType::FunctionType(const Type& t) : Type(t) {} +KindType::KindType(const Type& t) : Type(t) {} +SortType::SortType(const Type& t) : Type(t) {} + + }/* CVC4 namespace */ diff --git a/src/expr/type.h b/src/expr/type.h index 8a9d6cd70..4f9142698 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -24,153 +24,146 @@ #include <string> #include <vector> #include <limits.h> +#include <stdint.h> namespace CVC4 { -namespace expr { - namespace attr { - struct TypeCleanupStrategy; - }/* CVC4::expr::attr namespace */ -}/* CVC4::expr namespace */ - class NodeManager; +template <bool ref_count> class NodeTemplate; + +class BooleanType; +class FunctionType; +class KindType; +class SortType; /** * Class encapsulating CVC4 expression types. */ class CVC4_PUBLIC Type { + + friend class NodeManager; + protected: - static const unsigned RC_MAX = UINT_MAX; + + /** The internal expression representation */ + NodeTemplate<true>* d_typeNode; + + /** The responsible expression manager */ + NodeManager* d_nodeManager; + + /** + * Construct a new type given the typeNode; + */ + Type makeType(NodeTemplate<false> typeNode) const; + + /** + * Constructor for internal purposes. + * @param em the expression manager that handles this expression + * @param node the actual expression node pointer for this type + */ + Type(NodeManager* em, NodeTemplate<true>* typeNode); public: + /** + * Initialize from an integer. Fails if the integer is not 0. + * NOTE: This is here purely to support the auto-initialization + * behavior of the ANTLR3 C backend. Should be removed if future + * versions of ANTLR fix the problem. + */ + Type(uintptr_t n); + + /** Force a virtual destructor for safety. */ + virtual ~Type(); + + /** Default constructor */ + Type(); + + /** Copy constructor */ + Type(const Type& t); + + /** Check whether this is a null type */ + bool isNull() const; + + /** Assignment operator */ + Type& operator=(const Type& t); + /** Comparison for equality */ - //bool operator==(const Type& t) const; + bool operator==(const Type& t) const; /** Comparison for disequality */ - //bool operator!=(const Type& e) const; + bool operator!=(const Type& t) const; - /** Get the name of this type. May be empty for composite types. */ - std::string getName() const; + /** Is this the Boolean type? */ + bool isBoolean() const; - /** Is this the boolean type? */ - virtual bool isBoolean() const { - return false; - } + /** Cast to a Boolean type */ + operator BooleanType() const; /** Is this a function type? */ - virtual bool isFunction() const { - return false; - } + bool isFunction() const; /** Is this a predicate type? NOTE: all predicate types are also function types. */ - virtual bool isPredicate() const { - return false; - } + bool isPredicate() const; - /** Is this a kind type (i.e., the type of a type)? */ - virtual bool isKind() const { - return false; - } + /** Cast to a function type */ + operator FunctionType() const; - /** Outputs a string representation of this type to the stream. */ - virtual void toStream(std::ostream& out) const { - out << getName(); - } + /** Is this a sort kind */ + bool isSort() const; -protected: - /** Create an un-named type. */ - Type(); + /** Cast to a sort type */ + operator SortType() const; - /** Create a type with the given name. */ - Type(std::string name); + /** Is this a kind type (i.e., the type of a type)? */ + bool isKind() const; - /** The name of the type (may be empty). */ - std::string d_name; + /** Cast to a kind type */ + operator KindType() const; - /** - * The reference count for this Type (how many times it's referred - * to in the Type attribute table) - */ - unsigned d_rc; + /** Outputs a string representation of this type to the stream. */ + virtual void toStream(std::ostream& out) const; - /** Force a virtual destructor for safety. */ - virtual ~Type() { - Assert(d_rc == RC_MAX || d_rc == 0, - "illegal ref count %u for destructed Type", d_rc); - } - - /** Increment the reference count */ - void inc() { - if(d_rc != RC_MAX) { - ++d_rc; - } - } - - /** Decrement the reference count */ - void dec() { - if(d_rc != RC_MAX) { - Assert(d_rc != 0, "illegal ref count %u for dec()", d_rc); - --d_rc; - } - } - - friend class ::CVC4::NodeManager; - friend struct ::CVC4::expr::attr::TypeCleanupStrategy; }; /** * Singleton class encapsulating the boolean type. */ -class BooleanType : public Type { +class CVC4_PUBLIC BooleanType : public Type { public: - /** Is this the boolean type? (Returns true.) */ - bool isBoolean() const; - static BooleanType* getInstance(); -private: + /** Construct from the base type */ + BooleanType(const Type& type); - /** Create a type associated with nodeManager. */ - BooleanType(); - - /** - * Do-nothing private copy constructor operator, to prevent - * copy-construction. - */ - BooleanType(const BooleanType&); - - /** Destructor */ - ~BooleanType(); - - /** - * Do-nothing private assignment operator, to prevent assignment. - */ - BooleanType& operator=(const BooleanType&); + /** Is this the boolean type? (Returns true.) */ + bool isBoolean() const; - /** The singleton instance */ - static BooleanType s_instance; + /** Just outputs BOOLEAN */ + void toStream(std::ostream& out) const; }; /** * Class encapsulating a function type. - * TODO: Override == to check component types? */ -class FunctionType : public Type { +class CVC4_PUBLIC FunctionType : public Type { public: - /** Retrieve the argument types. The vector will be non-empty. */ - const std::vector<Type*> getArgTypes() const; + + /** Construct from the base type */ + FunctionType(const Type& type); + + /** Get the argument types */ + std::vector<Type> getArgTypes() const; /** Get the range type (i.e., the type of the result). */ - Type* getRangeType() const; + Type getRangeType() const; /** Is this as function type? (Returns true.) */ bool isFunction() const; - /** Is this as predicate type? (Returns true if range is - boolean.) */ + /** Is this as predicate type? (Returns true if range is Boolean.) */ bool isPredicate() const; /** @@ -179,74 +172,38 @@ public: */ void toStream(std::ostream& out) const; -private: - - /** - * Construct a function type associated with nodeManager, given a - * vector of argument types and the range type. - - * @param argTypes a non-empty vector of input types - * @param range the result type - */ - FunctionType(const std::vector<Type*>& argTypes, - Type* range); - - /** Destructor */ - ~FunctionType(); - - /** The list of input types. */ - const std::vector<Type*> d_argTypes; - - /** The result type. */ - Type* d_rangeType; - - friend class NodeManager; }; - -/** Class encapsulating the kind type (the type of types). -*/ -class KindType : public Type { +/** + * Class encapsulating a user-defined sort. + */ +class CVC4_PUBLIC SortType : public Type { public: - /** Is this the kind type? (Returns true.) */ - bool isKind() const; - - /** Get an instance of the kind type. */ - static KindType* getInstance(); - -private: - - KindType(); - - /* Do-nothing private copy constructor, to prevent copy - construction. */ - KindType(const KindType&); - /** Destructor */ - ~KindType(); + /** Construct from the base type */ + SortType(const Type& type); - /* Do-nothing private assignment operator, to prevent assignment. */ - KindType& operator=(const KindType&); + /** Get the name of the sort */ + std::string getName() const; - /** The singleton instance */ - static KindType s_instance; + /** Outouts the name of the sort */ + void toStream(std::ostream& out) const; }; -/** Class encapsulating a user-defined sort. - TODO: Should sort be uniquely named per-nodeManager and not conflict - with any builtins? */ -class SortType : public Type { +/** + * Class encapsulating the kind type (the type of types). + */ +class CVC4_PUBLIC KindType : public Type { public: - /** Destructor */ - ~SortType(); -private: - /** Create a sort with the given name. */ - SortType(std::string name); + /** Construct from the base type */ + KindType(const Type& type); + + /** Is this the kind type? (Returns true.) */ + bool isKind() const; - friend class NodeManager; }; /** @@ -257,22 +214,6 @@ private: */ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; -namespace expr { -namespace attr { - -struct TypeCleanupStrategy { - static void cleanup(Type* t) { - // reference-count the Type - t->dec(); - if(t->d_rc == 0) { - delete t; - } - } -};/* struct TypeCleanupStrategy */ - -}/* CVC4::expr::attr namespace */ -}/* CVC4::expr namespace */ - }/* CVC4 namespace */ #endif /* __CVC4__TYPE_H */ diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h new file mode 100644 index 000000000..86698459b --- /dev/null +++ b/src/expr/type_constant.h @@ -0,0 +1,26 @@ +/* + * type_constant.h + * + * Created on: Apr 5, 2010 + * Author: dejan + */ + +#ifndef __CVC4__TYPE_CONSTANT_H_ +#define __CVC4__TYPE_CONSTANT_H_ + +namespace CVC4 { + +enum TypeConstant { + BOOLEAN_TYPE, + KIND_TYPE +}; + +struct TypeConstantHashStrategy { + static inline size_t hash(TypeConstant tc) { + return tc; + } +};/* struct BoolHashStrategy */ + +} + +#endif /* __CVC4__TYPE_CONSTANT_H_ */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 16bde1de3..3f4435966 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -123,7 +123,7 @@ command returns [CVC4::Command* cmd = 0] declaration[CVC4::Command*& cmd] @init { std::vector<std::string> ids; - Type* t; + Type t; Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; } : // FIXME: These could be type or function declarations, if that matters. @@ -132,7 +132,7 @@ declaration[CVC4::Command*& cmd] ; /** Match the right-hand side of a declaration. Returns the type. */ -declType[CVC4::Type*& t, std::vector<std::string>& idList] +declType[CVC4::Type& t, std::vector<std::string>& idList] @init { Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } @@ -148,10 +148,10 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList] * Match the type in a declaration and do the declaration binding. * TODO: Actually parse sorts into Type objects. */ -type[CVC4::Type*& t] +type[CVC4::Type& t] @init { - Type* t2; - std::vector<Type*> typeList; + Type t2; + std::vector<Type> typeList; Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* Simple type */ @@ -199,7 +199,7 @@ identifier[std::string& id, * Matches a type. * TODO: parse more types */ -baseType[CVC4::Type*& t] +baseType[CVC4::Type& t] @init { std::string id; Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; @@ -211,7 +211,7 @@ baseType[CVC4::Type*& t] /** * Matches a type identifier */ -typeSymbol[CVC4::Type*& t] +typeSymbol[CVC4::Type& t] @init { std::string id; Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 5f07b16b7..57914c9de 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -62,38 +62,38 @@ Expr ParserState::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Type* +Type ParserState::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); - Type* t = getSymbol(var_name,type).getType(); + Type t = getSymbol(var_name,type).getType(); return t; } -Type* ParserState::getSort(const std::string& name) { +Type ParserState::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); - Type *t = d_declScope.lookupType(name); + Type t = d_declScope.lookupType(name); return t; } /* Returns true if name is bound to a boolean variable. */ bool ParserState::isBoolean(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean(); + return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); } /* Returns true if name is bound to a function. */ bool ParserState::isFunction(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction(); + return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); } /* Returns true if name is bound to a function returning boolean. */ bool ParserState::isPredicate(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); + return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); } Expr -ParserState::mkVar(const std::string& name, Type* type) { - Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; +ParserState::mkVar(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); defineVar(name,expr); return expr; @@ -101,7 +101,7 @@ ParserState::mkVar(const std::string& name, Type* type) { const std::vector<Expr> ParserState::mkVars(const std::vector<std::string> names, - Type* type) { + const Type& type) { std::vector<Expr> vars; for(unsigned i = 0; i < names.size(); ++i) { vars.push_back(mkVar(names[i],type)); @@ -134,19 +134,19 @@ ParserState::setLogic(const std::string& name) { } } -Type* +Type ParserState::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ) ; - Type* type = d_exprManager->mkSort(name); + Type type = d_exprManager->mkSort(name); d_declScope.bindType(name, type); Assert( isDeclared(name, SYM_SORT) ) ; return type; } -const std::vector<Type*> +const std::vector<Type> ParserState::mkSorts(const std::vector<std::string>& names) { - std::vector<Type*> types; + std::vector<Type> types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(mkSort(names[i])); } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index de624e3a0..3ca9c2c0e 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -174,7 +174,7 @@ public: /** * Returns a sort, given a name */ - Type* getSort(const std::string& sort_name); + Type getSort(const std::string& sort_name); /** * Checks if a symbol has been declared. @@ -216,15 +216,15 @@ public: * @param var_name the symbol to lookup * @param type the (namespace) type of the symbol */ - Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); + Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, Type* type); + Expr mkVar(const std::string& name, const Type& type); /** Create a set of new CVC4 variable expressions of the given type. */ const std::vector<Expr> - mkVars(const std::vector<std::string> names, Type* type); + mkVars(const std::vector<std::string> names, const Type& type); /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); @@ -234,12 +234,12 @@ public: /** * Creates a new sort with the given name. */ - Type* mkSort(const std::string& name); + Type mkSort(const std::string& name); /** * Creates a new sorts with the given names. */ - const std::vector<Type*> + const std::vector<Type> mkSorts(const std::vector<std::string>& names); /** Is the symbol bound to a boolean variable? */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 25c2fbc89..15f0c8844 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -285,7 +285,7 @@ attribute functionDeclaration @declarations { std::string name; - std::vector<Type*> sorts; + std::vector<Type> sorts; } : LPAREN_TOK functionName[name,CHECK_UNDECLARED] t = sortSymbol // require at least one sort @@ -305,10 +305,10 @@ functionDeclaration predicateDeclaration @declarations { std::string name; - std::vector<Type*> p_sorts; + std::vector<Type> p_sorts; } : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type *t; + { Type t; if( p_sorts.empty() ) { t = EXPR_MANAGER->booleanType(); } else { @@ -329,7 +329,7 @@ sortDeclaration /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sortList[std::vector<CVC4::Type*>& sorts] +sortList[std::vector<CVC4::Type>& sorts] : ( t = sortSymbol { sorts.push_back(t); })* ; @@ -341,7 +341,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : identifier[name,check,SYM_SORT] ; -sortSymbol returns [CVC4::Type* t] +sortSymbol returns [CVC4::Type t] @declarations { std::string name; } diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index dc2ad4d35..8a4c6b6f7 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -5,3 +5,9 @@ # theory ::CVC4::theory::bv::TheoryBV "theory_bv.h" + +constant CONST_BITVECTOR \ + ::CVC4::BitVector \ + ::CVC4::BitVectorHashStrategy \ + "util/bitvector.h" \ + "a fixed-width bit-vector constant"
\ No newline at end of file diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 37542d952..d9b7a4fa6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -139,7 +139,7 @@ class TheoryEngine { } Debug("rewrite") << "rewrote-children of " << in << std::endl << "got " << b << std::endl; - return Node(b); + return b; } /** diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 6597c8b48..7820acb0a 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -25,4 +25,7 @@ libutil_la_SOURCES = \ rational.h \ rational.cpp \ integer.h \ - integer.cpp + integer.cpp \ + bitvector.h \ + bitvector.cpp \ + gmp_util.h diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp new file mode 100644 index 000000000..bea06f71a --- /dev/null +++ b/src/util/bitvector.cpp @@ -0,0 +1,16 @@ +/* + * bitvector.cpp + * + * Created on: Apr 5, 2010 + * Author: dejan + */ + +#include "bitvector.h" + +namespace CVC4 { + +std::ostream& operator <<(std::ostream& os, const BitVector& bv) { + return os << bv.toString(); +} + +} diff --git a/src/util/bitvector.h b/src/util/bitvector.h new file mode 100644 index 000000000..3859fa407 --- /dev/null +++ b/src/util/bitvector.h @@ -0,0 +1,99 @@ +/* + * bitvector.h + * + * Created on: Mar 31, 2010 + * Author: dejan + */ + +#ifndef __CVC4__BITVECTOR_H_ +#define __CVC4__BITVECTOR_H_ + +#include <string> +#include <iostream> +#include "util/gmp_util.h" + +namespace CVC4 { + +class BitVector { + +private: + + unsigned d_size; + mpz_class d_value; + + BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {} + +public: + + BitVector(unsigned size = 0) + : d_size(size), d_value(0) {} + + BitVector(unsigned size, unsigned int z) + : d_size(size), d_value(z) {} + + BitVector(unsigned size, unsigned long int z) + : d_size(size), d_value(z) {} + + BitVector(unsigned size, const BitVector& q) + : d_size(size), d_value(q.d_value) {} + + ~BitVector() {} + + BitVector& operator =(const BitVector& x) { + if(this == &x) + return *this; + d_value = x.d_value; + return *this; + } + + bool operator ==(const BitVector& y) const { + if (d_size != y.d_size) return false; + return d_value == y.d_value; + } + + bool operator !=(const BitVector& y) const { + if (d_size == y.d_size) return false; + return d_value != y.d_value; + } + + BitVector operator +(const BitVector& y) const { + return BitVector(std::max(d_size, y.d_size), d_value + y.d_value); + } + + BitVector operator -(const BitVector& y) const { + return *this + ~y + 1; + } + + BitVector operator -() const { + return ~(*this) + 1; + } + + BitVector operator *(const BitVector& y) const { + return BitVector(d_size, d_value * y.d_value); + } + + BitVector operator ~() const { + return BitVector(d_size, d_value); + } + + size_t hash() const { + return gmpz_hash(d_value.get_mpz_t()); + } + + std::string toString(unsigned int base = 2) const { + return d_value.get_str(base); + } +}; + +struct BitVectorHashStrategy { + static inline size_t hash(const BitVector& bv) { + return bv.hash(); + } +}; + +std::ostream& operator <<(std::ostream& os, const BitVector& bv); + +} + + +#endif /* __CVC4__BITVECTOR_H_ */ diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h new file mode 100644 index 000000000..1849974cd --- /dev/null +++ b/src/util/gmp_util.h @@ -0,0 +1,28 @@ +/* + * gmp.h + * + * Created on: Apr 5, 2010 + * Author: dejan + */ + +#ifndef __CVC4__GMP_H_ +#define __CVC4__GMP_H_ + +#include <gmpxx.h> + +namespace CVC4 { + + /** Hashes the gmp integer primitive in a word by word fashion. */ + inline size_t gmpz_hash(const mpz_t toHash) { + size_t hash = 0; + for (int i=0, n=mpz_size(toHash); i<n; ++i){ + mp_limb_t limb = mpz_getlimbn(toHash, i); + hash = hash * 2; + hash = hash xor limb; + } + return hash; + } + +} + +#endif /* __CVC4__GMP_H_ */ diff --git a/src/util/integer.cpp b/src/util/integer.cpp index 3a7851eec..a26f2108f 100644 --- a/src/util/integer.cpp +++ b/src/util/integer.cpp @@ -23,6 +23,6 @@ using namespace CVC4; -std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){ +std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) { return os << n.toString(); } diff --git a/src/util/integer.h b/src/util/integer.h index c1e5d90ea..2aa8b711a 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -18,22 +18,12 @@ #ifndef __CVC4__INTEGER_H #define __CVC4__INTEGER_H -#include <gmpxx.h> #include <string> +#include <iostream> +#include "util/gmp_util.h" namespace CVC4 { -/** Hashes the gmp integer primitive in a word by word fashion. */ -inline size_t gmpz_hash(const mpz_t toHash){ - size_t hash = 0; - for (int i=0, n=mpz_size(toHash); i<n; ++i){ - mp_limb_t limb = mpz_getlimbn(toHash, i); - hash = hash * 2; - hash = hash xor limb; - } - return hash; -} - class Rational; class Integer { diff --git a/src/util/rational.h b/src/util/rational.h index 48b00899a..e4f0e2bb7 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -24,9 +24,8 @@ #ifndef __CVC4__RATIONAL_H #define __CVC4__RATIONAL_H -#include <gmpxx.h> #include <string> -#include "integer.h" +#include "util/integer.h" namespace CVC4 { @@ -76,20 +75,20 @@ public: /** * Constructs a canonical Rational from a numerator and denominator. */ - Rational( signed int n, signed int d) : d_value(n,d) { + Rational(signed int n, signed int d) : d_value(n,d) { d_value.canonicalize(); } Rational(unsigned int n, unsigned int d) : d_value(n,d) { d_value.canonicalize(); } - Rational( signed long int n, signed long int d) : d_value(n,d) { + Rational(signed long int n, signed long int d) : d_value(n,d) { d_value.canonicalize(); } Rational(unsigned long int n, unsigned long int d) : d_value(n,d) { d_value.canonicalize(); } - Rational(const Integer& n, const Integer& d): + Rational(const Integer& n, const Integer& d) : d_value(n.get_mpz(), d.get_mpz()) { d_value.canonicalize(); diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 5ae644193..d0be9a351 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -70,7 +70,7 @@ public: typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute; void testDeallocation() { - Type* booleanType = d_nodeManager->booleanType(); + Type booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); MyData* data; MyData* data1; @@ -88,7 +88,7 @@ public: typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute; typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute; void testInts(){ - Type* booleanType = d_nodeManager->booleanType(); + BooleanType booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); const uint64_t val = 63489; uint64_t data0 = 0; @@ -116,7 +116,7 @@ public: typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute; typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute; void testTNodes(){ - Type* booleanType = d_nodeManager->booleanType(); + BooleanType booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); Node val(d_nodeManager->mkVar(booleanType)); @@ -151,7 +151,7 @@ public: typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute; typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute; void testPtrs(){ - Type* booleanType = d_nodeManager->booleanType(); + BooleanType booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); Foo* val = new Foo(63489); @@ -182,7 +182,7 @@ public: typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute; typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute; void testConstPtrs(){ - Type* booleanType = d_nodeManager->booleanType(); + BooleanType booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); const Foo* val = new Foo(63489); @@ -212,7 +212,7 @@ public: typedef expr::Attribute<StringAttributeId, std::string> StringAttribute; typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute; void testStrings(){ - Type* booleanType = d_nodeManager->booleanType(); + BooleanType booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); std::string val("63489"); @@ -241,7 +241,7 @@ public: typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute; typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute; void testBools(){ - Type* booleanType = d_nodeManager->booleanType(); + BooleanType booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); bool val = true; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index e3b7811a4..bfe0ef3cf 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -69,10 +69,11 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_booleanType = d_nm->booleanType(); + d_booleanType = new Type(d_nm->booleanType()); } void tearDown() { + delete d_booleanType; delete d_scope; delete d_nm; delete d_ctxt; @@ -101,9 +102,7 @@ public: TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); lastId = attr::LastAttributeId<void*, false>::s_id; - TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); - TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id); lastId = attr::LastAttributeId<bool, false>::s_id; TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId); @@ -146,14 +145,18 @@ public: lastId = attr::LastAttributeId<TNode, false>::s_id; TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId); + + lastId = attr::LastAttributeId<Node, false>::s_id; + TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); + } void testCDAttributes() { //Debug.on("boolattr"); - Node a = d_nm->mkVar(d_booleanType); - Node b = d_nm->mkVar(d_booleanType); - Node c = d_nm->mkVar(d_booleanType); + Node a = d_nm->mkVar(*d_booleanType); + Node b = d_nm->mkVar(*d_booleanType); + Node c = d_nm->mkVar(*d_booleanType); Debug("boolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -279,10 +282,10 @@ public: void testAttributes() { //Debug.on("boolattr"); - Node a = d_nm->mkVar(d_booleanType); - Node b = d_nm->mkVar(d_booleanType); - Node c = d_nm->mkVar(d_booleanType); - Node unnamed = d_nm->mkVar(d_booleanType); + Node a = d_nm->mkVar(*d_booleanType); + Node b = d_nm->mkVar(*d_booleanType); + Node c = d_nm->mkVar(*d_booleanType); + Node unnamed = d_nm->mkVar(*d_booleanType); a.setAttribute(VarNameAttr(), "a"); b.setAttribute(VarNameAttr(), "b"); diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h index f93a3fcc8..67e6d3e98 100644 --- a/test/unit/expr/declaration_scope_black.h +++ b/test/unit/expr/declaration_scope_black.h @@ -56,7 +56,7 @@ public: void testBind() { DeclarationScope declScope; - Type *booleanType = d_exprManager->booleanType(); + Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); declScope.bind("x",x); TS_ASSERT( declScope.isBound("x") ); @@ -65,7 +65,7 @@ public: void testBind2() { DeclarationScope declScope; - Type *booleanType = d_exprManager->booleanType(); + Type booleanType = d_exprManager->booleanType(); // var name attribute shouldn't matter Expr y = d_exprManager->mkVar("y", booleanType); declScope.bind("x",y); @@ -75,7 +75,7 @@ public: void testBind3() { DeclarationScope declScope; - Type *booleanType = d_exprManager->booleanType(); + Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); declScope.bind("x",x); Expr y = d_exprManager->mkVar(booleanType); @@ -87,11 +87,11 @@ public: void testBind4() { DeclarationScope declScope; - Type *booleanType = d_exprManager->booleanType(); + Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); declScope.bind("x",x); - Type *t = d_exprManager->mkSort("T"); + Type t = d_exprManager->mkSort("T"); // duplicate binding for type is OK declScope.bindType("x",t); @@ -103,7 +103,7 @@ public: void testBindType() { DeclarationScope declScope; - Type *s = d_exprManager->mkSort("S"); + Type s = d_exprManager->mkSort("S"); declScope.bindType("S",s); TS_ASSERT( declScope.isBoundType("S") ); TS_ASSERT_EQUALS( declScope.lookupType("S"), s ); @@ -112,7 +112,7 @@ public: void testBindType2() { DeclarationScope declScope; // type name attribute shouldn't matter - Type *s = d_exprManager->mkSort("S"); + Type s = d_exprManager->mkSort("S"); declScope.bindType("T",s); TS_ASSERT( declScope.isBoundType("T") ); TS_ASSERT_EQUALS( declScope.lookupType("T"), s ); @@ -120,9 +120,9 @@ public: void testBindType3() { DeclarationScope declScope; - Type *s = d_exprManager->mkSort("S"); + Type s = d_exprManager->mkSort("S"); declScope.bindType("S",s); - Type *t = d_exprManager->mkSort("T"); + Type t = d_exprManager->mkSort("T"); // new binding covers old declScope.bindType("S",t); TS_ASSERT( declScope.isBoundType("S") ); @@ -131,7 +131,7 @@ public: void testPushScope() { DeclarationScope declScope; - Type *booleanType = d_exprManager->booleanType(); + Type booleanType = d_exprManager->booleanType(); Expr x = d_exprManager->mkVar(booleanType); declScope.bind("x",x); declScope.pushScope(); diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index fd36a7cfa..f40e32ef9 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -254,22 +254,18 @@ public: } void testGetType() { - /* Type* getType() const; */ + /* Type getType(); */ TS_ASSERT(a->getType() == d_em->booleanType()); TS_ASSERT(b->getType() == d_em->booleanType()); - TS_ASSERT(c->getType() == NULL); - TS_ASSERT(mult->getType() == NULL); - TS_ASSERT(plus->getType() == NULL); - TS_ASSERT(d->getType() == NULL); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(null->getType(), AssertionException); -#endif /* CVC4_ASSERTIONS */ - - TS_ASSERT(i1->getType() == NULL); - TS_ASSERT(i2->getType() == NULL); - TS_ASSERT(r1->getType() == NULL); - TS_ASSERT(r2->getType() == NULL); + TS_ASSERT(c->getType().isNull()); + TS_ASSERT(mult->getType().isNull()); + TS_ASSERT(plus->getType().isNull()); + TS_ASSERT(d->getType().isNull()); + TS_ASSERT(i1->getType().isNull()); + TS_ASSERT(i2->getType().isNull()); + TS_ASSERT(r1->getType().isNull()); + TS_ASSERT(r2->getType().isNull()); } void testToString() { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 23d1daf4e..6469806d6 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -36,7 +36,7 @@ private: Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; - Type* d_booleanType; + Type *d_booleanType; public: @@ -44,11 +44,11 @@ public: d_ctxt = new Context; d_nodeManager = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nodeManager); - - d_booleanType = d_nodeManager->booleanType(); + d_booleanType = new Type(d_nodeManager->booleanType()); } void tearDown() { + delete d_booleanType; delete d_scope; delete d_nodeManager; delete d_ctxt; @@ -97,12 +97,12 @@ public: void testOperatorEquals() { Node a, b, c; - b = d_nodeManager->mkVar(d_booleanType); + b = d_nodeManager->mkVar(*d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkVar(d_booleanType); + Node d = d_nodeManager->mkVar(*d_booleanType); TS_ASSERT(a==a); TS_ASSERT(a==b); @@ -137,12 +137,12 @@ public: Node a, b, c; - b = d_nodeManager->mkVar(d_booleanType); + b = d_nodeManager->mkVar(*d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkVar(d_booleanType); + Node d = d_nodeManager->mkVar(*d_booleanType); /*structed assuming operator == works */ TS_ASSERT(iff(a!=a, !(a==a))); @@ -199,7 +199,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType)); + Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(*d_booleanType)); b = c; TS_ASSERT(b==c); @@ -320,8 +320,8 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node a = d_nodeManager->mkVar(d_booleanType); - Node b = d_nodeManager->mkVar(d_booleanType); + Node a = d_nodeManager->mkVar(*d_booleanType); + Node b = d_nodeManager->mkVar(*d_booleanType); Node cnd = d_nodeManager->mkNode(PLUS, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -383,8 +383,8 @@ public: void testGetKind() { /*inline Kind getKind() const; */ - Node a = d_nodeManager->mkVar(d_booleanType); - Node b = d_nodeManager->mkVar(d_booleanType); + Node a = d_nodeManager->mkVar(*d_booleanType); + Node b = d_nodeManager->mkVar(*d_booleanType); Node n = d_nodeManager->mkNode(NOT, a); TS_ASSERT(NOT == n.getKind()); @@ -400,9 +400,9 @@ public: } void testGetOperator() { - Type* sort = d_nodeManager->mkSort("T"); - Type* booleanType = d_nodeManager->booleanType(); - Type* predType = d_nodeManager->mkFunctionType(sort, booleanType); + Type sort = d_nodeManager->mkSort("T"); + Type booleanType = d_nodeManager->booleanType(); + Type predType = d_nodeManager->mkFunctionType(sort, booleanType); Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); @@ -466,9 +466,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nodeManager->mkVar(d_booleanType); - Node y = d_nodeManager->mkVar(d_booleanType); - Node z = d_nodeManager->mkVar(d_booleanType); + Node x = d_nodeManager->mkVar(*d_booleanType); + Node y = d_nodeManager->mkVar(*d_booleanType); + Node z = d_nodeManager->mkVar(*d_booleanType); Node n = b << x << y << z << kind::AND; { // iterator @@ -490,7 +490,7 @@ public: } void testToString() { - Type* booleanType = d_nodeManager->booleanType(); + Type booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar("w",booleanType); Node x = d_nodeManager->mkVar("x",booleanType); @@ -503,7 +503,7 @@ public: } void testToStream() { - Type* booleanType = d_nodeManager->booleanType(); + Type booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar("w",booleanType); Node x = d_nodeManager->mkVar("x",booleanType); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 4521f3bf6..17e1d6f18 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -47,10 +47,11 @@ public: d_scope = new NodeManagerScope(d_nm); specKind = PLUS; - d_booleanType = d_nm->booleanType(); + d_booleanType = new Type(d_nm->booleanType()); } void tearDown() { + delete d_booleanType; delete d_scope; delete d_nm; delete d_ctxt; @@ -212,9 +213,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nm->mkVar(d_booleanType); - Node y = d_nm->mkVar(d_booleanType); - Node z = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); + Node y = d_nm->mkVar(*d_booleanType); + Node z = d_nm->mkVar(*d_booleanType); b << x << y << z << AND; { @@ -463,9 +464,9 @@ public: } void testAppend() { - Node x = d_nm->mkVar(d_booleanType); - Node y = d_nm->mkVar(d_booleanType); - Node z = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); + Node y = d_nm->mkVar(*d_booleanType); + Node z = d_nm->mkVar(*d_booleanType); Node m = d_nm->mkNode(AND, y, z, x); Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z); Node o = d_nm->mkNode(XOR, y, x); @@ -590,12 +591,12 @@ public: } void testConvenienceBuilders() { - Node a = d_nm->mkVar(d_booleanType); - Node b = d_nm->mkVar(d_booleanType); - Node c = d_nm->mkVar(d_booleanType); - Node d = d_nm->mkVar(d_booleanType); - Node e = d_nm->mkVar(d_booleanType); - Node f = d_nm->mkVar(d_booleanType); + Node a = d_nm->mkVar(*d_booleanType); + Node b = d_nm->mkVar(*d_booleanType); + Node c = d_nm->mkVar(*d_booleanType); + Node d = d_nm->mkVar(*d_booleanType); + Node e = d_nm->mkVar(*d_booleanType); + Node f = d_nm->mkVar(*d_booleanType); Node m = a && b; Node n = (a && b) || c; diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index e059fa509..873e28bb3 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -142,7 +142,7 @@ public: } void testMkVar1() { - Type* booleanType = d_nodeManager->booleanType(); + Type booleanType = d_nodeManager->booleanType(); Node x = d_nodeManager->mkVar(booleanType); TS_ASSERT_EQUALS(x.getKind(),VARIABLE); TS_ASSERT_EQUALS(x.getNumChildren(),0u); @@ -150,7 +150,7 @@ public: } void testMkVar2() { - Type* booleanType = d_nodeManager->booleanType(); + Type booleanType = d_nodeManager->booleanType(); Node x = d_nodeManager->mkVar("x", booleanType); TS_ASSERT_EQUALS(x.getKind(),VARIABLE); TS_ASSERT_EQUALS(x.getNumChildren(),0u); @@ -187,19 +187,19 @@ public: } void testBooleanType() { - Type* booleanType1 = d_nodeManager->booleanType(); - Type* booleanType2 = d_nodeManager->booleanType(); - Type* otherType = d_nodeManager->mkSort("T"); - TS_ASSERT( booleanType1->isBoolean() ); + Type booleanType1 = d_nodeManager->booleanType(); + Type booleanType2 = d_nodeManager->booleanType(); + Type otherType = d_nodeManager->mkSort("T"); + TS_ASSERT( booleanType1.isBoolean() ); TS_ASSERT_EQUALS(booleanType1, booleanType2); TS_ASSERT( booleanType1 != otherType ); } void testKindType() { - Type* kindType1 = d_nodeManager->kindType(); - Type* kindType2 = d_nodeManager->kindType(); - Type* otherType = d_nodeManager->mkSort("T"); - TS_ASSERT( kindType1->isKind() ); + Type kindType1 = d_nodeManager->kindType(); + Type kindType2 = d_nodeManager->kindType(); + Type otherType = d_nodeManager->mkSort("T"); + TS_ASSERT( kindType1.isKind() ); TS_ASSERT_EQUALS(kindType1, kindType2); TS_ASSERT( kindType1 != otherType ); // TODO: Is there a way to get the type of otherType (it should == kindType) @@ -213,98 +213,98 @@ public: * with the current type implementation it's the best we can do. */ void testMkFunctionType2() { - Type *booleanType = d_nodeManager->booleanType(); - Type *t = d_nodeManager->mkFunctionType(booleanType,booleanType); + Type booleanType = d_nodeManager->booleanType(); + Type t = d_nodeManager->mkFunctionType(booleanType,booleanType); TS_ASSERT( t != booleanType ); - TS_ASSERT( t->isFunction() ); + TS_ASSERT( t.isFunction() ); - FunctionType* ft = (FunctionType*)t; - TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u); - TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType); - TS_ASSERT_EQUALS(ft->getRangeType(), booleanType); + FunctionType ft = (FunctionType)t; + TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u); + TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType); + TS_ASSERT_EQUALS(ft.getRangeType(), booleanType); /* Type *t2 = d_nodeManager->mkFunctionType(booleanType,booleanType); TS_ASSERT_EQUALS( t, t2 );*/ } void testMkFunctionTypeVecType() { - Type *a = d_nodeManager->mkSort("a"); - Type *b = d_nodeManager->mkSort("b"); - Type *c = d_nodeManager->mkSort("c"); + Type a = d_nodeManager->mkSort("a"); + Type b = d_nodeManager->mkSort("b"); + Type c = d_nodeManager->mkSort("c"); - std::vector<Type*> argTypes; + std::vector<Type> argTypes; argTypes.push_back(a); argTypes.push_back(b); - Type *t = d_nodeManager->mkFunctionType(argTypes,c); + Type t = d_nodeManager->mkFunctionType(argTypes,c); TS_ASSERT( t != a ); TS_ASSERT( t != b ); TS_ASSERT( t != c ); - TS_ASSERT( t->isFunction() ); + TS_ASSERT( t.isFunction() ); - FunctionType* ft = (FunctionType*)t; - TS_ASSERT_EQUALS(ft->getArgTypes().size(), argTypes.size()); - TS_ASSERT_EQUALS(ft->getArgTypes()[0], a); - TS_ASSERT_EQUALS(ft->getArgTypes()[1], b); - TS_ASSERT_EQUALS(ft->getRangeType(), c); + FunctionType ft = (FunctionType)t; + TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size()); + TS_ASSERT_EQUALS(ft.getArgTypes()[0], a); + TS_ASSERT_EQUALS(ft.getArgTypes()[1], b); + TS_ASSERT_EQUALS(ft.getRangeType(), c); /* Type *t2 = d_nodeManager->mkFunctionType(argTypes,c); TS_ASSERT_EQUALS( t, t2 );*/ } void testMkFunctionTypeVec() { - Type *a = d_nodeManager->mkSort("a"); - Type *b = d_nodeManager->mkSort("b"); - Type *c = d_nodeManager->mkSort("c"); + Type a = d_nodeManager->mkSort("a"); + Type b = d_nodeManager->mkSort("b"); + Type c = d_nodeManager->mkSort("c"); - std::vector<Type*> types; + std::vector<Type> types; types.push_back(a); types.push_back(b); types.push_back(c); - Type *t = d_nodeManager->mkFunctionType(types); + Type t = d_nodeManager->mkFunctionType(types); TS_ASSERT( t != a ); TS_ASSERT( t != b ); TS_ASSERT( t != c ); - TS_ASSERT( t->isFunction() ); + TS_ASSERT( t.isFunction() ); - FunctionType* ft = (FunctionType*)t; - TS_ASSERT_EQUALS(ft->getArgTypes().size(), types.size()-1); - TS_ASSERT_EQUALS(ft->getArgTypes()[0], a); - TS_ASSERT_EQUALS(ft->getArgTypes()[1], b); - TS_ASSERT_EQUALS(ft->getRangeType(), c); + FunctionType ft = (FunctionType)t; + TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1); + TS_ASSERT_EQUALS(ft.getArgTypes()[0], a); + TS_ASSERT_EQUALS(ft.getArgTypes()[1], b); + TS_ASSERT_EQUALS(ft.getRangeType(), c); /* Type *t2 = d_nodeManager->mkFunctionType(types); TS_ASSERT_EQUALS( t, t2 );*/ } void testMkPredicateType() { - Type *a = d_nodeManager->mkSort("a"); - Type *b = d_nodeManager->mkSort("b"); - Type *c = d_nodeManager->mkSort("c"); - Type *booleanType = d_nodeManager->booleanType(); + Type a = d_nodeManager->mkSort("a"); + Type b = d_nodeManager->mkSort("b"); + Type c = d_nodeManager->mkSort("c"); + Type booleanType = d_nodeManager->booleanType(); - std::vector<Type*> argTypes; + std::vector<Type> argTypes; argTypes.push_back(a); argTypes.push_back(b); argTypes.push_back(c); - Type *t = d_nodeManager->mkPredicateType(argTypes); + Type t = d_nodeManager->mkPredicateType(argTypes); TS_ASSERT( t != a ); TS_ASSERT( t != b ); TS_ASSERT( t != c ); TS_ASSERT( t != booleanType ); - TS_ASSERT( t->isFunction() ); - - FunctionType* ft = (FunctionType*)t; - TS_ASSERT_EQUALS(ft->getArgTypes().size(), argTypes.size()); - TS_ASSERT_EQUALS(ft->getArgTypes()[0], a); - TS_ASSERT_EQUALS(ft->getArgTypes()[1], b); - TS_ASSERT_EQUALS(ft->getArgTypes()[2], c); - TS_ASSERT_EQUALS(ft->getRangeType(), booleanType); + TS_ASSERT( t.isFunction() ); + + FunctionType ft = (FunctionType)t; + TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size()); + TS_ASSERT_EQUALS(ft.getArgTypes()[0], a); + TS_ASSERT_EQUALS(ft.getArgTypes()[1], b); + TS_ASSERT_EQUALS(ft.getArgTypes()[2], c); + TS_ASSERT_EQUALS(ft.getRangeType(), booleanType); // Type *t2 = d_nodeManager->mkPredicateType(argTypes); // TS_ASSERT_EQUALS( t, t2 ); diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index 653e3a1d7..317817e15 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -146,17 +146,17 @@ class ParserWhite : public CxxTest::TestSuite { void setupContext(ParserState* parserState) { /* a, b, c: BOOLEAN */ - parserState->mkVar("a",(Type*)d_exprManager->booleanType()); - parserState->mkVar("b",(Type*)d_exprManager->booleanType()); - parserState->mkVar("c",(Type*)d_exprManager->booleanType()); + parserState->mkVar("a",d_exprManager->booleanType()); + parserState->mkVar("b",d_exprManager->booleanType()); + parserState->mkVar("c",d_exprManager->booleanType()); /* t, u, v: TYPE */ - Type *t = parserState->mkSort("t"); - Type *u = parserState->mkSort("u"); - Type *v = parserState->mkSort("v"); + Type t = parserState->mkSort("t"); + Type u = parserState->mkSort("u"); + Type v = parserState->mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ - parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); - parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); - parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t)); + parserState->mkVar("f", d_exprManager->mkFunctionType(t,u)); + parserState->mkVar("g", d_exprManager->mkFunctionType(u,v)); + parserState->mkVar("h", d_exprManager->mkFunctionType(v,t)); /* x:t; y:u; z:v; */ parserState->mkVar("x",t); parserState->mkVar("y",u); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 097724d48..25c22f196 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -211,8 +211,8 @@ public: void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); - Type* typeX = d_nm->booleanType(); - Type* typeF = d_nm->mkFunctionType(typeX, typeX); + Type typeX = d_nm->booleanType(); + Type typeF = d_nm->mkFunctionType(typeX, typeX); Node x = d_nm->mkVar("x",typeX); Node f = d_nm->mkVar("f",typeF); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index f5da06a0b..44b13c87c 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -107,10 +107,11 @@ public: d_outputChannel.clear(); d_euf = new TheoryUF(d_ctxt, d_outputChannel); - d_booleanType = d_nm->booleanType(); + d_booleanType = new Type(d_nm->booleanType()); } void tearDown() { + delete d_booleanType; delete d_euf; d_outputChannel.clear(); delete d_scope; @@ -119,8 +120,8 @@ public: } void testPushPopChain() { - Node x = d_nm->mkVar(d_booleanType); - Node f = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); + Node f = d_nm->mkVar(*d_booleanType); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); @@ -174,8 +175,8 @@ public: /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */ void testSimpleChain() { - Node x = d_nm->mkVar(d_booleanType); - Node f = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); + Node f = d_nm->mkVar(*d_booleanType); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); @@ -199,7 +200,7 @@ public: /* test that !(x == x) is inconsistent */ void testSelfInconsistent() { - Node x = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); Node x_neq_x = (x.eqNode(x)).notNode(); d_euf->assertFact(x_neq_x); @@ -212,7 +213,7 @@ public: /* test that (x == x) is consistent */ void testSelfConsistent() { - Node x = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); Node x_eq_x = x.eqNode(x); d_euf->assertFact(x_eq_x); @@ -228,8 +229,8 @@ public: f(x) != x } is inconsistent */ void testChain() { - Node x = d_nm->mkVar(d_booleanType); - Node f = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); + Node f = d_nm->mkVar(*d_booleanType); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); @@ -259,7 +260,7 @@ public: void testPushPopA() { - Node x = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); Node x_eq_x = x.eqNode(x); d_ctxt->push(); @@ -270,8 +271,8 @@ public: } void testPushPopB() { - Node x = d_nm->mkVar(d_booleanType); - Node f = d_nm->mkVar(d_booleanType); + Node x = d_nm->mkVar(*d_booleanType); + Node f = d_nm->mkVar(*d_booleanType); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_x_eq_x = f_x.eqNode(x); |