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