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 : : * An inference manager for Theory.
11 : : */
12 : :
13 : : #include "theory/theory_inference_manager.h"
14 : :
15 : : #include "options/proof_options.h"
16 : : #include "proof/eager_proof_generator.h"
17 : : #include "proof/trust_id.h"
18 : : #include "theory/builtin/proof_checker.h"
19 : : #include "theory/output_channel.h"
20 : : #include "theory/rewriter.h"
21 : : #include "theory/theory.h"
22 : : #include "theory/theory_state.h"
23 : : #include "theory/uf/equality_engine.h"
24 : : #include "theory/uf/proof_equality_engine.h"
25 : :
26 : : using namespace cvc5::internal::kind;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : :
31 : 667732 : TheoryInferenceManager::TheoryInferenceManager(Env& env,
32 : : Theory& t,
33 : : TheoryState& state,
34 : : const std::string& statsName,
35 : 667732 : bool cacheLemmas)
36 : : : EnvObj(env),
37 : 667732 : d_theory(t),
38 : 667732 : d_theoryState(state),
39 : 1335464 : d_out(t.getOutputChannel()),
40 : 667732 : d_ee(nullptr),
41 : 667732 : d_decManager(nullptr),
42 : 667732 : d_pfee(nullptr),
43 : 667732 : d_cacheLemmas(cacheLemmas),
44 : 667732 : d_keep(context()),
45 : 667732 : d_lemmasSent(userContext()),
46 : 667732 : d_numConflicts(0),
47 : 667732 : d_numCurrentLemmas(0),
48 : 667732 : d_numCurrentFacts(0),
49 : 1335464 : d_conflictIdStats(statisticsRegistry().registerHistogram<InferenceId>(
50 : 1335464 : statsName + "inferencesConflict")),
51 : 1335464 : d_factIdStats(statisticsRegistry().registerHistogram<InferenceId>(
52 : 1335464 : statsName + "inferencesFact")),
53 : 1335464 : d_lemmaIdStats(statisticsRegistry().registerHistogram<InferenceId>(
54 : 2003196 : statsName + "inferencesLemma"))
55 : : {
56 : : // don't add true lemma
57 : 667732 : Node truen = nodeManager()->mkConst(true);
58 : 667732 : d_lemmasSent.insert(truen);
59 : :
60 [ + + ]: 667732 : if (isProofEnabled())
61 : : {
62 : 141531 : context::UserContext* u = userContext();
63 : 141531 : d_defaultPg.reset(
64 : 283062 : new EagerProofGenerator(env, u, statsName + "EagerProofGenerator"));
65 : : }
66 : 667732 : }
67 : :
68 : 663208 : TheoryInferenceManager::~TheoryInferenceManager() {}
69 : :
70 : 667732 : void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
71 : : {
72 : 667732 : d_ee = ee;
73 : : // if proofs are enabled, also make a proof equality engine to wrap ee
74 : : // if it is non-null. If its proof equality engine has already been assigned,
75 : : // use it. This is to ensure that all theories use the same proof equality
76 : : // engine when in ee-mode=central.
77 [ + + ][ + + ]: 667732 : if (isProofEnabled() && d_ee != nullptr)
[ + + ]
78 : : {
79 : 128002 : d_pfee = d_ee->getProofEqualityEngine();
80 [ + + ]: 128002 : if (d_pfee == nullptr)
81 : : {
82 : 127722 : d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *d_ee);
83 : 127722 : d_pfee = d_pfeeAlloc.get();
84 : 127722 : d_ee->setProofEqualityEngine(d_pfee);
85 : : }
86 : : }
87 : 667732 : }
88 : :
89 : 667732 : void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
90 : : {
91 : 667732 : d_decManager = dm;
92 : 667732 : }
93 : :
94 : 2158476 : bool TheoryInferenceManager::isProofEnabled() const
95 : : {
96 : 2158476 : return d_env.isTheoryProofProducing();
97 : : }
98 : :
99 : 5470796 : void TheoryInferenceManager::reset()
100 : : {
101 : 5470796 : d_numConflicts = 0;
102 : 5470796 : d_numCurrentLemmas = 0;
103 : 5470796 : d_numCurrentFacts = 0;
104 : 5470796 : }
105 : :
106 : 4406067 : bool TheoryInferenceManager::hasSent() const
107 : : {
108 [ + + ]: 8812126 : return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
109 [ + + ][ - + ]: 8812126 : || d_numCurrentFacts > 0;
110 : : }
111 : :
112 : 0 : eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine() { return d_pfee; }
113 : :
114 : 14526 : void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
115 : : {
116 [ + + ]: 14526 : if (!d_theoryState.isInConflict())
117 : : {
118 : 29048 : TrustNode tconf = explainConflictEqConstantMerge(a, b);
119 : 14524 : trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE);
120 : 14524 : }
121 : 14526 : }
122 : :
123 : 3804 : void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
124 : : {
125 : 3804 : TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr);
126 : 7608 : return trustedConflict(tconf, id);
127 : 3804 : }
128 : :
129 : 174306 : void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
130 : : {
131 [ - + ][ - + ]: 174306 : Assert(id != InferenceId::UNKNOWN)
[ - - ]
132 : 0 : << "Must provide an inference id for conflict";
133 : 174306 : d_conflictIdStats << id;
134 : 174306 : resourceManager()->spendResource(id);
135 [ + - ][ - + ]: 348612 : Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
[ - - ]
136 : 174306 : << std::endl;
137 : 174306 : d_out.trustedConflict(tconf, id);
138 : 174306 : ++d_numConflicts;
139 : 174306 : }
140 : :
141 : 284 : void TheoryInferenceManager::conflictExp(InferenceId id,
142 : : ProofRule pfr,
143 : : const std::vector<Node>& exp,
144 : : const std::vector<Node>& args)
145 : : {
146 [ + + ]: 284 : if (!d_theoryState.isInConflict())
147 : : {
148 : : // make the trust node
149 : 187 : TrustNode tconf = mkConflictExp(pfr, exp, args);
150 : : // send it on the output channel
151 : 187 : trustedConflict(tconf, id);
152 : 187 : }
153 : 284 : }
154 : :
155 : 187 : TrustNode TheoryInferenceManager::mkConflictExp(ProofRule id,
156 : : const std::vector<Node>& exp,
157 : : const std::vector<Node>& args)
158 : : {
159 [ + + ]: 187 : if (d_pfee != nullptr)
160 : : {
161 : : // use proof equality engine to construct the trust node
162 : 88 : return d_pfee->assertConflict(id, exp, args);
163 : : }
164 : : // version without proofs
165 : 99 : Node conf = mkExplainPartial(exp, {});
166 : 99 : return TrustNode::mkTrustConflict(conf, nullptr);
167 : 99 : }
168 : :
169 : 6822 : void TheoryInferenceManager::conflictExp(InferenceId id,
170 : : const std::vector<Node>& exp,
171 : : ProofGenerator* pg)
172 : : {
173 [ + + ]: 6822 : if (!d_theoryState.isInConflict())
174 : : {
175 : : // make the trust node
176 : 6624 : TrustNode tconf = mkConflictExp(exp, pg);
177 : : // send it on the output channel
178 : 6624 : trustedConflict(tconf, id);
179 : 6624 : }
180 : 6822 : }
181 : :
182 : 10206 : TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
183 : : ProofGenerator* pg)
184 : : {
185 [ + + ]: 10206 : if (d_pfee != nullptr)
186 : : {
187 [ - + ][ - + ]: 5084 : Assert(pg != nullptr);
[ - - ]
188 : : // use proof equality engine to construct the trust node
189 : 5084 : return d_pfee->assertConflict(exp, pg);
190 : : }
191 : : // version without proofs
192 : 5122 : Node conf = mkExplainPartial(exp, {});
193 : 5122 : return TrustNode::mkTrustConflict(conf, nullptr);
194 : 5122 : }
195 : :
196 : 21209835 : bool TheoryInferenceManager::propagateLit(TNode lit)
197 : : {
198 : : // If already in conflict, no more propagation
199 [ + + ]: 21209835 : if (d_theoryState.isInConflict())
200 : : {
201 : 2177 : return false;
202 : : }
203 : : // Propagate out
204 : 21207658 : bool ok = d_out.propagate(lit);
205 [ + + ]: 21207658 : if (!ok)
206 : : {
207 : 125579 : d_theoryState.notifyInConflict();
208 : : }
209 : 21207658 : return ok;
210 : : }
211 : :
212 : 458312 : TrustNode TheoryInferenceManager::explainLit(TNode lit)
213 : : {
214 [ + + ]: 458312 : if (d_pfee != nullptr)
215 : : {
216 : 182824 : return d_pfee->explain(lit);
217 : : }
218 [ + - ]: 275488 : if (d_ee != nullptr)
219 : : {
220 : 275488 : Node exp = d_ee->mkExplainLit(lit);
221 : 275488 : return TrustNode::mkTrustPropExp(lit, exp, nullptr);
222 : 275488 : }
223 : 0 : Unimplemented() << "Inference manager for " << d_theory.getId()
224 : : << " was asked to explain a propagation but doesn't have an "
225 : : "equality engine or implement the "
226 : 0 : "TheoryInferenceManager::explainLit interface!";
227 : : }
228 : :
229 : 14524 : TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
230 : : TNode b)
231 : : {
232 : 14524 : Node lit = a.eqNode(b);
233 [ + + ]: 14524 : if (d_pfee != nullptr)
234 : : {
235 : 5773 : return d_pfee->assertConflict(lit);
236 : : }
237 [ + - ]: 8751 : if (d_ee != nullptr)
238 : : {
239 : 8751 : Node conf = d_ee->mkExplainLit(lit);
240 : 8751 : return TrustNode::mkTrustConflict(conf, nullptr);
241 : 8751 : }
242 : 0 : Unimplemented() << "Inference manager for " << d_theory.getId()
243 : 0 : << " mkTrustedConflictEqConstantMerge";
244 : 14524 : }
245 : :
246 : 455677 : bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p)
247 : : {
248 : 455677 : TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
249 : 911354 : return trustedLemma(tlem, id, p);
250 : 455677 : }
251 : :
252 : 3166199 : bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
253 : : InferenceId id,
254 : : LemmaProperty p)
255 : : {
256 : : // if the policy says to cache lemmas, check the cache and return false if
257 : : // we are a duplicate
258 [ + + ][ + - ]: 3166199 : if (d_cacheLemmas && !isLemmaPropertyLocal(p))
[ + + ]
259 : : {
260 [ + + ]: 3127246 : if (!cacheLemma(tlem.getNode(), p))
261 : : {
262 : 2452864 : return false;
263 : : }
264 : : }
265 [ - + ][ - + ]: 713335 : Assert(id != InferenceId::UNKNOWN)
[ - - ]
266 : 0 : << "Must provide an inference id for lemma";
267 : 713335 : d_lemmaIdStats << id;
268 : 713335 : resourceManager()->spendResource(id);
269 [ + - ][ - + ]: 713335 : Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
[ - - ]
270 : : // shouldn't send trivially true or false lemmas
271 [ - + ][ - + ]: 713335 : Assert(!rewrite(tlem.getProven()).isConst());
[ - - ]
272 : 713335 : d_numCurrentLemmas++;
273 : 713335 : d_out.trustedLemma(tlem, id, p);
274 : 713334 : return true;
275 : : }
276 : :
277 : 0 : bool TheoryInferenceManager::lemmaExp(Node conc,
278 : : InferenceId id,
279 : : ProofRule pfr,
280 : : const std::vector<Node>& exp,
281 : : const std::vector<Node>& noExplain,
282 : : const std::vector<Node>& args,
283 : : LemmaProperty p)
284 : : {
285 : : // make the trust node
286 : 0 : TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
287 : : // send it on the output channel
288 : 0 : return trustedLemma(trn, id, p);
289 : 0 : }
290 : :
291 : 1878 : TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
292 : : ProofRule id,
293 : : const std::vector<Node>& exp,
294 : : const std::vector<Node>& noExplain,
295 : : const std::vector<Node>& args)
296 : : {
297 [ + + ]: 1878 : if (d_pfee != nullptr)
298 : : {
299 : : // make the trust node from the proof equality engine
300 : 668 : return d_pfee->assertLemma(conc, id, exp, noExplain, args);
301 : : }
302 : : // otherwise, not using proofs, explain and make trust node
303 : 1210 : Node ant = mkExplainPartial(exp, noExplain);
304 : 2420 : Node lem = nodeManager()->mkNode(Kind::IMPLIES, ant, conc);
305 : 1210 : return TrustNode::mkTrustLemma(lem, nullptr);
306 : 1210 : }
307 : :
308 : 0 : bool TheoryInferenceManager::lemmaExp(Node conc,
309 : : InferenceId id,
310 : : const std::vector<Node>& exp,
311 : : const std::vector<Node>& noExplain,
312 : : ProofGenerator* pg,
313 : : LemmaProperty p)
314 : : {
315 : : // make the trust node
316 : 0 : TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
317 : : // send it on the output channel
318 : 0 : return trustedLemma(trn, id, p);
319 : 0 : }
320 : :
321 : 45687 : TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
322 : : const std::vector<Node>& exp,
323 : : const std::vector<Node>& noExplain,
324 : : ProofGenerator* pg)
325 : : {
326 [ + + ]: 45687 : if (d_pfee != nullptr)
327 : : {
328 : : // make the trust node from the proof equality engine
329 : 18065 : return d_pfee->assertLemma(conc, exp, noExplain, pg);
330 : : }
331 : : // otherwise, not using proofs, explain and make trust node
332 : 27622 : Node ant = mkExplainPartial(exp, noExplain);
333 : 55244 : Node lem = nodeManager()->mkNode(Kind::IMPLIES, ant, conc);
334 : 27622 : return TrustNode::mkTrustLemma(lem, nullptr);
335 : 27622 : }
336 : :
337 : 661857 : bool TheoryInferenceManager::hasCachedLemma(TNode lem,
338 : : CVC5_UNUSED LemmaProperty p)
339 : : {
340 : 661857 : Node rewritten = rewrite(lem);
341 : 1323714 : return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
342 : 661857 : }
343 : :
344 : 0 : uint32_t TheoryInferenceManager::numSentLemmas() const
345 : : {
346 : 0 : return d_numCurrentLemmas;
347 : : }
348 : :
349 : 1373114 : bool TheoryInferenceManager::hasSentLemma() const
350 : : {
351 : 1373114 : return d_numCurrentLemmas != 0;
352 : : }
353 : :
354 : 21627 : bool TheoryInferenceManager::assertInternalFact(TNode atom,
355 : : bool pol,
356 : : InferenceId id,
357 : : TNode exp)
358 : : {
359 : 64881 : return processInternalFact(
360 : 43254 : atom, pol, id, ProofRule::UNKNOWN, {exp}, {}, nullptr);
361 : : }
362 : :
363 : 57392 : bool TheoryInferenceManager::assertInternalFact(TNode atom,
364 : : bool pol,
365 : : InferenceId id,
366 : : ProofRule pfr,
367 : : const std::vector<Node>& exp,
368 : : const std::vector<Node>& args)
369 : : {
370 [ - + ][ - + ]: 57392 : Assert(pfr != ProofRule::UNKNOWN);
[ - - ]
371 : 57392 : return processInternalFact(atom, pol, id, pfr, exp, args, nullptr);
372 : : }
373 : :
374 : 487470 : bool TheoryInferenceManager::assertInternalFact(TNode atom,
375 : : bool pol,
376 : : InferenceId id,
377 : : const std::vector<Node>& exp,
378 : : ProofGenerator* pg)
379 : : {
380 : 487470 : return processInternalFact(atom, pol, id, ProofRule::ASSUME, exp, {}, pg);
381 : : }
382 : :
383 : 566489 : bool TheoryInferenceManager::processInternalFact(TNode atom,
384 : : bool pol,
385 : : InferenceId iid,
386 : : ProofRule id,
387 : : const std::vector<Node>& exp,
388 : : const std::vector<Node>& args,
389 : : ProofGenerator* pg)
390 : : {
391 [ - + ][ - + ]: 566489 : Assert(iid != InferenceId::UNKNOWN)
[ - - ]
392 : 0 : << "Must provide an inference id for fact";
393 : 566489 : d_factIdStats << iid;
394 : 566489 : resourceManager()->spendResource(iid);
395 : : // make the node corresponding to the explanation
396 : 566489 : Node expn = nodeManager()->mkAnd(exp);
397 [ + - ][ - - ]: 1132978 : Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
[ - + ][ - - ]
398 : 566489 : << " " << expn << ")" << std::endl;
399 : : // call the pre-notify fact method with preReg = false, isInternal = true
400 [ - + ]: 566489 : if (d_theory.preNotifyFact(atom, pol, expn, false, true))
401 : : {
402 : : // Handled in a theory-specific way that doesn't require equality engine,
403 : : // notice we return true, indicating that the fact was processed.
404 : 0 : return true;
405 : : }
406 [ - + ][ - + ]: 566489 : Assert(d_ee != nullptr);
[ - - ]
407 [ + - ]: 1132978 : Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
408 [ - - ][ - + ]: 566489 : << (pol ? Node(atom) : atom.notNode()) << " from "
[ - - ]
409 : 566489 : << expn << " / " << iid << " " << id << std::endl;
410 [ + - ]: 566489 : if (Configuration::isAssertionBuild())
411 : : {
412 : : // check that all facts hold in the equality engine, to ensure that we
413 : : // aren't processing a stale fact
414 : 566489 : std::vector<Node> expc = exp;
415 [ + + ]: 1577133 : for (size_t i = 0; i < expc.size(); i++)
416 : : {
417 : 1010644 : Node e = expc[i];
418 : 1010644 : bool epol = e.getKind() != Kind::NOT;
419 [ + + ]: 1010644 : Node eatom = epol ? e : e[0];
420 [ + - ]: 2021288 : Trace("infer-manager")
421 : 1010644 : << "...check " << eatom << " " << epol << std::endl;
422 [ + + ]: 1010644 : if (eatom.getKind() == Kind::AND)
423 : : {
424 [ - + ][ - + ]: 54999 : Assert(epol);
[ - - ]
425 [ + + ]: 471890 : for (const Node& ea : eatom)
426 : : {
427 : 416891 : expc.push_back(ea);
428 : 416891 : }
429 : 54999 : continue;
430 : 54999 : }
431 [ + + ]: 955645 : else if (eatom.getKind() == Kind::EQUAL)
432 : : {
433 [ - + ][ - + ]: 352366 : Assert(d_ee->hasTerm(eatom[0]));
[ - - ]
434 [ - + ][ - + ]: 352366 : Assert(d_ee->hasTerm(eatom[1]));
[ - - ]
435 : 352366 : Assert(!epol || d_ee->areEqual(eatom[0], eatom[1]));
436 : 352366 : Assert(epol || d_ee->areDisequal(eatom[0], eatom[1], false));
437 : : }
438 : : else
439 : : {
440 [ - + ][ - + ]: 603279 : Assert(d_ee->hasTerm(eatom));
[ - - ]
441 [ - + ][ - + ]: 603279 : Assert(d_ee->areEqual(eatom, nodeManager()->mkConst(epol)));
[ - - ]
442 : : }
443 [ + + ][ + + ]: 1065643 : }
444 : 566489 : }
445 : 566489 : d_numCurrentFacts++;
446 : : // Now, assert the fact. How to do so depends on whether proofs are enabled.
447 : 566489 : bool ret = false;
448 [ + + ]: 566489 : if (d_pfee == nullptr)
449 : : {
450 [ + - ]: 373798 : Trace("infer-manager") << "...assert without proofs..." << std::endl;
451 [ + + ]: 373798 : if (atom.getKind() == Kind::EQUAL)
452 : : {
453 : 312614 : ret = d_ee->assertEquality(atom, pol, expn);
454 : : }
455 : : else
456 : : {
457 : 61184 : ret = d_ee->assertPredicate(atom, pol, expn);
458 : : }
459 : : // Must reference count the equality and its explanation, which is not done
460 : : // by the equality engine. Notice that we do *not* need to do this for
461 : : // external assertions, which enter as facts in theory check. This is also
462 : : // not done if we are asserting to the proof equality engine, which does
463 : : // this caching itself within ProofEqEngine::assertFact.
464 : 373798 : d_keep.insert(atom);
465 : 373798 : d_keep.insert(expn);
466 : : }
467 : : else
468 : : {
469 [ - + ][ - + ]: 192691 : Assert(id != ProofRule::UNKNOWN);
[ - - ]
470 [ + - ]: 192691 : Trace("infer-manager") << "...assert with proofs..." << std::endl;
471 : : // Note that we reconstruct the original literal lit here, since both the
472 : : // original literal is needed for bookkeeping proofs. It is possible to
473 : : // optimize this so that a few less nodes are created, but at the cost
474 : : // of a more verbose interface to proof equality engine.
475 [ + + ]: 192691 : Node lit = pol ? Node(atom) : atom.notNode();
476 [ + + ]: 192691 : if (pg != nullptr)
477 : : {
478 : : // use the proof generator interface
479 : 154978 : ret = d_pfee->assertFact(lit, expn, pg);
480 : : }
481 : : else
482 : : {
483 : : // use the explict proof step interface
484 : 37713 : ret = d_pfee->assertFact(lit, id, expn, args);
485 : : }
486 : 192691 : }
487 : : // call the notify fact method with isInternal = true
488 : 566489 : d_theory.notifyFact(atom, pol, expn, true);
489 [ + - ]: 1132978 : Trace("infer-manager")
490 : 0 : << "TheoryInferenceManager::finished assertInternalFact, ret=" << ret
491 : 566489 : << std::endl;
492 : 566489 : return ret;
493 : 566489 : }
494 : :
495 : 79969 : void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
496 : : {
497 [ - + ]: 79969 : if (n.getKind() == Kind::AND)
498 : : {
499 [ - - ]: 0 : for (const Node& nc : n)
500 : : {
501 : 0 : d_ee->explainLit(nc, assumptions);
502 : 0 : }
503 : : }
504 : : else
505 : : {
506 : 79969 : d_ee->explainLit(n, assumptions);
507 : : }
508 : 79969 : }
509 : :
510 : 0 : Node TheoryInferenceManager::mkExplain(TNode n)
511 : : {
512 : 0 : std::vector<TNode> assumptions;
513 : 0 : explain(n, assumptions);
514 : 0 : return nodeManager()->mkAnd(assumptions);
515 : 0 : }
516 : :
517 : 34053 : Node TheoryInferenceManager::mkExplainPartial(
518 : : const std::vector<Node>& exp, const std::vector<Node>& noExplain)
519 : : {
520 : 34053 : std::vector<TNode> assumps;
521 [ + + ]: 116159 : for (const Node& e : exp)
522 : : {
523 [ + + ]: 82106 : if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
524 : : {
525 [ + - ]: 2500 : if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
526 : : {
527 : : // a non-explained literal
528 : 2500 : assumps.push_back(e);
529 : : }
530 : 2500 : continue;
531 : : }
532 : : // otherwise, explain it
533 : 79606 : explain(e, assumps);
534 : : }
535 : 68106 : return nodeManager()->mkAnd(assumps);
536 : 34053 : }
537 : :
538 : 0 : uint32_t TheoryInferenceManager::numSentFacts() const
539 : : {
540 : 0 : return d_numCurrentFacts;
541 : : }
542 : :
543 : 221284 : bool TheoryInferenceManager::hasSentFact() const
544 : : {
545 : 221284 : return d_numCurrentFacts != 0;
546 : : }
547 : :
548 : 3127246 : bool TheoryInferenceManager::cacheLemma(TNode lem, CVC5_UNUSED LemmaProperty p)
549 : : {
550 : 3127246 : Node rewritten = rewrite(lem);
551 [ + + ]: 3127246 : if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
552 : : {
553 : 2452864 : return false;
554 : : }
555 : 674382 : d_lemmasSent.insert(rewritten);
556 : 674382 : return true;
557 : 3127246 : }
558 : :
559 : 53471 : DecisionManager* TheoryInferenceManager::getDecisionManager()
560 : : {
561 : 53471 : return d_decManager;
562 : : }
563 : :
564 : 76958 : void TheoryInferenceManager::preferPhase(TNode n, bool pol)
565 : : {
566 : 76958 : Node en = d_theoryState.getValuation().ensureLiteral(n);
567 : 153916 : return d_out.preferPhase(en, pol);
568 : 76958 : }
569 : :
570 : 340242 : void TheoryInferenceManager::spendResource(Resource r)
571 : : {
572 : 340242 : d_out.spendResource(r);
573 : 340242 : }
574 : :
575 : 210007 : void TheoryInferenceManager::safePoint(Resource r) { d_out.safePoint(r); }
576 : :
577 : 671 : void TheoryInferenceManager::markUsed() { d_out.markUsed(); }
578 : :
579 : 3414 : void TheoryInferenceManager::setModelUnsound(IncompleteId id)
580 : : {
581 : 3414 : d_out.setModelUnsound(id);
582 : 3414 : }
583 : :
584 : 133 : void TheoryInferenceManager::setRefutationUnsound(IncompleteId id)
585 : : {
586 : 133 : d_out.setRefutationUnsound(id);
587 : 133 : }
588 : :
589 : 2211270 : void TheoryInferenceManager::notifyInConflict()
590 : : {
591 : 2211270 : d_theoryState.notifyInConflict();
592 : 2211270 : }
593 : :
594 : : } // namespace theory
595 : : } // namespace cvc5::internal
|
