diff options
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/cvc4.h | 31 | ||||
-rw-r--r-- | src/include/cvc4_expr.h | 3 |
2 files changed, 13 insertions, 21 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 7b068228f..5d33fa838 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -18,29 +18,19 @@ #include "util/result.h" #include "util/model.h" -// In terms of abstraction, this is below (and provides services to) -// ValidityChecker and above (and requires the services of) -// PropEngine. - namespace CVC4 { -// 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()? -// -// Probably better than that is to have a configuration object that -// indicates which passes are desired. The configuration occurs -// elsewhere (and can even occur at runtime). A simple "pass manager" -// of sorts determines check()'s behavior. -// -// The CNF conversion can go on in PropEngine. - class SmtEngine { /** Current set of assertions. */ // TODO: make context-aware to handle user-level push/pop. std::vector<Expr> d_assertList; -private: + /** Our expression manager */ + ExprManager *d_em; + + /** User-level options */ + Options *opts; + /** * Pre-process an Expr. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple @@ -74,10 +64,15 @@ private: void processAssertionList(); public: + /* + * Construct an SmtEngine with the given expression manager and user options. + */ + SmtEngine(ExprManager*, Options*); + /** - * Execute a command + * Execute a command. */ - void doCommand(Command c); + void doCommand(Command*); /** * Add a formula to the current context: preprocess, do per-theory diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index d99708991..863097123 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -74,9 +74,6 @@ public: Expr iffExpr(const Expr& right) const; Expr impExpr(const Expr& right) const; Expr xorExpr(const Expr& right) const; - Expr skolemExpr(int i) const; - Expr substExpr(const std::vector<Expr>& oldTerms, - const std::vector<Expr>& newTerms) const; Expr plusExpr(const Expr& right) const; Expr uMinusExpr() const; |