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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 */ 