From 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 6 Oct 2012 04:05:19 +0000 Subject: * Fix some regressions' expected outputs. * Ensure Rewriter::init() is called before ::rewrite(). The array type enumerator recently gave us an end-run around ::init(). TheoryEngine no longer calls these, they're done via static initialization. * Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412). (this commit was certified error- and warning-free by the test-and-commit script.) --- src/parser/smt2/Smt2.g | 23 +++++++++++++---------- src/theory/rewriter.cpp | 21 ++++++++++++++++----- src/theory/rewriter.h | 26 ++++++++++++++------------ src/theory/theory_engine.cpp | 4 +--- 4 files changed, 44 insertions(+), 30 deletions(-) (limited to 'src') 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::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*) 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(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -677,7 +676,6 @@ void TheoryEngine::shutdown() { } } - theory::Rewriter::shutdown(); d_ppCache.clear(); } -- cgit v1.2.3