Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
       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                 :            :  * A trie class for Nodes and TNodes.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__EXPR__NODE_TRIE_H
      19                 :            : #define CVC5__EXPR__NODE_TRIE_H
      20                 :            : 
      21                 :            : #include <map>
      22                 :            : #include "expr/node.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : 
      26                 :            : /** NodeTemplate trie class
      27                 :            :  *
      28                 :            :  * This is a trie data structure whose distinguishing feature is that it has
      29                 :            :  * no "data" members and only references to children. The motivation for having
      30                 :            :  * no data members is efficiency.
      31                 :            :  *
      32                 :            :  * One use of this class is to represent "term indices" or a "signature tables"
      33                 :            :  * for symbols with fixed arities. In this use case, we "index" terms by the
      34                 :            :  * list of representatives of their arguments.
      35                 :            :  *
      36                 :            :  * For example, consider the equivalence classes :
      37                 :            :  *
      38                 :            :  * { a, d, f( d, c ), f( a, c ) }
      39                 :            :  * { b, f( b, d ) }
      40                 :            :  * { c, f( b, b ) }
      41                 :            :  *
      42                 :            :  * where the first elements ( a, b, c ) are the representatives of these
      43                 :            :  * classes. The NodeTemplateTrie t we may build for f is :
      44                 :            :  *
      45                 :            :  * t :
      46                 :            :  *   t.d_data[a] :
      47                 :            :  *     t.d_data[a].d_data[c] :
      48                 :            :  *       t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf)
      49                 :            :  *   t.d_data[b] :
      50                 :            :  *     t.d_data[b].d_data[b] :
      51                 :            :  *       t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf)
      52                 :            :  *     t.d_data[b].d_data[a] :
      53                 :            :  *       t.d_data[b].d_data[a].d_data[f(b,d)] : (leaf)
      54                 :            :  *
      55                 :            :  * Leaf nodes store the terms that are indexed by the arguments, for example
      56                 :            :  * term f(d,c) is indexed by the representative arguments (a,c), and is stored
      57                 :            :  * as a the (single) key in the data of t.d_data[a].d_data[c].
      58                 :            :  */
      59                 :            : template <bool ref_count>
      60                 :            : class NodeTemplateTrie
      61                 :            : {
      62                 :            :  public:
      63                 :            :   /** The children of this node. */
      64                 :            :   std::map<NodeTemplate<ref_count>, NodeTemplateTrie<ref_count>> d_data;
      65                 :            :   /** For leaf nodes : does this node have data? */
      66                 :            :   bool hasData() const { return !d_data.empty(); }
      67                 :            :   /** For leaf nodes : get the node corresponding to this leaf. */
      68                 :    1948256 :   NodeTemplate<ref_count> getData() const { return d_data.begin()->first; }
      69                 :            :   /**
      70                 :            :    * Returns the term that is indexed by reps, if one exists, or
      71                 :            :    * or returns null otherwise.
      72                 :            :    */
      73                 :            :   NodeTemplate<ref_count> existsTerm(
      74                 :            :       const std::vector<NodeTemplate<ref_count>>& reps) const;
      75                 :            :   /**
      76                 :            :    * Returns the term that is previously indexed by reps, if one exists, or
      77                 :            :    * adds n to the trie, indexed by reps, and returns n.
      78                 :            :    */
      79                 :            :   NodeTemplate<ref_count> addOrGetTerm(
      80                 :            :       NodeTemplate<ref_count> n,
      81                 :            :       const std::vector<NodeTemplate<ref_count>>& reps);
      82                 :            :   /**
      83                 :            :    * Returns false if a term is previously indexed by reps.
      84                 :            :    * Returns true if no term is previously indexed by reps,
      85                 :            :    *   and adds n to the trie, indexed by reps.
      86                 :            :    */
      87                 :            :   inline bool addTerm(NodeTemplate<ref_count> n,
      88                 :            :                       const std::vector<NodeTemplate<ref_count>>& reps);
      89                 :            :   /** Debug print this trie on Trace c with indentation depth. */
      90                 :            :   void debugPrint(const char* c, unsigned depth = 0) const;
      91                 :            :   /** Clear all data from this trie. */
      92                 :    2913265 :   void clear() { d_data.clear(); }
      93                 :            :   /** Is this trie empty? */
      94                 :    2529670 :   bool empty() const { return d_data.empty(); }
      95                 :            :   /**
      96                 :            :    * Get leaves at the given depth, where depth>0. This argument is necessary
      97                 :            :    * since we do not know apriori the depth of where data occurs.
      98                 :            :    *
      99                 :            :    * If this trie stores applications of a function f, then depth should be set
     100                 :            :    * to the arity of f.
     101                 :            :    *
     102                 :            :    * Notice this method will never throw an assertion error, even if the
     103                 :            :    * depth is not set to the proper value. In particular, it will return
     104                 :            :    * the empty vector if the provided depth is larger than the actual depth,
     105                 :            :    * and will return internal nodes if the provided depth is less than the
     106                 :            :    * actual depth of the trie.
     107                 :            :    */
     108                 :            :   std::vector<Node> getLeaves(size_t depth) const;
     109                 :            : }; /* class NodeTemplateTrie */
     110                 :            : 
     111                 :            : template <bool ref_count>
     112                 :    2211809 : bool NodeTemplateTrie<ref_count>::addTerm(
     113                 :            :     NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
     114                 :            : {
     115                 :    2211809 :   return addOrGetTerm(n, reps) == n;
     116                 :            : }
     117                 :            : 
     118                 :            : /** Reference-counted version of the above data structure */
     119                 :            : typedef NodeTemplateTrie<true> NodeTrie;
     120                 :            : /** Non-reference-counted version of the above data structure */
     121                 :            : typedef NodeTemplateTrie<false> TNodeTrie;
     122                 :            : 
     123                 :            : }  // namespace cvc5::internal
     124                 :            : 
     125                 :            : #endif /* CVC5__EXPR__NODE_TRIE_H */