summaryrefslogtreecommitdiff
path: root/src/proof/lfsc_proof_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/lfsc_proof_printer.cpp')
-rw-r--r--src/proof/lfsc_proof_printer.cpp217
1 files changed, 0 insertions, 217 deletions
diff --git a/src/proof/lfsc_proof_printer.cpp b/src/proof/lfsc_proof_printer.cpp
deleted file mode 100644
index 464083841..000000000
--- a/src/proof/lfsc_proof_printer.cpp
+++ /dev/null
@@ -1,217 +0,0 @@
-/********************* */
-/*! \file lfsc_proof_printer.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andres Noetzli, Alex Ozdemir, Liana Hadarean
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 <algorithm>
-#include <iostream>
-#include <iterator>
-
-#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);
-}
-
-void LFSCProofPrinter::printSatInputProof(const std::vector<ClauseId>& clauses,
- std::ostream& out,
- const std::string& namingPrefix)
-{
- for (auto i = clauses.begin(), end = clauses.end(); i != end; ++i)
- {
- out << "\n (cnfc_proof _ _ _ "
- << ProofManager::getInputClauseName(*i, namingPrefix) << " ";
- }
- out << "cnfn_proof";
- std::fill_n(std::ostream_iterator<char>(out), clauses.size(), ')');
-}
-
-void LFSCProofPrinter::printCMapProof(const std::vector<ClauseId>& clauses,
- std::ostream& out,
- const std::string& namingPrefix)
-{
- for (size_t i = 0, n = clauses.size(); i < n; ++i)
- {
- out << "\n (CMapc_proof " << (i + 1) << " _ _ _ "
- << ProofManager::getInputClauseName(clauses[i], namingPrefix) << " ";
- }
- out << "CMapn_proof";
- std::fill_n(std::ostream_iterator<char>(out), clauses.size(), ')');
-}
-
-void LFSCProofPrinter::printSatClause(const prop::SatClause& clause,
- std::ostream& out,
- const std::string& namingPrefix)
-{
- for (auto i = clause.cbegin(); i != clause.cend(); ++i)
- {
- out << "(clc " << (i->isNegated() ? "(neg " : "(pos ")
- << ProofManager::getVarName(i->getSatVariable(), namingPrefix) << ") ";
- }
- out << "cln";
- std::fill_n(std::ostream_iterator<char>(out), clause.size(), ')');
-}
-
-// 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback