diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f30a98935..df2e47b5b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -263,7 +263,7 @@ class CVC4_PUBLIC SmtEngine { * Fully type-check the argument, and also type-check that it's * actually Boolean. */ - void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException); + void ensureBoolean(const Expr& e) throw(TypeCheckingException); void internalPush(); @@ -362,20 +362,20 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(const BoolExpr& e) throw(TypeCheckingException); + Result assertFormula(const Expr& 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) throw(TypeCheckingException); + Result query(const Expr& 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()) throw(TypeCheckingException); + Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException); /** * Simplify a formula without doing "much" work. Does not involve |