Fixes for free variables in assertions (#1762)
[cvc5.git] / src / theory / term_registration_visitor.cpp
1 /********************* */
2 /*! \file term_registration_visitor.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 ** [[ Add lengthier description here ]]
13 ** \todo document this file
14 **/
15
16 #include "theory/term_registration_visitor.h"
17
18 #include "options/quantifiers_options.h"
19 #include "theory/theory_engine.h"
20
21 using namespace std;
22 using namespace CVC4;
23 using namespace theory;
24
25 std::string PreRegisterVisitor::toString() const {
26 std::stringstream ss;
27 TNodeToTheorySetMap::const_iterator it = d_visited.begin();
28 for (; it != d_visited.end(); ++ it) {
29 ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
30 }
31 return ss.str();
32 }
33
34 bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
35
36 Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
37
38 if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS
39 || parent.getKind() == kind::LAMBDA
40 || parent.getKind() == kind::CHOICE
41 || parent.getKind() == kind::REWRITE_RULE
42 || parent.getKind() == kind::SEP_STAR
43 || parent.getKind() == kind::SEP_WAND
44 || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
45 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
46 )
47 && current != parent)
48 {
49 Debug("register::internal") << "quantifier:true" << std::endl;
50 return true;
51 }
52
53 TheoryId currentTheoryId = Theory::theoryOf(current);
54 TheoryId parentTheoryId = Theory::theoryOf(parent);
55
56 d_theories = Theory::setInsert(currentTheoryId, d_theories);
57 d_theories = Theory::setInsert(parentTheoryId, d_theories);
58
59 // Should we use the theory of the type
60 bool useType = false;
61 TheoryId typeTheoryId = THEORY_LAST;
62
63 if (current != parent) {
64 if (currentTheoryId != parentTheoryId) {
65 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
66 TypeNode type = current.getType();
67 useType = true;
68 typeTheoryId = Theory::theoryOf(type);
69 } else {
70 TypeNode type = current.getType();
71 typeTheoryId = Theory::theoryOf(type);
72 if (typeTheoryId != currentTheoryId) {
73 if (type.isInterpretedFinite()) {
74 useType = true;
75 }
76 }
77 }
78 }
79
80 // Get the theories that have already visited this node
81 TNodeToTheorySetMap::iterator find = d_visited.find(current);
82 if (find == d_visited.end()) {
83 if (useType) {
84 d_theories = Theory::setInsert(typeTheoryId, d_theories);
85 }
86 return false;
87 }
88
89 Theory::Set visitedTheories = (*find).second;
90 if (Theory::setContains(currentTheoryId, visitedTheories)) {
91 // The current theory has already visited it, so now it depends on the parent and the type
92 if (Theory::setContains(parentTheoryId, visitedTheories)) {
93 if (useType) {
94 TheoryId typeTheoryId = Theory::theoryOf(current.getType());
95 d_theories = Theory::setInsert(typeTheoryId, d_theories);
96 return Theory::setContains(typeTheoryId, visitedTheories);
97 } else {
98 return true;
99 }
100 } else {
101 return false;
102 }
103 } else {
104 return false;
105 }
106 }
107
108 void PreRegisterVisitor::visit(TNode current, TNode parent) {
109
110 Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
111 if (Debug.isOn("register::internal")) {
112 Debug("register::internal") << toString() << std::endl;
113 }
114
115 // Get the theories of the terms
116 TheoryId currentTheoryId = Theory::theoryOf(current);
117 TheoryId parentTheoryId = Theory::theoryOf(parent);
118
119 // Should we use the theory of the type
120 bool useType = false;
121 TheoryId typeTheoryId = THEORY_LAST;
122
123 if (current != parent) {
124 if (currentTheoryId != parentTheoryId) {
125 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
126 TypeNode type = current.getType();
127 useType = true;
128 typeTheoryId = Theory::theoryOf(type);
129 } else {
130 TypeNode type = current.getType();
131 typeTheoryId = Theory::theoryOf(type);
132 if (typeTheoryId != currentTheoryId) {
133 if (type.isInterpretedFinite()) {
134 useType = true;
135 }
136 }
137 }
138 }
139
140 Theory::Set visitedTheories = d_visited[current];
141 Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
142 if (!Theory::setContains(currentTheoryId, visitedTheories)) {
143 visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
144 d_visited[current] = visitedTheories;
145 Theory* th = d_engine->theoryOf(currentTheoryId);
146 th->preRegisterTerm(current);
147 Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
148 }
149 if (!Theory::setContains(parentTheoryId, visitedTheories)) {
150 visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
151 d_visited[current] = visitedTheories;
152 Theory* th = d_engine->theoryOf(parentTheoryId);
153 th->preRegisterTerm(current);
154 Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
155 }
156 if (useType) {
157 if (!Theory::setContains(typeTheoryId, visitedTheories)) {
158 visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
159 d_visited[current] = visitedTheories;
160 Theory* th = d_engine->theoryOf(typeTheoryId);
161 th->preRegisterTerm(current);
162 Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
163 }
164 }
165 Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
166
167 Assert(d_visited.find(current) != d_visited.end());
168 Assert(alreadyVisited(current, parent));
169 }
170
171 std::string SharedTermsVisitor::toString() const {
172 std::stringstream ss;
173 TNodeVisitedMap::const_iterator it = d_visited.begin();
174 for (; it != d_visited.end(); ++ it) {
175 ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
176 }
177 return ss.str();
178 }
179
180 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
181
182 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
183
184 if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS
185 || parent.getKind() == kind::LAMBDA
186 || parent.getKind() == kind::CHOICE
187 || parent.getKind() == kind::REWRITE_RULE
188 || parent.getKind() == kind::SEP_STAR
189 || parent.getKind() == kind::SEP_WAND
190 || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
191 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
192 )
193 && current != parent)
194 {
195 Debug("register::internal") << "quantifier:true" << std::endl;
196 return true;
197 }
198 TNodeVisitedMap::const_iterator find = d_visited.find(current);
199
200 // If node is not visited at all, just return false
201 if (find == d_visited.end()) {
202 Debug("register::internal") << "1:false" << std::endl;
203 return false;
204 }
205
206 Theory::Set theories = (*find).second;
207
208 TheoryId currentTheoryId = Theory::theoryOf(current);
209 TheoryId parentTheoryId = Theory::theoryOf(parent);
210
211 // Should we use the theory of the type
212 bool useType = false;
213 TheoryId typeTheoryId = THEORY_LAST;
214
215 if (current != parent) {
216 if (currentTheoryId != parentTheoryId) {
217 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
218 TypeNode type = current.getType();
219 useType = true;
220 typeTheoryId = Theory::theoryOf(type);
221 } else {
222 TypeNode type = current.getType();
223 typeTheoryId = Theory::theoryOf(type);
224 if (typeTheoryId != currentTheoryId) {
225 if (type.isInterpretedFinite()) {
226 useType = true;
227 }
228 }
229 }
230 }
231 if (current != parent) {
232 if (currentTheoryId != parentTheoryId) {
233 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
234 TypeNode type = current.getType();
235 useType = true;
236 typeTheoryId = Theory::theoryOf(type);
237 } else {
238 TypeNode type = current.getType();
239 typeTheoryId = Theory::theoryOf(type);
240 if (typeTheoryId != currentTheoryId) {
241 if (type.isInterpretedFinite()) {
242 useType = true;
243 }
244 }
245 }
246 }
247
248 if (Theory::setContains(currentTheoryId, theories)) {
249 if (Theory::setContains(parentTheoryId, theories)) {
250 if (useType) {
251 return Theory::setContains(typeTheoryId, theories);
252 } else {
253 return true;
254 }
255 } else {
256 return false;
257 }
258 } else {
259 return false;
260 }
261 }
262
263 void SharedTermsVisitor::visit(TNode current, TNode parent) {
264
265 Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
266 if (Debug.isOn("register::internal")) {
267 Debug("register::internal") << toString() << std::endl;
268 }
269
270 // Get the theories of the terms
271 TheoryId currentTheoryId = Theory::theoryOf(current);
272 TheoryId parentTheoryId = Theory::theoryOf(parent);
273
274 // Should we use the theory of the type
275 bool useType = false;
276 TheoryId typeTheoryId = THEORY_LAST;
277
278 if (current != parent) {
279 if (currentTheoryId != parentTheoryId) {
280 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
281 TypeNode type = current.getType();
282 useType = true;
283 typeTheoryId = Theory::theoryOf(type);
284 } else {
285 TypeNode type = current.getType();
286 typeTheoryId = Theory::theoryOf(type);
287 if (typeTheoryId != currentTheoryId) {
288 if (type.isInterpretedFinite()) {
289 useType = true;
290 }
291 }
292 }
293 }
294
295 Theory::Set visitedTheories = d_visited[current];
296 Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
297 if (!Theory::setContains(currentTheoryId, visitedTheories)) {
298 visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
299 Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
300 }
301 if (!Theory::setContains(parentTheoryId, visitedTheories)) {
302 visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
303 Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
304 }
305 if (useType) {
306 if (!Theory::setContains(typeTheoryId, visitedTheories)) {
307 visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
308 Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
309 }
310 }
311 Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
312
313 // Record the new theories that we visited
314 d_visited[current] = visitedTheories;
315
316 // If there is more than two theories and a new one has been added notify the shared terms database
317 if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
318 d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
319 }
320
321 Assert(d_visited.find(current) != d_visited.end());
322 Assert(alreadyVisited(current, parent));
323 }
324
325 void SharedTermsVisitor::start(TNode node) {
326 clear();
327 d_atom = node;
328 }
329
330 void SharedTermsVisitor::done(TNode node) {
331 clear();
332 }
333
334 void SharedTermsVisitor::clear() {
335 d_atom = TNode();
336 d_visited.clear();
337 }