From 159cb7ee8b6f28f3784a3f24b371760c2ab77f86 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 1 Apr 2011 00:56:42 +0000 Subject: This commit is a merge from the "betterstats" branch, which: * Makes Options an "omnipresent thread-local global" (like the notion of the "current NodeManager" was already). Options::current() accesses this structure. * Removes Options from constructors and data structures everywhere (this cleans up a lot of things). * No longer uses StatisticsRegistry statically. An instance of the registry is created and linked to a NodeManager. * StatisticsRegistry::current() is similar to Options::current(), but the pointer is stowed in the NodeManager (rather than stored) * The static functions of StatisticsRegistry have been left, for backward compatibility; they now use the "current" statistics registry. * SmtEngine::getStatisticsRegistry() is a public accessor for the registry; this is needed by main() to reach in and get the registry, for flushing statistics at the end. --- src/smt/smt_engine.cpp | 71 ++++++++++++++++++++------------------------------ src/smt/smt_engine.h | 52 +++++------------------------------- 2 files changed, 35 insertions(+), 88 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fe5e55ae6..cb6dd3460 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -120,28 +120,17 @@ public: using namespace CVC4::smt; -SmtEngine::SmtEngine(ExprManager* em) throw() : - d_exprManager(em) { - Options opts; - init(opts); -} - -SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() : - d_exprManager(em){ - init(opts); -} - -void SmtEngine::init(const Options& opts) throw() { - d_context = d_exprManager->getContext(); - d_userContext = new Context(); - - d_nodeManager = d_exprManager->getNodeManager(); +SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : + d_context(em->getContext()), + d_userContext(new Context()), + d_exprManager(em), + d_nodeManager(d_exprManager->getNodeManager()) { NodeManagerScope nms(d_nodeManager); // We have mutual dependancy here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_context, opts); + d_theoryEngine = new TheoryEngine(d_context); // Add the theories d_theoryEngine->addTheory(); @@ -149,7 +138,7 @@ void SmtEngine::init(const Options& opts) throw() { d_theoryEngine->addTheory(); d_theoryEngine->addTheory(); d_theoryEngine->addTheory(); - switch(opts.uf_implementation) { + switch(Options::current()->uf_implementation) { case Options::TIM: d_theoryEngine->addTheory(); break; @@ -157,30 +146,22 @@ void SmtEngine::init(const Options& opts) throw() { d_theoryEngine->addTheory(); break; default: - Unhandled(opts.uf_implementation); + Unhandled(Options::current()->uf_implementation); } - d_propEngine = new PropEngine(d_theoryEngine, d_context, opts); + d_propEngine = new PropEngine(d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); d_assertionList = NULL; - d_interactive = opts.interactive; - if(d_interactive) { + if(Options::current()->interactive) { d_assertionList = new(true) AssertionList(d_userContext); } d_assignments = NULL; d_haveAdditions = false; d_queryMade = false; - - d_typeChecking = opts.typeChecking; - d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion; - d_produceModels = opts.produceModels; - d_produceAssignments = opts.produceAssignments; - - d_incrementalSolving = opts.incrementalSolving; } void SmtEngine::shutdown() { @@ -354,7 +335,7 @@ void SmtEngine::defineFunction(Expr func, Expr formula) { Debug("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); - Type formulaType = formula.getType(d_typeChecking);// type check body + Type formulaType = formula.getType(Options::current()->typeChecking);// type check body Type funcType = func.getType(); Type rangeType = funcType.isFunction() ? FunctionType(funcType).getRangeType() : funcType; @@ -445,7 +426,7 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) throw(NoSuchFunctionException, AssertionException) { Node n; - if(!smt.d_lazyDefinitionExpansion) { + if(!Options::current()->lazyDefinitionExpansion) { Debug("expand") << "have: " << n << endl; n = expandDefinitions(smt, in); Debug("expand") << "made: " << n << endl; @@ -486,7 +467,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) } void SmtEngine::ensureBoolean(const BoolExpr& e) { - Type type = e.getType(d_typeChecking); + Type type = e.getType(Options::current()->typeChecking); Type boolType = d_exprManager->booleanType(); if(type != boolType) { stringstream ss; @@ -501,7 +482,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT checkSat(" << e << ")" << endl; - if(d_queryMade && !d_incrementalSolving) { + if(d_queryMade && !Options::current()->incrementalSolving) { throw ModalException("Cannot make multiple queries unless " "incremental solving is enabled " "(try --incremental)"); @@ -522,7 +503,7 @@ Result SmtEngine::query(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT query(" << e << ")" << endl; - if(d_queryMade && !d_incrementalSolving) { + if(d_queryMade && !Options::current()->incrementalSolving) { throw ModalException("Cannot make multiple queries unless " "incremental solving is enabled " "(try --incremental)"); @@ -554,7 +535,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { Expr SmtEngine::simplify(const Expr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); - if( d_typeChecking ) { + if( Options::current()->typeChecking ) { e.getType(true);// ensure expr is type-checked at this point } Debug("smt") << "SMT simplify(" << e << ")" << endl; @@ -566,9 +547,9 @@ Expr SmtEngine::simplify(const Expr& e) { Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); - Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point + Type type = e.getType(Options::current()->typeChecking);// ensure expr is type-checked at this point Debug("smt") << "SMT getValue(" << e << ")" << endl; - if(!d_produceModels) { + if(!Options::current()->produceModels) { const char* msg = "Cannot get value when produce-models options is off."; throw ModalException(msg); @@ -601,7 +582,7 @@ Expr SmtEngine::getValue(const Expr& e) bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Type type = e.getType(d_typeChecking); + Type type = e.getType(Options::current()->typeChecking); // must be Boolean CheckArgument( type.isBoolean(), e, "expected Boolean-typed variable or function application " @@ -615,7 +596,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { n.getMetaKind() == kind::metakind::VARIABLE ), e, "expected variable or defined-function application " "in addToAssignment(),\ngot %s", e.toString().c_str() ); - if(!d_produceAssignments) { + if(!Options::current()->produceAssignments) { return false; } if(d_assignments == NULL) { @@ -628,7 +609,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Debug("smt") << "SMT getAssignment()" << endl; - if(!d_produceAssignments) { + if(!Options::current()->produceAssignments) { const char* msg = "Cannot get the current assignment when " "produce-assignments option is off."; @@ -680,7 +661,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { vector SmtEngine::getAssertions() throw(ModalException, AssertionException) { Debug("smt") << "SMT getAssertions()" << endl; - if(!d_interactive) { + if(!Options::current()->interactive) { const char* msg = "Cannot query the current assertion list when not in interactive mode."; throw ModalException(msg); @@ -692,7 +673,7 @@ vector SmtEngine::getAssertions() void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT push()" << endl; - if(!d_incrementalSolving) { + if(!Options::current()->incrementalSolving) { throw ModalException("Cannot push when not solving incrementally (use --incremental)"); } d_userLevels.push_back(d_userContext->getLevel()); @@ -704,7 +685,7 @@ void SmtEngine::push() { void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT pop()" << endl; - if(!d_incrementalSolving) { + if(!Options::current()->incrementalSolving) { throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); } AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel()); @@ -731,4 +712,8 @@ void SmtEngine::internalPush() { d_propEngine->push(); } +StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { + return d_exprManager->d_nodeManager->getStatisticsRegistry(); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c884b2c5f..b872985fb 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -49,6 +49,8 @@ class NodeHashFunction; class TheoryEngine; +class StatisticsRegistry; + namespace context { class Context; }/* CVC4::context namespace */ @@ -139,44 +141,11 @@ class CVC4_PUBLIC SmtEngine { */ bool d_queryMade; - /** - * Whether or not to type check input expressions. - */ - bool d_typeChecking; - - /** - * Whether we're being used in an interactive setting. - */ - bool d_interactive; - - /** - * Whether we expand function definitions lazily. - */ - bool d_lazyDefinitionExpansion; - - /** - * Whether getValue() is enabled. - */ - bool d_produceModels; - - /** - * Whether getAssignment() is enabled. - */ - bool d_produceAssignments; - - /** - * Whether multiple queries can be made, and also push/pop is enabled. - */ - bool d_incrementalSolving; - /** * Most recent result of last checkSat/query or (set-info :status). */ Result d_status; - /** Called by the constructors to setup fields. */ - void init(const Options& opts) throw(); - /** * This is called by the destructor, just before destroying the * PropEngine, TheoryEngine, and DecisionEngine (in that order). It @@ -215,12 +184,7 @@ public: /** * Construct an SmtEngine with the given expression manager. */ - SmtEngine(ExprManager* em) throw(); - - /** - * Construct an SmtEngine with the given expression manager and user options. - */ - SmtEngine(ExprManager* em, const Options& opts) throw(); + SmtEngine(ExprManager* em) throw(AssertionException); /** * Destruct the SMT engine. @@ -336,12 +300,10 @@ public: */ void pop(); - /** Enable type checking. Forces a type check on any Expr parameter - to an SmtEngine method. */ - void enableTypeChecking() { d_typeChecking = true; } - - /** Disable type checking. */ - void disableTypeChecking() { d_typeChecking = false; } + /** + * Permit access to the underlying StatisticsRegistry. + */ + StatisticsRegistry* getStatisticsRegistry() const; };/* class SmtEngine */ -- cgit v1.2.3