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 | |
parent | 86716e3782aae62a38987f7f89bdf5498eca534a (diff) |
Switched cnf conversion to go through CnfStream.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 5 | ||||
-rw-r--r-- | src/smt/cnf_conversion.h | 46 | ||||
-rw-r--r-- | src/smt/cnf_converter.cpp | 431 | ||||
-rw-r--r-- | src/smt/cnf_converter.h | 170 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 57 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
6 files changed, 8 insertions, 706 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index fa7fed5f1..a2da2c949 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -7,7 +7,4 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ - smt_engine.h \ - cnf_converter.h \ - cnf_converter.cpp \ - cnf_conversion.h + smt_engine.h diff --git a/src/smt/cnf_conversion.h b/src/smt/cnf_conversion.h deleted file mode 100644 index 924cae063..000000000 --- a/src/smt/cnf_conversion.h +++ /dev/null @@ -1,46 +0,0 @@ -/********************* -*- C++ -*- */ -/** cnf_conversion.h - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A type for describing possible CNF conversions. - **/ - -#ifndef __CVC4__CNF_CONVERSION_H -#define __CVC4__CNF_CONVERSION_H - -namespace CVC4 { - -enum CnfConversion { - CNF_DIRECT_EXPONENTIAL = 0, - CNF_VAR_INTRODUCTION = 1 -}; - -inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) { - using namespace CVC4; - - switch(c) { - case CNF_DIRECT_EXPONENTIAL: - out << "CNF_DIRECT_EXPONENTIAL"; - break; - case CNF_VAR_INTRODUCTION: - out << "CNF_VAR_INTRODUCTION"; - break; - default: - out << "UNKNOWN-CONVERTER!" << int(c); - } - - return out; -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__CNF_CONVERSION_H */ diff --git a/src/smt/cnf_converter.cpp b/src/smt/cnf_converter.cpp deleted file mode 100644 index 7c53e9b04..000000000 --- a/src/smt/cnf_converter.cpp +++ /dev/null @@ -1,431 +0,0 @@ -/********************* -*- C++ -*- */ -/** cnf_converter.cpp - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A CNF converter for CVC4. - **/ - -#include "smt/cnf_converter.h" -#include "expr/node_builder.h" -#include "expr/node.h" -#include "util/output.h" -#include "util/Assert.h" - -namespace CVC4 { -namespace smt { - -static void printAST(std::ostream& out, const Node& n, int indent = 0) { - for(int i = 0; i < indent; ++i) { - out << " "; - } - if(n.getKind() == VARIABLE) { - out << "(VARIABLE " << n.getId(); - } else { - out << "(" << n.getKind(); - if(n.getNumChildren() > 0) { - out << std::endl; - } - for(Node::iterator i = n.begin(); i != n.end(); ++i) { - printAST(out, *i, indent + 1); - } - if(n.getNumChildren() > 0) { - for(int i = 0; i < indent; ++i) { - out << " "; - } - } - } - out << ")" << std::endl; -} - -Node CnfConverter::convert(const Node& e) { - if(d_conversion == CNF_DIRECT_EXPONENTIAL) { - return doConvert(e, NULL); - } - - NodeBuilder<> b(AND); - Node f = doConvert(e, &b); - - Debug("cnf") << "side conditions are:\n"; - NodeBuilder<> c = b; - printAST(Debug("cnf"), c); - - if(f.getKind() == AND) { - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - Debug("cnf") << "adding condition:\n"; - printAST(Debug("cnf"), *i); - b << *i; - } - } else { - Debug("cnf") << "adding condition:\n"; - printAST(Debug("cnf"), f); - b << f; - } - return b; -} - -Node CnfConverter::doConvert(const Node& e, NodeBuilder<>* sideConditions) { - Node n; - - if(conversionMapped(e)) { - Debug("cnf") << "conversion for " << e << " with id " << e.getId() << " is cached!" << std::endl; - n = getConversionMap(e); - } else { - switch(d_conversion) { - - case CNF_DIRECT_EXPONENTIAL: - Debug("cnf") << "direct conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl; - n = directConvert(e, sideConditions); - break; - - case CNF_VAR_INTRODUCTION: { - Debug("cnf") << "var-intro conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl; - std::vector<Node> v; - n = varIntroductionConvert(e, sideConditions); - Debug("cnf") << "got" << std::endl; - printAST(Debug("cnf"), n); - - break; - } - - default: - Unhandled(d_conversion); - } - - Debug("cnf") << "mapping conversion " << e << " with id " << e.getId() << " to " << n << " with id " << n.getId() << std::endl; - mapConversion(e, n); - Assert(conversionMapped(e)); - Assert(getConversionMap(e) == n); - } - - Debug("cnf") << "CONVERTED ================" << std::endl; - printAST(Debug("cnf"), e); - Debug("cnf") << "TO ================" << std::endl; - printAST(Debug("cnf"), n); - Debug("cnf") << "==========================" << std::endl; - - return n; -} - -Node CnfConverter::compressNOT(const Node& e, NodeBuilder<>* sideConditions) { - Assert(e.getKind() == NOT); - - Node f = doConvert(e[0], sideConditions); - - Debug("stari") << "compress-not " << e.getId() << "\n"; - - // short-circuit trivial NOTs - if(f.getKind() == TRUE) { - return d_nm->mkNode(FALSE); - } else if(f.getKind() == FALSE) { - return d_nm->mkNode(TRUE); - } else if(f.getKind() == NOT) { - return doConvert(f[0], sideConditions); - } else if(f.getKind() == AND) { - Debug("stari") << "not-converting a NOT AND\nstarted with\n"; - printAST(Debug("stari"), e[0]); - Debug("stari") << "now have\n"; - printAST(Debug("stari"), f); - NodeBuilder<> n(OR); - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - if((*i).getKind() == NOT) { - n << (*i)[0]; - } else { - n << d_nm->mkNode(NOT, *i); - } - } - return n; - } else if(f.getKind() == OR) { - NodeBuilder<> n(AND); - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - if((*i).getKind() == NOT) { - n << (*i)[0]; - } else { - n << d_nm->mkNode(NOT, *i); - } - } - return n; - } else { - return d_nm->mkNode(NOT, f); - } -} - - -Node CnfConverter::directConvert(const Node& e, NodeBuilder<>* sideConditions) { - switch(e.getKind()) { - - case NOT: - return compressNOT(e, sideConditions); - - case AND: - return flatten<AND>(e, sideConditions); - - case OR: { - Node n = flatten<OR>(e, sideConditions); - - NodeBuilder<> m(OR); - Debug("dor") << "calling directOrHelper on\n"; - printAST(Debug("dor"), n); - directOrHelper(n.begin(), n.end(), m, sideConditions); - - return m; - } - - case IMPLIES: { - Assert( e.getNumChildren() == 2 ); - // just turn x IMPLIES y into (NOT x) OR y - Node x = doConvert(e[0], sideConditions); - Node y = doConvert(e[1], sideConditions); - return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions); - } - - case IFF: - if(e.getNumChildren() == 2) { - // common case: - // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) - Node x = doConvert(e[0], sideConditions); - Node y = doConvert(e[1], sideConditions); - Node r = d_nm->mkNode(OR, - doConvert(d_nm->mkNode(AND, x, y), sideConditions), - doConvert(d_nm->mkNode(AND, - doConvert(d_nm->mkNode(NOT, x), sideConditions), - doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); - Debug("cnf") << "working on an IFF\n"; - printAST(Debug("cnf"), e); - Debug("cnf") << "which is\n"; - printAST(Debug("cnf"), r); - return doConvert(r, sideConditions); - } else { - // more than 2 children: - // treat x IFF y IFF z as (x IFF y) AND (y IFF z) ... - Node::iterator i = e.begin(); - Node x = doConvert(*i++, sideConditions); - NodeBuilder<> r(AND); - while(i != e.end()) { - Node y = doConvert(*i++, sideConditions); - // now we just have two: - // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) - r << d_nm->mkNode(OR, - doConvert(d_nm->mkNode(AND, x, y), sideConditions), - doConvert(d_nm->mkNode(AND, - doConvert(d_nm->mkNode(NOT, x), sideConditions), - doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); - x = y; - } - return doConvert(r, sideConditions); - } - - case XOR: - Assert( e.getNumChildren() == 2 ); - // just turn x XOR y into (x AND (NOT y)) OR ((NOT x) AND y) - return doConvert(d_nm->mkNode(OR, - d_nm->mkNode(AND, - e[0], - d_nm->mkNode(NOT, e[1])), - d_nm->mkNode(AND, - d_nm->mkNode(NOT, e[0]), - e[1])), sideConditions); - - default: - // variable or theory atom - return e; - } -} - -/** - * OR: all ORs and NOTs - * -- do nothing - * - * find an AND. - * prefix: a \/ b \/ c - * and term: d /\ e - * rest: f \/ g \/ h - * - * construct: prefix \/ child - * - * then, process rest. - * - * if rest has no additional ANDs - * then I get prefix \/ child \/ rest - * and I do same with other children - * - * if rest has additional ANDs - * then I get (prefix \/ child \/ rest'1) /\ (prefix \/ child \/ rest'2) /\ ... - * and I do same with other children - */ -void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>* sideConditions) { - static int nextID = 0; - int ID = ++nextID; - Debug("dor") << "beginning of directOrHelper " << ID << "\n"; - - while(p != end) { - // for each child of the expression: - - Debug("dor") << "CHILD == directOrHelper " << ID << "\n"; - printAST(Debug("dor"), *p); - - // convert the child first - Node n = doConvert(*p, sideConditions); - - Debug("dor") << "CNV CHILD == directOrHelper " << ID << "\n"; - printAST(Debug("dor"), *p); - - // if the child is an AND - if(n.getKind() == AND) { - Debug("dor") << "directOrHelper found AND " << ID << "\n"; - - NodeBuilder<> prefix = result; - result.clear(AND); - - for(Node::iterator i = n.begin(); i != n.end(); ++i) { - // for each child of the AND - NodeBuilder<> r = prefix; - - Debug("dor") << "directOrHelper AND " << ID << ", converting\n"; - printAST(Debug("dor"), *i); - - r << doConvert(*i, sideConditions); - NodeBuilder<> rx = r; - Debug("dor") << "prefix \\/ child is " << ID << "\n"; - printAST(Debug("dor"), rx); - Node::iterator p2 = p; - directOrHelper(++p2, end, r, sideConditions); - - Debug("dor") << "directOrHelper recursion done " << ID << "\n"; - Node rr = r; - Debug("dor") << "directOrHelper subterm of AND " << ID << "\n"; - printAST(Debug("dor"), rr); - - result << rr; - } - - Debug("dor") << "end of directOrHelper AND " << ID << "\n"; - NodeBuilder<> resultnb = result; - printAST(Debug("dor"), resultnb); - - return; - } else { - // if it's not an AND, pass it through, it's fine - result << n; - } - - Debug("cnf") << " ** result now " << result << std::endl; - - ++p; - } - - Debug("dor") << "end of directOrHelper NO AND " << ID << "\n"; - NodeBuilder<> resultnb = result; - printAST(Debug("dor"), resultnb); -} - -Node CnfConverter::varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions) { - switch(e.getKind()) { - - case NOT: { - Node f = compressNOT(e, sideConditions); - Debug("stari") << "compressNOT:\n"; - printAST(Debug("stari"), e); - printAST(Debug("stari"), f); - return f; - } - - case AND: { - Node n = flatten<AND>(e, sideConditions); - Node var = d_nm->mkVar(); - Node notVar = d_nm->mkNode(NOT, var); - for(Node::iterator i = n.begin(); i != n.end(); ++i) { - // *i has already been converted by flatten<>() - if((*i).getKind() == OR) { - NodeBuilder<> b(OR); - b << notVar; - for(Node::iterator j = (*i).begin(); j != (*i).end(); ++j) { - b << *j; - } - *sideConditions << b; - } else { - Debug("stari") << "*i should have been flattened:\n"; - printAST(Debug("stari"), *i); - Node x = convert(*i); - printAST(Debug("stari"), x); - //Assert(x == *i); - *sideConditions << d_nm->mkNode(OR, notVar, *i); - } - } - - return var; - } - - case OR: - return flatten<OR>(e, sideConditions); - - case IMPLIES: { - Assert( e.getNumChildren() == 2 ); - // just turn x IMPLIES y into (NOT x) OR y - Node x = doConvert(e[0], sideConditions); - Node y = doConvert(e[1], sideConditions); - return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions); - } - - case IFF: - if(e.getNumChildren() == 2) { - // common case: - // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) - Node x = doConvert(e[0], sideConditions); - Node y = doConvert(e[1], sideConditions); - Node r = d_nm->mkNode(OR, - doConvert(d_nm->mkNode(AND, x, y), sideConditions), - doConvert(d_nm->mkNode(AND, - doConvert(d_nm->mkNode(NOT, x), sideConditions), - doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); - Debug("cnf") << "working on an IFF\n"; - printAST(Debug("cnf"), e); - Debug("cnf") << "which is\n"; - printAST(Debug("cnf"), r); - return doConvert(r, sideConditions); - } else { - // more than 2 children: - // treat x IFF y IFF z as (x IFF y) AND (y IFF z) ... - Node::iterator i = e.begin(); - Node x = doConvert(*i++, sideConditions); - NodeBuilder<> r(AND); - while(i != e.end()) { - Node y = doConvert(*i++, sideConditions); - // now we just have two: - // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) - r << d_nm->mkNode(OR, - doConvert(d_nm->mkNode(AND, x, y), sideConditions), - doConvert(d_nm->mkNode(AND, - doConvert(d_nm->mkNode(NOT, x), sideConditions), - doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); - x = y; - } - return doConvert(r, sideConditions); - } - - case XOR: - Assert( e.getNumChildren() == 2 ); - // just turn x XOR y into (x AND (NOT y)) OR ((NOT x) AND y) - return doConvert(d_nm->mkNode(OR, - d_nm->mkNode(AND, - e[0], - d_nm->mkNode(NOT, e[1])), - d_nm->mkNode(AND, - d_nm->mkNode(NOT, e[0]), - e[1])), sideConditions); - - default: - // variable or theory atom - return e; - } -} - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h deleted file mode 100644 index 7b7be0480..000000000 --- a/src/smt/cnf_converter.h +++ /dev/null @@ -1,170 +0,0 @@ -/********************* -*- C++ -*- */ -/** cnf_converter.h - ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** A CNF converter for CVC4. - **/ - -#ifndef __CVC4__SMT__CNF_CONVERTER_H -#define __CVC4__SMT__CNF_CONVERTER_H - -#include "expr/node_builder.h" -#include "expr/node.h" -#include "smt/cnf_conversion.h" - -#include <map> - -namespace CVC4 { -namespace smt { - -class CnfConverter { - -private: - - /** Our node manager */ - NodeManager *d_nm; - - /** The type of conversion this converter performs */ - CVC4::CnfConversion d_conversion; - - /** Map of already-converted Nodes */ - std::map<Node, Node> d_conversionMap; - - /** - * Returns true iff the CNF conversion for the Node was cached - * previously. - */ - bool conversionMapped(const Node& n) { - return d_conversionMap.find(n) != d_conversionMap.end(); - } - - /** - * Returns true iff the CNF conversion for the Node was cached - * previously. - */ - Node getConversionMap(const Node& n) { - return d_conversionMap[n]; - } - - /** - * Cache a new CNF conversion. - */ - void mapConversion(const Node& n, const Node& m) { - d_conversionMap[n] = m; - } - - /** - * Compress a NOT: do NNF transformation plus a bit. Does DNE, - * NOT FALSE ==> TRUE, NOT TRUE ==> FALSE, and pushes NOT inside - * of ANDs and ORs. Calls doConvert() on subnodes. - */ - Node compressNOT(const Node& e, NodeBuilder<>* sideConditions); - - /** - * Flatten a Node of kind K. K here is going to be AND or OR. - * "Flattening" means to take all children of the Node with the same - * kind and hoist their children to the top-level. So e.g. - * (AND (AND x y) (AND (AND z)) w) ==> (AND x y z w). - */ - template <CVC4::Kind K> - Node flatten(const Node& e, NodeBuilder<>* sideConditions); - - /** - * Do a direct CNF conversion (with possible exponential blow-up in - * the number of clauses). No new variables are introduced. The - * output is equivalent to the input. - */ - Node directConvert(const Node& e, NodeBuilder<>* sideConditions); - - /** - * Helper method for "direct" CNF preprocessing. CNF-converts an OR. - */ - void directOrHelper(Node::iterator p, - Node::iterator end, - NodeBuilder<>& result, - NodeBuilder<>* sideConditions); - - /** - * Do a satisfiability-preserving CNF conversion with variable - * introduction. Doesn't suffer from exponential blow-up in the - * number of clauses, but new variables are introduced and the - * output is equisatisfiable (but not equivalent) to the input. - */ - Node varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions); - - /** - * Convert an expression into CNF. If a conversion already exists - * for the Node, it is returned. If a conversion doesn't exist, it - * is computed and returned (caching the result). - */ - Node doConvert(const Node& e, NodeBuilder<>* sideconditions); - -public: - - /** - * Construct a CnfConverter. - */ - CnfConverter(NodeManager* nm, CVC4::CnfConversion cnv = CNF_VAR_INTRODUCTION) : - d_nm(nm), - d_conversion(cnv) {} - - /** - * Convert an expression into CNF. If a conversion already exists - * for the Node, it is returned. If a conversion doesn't exist, it - * is computed and returned (caching the result). - */ - Node convert(const Node& e); - -};/* class CnfConverter */ - -template <CVC4::Kind K> -struct flatten_traits; - -template <> -struct flatten_traits<AND> { - static const CVC4::Kind ignore = TRUE; // TRUE AND x == x - static const CVC4::Kind shortout = FALSE; // FALSE AND x == FALSE -}; - -template <> -struct flatten_traits<OR> { - static const CVC4::Kind ignore = FALSE; // FALSE OR x == x - static const CVC4::Kind shortout = TRUE; // TRUE OR x == TRUE -}; - -template <CVC4::Kind K> -Node CnfConverter::flatten(const Node& e, NodeBuilder<>* sideConditions) { - Assert(e.getKind() == K); - - NodeBuilder<> n(K); - - for(Node::iterator i = e.begin(); i != e.end(); ++i) { - Node f = doConvert(*i, sideConditions); - if(f.getKind() == K) { - for(Node::iterator j = f.begin(); j != f.end(); ++j) { - n << *j; - } - } else if(f.getKind() == flatten_traits<K>::ignore) { - /* do nothing */ - } else if(f.getKind() == flatten_traits<K>::shortout) { - return f; - } else { - n << f; - } - } - - return n; -} - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__CNF_CONVERTER_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c0f825462..7e2b6e24c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,8 +27,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : d_opts(opts), d_de(), d_te(), - d_prop(d_de, d_te), - d_cnfConverter(d_nm, opts->d_cnfConversion) { + d_prop(d_de, d_te){ } SmtEngine::~SmtEngine() { @@ -43,62 +42,18 @@ Node SmtEngine::preprocess(const Node& e) { return e; } -Node SmtEngine::processAssertionList() { - if(d_assertions.size() == 1) { - return d_assertions[0]; +void SmtEngine::processAssertionList() { + for(unsigned i = 0; i < d_assertions.size(); ++i) { + d_prop.assertFormula(d_assertions[i]); } - - NodeBuilder<> asserts(AND); - for(std::vector<Node>::iterator i = d_assertions.begin(); - i != d_assertions.end(); - ++i) { - asserts << *i; - } - d_assertions.clear(); - d_assertions.push_back(asserts); - return d_assertions[0]; } -static void printAST(std::ostream& out, const Node& n, int indent = 0) { - for(int i = 0; i < indent; ++i) { - out << " "; - } - if(n.getKind() == VARIABLE) { - out << "(VARIABLE " << n.getId(); - } else { - out << "(" << n.getKind(); - if(n.getNumChildren() > 0) { - out << std::endl; - } - for(Node::iterator i = n.begin(); i != n.end(); ++i) { - printAST(out, *i, indent + 1); - } - if(n.getNumChildren() > 0) { - for(int i = 0; i < indent; ++i) { - out << " "; - } - } - } - out << ")" << std::endl; -} Result SmtEngine::check() { Debug("smt") << "SMT check()" << std::endl; - Node asserts = processAssertionList(); - - // CNF conversion - Debug("cnf") << "preprocessing " << asserts << std::endl; - Node assertsOut = d_cnfConverter.convert(asserts); - Debug("cnf") << " and got " << assertsOut << std::endl; - - Debug("smt") << "BEFORE CONVERSION ==" << std::endl; - printAST(Debug("smt"), asserts); - Debug("smt") << "AFTER CONVERSION ==" << std::endl; - printAST(Debug("smt"), assertsOut); - Debug("smt") << "===================" << std::endl; - - d_prop.solve(assertsOut); + processAssertionList(); + d_prop.solve(); return Result(Result::VALIDITY_UNKNOWN); } 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 */ |