From: Haniel Barbosa Date: Mon, 14 Dec 2020 19:06:47 +0000 (-0300) Subject: [proof-new] Make prop engine proof producing (#5667) X-Git-Tag: cvc5-1.0.0~2447 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4149c7ebfdf4270f736c611ad95b715ae1b077c5;p=cvc5.git [proof-new] Make prop engine proof producing (#5667) --- diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fee73babb..a8a92096c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -31,6 +31,7 @@ #include "options/smt_options.h" #include "proof/proof_manager.h" #include "prop/cnf_stream.h" +#include "prop/minisat/minisat.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" @@ -40,9 +41,6 @@ #include "util/resource_manager.h" #include "util/result.h" -using namespace std; -using namespace CVC4::context; - namespace CVC4 { namespace prop { @@ -67,25 +65,25 @@ public: }; PropEngine::PropEngine(TheoryEngine* te, - Context* satContext, - UserContext* userContext, + context::Context* satContext, + context::UserContext* userContext, ResourceManager* rm, OutputManager& outMgr, ProofNodeManager* pnm) : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), - d_theoryProxy(NULL), - d_satSolver(NULL), - d_registrar(NULL), - d_cnfStream(NULL), + d_theoryProxy(nullptr), + d_satSolver(nullptr), + d_registrar(nullptr), + d_pnm(pnm), + d_cnfStream(nullptr), d_pfCnfStream(nullptr), d_ppm(nullptr), d_interrupted(false), d_resourceManager(rm), d_outMgr(outMgr) { - Debug("prop") << "Constructing the PropEngine" << endl; d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); @@ -96,13 +94,22 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::CnfStream( d_satSolver, d_registrar, userContext, &d_outMgr, rm, true); - d_theoryProxy = new TheoryProxy( this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm); d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); + if (pnm) + { + d_pfCnfStream.reset(new ProofCnfStream( + userContext, + *d_cnfStream, + static_cast(d_satSolver)->getProofManager(), + pnm)); + d_ppm.reset( + new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get())); + } if (options::unsatCores()) { ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); @@ -113,6 +120,16 @@ void PropEngine::finishInit() { NodeManager* nm = NodeManager::currentNM(); d_cnfStream->convertAndAssert(nm->mkConst(true), false, false); + // this is necessary because if True is later asserted to the prop engine the + // CNF stream will ignore it since the SAT solver already had it registered, + // thus not having True as an assumption for the SAT proof. To solve this + // issue we track it directly here + if (isProofEnabled()) + { + static_cast(d_satSolver) + ->getProofManager() + ->registerSatAssumptions({nm->mkConst(true)}); + } d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false); } @@ -152,7 +169,16 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false, true); + if (isProofEnabled()) + { + d_pfCnfStream->convertAndAssert(node, false, false, nullptr); + // register in proof manager + d_ppm->registerAssertion(node); + } + else + { + d_cnfStream->convertAndAssert(node, false, false, true); + } } void PropEngine::assertLemma(theory::TrustNode trn, bool removable) @@ -160,9 +186,17 @@ void PropEngine::assertLemma(theory::TrustNode trn, bool removable) Node node = trn.getNode(); bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as (possibly) removable - d_cnfStream->convertAndAssert(node, removable, negated); + if (isProofEnabled()) + { + Assert(trn.getGenerator()); + d_pfCnfStream->convertAndAssert( + node, negated, removable, trn.getGenerator()); + } + else + { + d_cnfStream->convertAndAssert(node, removable, negated); + } } void PropEngine::assertLemmas(theory::TrustNode lem, @@ -269,61 +303,75 @@ Result PropEngine::checkSat() { return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT); } -Node PropEngine::getValue(TNode node) const { +Node PropEngine::getValue(TNode node) const +{ Assert(node.getType().isBoolean()); Assert(d_cnfStream->hasLiteral(node)); SatLiteral lit = d_cnfStream->getLiteral(node); SatValue v = d_satSolver->value(lit); - if(v == SAT_VALUE_TRUE) { + if (v == SAT_VALUE_TRUE) + { return NodeManager::currentNM()->mkConst(true); - } else if(v == SAT_VALUE_FALSE) { + } + else if (v == SAT_VALUE_FALSE) + { return NodeManager::currentNM()->mkConst(false); - } else { + } + else + { Assert(v == SAT_VALUE_UNKNOWN); return Node::null(); } } -bool PropEngine::isSatLiteral(TNode node) const { +bool PropEngine::isSatLiteral(TNode node) const +{ return d_cnfStream->hasLiteral(node); } -bool PropEngine::hasValue(TNode node, bool& value) const { +bool PropEngine::hasValue(TNode node, bool& value) const +{ Assert(node.getType().isBoolean()); Assert(d_cnfStream->hasLiteral(node)) << node; SatLiteral lit = d_cnfStream->getLiteral(node); SatValue v = d_satSolver->value(lit); - if(v == SAT_VALUE_TRUE) { + if (v == SAT_VALUE_TRUE) + { value = true; return true; - } else if(v == SAT_VALUE_FALSE) { + } + else if (v == SAT_VALUE_FALSE) + { value = false; return true; - } else { + } + else + { Assert(v == SAT_VALUE_UNKNOWN); return false; } } -void PropEngine::getBooleanVariables(std::vector& outputVariables) const { +void PropEngine::getBooleanVariables(std::vector& outputVariables) const +{ d_cnfStream->getBooleanVariables(outputVariables); } -void PropEngine::ensureLiteral(TNode n) { - d_cnfStream->ensureLiteral(n); -} +void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); } -void PropEngine::push() { +void PropEngine::push() +{ Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->push(); Debug("prop") << "push()" << endl; } -void PropEngine::pop() { +void PropEngine::pop() +{ Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->pop(); Debug("prop") << "pop()" << endl; @@ -335,16 +383,16 @@ void PropEngine::resetTrail() Debug("prop") << "resetTrail()" << endl; } -unsigned PropEngine::getAssertionLevel() const { +unsigned PropEngine::getAssertionLevel() const +{ return d_satSolver->getAssertionLevel(); } -bool PropEngine::isRunning() const { - return d_inCheckSat; -} +bool PropEngine::isRunning() const { return d_inCheckSat; } void PropEngine::interrupt() { - if(! d_inCheckSat) { + if (!d_inCheckSat) + { return; } @@ -358,43 +406,60 @@ void PropEngine::spendResource(ResourceManager::Resource r) d_resourceManager->spendResource(r); } -bool PropEngine::properExplanation(TNode node, TNode expl) const { - if(! d_cnfStream->hasLiteral(node)) { - Trace("properExplanation") << "properExplanation(): Failing because node " - << "being explained doesn't have a SAT literal ?!" << std::endl - << "properExplanation(): The node is: " << node << std::endl; +bool PropEngine::properExplanation(TNode node, TNode expl) const +{ + if (!d_cnfStream->hasLiteral(node)) + { + Trace("properExplanation") + << "properExplanation(): Failing because node " + << "being explained doesn't have a SAT literal ?!" << std::endl + << "properExplanation(): The node is: " << node << std::endl; return false; } SatLiteral nodeLit = d_cnfStream->getLiteral(node); - for(TNode::kinded_iterator i = expl.begin(kind::AND), - i_end = expl.end(kind::AND); - i != i_end; - ++i) { - if(! d_cnfStream->hasLiteral(*i)) { - Trace("properExplanation") << "properExplanation(): Failing because one of explanation " - << "nodes doesn't have a SAT literal" << std::endl - << "properExplanation(): The explanation node is: " << *i << std::endl; + for (TNode::kinded_iterator i = expl.begin(kind::AND), + i_end = expl.end(kind::AND); + i != i_end; + ++i) + { + if (!d_cnfStream->hasLiteral(*i)) + { + Trace("properExplanation") + << "properExplanation(): Failing because one of explanation " + << "nodes doesn't have a SAT literal" << std::endl + << "properExplanation(): The explanation node is: " << *i + << std::endl; return false; } SatLiteral iLit = d_cnfStream->getLiteral(*i); - if(iLit == nodeLit) { - Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl - << "properExplanation(): " << node << std::endl - << "properExplanation(): cannot be made to explain itself!" << std::endl; + if (iLit == nodeLit) + { + Trace("properExplanation") + << "properExplanation(): Failing because the node" << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): cannot be made to explain itself!" + << std::endl; return false; } - if(! d_satSolver->properExplanation(nodeLit, iLit)) { - Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl - << "properExplanation(): " << *i << std::endl - << "properExplanation(): is not part of a proper explanation node for" << std::endl - << "properExplanation(): " << node << std::endl - << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl - << "properExplanation(): node wasn't propagated before the node being explained" << std::endl; + if (!d_satSolver->properExplanation(nodeLit, iLit)) + { + Trace("properExplanation") + << "properExplanation(): SAT solver told us that node" << std::endl + << "properExplanation(): " << *i << std::endl + << "properExplanation(): is not part of a proper explanation node for" + << std::endl + << "properExplanation(): " << node << std::endl + << "properExplanation(): Perhaps it one of the two isn't assigned or " + "the explanation" + << std::endl + << "properExplanation(): node wasn't propagated before the node " + "being explained" + << std::endl; return false; } } @@ -402,13 +467,27 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const { return true; } +void PropEngine::checkProof(context::CDList* assertions) +{ + if (!d_pnm) + { + return; + } + return d_ppm->checkProof(assertions); +} + ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); } std::shared_ptr PropEngine::getProof() { - // TODO (proj #37) implement this - return nullptr; + if (!d_pnm) + { + return nullptr; + } + return d_ppm->getProof(); } -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; } + +} // namespace prop +} // namespace CVC4 diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index b311558ab..55a42c2a7 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -256,6 +256,8 @@ class PropEngine */ std::shared_ptr getProof(); + /** Is proof enabled? */ + bool isProofEnabled() const; private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment();