diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-23 16:42:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-23 16:42:12 +0000 |
commit | f6968899de4d27c5bc986c3ac89972fbbe35c361 (patch) | |
tree | dd3461b2e08e1568ca9aff97a56e93a0445b3abc /src/include/cvc4.h | |
parent | 95e5ca98d4c22897c0192a78ebeeb05e4838db2b (diff) |
fixups, file comments
Diffstat (limited to 'src/include/cvc4.h')
-rw-r--r-- | src/include/cvc4.h | 112 |
1 files changed, 95 insertions, 17 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h index c5e3bb013..7b068228f 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** vc.h +/** 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 @@ -12,30 +12,108 @@ #ifndef __CVC4_H #define __CVC4_H -#include "util/command.h" +#include <vector> #include "cvc4_expr.h" - -/* TODO provide way of querying whether you fall into a fragment / - * returning what fragment you're in */ +#include "util/command.h" +#include "util/result.h" +#include "util/model.h" // In terms of abstraction, this is below (and provides services to) -// users using the library interface, and also the parser for the main -// CVC4 binary. It is above (and requires the services of) the Prover -// class. +// ValidityChecker and above (and requires the services of) +// PropEngine. namespace CVC4 { -/** - * User-visible (library) interface to CVC4. - */ -class ValidityChecker { - // on entry to the validity checker interface, need to set up - // current state (ExprManager::d_current etc.) +// 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: + /** + * 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: - void doCommand(Command); + /** + * Execute a command + */ + void doCommand(Command c); + + /** + * 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(); - void query(Expr); -}; + /** + * Pop a user-level context. Throws an exception if nothing to pop. + */ + void pop(); +};/* class SmtEngine */ }/* CVC4 namespace */ |