1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of term database class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/term_database.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "options/base_options.h" |
20 |
|
#include "options/quantifiers_options.h" |
21 |
|
#include "options/smt_options.h" |
22 |
|
#include "options/theory_options.h" |
23 |
|
#include "options/uf_options.h" |
24 |
|
#include "theory/quantifiers/ematching/trigger_term_info.h" |
25 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
26 |
|
#include "theory/quantifiers/quantifiers_inference_manager.h" |
27 |
|
#include "theory/quantifiers/quantifiers_registry.h" |
28 |
|
#include "theory/quantifiers/quantifiers_state.h" |
29 |
|
#include "theory/quantifiers/term_util.h" |
30 |
|
#include "theory/rewriter.h" |
31 |
|
#include "theory/uf/equality_engine.h" |
32 |
|
|
33 |
|
using namespace cvc5::kind; |
34 |
|
using namespace cvc5::context; |
35 |
|
|
36 |
|
namespace cvc5 { |
37 |
|
namespace theory { |
38 |
|
namespace quantifiers { |
39 |
|
|
40 |
9928 |
TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) |
41 |
|
: QuantifiersUtil(env), |
42 |
|
d_qstate(qs), |
43 |
|
d_qim(nullptr), |
44 |
|
d_qreg(qr), |
45 |
|
d_termsContext(), |
46 |
9928 |
d_termsContextUse(options::termDbCd() ? qs.getSatContext() |
47 |
|
: &d_termsContext), |
48 |
|
d_processed(d_termsContextUse), |
49 |
|
d_typeMap(d_termsContextUse), |
50 |
|
d_ops(d_termsContextUse), |
51 |
|
d_opMap(d_termsContextUse), |
52 |
19856 |
d_inactive_map(qs.getSatContext()) |
53 |
|
{ |
54 |
9928 |
d_consistent_ee = true; |
55 |
9928 |
d_true = NodeManager::currentNM()->mkConst(true); |
56 |
9928 |
d_false = NodeManager::currentNM()->mkConst(false); |
57 |
9928 |
if (!options::termDbCd()) |
58 |
|
{ |
59 |
|
// when not maintaining terms in a context-dependent manner, we clear during |
60 |
|
// each presolve, which requires maintaining a single outermost level |
61 |
|
d_termsContext.push(); |
62 |
|
} |
63 |
9928 |
} |
64 |
|
|
65 |
19660 |
TermDb::~TermDb(){ |
66 |
|
|
67 |
19660 |
} |
68 |
|
|
69 |
9928 |
void TermDb::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; } |
70 |
|
|
71 |
25080 |
void TermDb::registerQuantifier( Node q ) { |
72 |
25080 |
Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q)); |
73 |
84296 |
for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++) |
74 |
|
{ |
75 |
118432 |
Node ic = d_qreg.getInstantiationConstant(q, i); |
76 |
59216 |
setTermInactive( ic ); |
77 |
|
} |
78 |
25080 |
} |
79 |
|
|
80 |
915 |
size_t TermDb::getNumOperators() const { return d_ops.size(); } |
81 |
|
|
82 |
2050 |
Node TermDb::getOperator(size_t i) const |
83 |
|
{ |
84 |
2050 |
Assert(i < d_ops.size()); |
85 |
2050 |
return d_ops[i]; |
86 |
|
} |
87 |
|
|
88 |
|
/** ground terms */ |
89 |
517993 |
size_t TermDb::getNumGroundTerms(Node f) const |
90 |
|
{ |
91 |
517993 |
NodeDbListMap::const_iterator it = d_opMap.find(f); |
92 |
517993 |
if (it != d_opMap.end()) |
93 |
|
{ |
94 |
500621 |
return it->second->d_list.size(); |
95 |
|
} |
96 |
17372 |
return 0; |
97 |
|
} |
98 |
|
|
99 |
2998121 |
Node TermDb::getGroundTerm(Node f, size_t i) const |
100 |
|
{ |
101 |
2998121 |
NodeDbListMap::const_iterator it = d_opMap.find(f); |
102 |
2998121 |
if (it != d_opMap.end()) |
103 |
|
{ |
104 |
2998121 |
Assert(i < it->second->d_list.size()); |
105 |
2998121 |
return it->second->d_list[i]; |
106 |
|
} |
107 |
|
Assert(false); |
108 |
|
return Node::null(); |
109 |
|
} |
110 |
|
|
111 |
248 |
size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const |
112 |
|
{ |
113 |
248 |
TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn); |
114 |
248 |
if (it != d_typeMap.end()) |
115 |
|
{ |
116 |
239 |
return it->second->d_list.size(); |
117 |
|
} |
118 |
9 |
return 0; |
119 |
|
} |
120 |
|
|
121 |
10246 |
Node TermDb::getTypeGroundTerm(TypeNode tn, size_t i) const |
122 |
|
{ |
123 |
10246 |
TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn); |
124 |
10246 |
if (it != d_typeMap.end()) |
125 |
|
{ |
126 |
10246 |
Assert(i < it->second->d_list.size()); |
127 |
10246 |
return it->second->d_list[i]; |
128 |
|
} |
129 |
|
Assert(false); |
130 |
|
return Node::null(); |
131 |
|
} |
132 |
|
|
133 |
2488 |
Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar) |
134 |
|
{ |
135 |
2488 |
TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn); |
136 |
2488 |
if (it != d_typeMap.end()) |
137 |
|
{ |
138 |
519 |
Assert(!it->second->d_list.empty()); |
139 |
519 |
if (!reqVar) |
140 |
|
{ |
141 |
178 |
return it->second->d_list[0]; |
142 |
|
} |
143 |
532 |
for (const Node& v : it->second->d_list) |
144 |
|
{ |
145 |
477 |
if (v.isVar()) |
146 |
|
{ |
147 |
286 |
return v; |
148 |
|
} |
149 |
|
} |
150 |
|
} |
151 |
2024 |
return getOrMakeTypeFreshVariable(tn); |
152 |
|
} |
153 |
|
|
154 |
2024 |
Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) |
155 |
|
{ |
156 |
2024 |
std::unordered_map<TypeNode, Node>::iterator it = d_type_fv.find(tn); |
157 |
2024 |
if (it == d_type_fv.end()) |
158 |
|
{ |
159 |
240 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
160 |
480 |
std::stringstream ss; |
161 |
240 |
ss << language::SetLanguage(options::outputLanguage()); |
162 |
240 |
ss << "e_" << tn; |
163 |
480 |
Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable"); |
164 |
480 |
Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn |
165 |
240 |
<< std::endl; |
166 |
240 |
if (options::instMaxLevel() != -1) |
167 |
|
{ |
168 |
|
QuantAttributes::setInstantiationLevelAttr(k, 0); |
169 |
|
} |
170 |
240 |
d_type_fv[tn] = k; |
171 |
240 |
return k; |
172 |
|
} |
173 |
1784 |
return it->second; |
174 |
|
} |
175 |
|
|
176 |
4864484 |
Node TermDb::getMatchOperator( Node n ) { |
177 |
4864484 |
Kind k = n.getKind(); |
178 |
|
//datatype operators may be parametric, always assume they are |
179 |
4864484 |
if (k == SELECT || k == STORE || k == UNION || k == INTERSECTION |
180 |
4832787 |
|| k == SUBSET || k == SETMINUS || k == MEMBER || k == SINGLETON |
181 |
4803883 |
|| k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || k == APPLY_TESTER |
182 |
4414176 |
|| k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH) |
183 |
|
{ |
184 |
|
//since it is parametric, use a particular one as op |
185 |
940526 |
TypeNode tn = n[0].getType(); |
186 |
940526 |
Node op = n.getOperator(); |
187 |
470263 |
std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op ); |
188 |
470263 |
if( ito!=d_par_op_map.end() ){ |
189 |
461667 |
std::map< TypeNode, Node >::iterator it = ito->second.find( tn ); |
190 |
461667 |
if( it!=ito->second.end() ){ |
191 |
460997 |
return it->second; |
192 |
|
} |
193 |
|
} |
194 |
9266 |
Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl; |
195 |
9266 |
d_par_op_map[op][tn] = n; |
196 |
9266 |
return n; |
197 |
|
} |
198 |
4394221 |
else if (inst::TriggerTermInfo::isAtomicTriggerKind(k)) |
199 |
|
{ |
200 |
4196691 |
return n.getOperator(); |
201 |
|
}else{ |
202 |
197530 |
return Node::null(); |
203 |
|
} |
204 |
|
} |
205 |
|
|
206 |
2519317 |
void TermDb::addTerm(Node n) |
207 |
|
{ |
208 |
2519317 |
if (d_processed.find(n) != d_processed.end()) |
209 |
|
{ |
210 |
1503686 |
return; |
211 |
|
} |
212 |
1015631 |
d_processed.insert(n); |
213 |
1015631 |
if (!TermUtil::hasInstConstAttr(n)) |
214 |
|
{ |
215 |
976331 |
Trace("term-db-debug") << "register term : " << n << std::endl; |
216 |
976331 |
DbList* dlt = getOrMkDbListForType(n.getType()); |
217 |
976331 |
dlt->d_list.push_back(n); |
218 |
|
// if this is an atomic trigger, consider adding it |
219 |
976331 |
if (inst::TriggerTermInfo::isAtomicTrigger(n)) |
220 |
|
{ |
221 |
409018 |
Trace("term-db") << "register term in db " << n << std::endl; |
222 |
|
|
223 |
818036 |
Node op = getMatchOperator(n); |
224 |
409018 |
Trace("term-db-debug") << " match operator is : " << op << std::endl; |
225 |
409018 |
DbList* dlo = getOrMkDbListForOp(op); |
226 |
409018 |
dlo->d_list.push_back(n); |
227 |
|
// If we are higher-order, we may need to register more terms. |
228 |
409018 |
addTermInternal(n); |
229 |
|
} |
230 |
|
} |
231 |
|
else |
232 |
|
{ |
233 |
39300 |
setTermInactive(n); |
234 |
|
} |
235 |
1015631 |
if (!n.isClosure()) |
236 |
|
{ |
237 |
2623740 |
for (const Node& nc : n) |
238 |
|
{ |
239 |
1608131 |
addTerm(nc); |
240 |
|
} |
241 |
|
} |
242 |
|
} |
243 |
|
|
244 |
976331 |
DbList* TermDb::getOrMkDbListForType(TypeNode tn) |
245 |
|
{ |
246 |
976331 |
TypeNodeDbListMap::iterator it = d_typeMap.find(tn); |
247 |
976331 |
if (it != d_typeMap.end()) |
248 |
|
{ |
249 |
951494 |
return it->second.get(); |
250 |
|
} |
251 |
49674 |
std::shared_ptr<DbList> dl = std::make_shared<DbList>(d_termsContextUse); |
252 |
24837 |
d_typeMap.insert(tn, dl); |
253 |
24837 |
return dl.get(); |
254 |
|
} |
255 |
|
|
256 |
468799 |
DbList* TermDb::getOrMkDbListForOp(TNode op) |
257 |
|
{ |
258 |
468799 |
NodeDbListMap::iterator it = d_opMap.find(op); |
259 |
468799 |
if (it != d_opMap.end()) |
260 |
|
{ |
261 |
374218 |
return it->second.get(); |
262 |
|
} |
263 |
189162 |
std::shared_ptr<DbList> dl = std::make_shared<DbList>(d_termsContextUse); |
264 |
94581 |
d_opMap.insert(op, dl); |
265 |
94581 |
Assert(op.getKind() != BOUND_VARIABLE); |
266 |
94581 |
d_ops.push_back(op); |
267 |
94581 |
return dl.get(); |
268 |
|
} |
269 |
|
|
270 |
572466 |
void TermDb::computeArgReps( TNode n ) { |
271 |
572466 |
if (d_arg_reps.find(n) == d_arg_reps.end()) |
272 |
|
{ |
273 |
339782 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
274 |
1084457 |
for (const TNode& nc : n) |
275 |
|
{ |
276 |
1489350 |
TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc; |
277 |
744675 |
d_arg_reps[n].push_back( r ); |
278 |
|
} |
279 |
|
} |
280 |
572466 |
} |
281 |
|
|
282 |
1819454 |
void TermDb::computeUfEqcTerms( TNode f ) { |
283 |
1819454 |
Assert(f == getOperatorRepresentative(f)); |
284 |
1819454 |
if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end()) |
285 |
|
{ |
286 |
1772994 |
return; |
287 |
|
} |
288 |
46460 |
d_func_map_eqc_trie[f].clear(); |
289 |
|
// get the matchable operators in the equivalence class of f |
290 |
92920 |
std::vector<TNode> ops; |
291 |
46460 |
getOperatorsFor(f, ops); |
292 |
46460 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
293 |
93017 |
for (TNode ff : ops) |
294 |
|
{ |
295 |
46557 |
DbList* dbl = getOrMkDbListForOp(ff); |
296 |
341666 |
for (const Node& n : dbl->d_list) |
297 |
|
{ |
298 |
295109 |
if (hasTermCurrent(n) && isTermActive(n)) |
299 |
|
{ |
300 |
279053 |
computeArgReps(n); |
301 |
558106 |
TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n); |
302 |
279053 |
d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]); |
303 |
|
} |
304 |
|
} |
305 |
|
} |
306 |
|
} |
307 |
|
|
308 |
3180164 |
void TermDb::computeUfTerms( TNode f ) { |
309 |
3180164 |
if (d_op_nonred_count.find(f) != d_op_nonred_count.end()) |
310 |
|
{ |
311 |
|
// already computed |
312 |
6278619 |
return; |
313 |
|
} |
314 |
40860 |
Assert(f == getOperatorRepresentative(f)); |
315 |
40860 |
d_op_nonred_count[f] = 0; |
316 |
|
// get the matchable operators in the equivalence class of f |
317 |
81709 |
std::vector<TNode> ops; |
318 |
40860 |
getOperatorsFor(f, ops); |
319 |
40860 |
Trace("term-db-debug") << "computeUfTerms for " << f << std::endl; |
320 |
40860 |
unsigned congruentCount = 0; |
321 |
40860 |
unsigned nonCongruentCount = 0; |
322 |
40860 |
unsigned alreadyCongruentCount = 0; |
323 |
40860 |
unsigned relevantCount = 0; |
324 |
40860 |
NodeManager* nm = NodeManager::currentNM(); |
325 |
74737 |
for (TNode ff : ops) |
326 |
|
{ |
327 |
40946 |
NodeDbListMap::iterator it = d_opMap.find(ff); |
328 |
40946 |
if (it == d_opMap.end()) |
329 |
|
{ |
330 |
|
// no terms for this operator |
331 |
7058 |
continue; |
332 |
|
} |
333 |
33888 |
Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl; |
334 |
344232 |
for (const Node& n : it->second->d_list) |
335 |
|
{ |
336 |
|
// to be added to term index, term must be relevant, and exist in EE |
337 |
310355 |
if (!hasTermCurrent(n) || !d_qstate.hasTerm(n)) |
338 |
|
{ |
339 |
|
Trace("term-db-debug") << n << " is not relevant." << std::endl; |
340 |
75720 |
continue; |
341 |
|
} |
342 |
|
|
343 |
310355 |
relevantCount++; |
344 |
327297 |
if (!isTermActive(n)) |
345 |
|
{ |
346 |
16942 |
Trace("term-db-debug") << n << " is already redundant." << std::endl; |
347 |
16942 |
alreadyCongruentCount++; |
348 |
16942 |
continue; |
349 |
|
} |
350 |
|
|
351 |
293413 |
computeArgReps(n); |
352 |
293413 |
Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; |
353 |
941570 |
for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++) |
354 |
|
{ |
355 |
648157 |
Trace("term-db-debug") << d_arg_reps[n][i] << " "; |
356 |
2592628 |
if (std::find(d_func_map_rel_dom[f][i].begin(), |
357 |
1296314 |
d_func_map_rel_dom[f][i].end(), |
358 |
2592628 |
d_arg_reps[n][i]) |
359 |
1944471 |
== d_func_map_rel_dom[f][i].end()) |
360 |
|
{ |
361 |
235393 |
d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]); |
362 |
|
} |
363 |
|
} |
364 |
293413 |
Trace("term-db-debug") << std::endl; |
365 |
293413 |
Assert(d_qstate.hasTerm(n)); |
366 |
586826 |
Trace("term-db-debug") |
367 |
293413 |
<< " and value : " << d_qstate.getRepresentative(n) << std::endl; |
368 |
528037 |
Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]); |
369 |
293413 |
Assert(d_qstate.hasTerm(at)); |
370 |
293413 |
Trace("term-db-debug2") << "...add term returned " << at << std::endl; |
371 |
352191 |
if (at != n && d_qstate.areEqual(at, n)) |
372 |
|
{ |
373 |
58778 |
setTermInactive(n); |
374 |
58778 |
Trace("term-db-debug") << n << " is redundant." << std::endl; |
375 |
58778 |
congruentCount++; |
376 |
58778 |
continue; |
377 |
|
} |
378 |
469259 |
std::vector<Node> lits; |
379 |
234635 |
if (checkCongruentDisequal(at, n, lits)) |
380 |
|
{ |
381 |
11 |
Assert(at.getNumChildren() == n.getNumChildren()); |
382 |
41 |
for (size_t k = 0, size = at.getNumChildren(); k < size; k++) |
383 |
|
{ |
384 |
30 |
if (at[k] != n[k]) |
385 |
|
{ |
386 |
18 |
lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate()); |
387 |
|
} |
388 |
|
} |
389 |
22 |
Node lem = nm->mkOr(lits); |
390 |
11 |
if (Trace.isOn("term-db-lemma")) |
391 |
|
{ |
392 |
|
Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " |
393 |
|
<< n << "!!!!" << std::endl; |
394 |
|
if (!d_qstate.getValuation().needCheck()) |
395 |
|
{ |
396 |
|
Trace("term-db-lemma") |
397 |
|
<< " all theories passed with no lemmas." << std::endl; |
398 |
|
// we should be a full effort check, prior to theory combination |
399 |
|
} |
400 |
|
Trace("term-db-lemma") << " add lemma : " << lem << std::endl; |
401 |
|
} |
402 |
11 |
d_qim->addPendingLemma(lem, InferenceId::QUANTIFIERS_TDB_DEQ_CONG); |
403 |
11 |
d_qstate.notifyInConflict(); |
404 |
11 |
d_consistent_ee = false; |
405 |
11 |
return; |
406 |
|
} |
407 |
234624 |
nonCongruentCount++; |
408 |
234624 |
d_op_nonred_count[f]++; |
409 |
|
} |
410 |
33877 |
if (Trace.isOn("tdb")) |
411 |
|
{ |
412 |
|
Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount |
413 |
|
<< " / "; |
414 |
|
Trace("tdb") << (nonCongruentCount + congruentCount) << " / " |
415 |
|
<< (nonCongruentCount + congruentCount |
416 |
|
+ alreadyCongruentCount) |
417 |
|
<< " / "; |
418 |
|
Trace("tdb") << relevantCount << " / " << it->second->d_list.size() |
419 |
|
<< std::endl; |
420 |
|
} |
421 |
|
} |
422 |
|
} |
423 |
|
|
424 |
6362474 |
Node TermDb::getOperatorRepresentative(TNode op) const { return op; } |
425 |
|
|
426 |
226605 |
bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp) |
427 |
|
{ |
428 |
226605 |
if (d_qstate.areDisequal(a, b)) |
429 |
|
{ |
430 |
11 |
exp.push_back(a.eqNode(b)); |
431 |
11 |
return true; |
432 |
|
} |
433 |
226594 |
return false; |
434 |
|
} |
435 |
|
|
436 |
2137881 |
bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { |
437 |
|
// notice if we are not higher-order, getOperatorRepresentative is a no-op |
438 |
2137881 |
f = getOperatorRepresentative(f); |
439 |
2137881 |
computeUfTerms( f ); |
440 |
2137881 |
Assert(!d_qstate.getEqualityEngine()->hasTerm(r) |
441 |
|
|| d_qstate.getEqualityEngine()->getRepresentative(r) == r); |
442 |
2137881 |
std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); |
443 |
2137881 |
if( it != d_func_map_rel_dom.end() ){ |
444 |
2113395 |
std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); |
445 |
2113395 |
if( it2!=it->second.end() ){ |
446 |
2113395 |
return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end(); |
447 |
|
}else{ |
448 |
|
return false; |
449 |
|
} |
450 |
|
}else{ |
451 |
24486 |
return false; |
452 |
|
} |
453 |
|
} |
454 |
|
|
455 |
585053 |
Node TermDb::evaluateTerm2(TNode n, |
456 |
|
std::map<TNode, Node>& visited, |
457 |
|
std::vector<Node>& exp, |
458 |
|
bool useEntailmentTests, |
459 |
|
bool computeExp, |
460 |
|
bool reqHasTerm) |
461 |
|
{ |
462 |
585053 |
std::map< TNode, Node >::iterator itv = visited.find( n ); |
463 |
585053 |
if( itv != visited.end() ){ |
464 |
44227 |
return itv->second; |
465 |
|
} |
466 |
540826 |
size_t prevSize = exp.size(); |
467 |
540826 |
Trace("term-db-eval") << "evaluate term : " << n << std::endl; |
468 |
1081652 |
Node ret = n; |
469 |
540826 |
if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ |
470 |
|
//do nothing |
471 |
|
} |
472 |
538363 |
else if (d_qstate.hasTerm(n)) |
473 |
|
{ |
474 |
252999 |
Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; |
475 |
252999 |
ret = d_qstate.getRepresentative(n); |
476 |
252999 |
if (computeExp) |
477 |
|
{ |
478 |
|
if (n != ret) |
479 |
|
{ |
480 |
|
exp.push_back(n.eqNode(ret)); |
481 |
|
} |
482 |
|
} |
483 |
252999 |
reqHasTerm = false; |
484 |
|
} |
485 |
285364 |
else if (n.hasOperator()) |
486 |
|
{ |
487 |
569858 |
std::vector<TNode> args; |
488 |
284929 |
bool ret_set = false; |
489 |
284929 |
Kind k = n.getKind(); |
490 |
569858 |
std::vector<Node> tempExp; |
491 |
648553 |
for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) |
492 |
|
{ |
493 |
979606 |
TNode c = evaluateTerm2(n[i], |
494 |
|
visited, |
495 |
|
tempExp, |
496 |
|
useEntailmentTests, |
497 |
|
computeExp, |
498 |
853427 |
reqHasTerm); |
499 |
489803 |
if (c.isNull()) |
500 |
|
{ |
501 |
89823 |
ret = Node::null(); |
502 |
89823 |
ret_set = true; |
503 |
89823 |
break; |
504 |
|
} |
505 |
399980 |
else if (c == d_true || c == d_false) |
506 |
|
{ |
507 |
|
// short-circuiting |
508 |
197399 |
if ((k == AND && c == d_false) || (k == OR && c == d_true)) |
509 |
|
{ |
510 |
32149 |
ret = c; |
511 |
32149 |
ret_set = true; |
512 |
32149 |
reqHasTerm = false; |
513 |
32149 |
break; |
514 |
|
} |
515 |
165250 |
else if (k == ITE && i == 0) |
516 |
|
{ |
517 |
4207 |
ret = evaluateTerm2(n[c == d_true ? 1 : 2], |
518 |
|
visited, |
519 |
|
tempExp, |
520 |
|
useEntailmentTests, |
521 |
|
computeExp, |
522 |
|
reqHasTerm); |
523 |
4207 |
ret_set = true; |
524 |
4207 |
reqHasTerm = false; |
525 |
4207 |
break; |
526 |
|
} |
527 |
|
} |
528 |
363624 |
if (computeExp) |
529 |
|
{ |
530 |
|
exp.insert(exp.end(), tempExp.begin(), tempExp.end()); |
531 |
|
} |
532 |
363624 |
Trace("term-db-eval") << " child " << i << " : " << c << std::endl; |
533 |
363624 |
args.push_back(c); |
534 |
|
} |
535 |
284929 |
if (ret_set) |
536 |
|
{ |
537 |
|
// if we short circuited |
538 |
126179 |
if (computeExp) |
539 |
|
{ |
540 |
|
exp.clear(); |
541 |
|
exp.insert(exp.end(), tempExp.begin(), tempExp.end()); |
542 |
|
} |
543 |
|
} |
544 |
|
else |
545 |
|
{ |
546 |
|
// get the (indexed) operator of n, if it exists |
547 |
317500 |
TNode f = getMatchOperator(n); |
548 |
|
// if it is an indexed term, return the congruent term |
549 |
158750 |
if (!f.isNull()) |
550 |
|
{ |
551 |
|
// if f is congruent to a term indexed by this class |
552 |
120026 |
TNode nn = getCongruentTerm(f, args); |
553 |
120026 |
Trace("term-db-eval") << " got congruent term " << nn |
554 |
60013 |
<< " from DB for " << n << std::endl; |
555 |
60013 |
if (!nn.isNull()) |
556 |
|
{ |
557 |
20243 |
if (computeExp) |
558 |
|
{ |
559 |
|
Assert(nn.getNumChildren() == n.getNumChildren()); |
560 |
|
for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++) |
561 |
|
{ |
562 |
|
if (nn[i] != n[i]) |
563 |
|
{ |
564 |
|
exp.push_back(nn[i].eqNode(n[i])); |
565 |
|
} |
566 |
|
} |
567 |
|
} |
568 |
20243 |
ret = d_qstate.getRepresentative(nn); |
569 |
20243 |
Trace("term-db-eval") << "return rep" << std::endl; |
570 |
20243 |
ret_set = true; |
571 |
20243 |
reqHasTerm = false; |
572 |
20243 |
Assert(!ret.isNull()); |
573 |
20243 |
if (computeExp) |
574 |
|
{ |
575 |
|
if (n != ret) |
576 |
|
{ |
577 |
|
exp.push_back(nn.eqNode(ret)); |
578 |
|
} |
579 |
|
} |
580 |
|
} |
581 |
|
} |
582 |
158750 |
if( !ret_set ){ |
583 |
138507 |
Trace("term-db-eval") << "return rewrite" << std::endl; |
584 |
|
// a theory symbol or a new UF term |
585 |
138507 |
if (n.getMetaKind() == metakind::PARAMETERIZED) |
586 |
|
{ |
587 |
39631 |
args.insert(args.begin(), n.getOperator()); |
588 |
|
} |
589 |
138507 |
ret = NodeManager::currentNM()->mkNode(n.getKind(), args); |
590 |
138507 |
ret = Rewriter::rewrite(ret); |
591 |
138507 |
if (ret.getKind() == EQUAL) |
592 |
|
{ |
593 |
16398 |
if (d_qstate.areDisequal(ret[0], ret[1])) |
594 |
|
{ |
595 |
4706 |
ret = d_false; |
596 |
|
} |
597 |
|
} |
598 |
138507 |
if (useEntailmentTests) |
599 |
|
{ |
600 |
1359 |
if (ret.getKind() == EQUAL || ret.getKind() == GEQ) |
601 |
|
{ |
602 |
15 |
Valuation& val = d_qstate.getValuation(); |
603 |
41 |
for (unsigned j = 0; j < 2; j++) |
604 |
|
{ |
605 |
|
std::pair<bool, Node> et = val.entailmentCheck( |
606 |
|
options::TheoryOfMode::THEORY_OF_TYPE_BASED, |
607 |
56 |
j == 0 ? ret : ret.negate()); |
608 |
30 |
if (et.first) |
609 |
|
{ |
610 |
4 |
ret = j == 0 ? d_true : d_false; |
611 |
4 |
if (computeExp) |
612 |
|
{ |
613 |
|
exp.push_back(et.second); |
614 |
|
} |
615 |
4 |
break; |
616 |
|
} |
617 |
|
} |
618 |
|
} |
619 |
|
} |
620 |
|
} |
621 |
|
} |
622 |
|
} |
623 |
|
// must have the term |
624 |
540826 |
if (reqHasTerm && !ret.isNull()) |
625 |
|
{ |
626 |
136589 |
Kind k = ret.getKind(); |
627 |
136589 |
if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT |
628 |
122369 |
&& k != FORALL) |
629 |
|
{ |
630 |
122174 |
if (!d_qstate.hasTerm(ret)) |
631 |
|
{ |
632 |
37423 |
ret = Node::null(); |
633 |
|
} |
634 |
|
} |
635 |
|
} |
636 |
1081652 |
Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret |
637 |
540826 |
<< ", reqHasTerm = " << reqHasTerm << std::endl; |
638 |
|
// clear the explanation if failed |
639 |
540826 |
if (computeExp && ret.isNull()) |
640 |
|
{ |
641 |
|
exp.resize(prevSize); |
642 |
|
} |
643 |
540826 |
visited[n] = ret; |
644 |
540826 |
return ret; |
645 |
|
} |
646 |
|
|
647 |
9164571 |
TNode TermDb::getEntailedTerm2(TNode n, |
648 |
|
std::map<TNode, TNode>& subs, |
649 |
|
bool subsRep, |
650 |
|
bool hasSubs) |
651 |
|
{ |
652 |
9164571 |
Trace("term-db-entail") << "get entailed term : " << n << std::endl; |
653 |
9164571 |
if (d_qstate.hasTerm(n)) |
654 |
|
{ |
655 |
2839879 |
Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; |
656 |
2839879 |
return n; |
657 |
6324692 |
}else if( n.getKind()==BOUND_VARIABLE ){ |
658 |
3612933 |
if( hasSubs ){ |
659 |
3612933 |
std::map< TNode, TNode >::iterator it = subs.find( n ); |
660 |
3612933 |
if( it!=subs.end() ){ |
661 |
2689687 |
Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; |
662 |
2689687 |
if( subsRep ){ |
663 |
348105 |
Assert(d_qstate.hasTerm(it->second)); |
664 |
348105 |
Assert(d_qstate.getRepresentative(it->second) == it->second); |
665 |
3037792 |
return it->second; |
666 |
|
} |
667 |
2341582 |
return getEntailedTerm2(it->second, subs, subsRep, hasSubs); |
668 |
|
} |
669 |
|
} |
670 |
2711759 |
}else if( n.getKind()==ITE ){ |
671 |
26068 |
for( unsigned i=0; i<2; i++ ){ |
672 |
21513 |
if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) |
673 |
|
{ |
674 |
7716 |
return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); |
675 |
|
} |
676 |
|
} |
677 |
|
}else{ |
678 |
2699488 |
if( n.hasOperator() ){ |
679 |
2705437 |
TNode f = getMatchOperator( n ); |
680 |
2692612 |
if( !f.isNull() ){ |
681 |
5359574 |
std::vector< TNode > args; |
682 |
5698791 |
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
683 |
7756087 |
TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs); |
684 |
4737083 |
if( c.isNull() ){ |
685 |
1718079 |
return TNode::null(); |
686 |
|
} |
687 |
3019004 |
c = d_qstate.getRepresentative(c); |
688 |
3019004 |
Trace("term-db-entail") << " child " << i << " : " << c << std::endl; |
689 |
3019004 |
args.push_back( c ); |
690 |
|
} |
691 |
1923416 |
TNode nn = getCongruentTerm(f, args); |
692 |
961708 |
Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl; |
693 |
961708 |
return nn; |
694 |
|
} |
695 |
|
} |
696 |
|
} |
697 |
947502 |
return TNode::null(); |
698 |
|
} |
699 |
|
|
700 |
91043 |
Node TermDb::evaluateTerm(TNode n, |
701 |
|
bool useEntailmentTests, |
702 |
|
bool reqHasTerm) |
703 |
|
{ |
704 |
182086 |
std::map< TNode, Node > visited; |
705 |
182086 |
std::vector<Node> exp; |
706 |
182086 |
return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); |
707 |
|
} |
708 |
|
|
709 |
|
Node TermDb::evaluateTerm(TNode n, |
710 |
|
std::vector<Node>& exp, |
711 |
|
bool useEntailmentTests, |
712 |
|
bool reqHasTerm) |
713 |
|
{ |
714 |
|
std::map<TNode, Node> visited; |
715 |
|
return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); |
716 |
|
} |
717 |
|
|
718 |
860201 |
TNode TermDb::getEntailedTerm(TNode n, |
719 |
|
std::map<TNode, TNode>& subs, |
720 |
|
bool subsRep) |
721 |
|
{ |
722 |
860201 |
return getEntailedTerm2(n, subs, subsRep, true); |
723 |
|
} |
724 |
|
|
725 |
87516 |
TNode TermDb::getEntailedTerm(TNode n) |
726 |
|
{ |
727 |
175032 |
std::map< TNode, TNode > subs; |
728 |
175032 |
return getEntailedTerm2(n, subs, false, false); |
729 |
|
} |
730 |
|
|
731 |
1789786 |
bool TermDb::isEntailed2( |
732 |
|
TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol) |
733 |
|
{ |
734 |
1789786 |
Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; |
735 |
1789786 |
Assert(n.getType().isBoolean()); |
736 |
1789786 |
if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ |
737 |
569784 |
TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); |
738 |
414010 |
if( !n1.isNull() ){ |
739 |
498902 |
TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); |
740 |
378569 |
if( !n2.isNull() ){ |
741 |
258236 |
if( n1==n2 ){ |
742 |
22648 |
return pol; |
743 |
|
}else{ |
744 |
235588 |
Assert(d_qstate.hasTerm(n1)); |
745 |
235588 |
Assert(d_qstate.hasTerm(n2)); |
746 |
235588 |
if( pol ){ |
747 |
121354 |
return d_qstate.areEqual(n1, n2); |
748 |
|
}else{ |
749 |
114234 |
return d_qstate.areDisequal(n1, n2); |
750 |
|
} |
751 |
|
} |
752 |
|
} |
753 |
|
} |
754 |
1375776 |
}else if( n.getKind()==NOT ){ |
755 |
456269 |
return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); |
756 |
919507 |
}else if( n.getKind()==OR || n.getKind()==AND ){ |
757 |
306653 |
bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); |
758 |
1021474 |
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
759 |
860473 |
if (isEntailed2(n[i], subs, subsRep, hasSubs, pol)) |
760 |
|
{ |
761 |
177621 |
if( simPol ){ |
762 |
63402 |
return true; |
763 |
|
} |
764 |
|
}else{ |
765 |
682852 |
if( !simPol ){ |
766 |
82250 |
return false; |
767 |
|
} |
768 |
|
} |
769 |
|
} |
770 |
161001 |
return !simPol; |
771 |
|
//Boolean equality here |
772 |
612854 |
}else if( n.getKind()==EQUAL || n.getKind()==ITE ){ |
773 |
80609 |
for( unsigned i=0; i<2; i++ ){ |
774 |
67609 |
if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) |
775 |
|
{ |
776 |
29395 |
unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2; |
777 |
29395 |
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; |
778 |
29395 |
return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol); |
779 |
|
} |
780 |
|
} |
781 |
570459 |
}else if( n.getKind()==APPLY_UF ){ |
782 |
454521 |
TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs); |
783 |
337894 |
if( !n1.isNull() ){ |
784 |
221267 |
Assert(d_qstate.hasTerm(n1)); |
785 |
221267 |
if( n1==d_true ){ |
786 |
|
return pol; |
787 |
221267 |
}else if( n1==d_false ){ |
788 |
|
return !pol; |
789 |
|
}else{ |
790 |
221267 |
return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false); |
791 |
|
} |
792 |
|
} |
793 |
232565 |
}else if( n.getKind()==FORALL && !pol ){ |
794 |
4790 |
return isEntailed2(n[1], subs, subsRep, hasSubs, pol); |
795 |
|
} |
796 |
513176 |
return false; |
797 |
|
} |
798 |
|
|
799 |
1432 |
bool TermDb::isEntailed(TNode n, bool pol) |
800 |
|
{ |
801 |
1432 |
Assert(d_consistent_ee); |
802 |
2864 |
std::map< TNode, TNode > subs; |
803 |
2864 |
return isEntailed2(n, subs, false, false, pol); |
804 |
|
} |
805 |
|
|
806 |
348305 |
bool TermDb::isEntailed(TNode n, |
807 |
|
std::map<TNode, TNode>& subs, |
808 |
|
bool subsRep, |
809 |
|
bool pol) |
810 |
|
{ |
811 |
348305 |
Assert(d_consistent_ee); |
812 |
348305 |
return isEntailed2(n, subs, subsRep, true, pol); |
813 |
|
} |
814 |
|
|
815 |
4402043 |
bool TermDb::isTermActive( Node n ) { |
816 |
4402043 |
return d_inactive_map.find( n )==d_inactive_map.end(); |
817 |
|
//return !n.getAttribute(NoMatchAttribute()); |
818 |
|
} |
819 |
|
|
820 |
157294 |
void TermDb::setTermInactive( Node n ) { |
821 |
157294 |
d_inactive_map[n] = true; |
822 |
|
//Trace("term-db-debug2") << "set no match attribute" << std::endl; |
823 |
|
//NoMatchAttribute nma; |
824 |
|
//n.setAttribute(nma,true); |
825 |
157294 |
} |
826 |
|
|
827 |
4386419 |
bool TermDb::hasTermCurrent( Node n, bool useMode ) { |
828 |
4386419 |
if( !useMode ){ |
829 |
|
return d_has_map.find( n )!=d_has_map.end(); |
830 |
|
} |
831 |
|
//some assertions are not sent to EE |
832 |
4386419 |
if (options::termDbMode() == options::TermDbMode::ALL) |
833 |
|
{ |
834 |
4386419 |
return true; |
835 |
|
} |
836 |
|
else if (options::termDbMode() == options::TermDbMode::RELEVANT) |
837 |
|
{ |
838 |
|
return d_has_map.find( n )!=d_has_map.end(); |
839 |
|
} |
840 |
|
Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode(); |
841 |
|
return false; |
842 |
|
} |
843 |
|
|
844 |
1146 |
bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) |
845 |
|
{ |
846 |
1146 |
if( options::instMaxLevel()!=-1 ){ |
847 |
970 |
if( n.hasAttribute(InstLevelAttribute()) ){ |
848 |
|
int64_t fml = |
849 |
970 |
f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f); |
850 |
970 |
unsigned ml = fml>=0 ? fml : options::instMaxLevel(); |
851 |
|
|
852 |
970 |
if( n.getAttribute(InstLevelAttribute())>ml ){ |
853 |
|
Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); |
854 |
|
Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl; |
855 |
|
return false; |
856 |
|
} |
857 |
|
}else{ |
858 |
|
if( options::instLevelInputOnly() ){ |
859 |
|
Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; |
860 |
|
return false; |
861 |
|
} |
862 |
|
} |
863 |
|
} |
864 |
|
// it cannot have instantiation constants, which originate from |
865 |
|
// counterexample-guided instantiation strategies. |
866 |
1146 |
return !TermUtil::hasInstConstAttr(n); |
867 |
|
} |
868 |
|
|
869 |
176 |
Node TermDb::getEligibleTermInEqc( TNode r ) { |
870 |
176 |
if( isTermEligibleForInstantiation( r, TNode::null() ) ){ |
871 |
176 |
return r; |
872 |
|
}else{ |
873 |
|
std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r ); |
874 |
|
if( it==d_term_elig_eqc.end() ){ |
875 |
|
Node h; |
876 |
|
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
877 |
|
eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); |
878 |
|
while (!eqc_i.isFinished()) |
879 |
|
{ |
880 |
|
TNode n = (*eqc_i); |
881 |
|
++eqc_i; |
882 |
|
if (isTermEligibleForInstantiation(n, TNode::null())) |
883 |
|
{ |
884 |
|
h = n; |
885 |
|
break; |
886 |
|
} |
887 |
|
} |
888 |
|
d_term_elig_eqc[r] = h; |
889 |
|
return h; |
890 |
|
}else{ |
891 |
|
return it->second; |
892 |
|
} |
893 |
|
} |
894 |
|
} |
895 |
|
|
896 |
27528 |
bool TermDb::resetInternal(Theory::Effort e) |
897 |
|
{ |
898 |
|
// do nothing |
899 |
27528 |
return true; |
900 |
|
} |
901 |
|
|
902 |
27528 |
bool TermDb::finishResetInternal(Theory::Effort e) |
903 |
|
{ |
904 |
|
// do nothing |
905 |
27528 |
return true; |
906 |
|
} |
907 |
|
|
908 |
372372 |
void TermDb::addTermInternal(Node n) |
909 |
|
{ |
910 |
|
// do nothing |
911 |
372372 |
} |
912 |
|
|
913 |
84357 |
void TermDb::getOperatorsFor(TNode f, std::vector<TNode>& ops) |
914 |
|
{ |
915 |
84357 |
ops.push_back(f); |
916 |
84357 |
} |
917 |
|
|
918 |
|
void TermDb::setHasTerm( Node n ) { |
919 |
|
Trace("term-db-debug2") << "hasTerm : " << n << std::endl; |
920 |
|
if( d_has_map.find( n )==d_has_map.end() ){ |
921 |
|
d_has_map[n] = true; |
922 |
|
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
923 |
|
setHasTerm( n[i] ); |
924 |
|
} |
925 |
|
} |
926 |
|
} |
927 |
|
|
928 |
8213 |
void TermDb::presolve() { |
929 |
8213 |
if (options::incrementalSolving() && !options::termDbCd()) |
930 |
|
{ |
931 |
|
d_termsContext.pop(); |
932 |
|
d_termsContext.push(); |
933 |
|
} |
934 |
8213 |
} |
935 |
|
|
936 |
28439 |
bool TermDb::reset( Theory::Effort effort ){ |
937 |
28439 |
d_op_nonred_count.clear(); |
938 |
28439 |
d_arg_reps.clear(); |
939 |
28439 |
d_func_map_trie.clear(); |
940 |
28439 |
d_func_map_eqc_trie.clear(); |
941 |
28439 |
d_func_map_rel_dom.clear(); |
942 |
28439 |
d_consistent_ee = true; |
943 |
|
|
944 |
28439 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
945 |
|
|
946 |
28439 |
Assert(ee->consistent()); |
947 |
|
// if higher-order, add equalities for the purification terms now |
948 |
28439 |
if (!resetInternal(effort)) |
949 |
|
{ |
950 |
|
return false; |
951 |
|
} |
952 |
|
|
953 |
|
//compute has map |
954 |
28439 |
if (options::termDbMode() == options::TermDbMode::RELEVANT) |
955 |
|
{ |
956 |
|
d_has_map.clear(); |
957 |
|
d_term_elig_eqc.clear(); |
958 |
|
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); |
959 |
|
while( !eqcs_i.isFinished() ){ |
960 |
|
TNode r = (*eqcs_i); |
961 |
|
bool addedFirst = false; |
962 |
|
Node first; |
963 |
|
//TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant |
964 |
|
eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee); |
965 |
|
while( !eqc_i.isFinished() ){ |
966 |
|
TNode n = (*eqc_i); |
967 |
|
if( first.isNull() ){ |
968 |
|
first = n; |
969 |
|
}else{ |
970 |
|
if( !addedFirst ){ |
971 |
|
addedFirst = true; |
972 |
|
setHasTerm( first ); |
973 |
|
} |
974 |
|
setHasTerm( n ); |
975 |
|
} |
976 |
|
++eqc_i; |
977 |
|
} |
978 |
|
++eqcs_i; |
979 |
|
} |
980 |
|
const LogicInfo& logicInfo = d_qstate.getLogicInfo(); |
981 |
|
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) |
982 |
|
{ |
983 |
|
if (!logicInfo.isTheoryEnabled(theoryId)) |
984 |
|
{ |
985 |
|
continue; |
986 |
|
} |
987 |
|
for (context::CDList<Assertion>::const_iterator |
988 |
|
it = d_qstate.factsBegin(theoryId), |
989 |
|
it_end = d_qstate.factsEnd(theoryId); |
990 |
|
it != it_end; |
991 |
|
++it) |
992 |
|
{ |
993 |
|
setHasTerm((*it).d_assertion); |
994 |
|
} |
995 |
|
} |
996 |
|
} |
997 |
|
// finish reset |
998 |
28439 |
return finishResetInternal(effort); |
999 |
|
} |
1000 |
|
|
1001 |
20562 |
TNodeTrie* TermDb::getTermArgTrie(Node f) |
1002 |
|
{ |
1003 |
20562 |
f = getOperatorRepresentative(f); |
1004 |
20562 |
computeUfTerms( f ); |
1005 |
20562 |
std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f); |
1006 |
20562 |
if( itut!=d_func_map_trie.end() ){ |
1007 |
12135 |
return &itut->second; |
1008 |
|
}else{ |
1009 |
8427 |
return NULL; |
1010 |
|
} |
1011 |
|
} |
1012 |
|
|
1013 |
1819454 |
TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f) |
1014 |
|
{ |
1015 |
1819454 |
f = getOperatorRepresentative(f); |
1016 |
1819454 |
computeUfEqcTerms( f ); |
1017 |
1819454 |
std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f); |
1018 |
1819454 |
if( itut==d_func_map_eqc_trie.end() ){ |
1019 |
|
return NULL; |
1020 |
|
}else{ |
1021 |
1819454 |
if( eqc.isNull() ){ |
1022 |
907035 |
return &itut->second; |
1023 |
|
}else{ |
1024 |
|
std::map<TNode, TNodeTrie>::iterator itute = |
1025 |
912419 |
itut->second.d_data.find(eqc); |
1026 |
912419 |
if( itute!=itut->second.d_data.end() ){ |
1027 |
560133 |
return &itute->second; |
1028 |
|
}else{ |
1029 |
352286 |
return NULL; |
1030 |
|
} |
1031 |
|
} |
1032 |
|
} |
1033 |
|
} |
1034 |
|
|
1035 |
|
TNode TermDb::getCongruentTerm( Node f, Node n ) { |
1036 |
|
f = getOperatorRepresentative(f); |
1037 |
|
computeUfTerms( f ); |
1038 |
|
std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f); |
1039 |
|
if( itut!=d_func_map_trie.end() ){ |
1040 |
|
computeArgReps( n ); |
1041 |
|
return itut->second.existsTerm( d_arg_reps[n] ); |
1042 |
|
}else{ |
1043 |
|
return TNode::null(); |
1044 |
|
} |
1045 |
|
} |
1046 |
|
|
1047 |
1021721 |
TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { |
1048 |
1021721 |
f = getOperatorRepresentative(f); |
1049 |
1021721 |
computeUfTerms( f ); |
1050 |
1021721 |
return d_func_map_trie[f].existsTerm( args ); |
1051 |
|
} |
1052 |
|
|
1053 |
|
} // namespace quantifiers |
1054 |
|
} // namespace theory |
1055 |
29505 |
} // namespace cvc5 |