summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/attribute.cpp43
-rw-r--r--src/expr/attribute.h227
-rw-r--r--src/expr/expr.cpp2
-rw-r--r--src/expr/expr.h2
-rw-r--r--src/expr/expr_manager.cpp24
-rw-r--r--src/expr/expr_manager.h22
-rw-r--r--src/expr/node.h4
-rw-r--r--src/expr/node_manager.cpp18
-rw-r--r--src/expr/node_manager.h59
-rw-r--r--src/expr/type.cpp33
-rw-r--r--src/expr/type.h76
-rw-r--r--src/parser/antlr_parser.cpp93
-rw-r--r--src/parser/antlr_parser.h28
-rw-r--r--src/parser/cvc/cvc_parser.g50
-rw-r--r--src/parser/smt/smt_lexer.g4
-rw-r--r--src/parser/smt/smt_parser.g76
-rw-r--r--src/smt/smt_engine.cpp14
-rw-r--r--src/theory/interrupted.h11
-rw-r--r--src/theory/uf/theory_uf.h3
-rw-r--r--src/util/output.h9
20 files changed, 504 insertions, 294 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index e8e93f6ff..be54a973e 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -17,24 +17,43 @@
#include "expr/node_value.h"
#include "util/output.h"
+#include <utility>
+
+using namespace std;
+
namespace CVC4 {
namespace expr {
namespace attr {
+/**
+ * Search for the NodeValue in all attribute tables and remove it,
+ * calling the cleanup function if one is defined.
+ */
+template <class T>
+inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
+ NodeValue* nv) {
+ for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+ typedef AttributeTraits<T, false> traits_t;
+ typedef AttrHash<T> hash_t;
+ pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
+ if(traits_t::cleanup[id] != NULL) {
+ typename hash_t::iterator i = table.find(pr);
+ if(i != table.end()) {
+ traits_t::cleanup[id]((*i).second);
+ table.erase(pr);
+ }
+ } else {
+ table.erase(pr);
+ }
+ }
+}
+
void AttributeManager::deleteAllAttributes(NodeValue* nv) {
d_bools.erase(nv);
- for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, false>::s_id; ++id) {
- d_ints.erase(std::make_pair(id, nv));
- }
- for(unsigned id = 0; id < attr::LastAttributeId<TNode, false>::s_id; ++id) {
- d_exprs.erase(std::make_pair(id, nv));
- }
- for(unsigned id = 0; id < attr::LastAttributeId<std::string, false>::s_id; ++id) {
- d_strings.erase(std::make_pair(id, nv));
- }
- for(unsigned id = 0; id < attr::LastAttributeId<void*, false>::s_id; ++id) {
- d_ptrs.erase(std::make_pair(id, nv));
- }
+ deleteFromTable(d_ints, nv);
+ deleteFromTable(d_exprs, nv);
+ deleteFromTable(d_strings, nv);
+ deleteFromTable(d_ptrs, nv);
// FIXME CD-bools in optimized table
/*
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 4dc050648..62619e2b6 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -389,28 +389,139 @@ public:
namespace attr {
/** Default cleanup for unmanaged Attribute<> */
-template <class T>
-struct AttributeCleanupFcn {
- static inline void cleanup(const T&) {}
-};
+struct NullCleanupFcn {
+};/* struct NullCleanupFcn */
/** Default cleanup for ManagedAttribute<> */
template <class T>
struct ManagedAttributeCleanupFcn {
-};
+};/* struct ManagedAttributeCleanupFcn<> */
/** Specialization for T* */
template <class T>
struct ManagedAttributeCleanupFcn<T*> {
static inline void cleanup(T* p) { delete p; }
-};
+};/* struct ManagedAttributeCleanupFcn<T*> */
/** Specialization for const T* */
template <class T>
struct ManagedAttributeCleanupFcn<const T*> {
static inline void cleanup(const T* p) { delete p; }
+};/* struct ManagedAttributeCleanupFcn<const T*> */
+
+/**
+ * Helper for Attribute<> class below to determine whether a cleanup
+ * is defined or not.
+ */
+template <class T, class C>
+struct getCleanupFcn {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupFcn<> */
+
+/**
+ * Specialization for NullCleanupFcn.
+ */
+template <class T>
+struct getCleanupFcn<T, NullCleanupFcn> {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupFcn<T, NullCleanupFcn> */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupFcn<T, NullCleanupFcn>::fn)(typename getCleanupFcn<T, NullCleanupFcn>::mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<T>.
+ */
+template <class T>
+struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::fn)(typename getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<T*>.
+ */
+template <class T>
+struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > {
+ typedef T* value_type;
+ typedef ManagedAttributeCleanupFcn<value_type> C;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > */
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<const T*>.
+ */
+template <class T>
+struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > {
+ typedef const T* value_type;
+ typedef ManagedAttributeCleanupFcn<value_type> C;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > */
+
+/**
+ * Cause compile-time error for improperly-instantiated
+ * getCleanupFcn<>.
+ */
+template <class T, class U>
+struct getCleanupFcn<T, ManagedAttributeCleanupFcn<U> >;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner. IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct LastAttributeId {
+ static uint64_t s_id;
+};
+
+/** Initially zero. */
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TRAITS ============================================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner. IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct AttributeTraits {
+ typedef void (*cleanup_t)(T);
+ static std::vector<cleanup_t> cleanup;
};
+template <class T, bool context_dep>
+std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
+ AttributeTraits<T, context_dep>::cleanup;
+
}/* CVC4::expr::attr namespace */
// ATTRIBUTE DEFINITION ========================================================
@@ -431,9 +542,16 @@ struct ManagedAttributeCleanupFcn<const T*> {
*/
template <class T,
class value_t,
- class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
+ class CleanupFcn = attr::NullCleanupFcn,
bool context_dep = false>
-struct Attribute {
+class Attribute {
+ /**
+ * The unique ID associated to this attribute. Assigned statically,
+ * at load time.
+ */
+ static const uint64_t s_id;
+
+public:
/** The value type for this attribute. */
typedef value_t value_type;
@@ -454,20 +572,43 @@ struct Attribute {
*/
static const bool context_dependent = context_dep;
-private:
-
/**
- * The unique ID associated to this attribute. Assigned statically,
- * at load time.
+ * Register this attribute kind and check that the ID is a valid ID
+ * for bool-valued attributes. Fail an assert if not. Otherwise
+ * return the id.
*/
- static const uint64_t s_id;
+ static inline uint64_t registerAttribute() {
+ typedef typename attr::KindValueToTableValueMapping<value_t>::table_value_type table_value_type;
+ typedef attr::AttributeTraits<table_value_type, context_dep> traits;
+ uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
+ Assert(traits::cleanup.size() == id);// sanity check
+ traits::cleanup.push_back(attr::getCleanupFcn<value_t, CleanupFcn>::fn);
+ return id;
+ }
+};/* class Attribute<> */
+
+/**
+ * An "attribute type" structure for boolean flags (special). The
+ * full one is below; the existence of this one disallows for boolean
+ * flag attributes with a specialized cleanup function.
+ */
+/* -- doesn't work; other specialization is "more specific" ??
+template <class T, class CleanupFcn, bool context_dep>
+class Attribute<T, bool, CleanupFcn, context_dep> {
+ template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
+ ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
};
+*/
/**
* An "attribute type" structure for boolean flags (special).
*/
-template <class T, class CleanupFcn, bool context_dep>
-struct Attribute<T, bool, CleanupFcn, context_dep> {
+template <class T, bool context_dep>
+class Attribute<T, bool, attr::NullCleanupFcn, context_dep> {
+ /** IDs for bool-valued attributes are actually bit assignments. */
+ static const uint64_t s_id;
+
+public:
/** The value type for this attribute; here, bool. */
typedef bool value_type;
@@ -495,21 +636,18 @@ struct Attribute<T, bool, CleanupFcn, context_dep> {
static const bool context_dependent = context_dep;
/**
- * Check that the ID is a valid ID for bool-valued attributes. Fail
- * an assert if not. Otherwise return the id.
+ * Register this attribute kind and check that the ID is a valid ID
+ * for bool-valued attributes. Fail an assert if not. Otherwise
+ * return the id.
*/
- static inline uint64_t checkID(uint64_t id) {
+ static inline uint64_t registerAttribute() {
+ uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
AlwaysAssert( id <= 63,
"Too many boolean node attributes registered "
"during initialization !" );
return id;
}
-
-private:
-
- /** IDs for bool-valued attributes are actually bit assignments. */
- static const uint64_t s_id;
-};
+};/* class Attribute<..., bool, ...> */
/**
* This is a context-dependent attribute kind (the only difference
@@ -520,7 +658,7 @@ private:
template <class T,
class value_type>
struct CDAttribute :
- public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {};
+ public Attribute<T, value_type, attr::NullCleanupFcn, true> {};
/**
* This is a managed attribute kind (the only difference between
@@ -541,35 +679,21 @@ struct ManagedAttribute :
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
-namespace attr {
-
-/**
- * This is the last-attribute-assigner. IDs are not globally
- * unique; rather, they are unique for each table_value_type.
- */
-template <class T, bool context_dep>
-struct LastAttributeId {
- static uint64_t s_id;
-};
-
-/** Initially zero. */
-template <class T, bool context_dep>
-uint64_t LastAttributeId<T, context_dep>::s_id = 0;
-
-}/* CVC4::expr::attr namespace */
-
/** Assign unique IDs to attributes at load time. */
+// Use of the comma-operator here forces instantiation (and
+// initialization) of the AttributeTraits<> structure and its
+// "cleanup" vector before registerAttribute() is called. This is
+// important because otherwise the vector is initialized later,
+// clearing the first-pushed cleanup function.
template <class T, class value_t, class CleanupFcn, bool context_dep>
const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
- attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::s_id++;
+ ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
+ Attribute<T, value_t, CleanupFcn, context_dep>::registerAttribute() );
-/**
- * Assign unique IDs to bool-valued attributes at load time, checking
- * that they are in range.
- */
-template <class T, class CleanupFcn, bool context_dep>
-const uint64_t Attribute<T, bool, CleanupFcn, context_dep>::s_id =
- Attribute<T, bool, CleanupFcn, context_dep>::checkID(attr::LastAttributeId<bool, context_dep>::s_id++);
+/** Assign unique IDs to attributes at load time. */
+template <class T, bool context_dep>
+const uint64_t Attribute<T, bool, attr::NullCleanupFcn, context_dep>::s_id =
+ Attribute<T, bool, attr::NullCleanupFcn, context_dep>::registerAttribute();
// ATTRIBUTE MANAGER ===========================================================
@@ -609,6 +733,9 @@ class AttributeManager {
/** Underlying hash table for context-dependent pointer-valued attributes */
CDAttrHash<void*> d_cdptrs;
+ template <class T>
+ void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
+
/**
* getTable<> is a helper template that gets the right table from an
* AttributeManager given its type.
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 2f84f018b..6f611cf95 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -91,7 +91,7 @@ size_t Expr::getNumChildren() const {
return d_node->getNumChildren();
}
-const Type* Expr::getType() const {
+Type* Expr::getType() const {
ExprManagerScope ems(*this);
return d_node->getType();
}
diff --git a/src/expr/expr.h b/src/expr/expr.h
index b297be6fb..c5478b1da 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -106,7 +106,7 @@ public:
/** Returns the type of the expression, if it has been computed.
* Returns NULL if the type of the expression is not known.
*/
- const Type* getType() const;
+ Type* getType() const;
/**
* Returns the string representation of the expression.
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index f0a35e5f1..0b0139118 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -42,12 +42,12 @@ ExprManager::~ExprManager() {
delete d_ctxt;
}
-const BooleanType* ExprManager::booleanType() const {
+BooleanType* ExprManager::booleanType() const {
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->booleanType();
}
-const KindType* ExprManager::kindType() const {
+KindType* ExprManager::kindType() const {
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->kindType();
}
@@ -106,32 +106,30 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
}
/** Make a function type from domain to range. */
-const FunctionType*
-ExprManager::mkFunctionType(const Type* domain,
- const Type* range) {
+FunctionType* ExprManager::mkFunctionType(Type* domain,
+ Type* range) {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(domain,range);
+ return d_nodeManager->mkFunctionType(domain, range);
}
/** Make a function type with input types from argTypes. */
-const FunctionType*
-ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes,
- const Type* range) {
+FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range) {
NodeManagerScope nms(d_nodeManager);
- return d_nodeManager->mkFunctionType(argTypes,range);
+ return d_nodeManager->mkFunctionType(argTypes, range);
}
-const Type* ExprManager::mkSort(const std::string& name) {
+Type* ExprManager::mkSort(const std::string& name) {
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->mkSort(name);
}
-Expr ExprManager::mkVar(const Type* type, const std::string& name) {
+Expr ExprManager::mkVar(Type* type, const std::string& name) {
NodeManagerScope nms(d_nodeManager);
return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
}
-Expr ExprManager::mkVar(const Type* type) {
+Expr ExprManager::mkVar(Type* type) {
NodeManagerScope nms(d_nodeManager);
return Expr(this, new Node(d_nodeManager->mkVar(type)));
}
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index ff4e0db6b..3c73e1ced 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -51,10 +51,10 @@ public:
~ExprManager();
/** Get the type for booleans */
- const BooleanType* booleanType() const;
+ BooleanType* booleanType() const;
/** Get the type for sorts. */
- const KindType* kindType() const;
+ KindType* kindType() const;
/**
* Make a unary expression of a given kind (TRUE, FALSE,...).
@@ -95,21 +95,21 @@ public:
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
/** Make a function type from domain to range. */
- const FunctionType*
- mkFunctionType(const Type* domain,
- const Type* range);
+ FunctionType*
+ mkFunctionType(Type* domain,
+ Type* range);
/** Make a function type with input types from argTypes. */
- const FunctionType*
- mkFunctionType(const std::vector<const Type*>& argTypes,
- const Type* range);
+ FunctionType*
+ mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range);
/** Make a new sort with the given name. */
- const Type* mkSort(const std::string& name);
+ Type* mkSort(const std::string& name);
// variables are special, because duplicates are permitted
- Expr mkVar(const Type* type, const std::string& name);
- Expr mkVar(const Type* type);
+ Expr mkVar(Type* type, const std::string& name);
+ Expr mkVar(Type* type);
private:
/** The context */
diff --git a/src/expr/node.h b/src/expr/node.h
index d1bb8f3b3..25990cedf 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -240,7 +240,7 @@ public:
* Returns the type of this node.
* @return the type
*/
- const Type* getType() const;
+ Type* getType() const;
/**
* Returns the kind of this node.
@@ -707,7 +707,7 @@ bool NodeTemplate<ref_count>::hasOperator() const {
}
template <bool ref_count>
-const Type* NodeTemplate<ref_count>::getType() const {
+Type* NodeTemplate<ref_count>::getType() const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
"Perhaps a public-facing function is missing a NodeManagerScope ?" );
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7be593575..7b171a48b 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -25,9 +25,18 @@ namespace CVC4 {
__thread NodeManager* NodeManager::s_current = 0;
+NodeManager::~NodeManager() {
+ NodeManagerScope nms(this);
+ while(!d_zombies.empty()) {
+ reclaimZombies();
+ }
+
+ poolRemove( &expr::NodeValue::s_null );
+}
+
NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
- NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
- if(find == d_nodeValueSet.end()) {
+ NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
+ if(find == d_nodeValuePool.end()) {
return NULL;
} else {
return *find;
@@ -87,7 +96,7 @@ void NodeManager::reclaimZombies() {
NodeValue* nv = *i;
// collect ONLY IF still zero
- if((*i)->d_rc == 0) {
+ if(nv->d_rc == 0) {
Debug("gc") << "deleting node value " << nv
<< " [" << nv->d_id << "]: " << nv->toString() << "\n";
@@ -101,8 +110,7 @@ void NodeManager::reclaimZombies() {
// decr ref counts of children
nv->decrRefCounts();
- //free(nv);
-#warning NOT FREEING NODEVALUES
+ free(nv);
}
}
}
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b40ec2978..a3be61e48 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -30,6 +30,7 @@
#include "expr/expr.h"
#include "expr/node_value.h"
#include "context/context.h"
+#include "expr/type.h"
namespace CVC4 {
@@ -44,7 +45,7 @@ struct Type {};
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupFcn> TypeAttr;
}/* CVC4::expr namespace */
@@ -55,12 +56,12 @@ class NodeManager {
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueInternalHashFcn,
- expr::NodeValue::NodeValueEq> NodeValueSet;
+ expr::NodeValue::NodeValueEq> NodeValuePool;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueIDHashFcn,
expr::NodeValue::NodeValueEq> ZombieSet;
- NodeValueSet d_nodeValueSet;
+ NodeValuePool d_nodeValuePool;
expr::attr::AttributeManager d_attrManager;
@@ -108,6 +109,8 @@ public:
poolInsert( &expr::NodeValue::s_null );
}
+ ~NodeManager();
+
static NodeManager* currentNM() { return s_current; }
// general expression-builders
@@ -121,8 +124,8 @@ public:
Node mkNode(Kind kind, const std::vector<Node>& children);
// variables are special, because duplicates are permitted
- Node mkVar(const Type* type, const std::string& name);
- Node mkVar(const Type* type);
+ Node mkVar(Type* type, const std::string& name);
+ Node mkVar(Type* type);
Node mkVar();
template <class AttrKind>
@@ -172,27 +175,26 @@ public:
const typename AttrKind::value_type& value);
/** Get the type for booleans. */
- inline const BooleanType* booleanType() const {
+ inline BooleanType* booleanType() const {
return BooleanType::getInstance();
}
/** Get the type for sorts. */
- inline const KindType* kindType() const {
+ inline KindType* kindType() const {
return KindType::getInstance();
}
/** Make a function type from domain to range. */
- inline const FunctionType*
- mkFunctionType(const Type* domain, const Type* range) const;
+ inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
/** Make a function type with input types from argTypes. */
- inline const FunctionType*
- mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) const;
+ inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range) const;
/** Make a new sort with the given name. */
- inline const Type* mkSort(const std::string& name) const;
+ inline Type* mkSort(const std::string& name) const;
- inline const Type* getType(TNode n) const;
+ inline Type* getType(TNode n) const;
};
/**
@@ -308,41 +310,39 @@ inline void NodeManager::setAttribute(TNode n,
/** Make a function type from domain to range.
* TODO: Function types should be unique for this manager. */
-const FunctionType*
-NodeManager::mkFunctionType(const Type* domain,
- const Type* range) const {
- std::vector<const Type*> argTypes;
+FunctionType* NodeManager::mkFunctionType(Type* domain,
+ Type* range) const {
+ std::vector<Type*> argTypes;
argTypes.push_back(domain);
return new FunctionType(argTypes, range);
}
/** Make a function type with input types from argTypes.
* TODO: Function types should be unique for this manager. */
-const FunctionType*
-NodeManager::mkFunctionType(const std::vector<const Type*>& argTypes,
- const Type* range) const {
+FunctionType* NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
+ Type* range) const {
Assert( argTypes.size() > 0 );
return new FunctionType(argTypes, range);
}
-const Type*
-NodeManager::mkSort(const std::string& name) const {
+Type* NodeManager::mkSort(const std::string& name) const {
return new SortType(name);
}
-inline const Type* NodeManager::getType(TNode n) const {
+
+inline Type* NodeManager::getType(TNode n) const {
return getAttribute(n, CVC4::expr::TypeAttr());
}
inline void NodeManager::poolInsert(expr::NodeValue* nv) {
- Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(),
+ Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
"NodeValue already in the pool!");
- d_nodeValueSet.insert(nv);// FIXME multithreading
+ d_nodeValuePool.insert(nv);// FIXME multithreading
}
inline void NodeManager::poolRemove(expr::NodeValue* nv) {
- Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(),
+ Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
"NodeValue is not in the pool!");
- d_nodeValueSet.erase(nv);// FIXME multithreading
+ d_nodeValuePool.erase(nv);// FIXME multithreading
}
}/* CVC4 namespace */
@@ -382,14 +382,15 @@ inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
return NodeBuilder<>(this, kind).append(children);
}
-inline Node NodeManager::mkVar(const Type* type, const std::string& name) {
+inline Node NodeManager::mkVar(Type* type, const std::string& name) {
Node n = mkVar(type);
n.setAttribute(expr::VarNameAttr(), name);
return n;
}
-inline Node NodeManager::mkVar(const Type* type) {
+inline Node NodeManager::mkVar(Type* type) {
Node n = mkVar();
+ type->inc();// reference-count the type
n.setAttribute(expr::TypeAttr(), type);
return n;
}
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 4bdda6810..2549f02ca 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -26,11 +26,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) {
}
Type::Type() :
- d_name(std::string("<undefined>")) {
+ d_name(std::string("<undefined>")),
+ d_rc(0) {
}
Type::Type(std::string name) :
- d_name(name) {
+ d_name(name) {
}
std::string Type::getName() const {
@@ -39,7 +40,9 @@ std::string Type::getName() const {
BooleanType BooleanType::s_instance;
-BooleanType::BooleanType() : Type(std::string("BOOLEAN")) {
+BooleanType::BooleanType() :
+ Type(std::string("BOOLEAN")) {
+ d_rc = RC_MAX;// singleton, not heap-allocated
}
BooleanType::~BooleanType() {
@@ -54,22 +57,23 @@ bool BooleanType::isBoolean() const {
return true;
}
-FunctionType::FunctionType(const std::vector<const Type*>& argTypes,
- const Type* range)
- : d_argTypes(argTypes),
- d_rangeType(range) {
+FunctionType::FunctionType(const std::vector<Type*>& argTypes,
+ Type* range) :
+ d_argTypes(argTypes),
+ d_rangeType(range) {
+
Assert( argTypes.size() > 0 );
}
- // FIXME: What becomes of argument types?
+// FIXME: What becomes of argument types?
FunctionType::~FunctionType() {
}
-const std::vector<const Type*> FunctionType::getArgTypes() const {
+const std::vector<Type*> FunctionType::getArgTypes() const {
return d_argTypes;
}
-const Type* FunctionType::getRangeType() const {
+Type* FunctionType::getRangeType() const {
return d_rangeType;
}
@@ -100,7 +104,9 @@ void FunctionType::toStream(std::ostream& out) const {
KindType KindType::s_instance;
-KindType::KindType() : Type(std::string("KIND")) {
+KindType::KindType() :
+ Type(std::string("KIND")) {
+ d_rc = RC_MAX;// singleton, not heap-allocated
}
KindType::~KindType() {
@@ -115,12 +121,11 @@ KindType::getInstance() {
return &s_instance;
}
-SortType::SortType(std::string name)
- : Type(name) {
+SortType::SortType(std::string name) :
+ Type(name) {
}
SortType::~SortType() {
}
-
}
diff --git a/src/expr/type.h b/src/expr/type.h
index 7009ed504..fd9ea01d7 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -17,19 +17,32 @@
#define __CVC4__TYPE_H
#include "cvc4_config.h"
+#include "util/output.h"
+#include "util/Assert.h"
#include <string>
#include <vector>
+#include <limits.h>
namespace CVC4 {
+namespace expr {
+ namespace attr {
+ struct TypeCleanupFcn;
+ }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
class NodeManager;
/**
* Class encapsulating CVC4 expression types.
*/
class CVC4_PUBLIC Type {
+protected:
+ static const unsigned RC_MAX = UINT_MAX;
+
public:
+
/** Comparision for equality */
bool operator==(const Type& t) const;
@@ -72,11 +85,38 @@ protected:
/** Create a type with the given name. */
Type(std::string name);
- /** Destructor */
- virtual ~Type() { };
-
/** The name of the type (may be empty). */
std::string d_name;
+
+ /**
+ * The reference count for this Type (how many times it's referred
+ * to in the Type attribute table)
+ */
+ unsigned d_rc;
+
+ /** 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::TypeCleanupFcn;
};
/**
@@ -117,10 +157,10 @@ class FunctionType : public Type {
public:
/** Retrieve the argument types. The vector will be non-empty. */
- const std::vector<const Type*> getArgTypes() const;
+ const std::vector<Type*> getArgTypes() const;
/** Get the range type (i.e., the type of the result). */
- const Type* getRangeType() const;
+ Type* getRangeType() const;
/** Is this as function type? (Returns true.) */
bool isFunction() const;
@@ -141,17 +181,17 @@ private:
* @param argTypes a non-empty vector of input types
* @param range the result type
*/
- FunctionType(const std::vector<const Type*>& argTypes,
- const Type* range);
+ FunctionType(const std::vector<Type*>& argTypes,
+ Type* range);
/** Destructor */
~FunctionType();
/** The list of input types. */
- const std::vector<const Type*> d_argTypes;
+ const std::vector<Type*> d_argTypes;
/** The result type. */
- const Type* d_rangeType;
+ Type* d_rangeType;
friend class NodeManager;
};
@@ -211,6 +251,22 @@ private:
*/
std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
-}
+namespace expr {
+namespace attr {
+
+struct TypeCleanupFcn {
+ static void cleanup(Type* t) {
+ // reference-count the Type
+ t->dec();
+ if(t->d_rc == 0) {
+ delete t;
+ }
+ }
+};
+
+}/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
+}/* CVC4 namespace */
#endif /* __CVC4__TYPE_H */
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 593a89873..d20e59db3 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -60,7 +60,7 @@ Expr AntlrParser::getSymbol(const std::string& name, SymbolType type) {
return d_varSymbolTable.getObject(name);
default:
- Unhandled("Unhandled symbol type!");
+ Unhandled(type);
}
}
@@ -72,17 +72,16 @@ Expr AntlrParser::getFunction(const std::string& name) {
return getSymbol(name, SYM_FUNCTION);
}
-const Type*
-AntlrParser::getType(const std::string& var_name,
- SymbolType type) {
+Type* AntlrParser::getType(const std::string& var_name,
+ SymbolType type) {
Assert( isDeclared(var_name, type) );
- const Type* t = getSymbol(var_name,type).getType();
+ Type* t = getSymbol(var_name, type).getType();
return t;
}
-const Type* AntlrParser::getSort(const std::string& name) {
+Type* AntlrParser::getSort(const std::string& name) {
Assert( isDeclared(name, SYM_SORT) );
- const Type* t = d_sortTable.getObject(name);
+ Type* t = d_sortTable.getObject(name);
return t;
}
@@ -134,33 +133,30 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
return result;
}
-const Type*
-AntlrParser::functionType(const Type* domainType,
- const Type* rangeType) {
- return d_exprManager->mkFunctionType(domainType,rangeType);
+Type* AntlrParser::functionType(Type* domainType,
+ Type* rangeType) {
+ return d_exprManager->mkFunctionType(domainType, rangeType);
}
-const Type*
-AntlrParser::functionType(const std::vector<const Type*>& argTypes,
- const Type* rangeType) {
+Type* AntlrParser::functionType(const std::vector<Type*>& argTypes,
+ Type* rangeType) {
Assert( argTypes.size() > 0 );
- return d_exprManager->mkFunctionType(argTypes,rangeType);
+ return d_exprManager->mkFunctionType(argTypes, rangeType);
}
-const Type*
-AntlrParser::functionType(const std::vector<const Type*>& sorts) {
+Type* AntlrParser::functionType(const std::vector<Type*>& sorts) {
Assert( sorts.size() > 0 );
if( sorts.size() == 1 ) {
return sorts[0];
} else {
- std::vector<const Type*> argTypes(sorts);
- const Type* rangeType = argTypes.back();
+ std::vector<Type*> argTypes(sorts);
+ Type* rangeType = argTypes.back();
argTypes.pop_back();
- return functionType(argTypes,rangeType);
+ return functionType(argTypes, rangeType);
}
}
-const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
+Type* AntlrParser::predicateType(const std::vector<Type*>& sorts) {
if(sorts.size() == 0) {
return d_exprManager->booleanType();
} else {
@@ -168,17 +164,16 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
}
}
-Expr
-AntlrParser::mkVar(const std::string& name, const Type* type) {
+Expr AntlrParser::mkVar(const std::string& name, Type* type) {
Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
Expr expr = d_exprManager->mkVar(type, name);
- defineVar(name,expr);
+ defineVar(name, expr);
return expr;
}
-const std::vector<Expr>
-AntlrParser::mkVars(const std::vector<std::string> names,
- const Type* type) {
+const std::vector<Expr>
+AntlrParser::mkVars(const std::vector<std::string> names,
+ Type* type) {
std::vector<Expr> vars;
for(unsigned i = 0; i < names.size(); ++i) {
vars.push_back(mkVar(names[i], type));
@@ -186,55 +181,51 @@ AntlrParser::mkVars(const std::vector<std::string> names,
return vars;
}
-void
-AntlrParser::defineVar(const std::string& name, const Expr& val) {
+void AntlrParser::defineVar(const std::string& name, const Expr& val) {
Assert(!isDeclared(name));
- d_varSymbolTable.bindName(name,val);
+ d_varSymbolTable.bindName(name, val);
Assert(isDeclared(name));
}
-void
-AntlrParser::undefineVar(const std::string& name) {
+void AntlrParser::undefineVar(const std::string& name) {
Assert(isDeclared(name));
d_varSymbolTable.unbindName(name);
Assert(!isDeclared(name));
}
-const Type*
-AntlrParser::newSort(const std::string& name) {
+Type* AntlrParser::newSort(const std::string& name) {
Debug("parser") << "newSort(" << name << ")" << std::endl;
Assert( !isDeclared(name, SYM_SORT) );
- const Type* type = d_exprManager->mkSort(name);
+ Type* type = d_exprManager->mkSort(name);
d_sortTable.bindName(name, type);
Assert( isDeclared(name, SYM_SORT) );
return type;
}
-const std::vector<const Type*>
+const std::vector<Type*>
AntlrParser::newSorts(const std::vector<std::string>& names) {
- std::vector<const Type*> types;
+ std::vector<Type*> types;
for(unsigned i = 0; i < names.size(); ++i) {
types.push_back(newSort(names[i]));
}
return types;
}
-void
-AntlrParser::setLogic(const std::string& name) {
+void AntlrParser::setLogic(const std::string& name) {
if( name == "QF_UF" ) {
newSort("U");
} else {
- Unhandled("setLogic: " + name);
+ Unhandled(name);
}
}
-const BooleanType* AntlrParser::booleanType() {
- return d_exprManager->booleanType();
+BooleanType* AntlrParser::booleanType() {
+ return d_exprManager->booleanType();
}
-const KindType* AntlrParser::kindType() {
- return d_exprManager->kindType();
+KindType* AntlrParser::kindType() {
+ return d_exprManager->kindType();
}
unsigned int AntlrParser::minArity(Kind kind) {
@@ -251,7 +242,7 @@ unsigned int AntlrParser::minArity(Kind kind) {
return 1;
case APPLY:
- case EQUAL:
+ case EQUAL:
case IFF:
case IMPLIES:
case PLUS:
@@ -262,7 +253,7 @@ unsigned int AntlrParser::minArity(Kind kind) {
return 3;
default:
- Unhandled("kind in minArity");
+ Unhandled(kind);
}
}
@@ -277,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) {
case NOT:
return 1;
- case EQUAL:
+ case EQUAL:
case IFF:
case IMPLIES:
case XOR:
@@ -293,7 +284,7 @@ unsigned int AntlrParser::maxArity(Kind kind) {
return UINT_MAX;
default:
- Unhandled("kind in maxArity");
+ Unhandled(kind);
}
}
@@ -309,7 +300,7 @@ bool AntlrParser::isDeclared(const std::string& name, SymbolType type) {
case SYM_SORT:
return d_sortTable.isBound(name);
default:
- Unhandled("Unhandled symbol type!");
+ Unhandled(type);
}
}
@@ -345,7 +336,7 @@ void AntlrParser::checkDeclaration(const std::string& varName,
break;
default:
- Unhandled("Unknown check type!");
+ Unhandled(check);
}
}
@@ -353,7 +344,7 @@ void AntlrParser::checkFunction(const std::string& name)
throw (antlr::SemanticException) {
if( d_checksEnabled && !isFunction(name) ) {
parseError("Expecting function symbol, found '" + name + "'");
- }
+ }
}
void AntlrParser::checkArity(Kind kind, unsigned int numArgs)
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 94d919555..e970ebd52 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -137,7 +137,7 @@ protected:
/**
* Returns a sort, given a name
*/
- const Type* getSort(const std::string& sort_name);
+ Type* getSort(const std::string& sort_name);
/**
* Types of symbols. Used to define namespaces.
@@ -193,7 +193,7 @@ protected:
* @param name the symbol to lookup
* @param type the (namespace) type of the symbol
*/
- const Type* getType(const std::string& var_name,
+ Type* getType(const std::string& var_name,
SymbolType type = SYM_VARIABLE);
/**
@@ -244,13 +244,13 @@ protected:
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
/** Create a new CVC4 variable expression of the given type. */
- Expr mkVar(const std::string& name, const Type* type);
+ Expr mkVar(const std::string& name, 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,
- const Type* type);
+ Type* type);
/** Create a new variable definition (e.g., from a let binding). */
void defineVar(const std::string& name, const Expr& val);
@@ -258,12 +258,12 @@ protected:
void undefineVar(const std::string& name);
/** Returns a function type over the given domain and range types. */
- const Type* functionType(const Type* domain, const Type* range);
+ Type* functionType(Type* domain, Type* range);
/** Returns a function type over the given types. argTypes must be
non-empty. */
- const Type* functionType(const std::vector<const Type*>& argTypes,
- const Type* rangeType);
+ Type* functionType(const std::vector<Type*>& argTypes,
+ Type* rangeType);
/**
* Returns a function type over the given types. If types has only
@@ -271,7 +271,7 @@ protected:
*
* @param types a non-empty list of input and output types.
*/
- const Type* functionType(const std::vector<const Type*>& types);
+ Type* functionType(const std::vector<Type*>& types);
/**
* Returns a predicate type over the given sorts. If sorts is empty,
@@ -279,17 +279,17 @@ protected:
* @param sorts a list of input types
*/
- const Type* predicateType(const std::vector<const Type*>& sorts);
+ Type* predicateType(const std::vector<Type*>& sorts);
/**
* Creates a new sort with the given name.
*/
- const Type* newSort(const std::string& name);
+ Type* newSort(const std::string& name);
/**
* Creates a new sorts with the given names.
*/
- const std::vector<const Type*>
+ const std::vector<Type*>
newSorts(const std::vector<std::string>& names);
/** Is the symbol bound to a boolean variable? */
@@ -302,10 +302,10 @@ protected:
bool isPredicate(const std::string& name);
/** Returns the boolean type. */
- const BooleanType* booleanType();
+ BooleanType* booleanType();
/** Returns the kind type (i.e., the type of types). */
- const KindType* kindType();
+ KindType* kindType();
/** Returns the minimum arity of the given kind. */
static unsigned int minArity(Kind kind);
@@ -346,7 +346,7 @@ private:
SymbolTable<Expr> d_varSymbolTable;
/** The sort table */
- SymbolTable<const Type*> d_sortTable;
+ SymbolTable<Type*> d_sortTable;
/** Are semantic checks enabled during parsing? */
bool d_checksEnabled;
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 9492b36d9..55ae0ff73 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -89,15 +89,15 @@ command returns [CVC4::Command* cmd = 0]
declaration returns [CVC4::DeclarationCommand* cmd]
{
vector<string> ids;
- const Type* t;
+ Type* t;
Debug("parser") << "declaration: " << LT(1)->getText() << endl;
-}
+}
: identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON
{ cmd = new DeclarationCommand(ids,t); }
;
/** Match the right-hand side of a declaration. Returns the type. */
-declType[std::vector<std::string>& idList] returns [const CVC4::Type* t]
+declType[std::vector<std::string>& idList] returns [CVC4::Type* t]
{
Debug("parser") << "declType: " << LT(1)->getText() << endl;
}
@@ -111,9 +111,9 @@ declType[std::vector<std::string>& idList] returns [const CVC4::Type* t]
* Match the type in a declaration and do the declaration binding.
* TODO: Actually parse sorts into Type objects.
*/
-type returns [const CVC4::Type* t]
+type returns [CVC4::Type* t]
{
- const Type *t1, *t2;
+ Type *t1, *t2;
Debug("parser") << "type: " << LT(1)->getText() << endl;
}
: /* Simple type */
@@ -122,10 +122,10 @@ type returns [const CVC4::Type* t]
t1 = baseType RIGHT_ARROW t2 = baseType
{ t = functionType(t1,t2); }
| /* Multi-parameter function type */
- LPAREN t1 = baseType
- { std::vector<const Type*> argTypes;
+ LPAREN t1 = baseType
+ { std::vector<Type*> argTypes;
argTypes.push_back(t1); }
- (COMMA t1 = baseType { argTypes.push_back(t1); } )+
+ (COMMA t1 = baseType { argTypes.push_back(t1); } )+
RPAREN RIGHT_ARROW t2 = baseType
{ t = functionType(argTypes,t2); }
;
@@ -136,7 +136,7 @@ type returns [const CVC4::Type* t]
* @param idList the list to fill with identifiers.
* @param check what kinds of check to perform on the symbols
*/
-identifierList[std::vector<std::string>& idList,
+identifierList[std::vector<std::string>& idList,
DeclarationCheck check = CHECK_NONE]
{
string id;
@@ -150,10 +150,10 @@ identifierList[std::vector<std::string>& idList,
* Matches an identifier and returns a string.
*/
identifier[DeclarationCheck check = CHECK_NONE,
- SymbolType type = SYM_VARIABLE]
+ SymbolType type = SYM_VARIABLE]
returns [std::string id]
: x:IDENTIFIER
- { id = x->getText();
+ { id = x->getText();
checkDeclaration(id, check, type); }
;
@@ -161,7 +161,7 @@ returns [std::string id]
* Matches a type.
* TODO: parse more types
*/
-baseType returns [const CVC4::Type* t]
+baseType returns [CVC4::Type* t]
{
std::string id;
Debug("parser") << "base type: " << LT(1)->getText() << endl;
@@ -173,7 +173,7 @@ baseType returns [const CVC4::Type* t]
/**
* Matches a type identifier
*/
-typeSymbol returns [const CVC4::Type* t]
+typeSymbol returns [CVC4::Type* t]
{
std::string id;
Debug("parser") << "type symbol: " << LT(1)->getText() << endl;
@@ -228,7 +228,7 @@ impliesFormula returns [CVC4::Expr f]
Expr e;
Debug("parser") << "=> Formula: " << LT(1)->getText() << endl;
}
- : f = orFormula
+ : f = orFormula
( IMPLIES e = impliesFormula
{ f = mkExpr(CVC4::kind::IMPLIES, f, e); }
)?
@@ -259,7 +259,7 @@ xorFormula returns [CVC4::Expr f]
Debug("parser") << "XOR formula: " << LT(1)->getText() << endl;
}
: f = andFormula
- ( XOR e = andFormula
+ ( XOR e = andFormula
{ f = mkExpr(CVC4::kind::XOR,f, e); }
)*
;
@@ -289,7 +289,7 @@ notFormula returns [CVC4::Expr f]
Debug("parser") << "NOT formula: " << LT(1)->getText() << endl;
}
: /* negation */
- NOT f = notFormula
+ NOT f = notFormula
{ f = mkExpr(CVC4::kind::NOT, f); }
| /* a boolean atom */
f = predFormula
@@ -300,7 +300,7 @@ predFormula returns [CVC4::Expr f]
Debug("parser") << "predicate formula: " << LT(1)->getText() << endl;
}
: { Expr e; }
- f = term
+ f = term
(EQUAL e = term
{ f = mkExpr(CVC4::kind::EQUAL, f, e); }
)?
@@ -315,8 +315,8 @@ term returns [CVC4::Expr t]
Debug("parser") << "term: " << LT(1)->getText() << endl;
}
: /* function application */
- // { isFunction(LT(1)->getText()) }?
- { Expr f;
+ // { isFunction(LT(1)->getText()) }?
+ { Expr f;
std::vector<CVC4::Expr> args; }
f = functionSymbol[CHECK_DECLARED]
{ args.push_back( f ); }
@@ -343,16 +343,16 @@ term returns [CVC4::Expr t]
/**
* Parses an ITE term.
*/
-iteTerm returns [CVC4::Expr t]
+iteTerm returns [CVC4::Expr t]
{
Expr iteCondition, iteThen, iteElse;
Debug("parser") << "ite: " << LT(1)->getText() << endl;
}
- : IF iteCondition = formula
+ : IF iteCondition = formula
THEN iteThen = formula
iteElse = iteElseTerm
- ENDIF
- { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
+ ENDIF
+ { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); }
;
/**
@@ -379,8 +379,8 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f]
{
Debug("parser") << "function symbol: " << LT(1)->getText() << endl;
std::string name;
-}
+}
: name = identifier[check,SYM_FUNCTION]
- { checkFunction(name);
+ { checkFunction(name);
f = getFunction(name); }
;
diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index e3985818c..d694cd93f 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -115,11 +115,11 @@ C_IDENTIFIER options { paraphrase = "an attribute (e.g., ':x')"; testLiterals =
;
VAR_IDENTIFIER options { paraphrase = "a variable (e.g., '?x')"; testLiterals = false; }
- : '?' IDENTIFIER
+ : '?' IDENTIFIER
;
FUN_IDENTIFIER options { paraphrase = "a function variable (e.g, '$x')"; testLiterals = false; }
- : '$' IDENTIFIER
+ : '$' IDENTIFIER
;
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index d1ac50651..f9758dc5c 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -102,12 +102,12 @@ benchAttribute returns [Command* smt_command = 0]
{ smt_command = new AssertCommand(formula); }
| FORMULA_ATTR formula = annotatedFormula
{ smt_command = new CheckSatCommand(formula); }
- | STATUS_ATTR b_status = status
- { smt_command = new SetBenchmarkStatusCommand(b_status); }
- | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN
- | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
- | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN
- | NOTES_ATTR STRING_LITERAL
+ | STATUS_ATTR b_status = status
+ { smt_command = new SetBenchmarkStatusCommand(b_status); }
+ | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN
+ | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN
+ | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN
+ | NOTES_ATTR STRING_LITERAL
| annotation
;
@@ -119,12 +119,12 @@ annotatedFormula returns [CVC4::Expr formula]
{
Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
Kind kind = CVC4::kind::UNDEFINED_KIND;
- vector<Expr> args;
+ vector<Expr> args;
std::string name;
Expr expr1, expr2, expr3;
}
: /* a built-in operator application */
- LPAREN kind = builtinOp annotatedFormulas[args] RPAREN
+ LPAREN kind = builtinOp annotatedFormulas[args] RPAREN
{ checkArity(kind, args.size());
formula = mkExpr(kind,args); }
@@ -134,16 +134,16 @@ annotatedFormula returns [CVC4::Expr formula]
{ std::vector<Expr> diseqs;
for(unsigned i = 0; i < args.size(); ++i) {
for(unsigned j = i+1; j < args.size(); ++j) {
- diseqs.push_back(mkExpr(CVC4::kind::NOT,
+ diseqs.push_back(mkExpr(CVC4::kind::NOT,
mkExpr(CVC4::kind::EQUAL,args[i],args[j])));
}
}
formula = mkExpr(CVC4::kind::AND, diseqs); }
| /* An ite expression */
- LPAREN (ITE | IF_THEN_ELSE)
+ LPAREN (ITE | IF_THEN_ELSE)
{ Expr test, trueExpr, falseExpr; }
- test = annotatedFormula
+ test = annotatedFormula
trueExpr = annotatedFormula
falseExpr = annotatedFormula
RPAREN
@@ -164,12 +164,12 @@ annotatedFormula returns [CVC4::Expr formula]
formula=annotatedFormula
{ undefineVar(name); }
RPAREN
-
+
| /* A non-built-in function application */
// Semantic predicate not necessary if parenthesized subexpressions
// are disallowed
- // { isFunction(LT(2)->getText()) }?
+ // { isFunction(LT(2)->getText()) }?
{ Expr f; }
LPAREN f = functionSymbol
@@ -180,7 +180,7 @@ annotatedFormula returns [CVC4::Expr formula]
| /* a variable */
{ std::string name; }
- ( name = identifier[CHECK_DECLARED]
+ ( name = identifier[CHECK_DECLARED]
| name = variable[CHECK_DECLARED]
| name = function_var[CHECK_DECLARED] )
{ formula = getVariable(name); }
@@ -195,7 +195,7 @@ annotatedFormula returns [CVC4::Expr formula]
* Matches a sequence of annotaed formulas and puts them into the formulas
* vector.
* @param formulas the vector to fill with formulas
- */
+ */
annotatedFormulas[std::vector<Expr>& formulas]
{
Expr f;
@@ -222,7 +222,7 @@ builtinOp returns [CVC4::Kind kind]
;
/**
- * Matches a (possibly undeclared) predicate identifier (returning the string).
+ * Matches a (possibly undeclared) predicate identifier (returning the string).
* @param check what kind of check to do with the symbol
*/
predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
@@ -241,14 +241,14 @@ functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
* Matches an previously declared function symbol (returning an Expr)
*/
functionSymbol returns [CVC4::Expr fun]
-{
+{
string name;
}
: name = functionName[CHECK_DECLARED]
{ checkFunction(name);
fun = getFunction(name); }
;
-
+
/**
* Matches an attribute name from the input (:attribute_name).
*/
@@ -272,12 +272,12 @@ function_var[DeclarationCheck check = CHECK_NONE] returns [std::string name]
* Matches the sort symbol, which can be an arbitrary identifier.
* @param check the check to perform on the name
*/
-sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
- : name = identifier[check,SYM_SORT]
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+ : name = identifier[check,SYM_SORT]
;
-sortSymbol returns [const CVC4::Type* t]
-{
+sortSymbol returns [CVC4::Type* t]
+{
std::string name;
}
: name = sortName { t = getSort(name); }
@@ -286,47 +286,47 @@ sortSymbol returns [const CVC4::Type* t]
functionDeclaration
{
string name;
- const Type* t;
- std::vector<const Type*> sorts;
+ Type* t;
+ std::vector<Type*> sorts;
}
- : LPAREN name = functionName[CHECK_UNDECLARED]
+ : LPAREN name = functionName[CHECK_UNDECLARED]
t = sortSymbol // require at least one sort
{ sorts.push_back(t); }
sortList[sorts] RPAREN
{ t = functionType(sorts);
- mkVar(name, t); }
+ mkVar(name, t); }
;
-
+
/**
* Matches the declaration of a predicate and declares it
*/
predicateDeclaration
{
string p_name;
- std::vector<const Type*> p_sorts;
- const Type *t;
+ std::vector<Type*> p_sorts;
+ Type *t;
}
: LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN
{ t = predicateType(p_sorts);
- mkVar(p_name, t); }
+ mkVar(p_name, t); }
;
-sortDeclaration
+sortDeclaration
{
string name;
}
: name = sortName[CHECK_UNDECLARED]
{ newSort(name); }
;
-
+
/**
* Matches a sequence of sort symbols and fills them into the given vector.
*/
-sortList[std::vector<const Type*>& sorts]
+sortList[std::vector<Type*>& sorts]
{
- const Type* t;
+ Type* t;
}
- : ( t = sortSymbol { sorts.push_back(t); })*
+ : ( t = sortSymbol { sorts.push_back(t); })*
;
/**
@@ -350,11 +350,11 @@ annotation
* @param check what kinds of check to do on the symbol
* @return the id string
*/
-identifier[DeclarationCheck check = CHECK_NONE,
- SymbolType type = SYM_VARIABLE]
+identifier[DeclarationCheck check = CHECK_NONE,
+ SymbolType type = SYM_VARIABLE]
returns [std::string id]
{
- Debug("parser") << "identifier: " << LT(1)->getText()
+ Debug("parser") << "identifier: " << LT(1)->getText()
<< " check? " << toString(check)
<< " type? " << toString(type) << endl;
}
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c00112cd0..a55c146b8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -51,12 +51,12 @@ public:
* passes over the Node. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
- static Node preprocess(SmtEngine& smt, TNode node);
+ static Node preprocess(SmtEngine& smt, TNode n);
/**
* Adds a formula to the current context.
*/
- static void addFormula(SmtEngine& smt, TNode node);
+ static void addFormula(SmtEngine& smt, TNode n);
};/* class SmtEnginePrivate */
}/* namespace CVC4::smt */
@@ -97,8 +97,8 @@ void SmtEngine::doCommand(Command* c) {
c->invoke(this);
}
-Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) {
- return smt.d_theoryEngine->preprocess(e);
+Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) {
+ return smt.d_theoryEngine->preprocess(n);
}
Result SmtEngine::check() {
@@ -111,9 +111,9 @@ Result SmtEngine::quickCheck() {
return Result(Result::VALIDITY_UNKNOWN);
}
-void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode e) {
- Debug("smt") << "push_back assertion " << e << std::endl;
- smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, e));
+void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) {
+ Debug("smt") << "push_back assertion " << n << std::endl;
+ smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
}
Result SmtEngine::checkSat(const BoolExpr& e) {
diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h
index f7a269f0b..00afd3b2b 100644
--- a/src/theory/interrupted.h
+++ b/src/theory/interrupted.h
@@ -13,6 +13,8 @@
** The theory output channel interface.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY__INTERRUPTED_H
#define __CVC4__THEORY__INTERRUPTED_H
@@ -21,14 +23,7 @@
namespace CVC4 {
namespace theory {
-class CVC4_PUBLIC Interrupted : public CVC4::Exception {
-public:
-
- // Constructors
- Interrupted() : CVC4::Exception("CVC4::Theory::Interrupted") {}
- Interrupted(const std::string& msg) : CVC4::Exception(msg) {}
- Interrupted(const char* msg) : CVC4::Exception(msg) {}
-
+class Interrupted : public CVC4::Exception {
};/* class Interrupted */
}/* CVC4::theory namespace */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 128e28ca2..ccbfa327a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -183,7 +183,8 @@ private:
* a ECAttr is being destructed.
*/
struct ECCleanupFcn{
- static void cleanup(ECData* & ec){
+ static void cleanup(ECData* ec){
+ Debug("ufgc") << "cleaning up ECData " << ec << "\n";
ec->deleteSelf();
}
};
diff --git a/src/util/output.h b/src/util/output.h
index 5c265e699..77b755ad5 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -109,6 +109,9 @@ public:
void off(const char* tag) { d_tags.erase (std::string(tag)); }
void off(std::string tag) { d_tags.erase (tag); }
+ bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+ bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
void setStream(std::ostream& os) { d_os = &os; }
};/* class Debug */
@@ -241,6 +244,9 @@ public:
void off(const char* tag) { d_tags.erase (std::string(tag)); };
void off(std::string tag) { d_tags.erase (tag); };
+ bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+ bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
void setStream(std::ostream& os) { d_os = &os; }
};/* class Trace */
@@ -289,6 +295,9 @@ public:
void off(const char* tag) {}
void off(std::string tag) {}
+ bool isOn(const char* tag) { return false; }
+ bool isOn(std::string tag) { return false; }
+
void setStream(std::ostream& os) {}
};/* class NullDebugC */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback