GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_trie.h Lines: 6 6 100.0 %
Date: 2021-03-23 Branches: 3 6 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_trie.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief A trie class for Nodes and TNodes.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__NODE_TRIE_H
18
#define CVC4__EXPR__NODE_TRIE_H
19
20
#include <map>
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
namespace theory {
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[d] :
53
 *       t.d_data[b].d_data[d].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
7332876
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
415227
  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
1384993
  void clear() { d_data.clear(); }
93
  /** Is this trie empty? */
94
1133392
  bool empty() const { return d_data.empty(); }
95
}; /* class NodeTemplateTrie */
96
97
template <bool ref_count>
98
1360067
bool NodeTemplateTrie<ref_count>::addTerm(
99
    NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
100
{
101
1360067
  return addOrGetTerm(n, reps) == n;
102
}
103
104
/** Reference-counted version of the above data structure */
105
typedef NodeTemplateTrie<true> NodeTrie;
106
/** Non-reference-counted version of the above data structure */
107
typedef NodeTemplateTrie<false> TNodeTrie;
108
109
}  // namespace theory
110
}  // namespace CVC4
111
112
#endif /* CVC4__EXPR__NODE_TRIE_H */