1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 "smt/smt_engine_scope.h" |
19 |
|
#include "smt/smt_statistics_registry.h" |
20 |
|
#include "theory/output_channel.h" |
21 |
|
#include "theory/rewriter.h" |
22 |
|
#include "theory/theory.h" |
23 |
|
#include "theory/theory_state.h" |
24 |
|
#include "theory/uf/equality_engine.h" |
25 |
|
#include "theory/uf/proof_equality_engine.h" |
26 |
|
|
27 |
|
using namespace cvc5::kind; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
|
32 |
108218 |
TheoryInferenceManager::TheoryInferenceManager(Theory& t, |
33 |
|
TheoryState& state, |
34 |
|
ProofNodeManager* pnm, |
35 |
|
const std::string& statsName, |
36 |
108218 |
bool cacheLemmas) |
37 |
|
: d_theory(t), |
38 |
|
d_theoryState(state), |
39 |
108218 |
d_out(t.getOutputChannel()), |
40 |
|
d_ee(nullptr), |
41 |
|
d_decManager(nullptr), |
42 |
|
d_pfee(nullptr), |
43 |
|
d_pnm(pnm), |
44 |
|
d_cacheLemmas(cacheLemmas), |
45 |
|
d_keep(t.getSatContext()), |
46 |
108218 |
d_lemmasSent(t.getUserContext()), |
47 |
|
d_numConflicts(0), |
48 |
|
d_numCurrentLemmas(0), |
49 |
|
d_numCurrentFacts(0), |
50 |
108218 |
d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( |
51 |
216436 |
statsName + "inferencesConflict")), |
52 |
108218 |
d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( |
53 |
216436 |
statsName + "inferencesFact")), |
54 |
108218 |
d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( |
55 |
649308 |
statsName + "inferencesLemma")) |
56 |
|
{ |
57 |
|
// don't add true lemma |
58 |
216436 |
Node truen = NodeManager::currentNM()->mkConst(true); |
59 |
108218 |
d_lemmasSent.insert(truen); |
60 |
108218 |
} |
61 |
|
|
62 |
108218 |
TheoryInferenceManager::~TheoryInferenceManager() |
63 |
|
{ |
64 |
108218 |
} |
65 |
|
|
66 |
108218 |
void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) |
67 |
|
{ |
68 |
108218 |
d_ee = ee; |
69 |
|
// if proofs are enabled, also make a proof equality engine to wrap ee |
70 |
|
// if it is non-null. If its proof equality engine has already been assigned, |
71 |
|
// use it. This is to ensure that all theories use the same proof equality |
72 |
|
// engine when in ee-mode=central. |
73 |
108218 |
if (d_pnm != nullptr && d_ee != nullptr) |
74 |
|
{ |
75 |
11919 |
d_pfee = d_ee->getProofEqualityEngine(); |
76 |
11919 |
if (d_pfee == nullptr) |
77 |
|
{ |
78 |
23712 |
d_pfeeAlloc.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(), |
79 |
11856 |
d_theoryState.getUserContext(), |
80 |
11856 |
*d_ee, |
81 |
23712 |
d_pnm)); |
82 |
11856 |
d_pfee = d_pfeeAlloc.get(); |
83 |
11856 |
d_ee->setProofEqualityEngine(d_pfee); |
84 |
|
} |
85 |
|
} |
86 |
108218 |
} |
87 |
|
|
88 |
108218 |
void TheoryInferenceManager::setDecisionManager(DecisionManager* dm) |
89 |
|
{ |
90 |
108218 |
d_decManager = dm; |
91 |
108218 |
} |
92 |
|
|
93 |
20373 |
bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; } |
94 |
|
|
95 |
771260 |
void TheoryInferenceManager::reset() |
96 |
|
{ |
97 |
771260 |
d_numConflicts = 0; |
98 |
771260 |
d_numCurrentLemmas = 0; |
99 |
771260 |
d_numCurrentFacts = 0; |
100 |
771260 |
} |
101 |
|
|
102 |
201983 |
bool TheoryInferenceManager::hasSent() const |
103 |
|
{ |
104 |
403966 |
return d_theoryState.isInConflict() || d_numCurrentLemmas > 0 |
105 |
394396 |
|| d_numCurrentFacts > 0; |
106 |
|
} |
107 |
|
|
108 |
|
eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine() { return d_pfee; } |
109 |
|
|
110 |
12834 |
void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) |
111 |
|
{ |
112 |
12834 |
if (!d_theoryState.isInConflict()) |
113 |
|
{ |
114 |
25506 |
TrustNode tconf = explainConflictEqConstantMerge(a, b); |
115 |
12753 |
trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE); |
116 |
|
} |
117 |
12834 |
} |
118 |
|
|
119 |
73653 |
void TheoryInferenceManager::conflict(TNode conf, InferenceId id) |
120 |
|
{ |
121 |
147306 |
TrustNode tconf = TrustNode::mkTrustConflict(conf, nullptr); |
122 |
147306 |
return trustedConflict(tconf, id); |
123 |
|
} |
124 |
|
|
125 |
102300 |
void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) |
126 |
|
{ |
127 |
102300 |
d_conflictIdStats << id; |
128 |
102300 |
smt::currentResourceManager()->spendResource(id); |
129 |
204600 |
Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")" |
130 |
102300 |
<< std::endl; |
131 |
102300 |
d_out.trustedConflict(tconf); |
132 |
102300 |
++d_numConflicts; |
133 |
102300 |
} |
134 |
|
|
135 |
8 |
void TheoryInferenceManager::conflictExp(InferenceId id, |
136 |
|
PfRule pfr, |
137 |
|
const std::vector<Node>& exp, |
138 |
|
const std::vector<Node>& args) |
139 |
|
{ |
140 |
8 |
if (!d_theoryState.isInConflict()) |
141 |
|
{ |
142 |
|
// make the trust node |
143 |
16 |
TrustNode tconf = mkConflictExp(pfr, exp, args); |
144 |
|
// send it on the output channel |
145 |
8 |
trustedConflict(tconf, id); |
146 |
|
} |
147 |
8 |
} |
148 |
|
|
149 |
8 |
TrustNode TheoryInferenceManager::mkConflictExp(PfRule id, |
150 |
|
const std::vector<Node>& exp, |
151 |
|
const std::vector<Node>& args) |
152 |
|
{ |
153 |
8 |
if (d_pfee != nullptr) |
154 |
|
{ |
155 |
|
// use proof equality engine to construct the trust node |
156 |
2 |
return d_pfee->assertConflict(id, exp, args); |
157 |
|
} |
158 |
|
// version without proofs |
159 |
12 |
Node conf = mkExplainPartial(exp, {}); |
160 |
6 |
return TrustNode::mkTrustConflict(conf, nullptr); |
161 |
|
} |
162 |
|
|
163 |
2553 |
void TheoryInferenceManager::conflictExp(InferenceId id, |
164 |
|
const std::vector<Node>& exp, |
165 |
|
ProofGenerator* pg) |
166 |
|
{ |
167 |
2553 |
if (!d_theoryState.isInConflict()) |
168 |
|
{ |
169 |
|
// make the trust node |
170 |
4880 |
TrustNode tconf = mkConflictExp(exp, pg); |
171 |
|
// send it on the output channel |
172 |
2440 |
trustedConflict(tconf, id); |
173 |
|
} |
174 |
2553 |
} |
175 |
|
|
176 |
3950 |
TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp, |
177 |
|
ProofGenerator* pg) |
178 |
|
{ |
179 |
3950 |
if (d_pfee != nullptr) |
180 |
|
{ |
181 |
425 |
Assert(pg != nullptr); |
182 |
|
// use proof equality engine to construct the trust node |
183 |
425 |
return d_pfee->assertConflict(exp, pg); |
184 |
|
} |
185 |
|
// version without proofs |
186 |
7050 |
Node conf = mkExplainPartial(exp, {}); |
187 |
3525 |
return TrustNode::mkTrustConflict(conf, nullptr); |
188 |
|
} |
189 |
|
|
190 |
8228111 |
bool TheoryInferenceManager::propagateLit(TNode lit) |
191 |
|
{ |
192 |
|
// If already in conflict, no more propagation |
193 |
8228111 |
if (d_theoryState.isInConflict()) |
194 |
|
{ |
195 |
1437 |
return false; |
196 |
|
} |
197 |
|
// Propagate out |
198 |
8226674 |
bool ok = d_out.propagate(lit); |
199 |
8226674 |
if (!ok) |
200 |
|
{ |
201 |
61945 |
d_theoryState.notifyInConflict(); |
202 |
|
} |
203 |
8226674 |
return ok; |
204 |
|
} |
205 |
|
|
206 |
201400 |
TrustNode TheoryInferenceManager::explainLit(TNode lit) |
207 |
|
{ |
208 |
201400 |
if (d_pfee != nullptr) |
209 |
|
{ |
210 |
32435 |
return d_pfee->explain(lit); |
211 |
|
} |
212 |
168965 |
if (d_ee != nullptr) |
213 |
|
{ |
214 |
337930 |
Node exp = d_ee->mkExplainLit(lit); |
215 |
168965 |
return TrustNode::mkTrustPropExp(lit, exp, nullptr); |
216 |
|
} |
217 |
|
Unimplemented() << "Inference manager for " << d_theory.getId() |
218 |
|
<< " was asked to explain a propagation but doesn't have an " |
219 |
|
"equality engine or implement the " |
220 |
|
"TheoryInferenceManager::explainLit interface!"; |
221 |
|
} |
222 |
|
|
223 |
12753 |
TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a, |
224 |
|
TNode b) |
225 |
|
{ |
226 |
25506 |
Node lit = a.eqNode(b); |
227 |
12753 |
if (d_pfee != nullptr) |
228 |
|
{ |
229 |
1535 |
return d_pfee->assertConflict(lit); |
230 |
|
} |
231 |
11218 |
if (d_ee != nullptr) |
232 |
|
{ |
233 |
22436 |
Node conf = d_ee->mkExplainLit(lit); |
234 |
11218 |
return TrustNode::mkTrustConflict(conf, nullptr); |
235 |
|
} |
236 |
|
Unimplemented() << "Inference manager for " << d_theory.getId() |
237 |
|
<< " mkTrustedConflictEqConstantMerge"; |
238 |
|
} |
239 |
|
|
240 |
1370044 |
bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p) |
241 |
|
{ |
242 |
2740087 |
TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr); |
243 |
2740087 |
return trustedLemma(tlem, id, p); |
244 |
|
} |
245 |
|
|
246 |
1691995 |
bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, |
247 |
|
InferenceId id, |
248 |
|
LemmaProperty p) |
249 |
|
{ |
250 |
|
// if the policy says to cache lemmas, check the cache and return false if |
251 |
|
// we are a duplicate |
252 |
1691995 |
if (d_cacheLemmas) |
253 |
|
{ |
254 |
1639895 |
if (!cacheLemma(tlem.getNode(), p)) |
255 |
|
{ |
256 |
1393550 |
return false; |
257 |
|
} |
258 |
|
} |
259 |
298445 |
d_lemmaIdStats << id; |
260 |
298445 |
smt::currentResourceManager()->spendResource(id); |
261 |
298445 |
Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl; |
262 |
298445 |
d_numCurrentLemmas++; |
263 |
298447 |
d_out.trustedLemma(tlem, p); |
264 |
298443 |
return true; |
265 |
|
} |
266 |
|
|
267 |
|
bool TheoryInferenceManager::lemmaExp(Node conc, |
268 |
|
InferenceId id, |
269 |
|
PfRule pfr, |
270 |
|
const std::vector<Node>& exp, |
271 |
|
const std::vector<Node>& noExplain, |
272 |
|
const std::vector<Node>& args, |
273 |
|
LemmaProperty p) |
274 |
|
{ |
275 |
|
// make the trust node |
276 |
|
TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args); |
277 |
|
// send it on the output channel |
278 |
|
return trustedLemma(trn, id, p); |
279 |
|
} |
280 |
|
|
281 |
386 |
TrustNode TheoryInferenceManager::mkLemmaExp(Node conc, |
282 |
|
PfRule id, |
283 |
|
const std::vector<Node>& exp, |
284 |
|
const std::vector<Node>& noExplain, |
285 |
|
const std::vector<Node>& args) |
286 |
|
{ |
287 |
386 |
if (d_pfee != nullptr) |
288 |
|
{ |
289 |
|
// make the trust node from the proof equality engine |
290 |
51 |
return d_pfee->assertLemma(conc, id, exp, noExplain, args); |
291 |
|
} |
292 |
|
// otherwise, not using proofs, explain and make trust node |
293 |
670 |
Node ant = mkExplainPartial(exp, noExplain); |
294 |
670 |
Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); |
295 |
335 |
return TrustNode::mkTrustLemma(lem, nullptr); |
296 |
|
} |
297 |
|
|
298 |
|
bool TheoryInferenceManager::lemmaExp(Node conc, |
299 |
|
InferenceId id, |
300 |
|
const std::vector<Node>& exp, |
301 |
|
const std::vector<Node>& noExplain, |
302 |
|
ProofGenerator* pg, |
303 |
|
LemmaProperty p) |
304 |
|
{ |
305 |
|
// make the trust node |
306 |
|
TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg); |
307 |
|
// send it on the output channel |
308 |
|
return trustedLemma(trn, id, p); |
309 |
|
} |
310 |
|
|
311 |
19327 |
TrustNode TheoryInferenceManager::mkLemmaExp(Node conc, |
312 |
|
const std::vector<Node>& exp, |
313 |
|
const std::vector<Node>& noExplain, |
314 |
|
ProofGenerator* pg) |
315 |
|
{ |
316 |
19327 |
if (d_pfee != nullptr) |
317 |
|
{ |
318 |
|
// make the trust node from the proof equality engine |
319 |
1845 |
return d_pfee->assertLemma(conc, exp, noExplain, pg); |
320 |
|
} |
321 |
|
// otherwise, not using proofs, explain and make trust node |
322 |
34964 |
Node ant = mkExplainPartial(exp, noExplain); |
323 |
34964 |
Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); |
324 |
17482 |
return TrustNode::mkTrustLemma(lem, nullptr); |
325 |
|
} |
326 |
|
|
327 |
121931 |
bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) |
328 |
|
{ |
329 |
243862 |
Node rewritten = Rewriter::rewrite(lem); |
330 |
243862 |
return d_lemmasSent.find(rewritten) != d_lemmasSent.end(); |
331 |
|
} |
332 |
|
|
333 |
|
uint32_t TheoryInferenceManager::numSentLemmas() const |
334 |
|
{ |
335 |
|
return d_numCurrentLemmas; |
336 |
|
} |
337 |
|
|
338 |
527280 |
bool TheoryInferenceManager::hasSentLemma() const |
339 |
|
{ |
340 |
527280 |
return d_numCurrentLemmas != 0; |
341 |
|
} |
342 |
|
|
343 |
13999 |
bool TheoryInferenceManager::assertInternalFact(TNode atom, |
344 |
|
bool pol, |
345 |
|
InferenceId id, |
346 |
|
TNode exp) |
347 |
|
{ |
348 |
41997 |
return processInternalFact( |
349 |
41997 |
atom, pol, id, PfRule::UNKNOWN, {exp}, {}, nullptr); |
350 |
|
} |
351 |
|
|
352 |
27689 |
bool TheoryInferenceManager::assertInternalFact(TNode atom, |
353 |
|
bool pol, |
354 |
|
InferenceId id, |
355 |
|
PfRule pfr, |
356 |
|
const std::vector<Node>& exp, |
357 |
|
const std::vector<Node>& args) |
358 |
|
{ |
359 |
27689 |
Assert(pfr != PfRule::UNKNOWN); |
360 |
27689 |
return processInternalFact(atom, pol, id, pfr, exp, args, nullptr); |
361 |
|
} |
362 |
|
|
363 |
314611 |
bool TheoryInferenceManager::assertInternalFact(TNode atom, |
364 |
|
bool pol, |
365 |
|
InferenceId id, |
366 |
|
const std::vector<Node>& exp, |
367 |
|
ProofGenerator* pg) |
368 |
|
{ |
369 |
314611 |
return processInternalFact(atom, pol, id, PfRule::ASSUME, exp, {}, pg); |
370 |
|
} |
371 |
|
|
372 |
356299 |
bool TheoryInferenceManager::processInternalFact(TNode atom, |
373 |
|
bool pol, |
374 |
|
InferenceId iid, |
375 |
|
PfRule id, |
376 |
|
const std::vector<Node>& exp, |
377 |
|
const std::vector<Node>& args, |
378 |
|
ProofGenerator* pg) |
379 |
|
{ |
380 |
356299 |
d_factIdStats << iid; |
381 |
356299 |
smt::currentResourceManager()->spendResource(iid); |
382 |
|
// make the node corresponding to the explanation |
383 |
712598 |
Node expn = NodeManager::currentNM()->mkAnd(exp); |
384 |
712598 |
Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode()) |
385 |
356299 |
<< " " << expn << ")" << std::endl; |
386 |
|
// call the pre-notify fact method with preReg = false, isInternal = true |
387 |
356299 |
if (d_theory.preNotifyFact(atom, pol, expn, false, true)) |
388 |
|
{ |
389 |
|
// Handled in a theory-specific way that doesn't require equality engine, |
390 |
|
// notice we return true, indicating that the fact was processed. |
391 |
|
return true; |
392 |
|
} |
393 |
356299 |
Assert(d_ee != nullptr); |
394 |
712598 |
Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: " |
395 |
712598 |
<< (pol ? Node(atom) : atom.notNode()) << " from " |
396 |
356299 |
<< expn << " / " << iid << " " << id << std::endl; |
397 |
356299 |
if (Configuration::isAssertionBuild()) |
398 |
|
{ |
399 |
|
// check that all facts hold in the equality engine, to ensure that we |
400 |
|
// aren't processing a stale fact |
401 |
712598 |
std::vector<Node> expc = exp; |
402 |
888249 |
for (size_t i = 0; i < expc.size(); i++) |
403 |
|
{ |
404 |
1031457 |
Node e = expc[i]; |
405 |
531950 |
bool epol = e.getKind() != NOT; |
406 |
1031457 |
Node eatom = epol ? e : e[0]; |
407 |
1063900 |
Trace("infer-manager") |
408 |
531950 |
<< "...check " << eatom << " " << epol << std::endl; |
409 |
531950 |
if (eatom.getKind() == AND) |
410 |
|
{ |
411 |
32443 |
Assert(epol); |
412 |
219334 |
for (const Node& ea : eatom) |
413 |
|
{ |
414 |
186891 |
expc.push_back(ea); |
415 |
|
} |
416 |
32443 |
continue; |
417 |
|
} |
418 |
499507 |
else if (eatom.getKind() == EQUAL) |
419 |
|
{ |
420 |
206447 |
Assert(d_ee->hasTerm(eatom[0])); |
421 |
206447 |
Assert(d_ee->hasTerm(eatom[1])); |
422 |
206447 |
Assert(!epol || d_ee->areEqual(eatom[0], eatom[1])); |
423 |
206447 |
Assert(epol || d_ee->areDisequal(eatom[0], eatom[1], false)); |
424 |
|
} |
425 |
|
else |
426 |
|
{ |
427 |
293060 |
Assert(d_ee->hasTerm(eatom)); |
428 |
293060 |
Assert(d_ee->areEqual(eatom, NodeManager::currentNM()->mkConst(epol))); |
429 |
|
} |
430 |
|
} |
431 |
|
} |
432 |
356299 |
d_numCurrentFacts++; |
433 |
|
// Now, assert the fact. How to do so depends on whether proofs are enabled. |
434 |
356299 |
bool ret = false; |
435 |
356299 |
if (d_pfee == nullptr) |
436 |
|
{ |
437 |
340121 |
Trace("infer-manager") << "...assert without proofs..." << std::endl; |
438 |
340121 |
if (atom.getKind() == kind::EQUAL) |
439 |
|
{ |
440 |
285834 |
ret = d_ee->assertEquality(atom, pol, expn); |
441 |
|
} |
442 |
|
else |
443 |
|
{ |
444 |
54287 |
ret = d_ee->assertPredicate(atom, pol, expn); |
445 |
|
} |
446 |
|
// Must reference count the equality and its explanation, which is not done |
447 |
|
// by the equality engine. Notice that we do *not* need to do this for |
448 |
|
// external assertions, which enter as facts in theory check. This is also |
449 |
|
// not done if we are asserting to the proof equality engine, which does |
450 |
|
// this caching itself within ProofEqEngine::assertFact. |
451 |
340121 |
d_keep.insert(atom); |
452 |
340121 |
d_keep.insert(expn); |
453 |
|
} |
454 |
|
else |
455 |
|
{ |
456 |
16178 |
Assert(id != PfRule::UNKNOWN); |
457 |
16178 |
Trace("infer-manager") << "...assert with proofs..." << std::endl; |
458 |
|
// Note that we reconstruct the original literal lit here, since both the |
459 |
|
// original literal is needed for bookkeeping proofs. It is possible to |
460 |
|
// optimize this so that a few less nodes are created, but at the cost |
461 |
|
// of a more verbose interface to proof equality engine. |
462 |
32356 |
Node lit = pol ? Node(atom) : atom.notNode(); |
463 |
16178 |
if (pg != nullptr) |
464 |
|
{ |
465 |
|
// use the proof generator interface |
466 |
14829 |
ret = d_pfee->assertFact(lit, expn, pg); |
467 |
|
} |
468 |
|
else |
469 |
|
{ |
470 |
|
// use the explict proof step interface |
471 |
1349 |
ret = d_pfee->assertFact(lit, id, expn, args); |
472 |
|
} |
473 |
|
} |
474 |
|
// call the notify fact method with isInternal = true |
475 |
356299 |
d_theory.notifyFact(atom, pol, expn, true); |
476 |
712598 |
Trace("infer-manager") |
477 |
356299 |
<< "TheoryInferenceManager::finished assertInternalFact, ret=" << ret |
478 |
356299 |
<< std::endl; |
479 |
356299 |
return ret; |
480 |
|
} |
481 |
|
|
482 |
41014 |
void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions) |
483 |
|
{ |
484 |
41014 |
if (n.getKind() == kind::AND) |
485 |
|
{ |
486 |
|
for (const Node& nc : n) |
487 |
|
{ |
488 |
|
d_ee->explainLit(nc, assumptions); |
489 |
|
} |
490 |
|
} |
491 |
|
else |
492 |
|
{ |
493 |
41014 |
d_ee->explainLit(n, assumptions); |
494 |
|
} |
495 |
41014 |
} |
496 |
|
|
497 |
|
Node TheoryInferenceManager::mkExplain(TNode n) |
498 |
|
{ |
499 |
|
std::vector<TNode> assumptions; |
500 |
|
explain(n, assumptions); |
501 |
|
return NodeManager::currentNM()->mkAnd(assumptions); |
502 |
|
} |
503 |
|
|
504 |
21348 |
Node TheoryInferenceManager::mkExplainPartial( |
505 |
|
const std::vector<Node>& exp, const std::vector<Node>& noExplain) |
506 |
|
{ |
507 |
42696 |
std::vector<TNode> assumps; |
508 |
65398 |
for (const Node& e : exp) |
509 |
|
{ |
510 |
47086 |
if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end()) |
511 |
|
{ |
512 |
3036 |
if (std::find(assumps.begin(), assumps.end(), e) == assumps.end()) |
513 |
|
{ |
514 |
|
// a non-explained literal |
515 |
3036 |
assumps.push_back(e); |
516 |
|
} |
517 |
3036 |
continue; |
518 |
|
} |
519 |
|
// otherwise, explain it |
520 |
41014 |
explain(e, assumps); |
521 |
|
} |
522 |
42696 |
return NodeManager::currentNM()->mkAnd(assumps); |
523 |
|
} |
524 |
|
|
525 |
|
uint32_t TheoryInferenceManager::numSentFacts() const |
526 |
|
{ |
527 |
|
return d_numCurrentFacts; |
528 |
|
} |
529 |
|
|
530 |
63114 |
bool TheoryInferenceManager::hasSentFact() const |
531 |
|
{ |
532 |
63114 |
return d_numCurrentFacts != 0; |
533 |
|
} |
534 |
|
|
535 |
1639895 |
bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p) |
536 |
|
{ |
537 |
3279790 |
Node rewritten = Rewriter::rewrite(lem); |
538 |
1639895 |
if (d_lemmasSent.find(rewritten) != d_lemmasSent.end()) |
539 |
|
{ |
540 |
1393550 |
return false; |
541 |
|
} |
542 |
246345 |
d_lemmasSent.insert(rewritten); |
543 |
246345 |
return true; |
544 |
|
} |
545 |
|
|
546 |
13889 |
DecisionManager* TheoryInferenceManager::getDecisionManager() |
547 |
|
{ |
548 |
13889 |
return d_decManager; |
549 |
|
} |
550 |
|
|
551 |
30452 |
void TheoryInferenceManager::requirePhase(TNode n, bool pol) |
552 |
|
{ |
553 |
30452 |
return d_out.requirePhase(n, pol); |
554 |
|
} |
555 |
|
|
556 |
12 |
void TheoryInferenceManager::spendResource(Resource r) |
557 |
|
{ |
558 |
12 |
d_out.spendResource(r); |
559 |
12 |
} |
560 |
|
|
561 |
160516 |
void TheoryInferenceManager::safePoint(Resource r) |
562 |
|
{ |
563 |
160516 |
d_out.safePoint(r); |
564 |
160516 |
} |
565 |
|
|
566 |
2174 |
void TheoryInferenceManager::setIncomplete(IncompleteId id) |
567 |
|
{ |
568 |
2174 |
d_out.setIncomplete(id); |
569 |
2174 |
} |
570 |
|
|
571 |
744036 |
void TheoryInferenceManager::notifyInConflict() |
572 |
|
{ |
573 |
744036 |
d_theoryState.notifyInConflict(); |
574 |
744036 |
} |
575 |
|
|
576 |
|
} // namespace theory |
577 |
29280 |
} // namespace cvc5 |