summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/declaration_scope.cpp9
-rw-r--r--src/expr/declaration_scope.h4
-rw-r--r--src/expr/expr_manager_scope.h2
-rw-r--r--src/expr/expr_manager_template.cpp5
-rw-r--r--src/expr/node_builder.h34
-rw-r--r--src/expr/node_manager.cpp30
-rw-r--r--src/expr/node_manager.h33
-rw-r--r--src/expr/type.cpp2
8 files changed, 82 insertions, 37 deletions
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index f36c8a6e3..09aa3ed9f 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -21,6 +21,7 @@
#include "expr/declaration_scope.h"
#include "expr/expr.h"
#include "expr/type.h"
+#include "expr/expr_manager_scope.h"
#include "context/cdmap.h"
#include "context/cdset.h"
#include "context/context.h"
@@ -48,11 +49,15 @@ DeclarationScope::~DeclarationScope() {
delete d_context;
}
-void DeclarationScope::bind(const std::string& name, Expr obj) throw() {
+void DeclarationScope::bind(const std::string& name, Expr obj) throw(AssertionException) {
+ CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+ ExprManagerScope ems(obj);
d_exprMap->insert(name, obj);
}
-void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw() {
+void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw(AssertionException) {
+ CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+ ExprManagerScope ems(obj);
d_exprMap->insert(name, obj);
d_functions->insert(obj);
}
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 9acc46b5f..17140c850 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -77,7 +77,7 @@ public:
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
*/
- void bind(const std::string& name, Expr obj) throw();
+ void bind(const std::string& name, Expr obj) throw(AssertionException);
/**
* Bind a function body to a name in the current scope. If
@@ -90,7 +90,7 @@ public:
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
*/
- void bindDefinedFunction(const std::string& name, Expr obj) throw();
+ void bindDefinedFunction(const std::string& name, Expr obj) throw(AssertionException);
/**
* Bind a type to a name in the current scope. If <code>name</code>
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index 4fc3f02d4..c1da288a4 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -17,6 +17,8 @@
** \todo document this file
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__EXPR_MANAGER_SCOPE_H
#define __CVC4__EXPR_MANAGER_SCOPE_H
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 9b8511de9..5d34fb53c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -95,9 +95,8 @@ ExprManager::ExprManager(const Options& options) :
}
ExprManager::~ExprManager() {
- delete d_nodeManager;
- delete d_ctxt;
#ifdef CVC4_STATISTICS_ON
+ NodeManagerScope nms(d_nodeManager);
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
if (d_exprStatistics[i] != NULL) {
StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
@@ -111,6 +110,8 @@ ExprManager::~ExprManager() {
}
}
#endif
+ delete d_nodeManager;
+ delete d_ctxt;
}
BooleanType ExprManager::booleanType() const {
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 3b9c41973..68655aed9 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -658,17 +658,12 @@ private:
expr::NodeValue* constructNV();
expr::NodeValue* constructNV() const;
- inline void maybeCheckType(const TNode n) const {
- /* force an immediate type check, if early type checking is
- enabled and the current node isn't a variable or constant */
- if( d_nm->d_earlyTypeChecking ) {
- kind::MetaKind mk = n.getMetaKind();
- if( mk != kind::metakind::VARIABLE
- && mk != kind::metakind::CONSTANT ) {
- d_nm->getType(n, true);
- }
- }
- }
+#ifdef CVC4_DEBUG
+ void maybeCheckType(const TNode n) const
+ throw(TypeCheckingExceptionPrivate, AssertionException);
+#else /* CVC4_DEBUG */
+ inline void maybeCheckType(const TNode n) const throw() { }
+#endif /* CVC4_DEBUG */
public:
@@ -716,6 +711,7 @@ public:
#include "expr/node.h"
#include "expr/node_manager.h"
+#include "util/options.h"
namespace CVC4 {
@@ -1240,6 +1236,22 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
}
}
+#ifdef CVC4_DEBUG
+template <unsigned nchild_thresh>
+inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
+ throw(TypeCheckingExceptionPrivate, AssertionException) {
+ /* force an immediate type check, if early type checking is
+ enabled and the current node isn't a variable or constant */
+ if( d_nm->getOptions()->earlyTypeChecking ) {
+ kind::MetaKind mk = n.getMetaKind();
+ if( mk != kind::metakind::VARIABLE
+ && mk != kind::metakind::CONSTANT ) {
+ d_nm->getType(n, true);
+ }
+ }
+}
+#endif /* CVC4_DEBUG */
+
}/* CVC4 namespace */
#endif /* __CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 9006bf4d9..207f1f492 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -29,6 +29,7 @@
#include "util/Assert.h"
#include "util/options.h"
+#include "util/stats.h"
#include "util/tls.h"
#include <algorithm>
@@ -84,22 +85,28 @@ struct NVReclaim {
};
NodeManager::NodeManager(context::Context* ctxt) :
- d_attrManager(ctxt) {
- Options options;
- init(options);
+ d_optionsAllocated(new Options()),
+ d_options(d_optionsAllocated),
+ d_statisticsRegistry(new StatisticsRegistry()),
+ d_attrManager(ctxt),
+ d_nodeUnderDeletion(NULL),
+ d_inReclaimZombies(false) {
+ init();
}
NodeManager::NodeManager(context::Context* ctxt,
const Options& options) :
- d_attrManager(ctxt) {
- init(options);
+ d_optionsAllocated(NULL),
+ d_options(&options),
+ d_statisticsRegistry(new StatisticsRegistry()),
+ d_attrManager(ctxt),
+ d_nodeUnderDeletion(NULL),
+ d_inReclaimZombies(false) {
+ init();
}
-inline void NodeManager::init(const Options& options) {
- d_nodeUnderDeletion = NULL;
- d_inReclaimZombies = false;
- d_earlyTypeChecking = options.earlyTypeChecking;
+inline void NodeManager::init() {
poolInsert( &expr::NodeValue::s_null );
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -145,6 +152,9 @@ NodeManager::~NodeManager() {
}
Debug("gc:leaks") << ":end:" << std::endl;
}
+
+ delete d_statisticsRegistry;
+ delete d_optionsAllocated;
}
void NodeManager::reclaimZombies() {
@@ -440,7 +450,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
Debug("getType") << "getting type for " << n << std::endl;
- if(needsCheck && !d_earlyTypeChecking) {
+ if(needsCheck && !d_options->earlyTypeChecking) {
/* Iterate and compute the children bottom up. This avoids stack
overflows in computeType() when the Node graph is really deep,
which should only affect us when we're type checking lazily. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d8a690da5..36720bbb3 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -39,10 +39,11 @@
#include "context/context.h"
#include "util/configuration_private.h"
#include "util/tls.h"
+#include "util/options.h"
namespace CVC4 {
-struct Options;
+class StatisticsRegistry;
namespace expr {
@@ -77,6 +78,10 @@ class NodeManager {
static CVC4_THREADLOCAL(NodeManager*) s_current;
+ const Options* d_optionsAllocated;
+ const Options* d_options;
+ StatisticsRegistry* d_statisticsRegistry;
+
NodeValuePool d_nodeValuePool;
expr::attr::AttributeManager d_attrManager;
@@ -120,12 +125,6 @@ class NodeManager {
Node d_operators[kind::LAST_KIND];
/**
- * Whether to do early type checking (only effective in debug
- * builds; other builds never do early type checking).
- */
- bool d_earlyTypeChecking;
-
- /**
* Look up a NodeValue in the pool associated to this NodeManager.
* The NodeValue argument need not be a "completely-constructed"
* NodeValue. In particular, "non-inlined" constants are permitted
@@ -247,7 +246,7 @@ class NodeManager {
TypeNode computeType(TNode n, bool check = false)
throw (TypeCheckingExceptionPrivate, AssertionException);
- void init(const Options& options);
+ void init();
public:
@@ -255,9 +254,19 @@ public:
explicit NodeManager(context::Context* ctxt, const Options& options);
~NodeManager();
- /** The node manager in the current context. */
+ /** The node manager in the current public-facing CVC4 library context */
static NodeManager* currentNM() { return s_current; }
+ /** Get this node manager's options */
+ const Options* getOptions() const {
+ return d_options;
+ }
+
+ /** Get this node manager's statistics registry */
+ StatisticsRegistry* getStatisticsRegistry() const {
+ return d_statisticsRegistry;
+ }
+
// general expression-builders
/** Create a node with one child. */
@@ -600,13 +609,19 @@ public:
NodeManagerScope(NodeManager* nm) :
d_oldNodeManager(NodeManager::s_current) {
+ // There are corner cases where nm can be NULL and it's ok.
+ // For example, if you write { Expr e; }, then when the null
+ // Expr is destructed, there's no active node manager.
+ //Assert(nm != NULL);
NodeManager::s_current = nm;
+ Options::s_current = nm ? nm->d_options : NULL;
Debug("current") << "node manager scope: "
<< NodeManager::s_current << "\n";
}
~NodeManagerScope() {
NodeManager::s_current = d_oldNodeManager;
+ Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
Debug("current") << "node manager scope: "
<< "returning to " << NodeManager::s_current << "\n";
}
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 0d12e7011..46a456d50 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -69,7 +69,7 @@ bool Type::isNull() const {
}
Type& Type::operator=(const Type& t) {
- NodeManagerScope nms(d_nodeManager);
+ NodeManagerScope nms(t.d_nodeManager);
if(this != &t) {
*d_typeNode = *t.d_typeNode;
d_nodeManager = t.d_nodeManager;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback