diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-25 00:42:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-25 00:42:52 +0000 |
commit | 2a1ac62e56d43893c59c4c2d91bcaca0dd7ce417 (patch) | |
tree | 5d2e6b493d8d366ab75163effaf13191dbf0bd71 /src/smt | |
parent | 06b391f721c8e9de4835e5a5bf2c60383ea7f8e9 (diff) |
additional work on parser hookup, configuration + build
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 11 |
2 files changed, 18 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f6b81465b..f9ebc713d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -10,8 +10,17 @@ **/ #include "smt/smt_engine.h" +#include "util/exception.h" +#include "util/command.h" namespace CVC4 { +void doCommand(Command* c) { + if(c->getSmtEngine() != this) + throw new IllegalArgumentException("SmtEngine does not match Command"); + + c->invoke(); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 149de058e..af2f45c23 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -15,7 +15,6 @@ #include <vector> #include "expr/expr.h" #include "expr/expr_manager.h" -#include "util/command.h" #include "util/result.h" #include "util/model.h" #include "util/options.h" @@ -26,6 +25,8 @@ namespace CVC4 { +class Command; + // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? @@ -84,7 +85,7 @@ public: /* * Construct an SmtEngine with the given expression manager and user options. */ - SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {} + SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {} /** * Execute a command. @@ -106,6 +107,12 @@ public: Result query(Expr); /** + * Add a formula to the current context and call check(). Returns + * true iff consistent. + */ + Result checkSat(Expr); + + /** * Simplify a formula without doing "much" work. Requires assist * from the SAT Engine. */ |