src/proof/dot/dot_printer.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Diego Della Rocca de Camargos, Haniel Barbosa, Vinícius Braga Freire
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2022 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.
  11  * ****************************************************************************
  12  *
  13  * The module for printing dot proofs.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__PROOF__DOT__DOT_PRINTER_H
  19 #define CVC5__PROOF__DOT__DOT_PRINTER_H
  20
  21 #include <iostream>
  22 #include <stack>
  23
  24 #include "printer/let_binding.h"
  25 #include "proof/proof_node.h"
  26 #include "smt/env_obj.h"
  27
  28 namespace cvc5::internal {
  29 namespace proof {
  30
  31 /**
  32  * An enumeration for proof nodes cluster type. Each type defines in which
  33  * cluster the proof node will be inserted when printed.
  34  */
  35 enum class ProofNodeClusterType : uint8_t
  36 {
  37   // ======== FIRST_SCOPE
  38   // Type of proof node cluster that is always in the root of the graph.
  39   // The rule is always SCOPE.
  40   FIRST_SCOPE = 0,
  41   // ======== SAT
  42   // Type of proof node cluster that is between FIRST_SCOPE and CNF.
  43   // The rules are: CHAIN_RESOLUTION, FACTORING, REORDERING, MACRO_RESOLUTION
  44   // and MACRO_RESOLUTION_TRUST.
  45   SAT,
  46   // ======== CNF
  47   // Type of proof node cluster that is below SAT and above THEORY_LEMMA or
  48   // PRE_PROCESSING.
  49   // The rules, that are described by the PfRule enumeration, are in the range
  50   // between NOT_NOT_ELIM and CNF_ITE_NEG3.
  51   CNF,
  52   // ======== THEORY_LEMMA
  53   // Proof nodes contained in a SCOPE which starts just after a SAT or CNF proof
  54   // cluster.
  55   THEORY_LEMMA,
  56   // ======== PRE_PROCESSING
  57   // Type of proof node cluster that is in the middle of the proof.
  58   // The rules can be of any type. The proof nodes that aren't THEORY_LEMMA
  59   // after CNF are PRE_PROCESSING. Therefore, the root of this cluster type
  60   // can't be a SCOPE proof node.
  61   PRE_PROCESSING,
  62   // ======== INPUT
  63   // Type of proof node that is always a leaf with regard to the FIRST_SCOPE.
  64   // The rules are always ASSUME and the argument assumed by it was only scoped
  65   // by the FIRST_SCOPE and no other SCOPE, i.e., it was not shadowed by an
  66   // inner scope.
  67   INPUT,
  68   // ======== NOT_DEFINED
  69   NOT_DEFINED
  70 };
  71
  72 class DotPrinter : protected EnvObj
  73 {
  74  public:
  75   DotPrinter(Env& env);
  76   ~DotPrinter();
  77
  78   /**
  79    * Print the full proof of assertions => false by pn using the dot format.
  80    * @param out the output stream
  81    * @param pn the root node of the proof to print
  82    */
  83   void print(std::ostream& out, const ProofNode* pn);
  84
  85  private:
  86   /**
  87    * Print the nodes of the proof in the format:
  88    * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", comment =
  89    * "{\"subProofQty\":$SUB_PROOF_QUANTITY}" ]; and then for each child of the
  90    * node $CHILD_ID -> $NODE_ID; and then recursively calls the function with
  91    * the child as argument.
  92    * @param out the output stream
  93    * @param pn the proof node to print
  94    * @param pfLetClosed the map from proof node hashs, of closed proof nodes, to
  95    * their printed ids
  96    * @param pfLetOpen the map, local to the current scope, of proof node hashs
  97    * to their printed ids
  98    * @param cfaMap the map from proof nodes to whether they contain assumptions
  99    * @param ancestorHashs a vector containing the hashs of all the proof nodes
 100    * ancestors traversed to get to pn
 101    * @param parentType the type of the parent node
 102    * @return the id of the proof node printed
 103    */
 104   uint64_t printInternal(std::ostream& out,
 105                          const ProofNode* pn,
 106                          std::map<size_t, uint64_t>& pfLetClosed,
 107                          std::map<size_t, uint64_t>& pfLetOpen,
 108                          std::unordered_map<const ProofNode*, bool>& cfaMap,
 109                          std::vector<size_t>& ancestorHashs,
 110                          ProofNodeClusterType parentType);
 111
 112   /**
 113    * Print the nodes of the proof in the format:
 114    * $NODE_ID [ label = "{$CONCLUSION|$RULE_NAME($RULE_ARGUMENTS)}", comment =
 115    * "{\"subProofQty\":$SUB_PROOF_QUANTITY}" ];
 116    * @param out the output stream
 117    * @param pn the proof node to print
 118    */
 119   inline void printProofNodeInfo(std::ostream& out, const ProofNode* pn);
 120
 121   /**
 122    * Return the arguments of a ProofNode
 123    * @param currentArguments an ostringstream that will store the arguments of
 124    * pn formatted as "$ARG[0], $ARG[1], ..., $ARG[N-1]"
 125    * @param pn a ProofNode
 126    */
 127   void ruleArguments(std::ostringstream& currentArguments, const ProofNode* pn);
 128
 129   /** Add an escape character before special characters of the given string.
 130    * @param s The string to have the characters processed.
 131    * @return The string with the special characters escaped.
 132    */
 133   static std::string sanitizeString(const std::string& s);
 134
 135   /** As above, but quotes are doubly escaped. */
 136   static std::string sanitizeStringDoubleQuotes(const std::string& s);
 137
 138   /** Traverse proof node and populate d_subpfCounter, mapping each proof node
 139    * to the number of subproofs it contains, including itself
 140    *
 141    * @param pn the proof node to be traversed
 142    */
 143   void countSubproofs(const ProofNode* pn);
 144
 145   /** Traverse proof node and populate d_lbind
 146    *
 147    * @param pn The proof node to be traversed
 148    */
 149   void letifyResults(const ProofNode* pn);
 150
 151   /** Define the proof node type and populate d_nodesClusterType and
 152    * d_scopesArgs.
 153    * @param pn The proof node to categorize.
 154    * @param last The type of the parent of the current proof node
 155    * @return the current node type
 156    */
 157   ProofNodeClusterType defineProofNodeType(const ProofNode* pn,
 158                                            ProofNodeClusterType last);
 159
 160   /** Whether the proof node is an input node or not. An input is a proof node
 161    * that has an ASSUME rule and the argument assumed by it must be scoped only
 162    * by the FIRST SCOPE. In other words, if there is at least one SCOPE (other
 163    * than the FIRST SCOPE) that is an ancestor of this ASSUME proof node and its
 164    * argument is scoped by this ancestor, then the ASSUME is no longer an input.
 165    * @param pn The proof node to be verified.
 166    * @return The bool indicating if the proof node is or not an input.
 167    */
 168   inline bool isInput(const ProofNode* pn);
 169
 170   /** Verify if the rule is in the SAT range (i.e. a PfRule that is
 171    * CHAIN_RESOLUTION, FACTORING, REORDERING, MACRO_RESOLUTION or
 172    * MACRO_RESOLUTION_TRUST).
 173    * @param rule The rule to be verified.
 174    * @return The bool indicating if the rule is or not in the SAT range.
 175    */
 176   inline bool isSat(const PfRule& rule);
 177
 178   /** Verify if the rule is in the CNF range (between NOT_NOT_ELIM and
 179    * CNF_ITE_NEG3) in the PfRule enumeration.
 180    * @param rule The rule to be verified.
 181    * @return The bool indicating if the rule is or not in the CNF range.
 182    */
 183   inline bool isCNF(const PfRule& rule);
 184
 185   /** Verify if the rule is a SCOPE
 186    * @param rule The rule to be verified.
 187    * @return The bool indicating if the rule is or not a SCOPE.
 188    */
 189   inline bool isSCOPE(const PfRule& rule);
 190
 191   /** Verify if the rule is in the theory lemma range (open interval between
 192    * CNF_ITE_NEG3 and LFSC_RULE) or if the rule is a SCOPE or THEORY_LEMMA.
 193    * @param rule The rule to be verified.
 194    * @return The bool indicating whether the rule is for a theory lemma
 195    * range.
 196    */
 197   inline bool isTheoryLemma(const PfRule& rule);
 198
 199   /** Verify if the rule is an ASSUME
 200    * @param rule The rule to be verified.
 201    * @return The bool indicating if the rule is or not an ASSUME.
 202    */
 203   inline bool isASSUME(const PfRule& rule);
 204
 205   /** All unique subproofs of a given proof node (counting itself). */
 206   std::map<const ProofNode*, size_t> d_subpfCounter;
 207
 208   /** Let binder for terms in proof nodes */
 209   LetBinding d_lbind;
 210
 211   /** Counter that indicates the current rule ID */
 212   uint64_t d_ruleID;
 213
 214   /** The arguments (assumptions), per level, of all scopes under which the
 215    * traversal is currently under. */
 216   std::vector<std::reference_wrapper<const std::vector<Node>>> d_scopesArgs;
 217
 218   /** All the subgraph description strings */
 219   std::vector<std::ostringstream> d_subgraphsStr;
 220 };
 221
 222 }  // namespace proof
 223 }  // namespace cvc5::internal
 224
 225 #endif