diff 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 */ |