1 /********************* */ 2 /*! \file lfsc_proof_printer.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andres Noetzli, Alex Ozdemir 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 "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 */ 155