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                 :            :  * Normalizes the input benchmark regardless of the symbol names and assertion
      11                 :            :  * order.
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "cvc5_private.h"
      15                 :            : 
      16                 :            : #ifndef CVC5__PREPROCESSING__PASSES__NORMALIZE_H
      17                 :            : #define CVC5__PREPROCESSING__PASSES__NORMALIZE_H
      18                 :            : 
      19                 :            : #include <unordered_map>
      20                 :            : 
      21                 :            : #include "preprocessing/preprocessing_pass.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : namespace preprocessing {
      25                 :            : namespace passes {
      26                 :            : 
      27                 :            : /**
      28                 :            :  * Struct for storing information about a node, used for normalization.
      29                 :            :  */
      30                 :            : struct NodeInfo
      31                 :            : {
      32                 :            :   /** The node itself. */
      33                 :            :   Node node;
      34                 :            :   /** Compressed string encoding of the DAG, aka patterns. */
      35                 :            :   std::string encoding;
      36                 :            :   /** Equivalence class ID. */
      37                 :            :   size_t equivClass;
      38                 :            :   /** First occurrence index (counter) of each symbol when traversing the DAG,
      39                 :            :    * aka super-pattern */
      40                 :            :   std::unordered_map<std::string, int32_t> role;
      41                 :            :   /** Variable names and their indices. */
      42                 :            :   std::vector<std::pair<std::string, int32_t>> varNames;
      43                 :            :   /** Index of the assertion after first round of sorting. */
      44                 :            :   size_t id;
      45                 :            : 
      46                 :            :   /** Default constructor. */
      47                 :            :   NodeInfo() {}
      48                 :            : 
      49                 :            :   /**
      50                 :            :    * Constructor with parameters.
      51                 :            :    * @param n The node.
      52                 :            :    * @param enc Compressed encoding string.
      53                 :            :    * @param eqClass Equivalence class ID.
      54                 :            :    * @param r Role map.
      55                 :            :    * @param vn Variable names and indices.
      56                 :            :    */
      57                 :          4 :   NodeInfo(const Node& n,
      58                 :            :            const std::string& enc,
      59                 :            :            uint32_t eqClass,
      60                 :            :            const std::unordered_map<std::string, int32_t>& r,
      61                 :            :            const std::vector<std::pair<std::string, int32_t>>& vn)
      62                 :          4 :       : node(n), encoding(enc), equivClass(eqClass), role(r), varNames(vn)
      63                 :            :   {
      64                 :          4 :   }
      65                 :            : 
      66                 :            :   /**
      67                 :            :    * Print node information to stdout.
      68                 :            :    */
      69                 :            :   void print() const
      70                 :            :   {
      71                 :            :     std::cout << "Node : " << node << std::endl;
      72                 :            :     std::cout << "Encoding: " << encoding << std::endl;
      73                 :            :     std::cout << "Roles: ";
      74                 :            :     for (const auto& [symbol, idx] : role)
      75                 :            :     {
      76                 :            :       std::cout << symbol << " : " << idx << " , ";
      77                 :            :     }
      78                 :            :     std::cout << std::endl;
      79                 :            :     std::cout << "Symbols: ";
      80                 :            :     for (const auto& [symbol, idx] : varNames)
      81                 :            :     {
      82                 :            :       std::cout << symbol << " : " << idx << " , ";
      83                 :            :     }
      84                 :            :     std::cout << std::endl;
      85                 :            :   }
      86                 :            : 
      87                 :            :   /**
      88                 :            :    * Set the ID of the node.
      89                 :            :    * @param i The ID to set.
      90                 :            :    */
      91                 :          4 :   void setId(uint32_t i) { id = i; }
      92                 :            : };
      93                 :            : 
      94                 :            : /**
      95                 :            :  * Preprocessing pass for normalizing assertions.
      96                 :            :  */
      97                 :            : class Normalize : public PreprocessingPass
      98                 :            : {
      99                 :            :  public:
     100                 :            :   /**
     101                 :            :    * Construct a Normalize preprocessing pass.
     102                 :            :    * @param preprocContext The preprocessing pass context.
     103                 :            :    */
     104                 :            :   Normalize(PreprocessingPassContext* preprocContext);
     105                 :            : 
     106                 :            :  protected:
     107                 :            :   /**
     108                 :            :    * Apply normalization to the assertions to preprocess.
     109                 :            :    * @param assertionsToPreprocess The assertions pipeline.
     110                 :            :    * @return The result of preprocessing.
     111                 :            :    */
     112                 :            :   PreprocessingPassResult applyInternal(
     113                 :            :       AssertionPipeline* assertionsToPreprocess) override;
     114                 :            : 
     115                 :            :  private:
     116                 :            :   /**
     117                 :            :    * Struct for tracking statistics of the normalization pass.
     118                 :            :    */
     119                 :            :   struct Statistics
     120                 :            :   {
     121                 :            :     /** Timer for the normalization pass. */
     122                 :            :     TimerStat d_passTime;
     123                 :            :     /** Construct statistics and register them. */
     124                 :            :     Statistics(StatisticsRegistry& reg);
     125                 :            :   };
     126                 :            : 
     127                 :            :   /**
     128                 :            :    * Get information about a node.
     129                 :            :    * @param node The node to analyze.
     130                 :            :    * @return Unique pointer to NodeInfo.
     131                 :            :    */
     132                 :            :   std::unique_ptr<NodeInfo> getNodeInfo(const Node& node);
     133                 :            : 
     134                 :            :   /** Statistics for the normalization pass. */
     135                 :            :   Statistics d_statistics;
     136                 :            : };
     137                 :            : 
     138                 :            : }  // namespace passes
     139                 :            : }  // namespace preprocessing
     140                 :            : }  // namespace cvc5::internal
     141                 :            : 
     142                 :            : #endif /* CVC5__PREPROCESSING__PASSES__NORMALIZE_H */