diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.h | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h new file mode 100644 index 000000000..078bf9cde --- /dev/null +++ b/src/smt/smt_engine.h @@ -0,0 +1,116 @@ +/********************* -*- 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 */ |