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.cpp | |
parent | 86716e3782aae62a38987f7f89bdf5498eca534a (diff) |
Switched cnf conversion to go through CnfStream.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 57 |
1 files changed, 6 insertions, 51 deletions
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); } |