Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of relevance manager.
11 : : */
12 : :
13 : : #include "theory/relevance_manager.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/node_algorithm.h"
18 : : #include "expr/term_context_stack.h"
19 : : #include "options/smt_options.h"
20 : : #include "smt/env.h"
21 : : #include "theory/relevance_manager.h"
22 : :
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : :
28 : 486 : RelevanceManager::RelevanceManager(Env& env, TheoryEngine* engine)
29 : : : TheoryEngineModule(env, engine, "RelevanceManager"),
30 : 486 : d_val(engine),
31 : 486 : d_input(userContext()),
32 : 486 : d_atomMap(userContext()),
33 : 486 : d_rset(context()),
34 : 486 : d_inFullEffortCheck(false),
35 : 486 : d_fullEffortCheckFail(false),
36 : 486 : d_success(false),
37 : 486 : d_trackRSetExp(false),
38 : 486 : d_miniscopeTopLevel(true),
39 : 486 : d_rsetExp(context()),
40 : 972 : d_jcache(context())
41 : : {
42 [ + + ]: 486 : if (options().smt.produceDifficulty)
43 : : {
44 : 467 : d_dman = std::make_unique<DifficultyManager>(env, this, d_val);
45 : 467 : d_trackRSetExp = true;
46 : : // we cannot miniscope AND at the top level, since we need to
47 : : // preserve the exact form of preprocessed assertions so the dependencies
48 : : // are tracked.
49 : 467 : d_miniscopeTopLevel = false;
50 : : }
51 : 486 : }
52 : :
53 : 483 : void RelevanceManager::notifyPreprocessedAssertions(
54 : : const std::vector<Node>& assertions, bool isInput)
55 : : {
56 : : // add to input list, which is user-context dependent
57 : 483 : std::vector<Node> toProcess;
58 [ + + ]: 1368 : for (const Node& a : assertions)
59 : : {
60 [ + + ][ - + ]: 885 : if (d_miniscopeTopLevel && a.getKind() == Kind::AND)
[ - + ]
61 : : {
62 : : // split top-level AND
63 [ - - ]: 0 : for (const Node& ac : a)
64 : : {
65 : 0 : toProcess.push_back(ac);
66 : 0 : }
67 : : }
68 : : else
69 : : {
70 : 885 : d_input.push_back(a);
71 : : // add to atoms map
72 : 885 : addInputToAtomsMap(a);
73 : : }
74 : : }
75 : 483 : addAssertionsInternal(toProcess);
76 : : // notify the difficulty manager if these are input assertions
77 [ + - ][ + + ]: 483 : if (isInput && d_dman != nullptr)
[ + + ]
78 : : {
79 : 464 : d_dman->notifyInputAssertions(assertions);
80 : : }
81 : 483 : }
82 : :
83 : 0 : void RelevanceManager::notifyPreprocessedAssertion(Node n, bool isInput)
84 : : {
85 : 0 : std::vector<Node> toProcess;
86 : 0 : toProcess.push_back(n);
87 : 0 : notifyPreprocessedAssertions(toProcess, isInput);
88 : 0 : }
89 : :
90 : 483 : void RelevanceManager::addAssertionsInternal(std::vector<Node>& toProcess)
91 : : {
92 : 483 : size_t i = 0;
93 [ - + ]: 483 : while (i < toProcess.size())
94 : : {
95 : 0 : Node a = toProcess[i];
96 : 0 : if (d_miniscopeTopLevel && a.getKind() == Kind::AND)
97 : : {
98 : : // difficulty tracking disables miniscoping of AND
99 : 0 : Assert(d_dman == nullptr);
100 : : // split AND
101 [ - - ]: 0 : for (const Node& ac : a)
102 : : {
103 : 0 : toProcess.push_back(ac);
104 : 0 : }
105 : : }
106 : : else
107 : : {
108 : : // note that a could be a literal, in which case we could add it to
109 : : // an "always relevant" set here.
110 : 0 : d_input.push_back(a);
111 : : // add to atoms map
112 : 0 : addInputToAtomsMap(a);
113 : : }
114 : 0 : i++;
115 : 0 : }
116 : 483 : }
117 : :
118 : 885 : void RelevanceManager::addInputToAtomsMap(TNode input)
119 : : {
120 : 885 : std::unordered_set<TNode> visited;
121 : 885 : std::vector<TNode> visit;
122 : 885 : TNode cur;
123 : 885 : visit.push_back(input);
124 : : do
125 : : {
126 : 1333 : cur = visit.back();
127 : 1333 : visit.pop_back();
128 [ + - ]: 1333 : if (visited.find(cur) == visited.end())
129 : : {
130 : 1333 : visited.insert(cur);
131 [ + + ]: 1333 : if (expr::isBooleanConnective(cur))
132 : : {
133 : 362 : visit.insert(visit.end(), cur.begin(), cur.end());
134 : 362 : continue;
135 : : }
136 : 971 : NodeList* ilist = getInputListFor(cur);
137 : 971 : ilist->push_back(input);
138 : : }
139 [ + + ]: 1333 : } while (!visit.empty());
140 : 885 : }
141 : :
142 : 1692 : void RelevanceManager::check(Theory::Effort effort)
143 : : {
144 [ + + ]: 1692 : if (Theory::fullEffort(effort))
145 : : {
146 : 428 : d_inFullEffortCheck = true;
147 : 428 : d_fullEffortCheckFail = false;
148 : : }
149 : 1692 : }
150 : :
151 : 1692 : void RelevanceManager::postCheck(CVC5_UNUSED Theory::Effort effort)
152 : : {
153 : 1692 : d_inFullEffortCheck = false;
154 : 1692 : }
155 : :
156 : 1737 : void RelevanceManager::computeRelevance()
157 : : {
158 : : // if not at full effort, should be tracking something else, e.g. explanation
159 : : // for why literals are relevant.
160 [ - + ][ - - ]: 1737 : Assert(d_inFullEffortCheck || d_trackRSetExp);
[ - + ][ - + ]
[ - - ]
161 [ + - ]: 3474 : Trace("rel-manager") << "RelevanceManager::computeRelevance, full effort = "
162 : 1737 : << d_inFullEffortCheck << "..." << std::endl;
163 : : // if we already failed
164 [ - + ]: 1737 : if (d_fullEffortCheckFail)
165 : : {
166 : 0 : d_success = false;
167 : 0 : return;
168 : : }
169 [ + + ]: 8660 : for (const Node& node : d_input)
170 : : {
171 [ - + ]: 6923 : if (!computeRelevanceFor(node))
172 : : {
173 : 0 : d_success = false;
174 : 0 : return;
175 : : }
176 : : }
177 [ - + ]: 1737 : if (TraceIsOn("rel-manager"))
178 : : {
179 [ - - ]: 0 : if (d_inFullEffortCheck)
180 : : {
181 [ - - ]: 0 : Trace("rel-manager") << "...success (full), size = " << d_rset.size()
182 : 0 : << std::endl;
183 : : }
184 : : else
185 : : {
186 [ - - ]: 0 : Trace("rel-manager") << "...success, exp size = " << d_rsetExp.size()
187 : 0 : << std::endl;
188 : : }
189 : : }
190 : 1737 : d_success = !d_fullEffortCheckFail;
191 : : }
192 : :
193 : 7475 : bool RelevanceManager::computeRelevanceFor(TNode input)
194 : : {
195 : 7475 : int32_t val = justify(input);
196 [ - + ]: 7475 : if (val == -1)
197 : : {
198 : : // if we are in full effort check and fail to justify, then we should
199 : : // give a failure and set success to false, or otherwise calls to
200 : : // isRelevant cannot be trusted. It might also be the case that the
201 : : // assertion has no value (val == 0), since it may correspond to an
202 : : // irrelevant Skolem definition, in this case we don't throw a warning.
203 [ - - ]: 0 : if (d_inFullEffortCheck)
204 : : {
205 : 0 : std::stringstream serr;
206 : 0 : serr << "RelevanceManager::computeRelevance: WARNING: failed to justify "
207 : 0 : << input;
208 : 0 : Trace("rel-manager") << serr.str() << std::endl;
209 : 0 : DebugUnhandled() << serr.str();
210 : : d_fullEffortCheckFail = true;
211 : : return false;
212 : 0 : }
213 : : }
214 : 7475 : return true;
215 : : }
216 : :
217 : 508 : bool RelevanceManager::updateJustifyLastChild(
218 : : const RlvPair& cur, std::vector<int32_t>& childrenJustify)
219 : : {
220 : : // This method is run when we are informed that child index of cur
221 : : // has justify status lastChildJustify. We return true if we would like to
222 : : // compute the next child, in this case we push the status of the current
223 : : // child to childrenJustify.
224 : 508 : size_t nchildren = cur.first.getNumChildren();
225 [ - + ][ - + ]: 508 : Assert(expr::isBooleanConnective(cur.first));
[ - - ]
226 : 508 : size_t index = childrenJustify.size();
227 [ - + ][ - + ]: 508 : Assert(index < nchildren);
[ - - ]
228 : 508 : Kind k = cur.first.getKind();
229 : : // Lookup the last child's value in the overall cache, we may choose to
230 : : // add this to childrenJustify if we return true.
231 : : RlvPair cp(cur.first[index],
232 : 1016 : d_ptctx.computeValue(cur.first, cur.second, index));
233 [ - + ][ - + ]: 508 : Assert(d_jcache.find(cp) != d_jcache.end());
[ - - ]
234 : 508 : int32_t lastChildJustify = d_jcache[cp];
235 [ + + ]: 508 : if (k == Kind::NOT)
236 : : {
237 : 318 : d_jcache[cur] = -lastChildJustify;
238 : : }
239 [ + + ][ + + ]: 190 : else if (k == Kind::IMPLIES || k == Kind::AND || k == Kind::OR)
[ + + ]
240 : : {
241 [ + + ]: 113 : if (lastChildJustify != 0)
242 : : {
243 : : // See if we short circuited? The value for short circuiting is false if
244 : : // we are AND or the first child of IMPLIES.
245 : 99 : if (lastChildJustify
246 [ + + ][ + + ]: 99 : == ((k == Kind::AND || (k == Kind::IMPLIES && index == 0)) ? -1 : 1))
[ + + ][ + + ]
247 : : {
248 [ + + ]: 40 : d_jcache[cur] = k == Kind::AND ? -1 : 1;
249 : 40 : return false;
250 : : }
251 : : }
252 : : // add current child to list first before (possibly) computing result
253 : 73 : childrenJustify.push_back(lastChildJustify);
254 [ + + ]: 73 : if (index + 1 == nchildren)
255 : : {
256 : : // finished all children, compute the overall value
257 [ + + ]: 12 : int ret = k == Kind::AND ? 1 : -1;
258 [ + + ]: 29 : for (int cv : childrenJustify)
259 : : {
260 [ + + ]: 23 : if (cv == 0)
261 : : {
262 : 6 : ret = 0;
263 : 6 : break;
264 : : }
265 : : }
266 : 12 : d_jcache[cur] = ret;
267 : : }
268 : : else
269 : : {
270 : : // continue
271 : 61 : return true;
272 : : }
273 : 12 : }
274 [ + + ]: 77 : else if (lastChildJustify == 0)
275 : : {
276 : : // all other cases, an unknown child implies we are unknown
277 : 17 : d_jcache[cur] = 0;
278 : : }
279 [ + + ]: 60 : else if (k == Kind::ITE)
280 : : {
281 [ + + ]: 58 : if (index == 0)
282 : : {
283 [ - + ][ - + ]: 29 : Assert(lastChildJustify != 0);
[ - - ]
284 : : // continue with branch
285 : 29 : childrenJustify.push_back(lastChildJustify);
286 [ + + ]: 29 : if (lastChildJustify == -1)
287 : : {
288 : : // also mark first branch as don't care
289 : 19 : childrenJustify.push_back(0);
290 : : }
291 : 29 : return true;
292 : : }
293 : : else
294 : : {
295 : : // should be in proper branch
296 [ + + ][ - + ]: 29 : Assert(childrenJustify[0] == (index == 1 ? 1 : -1));
[ - + ][ - - ]
297 : : // we are the value of the branch
298 : 29 : d_jcache[cur] = lastChildJustify;
299 : : }
300 : : }
301 : : else
302 : : {
303 [ - + ][ - - ]: 2 : Assert(k == Kind::XOR || k == Kind::EQUAL);
[ - + ][ - + ]
[ - - ]
304 [ - + ][ - + ]: 2 : Assert(nchildren == 2);
[ - - ]
305 [ - + ][ - + ]: 2 : Assert(lastChildJustify != 0);
[ - - ]
306 [ + + ]: 2 : if (index == 0)
307 : : {
308 : : // must compute the other child
309 : 1 : childrenJustify.push_back(lastChildJustify);
310 : 1 : return true;
311 : : }
312 : : else
313 : : {
314 : : // both children known, compute value
315 [ + - ][ + - ]: 1 : Assert(childrenJustify.size() == 1 && childrenJustify[0] != 0);
[ - + ][ - + ]
[ - - ]
316 : 2 : d_jcache[cur] =
317 [ + - ]: 1 : ((k == Kind::XOR ? -1 : 1) * lastChildJustify == childrenJustify[0])
318 [ + - ]: 2 : ? 1
319 : 1 : : -1;
320 : : }
321 : : }
322 : 377 : return false;
323 : 508 : }
324 : :
325 : 7475 : int32_t RelevanceManager::justify(TNode n)
326 : : {
327 : : // The set of nodes that we have computed currently have no value. Those
328 : : // that are marked as having no value in d_jcache must be recomputed, since
329 : : // the values for SAT literals may have changed.
330 : 7475 : std::unordered_set<RlvPair, RlvPairHashFunction> noJustify;
331 : : // the vector of values of children
332 : : std::unordered_map<RlvPair, std::vector<int32_t>, RlvPairHashFunction>
333 : 7475 : childJustify;
334 : 7475 : RlvPairIntMap::iterator it;
335 : : std::unordered_map<RlvPair, std::vector<int32_t>, RlvPairHashFunction>::
336 : 7475 : iterator itc;
337 : 7475 : RlvPair cur;
338 : 7475 : TCtxStack visit(&d_ptctx);
339 : 7475 : visit.pushInitial(n);
340 : : do
341 : : {
342 : 8491 : cur = visit.getCurrent();
343 : : // should always have Boolean type
344 [ - + ][ - + ]: 8491 : Assert(cur.first.getType().isBoolean());
[ - - ]
345 : 8491 : it = d_jcache.find(cur);
346 [ + + ]: 8491 : if (it != d_jcache.end())
347 : : {
348 [ + + ][ - + ]: 6888 : if (it->second != 0 || noJustify.find(cur) != noJustify.end())
[ + + ]
349 : : {
350 : 6815 : visit.pop();
351 : : // already computed value
352 : 6815 : continue;
353 : : }
354 : : }
355 : 1676 : itc = childJustify.find(cur);
356 : : // have we traversed to children yet?
357 [ + + ]: 1676 : if (itc == childJustify.end())
358 : : {
359 : : // are we not a Boolean connective (including NOT)?
360 [ + + ]: 1168 : if (expr::isBooleanConnective(cur.first))
361 : : {
362 : : // initialize its children justify vector as empty
363 : 417 : childJustify[cur].clear();
364 : : // start with the first child
365 : 417 : visit.pushChild(cur.first, cur.second, 0);
366 : : }
367 : : else
368 : : {
369 : 751 : visit.pop();
370 : : // The atom case, lookup the value in the valuation class to
371 : : // see its current value in the SAT solver, if it has one.
372 : 751 : int ret = 0;
373 : : // otherwise we look up the value
374 : : bool value;
375 [ + + ]: 751 : if (d_val.hasSatValue(cur.first, value))
376 : : {
377 [ + + ]: 720 : ret = value ? 1 : -1;
378 : : bool hasPol, pol;
379 : 720 : PolarityTermContext::getFlags(cur.second, hasPol, pol);
380 : : // relevant if weakly matches polarity
381 [ + + ][ + + ]: 720 : if (!hasPol || pol == value)
382 : : {
383 : 681 : d_rset.insert(cur.first);
384 [ + + ]: 681 : if (d_trackRSetExp)
385 : : {
386 : 593 : d_rsetExp[cur.first] = n;
387 [ + - ]: 1186 : Trace("rel-manager-exp")
388 : 0 : << "Reason for " << cur.first << " is " << n
389 : 593 : << ", polarity is " << hasPol << "/" << pol << std::endl;
390 : : }
391 : : }
392 : : }
393 : 751 : d_jcache[cur] = ret;
394 [ + + ]: 751 : if (ret == 0)
395 : : {
396 : 31 : noJustify.insert(cur);
397 : : }
398 : : }
399 : : }
400 : : else
401 : : {
402 : : // this processes the impact of the current child on the value of cur,
403 : : // and possibly requests that a new child is computed.
404 [ + + ]: 508 : if (updateJustifyLastChild(cur, itc->second))
405 : : {
406 [ - + ][ - + ]: 91 : Assert(itc->second.size() < cur.first.getNumChildren());
[ - - ]
407 : 91 : visit.pushChild(cur.first, cur.second, itc->second.size());
408 : : }
409 : : else
410 : : {
411 : 417 : visit.pop();
412 [ - + ][ - + ]: 417 : Assert(d_jcache.find(cur) != d_jcache.end());
[ - - ]
413 [ + + ]: 417 : if (d_jcache[cur] == 0)
414 : : {
415 : 27 : noJustify.insert(cur);
416 : : }
417 : : }
418 : : }
419 [ + + ]: 8491 : } while (!visit.empty());
420 : 7475 : RlvPair ci(n, d_ptctx.initialValue());
421 [ - + ][ - + ]: 7475 : Assert(d_jcache.find(ci) != d_jcache.end());
[ - - ]
422 : 14950 : return d_jcache[ci];
423 : 7475 : }
424 : :
425 : 1726 : bool RelevanceManager::isRelevant(TNode lit)
426 : : {
427 [ - + ][ - + ]: 1726 : Assert(d_inFullEffortCheck);
[ - - ]
428 : : // since this is used in full effort, and typically for all asserted literals,
429 : : // we just ensure relevance is fully computed here
430 : 1726 : computeRelevance();
431 [ - + ]: 1726 : if (!d_success)
432 : : {
433 : : // always relevant if we failed to compute
434 : 0 : return true;
435 : : }
436 : : // agnostic to negation
437 [ + + ]: 2449 : while (lit.getKind() == Kind::NOT)
438 : : {
439 : 723 : lit = lit[0];
440 : : }
441 : 1726 : return d_rset.find(lit) != d_rset.end();
442 : : }
443 : :
444 : 1072 : TNode RelevanceManager::getExplanationForRelevant(TNode lit)
445 : : {
446 : : // agnostic to negation
447 [ - + ]: 1072 : while (lit.getKind() == Kind::NOT)
448 : : {
449 : 0 : lit = lit[0];
450 : : }
451 : 1072 : NodeList* ilist = nullptr;
452 : 1072 : TNode nextInput;
453 : 1072 : size_t ninputs = 0;
454 : 1072 : size_t index = 0;
455 : : do
456 : : {
457 : : // check if it has an explanation yet
458 : 1624 : TNode exp = getExplanationForRelevantInternal(lit);
459 [ + + ]: 1624 : if (!exp.isNull())
460 : : {
461 : 602 : return exp;
462 : : }
463 : : // if the first time, we get the list of input formulas the atom occurs in
464 [ + + ]: 1022 : if (index == 0)
465 : : {
466 : 984 : ilist = getInputListFor(lit, false);
467 [ + + ]: 984 : if (ilist != nullptr)
468 : : {
469 : 543 : ninputs = ilist->size();
470 : : }
471 [ + - ]: 1968 : Trace("rel-manager-exp-debug")
472 : 0 : << "Atom " << lit << " occurs in " << ninputs << " assertions..."
473 : 984 : << std::endl;
474 : : }
475 [ + + ]: 1022 : if (index < ninputs)
476 : : {
477 : : // justify the next
478 : 552 : nextInput = (*ilist)[index];
479 : 552 : index++;
480 : : // justify the next input that the atom occurs in
481 : 552 : computeRelevanceFor(nextInput);
482 : : }
483 : : else
484 : : {
485 : 470 : nextInput = TNode::null();
486 : : }
487 [ + + ][ + + ]: 2646 : } while (!nextInput.isNull());
488 : :
489 : 470 : return TNode::null();
490 : 1072 : }
491 : :
492 : 1624 : TNode RelevanceManager::getExplanationForRelevantInternal(TNode atom) const
493 : : {
494 : 1624 : NodeMap::const_iterator it = d_rsetExp.find(atom);
495 [ + + ]: 1624 : if (it != d_rsetExp.end())
496 : : {
497 : 602 : return it->second;
498 : : }
499 : 1022 : return TNode::null();
500 : : }
501 : :
502 : 1955 : RelevanceManager::NodeList* RelevanceManager::getInputListFor(TNode atom,
503 : : bool doMake)
504 : : {
505 : 1955 : NodeListMap::const_iterator it = d_atomMap.find(atom);
506 [ + + ]: 1955 : if (it == d_atomMap.end())
507 : : {
508 [ + + ]: 1357 : if (!doMake)
509 : : {
510 : 441 : return nullptr;
511 : : }
512 : 916 : d_atomMap[atom] = std::make_shared<NodeList>(userContext());
513 : 916 : it = d_atomMap.find(atom);
514 : : }
515 : 1514 : return it->second.get();
516 : : }
517 : :
518 : 11 : std::unordered_set<TNode> RelevanceManager::getRelevantAssertions(bool& success)
519 : : {
520 : : // set in full effort check temporarily
521 : 11 : d_inFullEffortCheck = true;
522 : 11 : d_fullEffortCheckFail = false;
523 : 11 : computeRelevance();
524 : : // update success flag
525 : 11 : success = d_success;
526 : 11 : std::unordered_set<TNode> rset;
527 [ + - ]: 11 : if (success)
528 : : {
529 [ + + ]: 73 : for (const Node& a : d_rset)
530 : : {
531 : 62 : rset.insert(a);
532 : 62 : }
533 : : }
534 : : // reset in full effort check
535 : 11 : d_inFullEffortCheck = false;
536 : 11 : return rset;
537 : 0 : }
538 : :
539 : 908 : void RelevanceManager::notifyLemma(TNode n,
540 : : CVC5_UNUSED InferenceId id,
541 : : LemmaProperty p,
542 : : const std::vector<Node>& skAsserts,
543 : : CVC5_UNUSED const std::vector<Node>& sks)
544 : : {
545 : : // add to assertions
546 [ + + ][ - + ]: 908 : if (options().theory.relevanceFilter && isLemmaPropertyNeedsJustify(p))
[ - + ]
547 : : {
548 : 0 : notifyPreprocessedAssertion(n, false);
549 : 0 : notifyPreprocessedAssertions(skAsserts, false);
550 : : }
551 : : // notice that we may be in FULL or STANDARD effort here.
552 [ + + ]: 908 : if (d_dman != nullptr)
553 : : {
554 : : // notice that we don't compute relevance here, instead it is computed
555 : : // on demand based on the literals in n.
556 : 591 : d_dman->notifyLemma(n, d_inFullEffortCheck);
557 : : }
558 : 908 : }
559 : :
560 : 401 : bool RelevanceManager::needsCandidateModel()
561 : : {
562 [ + + ]: 401 : if (d_dman != nullptr)
563 : : {
564 : 287 : return d_dman->needsCandidateModel();
565 : : }
566 : 114 : return false;
567 : : }
568 : 24 : void RelevanceManager::notifyCandidateModel(TheoryModel* m)
569 : : {
570 [ + - ]: 24 : if (d_dman != nullptr)
571 : : {
572 : 24 : d_dman->notifyCandidateModel(m);
573 : : }
574 : 24 : }
575 : :
576 : 454 : void RelevanceManager::getDifficultyMap(std::map<Node, Node>& dmap,
577 : : bool includeLemmas)
578 : : {
579 [ + - ]: 454 : if (d_dman != nullptr)
580 : : {
581 : 454 : d_dman->getDifficultyMap(dmap, includeLemmas);
582 : : }
583 : 454 : }
584 : :
585 : : } // namespace theory
586 : : } // namespace cvc5::internal
|
