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 printer for the Eunoia format.
      11                 :            :  */
      12                 :            : #include <cstddef>
      13                 :            : #include <memory>
      14                 :            : 
      15                 :            : #include "cvc5_private.h"
      16                 :            : 
      17                 :            : #ifndef CVC5__PROOF__EO_PROOF_PRINTER_H
      18                 :            : #define CVC5__PROOF__EO_PROOF_PRINTER_H
      19                 :            : 
      20                 :            : #include <iostream>
      21                 :            : 
      22                 :            : #include "context/cdhashmap.h"
      23                 :            : #include "context/cdhashset.h"
      24                 :            : #include "expr/node_algorithm.h"
      25                 :            : #include "proof/eo/eo_list_node_converter.h"
      26                 :            : #include "proof/eo/eo_node_converter.h"
      27                 :            : #include "proof/eo/eo_print_channel.h"
      28                 :            : #include "proof/proof_checker.h"
      29                 :            : #include "proof/proof_node.h"
      30                 :            : #include "rewriter/rewrite_proof_rule.h"
      31                 :            : #include "smt/env_obj.h"
      32                 :            : #include "smt/proof_manager.h"
      33                 :            : 
      34                 :            : namespace cvc5::internal {
      35                 :            : 
      36                 :            : namespace proof {
      37                 :            : 
      38                 :            : class EoPrinter : protected EnvObj
      39                 :            : {
      40                 :            :  public:
      41                 :            :   EoPrinter(Env& env,
      42                 :            :             BaseEoNodeConverter& atp,
      43                 :            :             rewriter::RewriteDb* rdb,
      44                 :            :             uint32_t letThresh = 2);
      45                 :       1979 :   ~EoPrinter() {}
      46                 :            : 
      47                 :            :   /**
      48                 :            :    * Print the full proof pfn.
      49                 :            :    * @param out The output stream.
      50                 :            :    * @param pfn The proof node.
      51                 :            :    * @param psm The scope mode, which determines whether there are outermost
      52                 :            :    * scope to process in pfn. If this is the case, we print assume steps.
      53                 :            :    */
      54                 :            :   void print(std::ostream& out,
      55                 :            :              std::shared_ptr<ProofNode> pfn,
      56                 :            :              ProofScopeMode psm = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS);
      57                 :            :   /**
      58                 :            :    * Same as above, but with a Eunoia print channel.
      59                 :            :    * @param out The output stream.
      60                 :            :    * @param pfn The proof node.
      61                 :            :    * @param psm The scope mode.
      62                 :            :    */
      63                 :            :   void print(EoPrintChannelOut& out,
      64                 :            :              std::shared_ptr<ProofNode> pfn,
      65                 :            :              ProofScopeMode psm = ProofScopeMode::DEFINITIONS_AND_ASSERTIONS);
      66                 :            :   /**
      67                 :            :    * Print the proof, assuming that previous proofs have been printed on this
      68                 :            :    * printer that have (partially) given the definition of subterms and
      69                 :            :    * subproofs in pfn.
      70                 :            :    * @param out The output stream.
      71                 :            :    * @param pfn The proof node.
      72                 :            :    */
      73                 :            :   void printNext(EoPrintChannelOut& out, std::shared_ptr<ProofNode> pfn);
      74                 :            : 
      75                 :            :   /**
      76                 :            :    * Print proof rewrite rule name r to output stream out
      77                 :            :    * @param out The output stream.
      78                 :            :    * @param r The proof rewrite rule. This should be one of the proof rewrite
      79                 :            :    * rules that corresponds to a RARE rewrite.
      80                 :            :    */
      81                 :            :   void printDslRule(std::ostream& out, ProofRewriteRule r);
      82                 :            :   /**
      83                 :            :    * Get the let binding that is computed by calls to printing terms in this
      84                 :            :    * class.
      85                 :            :    */
      86                 :            :   LetBinding* getLetBinding();
      87                 :            : 
      88                 :            :   /** Return true if it is possible to trust the topmost application in pfn */
      89                 :            :   static bool isHandled(const Options& opts, const ProofNode* pfn);
      90                 :            : 
      91                 :            :  private:
      92                 :            :   /** Return true if id is handled as a theory rewrite for term n */
      93                 :            :   static bool isHandledTheoryRewrite(const Options& opts,
      94                 :            :                                      ProofRewriteRule id,
      95                 :            :                                      const Node& n);
      96                 :            :   /** Return if the equality is handled as a bitblast step */
      97                 :            :   static bool isHandledBitblastStep(const Node& eq);
      98                 :            :   /**
      99                 :            :    * Return true if it is possible to evaluate n using the evaluation side
     100                 :            :    * condition in the CPC signature. Notice this requires that all subterms of n
     101                 :            :    * are handled. This method is used for determining if an application of
     102                 :            :    * ProofRule::EVALUATE can be applied.
     103                 :            :    */
     104                 :            :   static bool canEvaluate(Node n);
     105                 :            :   /**
     106                 :            :    * Return true if it is possible to evaluate n using the distinct values side
     107                 :            :    * condition in the CPC signature. Notice this requires that all subterms of n
     108                 :            :    * are handled. This method is used for determining if an application of
     109                 :            :    * ProofRule::DISTINCT_VALUES can be applied.
     110                 :            :    */
     111                 :            :   static bool isHandledDistinctValues(const Node& n);
     112                 :            :   /**
     113                 :            :    * Whether we support evaluating (str.in_re s r) for any constant string s.
     114                 :            :    */
     115                 :            :   static bool canEvaluateRegExp(Node r);
     116                 :            :   /* Returns the normalized name of the proof rule of pfn */
     117                 :            :   std::string getRuleName(const ProofNode* pfn) const;
     118                 :            : 
     119                 :            :   //-------------
     120                 :            :   /**
     121                 :            :    * Select only those children required by the proof rule.
     122                 :            :    */
     123                 :            :   void getChildrenFromProofRule(
     124                 :            :       const ProofNode* pn, std::vector<std::shared_ptr<ProofNode>>& children);
     125                 :            :   /**
     126                 :            :    * Add the arguments of proof node pn to args in the order in which they
     127                 :            :    * should be printed. This also ensures the nodes have been converted via the
     128                 :            :    * Eunoia node converter.
     129                 :            :    */
     130                 :            :   void getArgsFromProofRule(const ProofNode* pn, std::vector<Node>& args);
     131                 :            :   /**
     132                 :            :    * Helper for print. Prints the proof node using the print channel out. This
     133                 :            :    * may either write the proof to an output stream or preprocess it.
     134                 :            :    *
     135                 :            :    * @param out The output channel to print to.
     136                 :            :    * @param pn The proof node to print.
     137                 :            :    * @param addToCache If true, we add (subproofs) of pn to the cache and do
     138                 :            :    * not print them with this method if they are encounted again.
     139                 :            :    */
     140                 :            :   void printProofInternal(EoPrintChannel* out,
     141                 :            :                           const ProofNode* pn,
     142                 :            :                           bool addToCache);
     143                 :            :   /**
     144                 :            :    * Called at preorder traversal of proof node pn. Prints (if necessary) to
     145                 :            :    * out.
     146                 :            :    */
     147                 :            :   void printStepPre(EoPrintChannel* out, const ProofNode* pn);
     148                 :            :   /**
     149                 :            :    * Called at postorder traversal of proof node pn. Prints (if necessary) to
     150                 :            :    * out.
     151                 :            :    */
     152                 :            :   void printStepPost(EoPrintChannel* out, const ProofNode* pn);
     153                 :            :   /**
     154                 :            :    * Allocate (if necessary) the identifier for an assume-push step for pn and
     155                 :            :    * return the identifier. pn should be an application of ProofRule::SCOPE.
     156                 :            :    */
     157                 :            :   size_t allocateAssumePushId(const ProofNode* pn, const Node& a);
     158                 :            :   /**
     159                 :            :    * Allocate (if necessary) the identifier for an assume step for the
     160                 :            :    * assumption for formula n and return the identifier. Note this identifier is
     161                 :            :    * unique for each assumed formula, although multiple assumption proofs for n
     162                 :            :    * may exist.
     163                 :            :    */
     164                 :            :   size_t allocateAssumeId(const Node& n, bool& wasAlloc);
     165                 :            :   /**
     166                 :            :    * Allocate (if necessary) the identifier for step
     167                 :            :    */
     168                 :            :   size_t allocateProofId(const ProofNode* pn, bool& wasAlloc);
     169                 :            :   /** Print let list to output stream out */
     170                 :            :   void printLetList(std::ostream& out, LetBinding& lbind);
     171                 :            :   /** Reference to the term processor */
     172                 :            :   BaseEoNodeConverter& d_tproc;
     173                 :            :   /** Assume id counter */
     174                 :            :   size_t d_pfIdCounter;
     175                 :            :   /** Mapping proofs to identifiers */
     176                 :            :   std::map<const ProofNode*, size_t> d_pletMap;
     177                 :            :   /**
     178                 :            :    * Context for d_passumeMap, which is pushed and popped when we encounter
     179                 :            :    * SCOPE proofs.
     180                 :            :    */
     181                 :            :   context::Context d_passumeCtx;
     182                 :            :   /**
     183                 :            :    * The set of proof nodes we have already printed with this class, as
     184                 :            :    * used by printProofInternal.
     185                 :            :    */
     186                 :            :   context::CDHashSet<const ProofNode*> d_alreadyPrinted;
     187                 :            :   /** Mapping assumed formulas to identifiers */
     188                 :            :   context::CDHashMap<Node, size_t> d_passumeMap;
     189                 :            :   /** The (dummy) type used for proof terms */
     190                 :            :   TypeNode d_pfType;
     191                 :            :   /** term prefix */
     192                 :            :   std::string d_termLetPrefix;
     193                 :            :   /** The false node */
     194                 :            :   Node d_false;
     195                 :            :   /** */
     196                 :            :   TypeNode d_absType;
     197                 :            :   /** Pointer to the rewrite database */
     198                 :            :   rewriter::RewriteDb* d_rdb;
     199                 :            :   /** The empty vector */
     200                 :            :   std::vector<Node> d_emptyVec;
     201                 :            :   /** The let binding */
     202                 :            :   LetBinding d_lbind;
     203                 :            :   /** The let binding we are using (possibly null) */
     204                 :            :   LetBinding* d_lbindUse;
     205                 :            :   /** The letification channel. */
     206                 :            :   EoPrintChannelPre d_eletify;
     207                 :            :   /** A cache for explicit type-of variables, for printing DSL_REWRITE steps */
     208                 :            :   std::map<ProofRewriteRule, std::vector<Node>> d_explicitTypeOf;
     209                 :            : };
     210                 :            : 
     211                 :            : }  // namespace proof
     212                 :            : }  // namespace cvc5::internal
     213                 :            : 
     214                 :            : #endif /* CVC5__PROOF__EO_PROOF_PRINTER_H */