diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/bitvector_proof.cpp | 16 | ||||
| -rw-r--r-- | src/proof/bitvector_proof.h | 3 | ||||
| -rw-r--r-- | src/proof/lfsc_proof_printer.cpp | 176 | ||||
| -rw-r--r-- | src/proof/lfsc_proof_printer.h | 105 | ||||
| -rw-r--r-- | src/proof/proof_manager.cpp | 27 | ||||
| -rw-r--r-- | src/proof/proof_manager.h | 6 | ||||
| -rw-r--r-- | src/proof/sat_proof.h | 108 | ||||
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 140 |
8 files changed, 348 insertions, 233 deletions
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<bool>(true); @@ -515,7 +515,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& 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_paren.str(); } else { @@ -615,7 +616,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& 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 <<lemma_paren.str(); return; @@ -1039,7 +1041,7 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, } os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; - d_resolutionProof->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 Solver> class TSatProof; typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; -template <class Solver> class LFSCSatProof; -typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof; - typedef std::unordered_set<Expr, ExprHashFunction> ExprSet; typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; typedef std::unordered_map<Expr, unsigned, ExprHashFunction> 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 <iostream> + +#include "prop/bvminisat/core/Solver.h" +#include "prop/minisat/core/Solver.h" + +namespace CVC4 { +namespace proof { + +template <class Solver> +std::string LFSCProofPrinter::clauseName(TSatProof<Solver>* 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 <class Solver> +void LFSCProofPrinter::printResolution(TSatProof<Solver>* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren) +{ + out << "(satlem_simplify _ _ _"; + paren << ")"; + + const ResChain<Solver>& res = satProof->getResolutionChain(id); + const typename ResChain<Solver>::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 <class Solver> +void LFSCProofPrinter::printAssumptionsResolution(TSatProof<Solver>* 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<typename Solver::TLit>& confl = + *(satProof->getAssumptionConflicts().at(id)); + + Assert(confl.size()); + + for (unsigned i = 0; i < confl.size(); ++i) + { + prop::SatLiteral lit = toSatLiteral<Solver>(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<Solver>(confl[i]); + prop::SatVariable v = lit.getSatVariable(); + out << "unit" << v << " "; + out << ProofManager::getVarName(v, satProof->getName()) << ")"; + } + out << "(\\ e e)\n"; + paren << ")"; +} + +template <class Solver> +void LFSCProofPrinter::printResolutions(TSatProof<Solver>* satProof, + std::ostream& out, + std::ostream& paren) +{ + Debug("bv-proof") << "; print resolutions" << std::endl; + std::set<ClauseId>::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 <class Solver> +void LFSCProofPrinter::printResolutionEmptyClause(TSatProof<Solver>* satProof, + std::ostream& out, + std::ostream& paren) +{ + printResolution(satProof, satProof->getEmptyClauseId(), out, paren); +} + +// Template specializations +template void LFSCProofPrinter::printAssumptionsResolution( + TSatProof<CVC4::Minisat::Solver>* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutions( + TSatProof<CVC4::Minisat::Solver>* satProof, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutionEmptyClause( + TSatProof<CVC4::Minisat::Solver>* satProof, + std::ostream& out, + std::ostream& paren); + +template void LFSCProofPrinter::printAssumptionsResolution( + TSatProof<CVC4::BVMinisat::Solver>* satProof, + ClauseId id, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutions( + TSatProof<CVC4::BVMinisat::Solver>* satProof, + std::ostream& out, + std::ostream& paren); +template void LFSCProofPrinter::printResolutionEmptyClause( + TSatProof<CVC4::BVMinisat::Solver>* 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 <iosfwd> +#include <string> +#include <vector> + +#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 <class Solver> + static void printAssumptionsResolution(TSatProof<Solver>* 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 <class Solver> + static void printResolutions(TSatProof<Solver>* 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 <class Solver> + static void printResolutionEmptyClause(TSatProof<Solver>* 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 <class Solver> + static std::string clauseName(TSatProof<Solver>* 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 <class Solver> + static void printResolution(TSatProof<Solver>* 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<LFSCCoreSatProof*>(getSatProof()), + static_cast<CoreSatProof*>(getSatProof()), static_cast<LFSCCnfProof*>(getCnfProof()), static_cast<LFSCTheoryProofEngine*>(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<bool>(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 Solver> class LFSCSatProof; -typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof; +typedef TSatProof<CVC4::Minisat::Solver> 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<Solver>* 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<ClauseId, int> d_glueMap; + struct Statistics { + IntStat d_numLearnedClauses; + IntStat d_numLearnedInProof; + IntStat d_numLemmasInProof; + AverageStat d_avgChainLength; + HistogramStat<uint64_t> d_resChainLengths; + HistogramStat<uint64_t> d_usedResChainLengths; + HistogramStat<uint64_t> d_clauseGlue; + HistogramStat<uint64_t> 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<ClauseId, int> d_glueMap; - struct Statistics { - IntStat d_numLearnedClauses; - IntStat d_numLearnedInProof; - IntStat d_numLemmasInProof; - AverageStat d_avgChainLength; - HistogramStat<uint64_t> d_resChainLengths; - HistogramStat<uint64_t> d_usedResChainLengths; - HistogramStat<uint64_t> d_clauseGlue; - HistogramStat<uint64_t> d_usedClauseGlue; - Statistics(const std::string& name); - ~Statistics(); - }; - bool d_satProofConstructed; Statistics d_statistics; }; /* class TSatProof */ -template <class SatSolver> -class LFSCSatProof : public TSatProof<SatSolver> { - private: - public: - LFSCSatProof(SatSolver* solver, context::Context* context, - const std::string& name, bool checkRes = false) - : TSatProof<SatSolver>(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 <class Solver> 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<Solver>::addRedundantLit(typename Solver::TLit lit) { template <class Solver> TSatProof<Solver>::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<Solver>::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<Solver>::~TSatProof() { } } -template <class Solver> -void TSatProof<Solver>::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 @@ -448,14 +441,6 @@ TSatProof<Solver>::getResolutionChain(ClauseId id) const { } template <class Solver> -typename TSatProof<Solver>::ResolutionChain* -TSatProof<Solver>::getMutableResolutionChain(ClauseId id) { - Assert(hasResolutionChain(id)); - ResolutionChain* chain = d_resolutionChains.find(id)->second; - return chain; -} - -template <class Solver> bool TSatProof<Solver>::isInputClause(ClauseId id) const { return d_inputClauses.find(id) != d_inputClauses.end(); } @@ -767,15 +752,6 @@ void TSatProof<Solver>::endResChain(ClauseId id) { d_resStack.pop_back(); } -// template <class Solver> -// void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) { -// Assert(d_resStack.size() > 0); -// ClauseId id = registerClause(clause, LEARNT); -// ResChain<Solver>* res = d_resStack.back(); -// registerResolution(id, res); -// d_resStack.pop_back(); -// } - template <class Solver> void TSatProof<Solver>::endResChain(typename Solver::TLit lit) { Assert(d_resStack.size() > 0); @@ -846,11 +822,6 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { registerResolution(unit_id, res); return unit_id; } -template <class Solver> -void TSatProof<Solver>::toStream(std::ostream& out) { - Debug("proof:sat") << "TSatProof<Solver>::printProof\n"; - Unimplemented("native proof printing not supported yet"); -} template <class Solver> ClauseId TSatProof<Solver>::storeUnitConflict( @@ -985,21 +956,6 @@ bool TSatProof<Solver>::proofConstructed() const { } template <class Solver> -std::string TSatProof<Solver>::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 <class Solver> prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) { if (isUnit(id)) { typename Solver::TLit lit = getUnit(id); @@ -1105,92 +1061,6 @@ TSatProof<Solver>::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); } -/// LFSCSatProof class -template <class Solver> -void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, - std::ostream& paren) { - out << "(satlem_simplify _ _ _"; - paren << ")"; - - const ResChain<Solver>& res = this->getResolutionChain(id); - const typename ResChain<Solver>::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 <class Solver> -void LFSCSatProof<Solver>::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<typename Solver::TLit>& confl = - *(this->d_assumptionConflictsDebug[id]); - - Assert(confl.size()); - - for (unsigned i = 0; i < confl.size(); ++i) { - prop::SatLiteral lit = toSatLiteral<Solver>(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<Solver>(confl[i]); - prop::SatVariable v = lit.getSatVariable(); - out << "unit" << v << " "; - out << ProofManager::getVarName(v, this->d_name) << ")"; - } - out << "(\\ e e)\n"; - paren << ")"; -} - -template <class Solver> -void LFSCSatProof<Solver>::printResolutions(std::ostream& out, - std::ostream& paren) { - Debug("bv-proof") << "; print resolutions" << std::endl; - std::set<ClauseId>::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 <class Solver> -void LFSCSatProof<Solver>::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: |