From 22f47a144520f39801abb3acacbf3639886b0478 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 21 Oct 2010 22:51:30 +0000 Subject: [PATCH] * 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 --- src/expr/node_builder.h | 2 +- src/main/getopt.cpp | 22 +++++- src/main/main.cpp | 9 +-- src/main/usage.h | 6 +- src/prop/prop_engine.cpp | 8 +-- src/prop/prop_engine.h | 6 +- src/prop/sat.h | 8 +-- src/smt/options.h | 4 ++ src/smt/smt_engine.cpp | 74 ++++++++++++-------- src/smt/smt_engine.h | 46 +++++++++++- src/theory/theory_engine.cpp | 6 +- src/theory/theory_engine.h | 7 +- test/unit/theory/shared_term_manager_black.h | 2 +- test/unit/theory/theory_engine_white.h | 2 +- 14 files changed, 135 insertions(+), 67 deletions(-) diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 4c8bc578a..095e81868 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -664,7 +664,7 @@ private: inline void debugCheckType(const TNode n) const { // force an immediate type check, if we are in debug mode // and the current node isn't a variable or constant - if( IS_DEBUG_BUILD && d_nm->d_earlyTypeChecking ) { + if( d_nm->d_earlyTypeChecking ) { kind::MetaKind mk = n.getMetaKind(); if( mk != kind::metakind::VARIABLE && mk != kind::metakind::CONSTANT ) { diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 5ddeced5d..25badb7e5 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -76,7 +76,9 @@ enum OptionValue { NO_INTERACTIVE, PRODUCE_MODELS, PRODUCE_ASSIGNMENTS, - NO_EARLY_TYPE_CHECKING + NO_TYPE_CHECKING, + LAZY_TYPE_CHECKING, + EAGER_TYPE_CHECKING, };/* enum OptionValue */ /** @@ -128,7 +130,9 @@ static struct option cmdlineOptions[] = { { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, PRODUCE_MODELS}, { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS}, - { "no-type-checking", no_argument, NULL, NO_EARLY_TYPE_CHECKING}, + { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING}, + { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING}, + { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING}, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -229,6 +233,8 @@ throw(OptionException) { case NO_CHECKING: opts->semanticChecks = false; + opts->typeChecking = false; + opts->earlyTypeChecking = false; break; case USE_MMAP: @@ -302,10 +308,20 @@ throw(OptionException) { opts->produceAssignments = true; break; - case NO_EARLY_TYPE_CHECKING: + case NO_TYPE_CHECKING: + opts->typeChecking = false; + opts->earlyTypeChecking = false; + break; + + case LAZY_TYPE_CHECKING: opts->earlyTypeChecking = false; break; + case EAGER_TYPE_CHECKING: + opts->typeChecking = true; + opts->earlyTypeChecking = true; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/main/main.cpp b/src/main/main.cpp index 8f790c211..8ed938351 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -128,18 +128,11 @@ int runCvc4(int argc, char* argv[]) { options.interactive = inputFromStdin && isatty(fileno(stdin)); } - /* Early type checking can be turned off by --no-type-checking OR - --no-checking. We're assuming that earlyTypeChecking is not - explicitly set by the user. */ - if(options.earlyTypeChecking) { - options.earlyTypeChecking = options.semanticChecks; - } - // Create the expression manager ExprManager exprMgr(options.earlyTypeChecking); // Create the SmtEngine - SmtEngine smt(&exprMgr, &options); + SmtEngine smt(&exprMgr, options); // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; diff --git a/src/main/usage.h b/src/main/usage.h index 7affc254c..5ad96aea6 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -37,8 +37,10 @@ CVC4 options:\n\ --mmap memory map file input\n\ --show-config show CVC4 static configuration\n\ --segv-nospin don't spin on segfault waiting for gdb\n\ - --no-checking disable semantic checks in the parser\n\ - --no-type-checking disable type checking [default in non-debug builds]\n\ + --lazy-type-checking type check expressions only when necessary (default)\n\ + --eager-type-checking type check expressions immediately on creation\n\ + --no-type-checking never type check expressions\n\ + --no-checking disable ALL semantic checks, including type checks \n\ --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ --verbose | -v increase verbosity (repeatable)\n\ --quiet | -q decrease verbosity (repeatable)\n\ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index d7b1e6d99..f503efae2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -57,15 +57,15 @@ public: } }; -PropEngine::PropEngine(const Options* opts, DecisionEngine* de, - TheoryEngine* te, Context* context) : +PropEngine::PropEngine(DecisionEngine* de, TheoryEngine* te, + Context* context, const Options& opts) : d_inCheckSat(false), - d_options(opts), + // d_options(opts), d_decisionEngine(de), d_theoryEngine(te), d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; - d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options); + d_satSolver = new SatSolver(this, d_theoryEngine, d_context, opts); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); d_satSolver->setCnfStream(d_cnfStream); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 1dada2e69..1c7c506ee 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -26,11 +26,11 @@ #include "expr/node.h" #include "util/result.h" #include "util/decision_engine.h" +#include "smt/options.h" namespace CVC4 { class TheoryEngine; -class Options; namespace prop { @@ -50,7 +50,7 @@ class PropEngine { bool d_inCheckSat; /** The global options */ - const Options *d_options; + //const Options d_options; /** The decision engine we will be using */ DecisionEngine *d_decisionEngine; @@ -76,7 +76,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*); + PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&); /** * Destructor. diff --git a/src/prop/sat.h b/src/prop/sat.h index a335b733b..17bf447f8 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -125,7 +125,7 @@ class SatSolver : public SatInputInterface { context::Context* d_context; /** Remember the options */ - Options* d_options; + // Options* d_options; /* Pointer to the concrete SAT solver. Including this via the preprocessor saves us a level of indirection vs, e.g., defining a @@ -203,7 +203,7 @@ public: SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context, - const Options* options); + const Options& options); ~SatSolver(); @@ -233,7 +233,7 @@ public: #ifdef __CVC4_USE_MINISAT inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, - context::Context* context, const Options* options) : + context::Context* context, const Options& options) : d_propEngine(propEngine), d_cnfStream(NULL), d_theoryEngine(theoryEngine), @@ -243,7 +243,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, // Create the solver d_minisat = new Minisat::SimpSolver(this, d_context); // Setup the verbosity - d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1; + d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1; // No random choices if(Debug.isOn("no_rnd_decisions")){ 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 v; if((*i).getKind() == kind::APPLY) { @@ -595,7 +607,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { vector 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 Node; typedef NodeTemplate 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 @@ -162,10 +190,15 @@ 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 */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4113466d7..2fcfc9626 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -126,7 +126,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { } } -TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : +TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) : d_propEngine(NULL), d_theoryOut(this, ctxt), d_hasShutDown(false), @@ -137,7 +137,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut); d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut); - switch(opts->uf_implementation) { + switch(opts.uf_implementation) { case Options::TIM: d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut); break; @@ -145,7 +145,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut); break; default: - Unhandled(opts->uf_implementation); + Unhandled(opts.uf_implementation); } d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut); d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ca39001fe..0bca372ca 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -22,10 +22,11 @@ #define __CVC4__THEORY_ENGINE_H #include "expr/node.h" -#include "theory/theory.h" -#include "theory/theoryof_table.h" #include "prop/prop_engine.h" +#include "smt/options.h" #include "theory/shared_term_manager.h" +#include "theory/theory.h" +#include "theory/theoryof_table.h" #include "util/stats.h" namespace CVC4 { @@ -206,7 +207,7 @@ public: /** * Construct a theory engine. */ - TheoryEngine(context::Context* ctxt, const Options* opts); + TheoryEngine(context::Context* ctxt, const Options& opts); /** * Destroy a theory engine. diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 3e7a9f523..5007f43ed 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -61,7 +61,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_theoryEngine = new TheoryEngine(d_ctxt, &d_options); + d_theoryEngine = new TheoryEngine(d_ctxt, d_options); } void tearDown() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 12c38d0d7..00766ec90 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -248,7 +248,7 @@ public: d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV"); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt, &d_options); + d_theoryEngine = new TheoryEngine(d_ctxt, d_options); // insert our fake versions into the TheoryEngine's theoryOf table d_theoryEngine->d_theoryOfTable. -- 2.30.2