diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e06a36128..65375ab65 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -29,6 +29,7 @@ #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) @@ -116,7 +117,7 @@ private: std::vector<Node> d_assertions; /** Our expression manager */ - ExprManager *d_public_em; + ExprManager *d_publicEm; /** Out internal expression/node manager */ NodeManager *d_nm; @@ -133,6 +134,9 @@ 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, * with a lot of "source-level configurability" to add multiple @@ -165,11 +169,6 @@ private: */ Node processAssertionList(); - /** - * Helper method for CNF preprocessing. CNF-converts an OR. - */ - void orHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result); - };/* class SmtEngine */ }/* CVC4 namespace */ |