diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-04 23:50:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-04 23:50:23 +0000 |
commit | dc4b8296ded0a2288fbfeb71b9ded9217bad6b86 (patch) | |
tree | 7bb1a9d305c46464e0470486e406cdffa9558644 /src/smt | |
parent | fb7d93e00e70b36d12c1d5deec914426c982b3cf (diff) |
beautification of the prop engine
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 15 |
2 files changed, 23 insertions, 15 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1555acb7d..a04d16d06 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -13,11 +13,14 @@ **/ #include "smt/smt_engine.h" -#include "util/exception.h" #include "expr/command.h" -#include "util/output.h" #include "expr/node_builder.h" +#include "util/output.h" +#include "util/exception.h" #include "util/options.h" +#include "prop/prop_engine.h" + +using namespace CVC4::prop; namespace CVC4 { @@ -25,13 +28,17 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_assertions(), d_publicEm(em), d_nm(em->getNodeManager()), - d_opts(opts), - d_de(), - d_te(), - d_prop(opts, d_de, d_te) { + d_opts(opts) +{ + d_de = new DecisionEngine(); + d_te = new TheoryEngine(); + d_prop = new PropEngine(opts, d_de, d_te); } SmtEngine::~SmtEngine() { + delete d_prop; + delete d_te; + delete d_de; } void SmtEngine::doCommand(Command* c) { @@ -45,7 +52,7 @@ Node SmtEngine::preprocess(const Node& e) { void SmtEngine::processAssertionList() { for(unsigned i = 0; i < d_assertions.size(); ++i) { - d_prop.assertFormula(d_assertions[i]); + d_prop->assertFormula(d_assertions[i]); } d_assertions.clear(); } @@ -54,7 +61,7 @@ void SmtEngine::processAssertionList() { Result SmtEngine::check() { Debug("smt") << "SMT check()" << std::endl; processAssertionList(); - return d_prop.solve(); + return d_prop->solve(); } Result SmtEngine::quickCheck() { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 79a35a6a1..eb9384ca5 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -19,14 +19,10 @@ #include <vector> #include "cvc4_config.h" -#include "expr/node.h" #include "expr/expr.h" -#include "expr/node_manager.h" -#include "expr/node_builder.h" #include "expr/expr_manager.h" #include "util/result.h" #include "util/model.h" -#include "prop/prop_engine.h" #include "util/decision_engine.h" // In terms of abstraction, this is below (and provides services to) @@ -37,6 +33,11 @@ namespace CVC4 { class Command; class Options; +class TheoryEngine; + +namespace prop { + class PropEngine; +} // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass @@ -125,13 +126,13 @@ private: const Options* d_opts; /** The decision engine */ - DecisionEngine d_de; + DecisionEngine* d_de; /** The decision engine */ - TheoryEngine d_te; + TheoryEngine* d_te; /** The propositional engine */ - PropEngine d_prop; + prop::PropEngine* d_prop; /** |