diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
commit | 64d530e5b9096e66398f92d93cf7bc4268df0e70 (patch) | |
tree | 189d63541053faca0c778b0c92d84db8d2b1e0ff /src/prop/prop_engine.h | |
parent | 842fd54de1da122f4c7274796550c2fe21c11db2 (diff) |
Addressed many of the concerns of bug 10 (build system code review).
Some parts split into other bugs: 19, 20, 21.
Addressed concerns of bug 11 (util package code review).
Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers
Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when
verbosity is not requested.
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 9f5f9dac1..181c0288e 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -23,6 +23,7 @@ #include "theory/theory_engine.h" #include "prop/minisat/simp/SimpSolver.h" #include "prop/minisat/core/SolverTypes.h" +#include "util/result.h" #include <map> #include "prop/cnf_stream.h" @@ -31,6 +32,8 @@ namespace CVC4 { namespace prop { class CnfStream; } + + class Options; } namespace CVC4 { @@ -40,20 +43,16 @@ namespace CVC4 { // propositional solver, DPLL or otherwise. class PropEngine { + const Options *d_opts; DecisionEngine &d_de; TheoryEngine &d_te; friend class CVC4::prop::CnfStream; - /* Morgan: I added these back. - * Why did you push these into solve()? - * I am guessing this is for either a technical reason I'm not seeing, - * or that you wanted to have a clean restart everytime solve() was called - * and to start from scratch everytime. (Avoid push/pop problems?) - * Is this right? + /** + * The SAT solver. */ - CVC4::prop::minisat::Solver * d_sat; - + CVC4::prop::minisat::Solver* d_sat; std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit; std::map<CVC4::prop::minisat::Lit, Node> d_lit2atom; @@ -101,7 +100,9 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&); + CVC4_PUBLIC PropEngine(const CVC4::Options* opts, + CVC4::DecisionEngine&, + CVC4::TheoryEngine&); CVC4_PUBLIC ~PropEngine(); /** @@ -115,7 +116,7 @@ public: * and invokes the sat solver for a satisfying assignment. * TODO: what does well-formed mean here? */ - void solve(); + Result solve(); };/* class PropEngine */ |