diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-02-02 20:56:47 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-02-02 20:56:47 +0000 |
| commit | a8588cb23c5257bb11a70348346476b55317faa3 (patch) | |
| tree | 34bead7e2b760d813ee02d04a9dec091eedbc745 /src/smt/smt_engine.h | |
| parent | 86716e3782aae62a38987f7f89bdf5498eca534a (diff) | |
Switched cnf conversion to go through CnfStream.
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b073a68c9..097500833 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -29,7 +29,6 @@ #include "util/options.h" #include "prop/prop_engine.h" #include "util/decision_engine.h" -#include "smt/cnf_converter.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -134,8 +133,6 @@ private: /** The propositional engine */ PropEngine d_prop; - /** The CNF converter in use */ - CVC4::smt::CnfConverter d_cnfConverter; /** * Pre-process an Node. This is expected to be highly-variable, @@ -167,7 +164,7 @@ private: * Process the assertion list: for literals and conjunctions of * literals, assert to T-solver. */ - Node processAssertionList(); + void processAssertionList(); };/* class SmtEngine */ |