diff options
Diffstat (limited to 'src/include/cvc4.h')
-rw-r--r-- | src/include/cvc4.h | 115 |
1 files changed, 0 insertions, 115 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h deleted file mode 100644 index bbaffabb0..000000000 --- a/src/include/cvc4.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc4.h - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - **/ - -#ifndef __CVC4_H -#define __CVC4_H - -#include <vector> -#include "cvc4_expr.h" -#include "util/command.h" -#include "util/result.h" -#include "util/model.h" - -namespace CVC4 { - -class SmtEngine { - /** Current set of assertions. */ - // TODO: make context-aware to handle user-level push/pop. - std::vector<Expr> d_assertList; - - /** 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 - * passes over the Expr. TODO: may need to specify a LEVEL of - * preprocessing (certain contexts need more/less ?). - */ - void preprocess(Expr); - - /** - * Adds a formula to the current context. - */ - void addFormula(Expr); - - /** - * Full check of consistency in current context. Returns true iff - * consistent. - */ - Result check(); - - /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). - */ - Result quickCheck(); - - /** - * Process the assertion list: for literals and conjunctions of - * literals, assert to T-solver. - */ - void processAssertionList(); - -public: - /* - * Construct an SmtEngine with the given expression manager and user options. - */ - SmtEngine(ExprManager*, Options*) throw(); - - /** - * Execute a command. - */ - void doCommand(Command*); - - /** - * Add a formula to the current context: preprocess, do per-theory - * setup, use processAssertionList(), asserting to T-solver for - * literals and conjunction of literals. Returns false iff - * inconsistent. - */ - Result assert(Expr); - - /** - * Add a formula to the current context and call check(). Returns - * true iff consistent. - */ - Result query(Expr); - - /** - * Simplify a formula without doing "much" work. Requires assist - * from the SAT Engine. - */ - Expr simplify(Expr); - - /** - * Get a (counter)model (only if preceded by a SAT or INVALID query. - */ - Model getModel(); - - /** - * Push a user-level context. - */ - void push(); - - /** - * Pop a user-level context. Throws an exception if nothing to pop. - */ - void pop(); -};/* class SmtEngine */ - -}/* CVC4 namespace */ - -#endif /* __CVC4_H */ |