1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Dejan Jovanovic |
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 |
|
* This is the interface to TheoryUF implementations |
14 |
|
* |
15 |
|
* All implementations of TheoryUF should inherit from this class. |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "theory/uf/theory_uf.h" |
19 |
|
|
20 |
|
#include <memory> |
21 |
|
#include <sstream> |
22 |
|
|
23 |
|
#include "expr/node_algorithm.h" |
24 |
|
#include "options/quantifiers_options.h" |
25 |
|
#include "options/smt_options.h" |
26 |
|
#include "options/theory_options.h" |
27 |
|
#include "options/uf_options.h" |
28 |
|
#include "proof/proof_node_manager.h" |
29 |
|
#include "smt/logic_exception.h" |
30 |
|
#include "theory/theory_model.h" |
31 |
|
#include "theory/type_enumerator.h" |
32 |
|
#include "theory/uf/cardinality_extension.h" |
33 |
|
#include "theory/uf/ho_extension.h" |
34 |
|
#include "theory/uf/theory_uf_rewriter.h" |
35 |
|
|
36 |
|
using namespace std; |
37 |
|
|
38 |
|
namespace cvc5 { |
39 |
|
namespace theory { |
40 |
|
namespace uf { |
41 |
|
|
42 |
|
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ |
43 |
9856 |
TheoryUF::TheoryUF(Env& env, |
44 |
|
OutputChannel& out, |
45 |
|
Valuation valuation, |
46 |
9856 |
std::string instanceName) |
47 |
|
: Theory(THEORY_UF, env, out, valuation, instanceName), |
48 |
|
d_thss(nullptr), |
49 |
|
d_ho(nullptr), |
50 |
|
d_functionsTerms(getSatContext()), |
51 |
9856 |
d_symb(getUserContext(), instanceName), |
52 |
|
d_state(env, valuation), |
53 |
19712 |
d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false), |
54 |
39424 |
d_notify(d_im, *this) |
55 |
|
{ |
56 |
9856 |
d_true = NodeManager::currentNM()->mkConst( true ); |
57 |
|
// indicate we are using the default theory state and inference managers |
58 |
9856 |
d_theoryState = &d_state; |
59 |
9856 |
d_inferManager = &d_im; |
60 |
9856 |
} |
61 |
|
|
62 |
19712 |
TheoryUF::~TheoryUF() { |
63 |
19712 |
} |
64 |
|
|
65 |
9856 |
TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; } |
66 |
|
|
67 |
3771 |
ProofRuleChecker* TheoryUF::getProofChecker() { return &d_checker; } |
68 |
|
|
69 |
9856 |
bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi) |
70 |
|
{ |
71 |
9856 |
esi.d_notify = &d_notify; |
72 |
9856 |
esi.d_name = d_instanceName + "theory::uf::ee"; |
73 |
19712 |
if (options::finiteModelFind() |
74 |
9856 |
&& options::ufssMode() != options::UfssMode::NONE) |
75 |
|
{ |
76 |
|
// need notifications about sorts |
77 |
286 |
esi.d_notifyNewClass = true; |
78 |
286 |
esi.d_notifyMerge = true; |
79 |
286 |
esi.d_notifyDisequal = true; |
80 |
|
} |
81 |
9856 |
return true; |
82 |
|
} |
83 |
|
|
84 |
9856 |
void TheoryUF::finishInit() { |
85 |
9856 |
Assert(d_equalityEngine != nullptr); |
86 |
|
// combined cardinality constraints are not evaluated in getModelValue |
87 |
9856 |
d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); |
88 |
|
// Initialize the cardinality constraints solver if the logic includes UF, |
89 |
|
// finite model finding is enabled, and it is not disabled by |
90 |
|
// options::ufssMode(). |
91 |
19712 |
if (options::finiteModelFind() |
92 |
9856 |
&& options::ufssMode() != options::UfssMode::NONE) |
93 |
|
{ |
94 |
286 |
d_thss.reset(new CardinalityExtension(d_state, d_im, this)); |
95 |
|
} |
96 |
|
// The kinds we are treating as function application in congruence |
97 |
9856 |
d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); |
98 |
9856 |
if (options::ufHo()) |
99 |
|
{ |
100 |
187 |
d_equalityEngine->addFunctionKind(kind::HO_APPLY); |
101 |
187 |
d_ho.reset(new HoExtension(d_state, d_im)); |
102 |
|
} |
103 |
9856 |
} |
104 |
|
|
105 |
|
static Node mkAnd(const std::vector<TNode>& conjunctions) { |
106 |
|
Assert(conjunctions.size() > 0); |
107 |
|
|
108 |
|
std::set<TNode> all; |
109 |
|
all.insert(conjunctions.begin(), conjunctions.end()); |
110 |
|
|
111 |
|
if (all.size() == 1) { |
112 |
|
// All the same, or just one |
113 |
|
return conjunctions[0]; |
114 |
|
} |
115 |
|
|
116 |
|
NodeBuilder conjunction(kind::AND); |
117 |
|
std::set<TNode>::const_iterator it = all.begin(); |
118 |
|
std::set<TNode>::const_iterator it_end = all.end(); |
119 |
|
while (it != it_end) { |
120 |
|
conjunction << *it; |
121 |
|
++ it; |
122 |
|
} |
123 |
|
|
124 |
|
return conjunction; |
125 |
|
}/* mkAnd() */ |
126 |
|
|
127 |
|
//--------------------------------- standard check |
128 |
|
|
129 |
15354 |
bool TheoryUF::needsCheckLastEffort() |
130 |
|
{ |
131 |
|
// last call effort needed if using finite model finding |
132 |
15354 |
return d_thss != nullptr; |
133 |
|
} |
134 |
|
|
135 |
1234702 |
void TheoryUF::postCheck(Effort level) |
136 |
|
{ |
137 |
1234702 |
if (d_state.isInConflict()) |
138 |
|
{ |
139 |
58066 |
return; |
140 |
|
} |
141 |
|
// check with the cardinality constraints extension |
142 |
1176636 |
if (d_thss != nullptr) |
143 |
|
{ |
144 |
88871 |
d_thss->check(level); |
145 |
|
} |
146 |
|
// check with the higher-order extension at full effort |
147 |
1176636 |
if (!d_state.isInConflict() && fullEffort(level)) |
148 |
|
{ |
149 |
74869 |
if (options::ufHo()) |
150 |
|
{ |
151 |
1049 |
d_ho->check(); |
152 |
|
} |
153 |
|
} |
154 |
|
} |
155 |
|
|
156 |
3377334 |
void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) |
157 |
|
{ |
158 |
3377334 |
if (d_state.isInConflict()) |
159 |
|
{ |
160 |
57092 |
return; |
161 |
|
} |
162 |
3320242 |
if (d_thss != nullptr) |
163 |
|
{ |
164 |
|
bool isDecision = |
165 |
218462 |
d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); |
166 |
218462 |
d_thss->assertNode(fact, isDecision); |
167 |
|
} |
168 |
3320242 |
switch (atom.getKind()) |
169 |
|
{ |
170 |
3103863 |
case kind::EQUAL: |
171 |
|
{ |
172 |
3103863 |
if (options::ufHo() && options::ufHoExt()) |
173 |
|
{ |
174 |
33184 |
if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) |
175 |
|
{ |
176 |
|
// apply extensionality eagerly using the ho extension |
177 |
3725 |
d_ho->applyExtensionality(fact); |
178 |
|
} |
179 |
|
} |
180 |
|
} |
181 |
3103863 |
break; |
182 |
13655 |
case kind::CARDINALITY_CONSTRAINT: |
183 |
|
case kind::COMBINED_CARDINALITY_CONSTRAINT: |
184 |
|
{ |
185 |
13655 |
if (d_thss == nullptr) |
186 |
|
{ |
187 |
|
if (!getLogicInfo().hasCardinalityConstraints()) |
188 |
|
{ |
189 |
|
std::stringstream ss; |
190 |
|
ss << "Cardinality constraint " << atom |
191 |
|
<< " was asserted, but the logic does not allow it." << std::endl; |
192 |
|
ss << "Try using a logic containing \"UFC\"." << std::endl; |
193 |
|
throw Exception(ss.str()); |
194 |
|
} |
195 |
|
else |
196 |
|
{ |
197 |
|
// support for cardinality constraints is not enabled, set incomplete |
198 |
|
d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); |
199 |
|
} |
200 |
|
} |
201 |
|
} |
202 |
13655 |
break; |
203 |
202724 |
default: break; |
204 |
|
} |
205 |
|
} |
206 |
|
//--------------------------------- end standard check |
207 |
|
|
208 |
464589 |
TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems) |
209 |
|
{ |
210 |
929178 |
Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node |
211 |
464589 |
<< std::endl; |
212 |
464589 |
Kind k = node.getKind(); |
213 |
464589 |
if (k == kind::HO_APPLY) |
214 |
|
{ |
215 |
284 |
if( !options::ufHo() ){ |
216 |
|
std::stringstream ss; |
217 |
|
ss << "Partial function applications are only supported with " |
218 |
|
"higher-order logic. Try adding the logic prefix HO_."; |
219 |
|
throw LogicException(ss.str()); |
220 |
|
} |
221 |
455 |
Node ret = d_ho->ppRewrite(node); |
222 |
284 |
if (ret != node) |
223 |
|
{ |
224 |
226 |
Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node |
225 |
113 |
<< " to " << ret << std::endl; |
226 |
113 |
return TrustNode::mkTrustRewrite(node, ret, nullptr); |
227 |
|
} |
228 |
|
} |
229 |
464305 |
else if (k == kind::APPLY_UF) |
230 |
|
{ |
231 |
|
// check for higher-order |
232 |
|
// logic exception if higher-order is not enabled |
233 |
86106 |
if (isHigherOrderType(node.getOperator().getType()) && !options::ufHo()) |
234 |
|
{ |
235 |
|
std::stringstream ss; |
236 |
|
ss << "UF received an application whose operator has higher-order type " |
237 |
|
<< node |
238 |
|
<< ", which is only supported with higher-order logic. Try adding the " |
239 |
|
"logic prefix HO_."; |
240 |
|
throw LogicException(ss.str()); |
241 |
|
} |
242 |
|
} |
243 |
464476 |
return TrustNode::null(); |
244 |
|
} |
245 |
|
|
246 |
378658 |
void TheoryUF::preRegisterTerm(TNode node) |
247 |
|
{ |
248 |
378658 |
Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; |
249 |
|
|
250 |
378658 |
if (d_thss != NULL) { |
251 |
45022 |
d_thss->preRegisterTerm(node); |
252 |
|
} |
253 |
|
|
254 |
|
// we always use APPLY_UF if not higher-order, HO_APPLY if higher-order |
255 |
|
//Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() ); |
256 |
378658 |
Assert(node.getKind() != kind::HO_APPLY || options::ufHo()); |
257 |
|
|
258 |
378658 |
Kind k = node.getKind(); |
259 |
378658 |
switch (k) |
260 |
|
{ |
261 |
166216 |
case kind::EQUAL: |
262 |
|
// Add the trigger for equality |
263 |
166216 |
d_equalityEngine->addTriggerPredicate(node); |
264 |
166216 |
break; |
265 |
137556 |
case kind::APPLY_UF: |
266 |
|
case kind::HO_APPLY: |
267 |
|
{ |
268 |
|
// Maybe it's a predicate |
269 |
137556 |
if (node.getType().isBoolean()) |
270 |
|
{ |
271 |
|
// Get triggered for both equal and dis-equal |
272 |
29478 |
d_equalityEngine->addTriggerPredicate(node); |
273 |
|
} |
274 |
|
else |
275 |
|
{ |
276 |
|
// Function applications/predicates |
277 |
108078 |
d_equalityEngine->addTerm(node); |
278 |
|
} |
279 |
|
// Remember the function and predicate terms |
280 |
137556 |
d_functionsTerms.push_back(node); |
281 |
|
} |
282 |
137556 |
break; |
283 |
3755 |
case kind::CARDINALITY_CONSTRAINT: |
284 |
|
case kind::COMBINED_CARDINALITY_CONSTRAINT: |
285 |
|
//do nothing |
286 |
3755 |
break; |
287 |
71131 |
default: |
288 |
|
// Variables etc |
289 |
71131 |
d_equalityEngine->addTerm(node); |
290 |
71131 |
break; |
291 |
|
} |
292 |
378658 |
} |
293 |
|
|
294 |
|
void TheoryUF::explain(TNode literal, Node& exp) |
295 |
|
{ |
296 |
|
Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; |
297 |
|
std::vector<TNode> assumptions; |
298 |
|
// Do the work |
299 |
|
bool polarity = literal.getKind() != kind::NOT; |
300 |
|
TNode atom = polarity ? literal : literal[0]; |
301 |
|
if (atom.getKind() == kind::EQUAL) |
302 |
|
{ |
303 |
|
d_equalityEngine->explainEquality( |
304 |
|
atom[0], atom[1], polarity, assumptions, nullptr); |
305 |
|
} |
306 |
|
else |
307 |
|
{ |
308 |
|
d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr); |
309 |
|
} |
310 |
|
exp = mkAnd(assumptions); |
311 |
|
} |
312 |
|
|
313 |
102830 |
TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); } |
314 |
|
|
315 |
13295 |
bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) |
316 |
|
{ |
317 |
13295 |
if( options::ufHo() ){ |
318 |
|
// must add extensionality disequalities for all pairs of (non-disequal) |
319 |
|
// function equivalence classes. |
320 |
400 |
if (!d_ho->collectModelInfoHo(m, termSet)) |
321 |
|
{ |
322 |
|
Trace("uf") << "Collect model info fail HO" << std::endl; |
323 |
|
return false; |
324 |
|
} |
325 |
|
} |
326 |
|
|
327 |
13295 |
Debug("uf") << "UF : finish collectModelInfo " << std::endl; |
328 |
13295 |
return true; |
329 |
|
} |
330 |
|
|
331 |
15207 |
void TheoryUF::presolve() { |
332 |
|
// TimerStat::CodeTimer codeTimer(d_presolveTimer); |
333 |
|
|
334 |
15207 |
Debug("uf") << "uf: begin presolve()" << endl; |
335 |
15207 |
if(options::ufSymmetryBreaker()) { |
336 |
306 |
vector<Node> newClauses; |
337 |
153 |
d_symb.apply(newClauses); |
338 |
155 |
for(vector<Node>::const_iterator i = newClauses.begin(); |
339 |
155 |
i != newClauses.end(); |
340 |
|
++i) { |
341 |
2 |
Debug("uf") << "uf: generating a lemma: " << *i << std::endl; |
342 |
|
// no proof generator provided |
343 |
2 |
d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY); |
344 |
|
} |
345 |
|
} |
346 |
15207 |
if( d_thss ){ |
347 |
336 |
d_thss->presolve(); |
348 |
|
} |
349 |
15207 |
Debug("uf") << "uf: end presolve()" << endl; |
350 |
15207 |
} |
351 |
|
|
352 |
105243 |
void TheoryUF::ppStaticLearn(TNode n, NodeBuilder& learned) |
353 |
|
{ |
354 |
|
//TimerStat::CodeTimer codeTimer(d_staticLearningTimer); |
355 |
|
|
356 |
210486 |
vector<TNode> workList; |
357 |
105243 |
workList.push_back(n); |
358 |
210486 |
std::unordered_set<TNode> processed; |
359 |
|
|
360 |
4940329 |
while(!workList.empty()) { |
361 |
2417543 |
n = workList.back(); |
362 |
|
|
363 |
2441109 |
if (n.isClosure()) |
364 |
|
{ |
365 |
|
// unsafe to go under quantifiers; we might pull bound vars out of scope! |
366 |
23566 |
processed.insert(n); |
367 |
23566 |
workList.pop_back(); |
368 |
23566 |
continue; |
369 |
|
} |
370 |
|
|
371 |
2393977 |
bool unprocessedChildren = false; |
372 |
7836146 |
for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { |
373 |
5442169 |
if(processed.find(*i) == processed.end()) { |
374 |
|
// unprocessed child |
375 |
1556214 |
workList.push_back(*i); |
376 |
1556214 |
unprocessedChildren = true; |
377 |
|
} |
378 |
|
} |
379 |
|
|
380 |
2393977 |
if(unprocessedChildren) { |
381 |
756086 |
continue; |
382 |
|
} |
383 |
|
|
384 |
1637891 |
workList.pop_back(); |
385 |
|
// has node n been processed in the meantime ? |
386 |
1637891 |
if(processed.find(n) != processed.end()) { |
387 |
19673 |
continue; |
388 |
|
} |
389 |
1618218 |
processed.insert(n); |
390 |
|
|
391 |
|
// == DIAMONDS == |
392 |
|
|
393 |
3236436 |
Debug("diamonds") << "===================== looking at" << endl |
394 |
1618218 |
<< n << endl; |
395 |
|
|
396 |
|
// binary OR of binary ANDs of EQUALities |
397 |
4057452 |
if(n.getKind() == kind::OR && n.getNumChildren() == 2 && |
398 |
2072766 |
n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && |
399 |
1638512 |
n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && |
400 |
1624408 |
(n[0][0].getKind() == kind::EQUAL) && |
401 |
1620870 |
(n[0][1].getKind() == kind::EQUAL) && |
402 |
4857238 |
(n[1][0].getKind() == kind::EQUAL) && |
403 |
1619510 |
(n[1][1].getKind() == kind::EQUAL)) { |
404 |
|
// now we have (a = b && c = d) || (e = f && g = h) |
405 |
|
|
406 |
634 |
Debug("diamonds") << "has form of a diamond!" << endl; |
407 |
|
|
408 |
|
TNode |
409 |
1250 |
a = n[0][0][0], b = n[0][0][1], |
410 |
1250 |
c = n[0][1][0], d = n[0][1][1], |
411 |
1250 |
e = n[1][0][0], f = n[1][0][1], |
412 |
1250 |
g = n[1][1][0], h = n[1][1][1]; |
413 |
|
|
414 |
|
// test that one of {a, b} = one of {c, d}, and make "b" the |
415 |
|
// shared node (i.e. put in the form (a = b && b = d)) |
416 |
|
// note we don't actually care about the shared ones, so the |
417 |
|
// "swaps" below are one-sided, ignoring b and c |
418 |
634 |
if(a == c) { |
419 |
16 |
a = b; |
420 |
618 |
} else if(a == d) { |
421 |
442 |
a = b; |
422 |
442 |
d = c; |
423 |
176 |
} else if(b == c) { |
424 |
|
// nothing to do |
425 |
52 |
} else if(b == d) { |
426 |
20 |
d = c; |
427 |
|
} else { |
428 |
|
// condition not satisfied |
429 |
16 |
Debug("diamonds") << "+ A fails" << endl; |
430 |
16 |
continue; |
431 |
|
} |
432 |
|
|
433 |
618 |
Debug("diamonds") << "+ A holds" << endl; |
434 |
|
|
435 |
|
// same: one of {e, f} = one of {g, h}, and make "f" the |
436 |
|
// shared node (i.e. put in the form (e = f && f = h)) |
437 |
618 |
if(e == g) { |
438 |
16 |
e = f; |
439 |
602 |
} else if(e == h) { |
440 |
454 |
e = f; |
441 |
454 |
h = g; |
442 |
148 |
} else if(f == g) { |
443 |
|
// nothing to do |
444 |
10 |
} else if(f == h) { |
445 |
6 |
h = g; |
446 |
|
} else { |
447 |
|
// condition not satisfied |
448 |
2 |
Debug("diamonds") << "+ B fails" << endl; |
449 |
2 |
continue; |
450 |
|
} |
451 |
|
|
452 |
616 |
Debug("diamonds") << "+ B holds" << endl; |
453 |
|
|
454 |
|
// now we have (a = b && b = d) || (e = f && f = h) |
455 |
|
// test that {a, d} == {e, h} |
456 |
1232 |
if( (a == e && d == h) || |
457 |
|
(a == h && d == e) ) { |
458 |
|
// learn: n implies a == d |
459 |
616 |
Debug("diamonds") << "+ C holds" << endl; |
460 |
1232 |
Node newEquality = a.eqNode(d); |
461 |
616 |
Debug("diamonds") << " ==> " << newEquality << endl; |
462 |
616 |
learned << n.impNode(newEquality); |
463 |
|
} else { |
464 |
|
Debug("diamonds") << "+ C fails" << endl; |
465 |
|
} |
466 |
|
} |
467 |
|
} |
468 |
|
|
469 |
105243 |
if(options::ufSymmetryBreaker()) { |
470 |
24124 |
d_symb.assertFormula(n); |
471 |
|
} |
472 |
105243 |
} /* TheoryUF::ppStaticLearn() */ |
473 |
|
|
474 |
2424 |
EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { |
475 |
|
|
476 |
|
// Check for equality (simplest) |
477 |
2424 |
if (d_equalityEngine->areEqual(a, b)) |
478 |
|
{ |
479 |
|
// The terms are implied to be equal |
480 |
|
return EQUALITY_TRUE; |
481 |
|
} |
482 |
|
|
483 |
|
// Check for disequality |
484 |
2424 |
if (d_equalityEngine->areDisequal(a, b, false)) |
485 |
|
{ |
486 |
|
// The terms are implied to be dis-equal |
487 |
|
return EQUALITY_FALSE; |
488 |
|
} |
489 |
|
|
490 |
|
// All other terms we interpret as dis-equal in the model |
491 |
2424 |
return EQUALITY_FALSE_IN_MODEL; |
492 |
|
} |
493 |
|
|
494 |
1463440 |
bool TheoryUF::areCareDisequal(TNode x, TNode y){ |
495 |
1463440 |
Assert(d_equalityEngine->hasTerm(x)); |
496 |
1463440 |
Assert(d_equalityEngine->hasTerm(y)); |
497 |
4390320 |
if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) |
498 |
4390320 |
&& d_equalityEngine->isTriggerTerm(y, THEORY_UF)) |
499 |
|
{ |
500 |
|
TNode x_shared = |
501 |
1427920 |
d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF); |
502 |
|
TNode y_shared = |
503 |
1427920 |
d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF); |
504 |
1172927 |
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); |
505 |
1172927 |
if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ |
506 |
917934 |
return true; |
507 |
|
} |
508 |
|
} |
509 |
545506 |
return false; |
510 |
|
} |
511 |
|
|
512 |
446324 |
void TheoryUF::addCarePairs(const TNodeTrie* t1, |
513 |
|
const TNodeTrie* t2, |
514 |
|
unsigned arity, |
515 |
|
unsigned depth) |
516 |
|
{ |
517 |
446324 |
if( depth==arity ){ |
518 |
131762 |
if( t2!=NULL ){ |
519 |
263524 |
Node f1 = t1->getData(); |
520 |
263524 |
Node f2 = t2->getData(); |
521 |
131762 |
if (!d_equalityEngine->areEqual(f1, f2)) |
522 |
|
{ |
523 |
121952 |
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; |
524 |
243904 |
vector< pair<TNode, TNode> > currentPairs; |
525 |
332347 |
for (size_t k = 0, nchildren = f1.getNumChildren(); k < nchildren; ++k) |
526 |
|
{ |
527 |
420790 |
TNode x = f1[k]; |
528 |
420790 |
TNode y = f2[k]; |
529 |
210395 |
Assert(d_equalityEngine->hasTerm(x)); |
530 |
210395 |
Assert(d_equalityEngine->hasTerm(y)); |
531 |
210395 |
Assert(!d_equalityEngine->areDisequal(x, y, false)); |
532 |
210395 |
Assert(!areCareDisequal(x, y)); |
533 |
210395 |
if (!d_equalityEngine->areEqual(x, y)) |
534 |
|
{ |
535 |
389997 |
if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) |
536 |
389997 |
&& d_equalityEngine->isTriggerTerm(y, THEORY_UF)) |
537 |
|
{ |
538 |
|
TNode x_shared = |
539 |
86522 |
d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF); |
540 |
|
TNode y_shared = |
541 |
86522 |
d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF); |
542 |
43261 |
currentPairs.push_back(make_pair(x_shared, y_shared)); |
543 |
|
} |
544 |
|
} |
545 |
|
} |
546 |
165213 |
for (unsigned c = 0; c < currentPairs.size(); ++ c) { |
547 |
43261 |
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl; |
548 |
43261 |
addCarePair(currentPairs[c].first, currentPairs[c].second); |
549 |
|
} |
550 |
|
} |
551 |
|
} |
552 |
|
}else{ |
553 |
314562 |
if( t2==NULL ){ |
554 |
111213 |
if( depth<(arity-1) ){ |
555 |
|
//add care pairs internal to each child |
556 |
131598 |
for (const std::pair<const TNode, TNodeTrie>& tt : t1->d_data) |
557 |
|
{ |
558 |
75750 |
addCarePairs(&tt.second, NULL, arity, depth + 1); |
559 |
|
} |
560 |
|
} |
561 |
|
//add care pairs based on each pair of non-disequal arguments |
562 |
541127 |
for (std::map<TNode, TNodeTrie>::const_iterator it = t1->d_data.begin(); |
563 |
541127 |
it != t1->d_data.end(); |
564 |
|
++it) |
565 |
|
{ |
566 |
429914 |
std::map<TNode, TNodeTrie>::const_iterator it2 = it; |
567 |
429914 |
++it2; |
568 |
5637446 |
for( ; it2 != t1->d_data.end(); ++it2 ){ |
569 |
2603766 |
if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) |
570 |
|
{ |
571 |
943500 |
if( !areCareDisequal(it->first, it2->first) ){ |
572 |
243690 |
addCarePairs( &it->second, &it2->second, arity, depth+1 ); |
573 |
|
} |
574 |
|
} |
575 |
|
} |
576 |
|
} |
577 |
|
}else{ |
578 |
|
//add care pairs based on product of indices, non-disequal arguments |
579 |
505824 |
for (const std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data) |
580 |
|
{ |
581 |
624550 |
for (const std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data) |
582 |
|
{ |
583 |
322075 |
if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) |
584 |
|
{ |
585 |
309545 |
if (!areCareDisequal(tt1.first, tt2.first)) |
586 |
|
{ |
587 |
91421 |
addCarePairs(&tt1.second, &tt2.second, arity, depth + 1); |
588 |
|
} |
589 |
|
} |
590 |
|
} |
591 |
|
} |
592 |
|
} |
593 |
|
} |
594 |
446324 |
} |
595 |
|
|
596 |
24001 |
void TheoryUF::computeCareGraph() { |
597 |
24001 |
if (d_sharedTerms.empty()) |
598 |
|
{ |
599 |
8242 |
return; |
600 |
|
} |
601 |
|
// Use term indexing. We build separate indices for APPLY_UF and HO_APPLY. |
602 |
|
// We maintain indices per operator for the former, and indices per |
603 |
|
// function type for the latter. |
604 |
31518 |
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." |
605 |
15759 |
<< std::endl; |
606 |
31518 |
std::map<Node, TNodeTrie> index; |
607 |
31518 |
std::map<TypeNode, TNodeTrie> hoIndex; |
608 |
31518 |
std::map<Node, size_t> arity; |
609 |
443185 |
for (TNode app : d_functionsTerms) |
610 |
|
{ |
611 |
854852 |
std::vector<TNode> reps; |
612 |
427426 |
bool has_trigger_arg = false; |
613 |
1002876 |
for (const Node& j : app) |
614 |
|
{ |
615 |
575450 |
reps.push_back(d_equalityEngine->getRepresentative(j)); |
616 |
575450 |
if (d_equalityEngine->isTriggerTerm(j, THEORY_UF)) |
617 |
|
{ |
618 |
502854 |
has_trigger_arg = true; |
619 |
|
} |
620 |
|
} |
621 |
427426 |
if (has_trigger_arg) |
622 |
|
{ |
623 |
386244 |
if (app.getKind() == kind::APPLY_UF) |
624 |
|
{ |
625 |
772424 |
Node op = app.getOperator(); |
626 |
386212 |
index[op].addTerm(app, reps); |
627 |
386212 |
arity[op] = reps.size(); |
628 |
|
} |
629 |
|
else |
630 |
|
{ |
631 |
32 |
Assert(app.getKind() == kind::HO_APPLY); |
632 |
|
// add it to the hoIndex for the function type |
633 |
32 |
hoIndex[app[0].getType()].addTerm(app, reps); |
634 |
|
} |
635 |
|
} |
636 |
|
} |
637 |
|
// for each index |
638 |
51212 |
for (std::pair<const Node, TNodeTrie>& tt : index) |
639 |
|
{ |
640 |
70906 |
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " |
641 |
35453 |
<< tt.first << "..." << std::endl; |
642 |
35453 |
Assert(arity.find(tt.first) != arity.end()); |
643 |
35453 |
addCarePairs(&tt.second, nullptr, arity[tt.first], 0); |
644 |
|
} |
645 |
15769 |
for (std::pair<const TypeNode, TNodeTrie>& tt : hoIndex) |
646 |
|
{ |
647 |
20 |
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index " |
648 |
10 |
<< tt.first << "..." << std::endl; |
649 |
|
// the arity of HO_APPLY is always two |
650 |
10 |
addCarePairs(&tt.second, nullptr, 2, 0); |
651 |
|
} |
652 |
31518 |
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." |
653 |
15759 |
<< std::endl; |
654 |
|
}/* TheoryUF::computeCareGraph() */ |
655 |
|
|
656 |
271431 |
void TheoryUF::eqNotifyNewClass(TNode t) { |
657 |
271431 |
if (d_thss != NULL) { |
658 |
52824 |
d_thss->newEqClass(t); |
659 |
|
} |
660 |
271431 |
} |
661 |
|
|
662 |
4579057 |
void TheoryUF::eqNotifyMerge(TNode t1, TNode t2) |
663 |
|
{ |
664 |
4579057 |
if (d_thss != NULL) { |
665 |
282277 |
d_thss->merge(t1, t2); |
666 |
|
} |
667 |
4579057 |
} |
668 |
|
|
669 |
893113 |
void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { |
670 |
893113 |
if (d_thss != NULL) { |
671 |
21042 |
d_thss->assertDisequal(t1, t2, reason); |
672 |
|
} |
673 |
893113 |
} |
674 |
|
|
675 |
86106 |
bool TheoryUF::isHigherOrderType(TypeNode tn) |
676 |
|
{ |
677 |
86106 |
Assert(tn.isFunction()); |
678 |
86106 |
std::map<TypeNode, bool>::iterator it = d_isHoType.find(tn); |
679 |
86106 |
if (it != d_isHoType.end()) |
680 |
|
{ |
681 |
81167 |
return it->second; |
682 |
|
} |
683 |
4939 |
bool ret = false; |
684 |
9878 |
const std::vector<TypeNode>& argTypes = tn.getArgTypes(); |
685 |
14161 |
for (const TypeNode& tnc : argTypes) |
686 |
|
{ |
687 |
9290 |
if (tnc.isFunction()) |
688 |
|
{ |
689 |
68 |
ret = true; |
690 |
68 |
break; |
691 |
|
} |
692 |
|
} |
693 |
4939 |
d_isHoType[tn] = ret; |
694 |
4939 |
return ret; |
695 |
|
} |
696 |
|
|
697 |
|
} // namespace uf |
698 |
|
} // namespace theory |
699 |
29358 |
} // namespace cvc5 |