diff options
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 11 |
1 files changed, 9 insertions, 2 deletions
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. */ |