diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
commit | 10df4ba0752eb23c76b9aa847e3ad116673a47b6 (patch) | |
tree | f41eec3963b7a9d96c0ea85179227d88ae57f0f6 /src/smt | |
parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 44 |
1 files changed, 24 insertions, 20 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index eca8c9d17..eb7792d2c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -162,7 +162,6 @@ public: PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); ); d_nodes[i] = n; } - };/* class AssertionPipeline */ struct SmtEngineStatistics { @@ -572,8 +571,9 @@ public: * formula might be pushed out to the propositional layer * immediately, or it might be simplified and kept, or it might not * even be simplified. + * the 2nd and 3rd arguments added for bookkeeping for proofs */ - void addFormula(TNode n) + void addFormula(TNode n, bool inUnsatCore, bool inInput = true) throw(TypeCheckingException, LogicException); /** @@ -1930,7 +1930,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Node falseNode = NodeManager::currentNM()->mkConst<bool>(false); Assert(!options::unsatCores()); d_assertions.clear(); - d_assertions.push_back(falseNode); + addFormula(falseNode, false, false); d_propagatorNeedsFinish = true; return false; } @@ -1969,7 +1969,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << d_nonClausalLearnedLiterals[i] << endl; Assert(!options::unsatCores()); d_assertions.clear(); - d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false); d_propagatorNeedsFinish = true; return false; } @@ -2005,7 +2005,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << learnedLiteral << endl; Assert(!options::unsatCores()); d_assertions.clear(); - d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false); d_propagatorNeedsFinish = true; return false; default: @@ -2031,7 +2031,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // if (!equations.empty()) { // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); // d_assertions.clear(); - // d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false); // return; // } // d_topLevelSubstitutions.simplifyRHS(constantPropagations); @@ -2642,7 +2642,7 @@ void SmtEnginePrivate::doMiplibTrick() { Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME); Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); - d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq))); + addFormula(Rewriter::rewrite(geq.andNode(leq)), false, false); SubstitutionMap nullMap(&d_fakeContext); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions status = d_smt.d_theoryEngine->solve(geq, nullMap); @@ -2693,7 +2693,7 @@ void SmtEnginePrivate::doMiplibTrick() { } newAssertion = Rewriter::rewrite(newAssertion); Debug("miplib") << " " << newAssertion << endl; - d_assertions.push_back(newAssertion); + addFormula(newAssertion, false, false); Debug("miplib") << " assertions to remove: " << endl; for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) { Debug("miplib") << " " << *k << endl; @@ -3417,7 +3417,7 @@ void SmtEnginePrivate::processAssertions() { d_iteSkolemMap.clear(); } -void SmtEnginePrivate::addFormula(TNode n) +void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) throw(TypeCheckingException, LogicException) { if (n == d_true) { @@ -3425,7 +3425,17 @@ void SmtEnginePrivate::addFormula(TNode n) return; } - Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl; + Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl; + // Give it to proof manager + PROOF( + if( inInput ){ + // n is an input assertion + ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); + }else{ + // n is the result of an unknown preprocessing step, add it to dependency map to null + ProofManager::currentPM()->addDependence(n, Node::null()); + } + ); // Add the normalized formula to the queue d_assertions.push_back(n); @@ -3465,8 +3475,6 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure expr is type-checked at this point. ensureBoolean(e); - // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); ); } // check to see if a postsolve() is pending @@ -3487,7 +3495,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE if(d_assertionList != NULL) { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode()); + d_private->addFormula(e.getNode(), inUnsatCore); } Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); @@ -3553,8 +3561,6 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); - // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3573,7 +3579,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce if(d_assertionList != NULL) { d_assertionList->push_back(e.notExpr()); } - d_private->addFormula(e.getNode().notNode()); + d_private->addFormula(e.getNode().notNode(), inUnsatCore); // Run the check Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); @@ -3625,9 +3631,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - - PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); ); - + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex @@ -3637,7 +3641,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec if(d_assertionList != NULL) { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode()); + d_private->addFormula(e.getNode(), inUnsatCore); return quickCheck().asValidityResult(); }/* SmtEngine::assertFormula() */ |