diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-21 22:51:30 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-21 22:51:30 +0000 |
commit | 22f47a144520f39801abb3acacbf3639886b0478 (patch) | |
tree | 13a5808dac1f0a946e1a14c414a45f16b2a6b00e /src/smt | |
parent | 91829206b4783a532453eab3c69de83b8b510286 (diff) |
* Option --no-type-checking now disables type checks in SmtEngine
* Adding options --lazy-type-checking and --eager-type-checking
to control type checking in NodeBuilder, which can now be enabled
in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options.h | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 74 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 46 |
3 files changed, 90 insertions, 34 deletions
diff --git a/src/smt/options.h b/src/smt/options.h index 7ddaf5d4d..73c38545f 100644 --- a/src/smt/options.h +++ b/src/smt/options.h @@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options { /** Whether we support SmtEngine::getAssignment() for this run. */ bool produceAssignments; + /** Whether we do typechecking at all. */ + bool typeChecking; + /** Whether we do typechecking at Expr creation time. */ bool earlyTypeChecking; @@ -109,6 +112,7 @@ struct CVC4_PUBLIC Options { interactiveSetByUser(false), produceModels(false), produceAssignments(false), + typeChecking(true), earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { } };/* struct Options */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2f2fba848..d76a002e7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -111,21 +111,20 @@ public: using namespace CVC4::smt; -SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : - d_context(em->getContext()), - d_exprManager(em), - d_nodeManager(em->getNodeManager()), - d_options(opts), - /* These next few are initialized below, after we have a NodeManager - * in scope. */ - d_decisionEngine(NULL), - d_theoryEngine(NULL), - d_propEngine(NULL), - d_definedFunctions(NULL), - d_assertionList(NULL), - d_assignments(NULL), - d_haveAdditions(false), - d_status() { +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_nodeManager = d_exprManager->getNodeManager(); NodeManagerScope nms(d_nodeManager); @@ -133,15 +132,26 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : // 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_propEngine = new PropEngine(opts, d_decisionEngine, - d_theoryEngine, d_context); + d_propEngine = new PropEngine(d_decisionEngine, d_theoryEngine, + d_context, opts); d_theoryEngine->setPropEngine(d_propEngine); d_definedFunctions = new(true) DefinedFunctionMap(d_context); - if(d_options->interactive) { + d_assertionList = NULL; + d_interactive = opts.interactive; + if(d_interactive) { d_assertionList = new(true) AssertionList(d_context); } + + d_assignments = NULL; + d_haveAdditions = false; + + d_typeChecking = opts.typeChecking; + d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion; + d_produceModels = opts.produceModels; + d_produceAssignments = opts.produceAssignments; + } void SmtEngine::shutdown() { @@ -299,7 +309,7 @@ void SmtEngine::defineFunction(Expr func, Expr formula) { Debug("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); - Type formulaType = formula.getType(true);// type check body + Type formulaType = formula.getType(d_typeChecking);// type check body Type funcType = func.getType(); Type rangeType = funcType.isFunction() ? FunctionType(funcType).getRangeType() : funcType; @@ -388,7 +398,7 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n) Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) throw(NoSuchFunctionException, AssertionException) { - if(!smt.d_options->lazyDefinitionExpansion) { + if(!smt.d_lazyDefinitionExpansion) { Node node = expandDefinitions(smt, n); Debug("expand") << "have: " << n << endl << "made: " << node << endl; @@ -416,7 +426,7 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) } void SmtEngine::ensureBoolean(const BoolExpr& e) { - Type type = e.getType(true); + Type type = e.getType(d_typeChecking); Type boolType = d_exprManager->booleanType(); if(type != boolType) { stringstream ss; @@ -468,7 +478,9 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { Expr SmtEngine::simplify(const Expr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); - e.getType(true);// ensure expr is type-checked at this point + if( d_typeChecking ) { + e.getType(true);// ensure expr is type-checked at this point + } Debug("smt") << "SMT simplify(" << e << ")" << endl; Unimplemented(); } @@ -476,14 +488,14 @@ Expr SmtEngine::simplify(const Expr& e) { Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); - Type type = e.getType(true);// ensure expr is type-checked at this point + Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point Debug("smt") << "SMT getValue(" << e << ")" << endl; - if(!d_options->interactive) { + if(!d_interactive) { const char* msg = "Cannot get value when not in interactive mode."; throw ModalException(msg); } - if(!d_options->produceModels) { + if(!d_produceModels) { const char* msg = "Cannot get value when produce-models options is off."; throw ModalException(msg); @@ -510,13 +522,13 @@ Expr SmtEngine::getValue(const Expr& e) Node resultNode = d_theoryEngine->getValue(n); // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType(true) == eNode.getType()); + Assert(resultNode.isNull() || resultNode.getType() == eNode.getType()); return Expr(d_exprManager, new Node(resultNode)); } bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { NodeManagerScope nms(d_nodeManager); - Type type = e.getType(true); + Type type = e.getType(d_typeChecking); // must be Boolean CheckArgument( type.isBoolean(), e, "expected Boolean-typed variable or function application " @@ -530,7 +542,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_options->produceAssignments) { + if(!d_produceAssignments) { return false; } if(d_assignments == NULL) { @@ -543,7 +555,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Debug("smt") << "SMT getAssignment()" << endl; - if(!d_options->produceAssignments) { + if(!d_produceAssignments) { const char* msg = "Cannot get the current assignment when " "produce-assignments option is off."; @@ -576,7 +588,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Node resultNode = d_theoryEngine->getValue(n); // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType(true) == boolType); + Assert(resultNode.isNull() || resultNode.getType() == boolType); vector<SExpr> v; if((*i).getKind() == kind::APPLY) { @@ -595,7 +607,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) { Debug("smt") << "SMT getAssertions()" << endl; - if(!d_options->interactive) { + if(!d_interactive) { const char* msg = "Cannot query the current assertion list when not in interactive mode."; throw ModalException(msg); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a3116dfa9..0831a0447 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -34,6 +34,7 @@ #include "util/hash.h" #include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" +#include "smt/options.h" #include "smt/bad_option_exception.h" // In terms of abstraction, this is below (and provides services to) @@ -47,7 +48,6 @@ typedef NodeTemplate<true> Node; typedef NodeTemplate<false> TNode; class NodeHashFunction; class Command; -class Options; class TheoryEngine; class DecisionEngine; @@ -99,7 +99,7 @@ class CVC4_PUBLIC SmtEngine { /** Out internal expression/node manager */ NodeManager* d_nodeManager; /** User-level options */ - const Options* d_options; + //const Options d_options; /** The decision engine */ DecisionEngine* d_decisionEngine; /** The decision engine */ @@ -126,11 +126,39 @@ class CVC4_PUBLIC SmtEngine { */ bool d_haveAdditions; + /** + * 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; + /** * 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 @@ -163,9 +191,14 @@ class CVC4_PUBLIC SmtEngine { 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, const Options& opts) throw(); /** * Destruct the SMT engine. @@ -273,6 +306,13 @@ 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; } + };/* class SmtEngine */ }/* CVC4 namespace */ |