Branch data Line data Source code
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-2025 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 : : * The theory of uninterpreted functions (UF)
14 : : */
15 : :
16 : : #include "theory/uf/theory_uf.h"
17 : :
18 : : #include <memory>
19 : : #include <sstream>
20 : :
21 : : #include "expr/node_algorithm.h"
22 : : #include "expr/skolem_manager.h"
23 : : #include "options/quantifiers_options.h"
24 : : #include "options/smt_options.h"
25 : : #include "options/theory_options.h"
26 : : #include "options/uf_options.h"
27 : : #include "proof/proof_node_manager.h"
28 : : #include "smt/logic_exception.h"
29 : : #include "theory/arith/arith_utilities.h"
30 : : #include "theory/theory_model.h"
31 : : #include "theory/type_enumerator.h"
32 : : #include "theory/uf/cardinality_extension.h"
33 : : #include "theory/uf/conversions_solver.h"
34 : : #include "theory/uf/ho_extension.h"
35 : : #include "theory/uf/lambda_lift.h"
36 : : #include "theory/uf/theory_uf_rewriter.h"
37 : :
38 : : using namespace std;
39 : :
40 : : namespace cvc5::internal {
41 : : namespace theory {
42 : : namespace uf {
43 : :
44 : : /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
45 : 50994 : TheoryUF::TheoryUF(Env& env,
46 : : OutputChannel& out,
47 : : Valuation valuation,
48 : 50994 : std::string instanceName)
49 : : : Theory(THEORY_UF, env, out, valuation, instanceName),
50 : : d_thss(nullptr),
51 : 50994 : d_lambdaLift(new LambdaLift(env)),
52 : : d_ho(nullptr),
53 : : d_dpfgen(env),
54 : : d_functionsTerms(context()),
55 : : d_symb(env, instanceName),
56 : : d_rewriter(nodeManager()),
57 : : d_checker(nodeManager()),
58 : : d_state(env, valuation),
59 : 50994 : d_im(env, *this, d_state, "theory::uf::" + instanceName, false),
60 : 50994 : d_notify(d_im, *this),
61 : 152982 : d_cpacb(*this)
62 : : {
63 : 50994 : d_true = nodeManager()->mkConst(true);
64 : : // indicate we are using the default theory state and inference managers
65 : 50994 : d_theoryState = &d_state;
66 : 50994 : d_inferManager = &d_im;
67 : 50994 : }
68 : :
69 : 101476 : TheoryUF::~TheoryUF() {
70 : 101476 : }
71 : :
72 : 50994 : TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
73 : :
74 : 20129 : ProofRuleChecker* TheoryUF::getProofChecker() { return &d_checker; }
75 : :
76 : 50994 : bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
77 : : {
78 : 50994 : esi.d_notify = &d_notify;
79 : 50994 : esi.d_name = d_instanceName + "theory::uf::ee";
80 : 50994 : if (options().quantifiers.finiteModelFind
81 [ + + ][ + - ]: 50994 : && options().uf.ufssMode != options::UfssMode::NONE)
[ + + ]
82 : : {
83 : : // need notifications about sorts
84 : 722 : esi.d_notifyNewClass = true;
85 : 722 : esi.d_notifyMerge = true;
86 : 722 : esi.d_notifyDisequal = true;
87 : : }
88 : 50994 : return true;
89 : : }
90 : :
91 : 50994 : void TheoryUF::finishInit() {
92 [ - + ][ - + ]: 50994 : Assert(d_equalityEngine != nullptr);
[ - - ]
93 : : // combined cardinality constraints are not evaluated in getModelValue
94 : 50994 : d_valuation.setUnevaluatedKind(Kind::COMBINED_CARDINALITY_CONSTRAINT);
95 [ + + ]: 50994 : if (logicInfo().hasCardinalityConstraints())
96 : : {
97 [ - + ]: 44 : if (!options().uf.ufCardExp)
98 : : {
99 : 0 : std::stringstream ss;
100 : : ss << "Logic with cardinality constraints not available in this "
101 : 0 : "configuration, try --uf-card-exp.";
102 : 0 : throw LogicException(ss.str());
103 : : }
104 : : }
105 : : // Initialize the cardinality constraints solver if the logic includes UF,
106 : : // finite model finding is enabled, and it is not disabled by
107 : : // the ufssMode option.
108 : 50994 : if (options().quantifiers.finiteModelFind
109 [ + + ][ + - ]: 50994 : && options().uf.ufssMode != options::UfssMode::NONE)
[ + + ]
110 : : {
111 : 722 : d_thss.reset(new CardinalityExtension(d_env, d_state, d_im, this));
112 : : }
113 : : // The kinds we are treating as function application in congruence
114 : 50994 : bool isHo = logicInfo().isHigherOrder();
115 : 50994 : d_equalityEngine->addFunctionKind(Kind::APPLY_UF, false, isHo);
116 [ + + ]: 50994 : if (isHo)
117 : : {
118 [ - + ]: 1160 : if (!options().uf.ufHoExp)
119 : : {
120 : 0 : std::stringstream ss;
121 : : ss << "Higher-order logic not available in this configuration, try "
122 : 0 : "--uf-ho-exp.";
123 : 0 : throw LogicException(ss.str());
124 : : }
125 : 1160 : d_equalityEngine->addFunctionKind(Kind::HO_APPLY);
126 : 1160 : d_ho.reset(new HoExtension(d_env, d_state, d_im, *d_lambdaLift.get()));
127 : : }
128 : : // conversion kinds
129 : 50994 : d_equalityEngine->addFunctionKind(Kind::INT_TO_BITVECTOR, true);
130 : 50994 : d_equalityEngine->addFunctionKind(Kind::BITVECTOR_TO_NAT, true);
131 : 50994 : }
132 : :
133 : : //--------------------------------- standard check
134 : :
135 : 49173 : bool TheoryUF::needsCheckLastEffort()
136 : : {
137 : : // last call effort needed if using finite model finding or
138 : : // arithmetic/bit-vector conversions
139 [ + + ][ + + ]: 49173 : return d_thss != nullptr || d_csolver != nullptr;
140 : : }
141 : :
142 : 2505180 : void TheoryUF::postCheck(Effort level)
143 : : {
144 [ + + ]: 2505180 : if (d_state.isInConflict())
145 : : {
146 : 123635 : return;
147 : : }
148 : : // check with the cardinality constraints extension
149 [ + + ]: 2381540 : if (d_thss != nullptr)
150 : : {
151 : 119117 : d_thss->check(level);
152 : : }
153 [ + - ]: 2381540 : if (!d_state.isInConflict())
154 : : {
155 : : // check with conversions solver at last call effort
156 [ + + ][ + + ]: 2381540 : if (d_csolver != nullptr && level == Effort::EFFORT_LAST_CALL)
[ + + ]
157 : : {
158 : 76 : d_csolver->check();
159 : : }
160 : : // check with the higher-order extension at full effort
161 [ + + ][ + + ]: 2381540 : if (fullEffort(level) && logicInfo().isHigherOrder())
[ + + ]
162 : : {
163 : 5213 : d_ho->check();
164 : : }
165 : : }
166 : : }
167 : :
168 : 6760200 : void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
169 : : {
170 [ + + ]: 6760200 : if (d_state.isInConflict())
171 : : {
172 : 122365 : return;
173 : : }
174 [ + + ]: 6637840 : if (d_thss != nullptr)
175 : : {
176 : : bool isDecision =
177 : 246321 : d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
178 : 246321 : d_thss->assertNode(fact, isDecision);
179 : : }
180 [ + + ][ + ]: 6637840 : switch (atom.getKind())
181 : : {
182 : 6184530 : case Kind::EQUAL:
183 : : {
184 [ + + ][ + - ]: 6184530 : if (logicInfo().isHigherOrder() && options().uf.ufHoExt)
[ + + ]
185 : : {
186 : 99994 : if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
187 : : {
188 : : // apply extensionality eagerly using the ho extension
189 : 15469 : d_ho->applyExtensionality(fact);
190 : : }
191 : : }
192 : : }
193 : 6184530 : break;
194 : 20972 : case Kind::CARDINALITY_CONSTRAINT:
195 : : case Kind::COMBINED_CARDINALITY_CONSTRAINT:
196 : : {
197 [ - + ]: 20972 : if (d_thss == nullptr)
198 : : {
199 [ - - ]: 0 : if (!logicInfo().hasCardinalityConstraints())
200 : : {
201 : 0 : std::stringstream ss;
202 : 0 : ss << "Cardinality constraint " << atom
203 : 0 : << " was asserted, but the logic does not allow it." << std::endl;
204 : 0 : ss << "Try using a logic containing \"UFC\"." << std::endl;
205 : 0 : throw Exception(ss.str());
206 : : }
207 : : else
208 : : {
209 : : // support for cardinality constraints is not enabled, set incomplete
210 : 0 : d_im.setModelUnsound(IncompleteId::UF_CARD_DISABLED);
211 : : }
212 : : }
213 : : }
214 : 20972 : break;
215 : 432337 : default: break;
216 : : }
217 : : }
218 : : //--------------------------------- end standard check
219 : :
220 : 391469 : TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
221 : : {
222 [ + - ]: 782938 : Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
223 : 391469 : << std::endl;
224 : 391469 : Kind k = node.getKind();
225 : 391469 : bool isHol = logicInfo().isHigherOrder();
226 [ - + ]: 391469 : if (node.getType().isAbstract())
227 : : {
228 : 0 : std::stringstream ss;
229 : 0 : ss << "Cannot process term of abstract type " << node;
230 : 0 : throw LogicException(ss.str());
231 : : }
232 [ + + ][ + + ]: 391469 : if (k == Kind::HO_APPLY || node.getType().isFunction())
[ + + ][ + + ]
[ - - ]
233 : : {
234 [ + + ]: 5357 : if (!isHol)
235 : : {
236 : 2 : std::stringstream ss;
237 [ - + ]: 1 : if (k == Kind::HO_APPLY)
238 : : {
239 : 0 : ss << "Higher-order function applications";
240 : : }
241 : : else
242 : : {
243 : 1 : ss << "Function terms";
244 : : }
245 : : ss << " are only supported with "
246 : 1 : "higher-order logic. Try adding the logic prefix HO_.";
247 : 1 : throw LogicException(ss.str());
248 : : }
249 : : }
250 [ + + ]: 386112 : else if (k == Kind::APPLY_UF)
251 : : {
252 : 264506 : if (!isHol && isHigherOrderType(node.getOperator().getType()))
253 : : {
254 : : // check for higher-order
255 : : // logic exception if higher-order is not enabled
256 : 0 : std::stringstream ss;
257 : 0 : ss << "UF received an application whose operator has higher-order type "
258 : 0 : << node
259 : : << ", which is only supported with higher-order logic. Try adding "
260 : 0 : "the logic prefix HO_.";
261 : 0 : throw LogicException(ss.str());
262 : : }
263 : : }
264 [ + + ]: 121522 : else if ((k == Kind::BITVECTOR_TO_NAT || k == Kind::INT_TO_BITVECTOR)
265 [ + + ][ + + ]: 243128 : && options().uf.eagerArithBvConv)
[ + + ]
266 : : {
267 : : // eliminate if option specifies to eliminate eagerly
268 : : Node ret = k == Kind::BITVECTOR_TO_NAT ? arith::eliminateBv2Nat(node)
269 : 16 : : arith::eliminateInt2Bv(node);
270 : 16 : return TrustNode::mkTrustRewrite(node, ret);
271 : : }
272 [ + + ]: 391452 : if (isHol)
273 : : {
274 : 40831 : TrustNode ret = d_ho->ppRewrite(node, lems);
275 [ + + ]: 40831 : if (!ret.isNull())
276 : : {
277 [ + - ]: 4772 : Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node
278 [ - + ][ - - ]: 2386 : << " to " << ret.getNode() << std::endl;
279 : 2386 : return ret;
280 : : }
281 : : }
282 : 389066 : return TrustNode::null();
283 : : }
284 : :
285 : 1066330 : void TheoryUF::preRegisterTerm(TNode node)
286 : : {
287 [ + - ]: 1066330 : Trace("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
288 : :
289 [ + + ]: 1066330 : if (d_thss != nullptr)
290 : : {
291 : 59226 : d_thss->preRegisterTerm(node);
292 : : }
293 : :
294 : 1066330 : Kind k = node.getKind();
295 [ + + ][ + + ]: 1066330 : switch (k)
[ + - ][ + ]
296 : : {
297 : 419982 : case Kind::EQUAL:
298 : : // Add the trigger for equality
299 : 419982 : d_state.addEqualityEngineTriggerPredicate(node);
300 : 419982 : break;
301 : 376911 : case Kind::APPLY_UF: preRegisterFunctionTerm(node); break;
302 : 768 : case Kind::HO_APPLY:
303 : : {
304 [ - + ]: 768 : if (!logicInfo().isHigherOrder())
305 : : {
306 : 0 : std::stringstream ss;
307 : : ss << "Partial function applications are only supported with "
308 : 0 : "higher-order logic. Try adding the logic prefix HO_.";
309 : 0 : throw LogicException(ss.str());
310 : : }
311 : 768 : preRegisterFunctionTerm(node);
312 : : }
313 : 768 : break;
314 : 83 : case Kind::INT_TO_BITVECTOR:
315 : : case Kind::BITVECTOR_TO_NAT:
316 : : {
317 [ - + ][ - + ]: 83 : Assert(!options().uf.eagerArithBvConv);
[ - - ]
318 : 83 : d_equalityEngine->addTerm(node);
319 : 83 : d_functionsTerms.push_back(node);
320 : : // initialize the conversions solver if not already done so
321 [ + + ]: 83 : if (d_csolver == nullptr)
322 : : {
323 : 45 : d_csolver.reset(new ConversionsSolver(d_env, d_state, d_im));
324 : : }
325 : : // call preregister
326 : 83 : d_csolver->preRegisterTerm(node);
327 : : }
328 : 83 : break;
329 : 5647 : case Kind::CARDINALITY_CONSTRAINT:
330 : : case Kind::COMBINED_CARDINALITY_CONSTRAINT:
331 : : // do nothing
332 : 5647 : break;
333 : 0 : case Kind::UNINTERPRETED_SORT_VALUE:
334 : : {
335 : : // Uninterpreted sort values should only appear in models, and should
336 : : // never appear in constraints. They are unallowed to ever appear in
337 : : // constraints since the cardinality of an uninterpreted sort may have an
338 : : // upper bound, e.g. if (forall ((x U) (y U)) (= x y)) holds, then @uc_U_2
339 : : // is a ill-formed term, as its existence cannot be assumed. The parser
340 : : // prevents the user from ever constructing uninterpreted sort values.
341 : : // However, they may be exported via models to API users. It is thus
342 : : // possible that these uninterpreted sort values are asserted back in
343 : : // constraints, hence this check is necessary.
344 : : throw LogicException(
345 : 0 : "An uninterpreted constant was preregistered to the UF theory.");
346 : : }
347 : : break;
348 : 262936 : default:
349 : : // Variables etc
350 : 262936 : d_equalityEngine->addTerm(node);
351 [ + + ]: 262936 : if (logicInfo().isHigherOrder())
352 : : {
353 : : // When using lazy lambda handling, if node is a lambda function, it must
354 : : // be marked as a shared term. This is to ensure we split on the equality
355 : : // of lambda functions with other functions when doing care graph
356 : : // based theory combination.
357 [ + + ]: 15877 : if (d_lambdaLift->isLambdaFunction(node))
358 : : {
359 : 637 : addSharedTerm(node);
360 : : }
361 : : }
362 [ - + ]: 247059 : else if (node.getType().isFunction())
363 : : {
364 : 0 : std::stringstream ss;
365 : : ss << "Function terms are only supported with higher-order logic. Try "
366 : 0 : "adding the logic prefix HO_.";
367 : 0 : throw LogicException(ss.str());
368 : : }
369 : 262936 : break;
370 : : }
371 : :
372 : 1066330 : }
373 : :
374 : 377679 : void TheoryUF::preRegisterFunctionTerm(TNode node)
375 : : {
376 : : // Maybe it's a predicate
377 [ + + ]: 377679 : if (node.getType().isBoolean())
378 : : {
379 : 115081 : d_state.addEqualityEngineTriggerPredicate(node);
380 : : }
381 : : else
382 : : {
383 : : // Function applications/predicates
384 : 262598 : d_equalityEngine->addTerm(node);
385 : : }
386 : : // Remember the function and predicate terms
387 : 377679 : d_functionsTerms.push_back(node);
388 : 377679 : }
389 : :
390 : 0 : void TheoryUF::explain(TNode literal, Node& exp)
391 : : {
392 [ - - ]: 0 : Trace("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
393 : 0 : std::vector<TNode> assumptions;
394 : : // Do the work
395 : 0 : bool polarity = literal.getKind() != Kind::NOT;
396 [ - - ]: 0 : TNode atom = polarity ? literal : literal[0];
397 [ - - ]: 0 : if (atom.getKind() == Kind::EQUAL)
398 : : {
399 : 0 : d_equalityEngine->explainEquality(
400 : : atom[0], atom[1], polarity, assumptions, nullptr);
401 : : }
402 : : else
403 : : {
404 : 0 : d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
405 : : }
406 : 0 : exp = nodeManager()->mkAnd(assumptions);
407 : 0 : }
408 : :
409 : 206695 : TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
410 : :
411 : 30459 : bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
412 : : {
413 [ + + ]: 30459 : if (logicInfo().isHigherOrder())
414 : : {
415 : : // must add extensionality disequalities for all pairs of (non-disequal)
416 : : // function equivalence classes.
417 [ + + ]: 866 : if (!d_ho->collectModelInfoHo(m, termSet))
418 : : {
419 [ + - ]: 8 : Trace("uf") << "Collect model info fail HO" << std::endl;
420 : 8 : return false;
421 : : }
422 : : }
423 : :
424 [ + - ]: 30451 : Trace("uf") << "UF : finish collectModelInfo " << std::endl;
425 : 30451 : return true;
426 : : }
427 : :
428 : 50981 : void TheoryUF::presolve() {
429 : : // TimerStat::CodeTimer codeTimer(d_presolveTimer);
430 : :
431 [ + - ]: 50981 : Trace("uf") << "uf: begin presolve()" << endl;
432 [ + + ]: 50981 : if (options().uf.ufSymmetryBreaker)
433 : : {
434 : 716 : vector<Node> newClauses;
435 : 358 : d_symb.apply(newClauses);
436 : 418 : for(vector<Node>::const_iterator i = newClauses.begin();
437 [ + + ]: 418 : i != newClauses.end();
438 : 60 : ++i) {
439 [ + - ]: 60 : Trace("uf") << "uf: generating a lemma: " << *i << std::endl;
440 : : // no proof generator provided
441 : 60 : d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY);
442 : : }
443 : : }
444 [ + + ]: 50981 : if( d_thss ){
445 : 735 : d_thss->presolve();
446 : : }
447 [ + - ]: 50981 : Trace("uf") << "uf: end presolve()" << endl;
448 : 50981 : }
449 : :
450 : 455813 : void TheoryUF::ppStaticLearn(TNode n, std::vector<TrustNode>& learned)
451 : : {
452 : : //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
453 : :
454 : : // Use the diamonds utility
455 : 455813 : d_dpfgen.ppStaticLearn(n, learned);
456 : :
457 [ + + ]: 455813 : if (options().uf.ufSymmetryBreaker)
458 : : {
459 : 54550 : d_symb.assertFormula(n);
460 : : }
461 : 455813 : } /* TheoryUF::ppStaticLearn() */
462 : :
463 : 7990 : EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
464 : :
465 : : // Check for equality (simplest)
466 [ + + ]: 7990 : if (d_equalityEngine->areEqual(a, b))
467 : : {
468 : : // The terms are implied to be equal
469 : 2016 : return EQUALITY_TRUE;
470 : : }
471 : :
472 : : // Check for disequality
473 [ - + ]: 5974 : if (d_equalityEngine->areDisequal(a, b, false))
474 : : {
475 : : // The terms are implied to be dis-equal
476 : 0 : return EQUALITY_FALSE;
477 : : }
478 : :
479 : : // All other terms we interpret as dis-equal in the model
480 : 5974 : return EQUALITY_FALSE_IN_MODEL;
481 : : }
482 : :
483 : 2639130 : bool TheoryUF::areCareDisequal(TNode x, TNode y)
484 : : {
485 : : // check for disequality first, as an optimization
486 : 5278190 : if (d_equalityEngine->hasTerm(x) && d_equalityEngine->hasTerm(y)
487 : 5278190 : && d_equalityEngine->areDisequal(x, y, false))
488 : : {
489 : 106704 : return true;
490 : : }
491 [ + + ][ - - ]: 2532420 : if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
492 [ + + ][ + + ]: 2532420 : && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
[ + + ][ + - ]
[ - - ]
493 : : {
494 : : TNode x_shared =
495 : 2116940 : d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
496 : : TNode y_shared =
497 : 2116940 : d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
498 : 2116940 : EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
499 [ + - ][ - + ]: 2116940 : if (eqStatus == EQUALITY_FALSE || eqStatus == EQUALITY_FALSE_AND_PROPAGATED)
500 : : {
501 : 0 : return true;
502 : : }
503 [ + + ]: 2116940 : else if (eqStatus == EQUALITY_FALSE_IN_MODEL)
504 : : {
505 : : // if x or y is a lambda function, and they are neither entailed to
506 : : // be equal or disequal, then we return false. This ensures the pair
507 : : // (x,y) may be considered for the care graph.
508 [ + + ][ - - ]: 3938490 : if (d_lambdaLift->isLambdaFunction(x)
509 [ + + ][ + + ]: 3938490 : || d_lambdaLift->isLambdaFunction(y))
[ + + ][ + - ]
[ - - ]
510 : : {
511 : 1308 : return false;
512 : : }
513 : 1967940 : return true;
514 : : }
515 : : }
516 : 563182 : return false;
517 : : }
518 : :
519 : 354787 : void TheoryUF::processCarePairArgs(TNode a, TNode b)
520 : : {
521 : : // if a and b are already equal, we ignore this pair
522 [ + + ]: 354787 : if (d_state.areEqual(a, b))
523 : : {
524 : 37459 : return;
525 : : }
526 : : // otherwise, we add pairs for each of their arguments
527 : 317328 : addCarePairArgs(a, b);
528 : :
529 : : // also split on functions
530 [ + + ]: 317328 : if (logicInfo().isHigherOrder())
531 : : {
532 : 72264 : NodeManager* nm = nodeManager();
533 [ + + ]: 215674 : for (size_t k = 0, nchild = a.getNumChildren(); k < nchild; ++k)
534 : : {
535 : 143410 : TNode x = a[k];
536 : 143410 : TNode y = b[k];
537 [ + + ]: 143410 : if (d_state.areEqual(x, y))
538 : : {
539 : 104364 : continue;
540 : : }
541 : : // Splitting on functions. This is required since conceptually the HO
542 : : // extension should be considered a separate entity with regards to
543 : : // theory combination (in particular, with the core UF solver). This is
544 : : // similar to how we handle sets of sets, where each set type is
545 : : // considered a separate entity. The types below must be equal to handle
546 : : // polymorphic operators taking higher-order arguments, e.g. set.map.
547 : 78092 : TypeNode xt = x.getType();
548 [ + + ][ + - ]: 39046 : if (xt.isFunction() && xt==y.getType())
[ + + ][ + + ]
[ - - ]
549 : : {
550 : 9998 : Node lemma = x.eqNode(y);
551 : 9998 : lemma = nm->mkNode(Kind::OR, lemma, lemma.notNode());
552 : 9998 : d_im.lemma(lemma, InferenceId::UF_HO_CG_SPLIT);
553 : : }
554 : : }
555 : : }
556 : : }
557 : :
558 : 67101 : void TheoryUF::computeCareGraph() {
559 [ + + ]: 67101 : if (d_state.getSharedTerms().empty())
560 : : {
561 : 26421 : return;
562 : : }
563 : 40680 : NodeManager* nm = nodeManager();
564 : : // Use term indexing. We build separate indices for APPLY_UF and HO_APPLY.
565 : : // We maintain indices per operator for the former, and indices per
566 : : // function type for the latter.
567 [ + - ]: 81360 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..."
568 : 40680 : << std::endl;
569 : 40680 : bool isHigherOrder = logicInfo().isHigherOrder();
570 : : // temporary keep set for higher-order indexing below
571 : 81360 : std::vector<Node> keep;
572 : 81360 : std::map<Node, TNodeTrie> index;
573 : 81360 : std::map<TypeNode, TNodeTrie> typeIndex;
574 : 40680 : std::map<Node, size_t> arity;
575 [ + + ]: 896278 : for (TNode app : d_functionsTerms)
576 : : {
577 : 1711200 : std::vector<TNode> reps;
578 : 855598 : bool has_trigger_arg = false;
579 [ + + ]: 1913630 : for (const Node& j : app)
580 : : {
581 : 1058030 : reps.push_back(d_equalityEngine->getRepresentative(j));
582 : : // if doing higher-order, higher-order arguments must all be considered as
583 : : // well
584 [ + + ][ - - ]: 1058030 : if (d_equalityEngine->isTriggerTerm(j, THEORY_UF)
585 [ + + ][ + + ]: 1058030 : || (isHigherOrder && j.getType().isFunction()))
[ + + ][ + + ]
[ + - ][ - - ]
586 : : {
587 : 874508 : has_trigger_arg = true;
588 : : }
589 : : }
590 [ + + ]: 855598 : if (has_trigger_arg)
591 : : {
592 [ + - ]: 1508700 : Trace("uf::sharing-terms")
593 : 754352 : << "...add: " << app << " / " << reps << std::endl;
594 : 754352 : Kind k = app.getKind();
595 [ + + ]: 754352 : if (k == Kind::APPLY_UF)
596 : : {
597 : 1506840 : Node op = app.getOperator();
598 : 753419 : index[op].addTerm(app, reps);
599 : 753419 : arity[op] = reps.size();
600 [ + + ][ + - ]: 753419 : if (isHigherOrder && d_equalityEngine->hasTerm(op))
[ + + ][ + + ]
[ - - ]
601 : : {
602 : : // Since we use a lazy app-completion scheme for equating fully
603 : : // and partially applied versions of terms, we must add all
604 : : // sub-chains to the HO index if the operator of this term occurs
605 : : // in a higher-order context in the equality engine. In other words,
606 : : // for (f a b c), this will add the terms:
607 : : // (HO_APPLY f a), (HO_APPLY (HO_APPLY f a) b),
608 : : // (HO_APPLY (HO_APPLY (HO_APPLY f a) b) c) to the higher-order
609 : : // term index for consideration when computing care pairs.
610 : 17432 : Node curr = op;
611 [ + + ]: 20258 : for (const Node& c : app)
612 : : {
613 : 34626 : Node happ = nm->mkNode(Kind::HO_APPLY, curr, c);
614 [ - + ][ - + ]: 11542 : Assert(curr.getType().isFunction());
[ - - ]
615 [ + + ][ - - ]: 34626 : typeIndex[curr.getType()].addTerm(happ, {curr, c});
616 : 11542 : curr = happ;
617 : 11542 : keep.push_back(happ);
618 : : }
619 : : }
620 : : }
621 [ + + ][ + + ]: 933 : else if (k == Kind::HO_APPLY || k == Kind::BITVECTOR_TO_NAT)
622 : : {
623 : : // add it to the typeIndex for the function type if HO_APPLY, or the
624 : : // bitvector type if bv2nat. The latter ensures that we compute
625 : : // care pairs based on bv2nat only for bitvectors of the same width.
626 : 805 : typeIndex[app[0].getType()].addTerm(app, reps);
627 : : }
628 : : else
629 : : {
630 : : // case for other operators, e.g. int2bv
631 : 128 : Node op = app.getOperator();
632 : 128 : index[op].addTerm(app, reps);
633 : 128 : arity[op] = reps.size();
634 : : }
635 : : }
636 : : }
637 : : // for each index
638 [ + + ]: 110685 : for (std::pair<const Node, TNodeTrie>& tt : index)
639 : : {
640 [ + - ]: 140010 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
641 : 70005 : << tt.first << "..." << std::endl;
642 [ - + ][ - + ]: 70005 : Assert(arity.find(tt.first) != arity.end());
[ - - ]
643 : 70005 : nodeTriePathPairProcess(&tt.second, arity[tt.first], d_cpacb);
644 : : }
645 [ + + ]: 42589 : for (std::pair<const TypeNode, TNodeTrie>& tt : typeIndex)
646 : : {
647 : : // functions for HO_APPLY which has arity 2, bitvectors for bv2nat which
648 : : // has arity one
649 [ + + ]: 1909 : size_t a = tt.first.isFunction() ? 2 : 1;
650 [ + - ]: 3818 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index "
651 : 1909 : << tt.first << "..." << std::endl;
652 : : // the arity of HO_APPLY is always two
653 : 1909 : nodeTriePathPairProcess(&tt.second, a, d_cpacb);
654 : : }
655 [ + - ]: 81360 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): finished."
656 : 40680 : << std::endl;
657 : : }/* TheoryUF::computeCareGraph() */
658 : :
659 : 779544 : void TheoryUF::eqNotifyNewClass(TNode t) {
660 [ + + ]: 779544 : if (d_thss != NULL) {
661 : 54675 : d_thss->newEqClass(t);
662 : : }
663 : 779544 : }
664 : :
665 : 9044060 : void TheoryUF::eqNotifyMerge(TNode t1, TNode t2)
666 : : {
667 [ + + ]: 9044060 : if (d_thss != NULL) {
668 : 337936 : d_thss->merge(t1, t2);
669 : : }
670 : 9044060 : }
671 : :
672 : 1691370 : void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
673 [ + + ]: 1691370 : if (d_thss != NULL) {
674 : 38415 : d_thss->assertDisequal(t1, t2, reason);
675 : : }
676 : 1691370 : }
677 : :
678 : 235978 : bool TheoryUF::isHigherOrderType(TypeNode tn)
679 : : {
680 [ - + ][ - + ]: 235978 : Assert(tn.isFunction());
[ - - ]
681 : 235978 : std::map<TypeNode, bool>::iterator it = d_isHoType.find(tn);
682 [ + + ]: 235978 : if (it != d_isHoType.end())
683 : : {
684 : 223239 : return it->second;
685 : : }
686 : 12739 : bool ret = false;
687 : 12739 : const std::vector<TypeNode>& argTypes = tn.getArgTypes();
688 [ + + ]: 32621 : for (const TypeNode& tnc : argTypes)
689 : : {
690 [ - + ]: 19882 : if (tnc.isFunction())
691 : : {
692 : 0 : ret = true;
693 : 0 : break;
694 : : }
695 : : }
696 : 12739 : d_isHoType[tn] = ret;
697 : 12739 : return ret;
698 : : }
699 : :
700 : : } // namespace uf
701 : : } // namespace theory
702 : : } // namespace cvc5::internal
|
