summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/attribute.cpp37
-rw-r--r--src/expr/attribute.h173
-rw-r--r--src/expr/expr_manager_template.cpp16
-rw-r--r--src/expr/expr_manager_template.h13
-rw-r--r--src/expr/node.h2
-rw-r--r--src/expr/node_manager.cpp24
-rw-r--r--src/expr/node_manager.h10
-rw-r--r--src/smt/smt_engine.cpp14
-rw-r--r--src/smt/smt_engine.h18
-rw-r--r--src/theory/quantifiers/first_order_reasoning.cpp1
-rw-r--r--src/theory/quantifiers/macros.cpp1
-rw-r--r--test/unit/context/stacking_map_black.h4
-rw-r--r--test/unit/context/stacking_vector_black.h4
-rw-r--r--test/unit/expr/attribute_black.h20
-rw-r--r--test/unit/expr/attribute_white.h41
-rw-r--r--test/unit/expr/node_black.h6
-rw-r--r--test/unit/expr/node_builder_black.h7
-rw-r--r--test/unit/expr/node_manager_black.h7
-rw-r--r--test/unit/expr/node_manager_white.h7
-rw-r--r--test/unit/expr/node_self_iterator_black.h7
-rw-r--r--test/unit/expr/node_white.h7
-rw-r--r--test/unit/util/boolean_simplification_black.h7
22 files changed, 224 insertions, 202 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 2cd884bba..63ea770ca 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -17,6 +17,7 @@
#include "expr/attribute.h"
#include "expr/node_value.h"
#include "util/output.h"
+#include "smt/smt_engine.h"
#include <utility>
@@ -26,13 +27,16 @@ namespace CVC4 {
namespace expr {
namespace attr {
-AttributeManager::AttributeManager(context::Context* ctxt) :
+SmtAttributes::SmtAttributes(context::Context* ctxt) :
d_cdbools(ctxt),
d_cdints(ctxt),
d_cdtnodes(ctxt),
d_cdnodes(ctxt),
d_cdstrings(ctxt),
- d_cdptrs(ctxt),
+ d_cdptrs(ctxt) {
+}
+
+AttributeManager::AttributeManager() :
d_inGarbageCollection(false)
{}
@@ -40,6 +44,15 @@ bool AttributeManager::inGarbageCollection() const {
return d_inGarbageCollection;
}
+SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) {
+ Assert(smt != NULL);
+ return *smt->d_smtAttributes;
+}
+
+const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const {
+ return *smt->d_smtAttributes;
+}
+
void AttributeManager::debugHook(int debugFlag) {
/* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
* debugHook() is an empty function for the purpose of debugging
@@ -57,6 +70,10 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
deleteFromTable(d_types, nv);
deleteFromTable(d_strings, nv);
deleteFromTable(d_ptrs, nv);
+}
+
+void SmtAttributes::deleteAllAttributes(TNode n) {
+ NodeValue* nv = n.d_nv;
d_cdbools.erase(nv);
deleteFromTable(d_cdints, nv);
@@ -74,32 +91,25 @@ void AttributeManager::deleteAllAttributes() {
deleteAllFromTable(d_types);
deleteAllFromTable(d_strings);
deleteAllFromTable(d_ptrs);
-
- d_cdbools.clear();
- d_cdints.clear();
- d_cdtnodes.clear();
- d_cdnodes.clear();
- d_cdstrings.clear();
- d_cdptrs.clear();
}
-void AttributeManager::deleteAttributes(const AttrIdVec& atids){
+void AttributeManager::deleteAttributes(const AttrIdVec& atids) {
typedef std::map<uint64_t, std::vector< uint64_t> > AttrToVecMap;
AttrToVecMap perTableIds;
- for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it){
+ for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it) {
const AttributeUniqueId& pair = *(*it);
std::vector< uint64_t>& inTable = perTableIds[pair.getTableId()];
inTable.push_back(pair.getWithinTypeId());
}
AttrToVecMap::iterator it = perTableIds.begin(), it_end = perTableIds.end();
- for(; it != it_end; ++it){
+ for(; it != it_end; ++it) {
Assert(((*it).first) <= LastAttrTable);
AttrTableId tableId = (AttrTableId) ((*it).first);
std::vector< uint64_t>& ids = (*it).second;
std::sort(ids.begin(), ids.end());
- switch(tableId){
+ switch(tableId) {
case AttrTableBool:
Unimplemented("delete attributes is unimplemented for bools");
break;
@@ -130,6 +140,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids){
case AttrTableCDPointer:
Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired.");
break;
+
case LastAttrTable:
default:
Unreachable();
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 0bca760ef..432fbbac9 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -20,6 +20,7 @@
* attributes and nodes due to template use */
#include "expr/node.h"
#include "expr/type_node.h"
+#include "context/context.h"
#ifndef __CVC4__EXPR__ATTRIBUTE_H
#define __CVC4__EXPR__ATTRIBUTE_H
@@ -34,34 +35,20 @@
#undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+ extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
+}/* CVC4::smt namespace */
+
namespace expr {
namespace attr {
// ATTRIBUTE MANAGER ===========================================================
-/**
- * A container for the main attribute tables of the system. There's a
- * one-to-one NodeManager : AttributeManager correspondence.
- */
-class AttributeManager {
-
- // IF YOU ADD ANY TABLES, don't forget to add them also to the
- // implementation of deleteAllAttributes().
-
- /** Underlying hash table for boolean-valued attributes */
- AttrHash<bool> d_bools;
- /** Underlying hash table for integral-valued attributes */
- AttrHash<uint64_t> d_ints;
- /** Underlying hash table for node-valued attributes */
- AttrHash<TNode> d_tnodes;
- /** Underlying hash table for node-valued attributes */
- AttrHash<Node> d_nodes;
- /** Underlying hash table for types attributes */
- AttrHash<TypeNode> d_types;
- /** Underlying hash table for string-valued attributes */
- AttrHash<std::string> d_strings;
- /** Underlying hash table for pointer-valued attributes */
- AttrHash<void*> d_ptrs;
+struct SmtAttributes {
+ SmtAttributes(context::Context*);
// IF YOU ADD ANY TABLES, don't forget to add them also to the
// implementation of deleteAllAttributes().
@@ -79,12 +66,23 @@ 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);
+ /** Delete all attributes of given node */
+ void deleteAllAttributes(TNode n);
template <class T>
void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv);
+};/* struct SmtAttributes */
+
+/**
+ * A container for the main attribute tables of the system. There's a
+ * one-to-one NodeManager : AttributeManager correspondence.
+ */
+class AttributeManager {
+
+ template <class T>
+ void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
+
template <class T>
void deleteAllFromTable(AttrHash<T>& table);
@@ -105,10 +103,31 @@ class AttributeManager {
void clearDeleteAllAttributesBuffer();
+ SmtAttributes& getSmtAttributes(SmtEngine*);
+ const SmtAttributes& getSmtAttributes(SmtEngine*) const;
+
public:
/** Construct an attribute manager. */
- AttributeManager(context::Context* ctxt);
+ AttributeManager();
+
+ // IF YOU ADD ANY TABLES, don't forget to add them also to the
+ // implementation of deleteAllAttributes().
+
+ /** Underlying hash table for boolean-valued attributes */
+ AttrHash<bool> d_bools;
+ /** Underlying hash table for integral-valued attributes */
+ AttrHash<uint64_t> d_ints;
+ /** Underlying hash table for node-valued attributes */
+ AttrHash<TNode> d_tnodes;
+ /** Underlying hash table for node-valued attributes */
+ AttrHash<Node> d_nodes;
+ /** Underlying hash table for types attributes */
+ AttrHash<TypeNode> d_types;
+ /** Underlying hash table for string-valued attributes */
+ AttrHash<std::string> d_strings;
+ /** Underlying hash table for pointer-valued attributes */
+ AttrHash<void*> d_ptrs;
/**
* Get a particular attribute on a particular node.
@@ -220,10 +239,10 @@ template <>
struct getTable<bool, false> {
static const AttrTableId id = AttrTableBool;
typedef AttrHash<bool> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_bools;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_bools;
}
};
@@ -233,10 +252,10 @@ template <>
struct getTable<uint64_t, false> {
static const AttrTableId id = AttrTableUInt64;
typedef AttrHash<uint64_t> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_ints;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_ints;
}
};
@@ -246,10 +265,10 @@ template <>
struct getTable<TNode, false> {
static const AttrTableId id = AttrTableTNode;
typedef AttrHash<TNode> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_tnodes;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_tnodes;
}
};
@@ -259,10 +278,10 @@ template <>
struct getTable<Node, false> {
static const AttrTableId id = AttrTableNode;
typedef AttrHash<Node> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_nodes;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_nodes;
}
};
@@ -272,10 +291,10 @@ template <>
struct getTable<TypeNode, false> {
static const AttrTableId id = AttrTableTypeNode;
typedef AttrHash<TypeNode> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_types;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_types;
}
};
@@ -285,10 +304,10 @@ template <>
struct getTable<std::string, false> {
static const AttrTableId id = AttrTableString;
typedef AttrHash<std::string> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_strings;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_strings;
}
};
@@ -298,10 +317,10 @@ template <class T>
struct getTable<T*, false> {
static const AttrTableId id = AttrTablePointer;
typedef AttrHash<void*> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_ptrs;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_ptrs;
}
};
@@ -311,10 +330,10 @@ template <class T>
struct getTable<const T*, false> {
static const AttrTableId id = AttrTablePointer;
typedef AttrHash<void*> table_type;
- static inline table_type& get(AttributeManager& am) {
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
return am.d_ptrs;
}
- static inline const table_type& get(const AttributeManager& am) {
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
return am.d_ptrs;
}
};
@@ -324,11 +343,11 @@ template <>
struct getTable<bool, true> {
static const AttrTableId id = AttrTableCDBool;
typedef CDAttrHash<bool> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdbools;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdbools;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdbools;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdbools;
}
};
@@ -337,11 +356,11 @@ template <>
struct getTable<uint64_t, true> {
static const AttrTableId id = AttrTableCDUInt64;
typedef CDAttrHash<uint64_t> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdints;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdints;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdints;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdints;
}
};
@@ -350,11 +369,11 @@ template <>
struct getTable<TNode, true> {
static const AttrTableId id = AttrTableCDTNode;
typedef CDAttrHash<TNode> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdtnodes;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdtnodes;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdtnodes;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdtnodes;
}
};
@@ -363,11 +382,11 @@ template <>
struct getTable<Node, true> {
static const AttrTableId id = AttrTableCDNode;
typedef CDAttrHash<Node> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdnodes;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdnodes;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdnodes;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdnodes;
}
};
@@ -376,11 +395,11 @@ template <>
struct getTable<std::string, true> {
static const AttrTableId id = AttrTableCDString;
typedef CDAttrHash<std::string> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdstrings;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdstrings;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdstrings;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdstrings;
}
};
@@ -389,11 +408,11 @@ template <class T>
struct getTable<T*, true> {
static const AttrTableId id = AttrTableCDPointer;
typedef CDAttrHash<void*> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdptrs;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdptrs;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdptrs;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdptrs;
}
};
@@ -402,11 +421,11 @@ template <class T>
struct getTable<const T*, true> {
static const AttrTableId id = AttrTableCDPointer;
typedef CDAttrHash<void*> table_type;
- static inline table_type& get(AttributeManager& am) {
- return am.d_cdptrs;
+ static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdptrs;
}
- static inline const table_type& get(const AttributeManager& am) {
- return am.d_cdptrs;
+ static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+ return am.getSmtAttributes(smt).d_cdptrs;
}
};
@@ -426,7 +445,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
table_type table_type;
const table_type& ah =
- getTable<value_type, AttrKind::context_dependent>::get(*this);
+ getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
typename table_type::const_iterator i =
ah.find(std::make_pair(AttrKind::getId(), nv));
@@ -469,7 +488,7 @@ struct HasAttribute<true, AttrKind> {
table_type;
const table_type& ah =
- getTable<value_type, AttrKind::context_dependent>::get(*am);
+ getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
typename table_type::const_iterator i =
ah.find(std::make_pair(AttrKind::getId(), nv));
@@ -497,7 +516,7 @@ struct HasAttribute<false, AttrKind> {
table_type table_type;
const table_type& ah =
- getTable<value_type, AttrKind::context_dependent>::get(*am);
+ getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
typename table_type::const_iterator i =
ah.find(std::make_pair(AttrKind::getId(), nv));
@@ -517,7 +536,7 @@ struct HasAttribute<false, AttrKind> {
table_type table_type;
const table_type& ah =
- getTable<value_type, AttrKind::context_dependent>::get(*am);
+ getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
typename table_type::const_iterator i =
ah.find(std::make_pair(AttrKind::getId(), nv));
@@ -557,7 +576,7 @@ AttributeManager::setAttribute(NodeValue* nv,
table_type table_type;
table_type& ah =
- getTable<value_type, AttrKind::context_dependent>::get(*this);
+ getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
}
@@ -590,8 +609,8 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
* Obliterate a NodeValue from a (context-dependent) attribute table.
*/
template <class T>
-inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
- NodeValue* nv) {
+inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table,
+ NodeValue* nv) {
for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) {
table.obliterate(std::make_pair(id, nv));
}
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 8bcfd58ba..fb9da3e37 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -17,7 +17,6 @@
#include "expr/node_manager.h"
#include "expr/expr_manager.h"
#include "expr/variable_type_map.h"
-#include "context/context.h"
#include "options/options.h"
#include "util/statistics_registry.h"
@@ -29,7 +28,7 @@ ${includes}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 33 "${template}"
+#line 32 "${template}"
#ifdef CVC4_STATISTICS_ON
#define INC_STAT(kind) \
@@ -64,14 +63,12 @@ ${includes}
#endif
using namespace std;
-using namespace CVC4::context;
using namespace CVC4::kind;
namespace CVC4 {
ExprManager::ExprManager() :
- d_ctxt(new Context()),
- d_nodeManager(new NodeManager(d_ctxt, this)) {
+ d_nodeManager(new NodeManager(this)) {
#ifdef CVC4_STATISTICS_ON
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
d_exprStatistics[i] = NULL;
@@ -83,8 +80,7 @@ ExprManager::ExprManager() :
}
ExprManager::ExprManager(const Options& options) :
- d_ctxt(new Context()),
- d_nodeManager(new NodeManager(d_ctxt, this, options)) {
+ d_nodeManager(new NodeManager(this, options)) {
#ifdef CVC4_STATISTICS_ON
for (unsigned i = 0; i < LAST_TYPE; ++ i) {
d_exprStatisticsVars[i] = NULL;
@@ -119,8 +115,6 @@ ExprManager::~ExprManager() throw() {
delete d_nodeManager;
d_nodeManager = NULL;
- delete d_ctxt;
- d_ctxt = NULL;
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << std::endl
@@ -962,10 +956,6 @@ NodeManager* ExprManager::getNodeManager() const {
return d_nodeManager;
}
-Context* ExprManager::getContext() const {
- return d_ctxt;
-}
-
Statistics ExprManager::getStatistics() const throw() {
return Statistics(*d_nodeManager->getStatisticsRegistry());
}
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 49094c593..deb2f6918 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -52,19 +52,12 @@ namespace expr {
}/* CVC4::expr::pickle namespace */
}/* CVC4::expr namespace */
-namespace context {
- class Context;
-}/* CVC4::context namespace */
-
namespace stats {
StatisticsRegistry* getStatisticsRegistry(ExprManager*);
}/* CVC4::stats namespace */
class CVC4_PUBLIC ExprManager {
private:
- /** The context */
- context::Context* d_ctxt;
-
/** The internal node manager */
NodeManager* d_nodeManager;
@@ -79,12 +72,6 @@ private:
NodeManager* getNodeManager() const;
/**
- * Returns the internal Context. Used by internal users, i.e. the
- * friend classes.
- */
- context::Context* getContext() const;
-
- /**
* Check some things about a newly-created DatatypeType.
*/
void checkResolvedDatatype(DatatypeType dtt) const;
diff --git a/src/expr/node.h b/src/expr/node.h
index 35f94b9e3..9f0eaf3cd 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -149,6 +149,7 @@ class NodeValue;
namespace attr {
class AttributeManager;
+ class SmtAttributes;
}/* CVC4::expr::attr namespace */
class ExprSetDepth;
@@ -214,6 +215,7 @@ class NodeTemplate {
friend class NodeBuilder;
friend class ::CVC4::expr::attr::AttributeManager;
+ friend class ::CVC4::expr::attr::SmtAttributes;
friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fb1284d0d..31b17ccda 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -80,12 +80,11 @@ struct NVReclaim {
}
};
-NodeManager::NodeManager(context::Context* ctxt,
- ExprManager* exprManager) :
+NodeManager::NodeManager(ExprManager* exprManager) :
d_options(new Options()),
d_statisticsRegistry(new StatisticsRegistry()),
next_id(0),
- d_attrManager(new expr::attr::AttributeManager(ctxt)),
+ d_attrManager(new expr::attr::AttributeManager()),
d_exprManager(exprManager),
d_nodeUnderDeletion(NULL),
d_inReclaimZombies(false),
@@ -94,13 +93,12 @@ NodeManager::NodeManager(context::Context* ctxt,
init();
}
-NodeManager::NodeManager(context::Context* ctxt,
- ExprManager* exprManager,
+NodeManager::NodeManager(ExprManager* exprManager,
const Options& options) :
d_options(new Options(options)),
d_statisticsRegistry(new StatisticsRegistry()),
next_id(0),
- d_attrManager(new expr::attr::AttributeManager(ctxt)),
+ d_attrManager(new expr::attr::AttributeManager()),
d_exprManager(exprManager),
d_nodeUnderDeletion(NULL),
d_inReclaimZombies(false),
@@ -129,6 +127,8 @@ NodeManager::~NodeManager() {
{
ScopedBool dontGC(d_inReclaimZombies);
+ // hopefully by this point all SmtEngines have been deleted
+ // already, along with all their attributes
d_attrManager->deleteAllAttributes();
}
@@ -229,6 +229,18 @@ void NodeManager::reclaimZombies() {
d_nodeUnderDeletion = nv;
// remove attributes
+ { // notify listeners of deleted node
+ TNode n;
+ n.d_nv = nv;
+ nv->d_rc = 1; // so that TNode doesn't assert-fail
+ for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyDeleteNode(n);
+ }
+ // this would mean that one of the listeners stowed away
+ // a reference to this node!
+ Assert(nv->d_rc == 1);
+ }
+ nv->d_rc = 0;
d_attrManager->deleteAllAttributes(nv);
// decr ref counts of children
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0aa222294..d4d89109c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -35,7 +35,6 @@
#include "expr/kind.h"
#include "expr/metakind.h"
#include "expr/node_value.h"
-#include "context/context.h"
#include "util/subrange_bound.h"
#include "util/tls.h"
#include "options/options.h"
@@ -66,6 +65,11 @@ public:
virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
+ /**
+ * Notify a listener of a Node that's being GCed. If this function stores a reference
+ * to the Node somewhere, very bad things will happen.
+ */
+ virtual void nmNotifyDeleteNode(TNode n) { }
};/* class NodeManagerListener */
class NodeManager {
@@ -307,8 +311,8 @@ class NodeManager {
public:
- explicit NodeManager(context::Context* ctxt, ExprManager* exprManager);
- explicit NodeManager(context::Context* ctxt, ExprManager* exprManager, const Options& options);
+ explicit NodeManager(ExprManager* exprManager);
+ explicit NodeManager(ExprManager* exprManager, const Options& options);
~NodeManager();
/** The node manager in the current public-facing CVC4 library context */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ea48cb3d0..a69952885 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -37,6 +37,7 @@
#include "expr/node_builder.h"
#include "expr/node.h"
#include "expr/node_self_iterator.h"
+#include "expr/attribute.h"
#include "prop/prop_engine.h"
#include "proof/theory_proof.h"
#include "smt/modal_exception.h"
@@ -521,6 +522,10 @@ public:
}
}
+ void nmNotifyDeleteNode(TNode n) {
+ d_smt.d_smtAttributes->deleteAllAttributes(n);
+ }
+
Node applySubstitutions(TNode node) const {
return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
}
@@ -654,7 +659,7 @@ public:
}/* namespace CVC4::smt */
SmtEngine::SmtEngine(ExprManager* em) throw() :
- d_context(em->getContext()),
+ d_context(new Context()),
d_userLevels(),
d_userContext(new UserContext()),
d_exprManager(em),
@@ -684,10 +689,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
d_cumulativeResourceUsed(0),
d_status(),
d_private(NULL),
+ d_smtAttributes(NULL),
d_statisticsRegistry(NULL),
d_stats(NULL) {
SmtScope smts(this);
+ d_smtAttributes = new expr::attr::SmtAttributes(d_context);
d_private = new smt::SmtEnginePrivate(*this);
d_statisticsRegistry = new StatisticsRegistry();
d_stats = new SmtEngineStatistics();
@@ -862,8 +869,13 @@ SmtEngine::~SmtEngine() throw() {
delete d_private;
d_private = NULL;
+ delete d_smtAttributes;
+ d_smtAttributes = NULL;
+
delete d_userContext;
d_userContext = NULL;
+ delete d_context;
+ d_context = NULL;
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7effa521a..30f84346a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -71,6 +71,13 @@ namespace prop {
class PropEngine;
}/* CVC4::prop namespace */
+namespace expr {
+ namespace attr {
+ class AttributeManager;
+ struct SmtAttributes;
+ }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
namespace smt {
/**
* Representation of a defined function. We keep these around in
@@ -342,9 +349,20 @@ class CVC4_PUBLIC SmtEngine {
// to access d_modelCommands
friend class ::CVC4::Model;
friend class ::CVC4::theory::TheoryModel;
+ // to access SmtAttributes
+ friend class expr::attr::AttributeManager;
// to access getModel(), which is private (for now)
friend class GetModelCommand;
+ /**
+ * There's something of a handshake between the expr package's
+ * AttributeManager and the SmtEngine because the expr package
+ * doesn't have a Context on its own (that's owned by the
+ * SmtEngine). Thus all context-dependent attributes are stored
+ * here.
+ */
+ expr::attr::SmtAttributes* d_smtAttributes;
+
StatisticsRegistry* d_statisticsRegistry;
smt::SmtEngineStatistics* d_stats;
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
index df60bbc33..5435fba34 100644
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
@@ -23,7 +23,6 @@ using namespace std;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::kind;
-using namespace CVC4::context;
void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 7321e22b4..81cd5948a 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -24,7 +24,6 @@ using namespace std;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::kind;
-using namespace CVC4::context;
bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h
index 91e12a25e..4daab5cce 100644
--- a/test/unit/context/stacking_map_black.h
+++ b/test/unit/context/stacking_map_black.h
@@ -39,8 +39,8 @@ class StackingMapBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_ctxt = new Context();
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
d_mapPtr = new StackingMap<TNode, TNode, TNodeHashFunction>(d_ctxt);
diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h
index c7e185735..35305e469 100644
--- a/test/unit/context/stacking_vector_black.h
+++ b/test/unit/context/stacking_vector_black.h
@@ -39,8 +39,8 @@ class StackingVectorBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_ctxt = new Context();
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
d_vectorPtr = new StackingVector<TNode>(d_ctxt);
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 8fee6571d..5f9a7ebce 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -26,31 +26,35 @@
#include "expr/node_manager.h"
#include "expr/node.h"
#include "expr/attribute.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
+using namespace CVC4::smt;
using namespace std;
class AttributeBlack : public CxxTest::TestSuite {
private:
- Context* d_ctxt;
+ ExprManager* d_exprManager;
NodeManager* d_nodeManager;
- NodeManagerScope* d_scope;
+ SmtEngine* d_smtEngine;
+ SmtScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context;
- d_nodeManager = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nodeManager);
+ d_exprManager = new ExprManager();
+ d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+ d_smtEngine = new SmtEngine(d_exprManager);
+ d_scope = new SmtScope(d_smtEngine);
}
void tearDown() {
delete d_scope;
- delete d_nodeManager;
- delete d_ctxt;
+ delete d_smtEngine;
+ delete d_exprManager;
}
class MyData {
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 11063cd1b..00ebc8b8d 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,7 +18,6 @@
#include <string>
-#include "context/context.h"
#include "expr/node_value.h"
#include "expr/node_builder.h"
#include "expr/node_manager.h"
@@ -29,10 +28,12 @@
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
#include "util/cvc4_assert.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
+using namespace CVC4::smt;
using namespace CVC4::expr;
using namespace CVC4::expr::attr;
using namespace std;
@@ -60,26 +61,27 @@ typedef CDAttribute<Test2, bool> TestFlag2cd;
class AttributeWhite : public CxxTest::TestSuite {
- Context* d_ctxt;
+ ExprManager* d_em;
NodeManager* d_nm;
- NodeManagerScope* d_scope;
+ SmtScope* d_scope;
TypeNode* d_booleanType;
+ SmtEngine* d_smtEngine;
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
-
+ d_em = new ExprManager();
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_smtEngine = new SmtEngine(d_em);
+ d_scope = new SmtScope(d_smtEngine);
d_booleanType = new TypeNode(d_nm->booleanType());
}
void tearDown() {
delete d_booleanType;
delete d_scope;
- delete d_nm;
- delete d_ctxt;
+ delete d_smtEngine;
+ delete d_em;
}
void testAttributeIds() {
@@ -145,7 +147,6 @@ public:
lastId = attr::LastAttributeId<TypeNode, false>::getId();
TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId);
-
}
void testCDAttributes() {
@@ -162,7 +163,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->push(); // level 1
+ d_smtEngine->push(); // level 1
// test that all boolean flags are FALSE to start
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
@@ -204,7 +205,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->push(); // level 2
+ d_smtEngine->push(); // level 2
Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
TS_ASSERT(a.getAttribute(TestFlag1cd()));
@@ -225,7 +226,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->push(); // level 3
+ d_smtEngine->push(); // level 3
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -244,7 +245,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be T)\n";
TS_ASSERT(c.getAttribute(TestFlag1cd()));
- d_ctxt->pop(); // level 2
+ d_smtEngine->pop(); // level 2
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -253,7 +254,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->pop(); // level 1
+ d_smtEngine->pop(); // level 1
Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
TS_ASSERT(a.getAttribute(TestFlag1cd()));
@@ -262,7 +263,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->pop(); // level 0
+ d_smtEngine->pop(); // level 0
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -271,13 +272,11 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException );
-#endif /* CVC4_ASSERTIONS */
+ TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException );
}
void testAttributes() {
- //Debug.on("bootattr");
+ //Debug.on("boolattr");
Node a = d_nm->mkVar(*d_booleanType);
Node b = d_nm->mkVar(*d_booleanType);
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 9f8ecb69e..7d6ee523a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -28,14 +28,12 @@
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
using namespace std;
class NodeBlack : public CxxTest::TestSuite {
private:
Options opts;
- Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
TypeNode* d_booleanType;
@@ -51,8 +49,7 @@ public:
free(argv[0]);
free(argv[1]);
- d_ctxt = new Context();
- d_nodeManager = new NodeManager(d_ctxt, NULL, opts);
+ d_nodeManager = new NodeManager(NULL, opts);
d_scope = new NodeManagerScope(d_nodeManager);
d_booleanType = new TypeNode(d_nodeManager->booleanType());
d_realType = new TypeNode(d_nodeManager->realType());
@@ -62,7 +59,6 @@ public:
delete d_booleanType;
delete d_scope;
delete d_nodeManager;
- delete d_ctxt;
}
bool imp(bool a, bool b) const {
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index c71ba48c5..9bac0d818 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -25,19 +25,16 @@
#include "expr/node_manager.h"
#include "expr/node.h"
#include "expr/kind.h"
-#include "context/context.h"
#include "util/cvc4_assert.h"
#include "util/rational.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
using namespace std;
class NodeBuilderBlack : public CxxTest::TestSuite {
private:
- Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
TypeNode* d_booleanType;
@@ -47,8 +44,7 @@ private:
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
specKind = AND;
@@ -63,7 +59,6 @@ public:
delete d_realType;
delete d_scope;
delete d_nm;
- delete d_ctxt;
}
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 9ca086d06..b94e6a691 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -21,7 +21,6 @@
#include "expr/node_manager.h"
#include "expr/node_manager_attributes.h"
-#include "context/context.h"
#include "util/rational.h"
#include "util/integer.h"
@@ -29,26 +28,22 @@
using namespace CVC4;
using namespace CVC4::expr;
using namespace CVC4::kind;
-using namespace CVC4::context;
class NodeManagerBlack : public CxxTest::TestSuite {
- Context* d_context;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_context = new Context;
- d_nodeManager = new NodeManager(d_context, NULL);
+ d_nodeManager = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nodeManager);
}
void tearDown() {
delete d_scope;
delete d_nodeManager;
- delete d_context;
}
void testMkNodeNot() {
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 7bc279f47..aaa3256dd 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,33 +19,28 @@
#include <string>
#include "expr/node_manager.h"
-#include "context/context.h"
#include "util/rational.h"
#include "util/integer.h"
using namespace CVC4;
using namespace CVC4::expr;
-using namespace CVC4::context;
class NodeManagerWhite : public CxxTest::TestSuite {
- Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context();
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
}
void tearDown() {
delete d_scope;
delete d_nm;
- delete d_ctxt;
}
void testMkConstRational() {
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 9f90bd1b0..7240deed5 100644
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -16,14 +16,12 @@
#include <cxxtest/TestSuite.h>
-#include "context/context.h"
#include "expr/node.h"
#include "expr/node_self_iterator.h"
#include "expr/node_builder.h"
#include "expr/convenience_node_builders.h"
using namespace CVC4;
-using namespace CVC4::context;
using namespace CVC4::kind;
using namespace CVC4::expr;
using namespace std;
@@ -31,7 +29,6 @@ using namespace std;
class NodeSelfIteratorBlack : public CxxTest::TestSuite {
private:
- Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
TypeNode* d_booleanType;
@@ -40,8 +37,7 @@ private:
public:
void setUp() {
- d_ctxt = new Context;
- d_nodeManager = new NodeManager(d_ctxt, NULL);
+ d_nodeManager = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nodeManager);
d_booleanType = new TypeNode(d_nodeManager->booleanType());
d_realType = new TypeNode(d_nodeManager->realType());
@@ -51,7 +47,6 @@ public:
delete d_booleanType;
delete d_scope;
delete d_nodeManager;
- delete d_ctxt;
}
void testSelfIteration() {
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index bcb3155e1..8a68db269 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -22,33 +22,28 @@
#include "expr/node_builder.h"
#include "expr/node_manager.h"
#include "expr/node.h"
-#include "context/context.h"
#include "util/cvc4_assert.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
using namespace CVC4::expr;
using namespace std;
class NodeWhite : public CxxTest::TestSuite {
- Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context();
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
}
void tearDown() {
delete d_scope;
delete d_nm;
- delete d_ctxt;
}
void testNull() {
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index e2937ccb2..db02ce207 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -14,7 +14,6 @@
** Black box testing of CVC4::BooleanSimplification.
**/
-#include "context/context.h"
#include "util/language.h"
#include "expr/node.h"
#include "expr/kind.h"
@@ -26,12 +25,10 @@
#include <set>
using namespace CVC4;
-using namespace CVC4::context;
using namespace std;
class BooleanSimplificationBlack : public CxxTest::TestSuite {
- Context* d_context;
NodeManager* d_nm;
NodeManagerScope* d_scope;
@@ -70,8 +67,7 @@ class BooleanSimplificationBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_context = new Context();
- d_nm = new NodeManager(d_context, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
a = d_nm->mkSkolem("a", d_nm->booleanType());
@@ -116,7 +112,6 @@ public:
delete d_scope;
delete d_nm;
- delete d_context;
}
void testNegate() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback