* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
Type booleanType = d_nodeManager->booleanType();
Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
FunctionType ft = (FunctionType)t;
Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP
Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.
I hate branching and merging.
<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>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
- <name>cvc4-antlr3</name>
+ <name>cvc4</name>
<comment></comment>
<projects>
</projects>
</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>
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 {
command.h \
command.cpp \
declaration_scope.h \
- declaration_scope.cpp
+ declaration_scope.cpp \
+ expr_manager_scope.h
EXTRA_DIST = \
@srcdir@/kind.h \
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);
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));
}
}
+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 */
#include "context/cdmap.h"
#include "expr/node.h"
-#include "expr/type.h"
#include "util/output.h"
// include supporting templates
/** 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 */
/** 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 */
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.
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) {
}
* @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 */
}
};
-/** 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;
}
};
}
};
-/** 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;
}
};
}
}
+/**
+ * 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 */
super::erase(nv);
}
+ /**
+ * Clear the hash table.
+ */
+ void clear() {
+ super::clear();
+ }
+
};/* class AttrHash<bool> */
/**
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"
#include <vector>
#include "expr/expr.h"
+#include "expr/type.h"
#include "util/result.h"
namespace CVC4 {
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 {
/* 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 */
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;
}
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);
}
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;
}
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. */
* @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.
*
* @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
--- /dev/null
+/*
+ * 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 */
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();
}
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) {
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) {
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,
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,
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,
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) {
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) {
~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,...).
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
* <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
* <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);
#include "util/Assert.h"
#include "util/output.h"
+#include "expr/expr_manager_scope.h"
${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;
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 {
/** 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.
#include "expr/kind.h"
#include "expr/metakind.h"
-#include "expr/type.h"
#include "util/Assert.h"
#include "util/output.h"
* Returns the type of this node.
* @return the type
*/
- Type* getType() const;
+ Type getType() const;
/**
* Returns the kind of this node.
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");
}
}
}
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 ?" );
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; "
}
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,
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
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. */
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
dealloc();
setUsed();
- return Node(poolNv);
+ return poolNv;
} else {
/* Subcase (b) The Node under construction is NOT already in the
* NodeManager's pool. */
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) {
__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;
}
};
}
};
+
+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
#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"
* 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
// 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();
}
// 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;
/**
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; }
/** 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
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.
* @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
* @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
* <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
* <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)
}
};
-/**
- * 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
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 {
}
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,
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;
}
#include "expr/node_manager.h"
#include "expr/type.h"
+#include "expr/type_constant.h"
#include "util/Assert.h"
#include <string>
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 */
#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;
/**
*/
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;
};
/**
*/
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 */
--- /dev/null
+/*
+ * 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_ */
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.
;
/** 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;
}
* 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 */
* 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;
/**
* 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;
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;
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));
}
}
-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]));
}
/**
* 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.
* @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);
/**
* 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? */
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
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 {
/**
* 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); })*
;
: identifier[name,check,SYM_SORT]
;
-sortSymbol returns [CVC4::Type* t]
+sortSymbol returns [CVC4::Type t]
@declarations {
std::string name;
}
#
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
}
Debug("rewrite") << "rewrote-children of " << in << std::endl
<< "got " << b << std::endl;
- return Node(b);
+ return b;
}
/**
rational.h \
rational.cpp \
integer.h \
- integer.cpp
+ integer.cpp \
+ bitvector.h \
+ bitvector.cpp \
+ gmp_util.h
--- /dev/null
+/*
+ * 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();
+}
+
+}
--- /dev/null
+/*
+ * 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_ */
--- /dev/null
+/*
+ * 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_ */
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();
}
#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 {
#ifndef __CVC4__RATIONAL_H
#define __CVC4__RATIONAL_H
-#include <gmpxx.h>
#include <string>
-#include "integer.h"
+#include "util/integer.h"
namespace CVC4 {
/**
* 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();
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;
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;
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));
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);
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);
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");
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;
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;
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);
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()));
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");
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") );
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);
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);
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);
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 );
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 );
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") );
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();
}
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() {
Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
- Type* d_booleanType;
+ 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();
+ d_booleanType = new Type(d_nodeManager->booleanType());
}
void tearDown() {
+ delete d_booleanType;
delete d_scope;
delete d_nodeManager;
delete d_ctxt;
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);
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)));
/*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);
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);
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());
}
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);
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
}
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);
}
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);
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;
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;
{
}
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);
}
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;
}
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);
}
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);
}
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)
* 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 );
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);
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);
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;
}
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);
/* 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);
/* 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);
/* 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);
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);
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();
}
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);
projects / cvc5.git / commitdiff