src/proof/lfsc_proof_printer.h

   1 /*********************                                                        */
   2 /*! \file lfsc_proof_printer.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Alex Ozdemir, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 "cvc4_private.h"
  18
  19 #ifndef CVC4__PROOF__LFSC_PROOF_PRINTER_H
  20 #define CVC4__PROOF__LFSC_PROOF_PRINTER_H
  21
  22 #include <iosfwd>
  23 #include <string>
  24 #include <vector>
  25
  26 #include "proof/clause_id.h"
  27 #include "proof/proof_manager.h"
  28 #include "proof/sat_proof.h"
  29 #include "proof/sat_proof_implementation.h"
  30 #include "util/proof.h"
  31
  32 namespace CVC4 {
  33 namespace proof {
  34
  35 class LFSCProofPrinter
  36 {
  37  public:
  38   /**
  39    * Prints the resolution proof for an assumption conflict.
  40    *
  41    * @param satProof The record of the reasoning done by the SAT solver
  42    * @param id The clause to print a proof for
  43    * @param out The stream to print to
  44    * @param paren A stream for the closing parentheses
  45    */
  46   template <class Solver>
  47   static void printAssumptionsResolution(TSatProof<Solver>* satProof,
  48                                          ClauseId id,
  49                                          std::ostream& out,
  50                                          std::ostream& paren);
  51
  52   /**
  53    * Prints the resolution proofs for learned clauses that have been used to
  54    * deduce unsat.
  55    *
  56    * @param satProof The record of the reasoning done by the SAT solver
  57    * @param out The stream to print to
  58    * @param paren A stream for the closing parentheses
  59    */
  60   template <class Solver>
  61   static void printResolutions(TSatProof<Solver>* satProof,
  62                                std::ostream& out,
  63                                std::ostream& paren);
  64
  65   /**
  66    * Prints the resolution proof for the empty clause.
  67    *
  68    * @param satProof The record of the reasoning done by the SAT solver
  69    * @param out The stream to print to
  70    * @param paren A stream for the closing parentheses
  71    */
  72   template <class Solver>
  73   static void printResolutionEmptyClause(TSatProof<Solver>* satProof,
  74                                          std::ostream& out,
  75                                          std::ostream& paren);
  76
  77   /**
  78    * The SAT solver is given a list of clauses.
  79    * Assuming that each clause has alreay been individually proven,
  80    * defines a proof of the input to the SAT solver.
  81    *
  82    * Prints an LFSC value corresponding to the proof, i.e. a value of type
  83    * (cnf_holds ...)
  84    *
  85    * @param clauses The clauses to print a proof of
  86    * @param out The stream to print to
  87    * @param namingPrefix The prefix for LFSC names
  88    */
  89   static void printSatInputProof(const std::vector<ClauseId>& clauses,
  90                                  std::ostream& out,
  91                                  const std::string& namingPrefix);
  92
  93   /**
  94    * The LRAT proof signature uses the concept of a _clause map_ (CMap), which
  95    * represents an indexed collection of (conjoined) clauses.
  96    *
  97    * Specifically, the signatures rely on a proof that a CMap containing the
  98    * clauses given to the SAT solver hold.
  99    *
 100    * Assuming that the individual clauses already have proofs, this function
 101    * prints a proof of the CMap mapping 1 to the first clause, 2 to the second,
 102    * and so on.
 103    *
 104    * That is, it prints a value of type (CMap_holds ...)
 105    *
 106    * @param clauses The clauses to print a proof of
 107    * @param out The stream to print to
 108    * @param namingPrefix The prefix for LFSC names
 109    */
 110   static void printCMapProof(const std::vector<ClauseId>& clauses,
 111                              std::ostream& out,
 112                              const std::string& namingPrefix);
 113
 114   /**
 115    * Prints a clause
 116    *
 117    * @param clause The clause to print
 118    * @param out The stream to print to
 119    * @param namingPrefix The prefix for LFSC names
 120    */
 121   static void printSatClause(const prop::SatClause& clause,
 122                              std::ostream& out,
 123                              const std::string& namingPrefix);
 124
 125  private:
 126
 127   /**
 128    * Maps a clause id to a string identifier used in the LFSC proof.
 129    *
 130    * @param satProof The record of the reasoning done by the SAT solver
 131    * @param id The clause to map to a string
 132    */
 133   template <class Solver>
 134   static std::string clauseName(TSatProof<Solver>* satProof, ClauseId id);
 135
 136   /**
 137    * Prints the resolution proof for a given clause.
 138    *
 139    * @param satProof The record of the reasoning done by the SAT solver
 140    * @param id The clause to print a proof for
 141    * @param out The stream to print to
 142    * @param paren A stream for the closing parentheses
 143    */
 144   template <class Solver>
 145   static void printResolution(TSatProof<Solver>* satProof,
 146                               ClauseId id,
 147                               std::ostream& out,
 148                               std::ostream& paren);
 149 };
 150
 151 }  // namespace proof
 152 }  // namespace CVC4
 153
 154 #endif /* CVC4__PROOF__LFSC_PROOF_PRINTER_H */