From ff53861016427723a7c29e9bbca6f497b4556164 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 4 Apr 2010 23:03:52 +0000 Subject: [PATCH] * Addressed issues brought up in Chris's review of Morgan's NodeManager (bug #65). Better documentation, etc. * As part of this, removed NodeManager::mkVar() (which created a variable of unknown type). This requires changes to lots of unit tests, which were using this function. * Performed some review of parser code (my code review #73). + I changed the way exceptions were caught and rethrown in src/parser/input.cpp. + ParserExceptions weren't being properly constructed (d_line and d_column weren't intiialized and could contain junk, leading to weird error messages). Fixed. * Fix to the current working directory used by run_regression script. Makes exceptional output easier to match against (in expected error output). * (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we compile any C code and don't use the C++ compiler. --- configure.ac | 5 +- src/expr/node_builder.h | 76 ++++--- src/expr/node_manager.cpp | 30 +-- src/expr/node_manager.h | 295 ++++++++++++++++++++-------- src/parser/input.cpp | 8 +- src/parser/parser_exception.h | 28 ++- test/regress/regress0/error.cvc | 2 +- test/regress/run_regression | 12 +- test/unit/expr/attribute_black.h | 3 +- test/unit/expr/attribute_white.h | 17 +- test/unit/expr/node_black.h | 27 +-- test/unit/expr/node_builder_black.h | 27 +-- test/unit/theory/theory_uf_white.h | 27 +-- 13 files changed, 380 insertions(+), 177 deletions(-) diff --git a/configure.ac b/configure.ac index 7007ba47f..d23cf4a6d 100644 --- a/configure.ac +++ b/configure.ac @@ -165,7 +165,8 @@ fi # Unpack standard build types. Any particular options can be overriden with # --enable/disable-X options if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi -# our defaults for CXXFLAGS are better than autoconf's +# our defaults for CFLAGS/CXXFLAGS are better than autoconf's +if test -z "${CFLAGS+set}"; then CFLAGS=; fi if test -z "${CXXFLAGS+set}"; then CXXFLAGS=; fi case "$with_build" in production) # highly optimized, no assertions, no tracing @@ -477,7 +478,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS" CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" -CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated" +CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden' diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 213a4cb35..5c0cfb987 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -241,7 +241,8 @@ class MultNodeBuilder; /** * A base class for NodeBuilders. When extending this class, use: * - * class MyExtendedNodeBuilder : public NodeBuilderBase { ... }; + * class MyExtendedNodeBuilder : + * public NodeBuilderBase { ... }; * * This ensures that certain member functions return the right * (derived) class type. @@ -396,13 +397,14 @@ protected: expr::NodeValue* newBlock = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = d_nv->d_nchildren) )); + ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); if(newBlock == NULL) { // In this case, d_nv was NOT freed. If we throw, the // deallocation should occur on destruction of the // NodeBuilder. throw std::bad_alloc(); } + d_nvMaxChildren = d_nv->d_nchildren; d_nv = newBlock; } } @@ -446,37 +448,43 @@ public: /** Get the begin-const-iterator of this Node-under-construction. */ inline const_iterator begin() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); return d_nv->begin(); } /** Get the end-const-iterator of this Node-under-construction. */ inline const_iterator end() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); return d_nv->end(); } /** Get the kind of this Node-under-construction. */ inline Kind getKind() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); return d_nv->getKind(); } /** Get the kind of this Node-under-construction. */ inline kind::MetaKind getMetaKind() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); return d_nv->getMetaKind(); } /** Get the current number of children of this Node-under-construction. */ inline unsigned getNumChildren() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); return d_nv->getNumChildren(); } /** Access to children of this Node-under-construction. */ inline Node operator[](int i) const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(), "index out of range for NodeBuilder[]"); return Node(d_nv->getChild(i)); @@ -500,7 +508,8 @@ public: /** Set the Kind of this Node-under-construction. */ inline Builder& operator<<(const Kind& k) { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); Assert(getKind() == kind::UNDEFINED_KIND, "can't redefine the Kind of a NodeBuilder"); AssertArgument(k != kind::UNDEFINED_KIND && @@ -518,7 +527,8 @@ public: * on it but then never wrote code like that. */ Builder& operator<<(TNode n) { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); /* FIXME: disable this "collapsing" for now.. if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) { Node n2 = operator Node(); @@ -529,15 +539,19 @@ public: } /** Append a sequence of children to this Node-under-construction. */ - inline Builder& append(const std::vector& children) { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + template + inline Builder& + append(const std::vector >& children) { + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); return append(children.begin(), children.end()); } /** Append a sequence of children to this Node-under-construction. */ template Builder& append(const Iterator& begin, const Iterator& end) { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); for(Iterator i = begin; i != end; ++i) { append(*i); } @@ -546,7 +560,8 @@ public: /** Append a child to this Node-under-construction. */ Builder& append(TNode n) { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node"); allocateNvIfNecessaryForAppend(); expr::NodeValue* nv = n.d_nv; @@ -561,7 +576,8 @@ public: operator Node() const; inline void toStream(std::ostream& out, int depth = -1) const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + Assert(!isUsed(), "NodeBuilder is one-shot only; " + "attempt to access it after conversion"); d_nv->toStream(out, depth); } @@ -596,7 +612,9 @@ public: NodeBuilderBase(buf, maxChildren) { } - inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) : + inline BackedNodeBuilder(expr::NodeValue* buf, + unsigned maxChildren, + NodeManager* nm) : NodeBuilderBase(buf, maxChildren) { } @@ -627,8 +645,12 @@ private: */ #define makeStackNodeBuilder(__v, __n) \ const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n); \ - ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v[1 + (((sizeof(::CVC4::expr::NodeValue) + sizeof(::CVC4::expr::NodeValue*) + 1) / sizeof(::CVC4::expr::NodeValue*)) * __cvc4_backednodebuilder_nchildren__ ## __v)]; \ - ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \ + ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v \ + [1 + ( ( ( sizeof(::CVC4::expr::NodeValue) + \ + sizeof(::CVC4::expr::NodeValue*) + 1 ) / \ + sizeof(::CVC4::expr::NodeValue*) ) * \ + __cvc4_backednodebuilder_nchildren__ ## __v)]; \ + ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \ __cvc4_backednodebuilder_nchildren__ ## __v) // IF THE ABOVE ASSERTION FAILS, write another compiler-specific // version of makeStackNodeBuilder() that works for your compiler @@ -718,7 +740,8 @@ public: // we don't want a vtable, so do not declare a dtor! //inline ~NodeBuilder(); - // This is needed for copy constructors of different sizes to access private fields + // This is needed for copy constructors of different sizes to access + // private fields template friend class NodeBuilder; @@ -845,7 +868,8 @@ inline Builder& NodeBuilderBase::operator+=(TNode e) { template inline Builder& NodeBuilderBase::operator-=(TNode e) { - return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); + return collapseTo(kind::PLUS). + append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); } template @@ -1171,12 +1195,13 @@ void NodeBuilderBase::realloc(size_t toSize) { // Ensure d_nv is not modified on allocation failure expr::NodeValue* newBlock = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) )); + ( sizeof(expr::NodeValue*) * toSize )); if(newBlock == NULL) { // In this case, d_nv was NOT freed. If we throw, the // deallocation should occur on destruction of the NodeBuilder. throw std::bad_alloc(); } + d_nvMaxChildren = toSize; // Here, the copy (between two heap-allocated buffers) has already // been done for us by the std::realloc(). d_nv = newBlock; @@ -1184,10 +1209,11 @@ void NodeBuilderBase::realloc(size_t toSize) { // Ensure d_nv is not modified on allocation failure expr::NodeValue* newBlock = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) )); + ( sizeof(expr::NodeValue*) * toSize )); if(newBlock == NULL) { throw std::bad_alloc(); } + d_nvMaxChildren = toSize; d_nv = newBlock; d_nv->d_id = 0; @@ -1239,7 +1265,8 @@ void NodeBuilderBase::decrRefCounts() { // NON-CONST VERSION OF NODE EXTRACTOR template NodeBuilderBase::operator Node() { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + 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!"); @@ -1410,7 +1437,8 @@ NodeBuilderBase::operator Node() { // CONST VERSION OF NODE EXTRACTOR template NodeBuilderBase::operator Node() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion"); + 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!"); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8f254ed9f..e735b7f09 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -58,33 +58,41 @@ NodeManager::~NodeManager() { } /** - * This class ensure that NodeManager::d_reclaiming gets set to false + * This class ensures that NodeManager::d_reclaiming gets set to false * even on exceptional exit from NodeManager::reclaimZombies(). */ struct Reclaim { bool& d_reclaimField; + Reclaim(bool& reclaim) : d_reclaimField(reclaim) { Debug("gc") << ">> setting RECLAIM field\n"; d_reclaimField = true; } + ~Reclaim() { Debug("gc") << "<< clearing RECLAIM field\n"; d_reclaimField = false; } }; +/** + * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on + * exceptional exit from NodeManager::reclaimZombies(). + */ struct NVReclaim { - NodeValue*& d_reclaimField; - NVReclaim(NodeValue*& reclaim) : - d_reclaimField(reclaim) { + NodeValue*& d_deletionField; + + NVReclaim(NodeValue*& deletionField) : + d_deletionField(deletionField) { Debug("gc") << ">> setting NVRECLAIM field\n"; } + ~NVReclaim() { Debug("gc") << "<< clearing NVRECLAIM field\n"; - d_reclaimField = NULL; + d_deletionField = NULL; } }; @@ -107,11 +115,11 @@ void NodeManager::reclaimZombies() { // Let's say we're reclaiming zombie NodeValue "A" and its child "B" // then becomes a zombie (NodeManager::gc(B) is called). // - // One way to handle B's zombification is simply to put it into - // d_zombies. This is what we do. However, if we're currently - // processing d_zombies in the loop below, such addition may be - // invisible to us (B is leaked) or even invalidate our iterator, - // causing a crash. + // One way to handle B's zombification would be simply to put it + // into d_zombies. This is what we do. However, if we were to + // concurrently process d_zombies in the loop below, such addition + // may be invisible to us (B is leaked) or even invalidate our + // iterator, causing a crash. So we need to copy the set away. vector zombies; zombies.reserve(d_zombies.size()); @@ -149,6 +157,6 @@ void NodeManager::reclaimZombies() { free(nv); } } -} +}/* NodeManager::reclaimZombies() */ }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 71242f2e1..04d2ddac7 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -65,25 +65,100 @@ class NodeManager { expr::attr::AttributeManager d_attrManager; + /** + * The node value we're currently freeing. This unique node value + * is permitted to have outstanding TNodes to it (in "soft" + * contexts, like as a key in attribute tables), even though + * normally it's an error to have a TNode to a node value with a + * reference count of 0. Being "under deletion" also enables + * assertions that inc() is not called on it. (A poorly-behaving + * attribute cleanup function could otherwise create a "Node" that + * points to the node value that is in the process of being deleted, + * springing it back to life.) + */ expr::NodeValue* d_nodeUnderDeletion; + + /** + * True iff we are in reclaimZombies(). This avoids unnecessary + * recursion; a NodeValue being deleted might zombify other + * NodeValues, but these shouldn't trigger a (recursive) call to + * reclaimZombies(). + */ bool d_reclaiming; + + /** + * The set of zombie nodes. We may want to revisit this design, as + * we might like to delete nodes in least-recently-used order. But + * we also need to avoid processing a zombie twice. + */ ZombieSet d_zombies; + /** + * A set of operator singletons (w.r.t. to this NodeManager + * instance) for operators. Conceptually, Nodes with kind, say, + * PLUS, are APPLYs of a PLUS operator to arguments. This array + * holds the set of operators for these things. A PLUS operator is + * a Node with kind "BUILTIN", and if you call + * plusOperator->getConst(), you get kind::PLUS back. + */ + Node d_operators[kind::LAST_KIND]; + + /** + * Look up a NodeValue in the pool associated to this NodeManager. + * The NodeValue argument need not be a "completely-constructed" + * NodeValue. In particular, "non-inlined" constants are permited + * (see below). + * + * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be + * correctly set, and d_children[0..n-1] should be valid (extant) + * NodeValues for lookup. + * + * For CONSTANT metakinds, nv's d_kind should be set correctly. + * Normally a CONSTANT would have d_nchildren == 0 and the constant + * value inlined in the d_children space. However, here we permit + * "non-inlined" NodeValues to avoid unnecessary copying. For + * these, d_nchildren == 1, and d_nchildren is a pointer to the + * constant value. + * + * The point of this complex design is to permit efficient lookups + * (without fully constructing a NodeValue). In the case that the + * argument is not fully constructed, and this function returns + * NULL, the caller should fully construct an equivalent one before + * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not + * permitted in the pool! + */ inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const; - void poolInsert(expr::NodeValue* nv); + + /** + * Insert a NodeValue into the NodeManager's pool. + * + * It is an error to insert a NodeValue already in the pool. + * Enquire first with poolLookup(). + */ + inline void poolInsert(expr::NodeValue* nv); + + /** + * Remove a NodeValue from the NodeManager's pool. + * + * It is an error to request the removal of a NodeValue from the + * pool that is not in the pool. + */ inline void poolRemove(expr::NodeValue* nv); - bool isCurrentlyDeleting(const expr::NodeValue* nv) const{ + /** + * Determine if nv is currently being deleted by the NodeManager. + */ + inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const { return d_nodeUnderDeletion == nv; } - Node d_operators[kind::LAST_KIND]; - /** * Register a NodeValue as a zombie. */ inline void gc(expr::NodeValue* nv) { Assert(nv->d_rc == 0); + // if d_reclaiming is set, make sure we don't call + // reclaimZombies(), because it's already running. if(d_reclaiming) {// FIXME multithreading // currently reclaiming zombies; just push onto the list Debug("gc") << "zombifying node value " << nv @@ -169,6 +244,7 @@ public: static NodeManager* currentNM() { return s_current; } // general expression-builders + /** Create a node with no children. */ Node mkNode(Kind kind); @@ -182,33 +258,45 @@ public: Node mkNode(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 mkNode(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 mkNode(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); /** Create a node with an arbitrary number of children. */ - Node mkNode(Kind kind, const std::vector& children); - - // NOTE: variables are special, because duplicates are permitted + template + Node mkNode(Kind kind, const std::vector >& children); - /** Create a variable with the given type and name. */ + /** + * Create a variable with the given type and name. NOTE that no + * lookup is done on the name. If you mkVar(type, "a") and then + * mkVar(type, "a") again, you have two variables. + */ Node mkVar(Type* type, const std::string& name); /** Create a variable with the given type. */ Node mkVar(Type* type); - /** Create a variable of unknown type (?). */ - Node mkVar(); - - /** Create a constant of type T */ + /** + * Create a constant of type T. It will have the appropriate + * CONST_* kind defined for T. + */ template Node mkConst(const T&); - /** Determine whether Nodes of a particular Kind have operators. */ - static inline bool hasOperator(Kind mk); + /** + * Determine whether Nodes of a particular Kind have operators. + * @returns true if Nodes of Kind k have operators. + */ + static inline bool hasOperator(Kind k); - /** Get the (singleton) operator of an OPERATOR-kinded kind. */ + /** + * Get the (singleton) operator of an OPERATOR-kinded kind. The + * returned node n will have kind BUILTIN, and calling + * n.getConst() will yield k. + */ inline TNode operatorOf(Kind k) { AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k, "Kind is not an OPERATOR-kinded kind " @@ -216,7 +304,8 @@ public: return d_operators[k]; } - /** Retrieve an attribute for a node. + /** + * Retrieve an attribute for a node. * * @param nv the node value * @param attr an instance of the attribute kind to retrieve. @@ -227,43 +316,52 @@ public: inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, const AttrKind& attr) const; - /** Check whether an attribute is set for a node. + /** + * Check whether an attribute is set for a node. * * @param nv the node value * @param attr an instance of the attribute kind to check - * @returns true iff attr is set for nv. + * @returns true iff attr is set for + * nv. */ template inline bool hasAttribute(expr::NodeValue* nv, const AttrKind& attr) const; - /** Check whether an attribute is set for a node. + /** + * Check whether an attribute is set for a node, and, if so, + * retrieve it. * * @param nv the node value * @param attr an instance of the attribute kind to check * @param value a reference to an object of the attribute's value type. * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default value of - * the attribute. - * @returns true iff attr is set for nv. + * set for nv; otherwise, it will be set to the default + * value of the attribute. + * @returns true iff attr is set for + * nv. */ template inline bool getAttribute(expr::NodeValue* nv, const AttrKind& attr, typename AttrKind::value_type& value) const; - /** Set an attribute for a node. - * - * @param nv the node value - * @param attr an instance of the attribute kind to set - * @param value the value of attr for nv - */ + /** + * Set an attribute for a node. If the node doesn't have the + * attribute, this function assigns one. If the node has one, this + * overwrites it. + * + * @param nv the node value + * @param attr an instance of the attribute kind to set + * @param value the value of attr for nv + */ template inline void setAttribute(expr::NodeValue* nv, const AttrKind&, const typename AttrKind::value_type& value); - /** Retrieve an attribute for a TNode. + /** + * Retrieve an attribute for a TNode. * * @param n the node * @param attr an instance of the attribute kind to retrieve. @@ -274,12 +372,8 @@ public: inline typename AttrKind::value_type getAttribute(TNode n, const AttrKind&) const; - /* NOTE: there are two, distinct hasAttribute() declarations for - a reason (rather than using a pointer-valued argument with a - default value): they permit more optimized code in the underlying - hasAttribute() implementations. */ - - /** Check whether an attribute is set for a TNode. + /** + * Check whether an attribute is set for a TNode. * * @param n the node * @param attr an instance of the attribute kind to check @@ -289,7 +383,9 @@ public: inline bool hasAttribute(TNode n, const AttrKind& attr) const; - /** Check whether an attribute is set for a TNode. + /** + * Check whether an attribute is set for a TNode and, if so, retieve + * it. * * @param n the node * @param attr an instance of the attribute kind to check @@ -304,33 +400,46 @@ public: const AttrKind& attr, typename AttrKind::value_type& value) const; - /** Set an attribute for a TNode. - * - * @param n the node - * @param attr an instance of the attribute kind to set - * @param value the value of attr for n - */ + /** + * Set an attribute for a node. If the node doesn't have the + * attribute, this function assigns one. If the node has one, this + * overwrites it. + * + * @param n the node + * @param attr an instance of the attribute kind to set + * @param value the value of attr for n + */ template inline void setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value); - /** Get the type for booleans. */ + /** Get the (singleton) type for booleans. */ inline BooleanType* booleanType() const { return BooleanType::getInstance(); } - /** Get the type for sorts. */ + /** Get the (singleton) type for sorts. */ inline KindType* kindType() const { return KindType::getInstance(); } - /** Make a function type from domain to range. */ + /** + * Make a function type from domain to range. + * + * @param domain the domain type + * @param range the range type + * @returns the functional type domain -> range + */ inline FunctionType* mkFunctionType(Type* domain, Type* range) const; /** * Make a function type with input types from * argTypes. argTypes must have at least one element. + * + * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n]) + * @param range the range type + * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range */ inline FunctionType* mkFunctionType(const std::vector& argTypes, Type* range) const; @@ -399,24 +508,37 @@ public: NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) { NodeManager::s_current = nm; - Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; + Debug("current") << "node manager scope: " + << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n"; + Debug("current") << "node manager scope: " + << "returning to " << NodeManager::s_current << "\n"; } }; /** - * Creates - * a NodeManagerScope with the underlying NodeManager - * of a given Expr or ExprManager. - * The NodeManagerScope is destroyed when the ExprManagerScope - * is destroyed. See NodeManagerScope for more information. + * Creates a NodeManagerScope with the underlying + * NodeManager of a given Expr or + * ExprManager. The NodeManagerScope is + * destroyed when the ExprManagerScope is destroyed. See + * NodeManagerScope for more information. */ -// NOTE: Without this, we'd need Expr to be a friend of ExprManager. -// [chris 3/25/2010] Why? +// 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 it's 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: @@ -431,8 +553,8 @@ public: }; template -inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv, - const AttrKind&) const { +inline typename AttrKind::value_type +NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const { return d_attrManager.getAttribute(nv, AttrKind()); } @@ -443,42 +565,42 @@ inline bool NodeManager::hasAttribute(expr::NodeValue* nv, } template -inline bool NodeManager::getAttribute(expr::NodeValue* nv, - const AttrKind&, - typename AttrKind::value_type& ret) const { +inline bool +NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&, + typename AttrKind::value_type& ret) const { return d_attrManager.getAttribute(nv, AttrKind(), ret); } template -inline void NodeManager::setAttribute(expr::NodeValue* nv, - const AttrKind&, - const typename AttrKind::value_type& value) { +inline void +NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&, + const typename AttrKind::value_type& value) { d_attrManager.setAttribute(nv, AttrKind(), value); } template -inline typename AttrKind::value_type NodeManager::getAttribute(TNode n, - const AttrKind&) const { +inline typename AttrKind::value_type +NodeManager::getAttribute(TNode n, const AttrKind&) const { return d_attrManager.getAttribute(n.d_nv, AttrKind()); } template -inline bool NodeManager::hasAttribute(TNode n, - const AttrKind&) const { +inline bool +NodeManager::hasAttribute(TNode n, const AttrKind&) const { return d_attrManager.hasAttribute(n.d_nv, AttrKind()); } template -inline bool NodeManager::getAttribute(TNode n, - const AttrKind&, - typename AttrKind::value_type& ret) const { +inline bool +NodeManager::getAttribute(TNode n, const AttrKind&, + typename AttrKind::value_type& ret) const { return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret); } template -inline void NodeManager::setAttribute(TNode n, - const AttrKind&, - const typename AttrKind::value_type& value) { +inline void +NodeManager::setAttribute(TNode n, const AttrKind&, + const typename AttrKind::value_type& value) { d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } @@ -574,6 +696,7 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) { inline void NodeManager::poolRemove(expr::NodeValue* nv) { Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), "NodeValue is not in the pool!"); + d_nodeValuePool.erase(nv);// FIXME multithreading } @@ -620,20 +743,27 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { return NodeBuilder<>(this, kind) << child1 << child2; } -inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3) { return NodeBuilder<>(this, kind) << child1 << child2 << child3; } -inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4) { return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4; } -inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5; +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 + << child5; } // N-ary version -inline Node NodeManager::mkNode(Kind kind, const std::vector& children) { +template +inline Node NodeManager::mkNode(Kind kind, + const std::vector >& + children) { return NodeBuilder<>(this, kind).append(children); } @@ -644,17 +774,12 @@ inline Node NodeManager::mkVar(Type* type, const std::string& name) { } inline Node NodeManager::mkVar(Type* type) { - Node n = mkVar(); + Node n = Node(NodeBuilder<>(this, kind::VARIABLE)); type->inc();// reference-count the type n.setAttribute(TypeAttr(), type); return n; } -inline Node NodeManager::mkVar() { - // TODO: rewrite to not use NodeBuilder - return NodeBuilder<>(this, kind::VARIABLE); -} - template Node NodeManager::mkConst(const T& val) { // typedef typename kind::metakind::constantMap::OwningTheory theory_t; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 4d5f348d8..fd1a4cbd6 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -43,7 +43,7 @@ void Input::enableChecks() { d_parserState->enableChecks(); } -Command* Input::parseNextCommand() throw (ParserException) { +Command* Input::parseNextCommand() throw(ParserException) { Debug("parser") << "parseNextCommand()" << std::endl; Command* cmd = NULL; if(!done()) { @@ -54,14 +54,14 @@ Command* Input::parseNextCommand() throw (ParserException) { } } catch(ParserException& e) { d_parserState->setDone(); - throw ParserException(e.toString()); + throw; } } Debug("parser") << "parseNextCommand() => " << cmd << std::endl; return cmd; } -Expr Input::parseNextExpression() throw (ParserException) { +Expr Input::parseNextExpression() throw(ParserException) { Debug("parser") << "parseNextExpression()" << std::endl; Expr result; if(!done()) { @@ -71,7 +71,7 @@ Expr Input::parseNextExpression() throw (ParserException) { d_parserState->setDone(); } catch(ParserException& e) { d_parserState->setDone(); - throw ParserException(e.toString()); + throw; } } Debug("parser") << "parseNextExpression() => " << result << std::endl; diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 7b0f8bda9..dfca01ce2 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -30,9 +30,26 @@ namespace parser { class CVC4_PUBLIC ParserException : public Exception { public: // Constructors - ParserException() { } - ParserException(const std::string& msg): Exception(msg) { } - ParserException(const char* msg): Exception(msg) { } + ParserException() : + d_filename(), + d_line(0), + d_column(0) { + } + + ParserException(const std::string& msg) : + Exception(msg), + d_filename(), + d_line(0), + d_column(0) { + } + + ParserException(const char* msg) : + Exception(msg), + d_filename(), + d_line(0), + d_column(0) { + } + ParserException(const std::string& msg, const std::string& filename, unsigned long line, unsigned long column) : Exception(msg), @@ -43,11 +60,12 @@ public: // Destructor virtual ~ParserException() throw() {} + virtual std::string toString() const { if( d_line > 0 ) { std::stringstream ss; - ss << "Parser Error: " << d_filename << ":" << d_line << "." - << d_column << ": " << d_msg; + ss << "Parse Error: " << d_filename << ":" << d_line << "." + << d_column << ": " << d_msg; return ss.str(); } else { return "Parse Error: " + d_msg; diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index 09a69e212..982731b34 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,4 +1,4 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared +% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared p : BOOL; % EXIT: 1 diff --git a/test/regress/run_regression b/test/regress/run_regression index 65ab6c31a..439c8e6c9 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -77,7 +77,17 @@ else echo "$expected_error" >"$experrfile" fi -("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile" +cvc4dir=`dirname "$cvc4"` +cvc4dirfull=`cd "$cvc4dir" && pwd` +if [ -z "$cvc4dirfull" ]; then + error "getting directory of \`$cvc4 !?" +fi +cvc4base=`basename "$cvc4"` +cvc4full="$cvc4dirfull/$cvc4base" +( cd `dirname "$benchmark"`; + "$cvc4full" --segv-nospin `basename "$benchmark"`; + echo $? >"$exitstatusfile" +) > "$outfile" 2> "$errfile" diffs=`diff -u "$expoutfile" "$outfile"` diffexit=$? diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index eb728c62c..e87c8d708 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -70,7 +70,8 @@ public: typedef expr::Attribute MyDataAttribute; void testDeallocation() { - Node* node = new Node(d_nodeManager->mkVar()); + Type* booleanType = d_nodeManager->booleanType(); + Node* node = new Node(d_nodeManager->mkVar(booleanType)); MyData* data; MyData* data1; MyDataAttribute attr; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 64c768a13..e0d9d6bf4 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -60,6 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite { Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; + Type* d_booleanType; public: @@ -67,6 +68,8 @@ public: d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); + + d_booleanType = d_nm->booleanType(); } void tearDown() { @@ -150,9 +153,9 @@ public: //Debug.on("boolattr"); - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); + 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())); @@ -280,10 +283,10 @@ public: //Debug.on("boolattr"); - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - Node unnamed = d_nm->mkVar(); + 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/node_black.h b/test/unit/expr/node_black.h index d420c6e26..9e199aa9a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -36,6 +36,7 @@ private: Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; + Type* d_booleanType; public: @@ -43,6 +44,8 @@ public: d_ctxt = new Context; d_nodeManager = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nodeManager); + + d_booleanType = d_nodeManager->booleanType(); } void tearDown() { @@ -94,12 +97,12 @@ public: void testOperatorEquals() { Node a, b, c; - b = d_nodeManager->mkVar(); + b = d_nodeManager->mkVar(d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkVar(); + Node d = d_nodeManager->mkVar(d_booleanType); TS_ASSERT(a==a); TS_ASSERT(a==b); @@ -134,12 +137,12 @@ public: Node a, b, c; - b = d_nodeManager->mkVar(); + b = d_nodeManager->mkVar(d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkVar(); + Node d = d_nodeManager->mkVar(d_booleanType); /*structed assuming operator == works */ TS_ASSERT(iff(a!=a, !(a==a))); @@ -196,7 +199,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar()); + Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType)); b = c; TS_ASSERT(b==c); @@ -317,8 +320,8 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node a = d_nodeManager->mkVar(); - Node b = d_nodeManager->mkVar(); + 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); @@ -380,8 +383,8 @@ public: void testGetKind() { /*inline Kind getKind() const; */ - Node a = d_nodeManager->mkVar(); - Node b = d_nodeManager->mkVar(); + 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()); @@ -463,9 +466,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nodeManager->mkVar(); - Node y = d_nodeManager->mkVar(); - Node z = d_nodeManager->mkVar(); + 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 diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 2a7b3623e..eec6949f0 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -37,6 +37,7 @@ private: Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; + Type* d_booleanType; public: @@ -44,7 +45,9 @@ public: d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); + specKind = PLUS; + d_booleanType = d_nm->booleanType(); } void tearDown() { @@ -209,9 +212,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nm->mkVar(); - Node y = d_nm->mkVar(); - Node z = d_nm->mkVar(); + 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; { @@ -460,9 +463,9 @@ public: } void testAppend() { - Node x = d_nm->mkVar(); - Node y = d_nm->mkVar(); - Node z = d_nm->mkVar(); + 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); @@ -587,12 +590,12 @@ public: } void testConvenienceBuilders() { - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - Node d = d_nm->mkVar(); - Node e = d_nm->mkVar(); - Node f = d_nm->mkVar(); + 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/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index a204d79b7..369be5a16 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -31,7 +31,6 @@ using namespace CVC4::context; using namespace std; - /** * Very basic OutputChannel for testing simple Theory Behaviour. * Stores a call sequence for the output channel @@ -95,6 +94,8 @@ class TheoryUFWhite : public CxxTest::TestSuite { TheoryUF* d_euf; + Type* d_booleanType; + public: TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {} @@ -105,6 +106,8 @@ public: d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); d_euf = new TheoryUF(d_ctxt, d_outputChannel); + + d_booleanType = d_nm->booleanType(); } void tearDown() { @@ -116,8 +119,8 @@ public: } void testPushPopChain() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + 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); @@ -171,8 +174,8 @@ public: /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */ void testSimpleChain() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + 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); @@ -196,7 +199,7 @@ public: /* test that !(x == x) is inconsistent */ void testSelfInconsistent() { - Node x = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); Node x_neq_x = (x.eqNode(x)).notNode(); d_euf->assertFact(x_neq_x); @@ -209,7 +212,7 @@ public: /* test that (x == x) is consistent */ void testSelfConsistent() { - Node x = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); Node x_eq_x = x.eqNode(x); d_euf->assertFact(x_eq_x); @@ -225,8 +228,8 @@ public: f(x) != x } is inconsistent */ void testChain() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + 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); @@ -256,7 +259,7 @@ public: void testPushPopA() { - Node x = d_nm->mkVar(); + Node x = d_nm->mkVar(d_booleanType); Node x_eq_x = x.eqNode(x); d_ctxt->push(); @@ -267,8 +270,8 @@ public: } void testPushPopB() { - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); + 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); -- 2.30.2