diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-01-26 07:29:41 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-01-26 07:29:41 +0000 |
commit | 21e01d42ed4c0b6d9fa5855c2e0cfc1a3765d14f (patch) | |
tree | ec785ced868a294e72cc751a293c618488743c8b /src/smt | |
parent | f2d38a8522579f9b3e434f76a9426fa8d2f06d07 (diff) |
fixes to build structure, util classes, lots of fixes to Node and NodeBuilder. outstanding SEGVs fixed
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.in | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 47 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
3 files changed, 40 insertions, 11 deletions
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in index 35126e382..aa00d5e25 100644 --- a/src/smt/Makefile.in +++ b/src/smt/Makefile.in @@ -92,6 +92,8 @@ AUTOCONF = @AUTOCONF@ AUTOHEADER = @AUTOHEADER@ AUTOMAKE = @AUTOMAKE@ AWK = @AWK@ +BUILDING_SHARED = @BUILDING_SHARED@ +BUILDING_STATIC = @BUILDING_STATIC@ CC = @CC@ CCDEPMODE = @CCDEPMODE@ CFLAGS = @CFLAGS@ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4c7f6a156..018936f7c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -15,37 +15,55 @@ #include "smt/smt_engine.h" #include "util/exception.h" #include "util/command.h" +#include "util/output.h" +#include "expr/node_builder.h" namespace CVC4 { SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() : - d_public_em(em), - d_em(em->getNodeManager()), - d_opts(opts), - d_de(), - d_te(), - d_prop(d_de, d_te) { - } + d_assertions(), + d_public_em(em), + d_nm(em->getNodeManager()), + d_opts(opts), + d_de(), + d_te(), + d_prop(d_de, d_te) { +} SmtEngine::~SmtEngine() { } void SmtEngine::doCommand(Command* c) { + NodeManagerScope nms(d_nm); c->invoke(this); } Node SmtEngine::preprocess(const Node& e) { + if(e.getKind() == NOT) { + if(e[0].getKind() == TRUE) { + return d_nm->mkNode(FALSE); + } else if(e[0].getKind() == FALSE) { + return d_nm->mkNode(TRUE); + } else if(e[0].getKind() == NOT) { + return preprocess(e[0][0]); + } + } return e; } Node SmtEngine::processAssertionList() { - Node asserts; + if(d_assertions.size() == 1) { + return d_assertions[0]; + } + + NodeBuilder<> asserts(AND); for(std::vector<Node>::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) { - asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i); + asserts << *i; } + return asserts; } @@ -61,25 +79,34 @@ Result SmtEngine::quickCheck() { } void SmtEngine::addFormula(const Node& e) { + Debug("smt") << "push_back assertion " << e << std::endl; d_assertions.push_back(e); } Result SmtEngine::checkSat(const BoolExpr& e) { + NodeManagerScope nms(d_nm); Node node_e = preprocess(e.getNode()); addFormula(node_e); return check(); } Result SmtEngine::query(const BoolExpr& e) { - Node node_e = preprocess(e.getNode()); + NodeManagerScope nms(d_nm); + Node node_e = preprocess(d_nm->mkNode(NOT, e.getNode())); addFormula(node_e); return check(); } Result SmtEngine::assertFormula(const BoolExpr& e) { + NodeManagerScope nms(d_nm); Node node_e = preprocess(e.getNode()); addFormula(node_e); return quickCheck(); } +Expr SmtEngine::simplify(const Expr& e) { + Expr simplify(const Expr& e); + Unimplemented(); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 98cffb6de..027d3d603 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -118,7 +118,7 @@ private: ExprManager *d_public_em; /** Out internal expression/node manager */ - NodeManager *d_em; + NodeManager *d_nm; /** User-level options */ Options *d_opts; |