diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 16:57:11 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-22 16:57:11 +0000 |
commit | 533ed01ce6fdd3b93130b7ba0dbeedcd807a7a1f (patch) | |
tree | 593a1e9f62cc9605ac374df1203e85e437d424d9 /src/smt/smt_engine.cpp | |
parent | 6bdd652a8511df2f341b30daec60d5402986ed5b (diff) |
Small changes to the smt-engine, removed the assertions list.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 24795111f..36954ace4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -25,7 +25,6 @@ using namespace CVC4::prop; namespace CVC4 { SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : - d_assertions(), d_exprManager(em), d_nodeManager(em->getNodeManager()), d_options(opts) @@ -50,35 +49,25 @@ Node SmtEngine::preprocess(const Node& e) { return e; } -void SmtEngine::processAssertionList() { - for(unsigned i = 0; i < d_assertions.size(); ++i) { - d_propEngine->assertFormula(d_assertions[i]); - } - d_assertions.clear(); -} - Result SmtEngine::check() { Debug("smt") << "SMT check()" << std::endl; - processAssertionList(); return d_propEngine->checkSat(); } Result SmtEngine::quickCheck() { Debug("smt") << "SMT quickCheck()" << std::endl; - processAssertionList(); return Result(Result::VALIDITY_UNKNOWN); } void SmtEngine::addFormula(const Node& e) { Debug("smt") << "push_back assertion " << e << std::endl; - d_assertions.push_back(e); + d_propEngine->assertFormula(preprocess(e)); } Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; - Node node_e = preprocess(e.getNode()); - addFormula(node_e); + addFormula(e.getNode()); Result r = check().asSatisfiabilityResult(); Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl; return r; @@ -87,8 +76,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT query(" << e << ")" << std::endl; - Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode())); - addFormula(node_e); + addFormula(e.getNode().notExpr()); Result r = check().asValidityResult(); Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl; return r; @@ -97,8 +85,7 @@ Result SmtEngine::query(const BoolExpr& e) { Result SmtEngine::assertFormula(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; - Node node_e = preprocess(e.getNode()); - addFormula(node_e); + addFormula(e.getNode()); return quickCheck().asValidityResult(); } |