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 \
**/
+#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"
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);
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 {
}
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;
}
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) {
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;
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
#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"
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())));
}
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);
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
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();
class BitVectorProof;
template <class Solver> class LFSCSatProof;
-typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof;
+typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
class LFSCCnfProof;
class LFSCTheoryProofEngine;
{
public:
LFSCProof(SmtEngine* smtEngine,
- LFSCCoreSatProof* sat,
+ CoreSatProof* sat,
LFSCCnfProof* cnf,
LFSCTheoryProofEngine* theory);
~LFSCProof() override {}
void checkUnrewrittenAssertion(const NodeSet& assertions) const;
- LFSCCoreSatProof* d_satProof;
+ CoreSatProof* d_satProof;
LFSCCnfProof* d_cnfProof;
LFSCTheoryProofEngine* d_theoryProof;
SmtEngine* d_smtEngine;
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);
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);
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);
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;
VarSet d_assumptions; // assumption literals for bv solver
IdHashSet d_assumptionConflicts; // assumption conflicts not actually added
// to SAT solver
- IdToConflicts d_assumptionConflictsDebug;
// Resolutions.
ResStack d_resStack;
bool d_checkRes;
- const ClauseId d_emptyClauseId;
const ClauseId d_nullId;
// temporary map for updating CRefs
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);
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),
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),
}
}
-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
return *chain;
}
-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();
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);
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(
return d_satProofConstructed;
}
-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)) {
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:
projects / cvc5.git / commitdiff