Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * The module for printing Alethe proof nodes
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__PROOF__ALETHE__ALETHE_PROOF_PRINTER_H
      16                 :            : #define CVC5__PROOF__ALETHE__ALETHE_PROOF_PRINTER_H
      17                 :            : 
      18                 :            : #include "context/cdhashset.h"
      19                 :            : #include "proof/alethe/alethe_let_binding.h"
      20                 :            : #include "proof/alethe/alethe_node_converter.h"
      21                 :            : #include "proof/alethe/alethe_proof_rule.h"
      22                 :            : #include "proof/proof_node.h"
      23                 :            : #include "proof/proof_node_updater.h"
      24                 :            : #include "smt/env_obj.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : 
      28                 :            : namespace proof {
      29                 :            : 
      30                 :            : /** A callback for populating a let binder.
      31                 :            :  *
      32                 :            :  * This callback does not actually update the proof node, but rather just
      33                 :            :  * considers the terms in the proof nodes for sharing. This is done in
      34                 :            :  * `shouldUpdate`, which is called on every proof node and always returns false.
      35                 :            :  */
      36                 :            : class LetUpdaterPfCallback : public ProofNodeUpdaterCallback
      37                 :            : {
      38                 :            :  public:
      39                 :            :   LetUpdaterPfCallback(AletheLetBinding& lbind);
      40                 :            :   ~LetUpdaterPfCallback();
      41                 :            :   void initializeUpdate();
      42                 :            :   /** Analyze the given proof node and populate d_lbind with its terms.
      43                 :            :    *
      44                 :            :    * Always returns false. */
      45                 :            :   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
      46                 :            :                     const std::vector<Node>& fa,
      47                 :            :                     bool& continueUpdate) override;
      48                 :            : 
      49                 :            :  protected:
      50                 :            :   /** The let binder populated during the update. */
      51                 :            :   AletheLetBinding& d_lbind;
      52                 :            : };
      53                 :            : 
      54                 :            : /**
      55                 :            :  * The Alethe printer, which prints proof nodes in an Alethe proof, according to
      56                 :            :  * the proof rules defined in alethe_proof_rule.h.
      57                 :            :  *
      58                 :            :  * It expects to print proof nodes that have been processed by the Alethe proof
      59                 :            :  * post-processor.
      60                 :            :  */
      61                 :            : class AletheProofPrinter : protected EnvObj
      62                 :            : {
      63                 :            :  public:
      64                 :            :   AletheProofPrinter(Env& env, AletheNodeConverter& anc);
      65                 :        476 :   ~AletheProofPrinter() {}
      66                 :            :   /**
      67                 :            :    * Prints a proof node in the Alethe proof format
      68                 :            :    *
      69                 :            :    * @param out The stream to write to
      70                 :            :    * @param pfn The proof node to be printed
      71                 :            :    * @param assertionNames Mapping between assertions and names, if they were
      72                 :            :    * given by the user.
      73                 :            :    */
      74                 :            :   void print(std::ostream& out,
      75                 :            :              std::shared_ptr<ProofNode> pfn,
      76                 :            :              const std::map<Node, std::string>& assertionNames);
      77                 :            : 
      78                 :            :  private:
      79                 :            :   /** The printing context */
      80                 :            :   context::Context d_context;
      81                 :            :   /** Assumptions in context */
      82                 :            :   context::CDHashMap<Node, std::string> d_assumptionsMap;
      83                 :            :   /** Printed steps in context */
      84                 :            :   context::CDHashMap<ProofNode*, std::string> d_pfMap;
      85                 :            : 
      86                 :            :   /** Prints an Alethe proof node
      87                 :            :    *
      88                 :            :    * The printing is parameterized by a prefix to be used in the step ids, as
      89                 :            :    * well as by the current id (which will be incremented after this proof node,
      90                 :            :    * if it is fresh, is printed). The prefix is used to facilitate identifying
      91                 :            :    * that steps are under a given anchor.
      92                 :            :    *
      93                 :            :    * @param out The stream to write to
      94                 :            :    * @param prefix The prefix to be used in step ids.
      95                 :            :    * @param id The current id being used for printing step ids
      96                 :            :    * @param pfn The proof node to be printed
      97                 :            :    */
      98                 :            :   void printInternal(std::ostream& out,
      99                 :            :                      const std::string& prefix,
     100                 :            :                      size_t& id,
     101                 :            :                      std::shared_ptr<ProofNode> pfn);
     102                 :            : 
     103                 :            :   /** Print term into stream
     104                 :            :    *
     105                 :            :    * The printing is done separately because it uses the let binder (d_lbind)
     106                 :            :    * for converting the term before printing.
     107                 :            :    *
     108                 :            :    * @param out The stream to write to
     109                 :            :    * @param n The node to be printed
     110                 :            :    */
     111                 :            :   void printTerm(std::ostream& out, TNode n);
     112                 :            : 
     113                 :            :   /** Print the id for the previously printed step/assumption of the given proof
     114                 :            :    * node.
     115                 :            :    *
     116                 :            :    * @param out The stream to write to
     117                 :            :    * @param pfn The proof node
     118                 :            :    * @param assumptionsMap Map from assumptions to their ids
     119                 :            :    * @param pfMap Map from proof nodes to their ids
     120                 :            :    */
     121                 :            :   void printStepId(std::ostream& out, std::shared_ptr<ProofNode> pfn);
     122                 :            : 
     123                 :            :   /** Print the step with respective id, rule, premises and arguments.
     124                 :            :    *
     125                 :            :    * @param out The stream to write to
     126                 :            :    * @param stepId The id of the step
     127                 :            :    * @param rule The Alethe rule of the step
     128                 :            :    * @param pfArgs The arguments of this step
     129                 :            :    * @param pfChildren The premises of this step
     130                 :            :    */
     131                 :            :   void printStep(std::ostream& out,
     132                 :            :                  const std::string& stepId,
     133                 :            :                  AletheRule arule,
     134                 :            :                  const std::vector<Node>& pfArgs,
     135                 :            :                  const std::vector<std::shared_ptr<ProofNode>>& pfChildren);
     136                 :            : 
     137                 :            :   /** The let binder for printing with sharing. */
     138                 :            :   AletheLetBinding d_lbind;
     139                 :            : 
     140                 :            :   /** The Alethe node converter */
     141                 :            :   AletheNodeConverter& d_anc;
     142                 :            : 
     143                 :            :   /** The callback used for computing the let binding. */
     144                 :            :   std::unique_ptr<LetUpdaterPfCallback> d_cb;
     145                 :            : };
     146                 :            : 
     147                 :            : }  // namespace proof
     148                 :            : 
     149                 :            : }  // namespace cvc5::internal
     150                 :            : 
     151                 :            : #endif /* CVC5__PROOF__ALETHE__ALETHE_PROOF_PRINTER_H */