From d26cd7a159bb56f492e21b7536f68abf821ca02a Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Fri, 11 Dec 2009 04:00:14 +0000 Subject: Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager. --- src/smt/smt_engine.cpp | 45 +++++++++++------ src/smt/smt_engine.h | 134 ++++++++++++++++++++++++++----------------------- 2 files changed, 100 insertions(+), 79 deletions(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4ccdd07d0..723263177 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -15,24 +15,39 @@ namespace CVC4 { +SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : + d_public_em(em), + d_em(em->getNodeManager()), + d_opts(opts), + d_de(), + d_te(), + d_prop(d_de, d_te) { + } + +SmtEngine::~SmtEngine() { + +} + void SmtEngine::doCommand(Command* c) { c->invoke(this); } -Node SmtEngine::preprocess(Node e) { +Node SmtEngine::preprocess(const Node& e) { return e; } -void SmtEngine::processAssertionList() { +Node SmtEngine::processAssertionList() { + Node asserts; for(std::vector::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) - d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i); + asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i); + return asserts; } Result SmtEngine::check() { - processAssertionList(); - d_prop.solve(d_expr); + Node asserts = processAssertionList(); + d_prop.solve(asserts); return Result(Result::VALIDITY_UNKNOWN); } @@ -41,25 +56,25 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEngine::addFormula(Node e) { +void SmtEngine::addFormula(const Node& e) { d_assertions.push_back(e); } -Result SmtEngine::checkSat(Node e) { - e = preprocess(e); - addFormula(e); +Result SmtEngine::checkSat(const BoolExpr& e) { + Node node_e = preprocess(e.getNode()); + addFormula(node_e); return check(); } -Result SmtEngine::query(Node e) { - e = preprocess(e); - addFormula(e); +Result SmtEngine::query(const BoolExpr& e) { + Node node_e = preprocess(e.getNode()); + addFormula(node_e); return check(); } -Result SmtEngine::assertFormula(Node e) { - e = preprocess(e); - addFormula(e); +Result SmtEngine::assertFormula(const BoolExpr& e) { + Node node_e = preprocess(e.getNode()); + addFormula(node_e); return quickCheck(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c4addc7dd..edcbdcca3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -16,7 +16,9 @@ #include "cvc4_config.h" #include "expr/node.h" +#include "expr/expr.h" #include "expr/node_manager.h" +#include "expr/expr_manager.h" #include "util/result.h" #include "util/model.h" #include "util/options.h" @@ -42,73 +44,19 @@ class Command; // // 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 d_assertions; - - /** Our expression manager */ - NodeManager *d_em; - - /** User-level options */ - Options *d_opts; - - /** Expression built-up for handing off to the propagation engine */ - Node d_expr; - - /** The decision engine */ - DecisionEngine d_de; - - /** The decision engine */ - TheoryEngine d_te; - - /** The propositional engine */ - PropEngine d_prop; - - /** - * Pre-process an Node. This is expected to be highly-variable, - * with a lot of "source-level configurability" to add multiple - * passes over the Node. TODO: may need to specify a LEVEL of - * preprocessing (certain contexts need more/less ?). - */ - Node preprocess(Node); +class CVC4_PUBLIC SmtEngine { - /** - * Adds a formula to the current context. - */ - void addFormula(Node); - - /** - * Full check of consistency in current context. Returns true iff - * consistent. - */ - Result check(); +public: /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). + * Construct an SmtEngine with the given expression manager and user options. */ - Result quickCheck(); + SmtEngine(ExprManager* em, Options* opts) throw(); /** - * 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. + * Destruct the smt engine. */ - SmtEngine(NodeManager* em, Options* opts) throw() : - d_em(em), - d_opts(opts), - d_expr(Node::null()), - d_de(), - d_te(), - d_prop(d_de, d_te) { - } + ~SmtEngine(); /** * Execute a command. @@ -121,25 +69,25 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(Node); + Result assertFormula(const BoolExpr& e); /** * Add a formula to the current context and call check(). Returns * true iff consistent. */ - Result query(Node); + Result query(const BoolExpr& e); /** * Add a formula to the current context and call check(). Returns * true iff consistent. */ - Result checkSat(Node); + Result checkSat(const BoolExpr& e); /** * Simplify a formula without doing "much" work. Requires assist * from the SAT Engine. */ - Node simplify(Node); + Expr simplify(const Expr& e); /** * Get a (counter)model (only if preceded by a SAT or INVALID query. @@ -155,6 +103,64 @@ public: * Pop a user-level context. Throws an exception if nothing to pop. */ void pop(); + +private: + + /** Current set of assertions. */ + // TODO: make context-aware to handle user-level push/pop. + std::vector d_assertions; + + /** Our expression manager */ + ExprManager *d_public_em; + + /** Out internal expression/node manager */ + NodeManager *d_em; + + /** User-level options */ + Options *d_opts; + + /** The decision engine */ + DecisionEngine d_de; + + /** The decision engine */ + TheoryEngine d_te; + + /** The propositional engine */ + PropEngine d_prop; + + /** + * Pre-process an Node. This is expected to be highly-variable, + * with a lot of "source-level configurability" to add multiple + * passes over the Node. TODO: may need to specify a LEVEL of + * preprocessing (certain contexts need more/less ?). + */ + Node preprocess(const Node& e); + + /** + * Adds a formula to the current context. + */ + void addFormula(const Node& e); + + /** + * 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. + */ + Node processAssertionList(); + + };/* class SmtEngine */ }/* CVC4 namespace */ -- cgit v1.2.3