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/smt_engine.h | |
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/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 46 |
1 files changed, 43 insertions, 3 deletions
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 */ |