summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/parser/smt2/Smt2.g23
-rw-r--r--src/theory/rewriter.cpp21
-rw-r--r--src/theory/rewriter.h26
-rw-r--r--src/theory/theory_engine.cpp4
4 files changed, 44 insertions, 30 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1bfba3eb4..dbefc0305 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -217,8 +217,7 @@ command returns [CVC4::Command* cmd = NULL]
symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name); }
LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
- {
- PARSER_STATE->pushScope();
+ { PARSER_STATE->pushScope();
for(std::vector<std::string>::const_iterator i = names.begin(),
iend = names.end();
i != iend;
@@ -308,13 +307,15 @@ command returns [CVC4::Command* cmd = NULL]
( k=INTEGER_LITERAL
{ unsigned n = AntlrInput::tokenToUnsigned(k);
if(n == 0) {
- cmd = new EmptyCommand;
+ cmd = new EmptyCommand();
} else if(n == 1) {
- cmd = new PushCommand;
+ PARSER_STATE->pushScope();
+ cmd = new PushCommand();
} else {
- CommandSequence* seq = new CommandSequence;
+ CommandSequence* seq = new CommandSequence();
do {
- seq->addCommand(new PushCommand);
+ PARSER_STATE->pushScope();
+ seq->addCommand(new PushCommand());
} while(--n > 0);
cmd = seq;
}
@@ -329,13 +330,15 @@ command returns [CVC4::Command* cmd = NULL]
( k=INTEGER_LITERAL
{ unsigned n = AntlrInput::tokenToUnsigned(k);
if(n == 0) {
- cmd = new EmptyCommand;
+ cmd = new EmptyCommand();
} else if(n == 1) {
- cmd = new PopCommand;
+ PARSER_STATE->popScope();
+ cmd = new PopCommand();
} else {
- CommandSequence* seq = new CommandSequence;
+ CommandSequence* seq = new CommandSequence();
do {
- seq->addCommand(new PopCommand);
+ PARSER_STATE->popScope();
+ seq->addCommand(new PopCommand());
} while(--n > 0);
cmd = seq;
}
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 988b2b327..5cdd507d2 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -5,7 +5,7 @@
** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -34,6 +34,18 @@ static TheoryId theoryOf(TNode node) {
static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
#endif /* CVC4_ASSERTIONS */
+class RewriterInitializer {
+ static RewriterInitializer s_rewriterInitializer;
+ RewriterInitializer() { Rewriter::init(); }
+ ~RewriterInitializer() { Rewriter::shutdown(); }
+};/* class RewriterInitializer */
+
+/**
+ * This causes initialization of the rewriter before first use,
+ * and tear-down at exit time.
+ */
+RewriterInitializer RewriterInitializer::s_rewriterInitializer;
+
/**
* TheoryEngine::rewrite() keeps a stack of things that are being pre-
* and post-rewritten. Each element of the stack is a
@@ -220,8 +232,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
Unreachable();
return Node::null();
-}
-
+}/* Rewriter::rewriteTo() */
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index afca18b76..9a6618215 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -5,7 +5,7 @@
** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -50,11 +50,15 @@ struct RewriteResponse {
status(status), node(node) {}
};/* struct RewriteResponse */
+class RewriterInitializer;
+
/**
* The main rewriter class. All functionality is static.
*/
class Rewriter {
+ friend class RewriterInitializer;
+
/** Returns the appropriate cache for a node */
static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
@@ -70,8 +74,8 @@ class Rewriter {
TNode node, TNode cache);
// disable construction of rewriters; all functionality is static
- Rewriter() CVC4_UNUSED;
- Rewriter(const Rewriter&) CVC4_UNUSED;
+ Rewriter() CVC4_UNDEFINED;
+ Rewriter(const Rewriter&) CVC4_UNDEFINED;
/**
* Rewrites the node using the given theory rewriter.
@@ -89,15 +93,6 @@ class Rewriter {
*/
static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
-public:
-
-
- /**
- * Rewrites the node using theoryOf() to determine which rewriter to
- * use on the node.
- */
- static Node rewrite(TNode node);
-
/**
* Should be called before the rewriter gets used for the first time.
*/
@@ -108,6 +103,13 @@ public:
*/
static void shutdown();
+public:
+
+ /**
+ * Rewrites the node using theoryOf() to determine which rewriter to
+ * use on the node.
+ */
+ static Node rewrite(TNode node);
};/* class Rewriter */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4de6dc231..252109a26 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -5,7 +5,7 @@
** Major contributors: barrett, dejan
** Minor contributors (to current version): cconway, taking
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -94,7 +94,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_curr_model = new theory::TheoryModel( context, "DefaultModel", true );
d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
- Rewriter::init();
StatisticsRegistry::registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -677,7 +676,6 @@ void TheoryEngine::shutdown() {
}
}
- theory::Rewriter::shutdown();
d_ppCache.clear();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback