diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-01-30 02:22:25 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-01-30 02:22:25 +0000 |
| commit | 39b707ad22813c184da61c3e2337359ca8061797 (patch) | |
| tree | f1e4f3476822c4da3f423dc114ca1583bdcf063e /src/prop/prop_engine.h | |
| parent | e081fe6309b02a23b81330c151876f04ad774465 (diff) | |
cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 6cb818d10..6e1f8cb61 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -35,11 +35,11 @@ namespace CVC4 { class PropEngine { DecisionEngine &d_de; TheoryEngine &d_te; - CVC4::prop::minisat::SimpSolver d_sat; - std::map<Node, CVC4::prop::minisat::Var> d_vars; - std::map<CVC4::prop::minisat::Var, Node> d_varsReverse; + //CVC4::prop::minisat::SimpSolver d_sat; + //std::map<Node, CVC4::prop::minisat::Var> d_vars; + //std::map<CVC4::prop::minisat::Var, Node> d_varsReverse; - void addVars(Node); + void addVars(CVC4::prop::minisat::SimpSolver*, std::map<Node, CVC4::prop::minisat::Var>*, std::map<CVC4::prop::minisat::Var, Node>*, Node); public: /** |