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 : 49903 : TheoryUF::TheoryUF(Env& env,
46 : : OutputChannel& out,
47 : : Valuation valuation,
48 : 49903 : std::string instanceName)
49 : : : Theory(THEORY_UF, env, out, valuation, instanceName),
50 : : d_thss(nullptr),
51 : 49903 : 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 : 49903 : d_im(env, *this, d_state, "theory::uf::" + instanceName, false),
60 : 49903 : d_distinct(env, d_state, d_im),
61 : 49903 : d_notify(d_im, *this),
62 : 149709 : d_cpacb(*this)
63 : : {
64 : 49903 : d_true = nodeManager()->mkConst(true);
65 : : // indicate we are using the default theory state and inference managers
66 : 49903 : d_theoryState = &d_state;
67 : 49903 : d_inferManager = &d_im;
68 : 49903 : }
69 : :
70 : 99116 : TheoryUF::~TheoryUF() {
71 : 99116 : }
72 : :
73 : 49903 : TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
74 : :
75 : 18861 : ProofRuleChecker* TheoryUF::getProofChecker() { return &d_checker; }
76 : :
77 : 49903 : bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
78 : : {
79 : 49903 : esi.d_notify = &d_notify;
80 : 49903 : esi.d_name = d_instanceName + "theory::uf::ee";
81 : 49903 : if (options().quantifiers.finiteModelFind
82 [ + + ][ + - ]: 49903 : && options().uf.ufssMode != options::UfssMode::NONE)
[ + + ]
83 : : {
84 : : // need notifications about sorts
85 : 724 : esi.d_notifyNewClass = true;
86 : 724 : esi.d_notifyMerge = true;
87 : 724 : esi.d_notifyDisequal = true;
88 : : }
89 : 49903 : return true;
90 : : }
91 : :
92 : 49903 : void TheoryUF::finishInit() {
93 [ - + ][ - + ]: 49903 : Assert(d_equalityEngine != nullptr);
[ - - ]
94 : : // combined cardinality constraints are not evaluated in getModelValue
95 : 49903 : d_valuation.setUnevaluatedKind(Kind::COMBINED_CARDINALITY_CONSTRAINT);
96 : : // distinct should not be sent to the model
97 : 49903 : d_valuation.setIrrelevantKind(Kind::DISTINCT);
98 [ + + ]: 49903 : if (logicInfo().hasCardinalityConstraints())
99 : : {
100 [ - + ]: 46 : if (!options().uf.ufCardExp)
101 : : {
102 : 0 : std::stringstream ss;
103 : : ss << "Logic with cardinality constraints not available in this "
104 : 0 : "configuration, try --uf-card-exp.";
105 : 0 : throw SafeLogicException(ss.str());
106 : : }
107 : : }
108 : : // Initialize the cardinality constraints solver if the logic includes UF,
109 : : // finite model finding is enabled, and it is not disabled by
110 : : // the ufssMode option.
111 : 49903 : if (options().quantifiers.finiteModelFind
112 [ + + ][ + - ]: 49903 : && options().uf.ufssMode != options::UfssMode::NONE)
[ + + ]
113 : : {
114 : 724 : d_thss.reset(new CardinalityExtension(d_env, d_state, d_im, this));
115 : : }
116 : : // The kinds we are treating as function application in congruence
117 : 49903 : bool isHo = logicInfo().isHigherOrder();
118 : 49903 : d_equalityEngine->addFunctionKind(Kind::APPLY_UF, false, isHo);
119 [ + + ]: 49903 : if (isHo)
120 : : {
121 [ - + ]: 1201 : if (!options().uf.ufHoExp)
122 : : {
123 : 0 : std::stringstream ss;
124 : : ss << "Higher-order logic not available in this configuration, try "
125 : 0 : "--uf-ho-exp.";
126 : 0 : throw SafeLogicException(ss.str());
127 : : }
128 : 1201 : d_equalityEngine->addFunctionKind(Kind::HO_APPLY);
129 : 1201 : d_ho.reset(new HoExtension(d_env, d_state, d_im, *d_lambdaLift.get()));
130 : : }
131 : : // conversion kinds
132 : 49903 : d_equalityEngine->addFunctionKind(Kind::INT_TO_BITVECTOR, true);
133 : 49903 : d_equalityEngine->addFunctionKind(Kind::BITVECTOR_UBV_TO_INT, true);
134 : 49903 : }
135 : :
136 : : //--------------------------------- standard check
137 : :
138 : 49016 : bool TheoryUF::needsCheckLastEffort()
139 : : {
140 : : // last call effort needed if using finite model finding,
141 : : // arithmetic/bit-vector conversions, or higher-order extension
142 [ + + ][ + + ]: 96390 : return d_thss != nullptr || d_csolver != nullptr || d_ho != nullptr
143 [ + + ][ + + ]: 96390 : || d_distinct.needsCheckLastEffort();
144 : : }
145 : :
146 : 2551060 : void TheoryUF::postCheck(Effort level)
147 : : {
148 [ + + ]: 2551060 : if (d_state.isInConflict())
149 : : {
150 : 114485 : return;
151 : : }
152 : : // check with the cardinality constraints extension
153 [ + + ]: 2436580 : if (d_thss != nullptr)
154 : : {
155 : 111185 : d_thss->check(level);
156 : : }
157 [ + - ]: 2436580 : if (!d_state.isInConflict())
158 : : {
159 [ + + ]: 2436580 : if (level == Effort::EFFORT_LAST_CALL)
160 : : {
161 : : // check with conversions solver at last call effort
162 [ + + ]: 2918 : if (d_csolver != nullptr)
163 : : {
164 : 86 : d_csolver->check();
165 : : }
166 : : }
167 : 2436580 : d_distinct.check(level);
168 : : // check with the higher-order extension at full effort
169 [ + + ][ + + ]: 2436580 : if (fullEffort(level) && logicInfo().isHigherOrder())
[ + + ]
170 : : {
171 : 5492 : d_ho->check();
172 : : }
173 : : }
174 : : }
175 : :
176 : 6930490 : void TheoryUF::notifyFact(TNode atom,
177 : : bool pol,
178 : : TNode fact,
179 : : CVC5_UNUSED bool isInternal)
180 : : {
181 [ + + ]: 6930490 : if (d_state.isInConflict())
182 : : {
183 : 113369 : return;
184 : : }
185 [ + + ]: 6817120 : if (d_thss != nullptr)
186 : : {
187 : : bool isDecision =
188 : 231748 : d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
189 : 231748 : d_thss->assertNode(fact, isDecision);
190 : : }
191 [ + + ][ + + ]: 6817120 : switch (atom.getKind())
192 : : {
193 : 6314830 : case Kind::EQUAL:
194 : : {
195 [ + + ][ + - ]: 6314830 : if (logicInfo().isHigherOrder() && options().uf.ufHoExt)
[ + + ]
196 : : {
197 : 136625 : if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
198 : : {
199 : : // apply extensionality eagerly using the ho extension
200 : 34832 : d_ho->applyExtensionality(fact);
201 : : }
202 : : }
203 : : }
204 : 6314830 : break;
205 : 16614 : case Kind::DISTINCT:
206 : : {
207 : : // call the distinct extension
208 : 16614 : d_distinct.assertDistinct(atom, pol, fact);
209 : : }
210 : 16614 : break;
211 : 19230 : case Kind::CARDINALITY_CONSTRAINT:
212 : : case Kind::COMBINED_CARDINALITY_CONSTRAINT:
213 : : {
214 [ - + ]: 19230 : if (d_thss == nullptr)
215 : : {
216 [ - - ]: 0 : if (!logicInfo().hasCardinalityConstraints())
217 : : {
218 : 0 : std::stringstream ss;
219 : 0 : ss << "Cardinality constraint " << atom
220 : 0 : << " was asserted, but the logic does not allow it." << std::endl;
221 : 0 : ss << "Try using a logic containing \"UFC\"." << std::endl;
222 : 0 : throw Exception(ss.str());
223 : : }
224 : : else
225 : : {
226 : : // support for cardinality constraints is not enabled, set incomplete
227 : 0 : d_im.setModelUnsound(IncompleteId::UF_CARD_DISABLED);
228 : : }
229 : : }
230 : : }
231 : 19230 : break;
232 : 466441 : default: break;
233 : : }
234 : : }
235 : : //--------------------------------- end standard check
236 : :
237 : 368939 : TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
238 : : {
239 [ + - ]: 737878 : Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
240 : 368939 : << std::endl;
241 : 368939 : Kind k = node.getKind();
242 : 368939 : bool isHol = logicInfo().isHigherOrder();
243 [ - + ]: 368939 : if (node.getType().isAbstract())
244 : : {
245 : 0 : std::stringstream ss;
246 : 0 : ss << "Cannot process term of abstract type " << node;
247 : 0 : throw LogicException(ss.str());
248 : : }
249 [ + + ][ + + ]: 368939 : if (k == Kind::HO_APPLY || node.getType().isFunction())
[ + + ][ + + ]
[ - - ]
250 : : {
251 [ + + ]: 7998 : if (!isHol)
252 : : {
253 : 2 : std::stringstream ss;
254 [ - + ]: 1 : if (k == Kind::HO_APPLY)
255 : : {
256 : 0 : ss << "Higher-order function applications";
257 : : }
258 : : else
259 : : {
260 : 1 : ss << "Function terms";
261 : : }
262 : : ss << " are only supported with "
263 : 1 : "higher-order logic. Try adding the logic prefix HO_.";
264 : 1 : throw LogicException(ss.str());
265 : : }
266 : : }
267 [ + + ]: 360941 : else if (k == Kind::APPLY_UF)
268 : : {
269 : 243548 : if (!isHol && isHigherOrderType(node.getOperator().getType()))
270 : : {
271 : : // check for higher-order
272 : : // logic exception if higher-order is not enabled
273 : 0 : std::stringstream ss;
274 : 0 : ss << "UF received an application whose operator has higher-order type "
275 : 0 : << node
276 : : << ", which is only supported with higher-order logic. Try adding "
277 : 0 : "the logic prefix HO_.";
278 : 0 : throw LogicException(ss.str());
279 : : }
280 : : }
281 [ + + ]: 117249 : else if ((k == Kind::BITVECTOR_UBV_TO_INT || k == Kind::INT_TO_BITVECTOR)
282 [ + + ][ + + ]: 234642 : && options().uf.eagerArithBvConv)
[ + + ]
283 : : {
284 : : // eliminate if option specifies to eliminate eagerly
285 : : Node ret = k == Kind::BITVECTOR_UBV_TO_INT ? arith::eliminateBv2Nat(node)
286 : 14 : : arith::eliminateInt2Bv(node);
287 : 14 : return TrustNode::mkTrustRewrite(node, ret);
288 : : }
289 [ + + ]: 368924 : if (isHol)
290 : : {
291 : 47977 : TrustNode ret = d_ho->ppRewrite(node, lems);
292 [ + + ]: 47977 : if (!ret.isNull())
293 : : {
294 [ + - ]: 9962 : Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node
295 [ - + ][ - - ]: 4981 : << " to " << ret.getNode() << std::endl;
296 : 4981 : return ret;
297 : : }
298 : : }
299 : 363943 : return TrustNode::null();
300 : : }
301 : :
302 : 950396 : void TheoryUF::preRegisterTerm(TNode node)
303 : : {
304 [ + - ]: 950396 : Trace("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
305 : :
306 [ + + ]: 950396 : if (d_thss != nullptr)
307 : : {
308 : 55926 : d_thss->preRegisterTerm(node);
309 : : }
310 : :
311 : 950396 : Kind k = node.getKind();
312 [ + + ][ + + ]: 950396 : switch (k)
[ + - ][ + ]
313 : : {
314 : 342025 : case Kind::EQUAL:
315 : : // Add the trigger for equality
316 : 342025 : d_state.addEqualityEngineTriggerPredicate(node);
317 : 342025 : break;
318 : 351432 : case Kind::APPLY_UF: preRegisterFunctionTerm(node); break;
319 : 916 : case Kind::HO_APPLY:
320 : : {
321 [ - + ]: 916 : if (!logicInfo().isHigherOrder())
322 : : {
323 : 0 : std::stringstream ss;
324 : : ss << "Partial function applications are only supported with "
325 : 0 : "higher-order logic. Try adding the logic prefix HO_.";
326 : 0 : throw LogicException(ss.str());
327 : : }
328 : 916 : preRegisterFunctionTerm(node);
329 : : }
330 : 916 : break;
331 : 110 : case Kind::INT_TO_BITVECTOR:
332 : : case Kind::BITVECTOR_UBV_TO_INT:
333 : : {
334 [ - + ][ - + ]: 110 : Assert(!options().uf.eagerArithBvConv);
[ - - ]
335 : 110 : d_equalityEngine->addTerm(node);
336 : 110 : d_functionsTerms.push_back(node);
337 : : // initialize the conversions solver if not already done so
338 [ + + ]: 110 : if (d_csolver == nullptr)
339 : : {
340 : 60 : d_csolver.reset(new ConversionsSolver(d_env, d_state, d_im));
341 : : }
342 : : // call preregister
343 : 110 : d_csolver->preRegisterTerm(node);
344 : : }
345 : 110 : break;
346 : 5260 : case Kind::CARDINALITY_CONSTRAINT:
347 : : case Kind::COMBINED_CARDINALITY_CONSTRAINT:
348 : : // do nothing
349 : 5260 : break;
350 : 0 : case Kind::UNINTERPRETED_SORT_VALUE:
351 : : {
352 : : // Uninterpreted sort values should only appear in models, and should
353 : : // never appear in constraints. They are unallowed to ever appear in
354 : : // constraints since the cardinality of an uninterpreted sort may have an
355 : : // upper bound, e.g. if (forall ((x U) (y U)) (= x y)) holds, then @uc_U_2
356 : : // is a ill-formed term, as its existence cannot be assumed. The parser
357 : : // prevents the user from ever constructing uninterpreted sort values.
358 : : // However, they may be exported via models to API users. It is thus
359 : : // possible that these uninterpreted sort values are asserted back in
360 : : // constraints, hence this check is necessary.
361 : : throw LogicException(
362 : 0 : "An uninterpreted constant was preregistered to the UF theory.");
363 : : }
364 : : break;
365 : 250653 : default:
366 : : // Variables etc
367 : 250653 : d_equalityEngine->addTerm(node);
368 [ + + ]: 250653 : if (logicInfo().isHigherOrder())
369 : : {
370 : : // When using lazy lambda handling, if node is a lambda function, it must
371 : : // be marked as a shared term. This is to ensure we split on the equality
372 : : // of lambda functions with other functions when doing care graph
373 : : // based theory combination.
374 [ + + ]: 18590 : if (d_lambdaLift->isLambdaFunction(node))
375 : : {
376 : 668 : addSharedTerm(node);
377 : : }
378 : : }
379 [ - + ]: 232063 : else if (node.getType().isFunction())
380 : : {
381 : 0 : std::stringstream ss;
382 : : ss << "Function terms are only supported with higher-order logic. Try "
383 : 0 : "adding the logic prefix HO_.";
384 : 0 : throw LogicException(ss.str());
385 : : }
386 : 250653 : break;
387 : : }
388 : :
389 : 950396 : }
390 : :
391 : 352348 : void TheoryUF::preRegisterFunctionTerm(TNode node)
392 : : {
393 : : // Maybe it's a predicate
394 [ + + ]: 352348 : if (node.getType().isBoolean())
395 : : {
396 : 112306 : d_state.addEqualityEngineTriggerPredicate(node);
397 : : }
398 : : else
399 : : {
400 : : // Function applications/predicates
401 : 240042 : d_equalityEngine->addTerm(node);
402 : : }
403 : : // Remember the function and predicate terms
404 : 352348 : d_functionsTerms.push_back(node);
405 : 352348 : }
406 : :
407 : 0 : void TheoryUF::explain(TNode literal, Node& exp)
408 : : {
409 [ - - ]: 0 : Trace("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
410 : 0 : std::vector<TNode> assumptions;
411 : : // Do the work
412 : 0 : bool polarity = literal.getKind() != Kind::NOT;
413 [ - - ]: 0 : TNode atom = polarity ? literal : literal[0];
414 [ - - ]: 0 : if (atom.getKind() == Kind::EQUAL)
415 : : {
416 : 0 : d_equalityEngine->explainEquality(
417 : : atom[0], atom[1], polarity, assumptions, nullptr);
418 : : }
419 : : else
420 : : {
421 : 0 : d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
422 : : }
423 : 0 : exp = nodeManager()->mkAnd(assumptions);
424 : 0 : }
425 : :
426 : 188596 : TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
427 : :
428 : 29108 : bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
429 : : {
430 [ + + ]: 29108 : if (logicInfo().isHigherOrder())
431 : : {
432 : : // must add extensionality disequalities for all pairs of (non-disequal)
433 : : // function equivalence classes.
434 [ + + ]: 1274 : if (!d_ho->collectModelInfoHo(m, termSet))
435 : : {
436 [ + - ]: 9 : Trace("uf") << "Collect model info fail HO" << std::endl;
437 : 9 : return false;
438 : : }
439 : : }
440 : :
441 [ + - ]: 29099 : Trace("uf") << "UF : finish collectModelInfo " << std::endl;
442 : 29099 : return true;
443 : : }
444 : :
445 : 49334 : void TheoryUF::presolve() {
446 : : // TimerStat::CodeTimer codeTimer(d_presolveTimer);
447 : :
448 [ + - ]: 49334 : Trace("uf") << "uf: begin presolve()" << endl;
449 [ + + ]: 49334 : if (options().uf.ufSymmetryBreaker)
450 : : {
451 : 620 : vector<Node> newClauses;
452 : 310 : d_symb.apply(newClauses);
453 : 360 : for(vector<Node>::const_iterator i = newClauses.begin();
454 [ + + ]: 360 : i != newClauses.end();
455 : 50 : ++i) {
456 [ + - ]: 50 : Trace("uf") << "uf: generating a lemma: " << *i << std::endl;
457 : : // no proof generator provided
458 : 50 : d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY);
459 : : }
460 : : }
461 [ + + ]: 49334 : if( d_thss ){
462 : 723 : d_thss->presolve();
463 : : }
464 [ + - ]: 49334 : Trace("uf") << "uf: end presolve()" << endl;
465 : 49334 : }
466 : :
467 : 341204 : void TheoryUF::ppStaticLearn(TNode n, std::vector<TrustNode>& learned)
468 : : {
469 : : //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
470 : :
471 : : // Use the diamonds utility
472 : 341204 : d_dpfgen.ppStaticLearn(n, learned);
473 : :
474 [ + + ]: 341204 : if (options().uf.ufSymmetryBreaker)
475 : : {
476 : 53741 : d_symb.assertFormula(n);
477 : : }
478 : 341204 : } /* TheoryUF::ppStaticLearn() */
479 : :
480 : 6507 : EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
481 : :
482 : : // Check for equality (simplest)
483 [ + + ]: 6507 : if (d_equalityEngine->areEqual(a, b))
484 : : {
485 : : // The terms are implied to be equal
486 : 1732 : return EQUALITY_TRUE;
487 : : }
488 : :
489 : : // Check for disequality
490 [ - + ]: 4775 : if (d_equalityEngine->areDisequal(a, b, false))
491 : : {
492 : : // The terms are implied to be dis-equal
493 : 0 : return EQUALITY_FALSE;
494 : : }
495 : :
496 : : // All other terms we interpret as dis-equal in the model
497 : 4775 : return EQUALITY_FALSE_IN_MODEL;
498 : : }
499 : :
500 : 2402860 : bool TheoryUF::areCareDisequal(TNode x, TNode y)
501 : : {
502 : : // check for disequality first, as an optimization
503 : 4805650 : if (d_equalityEngine->hasTerm(x) && d_equalityEngine->hasTerm(y)
504 : 4805650 : && d_equalityEngine->areDisequal(x, y, false))
505 : : {
506 : 107713 : return true;
507 : : }
508 [ + + ][ - - ]: 2295150 : if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
509 [ + + ][ + + ]: 2295150 : && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
[ + + ][ + - ]
[ - - ]
510 : : {
511 : : TNode x_shared =
512 : 1919500 : d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
513 : : TNode y_shared =
514 : 1919500 : d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
515 : 1919500 : EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
516 [ + - ][ - + ]: 1919500 : if (eqStatus == EQUALITY_FALSE || eqStatus == EQUALITY_FALSE_AND_PROPAGATED)
517 : : {
518 : 0 : return true;
519 : : }
520 [ + + ]: 1919500 : else if (eqStatus == EQUALITY_FALSE_IN_MODEL)
521 : : {
522 : : // if x or y is a lambda function, and they are neither entailed to
523 : : // be equal or disequal, then we return false. This ensures the pair
524 : : // (x,y) may be considered for the care graph.
525 [ + + ][ - - ]: 3484650 : if (d_lambdaLift->isLambdaFunction(x)
526 [ + + ][ - + ]: 3484650 : || d_lambdaLift->isLambdaFunction(y))
[ + + ][ + - ]
[ - - ]
527 : : {
528 : 609 : return false;
529 : : }
530 : 1741710 : return true;
531 : : }
532 : : }
533 : 552824 : return false;
534 : : }
535 : :
536 : 367294 : void TheoryUF::processCarePairArgs(TNode a, TNode b)
537 : : {
538 : : // if a and b are already equal, we ignore this pair
539 [ + + ]: 367294 : if (d_state.areEqual(a, b))
540 : : {
541 : 35298 : return;
542 : : }
543 : : // otherwise, we add pairs for each of their arguments
544 : 331996 : addCarePairArgs(a, b);
545 : :
546 : : // also split on functions
547 [ + + ]: 331996 : if (logicInfo().isHigherOrder())
548 : : {
549 : 113598 : NodeManager* nm = nodeManager();
550 [ + + ]: 339643 : for (size_t k = 0, nchild = a.getNumChildren(); k < nchild; ++k)
551 : : {
552 : 226045 : TNode x = a[k];
553 : 226045 : TNode y = b[k];
554 [ + + ]: 226045 : if (d_state.areEqual(x, y))
555 : : {
556 : 185755 : continue;
557 : : }
558 : : // Splitting on functions. This is required since conceptually the HO
559 : : // extension should be considered a separate entity with regards to
560 : : // theory combination (in particular, with the core UF solver). This is
561 : : // similar to how we handle sets of sets, where each set type is
562 : : // considered a separate entity. The types below must be equal to handle
563 : : // polymorphic operators taking higher-order arguments, e.g. set.map.
564 : 80580 : TypeNode xt = x.getType();
565 [ + + ][ + - ]: 40290 : if (xt.isFunction() && xt==y.getType())
[ + + ][ + + ]
[ - - ]
566 : : {
567 : 10980 : Node lemma = x.eqNode(y);
568 : 10980 : lemma = nm->mkNode(Kind::OR, lemma, lemma.notNode());
569 : 10980 : d_im.lemma(lemma, InferenceId::UF_HO_CG_SPLIT);
570 : : }
571 : : }
572 : : }
573 : : }
574 : :
575 : 29108 : void TheoryUF::computeRelevantTerms(std::set<Node>& termSet)
576 : : {
577 [ + + ]: 29108 : if (d_ho!=nullptr)
578 : : {
579 : 1274 : d_ho->computeRelevantTerms(termSet);
580 : : }
581 : 29108 : }
582 : :
583 : 65391 : void TheoryUF::computeCareGraph() {
584 : 65391 : bool isHigherOrder = logicInfo().isHigherOrder();
585 : : // note that if we are higher-order, we may still generate splits for
586 : : // function arguments
587 [ + + ][ + + ]: 65391 : if (d_state.getSharedTerms().empty() && !isHigherOrder)
[ + + ]
588 : : {
589 : 25315 : return;
590 : : }
591 : 40076 : NodeManager* nm = nodeManager();
592 : : // Use term indexing. We build separate indices for APPLY_UF and HO_APPLY.
593 : : // We maintain indices per operator for the former, and indices per
594 : : // function type for the latter.
595 [ + - ]: 80152 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..."
596 : 40076 : << std::endl;
597 : : // temporary keep set for higher-order indexing below
598 : 80152 : std::vector<Node> keep;
599 : 80152 : std::map<Node, TNodeTrie> index;
600 : 80152 : std::map<TypeNode, TNodeTrie> typeIndex;
601 : 40076 : std::map<Node, size_t> arity;
602 [ + + ]: 815865 : for (TNode app : d_functionsTerms)
603 : : {
604 : 1551580 : std::vector<TNode> reps;
605 : 775789 : bool has_trigger_arg = false;
606 [ + + ]: 1746000 : for (const Node& j : app)
607 : : {
608 : 970213 : reps.push_back(d_equalityEngine->getRepresentative(j));
609 : : // if doing higher-order, higher-order arguments must all be considered as
610 : : // well
611 [ + + ][ - - ]: 970213 : if (d_equalityEngine->isTriggerTerm(j, THEORY_UF)
612 [ + + ][ + + ]: 970213 : || (isHigherOrder && j.getType().isFunction()))
[ + + ][ + + ]
[ + - ][ - - ]
613 : : {
614 : 794233 : has_trigger_arg = true;
615 : : }
616 : : }
617 [ + + ]: 775789 : if (has_trigger_arg)
618 : : {
619 [ + - ]: 1355760 : Trace("uf::sharing-terms")
620 : 677881 : << "...add: " << app << " / " << reps << std::endl;
621 : 677881 : Kind k = app.getKind();
622 [ + + ]: 677881 : if (k == Kind::APPLY_UF)
623 : : {
624 : 1353610 : Node op = app.getOperator();
625 : 676804 : index[op].addTerm(app, reps);
626 : 676804 : arity[op] = reps.size();
627 [ + + ][ + - ]: 676804 : if (isHigherOrder && d_equalityEngine->hasTerm(op))
[ + + ][ + + ]
[ - - ]
628 : : {
629 : : // Since we use a lazy app-completion scheme for equating fully
630 : : // and partially applied versions of terms, we must add all
631 : : // sub-chains to the HO index if the operator of this term occurs
632 : : // in a higher-order context in the equality engine. In other words,
633 : : // for (f a b c), this will add the terms:
634 : : // (HO_APPLY f a), (HO_APPLY (HO_APPLY f a) b),
635 : : // (HO_APPLY (HO_APPLY (HO_APPLY f a) b) c) to the higher-order
636 : : // term index for consideration when computing care pairs.
637 : 19138 : Node curr = op;
638 [ + + ]: 21820 : for (const Node& c : app)
639 : : {
640 : 36753 : Node happ = nm->mkNode(Kind::HO_APPLY, curr, c);
641 [ - + ][ - + ]: 12251 : Assert(curr.getType().isFunction());
[ - - ]
642 [ + + ][ - - ]: 36753 : typeIndex[curr.getType()].addTerm(happ, {curr, c});
643 : 12251 : curr = happ;
644 : 12251 : keep.push_back(happ);
645 : : }
646 : : }
647 : : }
648 [ + + ][ + + ]: 1077 : else if (k == Kind::HO_APPLY || k == Kind::BITVECTOR_UBV_TO_INT)
649 : : {
650 : : // add it to the typeIndex for the function type if HO_APPLY, or the
651 : : // bitvector type if bv2nat. The latter ensures that we compute
652 : : // care pairs based on bv2nat only for bitvectors of the same width.
653 : 948 : typeIndex[app[0].getType()].addTerm(app, reps);
654 : : }
655 : : else
656 : : {
657 : : // case for other operators, e.g. int2bv
658 : 129 : Node op = app.getOperator();
659 : 129 : index[op].addTerm(app, reps);
660 : 129 : arity[op] = reps.size();
661 : : }
662 : : }
663 : : }
664 : : // for each index
665 [ + + ]: 104552 : for (std::pair<const Node, TNodeTrie>& tt : index)
666 : : {
667 [ + - ]: 128952 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
668 : 64476 : << tt.first << "..." << std::endl;
669 [ - + ][ - + ]: 64476 : Assert(arity.find(tt.first) != arity.end());
[ - - ]
670 : 64476 : nodeTriePathPairProcess(&tt.second, arity[tt.first], d_cpacb);
671 : : }
672 [ + + ]: 42013 : for (std::pair<const TypeNode, TNodeTrie>& tt : typeIndex)
673 : : {
674 : : // functions for HO_APPLY which has arity 2, bitvectors for bv2nat which
675 : : // has arity one
676 [ + + ]: 1937 : size_t a = tt.first.isFunction() ? 2 : 1;
677 [ + - ]: 3874 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index "
678 : 1937 : << tt.first << "..." << std::endl;
679 : : // the arity of HO_APPLY is always two
680 : 1937 : nodeTriePathPairProcess(&tt.second, a, d_cpacb);
681 : : }
682 [ + - ]: 80152 : Trace("uf::sharing") << "TheoryUf::computeCareGraph(): finished."
683 : 40076 : << std::endl;
684 : : }/* TheoryUF::computeCareGraph() */
685 : :
686 : 747985 : void TheoryUF::eqNotifyNewClass(TNode t) {
687 [ + + ]: 747985 : if (d_thss != NULL) {
688 : 51531 : d_thss->newEqClass(t);
689 : : }
690 : 747985 : }
691 : :
692 : 9115900 : void TheoryUF::eqNotifyMerge(TNode t1, TNode t2)
693 : : {
694 [ + + ]: 9115900 : if (d_thss != NULL)
695 : : {
696 : 320612 : d_thss->merge(t1, t2);
697 : : }
698 : : // check if we have a conflict due to distinct
699 : 9115900 : d_distinct.eqNotifyMerge(t1, t2);
700 : 9115900 : }
701 : :
702 : 1540650 : void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
703 [ + + ]: 1540650 : if (d_thss != NULL) {
704 : 36824 : d_thss->assertDisequal(t1, t2, reason);
705 : : }
706 : 1540650 : }
707 : :
708 : 211846 : bool TheoryUF::isHigherOrderType(TypeNode tn)
709 : : {
710 [ - + ][ - + ]: 211846 : Assert(tn.isFunction());
[ - - ]
711 : 211846 : std::map<TypeNode, bool>::iterator it = d_isHoType.find(tn);
712 [ + + ]: 211846 : if (it != d_isHoType.end())
713 : : {
714 : 199341 : return it->second;
715 : : }
716 : 12505 : bool ret = false;
717 : 12505 : const std::vector<TypeNode>& argTypes = tn.getArgTypes();
718 [ + + ]: 31523 : for (const TypeNode& tnc : argTypes)
719 : : {
720 [ - + ]: 19018 : if (tnc.isFunction())
721 : : {
722 : 0 : ret = true;
723 : 0 : break;
724 : : }
725 : : }
726 : 12505 : d_isHoType[tn] = ret;
727 : 12505 : return ret;
728 : : }
729 : :
730 : : } // namespace uf
731 : : } // namespace theory
732 : : } // namespace cvc5::internal
|
