diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-10 18:44:51 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2009-12-10 18:44:51 +0000 |
commit | f79afa96e7e7176b974252dd05a9f7bdf70194e8 (patch) | |
tree | cb12c0a880f8fbb356516a86699b0063a7bb8981 /src/prop/prop_engine.h | |
parent | 8b2d1d64b886db4cff74e2a7b1370841979001b2 (diff) |
killing expr into node...
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a3355bf89..21a6669d7 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -13,7 +13,7 @@ #define __CVC4__PROP_ENGINE_H #include "cvc4_config.h" -#include "expr/expr.h" +#include "expr/node.h" #include "util/decision_engine.h" #include "theory/theory_engine.h" #include "prop/minisat/simp/SimpSolver.h" @@ -31,10 +31,10 @@ class PropEngine { DecisionEngine &d_de; TheoryEngine &d_te; CVC4::prop::minisat::SimpSolver d_sat; - std::map<Expr, CVC4::prop::minisat::Var> d_vars; - std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse; + std::map<Node, CVC4::prop::minisat::Var> d_vars; + std::map<CVC4::prop::minisat::Var, Node> d_varsReverse; - void addVars(Expr); + void addVars(Node); public: /** @@ -45,7 +45,7 @@ public: /** * Converts to CNF if necessary. */ - void solve(Expr); + void solve(Node); };/* class PropEngine */ |