Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Hans-Joerg Schurr
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * Print channels for LFSC proofs.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__PROOF__LFSC__LFSC_PRINT_CHANNEL_H
      19                 :            : #define CVC5__PROOF__LFSC__LFSC_PRINT_CHANNEL_H
      20                 :            : 
      21                 :            : #include <iostream>
      22                 :            : #include <map>
      23                 :            : 
      24                 :            : #include "expr/node.h"
      25                 :            : #include "printer/let_binding.h"
      26                 :            : #include "proof/lfsc/lfsc_util.h"
      27                 :            : #include "proof/proof_node.h"
      28                 :            : #include "rewriter/rewrite_proof_rule.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : namespace proof {
      32                 :            : 
      33                 :            : /**
      34                 :            :  * LFSC proofs are printed in two phases: the first phase computes the
      35                 :            :  * letification of terms in the proof as well as other information that is
      36                 :            :  * required for printing the preamble of the proof. The second phase prints the
      37                 :            :  * proof to an output stream. This is the base class for these two phases.
      38                 :            :  */
      39                 :            : class LfscPrintChannel
      40                 :            : {
      41                 :            :  public:
      42                 :       2834 :   LfscPrintChannel() {}
      43                 :       2834 :   virtual ~LfscPrintChannel() {}
      44                 :            :   /** Print node n */
      45                 :          0 :   virtual void printNode(TNode n) {}
      46                 :            :   /** Print type node n */
      47                 :      15479 :   virtual void printTypeNode(TypeNode tn) {}
      48                 :            :   /** Print a hole */
      49                 :   20348500 :   virtual void printHole() {}
      50                 :            :   /**
      51                 :            :    * Print an application of the trusting the result res, whose source is the
      52                 :            :    * given proof rule.
      53                 :            :    */
      54                 :          0 :   virtual void printTrust(TNode res, ProofRule src) {}
      55                 :            :   /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */
      56                 :          0 :   virtual void printOpenRule(const ProofNode* pn) {}
      57                 :            :   /** Print the opening of LFSC rule lr, e.g. "(cong " */
      58                 :    1179250 :   virtual void printOpenLfscRule(LfscRule lr) {}
      59                 :            :   /** Print the closing of # nparen proof rules */
      60                 :    8292260 :   virtual void printCloseRule(size_t nparen = 1) {}
      61                 :            :   /** Print an identifier for the given prefix */
      62                 :    3667640 :   virtual void printId(size_t id, const std::string& prefix) {}
      63                 :            :   /** Print an end line */
      64                 :    1198480 :   virtual void printEndLine() {}
      65                 :            : };
      66                 :            : 
      67                 :            : /** Prints the proof to output stream d_out */
      68                 :            : class LfscPrintChannelOut : public LfscPrintChannel
      69                 :            : {
      70                 :            :  public:
      71                 :            :   LfscPrintChannelOut(std::ostream& out);
      72                 :            :   void printNode(TNode n) override;
      73                 :            :   void printTypeNode(TypeNode tn) override;
      74                 :            :   void printHole() override;
      75                 :            :   void printTrust(TNode res, ProofRule src) override;
      76                 :            :   void printOpenRule(const ProofNode* pn) override;
      77                 :            :   void printOpenLfscRule(LfscRule lr) override;
      78                 :            :   void printCloseRule(size_t nparen = 1) override;
      79                 :            :   void printId(size_t id, const std::string& prefix) override;
      80                 :            :   void printEndLine() override;
      81                 :            :   //------------------- helper methods
      82                 :            :   /**
      83                 :            :    * Print node to stream in the expected format of LFSC.
      84                 :            :    */
      85                 :            :   static void printNodeInternal(std::ostream& out, Node n);
      86                 :            :   /**
      87                 :            :    * Print type node to stream in the expected format of LFSC.
      88                 :            :    */
      89                 :            :   static void printTypeNodeInternal(std::ostream& out, TypeNode tn);
      90                 :            :   static void printRule(std::ostream& out, const ProofNode* pn);
      91                 :            :   static void printId(std::ostream& out, size_t id, const std::string& prefix);
      92                 :            :   static void printProofRewriteRule(std::ostream& out, ProofRewriteRule id);
      93                 :            :   //------------------- end helper methods
      94                 :            :  private:
      95                 :            :   /**
      96                 :            :    * Replaces "(_ " with "(" to eliminate indexed symbols
      97                 :            :    * Replaces "__LFSC_TMP" with ""
      98                 :            :    */
      99                 :            :   static void cleanSymbols(std::string& s);
     100                 :            :   /** The output stream */
     101                 :            :   std::ostream& d_out;
     102                 :            : };
     103                 :            : 
     104                 :            : /**
     105                 :            :  * Run on the proof before it is printed, and does two preparation steps:
     106                 :            :  * - Computes the letification of nodes that appear in the proof.
     107                 :            :  * - Computes the set of DSL rules that appear in the proof.
     108                 :            :  */
     109                 :            : class LfscPrintChannelPre : public LfscPrintChannel
     110                 :            : {
     111                 :            :  public:
     112                 :            :   LfscPrintChannelPre(LetBinding& lbind);
     113                 :            :   void printNode(TNode n) override;
     114                 :            :   void printTrust(TNode res, ProofRule src) override;
     115                 :            :   void printOpenRule(const ProofNode* pn) override;
     116                 :            : 
     117                 :            :   /** Get the DSL rewrites */
     118                 :            :   const std::unordered_set<ProofRewriteRule>& getDslRewrites() const;
     119                 :            : 
     120                 :            :  private:
     121                 :            :   /** The let binding */
     122                 :            :   LetBinding& d_lbind;
     123                 :            :   /** The DSL rules we have seen */
     124                 :            :   std::unordered_set<ProofRewriteRule> d_dprs;
     125                 :            : };
     126                 :            : 
     127                 :            : }  // namespace proof
     128                 :            : }  // namespace cvc5::internal
     129                 :            : 
     130                 :            : #endif