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 : 655252 : TheoryInferenceManager::TheoryInferenceManager(Env& env,
35 : : Theory& t,
36 : : TheoryState& state,
37 : : const std::string& statsName,
38 : 655252 : bool cacheLemmas)
39 : : : EnvObj(env),
40 : : d_theory(t),
41 : : d_theoryState(state),
42 : 655252 : 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 : 1310500 : d_lemmasSent(userContext()),
49 : : d_numConflicts(0),
50 : : d_numCurrentLemmas(0),
51 : : d_numCurrentFacts(0),
52 : 1310500 : d_conflictIdStats(statisticsRegistry().registerHistogram<InferenceId>(
53 : 655252 : statsName + "inferencesConflict")),
54 : 655252 : d_factIdStats(statisticsRegistry().registerHistogram<InferenceId>(
55 : 655252 : statsName + "inferencesFact")),
56 : 655252 : d_lemmaIdStats(statisticsRegistry().registerHistogram<InferenceId>(
57 : 1310500 : statsName + "inferencesLemma"))
58 : : {
59 : : // don't add true lemma
60 : 1310500 : Node truen = nodeManager()->mkConst(true);
61 : 655252 : d_lemmasSent.insert(truen);
62 : :
63 [ + + ]: 655252 : if (isProofEnabled())
64 : : {
65 : 138918 : context::UserContext* u = userContext();
66 : 138918 : d_defaultPg.reset(
67 : 277836 : new EagerProofGenerator(env, u, statsName + "EagerProofGenerator"));
68 : : }
69 : 655252 : }
70 : :
71 : 651924 : TheoryInferenceManager::~TheoryInferenceManager()
72 : : {
73 : 651924 : }
74 : :
75 : 655252 : void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
76 : : {
77 : 655252 : 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 [ + + ][ + + ]: 655252 : if (isProofEnabled() && d_ee != nullptr)
[ + + ]
83 : : {
84 : 124998 : d_pfee = d_ee->getProofEqualityEngine();
85 [ + + ]: 124998 : if (d_pfee == nullptr)
86 : : {
87 : 124688 : d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *d_ee);
88 : 124688 : d_pfee = d_pfeeAlloc.get();
89 : 124688 : d_ee->setProofEqualityEngine(d_pfee);
90 : : }
91 : : }
92 : 655252 : }
93 : :
94 : 655252 : void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
95 : : {
96 : 655252 : d_decManager = dm;
97 : 655252 : }
98 : :
99 : 2011240 : bool TheoryInferenceManager::isProofEnabled() const
100 : : {
101 : 2011240 : return d_env.isTheoryProofProducing();
102 : : }
103 : :
104 : 4960140 : void TheoryInferenceManager::reset()
105 : : {
106 : 4960140 : d_numConflicts = 0;
107 : 4960140 : d_numCurrentLemmas = 0;
108 : 4960140 : d_numCurrentFacts = 0;
109 : 4960140 : }
110 : :
111 : 4094820 : bool TheoryInferenceManager::hasSent() const
112 : : {
113 [ + + ]: 8189620 : return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
114 [ + + ][ - + ]: 8189620 : || d_numCurrentFacts > 0;
115 : : }
116 : :
117 : 0 : eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine() { return d_pfee; }
118 : :
119 : 14535 : void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
120 : : {
121 [ + + ]: 14535 : if (!d_theoryState.isInConflict())
122 : : {
123 : 28962 : TrustNode tconf = explainConflictEqConstantMerge(a, b);
124 : 14481 : trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE);
125 : : }
126 : 14535 : }
127 : :
128 : 24597 : void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
129 : : {
130 : 49194 : TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr);
131 : 49194 : return trustedConflict(tconf, id);
132 : : }
133 : :
134 : 160786 : void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
135 : : {
136 [ - + ][ - + ]: 160786 : Assert(id != InferenceId::UNKNOWN)
[ - - ]
137 : 0 : << "Must provide an inference id for conflict";
138 : 160786 : d_conflictIdStats << id;
139 : 160786 : resourceManager()->spendResource(id);
140 [ + - ][ - + ]: 321572 : Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
[ - - ]
141 : 160786 : << std::endl;
142 : 160786 : d_out.trustedConflict(tconf, id);
143 : 160786 : ++d_numConflicts;
144 : 160786 : }
145 : :
146 : 319 : void TheoryInferenceManager::conflictExp(InferenceId id,
147 : : ProofRule pfr,
148 : : const std::vector<Node>& exp,
149 : : const std::vector<Node>& args)
150 : : {
151 [ + + ]: 319 : if (!d_theoryState.isInConflict())
152 : : {
153 : : // make the trust node
154 : 209 : TrustNode tconf = mkConflictExp(pfr, exp, args);
155 : : // send it on the output channel
156 : 209 : trustedConflict(tconf, id);
157 : : }
158 : 319 : }
159 : :
160 : 209 : TrustNode TheoryInferenceManager::mkConflictExp(ProofRule id,
161 : : const std::vector<Node>& exp,
162 : : const std::vector<Node>& args)
163 : : {
164 [ + + ]: 209 : if (d_pfee != nullptr)
165 : : {
166 : : // use proof equality engine to construct the trust node
167 : 110 : 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 : 2397 : void TheoryInferenceManager::conflictExp(InferenceId id,
175 : : const std::vector<Node>& exp,
176 : : ProofGenerator* pg)
177 : : {
178 [ + + ]: 2397 : if (!d_theoryState.isInConflict())
179 : : {
180 : : // make the trust node
181 : 2201 : TrustNode tconf = mkConflictExp(exp, pg);
182 : : // send it on the output channel
183 : 2201 : trustedConflict(tconf, id);
184 : : }
185 : 2397 : }
186 : :
187 : 5017 : TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
188 : : ProofGenerator* pg)
189 : : {
190 [ + + ]: 5017 : if (d_pfee != nullptr)
191 : : {
192 [ - + ][ - + ]: 2204 : Assert(pg != nullptr);
[ - - ]
193 : : // use proof equality engine to construct the trust node
194 : 2204 : return d_pfee->assertConflict(exp, pg);
195 : : }
196 : : // version without proofs
197 : 2813 : Node conf = mkExplainPartial(exp, {});
198 : 2813 : return TrustNode::mkTrustConflict(conf, nullptr);
199 : : }
200 : :
201 : 17907400 : bool TheoryInferenceManager::propagateLit(TNode lit)
202 : : {
203 : : // If already in conflict, no more propagation
204 [ + + ]: 17907400 : if (d_theoryState.isInConflict())
205 : : {
206 : 2059 : return false;
207 : : }
208 : : // Propagate out
209 : 17905300 : bool ok = d_out.propagate(lit);
210 [ + + ]: 17905300 : if (!ok)
211 : : {
212 : 130158 : d_theoryState.notifyInConflict();
213 : : }
214 : 17905300 : return ok;
215 : : }
216 : :
217 : 405956 : TrustNode TheoryInferenceManager::explainLit(TNode lit)
218 : : {
219 [ + + ]: 405956 : if (d_pfee != nullptr)
220 : : {
221 : 180626 : return d_pfee->explain(lit);
222 : : }
223 [ + - ]: 225330 : if (d_ee != nullptr)
224 : : {
225 : 225330 : Node exp = d_ee->mkExplainLit(lit);
226 : 225330 : 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 : 14481 : TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
235 : : TNode b)
236 : : {
237 : 28962 : Node lit = a.eqNode(b);
238 [ + + ]: 14481 : if (d_pfee != nullptr)
239 : : {
240 : 6629 : return d_pfee->assertConflict(lit);
241 : : }
242 [ + - ]: 7852 : if (d_ee != nullptr)
243 : : {
244 : 7852 : Node conf = d_ee->mkExplainLit(lit);
245 : 7852 : return TrustNode::mkTrustConflict(conf, nullptr);
246 : : }
247 : 0 : Unimplemented() << "Inference manager for " << d_theory.getId()
248 : 0 : << " mkTrustedConflictEqConstantMerge";
249 : : }
250 : :
251 : 369840 : bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p)
252 : : {
253 : 739680 : TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
254 : 739680 : return trustedLemma(tlem, id, p);
255 : : }
256 : :
257 : 1954920 : 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 [ + + ]: 1954920 : if (d_cacheLemmas)
264 : : {
265 [ + + ]: 1924160 : if (!cacheLemma(tlem.getNode(), p))
266 : : {
267 : 1292460 : return false;
268 : : }
269 : : }
270 [ - + ][ - + ]: 662468 : Assert(id != InferenceId::UNKNOWN)
[ - - ]
271 : 0 : << "Must provide an inference id for lemma";
272 : 662468 : d_lemmaIdStats << id;
273 : 662468 : resourceManager()->spendResource(id);
274 [ + - ][ - + ]: 662468 : Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
[ - - ]
275 : : // shouldn't send trivially true or false lemmas
276 [ - + ][ - + ]: 662468 : Assert(!rewrite(tlem.getProven()).isConst());
[ - - ]
277 : 662468 : d_numCurrentLemmas++;
278 : 662468 : d_out.trustedLemma(tlem, id, p);
279 : 662467 : 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 : 2043 : 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 [ + + ]: 2043 : if (d_pfee != nullptr)
303 : : {
304 : : // make the trust node from the proof equality engine
305 : 835 : 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 : 37998 : TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
327 : : const std::vector<Node>& exp,
328 : : const std::vector<Node>& noExplain,
329 : : ProofGenerator* pg)
330 : : {
331 [ + + ]: 37998 : if (d_pfee != nullptr)
332 : : {
333 : : // make the trust node from the proof equality engine
334 : 14918 : return d_pfee->assertLemma(conc, exp, noExplain, pg);
335 : : }
336 : : // otherwise, not using proofs, explain and make trust node
337 : 46160 : Node ant = mkExplainPartial(exp, noExplain);
338 : 46160 : Node lem = nodeManager()->mkNode(Kind::IMPLIES, ant, conc);
339 : 23080 : return TrustNode::mkTrustLemma(lem, nullptr);
340 : : }
341 : :
342 : 649821 : bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
343 : : {
344 : 649821 : Node rewritten = rewrite(lem);
345 : 1299640 : 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 : 1214820 : bool TheoryInferenceManager::hasSentLemma() const
354 : : {
355 : 1214820 : return d_numCurrentLemmas != 0;
356 : : }
357 : :
358 : 18522 : bool TheoryInferenceManager::assertInternalFact(TNode atom,
359 : : bool pol,
360 : : InferenceId id,
361 : : TNode exp)
362 : : {
363 : 55566 : return processInternalFact(
364 : 55566 : atom, pol, id, ProofRule::UNKNOWN, {exp}, {}, nullptr);
365 : : }
366 : :
367 : 39089 : 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 [ - + ][ - + ]: 39089 : Assert(pfr != ProofRule::UNKNOWN);
[ - - ]
375 : 39089 : return processInternalFact(atom, pol, id, pfr, exp, args, nullptr);
376 : : }
377 : :
378 : 405292 : bool TheoryInferenceManager::assertInternalFact(TNode atom,
379 : : bool pol,
380 : : InferenceId id,
381 : : const std::vector<Node>& exp,
382 : : ProofGenerator* pg)
383 : : {
384 : 405292 : return processInternalFact(atom, pol, id, ProofRule::ASSUME, exp, {}, pg);
385 : : }
386 : :
387 : 462903 : 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 [ - + ][ - + ]: 462903 : Assert(iid != InferenceId::UNKNOWN)
[ - - ]
396 : 0 : << "Must provide an inference id for fact";
397 : 462903 : d_factIdStats << iid;
398 : 462903 : resourceManager()->spendResource(iid);
399 : : // make the node corresponding to the explanation
400 : 925806 : Node expn = nodeManager()->mkAnd(exp);
401 [ + - ][ - - ]: 925806 : Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
[ - + ][ - - ]
402 : 462903 : << " " << expn << ")" << std::endl;
403 : : // call the pre-notify fact method with preReg = false, isInternal = true
404 [ - + ]: 462903 : 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 [ - + ][ - + ]: 462903 : Assert(d_ee != nullptr);
[ - - ]
411 [ + - ]: 925806 : Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
412 [ - - ][ - + ]: 462903 : << (pol ? Node(atom) : atom.notNode()) << " from "
[ - - ]
413 : 462903 : << expn << " / " << iid << " " << id << std::endl;
414 [ + - ]: 462903 : 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 : 925806 : std::vector<Node> expc = exp;
419 [ + + ]: 1380900 : for (size_t i = 0; i < expc.size(); i++)
420 : : {
421 : 918002 : Node e = expc[i];
422 : 918002 : bool epol = e.getKind() != Kind::NOT;
423 [ + + ]: 918002 : Node eatom = epol ? e : e[0];
424 [ + - ]: 1836000 : Trace("infer-manager")
425 : 918002 : << "...check " << eatom << " " << epol << std::endl;
426 [ + + ]: 918002 : if (eatom.getKind() == Kind::AND)
427 : : {
428 [ - + ][ - + ]: 61751 : Assert(epol);
[ - - ]
429 [ + + ]: 476018 : for (const Node& ea : eatom)
430 : : {
431 : 414267 : expc.push_back(ea);
432 : : }
433 : 61751 : continue;
434 : : }
435 [ + + ]: 856251 : else if (eatom.getKind() == Kind::EQUAL)
436 : : {
437 [ - + ][ - + ]: 257799 : Assert(d_ee->hasTerm(eatom[0]));
[ - - ]
438 [ - + ][ - + ]: 257799 : Assert(d_ee->hasTerm(eatom[1]));
[ - - ]
439 : 257799 : Assert(!epol || d_ee->areEqual(eatom[0], eatom[1]));
440 : 257799 : Assert(epol || d_ee->areDisequal(eatom[0], eatom[1], false));
441 : : }
442 : : else
443 : : {
444 [ - + ][ - + ]: 598452 : Assert(d_ee->hasTerm(eatom));
[ - - ]
445 [ - + ][ - + ]: 598452 : Assert(d_ee->areEqual(eatom, nodeManager()->mkConst(epol)));
[ - - ]
446 : : }
447 : : }
448 : : }
449 : 462903 : d_numCurrentFacts++;
450 : : // Now, assert the fact. How to do so depends on whether proofs are enabled.
451 : 462903 : bool ret = false;
452 [ + + ]: 462903 : if (d_pfee == nullptr)
453 : : {
454 [ + - ]: 355412 : Trace("infer-manager") << "...assert without proofs..." << std::endl;
455 [ + + ]: 355412 : if (atom.getKind() == Kind::EQUAL)
456 : : {
457 : 279756 : ret = d_ee->assertEquality(atom, pol, expn);
458 : : }
459 : : else
460 : : {
461 : 75656 : 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 : 355412 : d_keep.insert(atom);
469 : 355412 : d_keep.insert(expn);
470 : : }
471 : : else
472 : : {
473 [ - + ][ - + ]: 107491 : Assert(id != ProofRule::UNKNOWN);
[ - - ]
474 [ + - ]: 107491 : 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 [ + + ]: 214982 : Node lit = pol ? Node(atom) : atom.notNode();
480 [ + + ]: 107491 : if (pg != nullptr)
481 : : {
482 : : // use the proof generator interface
483 : 79870 : ret = d_pfee->assertFact(lit, expn, pg);
484 : : }
485 : : else
486 : : {
487 : : // use the explict proof step interface
488 : 27621 : ret = d_pfee->assertFact(lit, id, expn, args);
489 : : }
490 : : }
491 : : // call the notify fact method with isInternal = true
492 : 462903 : d_theory.notifyFact(atom, pol, expn, true);
493 [ + - ]: 925806 : Trace("infer-manager")
494 : 0 : << "TheoryInferenceManager::finished assertInternalFact, ret=" << ret
495 : 462903 : << std::endl;
496 : 462903 : return ret;
497 : : }
498 : :
499 : 66104 : void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
500 : : {
501 [ - + ]: 66104 : 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 : 66104 : d_ee->explainLit(n, assumptions);
511 : : }
512 : 66104 : }
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 : 27200 : Node TheoryInferenceManager::mkExplainPartial(
522 : : const std::vector<Node>& exp, const std::vector<Node>& noExplain)
523 : : {
524 : 54400 : std::vector<TNode> assumps;
525 [ + + ]: 95335 : for (const Node& e : exp)
526 : : {
527 [ + + ]: 68135 : if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
528 : : {
529 [ + - ]: 2407 : if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
530 : : {
531 : : // a non-explained literal
532 : 2407 : assumps.push_back(e);
533 : : }
534 : 2407 : continue;
535 : : }
536 : : // otherwise, explain it
537 : 65728 : explain(e, assumps);
538 : : }
539 : 54400 : return nodeManager()->mkAnd(assumps);
540 : : }
541 : :
542 : 0 : uint32_t TheoryInferenceManager::numSentFacts() const
543 : : {
544 : 0 : return d_numCurrentFacts;
545 : : }
546 : :
547 : 196810 : bool TheoryInferenceManager::hasSentFact() const
548 : : {
549 : 196810 : return d_numCurrentFacts != 0;
550 : : }
551 : :
552 : 1924160 : bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
553 : : {
554 : 3848310 : Node rewritten = rewrite(lem);
555 [ + + ]: 1924160 : if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
556 : : {
557 : 1292460 : return false;
558 : : }
559 : 631700 : d_lemmasSent.insert(rewritten);
560 : 631700 : return true;
561 : : }
562 : :
563 : 52508 : DecisionManager* TheoryInferenceManager::getDecisionManager()
564 : : {
565 : 52508 : return d_decManager;
566 : : }
567 : :
568 : 69192 : void TheoryInferenceManager::preferPhase(TNode n, bool pol)
569 : : {
570 : 138384 : Node en = d_theoryState.getValuation().ensureLiteral(n);
571 : 138384 : return d_out.preferPhase(en, pol);
572 : : }
573 : :
574 : 355213 : void TheoryInferenceManager::spendResource(Resource r)
575 : : {
576 : 355213 : d_out.spendResource(r);
577 : 355213 : }
578 : :
579 : 156468 : void TheoryInferenceManager::safePoint(Resource r)
580 : : {
581 : 156468 : d_out.safePoint(r);
582 : 156468 : }
583 : :
584 : 9186 : void TheoryInferenceManager::setModelUnsound(IncompleteId id)
585 : : {
586 : 9186 : d_out.setModelUnsound(id);
587 : 9186 : }
588 : :
589 : 119 : void TheoryInferenceManager::setRefutationUnsound(IncompleteId id)
590 : : {
591 : 119 : d_out.setRefutationUnsound(id);
592 : 119 : }
593 : :
594 : 1985290 : void TheoryInferenceManager::notifyInConflict()
595 : : {
596 : 1985290 : d_theoryState.notifyInConflict();
597 : 1985290 : }
598 : :
599 : : } // namespace theory
600 : : } // namespace cvc5::internal
|
