diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 23 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 21 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 24 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 16 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 3 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 33 |
7 files changed, 81 insertions, 43 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index aa1fc9587..eda736b8a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -120,7 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const { return find != d_nodeToLiteralMap.end(); } -void TseitinCnfStream::ensureLiteral(TNode n) { +void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // These are not removable and have no proof ID d_removable = false; @@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. - lit = convertAtom(n); + lit = convertAtom(n, noPreregistration); } Assert(hasLiteral(n) && getNode(lit) == n); @@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) { d_cnfProof = proof; } -SatLiteral CnfStream::convertAtom(TNode node) { +SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!hasLiteral(node), "atom already mapped!"); @@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { } else { theoryLiteral = true; canEliminate = false; - preRegister = true; + preRegister = !noPreregistration; } // Make a new literal (variables are not considered theory literals) @@ -258,7 +258,11 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node"); - Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str()); + + Assert(d_nodeToLiteralMap.contains(node), + "Literal not in the CNF Cache: %s\n", + node.toString().c_str()); + SatLiteral literal = d_nodeToLiteralMap[node]; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; @@ -675,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id, TNode from, - theory::TheoryId ownerTheory) { + LemmaProofRecipe* proofRecipe) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -685,7 +689,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - d_cnfProof->setExplainerTheory(ownerTheory); + if (proofRecipe) { + Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; + proofRecipe->dump("pf::sat"); + d_cnfProof->setProofRecipe(proofRecipe); + } + if (proof_id != RULE_INVALID) { d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index cf9d519a7..6cc10d878 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -36,6 +36,9 @@ #include "smt_util/lemma_channels.h" namespace CVC4 { + +class LemmaProofRecipe; + namespace prop { class PropEngine; @@ -174,7 +177,7 @@ protected: * structure in this expression. Assumed to not be in the * translation cache. */ - SatLiteral convertAtom(TNode node); + SatLiteral convertAtom(TNode node, bool noPreprocessing = false); public: @@ -207,14 +210,10 @@ public: * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated - * @param ownerTheory indicates the theory that should invoked to prove the formula. + * @param proofRecipe contains the proof recipe for proving this node */ - virtual void convertAndAssert(TNode node, - bool removable, - bool negated, - ProofRule proof_id, - TNode from = TNode::null(), - theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0; + /** * Get the node that is represented by the given SatLiteral. * @param literal the literal from the sat solver @@ -235,7 +234,7 @@ public: * this is like a "convert-but-don't-assert" version of * convertAndAssert(). */ - virtual void ensureLiteral(TNode n) = 0; + virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -284,7 +283,7 @@ public: */ void convertAndAssert(TNode node, bool removable, bool negated, ProofRule rule, TNode from = TNode::null(), - theory::TheoryId ownerTheory = theory::THEORY_LAST); + LemmaProofRecipe* proofRecipe = NULL); /** * Constructs the stream to use the given sat solver. @@ -337,7 +336,7 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n); + void ensureLiteral(TNode n, bool noPreregistration = false); };/* class TseitinCnfStream */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 411b89514..d898b66a2 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -232,6 +232,8 @@ CRef Solver::reason(Var x) { vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); + Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl; + // Sort the literals by trail index level lemma_lt lt(*this); sort(explanation, lt); @@ -266,6 +268,12 @@ CRef Solver::reason(Var x) { } explanation.shrink(i - j); + Debug("pf::sat") << "Solver::reason: explanation = " ; + for (int i = 0; i < explanation.size(); ++i) { + Debug("pf::sat") << explanation[i] << " "; + } + Debug("pf::sat") << std::endl; + // We need an explanation clause so we add a fake literal if (j == 1) { // Add not TRUE to the clause @@ -276,6 +284,7 @@ CRef Solver::reason(Var x) { CRef real_reason = ca.alloc(explLevel, explanation, true); // FIXME: at some point will need more information about where this explanation // came from (ie. the theory/sharing) + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ProofManager::getCnfProof()->registerConvertedClause(id, true); // no need to pop current assertion as this is not converted to cnf @@ -336,6 +345,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // If we are in solve or decision level > 0 if (minisat_busy || decisionLevel() > 0) { + Debug("pf::sat") << "Add clause adding a new lemma: "; + for (int k = 0; k < ps.size(); ++k) { + Debug("pf::sat") << ps[k] << " "; + } + Debug("pf::sat") << std::endl; + lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); @@ -1666,6 +1681,13 @@ CRef Solver::updateLemmas() { { // The current lemma vec<Lit>& lemma = lemmas[i]; + + Debug("pf::sat") << "Solver::updateLemmas: working on lemma: "; + for (int k = 0; k < lemma.size(); ++k) { + Debug("pf::sat") << lemma[k] << " "; + } + Debug("pf::sat") << std::endl; + // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { Assert (! PROOF_ON()); @@ -1725,6 +1747,7 @@ CRef Solver::updateLemmas() { TNode cnf_assertion = lemmas_cnf_assertion[i].first; TNode cnf_def = lemmas_cnf_assertion[i].second; + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); @@ -1741,6 +1764,7 @@ CRef Solver::updateLemmas() { Node cnf_assertion = lemmas_cnf_assertion[i].first; Node cnf_def = lemmas_cnf_assertion[i].second; + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index bfbf9da6f..ff726e299 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { // FIXME: This relies on the invariant that when ok() is false // the SAT solver does not add the clause (which is what Minisat currently does) if (!ok()) { - return ClauseIdUndef; + return ClauseIdUndef; } d_minisat->addClause(minisat_clause, removable, clause_id); PROOF( Assert (clause_id != ClauseIdError);); @@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() { } bool MinisatSatSolver::ok() const { - return d_minisat->okay(); + return d_minisat->okay(); } void MinisatSatSolver::interrupt() { @@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const return true; } -void MinisatSatSolver::requirePhase(SatLiteral lit) { +void MinisatSatSolver::requirePhase(SatLiteral lit) { Assert(!d_minisat->rnd_pol); Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl; SatVariable v = lit.getSatVariable(); d_minisat->freezePolarity(v, lit.isNegated()); } -bool MinisatSatSolver::flipDecision() { +bool MinisatSatSolver::flipDecision() { Debug("minisat") << "flipDecision()" << std::endl; return d_minisat->flipDecision(); } -bool MinisatSatSolver::isDecision(SatVariable decn) const { - return d_minisat->isDecision( decn ); +bool MinisatSatSolver::isDecision(SatVariable decn) const { + return d_minisat->isDecision( decn ); } /** Incremental interface */ @@ -291,7 +291,7 @@ namespace CVC4 { template<> prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) { return prop::MinisatSatSolver::toSatLiteral(lit); -} +} template<> void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl, @@ -300,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& } } /* namespace CVC4 */ - - diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 54cf4c457..eb607e901 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -132,13 +132,13 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, - theory::TheoryId ownerTheory, + LemmaProofRecipe* proofRecipe, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as (possibly) removable - d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory); + d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index b9ce7ca7e..c02015931 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -37,6 +37,7 @@ namespace CVC4 { class ResourceManager; class DecisionEngine; class TheoryEngine; +class LemmaProofRecipe; namespace theory { class TheoryRegistrar; @@ -134,7 +135,7 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null()); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 4a4515eb9..6e8f1fbbf 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -99,29 +99,34 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode); - Node explanationNode = theoryExplanation.node; - theory::TheoryId explainerTheory = theoryExplanation.theory; + LemmaProofRecipe* proofRecipe = NULL; + PROOF(proofRecipe = new LemmaProofRecipe;); + + Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); PROOF({ - ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode); - ProofManager::getCnfProof()->setExplainerTheory(explainerTheory); + ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); + ProofManager::getCnfProof()->setProofRecipe(proofRecipe); + + Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " + << std::endl; + proofRecipe->dump("pf::sat"); - Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: " - << explainerTheory << std::endl; + delete proofRecipe; + proofRecipe = NULL; }); - Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl; - if (explanationNode.getKind() == kind::AND) { - Node::const_iterator it = explanationNode.begin(); - Node::const_iterator it_end = explanationNode.end(); + Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; + if (theoryExplanation.getKind() == kind::AND) { + Node::const_iterator it = theoryExplanation.begin(); + Node::const_iterator it_end = theoryExplanation.end(); explanation.push_back(l); for (; it != it_end; ++ it) { explanation.push_back(~d_cnfStream->getLiteral(*it)); } } else { explanation.push_back(l); - explanation.push_back(~d_cnfStream->getLiteral(explanationNode)); + explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation)); } } @@ -175,7 +180,9 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { Debug("shared") << "=) " << asNode << std::endl; } - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST); + + LemmaProofRecipe* noProofRecipe = NULL; + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe); } else { Debug("shared") << "=(" << asNode << std::endl; } |