Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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 benchmark utility.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__SMT__PRINT_BENCHMARK_H
      19                 :            : #define CVC5__SMT__PRINT_BENCHMARK_H
      20                 :            : 
      21                 :            : #include <iosfwd>
      22                 :            : #include <vector>
      23                 :            : 
      24                 :            : #include "expr/node.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : 
      28                 :            : class Printer;
      29                 :            : class NodeConverter;
      30                 :            : 
      31                 :            : namespace smt {
      32                 :            : 
      33                 :            : /**
      34                 :            :  * A utility for printing a benchmark. This utility requires no bookkeeping
      35                 :            :  * about which commands have been executed. It reconstructs the set of
      36                 :            :  * commands that would have been required for generating a benchmark based on
      37                 :            :  * a list of nodes.
      38                 :            :  */
      39                 :            : class PrintBenchmark
      40                 :            : {
      41                 :            :  public:
      42                 :            :   /**
      43                 :            :    * Constructor.
      44                 :            :    * @param nm     The associated node manager.
      45                 :            :    * @param p      The associated printer.
      46                 :            :    * @param sorted True if declarations should be sorted wrt node id.
      47                 :            :    * @param c      The associated node converter.
      48                 :            :    */
      49                 :       1953 :   PrintBenchmark(NodeManager * nm,
      50                 :            :                  const Printer* p,
      51                 :            :                  bool sorted = true,
      52                 :            :                  NodeConverter* c = nullptr)
      53                 :       1953 :       : d_nm(nm), d_printer(p), d_sorted(sorted), d_converter(c)
      54                 :            :   {
      55                 :       1953 :   }
      56                 :            :   /**
      57                 :            :    * Print the declarations and definitions from a set of definitions and terms.
      58                 :            :    *
      59                 :            :    * @param outDecl The output stream to print the declarations on
      60                 :            :    * @param outDef The output stream to print the definitions on.
      61                 :            :    * @param def The definitions to print.
      62                 :            :    * @param term The terms to print declarations and definitions from.
      63                 :            :    */
      64                 :            :   void printDeclarationsFrom(std::ostream& outDecl,
      65                 :            :                              std::ostream& outDef,
      66                 :            :                              const std::vector<Node>& defs,
      67                 :            :                              const std::vector<Node>& terms);
      68                 :            :   /**
      69                 :            :    * Print assertions. This prints a parsable set of commands on the output
      70                 :            :    * stream out that defines (recursive) functions in defs, and asserts
      71                 :            :    * assertions. It does not print a set-logic or check-sat command.
      72                 :            :    *
      73                 :            :    * Each node in defs is either of the form:
      74                 :            :    * (1) (= s t), where s is a (non-recursively) defined function, where
      75                 :            :    * the term t may be a lambda if s has non-zero arity.
      76                 :            :    * (2) (forall V (= (s V) t)), where s is a recursively defined function.
      77                 :            :    */
      78                 :            :   void printAssertions(std::ostream& out,
      79                 :            :                        const std::vector<Node>& defs,
      80                 :            :                        const std::vector<Node>& assertions);
      81                 :            :   /**
      82                 :            :    * Print assertions, without special handling of defined functions.
      83                 :            :    */
      84                 :            :   void printAssertions(std::ostream& out, const std::vector<Node>& assertions);
      85                 :            : 
      86                 :            :   /**
      87                 :            :    * Print benchmark, which prints a parsable benchmark on the output stream
      88                 :            :    * out. It relies on the printAssertions method above, as well as printing
      89                 :            :    * the logic based on given string and a final check-sat command.
      90                 :            :    *
      91                 :            :    * For the best printing, defs should be given in the order in which
      92                 :            :    * the symbols were declared. If this is not the case, then we may e.g.
      93                 :            :    * group blocks of definitions that were not grouped in the input.
      94                 :            :    */
      95                 :            :   void printBenchmark(std::ostream& out,
      96                 :            :                       const std::string& logic,
      97                 :            :                       const std::vector<Node>& defs,
      98                 :            :                       const std::vector<Node>& assertions);
      99                 :            : 
     100                 :            :   /**
     101                 :            :    * Mark that the given symbol should not be printed in benchmark outputs.
     102                 :            :    */
     103                 :            :   static void markNoPrint(Node& sym);
     104                 :            : 
     105                 :            :  private:
     106                 :            :   /**
     107                 :            :    * print declared symbols in funs but not processed; updates processed to
     108                 :            :    * include what was printed
     109                 :            :    */
     110                 :            :   void printDeclaredFuns(std::ostream& out,
     111                 :            :                          const std::vector<Node>& funs,
     112                 :            :                          std::unordered_set<Node>& processed);
     113                 :            :   /**
     114                 :            :    * Get the connected types. This traverses subfield types of datatypes and
     115                 :            :    * adds to connectedTypes everything that is necessary for printing tn.
     116                 :            :    *
     117                 :            :    * @param tn The type to traverse
     118                 :            :    * @param connectedTypes The types that tn depends on
     119                 :            :    * @param process The types we have already processed. We update this set
     120                 :            :    * with those added to connectedTypes.
     121                 :            :    */
     122                 :            :   void getConnectedSubfieldTypes(TypeNode tn,
     123                 :            :                                  std::vector<TypeNode>& connectedTypes,
     124                 :            :                                  std::unordered_set<TypeNode>& processed);
     125                 :            :   /**
     126                 :            :    * Get connected definitions for symbol v.
     127                 :            :    *
     128                 :            :    * @param recDefs The recursive function definitions that v depends on
     129                 :            :    * @param ordinaryDefs The non-recursive definitions that v depends on
     130                 :            :    * @param syms The declared symbols that v depends on
     131                 :            :    * @param defMap Map from symbols to their definitions
     132                 :            :    * @param processedDefs The (recursive or non-recursive) definitions we have
     133                 :            :    * processed already. We update this with symbols we add to recDefs and
     134                 :            :    * ordinaryDefs.
     135                 :            :    * @param visited The set of terms we have already visited when searching for
     136                 :            :    * free symbols. This set is updated for the bodies of definitions processed
     137                 :            :    * in this call.
     138                 :            :    */
     139                 :            :   void getConnectedDefinitions(
     140                 :            :       Node v,
     141                 :            :       std::vector<Node>& recDefs,
     142                 :            :       std::vector<Node>& ordinaryDefs,
     143                 :            :       std::unordered_set<Node>& syms,
     144                 :            :       const std::unordered_map<Node, std::pair<bool, Node>>& defMap,
     145                 :            :       std::unordered_set<Node>& processedDefs,
     146                 :            :       std::unordered_set<TNode>& visited);
     147                 :            :   /**
     148                 :            :    * Decompose definition assertion a.
     149                 :            :    *
     150                 :            :    * @param a The definition assertion
     151                 :            :    * @param isRecDef Updated to true if a is a recursive function definition (a
     152                 :            :    * quantified formula)
     153                 :            :    * @param sym Updated to the symbol that a defines
     154                 :            :    * @param body Update to the term that defines sym
     155                 :            :    * @return true if the definition was successfully inferred
     156                 :            :    */
     157                 :            :   bool decomposeDefinition(Node a, bool& isRecDef, Node& sym, Node& body);
     158                 :            :   /** Pointer to the node manager */
     159                 :            :   NodeManager * d_nm;
     160                 :            :   /**
     161                 :            :    * Pointer to the printer we are using, which is responsible for printing
     162                 :            :    * individual commands.
     163                 :            :    */
     164                 :            :   const Printer* d_printer;
     165                 :            :   /* True if declarations should be sorted wrt node id. */
     166                 :            :   bool d_sorted;
     167                 :            :   /** (Optional) node converter */
     168                 :            :   NodeConverter* d_converter;
     169                 :            : };
     170                 :            : 
     171                 :            : }  // namespace smt
     172                 :            : }  // namespace cvc5::internal
     173                 :            : 
     174                 :            : #endif /* CVC5__SMT__PRINT_BENCHMARK_H */