From de0dd1dc966b05467f1a5443ff33094262f5076a Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 1 Jun 2016 17:41:17 -0700 Subject: Revert "Merging proof branch" This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8. --- src/prop/cnf_stream.cpp | 23 +++++++---------------- src/prop/cnf_stream.h | 21 +++++++++++---------- src/prop/minisat/core/Solver.cc | 24 ------------------------ src/prop/minisat/minisat.cpp | 16 +++++++++------- src/prop/prop_engine.cpp | 4 ++-- src/prop/prop_engine.h | 3 +-- src/prop/theory_proxy.cpp | 33 +++++++++++++-------------------- 7 files changed, 43 insertions(+), 81 deletions(-) (limited to 'src/prop') diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index eda736b8a..aa1fc9587 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, bool noPreregistration) { +void TseitinCnfStream::ensureLiteral(TNode n) { // These are not removable and have no proof ID d_removable = false; @@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { d_literalToNodeMap.insert_safe(~lit, n.notNode()); } else { // We have a theory atom or variable. - lit = convertAtom(n, noPreregistration); + lit = convertAtom(n); } Assert(hasLiteral(n) && getNode(lit) == n); @@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) { d_cnfProof = proof; } -SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { +SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!hasLiteral(node), "atom already mapped!"); @@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { } else { theoryLiteral = true; canEliminate = false; - preRegister = !noPreregistration; + preRegister = true; } // Make a new literal (variables are not considered theory literals) @@ -258,11 +258,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { 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; @@ -679,7 +675,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id, TNode from, - LemmaProofRecipe* proofRecipe) { + theory::TheoryId ownerTheory) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; @@ -689,12 +685,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, Node assertion = negated ? node.notNode() : (Node)node; Node from_assertion = negated? from.notNode() : (Node) from; - if (proofRecipe) { - Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl; - proofRecipe->dump("pf::sat"); - d_cnfProof->setProofRecipe(proofRecipe); - } - + d_cnfProof->setExplainerTheory(ownerTheory); 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 6cc10d878..cf9d519a7 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -36,9 +36,6 @@ #include "smt_util/lemma_channels.h" namespace CVC4 { - -class LemmaProofRecipe; - namespace prop { class PropEngine; @@ -177,7 +174,7 @@ protected: * structure in this expression. Assumed to not be in the * translation cache. */ - SatLiteral convertAtom(TNode node, bool noPreprocessing = false); + SatLiteral convertAtom(TNode node); public: @@ -210,10 +207,14 @@ 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 proofRecipe contains the proof recipe for proving this node + * @param ownerTheory indicates the theory that should invoked to prove the formula. */ - virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0; - + virtual void convertAndAssert(TNode node, + bool removable, + bool negated, + ProofRule proof_id, + TNode from = TNode::null(), + theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0; /** * Get the node that is represented by the given SatLiteral. * @param literal the literal from the sat solver @@ -234,7 +235,7 @@ public: * this is like a "convert-but-don't-assert" version of * convertAndAssert(). */ - virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0; + virtual void ensureLiteral(TNode n) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -283,7 +284,7 @@ public: */ void convertAndAssert(TNode node, bool removable, bool negated, ProofRule rule, TNode from = TNode::null(), - LemmaProofRecipe* proofRecipe = NULL); + theory::TheoryId ownerTheory = theory::THEORY_LAST); /** * Constructs the stream to use the given sat solver. @@ -336,7 +337,7 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n, bool noPreregistration = false); + void ensureLiteral(TNode n); };/* class TseitinCnfStream */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d898b66a2..411b89514 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -232,8 +232,6 @@ CRef Solver::reason(Var x) { vec 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); @@ -268,12 +266,6 @@ 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 @@ -284,7 +276,6 @@ 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 @@ -345,12 +336,6 @@ bool Solver::addClause_(vec& 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); @@ -1681,13 +1666,6 @@ CRef Solver::updateLemmas() { { // The current lemma vec& 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()); @@ -1747,7 +1725,6 @@ 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); @@ -1764,7 +1741,6 @@ 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 ff726e299..bfbf9da6f 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,3 +300,5 @@ 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 eb607e901..54cf4c457 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, - LemmaProofRecipe* proofRecipe, + theory::TheoryId ownerTheory, 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, proofRecipe); + d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index c02015931..b9ce7ca7e 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -37,7 +37,6 @@ namespace CVC4 { class ResourceManager; class DecisionEngine; class TheoryEngine; -class LemmaProofRecipe; namespace theory { class TheoryRegistrar; @@ -135,7 +134,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, LemmaProofRecipe* proofRecipe, TNode from = TNode::null()); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, 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 6e8f1fbbf..4a4515eb9 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -99,34 +99,29 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - LemmaProofRecipe* proofRecipe = NULL; - PROOF(proofRecipe = new LemmaProofRecipe;); - - Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); + NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode); + Node explanationNode = theoryExplanation.node; + theory::TheoryId explainerTheory = theoryExplanation.theory; PROOF({ - ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); - ProofManager::getCnfProof()->setProofRecipe(proofRecipe); - - Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " - << std::endl; - proofRecipe->dump("pf::sat"); + ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode); + ProofManager::getCnfProof()->setExplainerTheory(explainerTheory); - delete proofRecipe; - proofRecipe = NULL; + Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: " + << explainerTheory << std::endl; }); - 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(); + 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(); 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(theoryExplanation)); + explanation.push_back(~d_cnfStream->getLiteral(explanationNode)); } } @@ -180,9 +175,7 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { Debug("shared") << "=) " << asNode << std::endl; } - - LemmaProofRecipe* noProofRecipe = NULL; - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe); + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST); } else { Debug("shared") << "=(" << asNode << std::endl; } -- cgit v1.2.3