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-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                 :            :  * Utilities for constructing canonical terms.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__EXPR__TERM_CANONIZE_H
      19                 :            : #define CVC5__EXPR__TERM_CANONIZE_H
      20                 :            : 
      21                 :            : #include <map>
      22                 :            : #include "expr/node.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace expr {
      26                 :            : 
      27                 :            : /**
      28                 :            :  * Generalization of types. This class is a simple callback for giving
      29                 :            :  * identifiers to variables that may be a more fine-grained way of classifying
      30                 :            :  * the variable than its type. An example usage of type classes are for
      31                 :            :  * distinguishing "list variables" for rewrite rule reconstruction.
      32                 :            :  */
      33                 :            : class TypeClassCallback
      34                 :            : {
      35                 :            :  public:
      36                 :       3228 :   TypeClassCallback() {}
      37                 :       3227 :   virtual ~TypeClassCallback() {}
      38                 :            :   /** Return the type class for variable v */
      39                 :            :   virtual uint32_t getTypeClass(TNode v) = 0;
      40                 :            : };
      41                 :            : 
      42                 :            : /** TermCanonize
      43                 :            :  *
      44                 :            :  * This class contains utilities for canonizing terms with respect to
      45                 :            :  * free variables (which are of kind BOUND_VARIABLE). For example, this
      46                 :            :  * class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2)
      47                 :            :  * are effectively the same term.
      48                 :            :  */
      49                 :            : class TermCanonize
      50                 :            : {
      51                 :            :  public:
      52                 :            :   /**
      53                 :            :    * @param tcc The type class callback. This class will canonize variables in
      54                 :            :    * a way that disinguishes variables that are given different type class
      55                 :            :    * identifiers. Otherwise, this class will assume all variables of the
      56                 :            :    * same type have the same type class.
      57                 :            :    */
      58                 :            :   TermCanonize(TypeClassCallback* tcc = nullptr);
      59                 :     121964 :   ~TermCanonize() {}
      60                 :            : 
      61                 :            :   /** Maps operators to an identifier, useful for ordering. */
      62                 :            :   int getIdForOperator(Node op);
      63                 :            :   /** Maps types to an identifier, useful for ordering. */
      64                 :            :   int getIdForType(TypeNode t);
      65                 :            :   /** get term order
      66                 :            :    *
      67                 :            :    * Returns true if a <= b in the term ordering used by this class. The
      68                 :            :    * term order is determined by the leftmost position in a and b whose
      69                 :            :    * operators o_a and o_b are distinct at that position. Then a <= b iff
      70                 :            :    * getIdForOperator( o_a ) <= getIdForOperator( o_b ).
      71                 :            :    */
      72                 :            :   bool getTermOrder(Node a, Node b);
      73                 :            :   /** get canonical free variable #i of type tn */
      74                 :            :   Node getCanonicalFreeVar(TypeNode tn, size_t i, uint32_t tc = 0);
      75                 :            :   /**
      76                 :            :    * Return the range of the free variable in the above map, or 0 if it does not
      77                 :            :    * exist.
      78                 :            :    */
      79                 :            :   size_t getIndexForFreeVariable(Node v) const;
      80                 :            :   /** get canonical term
      81                 :            :    *
      82                 :            :    * This returns a canonical (alpha-equivalent) version of n, where
      83                 :            :    * bound variables in n may be replaced by other ones, and arguments of
      84                 :            :    * commutative operators of n may be sorted (if apply_torder is true). If
      85                 :            :    * doHoVar is true, we also canonicalize bound variables that occur in
      86                 :            :    * operators.
      87                 :            :    *
      88                 :            :    * In detail, we replace bound variables in n so the the leftmost occurrence
      89                 :            :    * of a bound variable for type T is the first canonical free variable for T,
      90                 :            :    * the second leftmost is the second, and so on, for each type T.
      91                 :            :    */
      92                 :            :   Node getCanonicalTerm(TNode n,
      93                 :            :                         bool apply_torder = false,
      94                 :            :                         bool doHoVar = true);
      95                 :            :   /**
      96                 :            :    * Same as above but tracks visited map, mapping subterms of n to their
      97                 :            :    * canonical forms.
      98                 :            :    */
      99                 :            :   Node getCanonicalTerm(TNode n,
     100                 :            :                         std::map<TNode, Node>& visited,
     101                 :            :                         bool apply_torder = false,
     102                 :            :                         bool doHoVar = true);
     103                 :            : 
     104                 :            :  private:
     105                 :            :   /** The (optional) type class callback */
     106                 :            :   TypeClassCallback* d_tcc;
     107                 :            :   /** the number of ids we have allocated for operators */
     108                 :            :   int d_op_id_count;
     109                 :            :   /** map from operators to id */
     110                 :            :   std::map<Node, int> d_op_id;
     111                 :            :   /** the number of ids we have allocated for types */
     112                 :            :   int d_typ_id_count;
     113                 :            :   /** map from type to id */
     114                 :            :   std::map<TypeNode, int> d_typ_id;
     115                 :            :   /** free variables for each type / type class pair */
     116                 :            :   std::map<std::pair<TypeNode, uint32_t>, std::vector<Node> > d_cn_free_var;
     117                 :            :   /**
     118                 :            :    * Map from each free variable above to their index in their respective vector
     119                 :            :    */
     120                 :            :   std::map<Node, size_t> d_fvIndex;
     121                 :            :   /** Get type class */
     122                 :            :   uint32_t getTypeClass(TNode v);
     123                 :            :   /** get canonical term
     124                 :            :    *
     125                 :            :    * This is a helper function for getCanonicalTerm above. We maintain a
     126                 :            :    * counter of how many variables we have allocated for each type (var_count),
     127                 :            :    * and a cache of visited nodes (visited).
     128                 :            :    */
     129                 :            :   Node getCanonicalTerm(
     130                 :            :       TNode n,
     131                 :            :       bool apply_torder,
     132                 :            :       bool doHoVar,
     133                 :            :       std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
     134                 :            :       std::map<TNode, Node>& visited);
     135                 :            : };
     136                 :            : 
     137                 :            : }  // namespace expr
     138                 :            : }  // namespace cvc5::internal
     139                 :            : 
     140                 :            : #endif /* CVC5__EXPR__TERM_CANONIZE_H */