From ed7bc3afb8c6ee663b3d535674513c7ff4376050 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 27 Aug 2018 14:14:38 -0700 Subject: [PATCH] Resolution proof: separate printing from proof (#1964) Currently, we have an LFSCSatProof which inherits from TSatProof and implements printing the proof. The seperation is not clean (e.g. clauseName is used for printing only but is in TSatProof) and the inheritance does not add any value while making dependencies more confusing. The plan is that TSatProof becomes a self-contained part that the MiniSat implementations generate and ProofManager prints out. This commit is a first step in that direction. For SAT solvers with native capabilities for producing proofs, we would simply implement a different LFSC printer of their proof representation without changing the SAT solver itself. The inheritance would make this awkward to deal with. Additionally, the commit cleans up some unused functions and adjusts the visibility of TSatProof methods and members. --- src/Makefile.am | 2 + src/proof/bitvector_proof.cpp | 16 +-- src/proof/bitvector_proof.h | 3 - src/proof/lfsc_proof_printer.cpp | 176 +++++++++++++++++++++++++++ src/proof/lfsc_proof_printer.h | 105 ++++++++++++++++ src/proof/proof_manager.cpp | 27 ++-- src/proof/proof_manager.h | 6 +- src/proof/sat_proof.h | 108 ++++++---------- src/proof/sat_proof_implementation.h | 140 +-------------------- 9 files changed, 350 insertions(+), 233 deletions(-) create mode 100644 src/proof/lfsc_proof_printer.cpp create mode 100644 src/proof/lfsc_proof_printer.h diff --git a/src/Makefile.am b/src/Makefile.am index 3681280ec..8b13c9f34 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -150,6 +150,8 @@ libcvc4_la_SOURCES = \ proof/cnf_proof.h \ proof/lemma_proof.cpp \ proof/lemma_proof.h \ + proof/lfsc_proof_printer.cpp \ + proof/lfsc_proof_printer.h \ proof/proof.h \ proof/proof_manager.cpp \ proof/proof_manager.h \ diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 0c3f0704c..8f001ffa1 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,11 +15,12 @@ **/ +#include "proof/bitvector_proof.h" #include "options/bv_options.h" #include "options/proof_options.h" #include "proof/array_proof.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" +#include "proof/lfsc_proof_printer.h" #include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" @@ -48,16 +49,15 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { Assert (d_resolutionProof == NULL); - d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true); + d_resolutionProof = new BVSatProof(solver, &d_fakeContext, "bb", true); } theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; } void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) { + Assert (d_resolutionProof != NULL); Assert (d_cnfProof == NULL); d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb"); - Assert (d_resolutionProof != NULL); - d_resolutionProof->setCnfProof(d_cnfProof); // true and false have to be setup in a special way Node true_node = NodeManager::currentNM()->mkConst(true); @@ -515,7 +515,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector& lemma, std::os Expr lem = utils::mkOr(lemma); Assert (d_bbConflictMap.find(lem) != d_bbConflictMap.end()); ClauseId lemma_id = d_bbConflictMap[lem]; - d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof, lemma_id, os, lemma_paren); os <& lemma, std::os } ClauseId lemma_id = it->second; - d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof, lemma_id, os, lemma_paren); os <printResolutions(os, paren); + proof::LFSCProofPrinter::printResolutions(d_resolutionProof, os, paren); } std::string LFSCBitVectorProof::assignAlias(Expr expr) { diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 0bced2690..63f1cdf63 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -52,9 +52,6 @@ namespace CVC4 { template class TSatProof; typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; -template class LFSCSatProof; -typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof; - typedef std::unordered_set ExprSet; typedef std::unordered_map ExprToClauseId; typedef std::unordered_map ExprToId; diff --git a/src/proof/lfsc_proof_printer.cpp b/src/proof/lfsc_proof_printer.cpp new file mode 100644 index 000000000..e1fa3acdb --- /dev/null +++ b/src/proof/lfsc_proof_printer.cpp @@ -0,0 +1,176 @@ +/********************* */ +/*! \file lfsc_proof_printer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Prints proofs in the LFSC format + ** + ** Prints proofs in the LFSC format. + **/ + +#include "proof/lfsc_proof_printer.h" + +#include + +#include "prop/bvminisat/core/Solver.h" +#include "prop/minisat/core/Solver.h" + +namespace CVC4 { +namespace proof { + +template +std::string LFSCProofPrinter::clauseName(TSatProof* satProof, + ClauseId id) +{ + std::ostringstream os; + if (satProof->isInputClause(id)) + { + os << ProofManager::getInputClauseName(id, satProof->getName()); + } + else if (satProof->isLemmaClause(id)) + { + os << ProofManager::getLemmaClauseName(id, satProof->getName()); + } + else + { + os << ProofManager::getLearntClauseName(id, satProof->getName()); + } + return os.str(); +} + +template +void LFSCProofPrinter::printResolution(TSatProof* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren) +{ + out << "(satlem_simplify _ _ _"; + paren << ")"; + + const ResChain& res = satProof->getResolutionChain(id); + const typename ResChain::ResSteps& steps = res.getSteps(); + + for (int i = steps.size() - 1; i >= 0; i--) + { + out << " ("; + out << (steps[i].sign ? "R" : "Q") << " _ _"; + } + + ClauseId start_id = res.getStart(); + out << " " << clauseName(satProof, start_id); + + for (unsigned i = 0; i < steps.size(); i++) + { + prop::SatVariable v = + prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); + out << " " << clauseName(satProof, steps[i].id) << " " + << ProofManager::getVarName(v, satProof->getName()) << ")"; + } + + if (id == satProof->getEmptyClauseId()) + { + out << " (\\ empty empty)"; + return; + } + + out << " (\\ " << clauseName(satProof, id) << "\n"; // bind to lemma name + paren << ")"; +} + +template +void LFSCProofPrinter::printAssumptionsResolution(TSatProof* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren) +{ + Assert(satProof->isAssumptionConflict(id)); + // print the resolution proving the assumption conflict + printResolution(satProof, id, out, paren); + // resolve out assumptions to prove empty clause + out << "(satlem_simplify _ _ _ "; + const std::vector& confl = + *(satProof->getAssumptionConflicts().at(id)); + + Assert(confl.size()); + + for (unsigned i = 0; i < confl.size(); ++i) + { + prop::SatLiteral lit = toSatLiteral(confl[i]); + out << "("; + out << (lit.isNegated() ? "Q" : "R") << " _ _ "; + } + + out << clauseName(satProof, id) << " "; + for (int i = confl.size() - 1; i >= 0; --i) + { + prop::SatLiteral lit = toSatLiteral(confl[i]); + prop::SatVariable v = lit.getSatVariable(); + out << "unit" << v << " "; + out << ProofManager::getVarName(v, satProof->getName()) << ")"; + } + out << "(\\ e e)\n"; + paren << ")"; +} + +template +void LFSCProofPrinter::printResolutions(TSatProof* satProof, + std::ostream& out, + std::ostream& paren) +{ + Debug("bv-proof") << "; print resolutions" << std::endl; + std::set::iterator it = satProof->getSeenLearnt().begin(); + for (; it != satProof->getSeenLearnt().end(); ++it) + { + if (*it != satProof->getEmptyClauseId()) + { + Debug("bv-proof") << "; print resolution for " << *it << std::endl; + printResolution(satProof, *it, out, paren); + } + } + Debug("bv-proof") << "; done print resolutions" << std::endl; +} + +template +void LFSCProofPrinter::printResolutionEmptyClause(TSatProof* satProof, + std::ostream& out, + std::ostream& paren) +{ + printResolution(satProof, satProof->getEmptyClauseId(), out, paren); +} + +// Template specializations +template void LFSCProofPrinter::printAssumptionsResolution( + TSatProof* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutions( + TSatProof* satProof, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutionEmptyClause( + TSatProof* satProof, + std::ostream& out, + std::ostream& paren); + +template void LFSCProofPrinter::printAssumptionsResolution( + TSatProof* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutions( + TSatProof* satProof, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutionEmptyClause( + TSatProof* satProof, + std::ostream& out, + std::ostream& paren); +} // namespace proof +} // namespace CVC4 diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h new file mode 100644 index 000000000..bf4bfabad --- /dev/null +++ b/src/proof/lfsc_proof_printer.h @@ -0,0 +1,105 @@ +/********************* */ +/*! \file lfsc_proof_printer.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Prints proofs in the LFSC format + ** + ** Prints proofs in the LFSC format. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__LFSC_PROOF_PRINTER_H +#define __CVC4__PROOF__LFSC_PROOF_PRINTER_H + +#include +#include +#include + +#include "proof/clause_id.h" +#include "proof/proof_manager.h" +#include "proof/sat_proof.h" +#include "proof/sat_proof_implementation.h" +#include "util/proof.h" + +namespace CVC4 { +namespace proof { + +class LFSCProofPrinter +{ + public: + /** + * Prints the resolution proof for an assumption conflict. + * + * @param satProof The record of the reasoning done by the SAT solver + * @param id The clause to print a proof for + * @param out The stream to print to + * @param paren A stream for the closing parentheses + */ + template + static void printAssumptionsResolution(TSatProof* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren); + + /** + * Prints the resolution proofs for learned clauses that have been used to + * deduce unsat. + * + * @param satProof The record of the reasoning done by the SAT solver + * @param out The stream to print to + * @param paren A stream for the closing parentheses + */ + template + static void printResolutions(TSatProof* satProof, + std::ostream& out, + std::ostream& paren); + + /** + * Prints the resolution proof for the empty clause. + * + * @param satProof The record of the reasoning done by the SAT solver + * @param out The stream to print to + * @param paren A stream for the closing parentheses + */ + template + static void printResolutionEmptyClause(TSatProof* satProof, + std::ostream& out, + std::ostream& paren); + + private: + /** + * Maps a clause id to a string identifier used in the LFSC proof. + * + * @param satProof The record of the reasoning done by the SAT solver + * @param id The clause to map to a string + */ + template + static std::string clauseName(TSatProof* satProof, ClauseId id); + + /** + * Prints the resolution proof for a given clause. + * + * @param satProof The record of the reasoning done by the SAT solver + * @param id The clause to print a proof for + * @param out The stream to print to + * @param paren A stream for the closing parentheses + */ + template + static void printResolution(TSatProof* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren); +}; + +} // namespace proof +} // namespace CVC4 + +#endif /* __CVC4__PROOF__LFSC_PROOF_PRINTER_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index f2205e2ed..cc5332cfd 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -24,6 +24,7 @@ #include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" +#include "proof/lfsc_proof_printer.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "proof/theory_proof.h" @@ -87,7 +88,7 @@ const Proof& ProofManager::getProof(SmtEngine* smt) Assert(currentPM()->d_format == LFSC); currentPM()->d_fullProof.reset(new LFSCProof( smt, - static_cast(getSatProof()), + static_cast(getSatProof()), static_cast(getCnfProof()), static_cast(getTheoryProofEngine()))); } @@ -141,18 +142,17 @@ SkolemizationManager* ProofManager::getSkolemizationManager() { void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); - currentPM()->d_satProof = new LFSCCoreSatProof(solver, d_context, ""); + currentPM()->d_satProof = new CoreSatProof(solver, d_context, ""); } void ProofManager::initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx) { ProofManager* pm = currentPM(); + Assert(pm->d_satProof != NULL); Assert (pm->d_cnfProof == NULL); Assert (pm->d_format == LFSC); CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, ""); pm->d_cnfProof = cnf; - Assert(pm-> d_satProof != NULL); - pm->d_satProof->setCnfProof(cnf); // true and false have to be setup in a special way Node true_node = NodeManager::currentNM()->mkConst(true); @@ -541,16 +541,14 @@ void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } - - LFSCProof::LFSCProof(SmtEngine* smtEngine, - LFSCCoreSatProof* sat, + CoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory) - : d_satProof(sat) - , d_cnfProof(cnf) - , d_theoryProof(theory) - , d_smtEngine(smtEngine) + : d_satProof(sat), + d_cnfProof(cnf), + d_theoryProof(theory), + d_smtEngine(smtEngine) {} void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const @@ -732,11 +730,12 @@ void LFSCProof::toStream(std::ostream& out) const Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { - ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren); + proof::LFSCProofPrinter::printResolutionEmptyClause( + ProofManager::getBitVectorProof()->getSatProof(), out, paren); } else { // print actual resolution proof - d_satProof->printResolutions(out, paren); - d_satProof->printResolutionEmptyClause(out, paren); + proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren); + proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof, out, paren); } out << paren.str(); diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 0defaac84..89aa66c2d 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -72,7 +72,7 @@ class ArrayProof; class BitVectorProof; template class LFSCSatProof; -typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof; +typedef TSatProof CoreSatProof; class LFSCCnfProof; class LFSCTheoryProofEngine; @@ -299,7 +299,7 @@ class LFSCProof : public Proof { public: LFSCProof(SmtEngine* smtEngine, - LFSCCoreSatProof* sat, + CoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory); ~LFSCProof() override {} @@ -315,7 +315,7 @@ class LFSCProof : public Proof void checkUnrewrittenAssertion(const NodeSet& assertions) const; - LFSCCoreSatProof* d_satProof; + CoreSatProof* d_satProof; LFSCCnfProof* d_cnfProof; LFSCTheoryProofEngine* d_theoryProof; SmtEngine* d_smtEngine; diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 5ae078890..8fd2cb9eb 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -114,8 +114,7 @@ class TSatProof { public: TSatProof(Solver* solver, context::Context* context, const std::string& name, bool checkRes = false); - virtual ~TSatProof(); - void setCnfProof(CnfProof* cnf_proof); + ~TSatProof(); void startResChain(typename Solver::TLit start); void startResChain(typename Solver::TCRef start); @@ -204,44 +203,34 @@ class TSatProof { bool derivedEmptyClause() const; prop::SatClause* buildClause(ClauseId id); - virtual void printResolution(ClauseId id, std::ostream& out, - std::ostream& paren) = 0; - virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; - virtual void printResolutionEmptyClause(std::ostream& out, - std::ostream& paren) = 0; - virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, - std::ostream& paren) = 0; - void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas); void storeClauseGlue(ClauseId clause, int glue); - protected: - void print(ClauseId id) const; - void printRes(ClauseId id) const; - void printRes(const ResolutionChain& res) const; - bool isInputClause(ClauseId id) const; bool isLemmaClause(ClauseId id) const; bool isAssumptionConflict(ClauseId id) const; - bool isUnit(ClauseId id) const; - typename Solver::TLit getUnit(ClauseId id) const; - - bool isUnit(typename Solver::TLit lit) const; - ClauseId getUnitId(typename Solver::TLit lit) const; - - - bool hasResolutionChain(ClauseId id) const; /** Returns the resolution chain associated with id. Assert fails if * hasResolution(id) does not hold. */ const ResolutionChain& getResolutionChain(ClauseId id) const; - /** Returns a mutable pointer to the resolution chain associated with id. - * Assert fails if hasResolution(id) does not hold. */ - ResolutionChain* getMutableResolutionChain(ClauseId id); + const std::string& getName() const { return d_name; } + const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; } + const IdSet& getSeenLearnt() const { return d_seenLearnt; } + const IdToConflicts& getAssumptionConflicts() const + { + return d_assumptionConflictsDebug; + } + + private: + bool isUnit(ClauseId id) const; + typename Solver::TLit getUnit(ClauseId id) const; + + bool isUnit(typename Solver::TLit lit) const; + ClauseId getUnitId(typename Solver::TLit lit) const; void createLitSet(ClauseId id, LitSet& set); @@ -263,10 +252,8 @@ class TSatProof { const typename Solver::TClause& getClause(typename Solver::TCRef ref) const; - typename Solver::TClause* getMutableClause(typename Solver::TCRef ref); void getLitVec(ClauseId id, LitVector& vec); - virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); @@ -291,16 +278,33 @@ class TSatProof { LitVector& removeStack, LitSet& inClause, LitSet& seen); void removeRedundantFromRes(ResChain* res, ClauseId id); - std::string varName(typename Solver::TLit lit); - std::string clauseName(ClauseId id); + void print(ClauseId id) const; + void printRes(ClauseId id) const; + void printRes(const ResolutionChain& res) const; + + std::unordered_map d_glueMap; + struct Statistics { + IntStat d_numLearnedClauses; + IntStat d_numLearnedInProof; + IntStat d_numLemmasInProof; + AverageStat d_avgChainLength; + HistogramStat d_resChainLengths; + HistogramStat d_usedResChainLengths; + HistogramStat d_clauseGlue; + HistogramStat d_usedClauseGlue; + Statistics(const std::string& name); + ~Statistics(); + }; + + std::string d_name; - void addToProofManager(ClauseId id, ClauseKind kind); - void addToCnfProof(ClauseId id); + const ClauseId d_emptyClauseId; + IdSet d_seenLearnt; + IdToConflicts d_assumptionConflictsDebug; // Internal data. Solver* d_solver; context::Context* d_context; - CnfProof* d_cnfProof; // clauses IdCRefMap d_idClause; @@ -315,7 +319,6 @@ class TSatProof { VarSet d_assumptions; // assumption literals for bv solver IdHashSet d_assumptionConflicts; // assumption conflicts not actually added // to SAT solver - IdToConflicts d_assumptionConflictsDebug; // Resolutions. @@ -336,7 +339,6 @@ class TSatProof { ResStack d_resStack; bool d_checkRes; - const ClauseId d_emptyClauseId; const ClauseId d_nullId; // temporary map for updating CRefs @@ -349,49 +351,13 @@ class TSatProof { ClauseId d_trueLit; ClauseId d_falseLit; - std::string d_name; - - IdSet d_seenLearnt; IdToSatClause d_seenInputs; IdToSatClause d_seenLemmas; - private: - std::unordered_map d_glueMap; - struct Statistics { - IntStat d_numLearnedClauses; - IntStat d_numLearnedInProof; - IntStat d_numLemmasInProof; - AverageStat d_avgChainLength; - HistogramStat d_resChainLengths; - HistogramStat d_usedResChainLengths; - HistogramStat d_clauseGlue; - HistogramStat d_usedClauseGlue; - Statistics(const std::string& name); - ~Statistics(); - }; - bool d_satProofConstructed; Statistics d_statistics; }; /* class TSatProof */ -template -class LFSCSatProof : public TSatProof { - private: - public: - LFSCSatProof(SatSolver* solver, context::Context* context, - const std::string& name, bool checkRes = false) - : TSatProof(solver, context, name, checkRes) {} - void printResolution(ClauseId id, - std::ostream& out, - std::ostream& paren) override; - void printResolutions(std::ostream& out, std::ostream& paren) override; - void printResolutionEmptyClause(std::ostream& out, - std::ostream& paren) override; - void printAssumptionsResolution(ClauseId id, - std::ostream& out, - std::ostream& paren) override; -}; /* class LFSCSatProof */ - template prop::SatLiteral toSatLiteral(typename Solver::TLit lit); diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 82e7cb7b2..96f99be47 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -188,9 +188,12 @@ void ResChain::addRedundantLit(typename Solver::TLit lit) { template TSatProof::TSatProof(Solver* solver, context::Context* context, const std::string& name, bool checkRes) - : d_solver(solver), + : d_name(name), + d_emptyClauseId(ClauseIdEmpty), + d_seenLearnt(), + d_assumptionConflictsDebug(), + d_solver(solver), d_context(context), - d_cnfProof(NULL), d_idClause(), d_clauseId(), d_idUnit(context), @@ -200,19 +203,15 @@ TSatProof::TSatProof(Solver* solver, context::Context* context, d_lemmaClauses(), d_assumptions(), d_assumptionConflicts(), - d_assumptionConflictsDebug(), d_resolutionChains(d_context), d_resStack(), d_checkRes(checkRes), - d_emptyClauseId(ClauseIdEmpty), d_nullId(-2), d_temp_clauseId(), d_temp_idClause(), d_unitConflictId(context), d_trueLit(ClauseIdUndef), d_falseLit(ClauseIdUndef), - d_name(name), - d_seenLearnt(), d_seenInputs(), d_seenLemmas(), d_satProofConstructed(false), @@ -266,12 +265,6 @@ TSatProof::~TSatProof() { } } -template -void TSatProof::setCnfProof(CnfProof* cnf_proof) { - Assert(d_cnfProof == NULL); - d_cnfProof = cnf_proof; -} - /** * Returns true if the resolution chain corresponding to id * does resolve to the clause associated to id @@ -447,14 +440,6 @@ TSatProof::getResolutionChain(ClauseId id) const { return *chain; } -template -typename TSatProof::ResolutionChain* -TSatProof::getMutableResolutionChain(ClauseId id) { - Assert(hasResolutionChain(id)); - ResolutionChain* chain = d_resolutionChains.find(id)->second; - return chain; -} - template bool TSatProof::isInputClause(ClauseId id) const { return d_inputClauses.find(id) != d_inputClauses.end(); @@ -767,15 +752,6 @@ void TSatProof::endResChain(ClauseId id) { d_resStack.pop_back(); } -// template -// void TSatProof::endResChain(typename Solver::TCRef clause) { -// Assert(d_resStack.size() > 0); -// ClauseId id = registerClause(clause, LEARNT); -// ResChain* res = d_resStack.back(); -// registerResolution(id, res); -// d_resStack.pop_back(); -// } - template void TSatProof::endResChain(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); @@ -846,11 +822,6 @@ ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { registerResolution(unit_id, res); return unit_id; } -template -void TSatProof::toStream(std::ostream& out) { - Debug("proof:sat") << "TSatProof::printProof\n"; - Unimplemented("native proof printing not supported yet"); -} template ClauseId TSatProof::storeUnitConflict( @@ -984,21 +955,6 @@ bool TSatProof::proofConstructed() const { return d_satProofConstructed; } -template -std::string TSatProof::clauseName(ClauseId id) { - std::ostringstream os; - if (isInputClause(id)) { - os << ProofManager::getInputClauseName(id, d_name); - return os.str(); - } else if (isLemmaClause(id)) { - os << ProofManager::getLemmaClauseName(id, d_name); - return os.str(); - } else { - os << ProofManager::getLearntClauseName(id, d_name); - return os.str(); - } -} - template prop::SatClause* TSatProof::buildClause(ClauseId id) { if (isUnit(id)) { @@ -1105,92 +1061,6 @@ TSatProof::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); } -/// LFSCSatProof class -template -void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, - std::ostream& paren) { - out << "(satlem_simplify _ _ _"; - paren << ")"; - - const ResChain& res = this->getResolutionChain(id); - const typename ResChain::ResSteps& steps = res.getSteps(); - - for (int i = steps.size() - 1; i >= 0; i--) { - out << " ("; - out << (steps[i].sign ? "R" : "Q") << " _ _"; - } - - ClauseId start_id = res.getStart(); - out << " " << this->clauseName(start_id); - - for (unsigned i = 0; i < steps.size(); i++) { - prop::SatVariable v = - prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); - out << " " << this->clauseName(steps[i].id) << " " - << ProofManager::getVarName(v, this->d_name) << ")"; - } - - if (id == this->d_emptyClauseId) { - out <<" (\\ empty empty)"; - return; - } - - out << " (\\ " << this->clauseName(id) << "\n"; // bind to lemma name - paren << ")"; -} - -/// LFSCSatProof class -template -void LFSCSatProof::printAssumptionsResolution(ClauseId id, - std::ostream& out, - std::ostream& paren) { - Assert(this->isAssumptionConflict(id)); - // print the resolution proving the assumption conflict - printResolution(id, out, paren); - // resolve out assumptions to prove empty clause - out << "(satlem_simplify _ _ _ "; - std::vector& confl = - *(this->d_assumptionConflictsDebug[id]); - - Assert(confl.size()); - - for (unsigned i = 0; i < confl.size(); ++i) { - prop::SatLiteral lit = toSatLiteral(confl[i]); - out << "("; - out << (lit.isNegated() ? "Q" : "R") << " _ _ "; - } - - out << this->clauseName(id) << " "; - for (int i = confl.size() - 1; i >= 0; --i) { - prop::SatLiteral lit = toSatLiteral(confl[i]); - prop::SatVariable v = lit.getSatVariable(); - out << "unit" << v << " "; - out << ProofManager::getVarName(v, this->d_name) << ")"; - } - out << "(\\ e e)\n"; - paren << ")"; -} - -template -void LFSCSatProof::printResolutions(std::ostream& out, - std::ostream& paren) { - Debug("bv-proof") << "; print resolutions" << std::endl; - std::set::iterator it = this->d_seenLearnt.begin(); - for (; it != this->d_seenLearnt.end(); ++it) { - if (*it != this->d_emptyClauseId) { - Debug("bv-proof") << "; print resolution for " << *it << std::endl; - printResolution(*it, out, paren); - } - } - Debug("bv-proof") << "; done print resolutions" << std::endl; -} - -template -void LFSCSatProof::printResolutionEmptyClause(std::ostream& out, - std::ostream& paren) { - printResolution(this->d_emptyClauseId, out, paren); -} - inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { switch (k) { case CVC4::INPUT: -- 2.30.2