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.
# 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
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'
/**
* A base class for NodeBuilders. When extending this class, use:
*
- * class MyExtendedNodeBuilder : public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
+ * class MyExtendedNodeBuilder :
+ * public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
*
* This ensures that certain member functions return the right
* (derived) class type.
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;
}
}
/** 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<true>();
}
/** 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<true>();
}
/** 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));
/** 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 &&
* 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();
}
/** Append a sequence of children to this Node-under-construction. */
- inline Builder& append(const std::vector<Node>& children) {
- Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ template <bool ref_count>
+ inline Builder&
+ append(const std::vector<NodeTemplate<ref_count> >& 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 <class Iterator>
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);
}
/** 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;
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);
}
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
- inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) :
+ inline BackedNodeBuilder(expr::NodeValue* buf,
+ unsigned maxChildren,
+ NodeManager* nm) :
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
*/
#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
// 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 <unsigned N>
friend class NodeBuilder;
template <class Builder>
inline Builder& NodeBuilderBase<Builder>::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 <class Builder>
// 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;
// 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;
// NON-CONST VERSION OF NODE EXTRACTOR
template <class Builder>
NodeBuilderBase<Builder>::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!");
// CONST VERSION OF NODE EXTRACTOR
template <class Builder>
NodeBuilderBase<Builder>::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!");
}
/**
- * 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;
}
};
// 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<NodeValue*> zombies;
zombies.reserve(d_zombies.size());
free(nv);
}
}
-}
+}/* NodeManager::reclaimZombies() */
}/* CVC4 namespace */
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<CVC4::Kind>(), 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
static NodeManager* currentNM() { return s_current; }
// general expression-builders
+
/** Create a node with no children. */
Node mkNode(Kind kind);
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<Node>& children);
-
- // NOTE: variables are special, because duplicates are permitted
+ template <bool ref_count>
+ Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& 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 <class T>
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<CVC4::Kind>() will yield k.
+ */
inline TNode operatorOf(Kind k) {
AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
"Kind is not an OPERATOR-kinded kind "
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.
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 <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+ * @returns <code>true</code> iff <code>attr</code> is set for
+ * <code>nv</code>.
*/
template <class AttrKind>
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.
* <code>value</code> will be set to the value of the attribute, if it is
- * set for <code>nv</code>; otherwise, it will be set to the default value of
- * the attribute.
- * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+ * set for <code>nv</code>; otherwise, it will be set to the default
+ * value of the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for
+ * <code>nv</code>.
*/
template <class AttrKind>
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 <code>attr</code> for <code>nv</code>
- */
+ /**
+ * 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 <code>attr</code> for <code>nv</code>
+ */
template <class AttrKind>
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.
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
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
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 <code>attr</code> for <code>n</code>
- */
+ /**
+ * 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 <code>attr</code> for <code>n</code>
+ */
template <class AttrKind>
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. <code>argTypes</code> 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<Type*>& argTypes,
Type* range) const;
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 <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.
+ * 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: 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:
};
template <class AttrKind>
-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());
}
}
template <class AttrKind>
-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 <class AttrKind>
-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 <class AttrKind>
-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 <class AttrKind>
-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 <class AttrKind>
-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 <class AttrKind>
-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);
}
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
}
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<Node>& children) {
+template <bool ref_count>
+inline Node NodeManager::mkNode(Kind kind,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
return NodeBuilder<>(this, kind).append(children);
}
}
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 <class T>
Node NodeManager::mkConst(const T& val) {
// typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
d_parserState->enableChecks();
}
-Command* Input::parseNextCommand() throw (ParserException) {
+Command* Input::parseNextCommand() throw(ParserException) {
Debug("parser") << "parseNextCommand()" << std::endl;
Command* cmd = NULL;
if(!done()) {
}
} 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()) {
d_parserState->setDone();
} catch(ParserException& e) {
d_parserState->setDone();
- throw ParserException(e.toString());
+ throw;
}
}
Debug("parser") << "parseNextExpression() => " << result << std::endl;
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),
// 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;
% 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
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=$?
typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> 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;
Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
+ Type* d_booleanType;
public:
d_ctxt = new Context;
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
+
+ d_booleanType = d_nm->booleanType();
}
void tearDown() {
//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()));
//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");
Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
+ Type* d_booleanType;
public:
d_ctxt = new Context;
d_nodeManager = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nodeManager);
+
+ d_booleanType = d_nodeManager->booleanType();
}
void tearDown() {
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);
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)));
/*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);
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);
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());
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
Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
+ Type* d_booleanType;
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() {
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;
{
}
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);
}
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;
using namespace std;
-
/**
* Very basic OutputChannel for testing simple Theory Behaviour.
* Stores a call sequence for the output channel
TheoryUF* d_euf;
+ Type* d_booleanType;
+
public:
TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {}
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
d_euf = new TheoryUF(d_ctxt, d_outputChannel);
+
+ d_booleanType = d_nm->booleanType();
}
void tearDown() {
}
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);
/* 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);
/* 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);
/* 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);
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);
void testPushPopA() {
- Node x = d_nm->mkVar();
+ Node x = d_nm->mkVar(d_booleanType);
Node x_eq_x = x.eqNode(x);
d_ctxt->push();
}
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);
projects / cvc5.git / commitdiff