GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/lazy_trie.h Lines: 6 6 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file lazy_trie.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, 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 lazy trie
13
 **/
14
15
#ifndef CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
16
#define CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
17
18
#include "expr/node.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace quantifiers {
23
24
/** abstract evaluator class
25
 *
26
 * This class is used for the LazyTrie data structure below.
27
 */
28
6994
class LazyTrieEvaluator
29
{
30
 public:
31
6988
  virtual ~LazyTrieEvaluator() {}
32
  virtual Node evaluate(Node n, unsigned index) = 0;
33
};
34
35
/** LazyTrie
36
 *
37
 * This is a trie where terms are added in a lazy fashion. This data structure
38
 * is useful, for instance, when we are only interested in when two terms
39
 * map to the same node in the trie but we need not care about computing
40
 * exactly where they are.
41
 *
42
 * In other words, when a term n is added to this trie, we do not insist
43
 * that n is placed at the maximal depth of the trie. Instead, we place n at a
44
 * minimal depth node that has no children. In this case we say n is partially
45
 * evaluated in this trie.
46
 *
47
 * This class relies on an abstract evaluator interface above, which evaluates
48
 * nodes for indices.
49
 *
50
 * For example, say we have terms a, b, c and an evaluator ev where:
51
 *   ev->evaluate( a, 0,1,2 ) = 0, 5, 6
52
 *   ev->evaluate( b, 0,1,2 ) = 1, 3, 0
53
 *   ev->evaluate( c, 0,1,2 ) = 1, 3, 2
54
 * After adding a to the trie, we get:
55
 *   root: a
56
 * After adding b to the resulting trie, we get:
57
 *   root: null
58
 *     d_children[0]: a
59
 *     d_children[1]: b
60
 * After adding c to the resulting trie, we get:
61
 *   root: null
62
 *     d_children[0]: a
63
 *     d_children[1]: null
64
 *       d_children[3]: null
65
 *         d_children[0] : b
66
 *         d_children[2] : c
67
 * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
68
 */
69
class LazyTrie
70
{
71
 public:
72
28855
  LazyTrie() {}
73
28855
  ~LazyTrie() {}
74
  /** the data at this node, which may be partially evaluated */
75
  Node d_lazy_child;
76
  /** the children of this node */
77
  std::map<Node, LazyTrie> d_children;
78
  /** clear the trie */
79
1334
  void clear() { d_children.clear(); }
80
  /** add n to the trie
81
   *
82
   * This function returns a node that is mapped to the same node in the trie
83
   * if one exists, or n otherwise.
84
   *
85
   * ev is an evaluator which determines where n is placed in the trie
86
   * index is the depth of this node
87
   * ntotal is the maximal depth of the trie
88
   * forceKeep is whether we wish to force that n is chosen as a representative
89
   */
90
  Node add(Node n,
91
           LazyTrieEvaluator* ev,
92
           unsigned index,
93
           unsigned ntotal,
94
           bool forceKeep);
95
};
96
97
using IndTriePair = std::pair<unsigned, LazyTrie*>;
98
99
/** Lazy trie with multiple elements per leaf
100
 *
101
 * As the above trie, but allows multiple elements per leaf. This is done by
102
 * keeping classes of elements associated with each element kept in a leaf,
103
 * which is denoted the representative of the class associated with that leaf.
104
 *
105
 * Another feature of this data structure is to allow the insertion of new
106
 * classifiers besides that of data.
107
 */
108
34
class LazyTrieMulti
109
{
110
 public:
111
  /** maps representatives to their classes
112
   *
113
   * the equivalence relation is defined in terms of the tuple of evaluations
114
   * under the current classifiers. For example if we currently have three
115
   * classifiers and four elements -- a,b,c,d -- have been inserted into the
116
   * trie such that their evaluation on the classifiers are:
117
   *
118
   * a -> (0, 0, 0)
119
   * b -> (1, 3, 0)
120
   * c -> (1, 3, 0)
121
   * d -> (1, 3, 0)
122
   *
123
   * then a is the representative of the class {a}, while b of the class {b,c,d}
124
    */
125
  std::map<Node, std::vector<Node>> d_rep_to_class;
126
  /** adds a new classifier to the trie
127
   *
128
   * When a new classifier is added a new level is added to each leaf that has
129
   * data and the class associated with the element is the leaf is separated
130
   * according to the new classifier.
131
   *
132
   * For example in the following trie with three classifiers:
133
   *
134
   *   root: null
135
   *     d_children[0]: a -> {a}
136
   *     d_children[1]: null
137
   *       d_children[3]: null
138
   *         d_children[0] : b -> {b, c, d}
139
   *
140
   * to which we add a fourth classifier C such that C(b) = 0, C(c) = 1, C(d) =
141
   * 1 we have the resulting trie:
142
   *
143
   *   root: null
144
   *     d_children[0]: a -> {a}
145
   *     d_children[1]: null
146
   *       d_children[3]: null
147
   *         d_children[0] : null
148
   *           d_children[0] : b -> {b}
149
   *           d_children[1] : c -> {c, d}
150
   *
151
   * ntotal is the number of classifiers before the addition of the new one. In
152
   * the above example it would be 3.
153
   */
154
  void addClassifier(LazyTrieEvaluator* ev, unsigned ntotal);
155
  /** adds an element to the trie
156
   *
157
   * If f ends it in a leaf that already contains an element, it is added to the
158
   * class of that element. Otherwise it becomes the representative of the class
159
   * containing only itself.
160
   */
161
  Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
162
  /** clear the trie */
163
  void clear();
164
165
  /** A regular lazy trie */
166
  LazyTrie d_trie;
167
};
168
169
} /* CVC4::theory::quantifiers namespace */
170
} /* CVC4::theory namespace */
171
} /* CVC4 namespace */
172
173
#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */