src/proof/lfsc_proof_printer.cpp

   1 /*********************                                                        */
   2 /*! \file lfsc_proof_printer.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Alex Ozdemir, Liana Hadarean
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Prints proofs in the LFSC format
  13  **
  14  ** Prints proofs in the LFSC format.
  15  **/
  16
  17 #include "proof/lfsc_proof_printer.h"
  18
  19 #include <algorithm>
  20 #include <iostream>
  21 #include <iterator>
  22
  23 #include "prop/bvminisat/core/Solver.h"
  24 #include "prop/minisat/core/Solver.h"
  25
  26 namespace CVC4 {
  27 namespace proof {
  28
  29 template <class Solver>
  30 std::string LFSCProofPrinter::clauseName(TSatProof<Solver>* satProof,
  31                                          ClauseId id)
  32 {
  33   std::ostringstream os;
  34   if (satProof->isInputClause(id))
  35   {
  36     os << ProofManager::getInputClauseName(id, satProof->getName());
  37   }
  38   else if (satProof->isLemmaClause(id))
  39   {
  40     os << ProofManager::getLemmaClauseName(id, satProof->getName());
  41   }
  42   else
  43   {
  44     os << ProofManager::getLearntClauseName(id, satProof->getName());
  45   }
  46   return os.str();
  47 }
  48
  49 template <class Solver>
  50 void LFSCProofPrinter::printResolution(TSatProof<Solver>* satProof,
  51                                        ClauseId id,
  52                                        std::ostream& out,
  53                                        std::ostream& paren)
  54 {
  55   out << "(satlem_simplify _ _ _";
  56   paren << ")";
  57
  58   const ResChain<Solver>& res = satProof->getResolutionChain(id);
  59   const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
  60
  61   for (int i = steps.size() - 1; i >= 0; i--)
  62   {
  63     out << " (";
  64     out << (steps[i].sign ? "R" : "Q") << " _ _";
  65   }
  66
  67   ClauseId start_id = res.getStart();
  68   out << " " << clauseName(satProof, start_id);
  69
  70   for (unsigned i = 0; i < steps.size(); i++)
  71   {
  72     prop::SatVariable v =
  73         prop::MinisatSatSolver::toSatVariable(var(steps[i].lit));
  74     out << " " << clauseName(satProof, steps[i].id) << " "
  75         << ProofManager::getVarName(v, satProof->getName()) << ")";
  76   }
  77
  78   if (id == satProof->getEmptyClauseId())
  79   {
  80     out << " (\\ empty empty)";
  81     return;
  82   }
  83
  84   out << " (\\ " << clauseName(satProof, id) << "\n";  // bind to lemma name
  85   paren << ")";
  86 }
  87
  88 template <class Solver>
  89 void LFSCProofPrinter::printAssumptionsResolution(TSatProof<Solver>* satProof,
  90                                                   ClauseId id,
  91                                                   std::ostream& out,
  92                                                   std::ostream& paren)
  93 {
  94   Assert(satProof->isAssumptionConflict(id));
  95   // print the resolution proving the assumption conflict
  96   printResolution(satProof, id, out, paren);
  97   // resolve out assumptions to prove empty clause
  98   out << "(satlem_simplify _ _ _ ";
  99   const std::vector<typename Solver::TLit>& confl =
 100       *(satProof->getAssumptionConflicts().at(id));
 101
 102   Assert(confl.size());
 103
 104   for (unsigned i = 0; i < confl.size(); ++i)
 105   {
 106     prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
 107     out << "(";
 108     out << (lit.isNegated() ? "Q" : "R") << " _ _ ";
 109   }
 110
 111   out << clauseName(satProof, id) << " ";
 112   for (int i = confl.size() - 1; i >= 0; --i)
 113   {
 114     prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
 115     prop::SatVariable v = lit.getSatVariable();
 116     out << "unit" << v << " ";
 117     out << ProofManager::getVarName(v, satProof->getName()) << ")";
 118   }
 119   out << "(\\ e e)\n";
 120   paren << ")";
 121 }
 122
 123 template <class Solver>
 124 void LFSCProofPrinter::printResolutions(TSatProof<Solver>* satProof,
 125                                         std::ostream& out,
 126                                         std::ostream& paren)
 127 {
 128   Debug("bv-proof") << "; print resolutions" << std::endl;
 129   std::set<ClauseId>::iterator it = satProof->getSeenLearnt().begin();
 130   for (; it != satProof->getSeenLearnt().end(); ++it)
 131   {
 132     if (*it != satProof->getEmptyClauseId())
 133     {
 134       Debug("bv-proof") << "; print resolution for " << *it << std::endl;
 135       printResolution(satProof, *it, out, paren);
 136     }
 137   }
 138   Debug("bv-proof") << "; done print resolutions" << std::endl;
 139 }
 140
 141 template <class Solver>
 142 void LFSCProofPrinter::printResolutionEmptyClause(TSatProof<Solver>* satProof,
 143                                                   std::ostream& out,
 144                                                   std::ostream& paren)
 145 {
 146   printResolution(satProof, satProof->getEmptyClauseId(), out, paren);
 147 }
 148
 149 void LFSCProofPrinter::printSatInputProof(const std::vector<ClauseId>& clauses,
 150                                       std::ostream& out,
 151                                       const std::string& namingPrefix)
 152 {
 153   for (auto i = clauses.begin(), end = clauses.end(); i != end; ++i)
 154   {
 155     out << "\n    (cnfc_proof _ _ _ "
 156         << ProofManager::getInputClauseName(*i, namingPrefix) << " ";
 157   }
 158   out << "cnfn_proof";
 159   std::fill_n(std::ostream_iterator<char>(out), clauses.size(), ')');
 160 }
 161
 162 void LFSCProofPrinter::printCMapProof(const std::vector<ClauseId>& clauses,
 163                                       std::ostream& out,
 164                                       const std::string& namingPrefix)
 165 {
 166   for (size_t i = 0, n = clauses.size(); i < n; ++i)
 167   {
 168     out << "\n    (CMapc_proof " << (i + 1) << " _ _ _ "
 169         << ProofManager::getInputClauseName(clauses[i], namingPrefix) << " ";
 170   }
 171   out << "CMapn_proof";
 172   std::fill_n(std::ostream_iterator<char>(out), clauses.size(), ')');
 173 }
 174
 175 void LFSCProofPrinter::printSatClause(const prop::SatClause& clause,
 176                                       std::ostream& out,
 177                                       const std::string& namingPrefix)
 178 {
 179   for (auto i = clause.cbegin(); i != clause.cend(); ++i)
 180   {
 181     out << "(clc " << (i->isNegated() ? "(neg " : "(pos ")
 182         << ProofManager::getVarName(i->getSatVariable(), namingPrefix) << ") ";
 183   }
 184   out << "cln";
 185   std::fill_n(std::ostream_iterator<char>(out), clause.size(), ')');
 186 }
 187
 188 // Template specializations
 189 template void LFSCProofPrinter::printAssumptionsResolution(
 190     TSatProof<CVC4::Minisat::Solver>* satProof,
 191     ClauseId id,
 192     std::ostream& out,
 193     std::ostream& paren);
 194 template void LFSCProofPrinter::printResolutions(
 195     TSatProof<CVC4::Minisat::Solver>* satProof,
 196     std::ostream& out,
 197     std::ostream& paren);
 198 template void LFSCProofPrinter::printResolutionEmptyClause(
 199     TSatProof<CVC4::Minisat::Solver>* satProof,
 200     std::ostream& out,
 201     std::ostream& paren);
 202
 203 template void LFSCProofPrinter::printAssumptionsResolution(
 204     TSatProof<CVC4::BVMinisat::Solver>* satProof,
 205     ClauseId id,
 206     std::ostream& out,
 207     std::ostream& paren);
 208 template void LFSCProofPrinter::printResolutions(
 209     TSatProof<CVC4::BVMinisat::Solver>* satProof,
 210     std::ostream& out,
 211     std::ostream& paren);
 212 template void LFSCProofPrinter::printResolutionEmptyClause(
 213     TSatProof<CVC4::BVMinisat::Solver>* satProof,
 214     std::ostream& out,
 215     std::ostream& paren);
 216 }  // namespace proof
 217 }  // namespace CVC4