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/smt/smt_engine.h | |
parent | 95e5ca98d4c22897c0192a78ebeeb05e4838db2b (diff) |
fixups, file comments
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 116 |
1 files changed, 0 insertions, 116 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h deleted file mode 100644 index 078bf9cde..000000000 --- a/src/smt/smt_engine.h +++ /dev/null @@ -1,116 +0,0 @@ -/********************* -*- C++ -*- */ -/** prover.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__SMT__SMT_ENGINE_H -#define __CVC4__SMT__SMT_ENGINE_H - -#include <vector> -#include "core/cvc4_expr.h" -#include "core/result.h" -#include "core/model.h" - -// In terms of abstraction, this is below (and provides services to) -// ValidityChecker and above (and requires the services of) -// PropEngine. - -namespace CVC4 { -namespace smt { - -// 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: - /** - * 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::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__SMT_ENGINE_H */ |