diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
commit | cf287f593931a1c4fc141e18845b4c5d36879889 (patch) | |
tree | 4dad0f555b7db01fbeedcd9eace394cd8f7a0fb4 /src/smt/smt_engine.h | |
parent | b7b1c1d99ffa333704af2c8ecd60b1af8833a28b (diff) |
Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 43a7ee58d..25800f5b3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -234,7 +234,7 @@ class CVC4_PUBLIC SmtEngine { * Fully type-check the argument, and also type-check that it's * actually Boolean. */ - void ensureBoolean(const BoolExpr& e); + void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException); void internalPush(); @@ -337,20 +337,20 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(const BoolExpr& e); + Result assertFormula(const BoolExpr& e) throw(TypeCheckingException); /** * Check validity of an expression with respect to the current set * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const BoolExpr& e); + Result query(const BoolExpr& e) throw(TypeCheckingException); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const BoolExpr& e = BoolExpr()); + Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException); /** * Simplify a formula without doing "much" work. Does not involve @@ -361,7 +361,7 @@ public: * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify(const Expr& e); + Expr simplify(const Expr& e) throw(TypeCheckingException); /** * Get the assigned value of an expr (only if immediately preceded |