src/expr/node_converter.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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  * Node converter utility
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC4__EXPR__NODE_CONVERTER_H
  19 #define CVC4__EXPR__NODE_CONVERTER_H
  20
  21 #include <iostream>
  22 #include <map>
  23
  24 #include "expr/node.h"
  25 #include "expr/type_node.h"
  26
  27 namespace cvc5 {
  28
  29 /**
  30  * A node converter for terms and types. Implements term/type traversals,
  31  * calling the provided implementations of conversion methods (pre/postConvert
  32  * and pre/postConvertType) at pre-traversal and post-traversal.
  33  *
  34  * This class can be used as a generic method for converting terms/types, which
  35  * is orthogonal to methods for traversing nodes.
  36  */
  37 class NodeConverter
  38 {
  39  public:
  40   /**
  41    * @param forceIdem If true, this assumes that terms returned by postConvert
  42    * and postConvertType should not be converted again.
  43    */
  44   NodeConverter(bool forceIdem = true);
  45   virtual ~NodeConverter() {}
  46   /**
  47    * This converts node n based on the preConvert/postConvert methods that can
  48    * be overriden by instances of this class.
  49    *
  50    * If n is null, this always returns the null node.
  51    */
  52   Node convert(Node n);
  53
  54   /**
  55    * This converts type node n based on the preConvertType/postConvertType
  56    * methods that can be overriden by instances of this class.
  57    */
  58   TypeNode convertType(TypeNode tn);
  59
  60  protected:
  61   //------------------------- virtual interface
  62   /** Should we traverse n? */
  63   virtual bool shouldTraverse(Node n);
  64   /**
  65    * Run the conversion for n during pre-order traversal.
  66    * Returning null is equivalent to saying the node should not be changed.
  67    */
  68   virtual Node preConvert(Node n);
  69   /**
  70    * Run the conversion for post-order traversal, where notice n is a term
  71    * of the form:
  72    *   (f i_1 ... i_m)
  73    * where i_1, ..., i_m are terms that have been returned by previous calls
  74    * to postConvert.
  75    *
  76    * Returning null is equivalent to saying the node should not be changed.
  77    */
  78   virtual Node postConvert(Node n);
  79   /**
  80    * Run the conversion, same as `preConvert`, but for type nodes, which notice
  81    * can be built from children similar to Node.
  82    */
  83   virtual TypeNode preConvertType(TypeNode n);
  84   /**
  85    * Run the conversion, same as `postConvert`, but for type nodes, which notice
  86    * can be built from children similar to Node.
  87    */
  88   virtual TypeNode postConvertType(TypeNode n);
  89   //------------------------- end virtual interface
  90  private:
  91   /** Add to cache */
  92   void addToCache(TNode cur, TNode ret);
  93   /** Add to type cache */
  94   void addToTypeCache(TypeNode cur, TypeNode ret);
  95   /** Node cache for preConvert */
  96   std::unordered_map<Node, Node> d_preCache;
  97   /** Node cache for postConvert */
  98   std::unordered_map<Node, Node> d_cache;
  99   /** TypeNode cache for preConvert */
 100   std::unordered_map<TypeNode, TypeNode> d_preTCache;
 101   /** TypeNode cache for postConvert */
 102   std::unordered_map<TypeNode, TypeNode> d_tcache;
 103   /** Whether this node converter is idempotent. */
 104   bool d_forceIdem;
 105 };
 106
 107 }  // namespace cvc5
 108
 109 #endif