From 044329296028ad944b703929fad4d85aa6183472 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 9 Feb 2010 23:07:33 +0000 Subject: Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser. --- src/smt/smt_engine.h | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'src/smt/smt_engine.h') diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index eb9384ca5..d796959a9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -117,23 +117,22 @@ private: std::vector d_assertions; /** Our expression manager */ - ExprManager* d_publicEm; + ExprManager* d_exprManager; /** Out internal expression/node manager */ - NodeManager* d_nm; + NodeManager* d_nodeManager; /** User-level options */ - const Options* d_opts; + const Options* d_options; /** The decision engine */ - DecisionEngine* d_de; + DecisionEngine* d_decisionEngine; /** The decision engine */ - TheoryEngine* d_te; + TheoryEngine* d_theoryEngine; /** The propositional engine */ - prop::PropEngine* d_prop; - + prop::PropEngine* d_propEngine; /** * Pre-process an Node. This is expected to be highly-variable, @@ -141,12 +140,12 @@ private: * passes over the Node. TODO: may need to specify a LEVEL of * preprocessing (certain contexts need more/less ?). */ - Node preprocess(const Node& e); + Node preprocess(const Node& node); /** * Adds a formula to the current context. */ - void addFormula(const Node& e); + void addFormula(const Node& node); /** * Full check of consistency in current context. Returns true iff -- cgit v1.2.3