Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Hans-Joerg Schurr
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * Implementation of the proof-producing equality engine.
14 : : */
15 : :
16 : : #include "theory/uf/proof_equality_engine.h"
17 : :
18 : : #include "proof/lazy_proof_chain.h"
19 : : #include "proof/proof_node.h"
20 : : #include "proof/proof_node_manager.h"
21 : : #include "smt/env.h"
22 : : #include "theory/rewriter.h"
23 : : #include "theory/uf/eq_proof.h"
24 : : #include "theory/uf/equality_engine.h"
25 : : #include "theory/uf/proof_checker.h"
26 : :
27 : : using namespace cvc5::internal::kind;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace eq {
32 : :
33 : 142703 : ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee)
34 : 285406 : : EagerProofGenerator(env, env.getUserContext(), "pfee::" + ee.identify()),
35 : : d_ee(ee),
36 : : d_factPg(env, env.getContext()),
37 : : d_assumpPg(env.getProofNodeManager()),
38 : : d_proof(env,
39 : : nullptr,
40 : : env.getContext(),
41 : 285406 : "pfee::LazyCDProof::" + ee.identify()),
42 : 713515 : d_keep(env.getContext())
43 : : {
44 : 142703 : NodeManager* nm = nodeManager();
45 : 142703 : d_true = nm->mkConst(true);
46 : 142703 : d_false = nm->mkConst(false);
47 [ - + ][ - + ]: 142703 : AlwaysAssert(env.getProofNodeManager() != nullptr)
[ - - ]
48 : 0 : << "Should not construct ProofEqEngine without proof node manager";
49 : 142703 : }
50 : :
51 : 0 : bool ProofEqEngine::assertFact(Node lit,
52 : : ProofRule id,
53 : : const std::vector<Node>& exp,
54 : : const std::vector<Node>& args)
55 : : {
56 [ - - ]: 0 : Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
57 : 0 : << ", args = " << args << std::endl;
58 : :
59 [ - - ]: 0 : Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
60 : 0 : bool polarity = lit.getKind() != Kind::NOT;
61 : : // register the step in the proof
62 [ - - ]: 0 : if (holds(atom, polarity))
63 : : {
64 : : // we do not process this fact if it already holds
65 : 0 : return false;
66 : : }
67 : : // Buffer the step in the fact proof generator. We do this instead of
68 : : // adding explict steps to the lazy proof d_proof since CDProof has
69 : : // (at most) one proof for each formula. Thus, we "claim" only the
70 : : // formula that is proved by this fact. Otherwise, aliasing may occur,
71 : : // which leads to cyclic or bogus proofs.
72 : 0 : ProofStep ps;
73 : 0 : ps.d_rule = id;
74 : 0 : ps.d_children = exp;
75 : 0 : ps.d_args = args;
76 : 0 : d_factPg.addStep(lit, ps);
77 : : // add lazy step to proof
78 : 0 : d_proof.addLazyStep(lit, &d_factPg);
79 : : // second, assert it to the equality engine
80 : 0 : Node reason = nodeManager()->mkAnd(exp);
81 : 0 : return assertFactInternal(atom, polarity, reason);
82 : : }
83 : :
84 : 30491 : bool ProofEqEngine::assertFact(Node lit,
85 : : ProofRule id,
86 : : Node exp,
87 : : const std::vector<Node>& args)
88 : : {
89 [ + - ]: 60982 : Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
90 : 30491 : << ", args = " << args << std::endl;
91 [ + + ]: 60982 : Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
92 : 30491 : bool polarity = lit.getKind() != Kind::NOT;
93 : : // register the step in the proof
94 [ + + ]: 30491 : if (holds(atom, polarity))
95 : : {
96 : : // we do not process this fact if it already holds
97 : 3868 : return false;
98 : : }
99 : : // must extract the explanation as a vector
100 : 53246 : std::vector<Node> expv;
101 : : // Flatten (single occurrences) of AND. We do not allow nested AND, it is
102 : : // the responsibilty of the caller to ensure these do not occur.
103 [ + + ]: 26623 : if (exp != d_true)
104 : : {
105 [ - + ]: 5095 : if (exp.getKind() == Kind::AND)
106 : : {
107 [ - - ]: 0 : for (const Node& expc : exp)
108 : : {
109 : : // should not have doubly nested AND
110 : 0 : Assert(expc.getKind() != Kind::AND);
111 : 0 : expv.push_back(expc);
112 : : }
113 : : }
114 : : else
115 : : {
116 : 5095 : expv.push_back(exp);
117 : : }
118 : : }
119 : : // buffer the step in the fact proof generator
120 : 26623 : ProofStep ps;
121 : 26623 : ps.d_rule = id;
122 : 26623 : ps.d_children = expv;
123 : 26623 : ps.d_args = args;
124 : 26623 : d_factPg.addStep(lit, ps);
125 : : // add lazy step to proof
126 : 26623 : d_proof.addLazyStep(lit, &d_factPg);
127 : : // second, assert it to the equality engine
128 : 26623 : return assertFactInternal(atom, polarity, exp);
129 : : }
130 : :
131 : 0 : bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
132 : : {
133 [ - - ]: 0 : Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
134 : 0 : << " via buffer with " << psb.getNumSteps() << " steps"
135 : 0 : << std::endl;
136 [ - - ]: 0 : Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
137 : 0 : bool polarity = lit.getKind() != Kind::NOT;
138 [ - - ]: 0 : if (holds(atom, polarity))
139 : : {
140 : : // we do not process this fact if it already holds
141 : 0 : return false;
142 : : }
143 : : // buffer the steps in the fact proof generator
144 : 0 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
145 [ - - ]: 0 : for (const std::pair<Node, ProofStep>& step : steps)
146 : : {
147 : 0 : d_factPg.addStep(step.first, step.second);
148 : : }
149 : : // add lazy step to proof
150 : 0 : d_proof.addLazyStep(lit, &d_factPg);
151 : : // second, assert it to the equality engine
152 : 0 : return assertFactInternal(atom, polarity, exp);
153 : : }
154 : :
155 : 1383700 : bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
156 : : {
157 [ + - ]: 2767400 : Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
158 : 1383700 : << " via generator" << std::endl;
159 [ + + ]: 2767400 : Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit;
160 : 1383700 : bool polarity = lit.getKind() != Kind::NOT;
161 [ + + ]: 1383700 : if (holds(atom, polarity))
162 : : {
163 : : // we do not process this fact if it already holds
164 : 411583 : return false;
165 : : }
166 : : // note the proof generator is responsible for remembering the explanation
167 : 972118 : d_proof.addLazyStep(lit, pg);
168 : : // second, assert it to the equality engine
169 : 972118 : return assertFactInternal(atom, polarity, exp);
170 : : }
171 : :
172 : 14033 : TrustNode ProofEqEngine::assertConflict(Node lit)
173 : : {
174 [ + - ]: 14033 : Trace("pfee") << "pfee::assertConflict " << lit << std::endl;
175 : 28066 : std::vector<TNode> assumps;
176 : 14033 : explainWithProof(lit, assumps, &d_proof);
177 : : // lit may not be equivalent to false, but should rewrite to false
178 [ + - ]: 14033 : if (lit != d_false)
179 : : {
180 [ - + ][ - + ]: 14033 : Assert(rewrite(lit) == d_false)
[ - - ]
181 : : << "pfee::assertConflict: conflict literal is not rewritable to "
182 : 0 : "false";
183 : 14033 : std::vector<Node> exp;
184 : 14033 : exp.push_back(lit);
185 : 14033 : std::vector<Node> args;
186 [ - + ]: 14033 : if (!d_proof.addStep(d_false, ProofRule::MACRO_SR_PRED_ELIM, exp, args))
187 : : {
188 : 0 : Assert(false) << "pfee::assertConflict: failed conflict step";
189 : : return TrustNode::null();
190 : : }
191 : : }
192 : : return ensureProofForFact(
193 : 14033 : d_false, assumps, TrustNodeKind::CONFLICT, &d_proof);
194 : : }
195 : :
196 : 110 : TrustNode ProofEqEngine::assertConflict(ProofRule id,
197 : : const std::vector<Node>& exp,
198 : : const std::vector<Node>& args)
199 : : {
200 [ + - ]: 220 : Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
201 : 110 : << ", args = " << args << std::endl;
202 : : // conflict is same as lemma concluding false
203 : 110 : return assertLemma(d_false, id, exp, {}, args);
204 : : }
205 : :
206 : 2814 : TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
207 : : ProofGenerator* pg)
208 : : {
209 [ - + ][ - + ]: 2814 : Assert(pg != nullptr);
[ - - ]
210 [ + - ]: 5628 : Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
211 : 2814 : << std::endl;
212 : 2814 : return assertLemma(d_false, exp, {}, pg);
213 : : }
214 : :
215 : 945 : TrustNode ProofEqEngine::assertLemma(Node conc,
216 : : ProofRule id,
217 : : const std::vector<Node>& exp,
218 : : const std::vector<Node>& noExplain,
219 : : const std::vector<Node>& args)
220 : : {
221 [ + - ]: 1890 : Trace("pfee") << "pfee::assertLemma " << conc << " " << id
222 : 0 : << ", exp = " << exp << ", noExplain = " << noExplain
223 : 945 : << ", args = " << args << std::endl;
224 [ - + ][ - + ]: 945 : Assert(conc != d_true);
[ - - ]
225 : 2835 : LazyCDProof tmpProof(d_env, &d_proof);
226 : : LazyCDProof* curr;
227 : : TrustNodeKind tnk;
228 : : // same policy as above: for conflicts, use existing lazy proof
229 [ + + ][ + - ]: 945 : if (conc == d_false && noExplain.empty())
[ + + ]
230 : : {
231 : 110 : curr = &d_proof;
232 : 110 : tnk = TrustNodeKind::CONFLICT;
233 : : }
234 : : else
235 : : {
236 : 835 : curr = &tmpProof;
237 : 835 : tnk = TrustNodeKind::LEMMA;
238 : : }
239 : : // explain each literal in the vector
240 : 1890 : std::vector<TNode> assumps;
241 : 945 : explainVecWithProof(tnk, assumps, exp, noExplain, curr);
242 : : // Register the proof step. We use a separate lazy CDProof which will make
243 : : // calls to curr above for the proofs of the literals in exp.
244 [ + - ]: 1890 : LazyCDProof outer(d_env, curr);
245 [ - + ]: 945 : if (!outer.addStep(conc, id, exp, args))
246 : : {
247 : : // a step went wrong, e.g. during checking
248 : 0 : Assert(false) << "pfee::assertConflict: register proof step";
249 : : return TrustNode::null();
250 : : }
251 : : // Now get the proof for conc.
252 : 945 : return ensureProofForFact(conc, assumps, tnk, &outer);
253 : : }
254 : :
255 : 19260 : TrustNode ProofEqEngine::assertLemma(Node conc,
256 : : const std::vector<Node>& exp,
257 : : const std::vector<Node>& noExplain,
258 : : ProofGenerator* pg)
259 : : {
260 [ - + ][ - + ]: 19260 : Assert(pg != nullptr);
[ - - ]
261 [ + - ]: 38520 : Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
262 : 0 : << ", noExplain = " << noExplain << " via generator"
263 : 19260 : << std::endl;
264 : 57780 : LazyCDProof tmpProof(d_env, &d_proof);
265 : : LazyCDProof* curr;
266 : : TrustNodeKind tnk;
267 : : // same policy as above: for conflicts, use existing lazy proof
268 [ + + ][ + + ]: 19260 : if (conc == d_false && noExplain.empty())
[ + + ]
269 : : {
270 : 2814 : curr = &d_proof;
271 : 2814 : tnk = TrustNodeKind::CONFLICT;
272 : : }
273 : : else
274 : : {
275 : 16446 : curr = &tmpProof;
276 : 16446 : tnk = TrustNodeKind::LEMMA;
277 : : }
278 : : // explain each literal in the vector
279 : 38520 : std::vector<TNode> assumps;
280 : 19260 : explainVecWithProof(tnk, assumps, exp, noExplain, curr);
281 : : // We use a lazy proof chain here. The provided proof generator sets up the
282 : : // "skeleton" that is the base of the proof we are constructing. The call to
283 : : // LazyCDProofChain::getProofFor will expand the leaves of this proof via
284 : : // calls to curr.
285 [ + - ]: 38520 : LazyCDProofChain outer(d_env, true, nullptr, curr, false);
286 : 19260 : outer.addLazyStep(conc, pg);
287 : 38520 : return ensureProofForFact(conc, assumps, tnk, &outer);
288 : : }
289 : :
290 : 295933 : TrustNode ProofEqEngine::explain(Node conc)
291 : : {
292 [ + - ]: 295933 : Trace("pfee") << "pfee::explain " << conc << std::endl;
293 : 887799 : LazyCDProof tmpProof(d_env, &d_proof);
294 : 295933 : std::vector<TNode> assumps;
295 : 295933 : explainWithProof(conc, assumps, &tmpProof);
296 : 591866 : return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
297 : : }
298 : :
299 : 20205 : void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
300 : : std::vector<TNode>& assumps,
301 : : const std::vector<Node>& exp,
302 : : const std::vector<Node>& noExplain,
303 : : LazyCDProof* curr)
304 : : {
305 : 40410 : std::vector<Node> expn;
306 [ + + ]: 66203 : for (const Node& e : exp)
307 : : {
308 [ + + ]: 45998 : if (std::find(noExplain.begin(), noExplain.end(), e) == noExplain.end())
309 : : {
310 : 43765 : explainWithProof(e, assumps, curr);
311 : : }
312 : : else
313 : : {
314 : : // it did not have a proof; it was an assumption of the previous rule
315 : 2233 : assumps.push_back(e);
316 : : // it is not a conflict, since it may involve new literals
317 : 2233 : tnk = TrustNodeKind::LEMMA;
318 : : // ensure this is an assumption
319 : 2233 : curr->addLazyStep(e, &d_assumpPg);
320 : : }
321 : : }
322 : 20205 : }
323 : :
324 : 330171 : TrustNode ProofEqEngine::ensureProofForFact(Node conc,
325 : : const std::vector<TNode>& assumps,
326 : : TrustNodeKind tnk,
327 : : ProofGenerator* curr)
328 : : {
329 [ + - ]: 330171 : Trace("pfee-proof") << std::endl;
330 [ + - ]: 660342 : Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
331 : 330171 : << assumps << ", TrustNodeKind=" << tnk << std::endl;
332 : 330171 : NodeManager* nm = nodeManager();
333 : : // The proof
334 : 330171 : std::shared_ptr<ProofNode> pf;
335 : 330171 : ProofGenerator* pfg = nullptr;
336 : : // the explanation is the conjunction of assumptions
337 : 660342 : Node exp;
338 : : // If proofs are enabled, generate the proof and possibly modify the
339 : : // assumptions to match SCOPE.
340 [ - + ][ - + ]: 330171 : Assert(curr != nullptr);
[ - - ]
341 [ + - ]: 660342 : Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
342 : 330171 : << std::endl;
343 : : // get the proof for conc
344 : 660342 : std::shared_ptr<ProofNode> pfBody = curr->getProofFor(conc);
345 [ - + ]: 330171 : if (pfBody == nullptr)
346 : : {
347 [ - - ]: 0 : Trace("pfee-proof")
348 : 0 : << "pfee::ensureProofForFact: failed to make proof for fact"
349 : 0 : << std::endl
350 : 0 : << std::endl;
351 : : // should have existed
352 : 0 : Assert(false) << "pfee::assertConflict: failed to get proof for " << conc;
353 : : return TrustNode::null();
354 : : }
355 : : // clone it so that we have a fresh copy
356 : 330171 : pfBody = pfBody->clone();
357 [ + - ]: 330171 : Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl;
358 : : // The free assumptions must be closed by assumps, which should be passed
359 : : // as arguments of SCOPE. However, some of the free assumptions may not
360 : : // literally be equal to assumps, for instance, due to symmetry. In other
361 : : // words, the SCOPE could be closing (= x y) in a proof with free
362 : : // assumption (= y x). We modify the proof leaves to account for this
363 : : // below.
364 : :
365 : 660342 : std::vector<Node> scopeAssumps;
366 : : // we first ensure the assumptions are flattened
367 [ + + ]: 1638520 : for (const TNode& a : assumps)
368 : : {
369 [ + + ]: 1308350 : if (a.getKind() == Kind::AND)
370 : : {
371 : 17138 : scopeAssumps.insert(scopeAssumps.end(), a.begin(), a.end());
372 : : }
373 : : else
374 : : {
375 : 1291220 : scopeAssumps.push_back(a);
376 : : }
377 : : }
378 : : // Scope the proof constructed above, and connect the formula with the proof
379 : : // minimize the assumptions.
380 : 330171 : ProofNodeManager* pnm = d_env.getProofNodeManager();
381 : 330171 : pf = pnm->mkScope(pfBody, scopeAssumps, true, true);
382 : : // If we have no assumptions, and are proving an explanation for propagation
383 [ + + ][ + + ]: 330171 : if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
[ + + ]
384 : : {
385 : : // Must add "true" as an explicit argument. This is to ensure that the
386 : : // propagation F from true proves (=> true F) instead of F, since this is
387 : : // the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or
388 : : // minimize here, since we already ensured the proof was closed above, and
389 : : // we do not want to minimize, or else "true" would be omitted.
390 : 4440 : scopeAssumps.push_back(nm->mkConst(true));
391 : 4440 : pf = pnm->mkScope(pf, scopeAssumps, false);
392 : : }
393 : 330171 : exp = nm->mkAnd(scopeAssumps);
394 : : // Make the lemma or conflict node. This must exactly match the conclusion
395 : : // of SCOPE below.
396 : 660342 : Node formula;
397 [ + + ]: 330171 : if (tnk == TrustNodeKind::CONFLICT)
398 : : {
399 : : // conflict is negated
400 [ - + ][ - + ]: 16957 : Assert(conc == d_false);
[ - - ]
401 : 16957 : formula = exp;
402 : : }
403 : : else
404 : : {
405 : 313214 : formula = exp == d_true
406 : 930839 : ? conc
407 [ + + ]: 304411 : : (conc == d_false ? exp.negate()
408 : 313214 : : nm->mkNode(Kind::IMPLIES, exp, conc));
409 : : }
410 [ + - ]: 660342 : Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
411 : 330171 : << std::endl;
412 : : // should always be non-null
413 [ - + ][ - + ]: 330171 : Assert(pf != nullptr);
[ - - ]
414 : 330171 : if (TraceIsOn("pfee-proof") || TraceIsOn("pfee-proof-final"))
415 : : {
416 [ - - ]: 0 : Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
417 : 0 : << std::endl;
418 : 0 : std::stringstream ss;
419 : 0 : pf->printDebug(ss);
420 : 0 : Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss.str()
421 : 0 : << std::endl;
422 : : }
423 : : // Should be a closed proof now. If it is not, then the overall proof
424 : : // is malformed.
425 [ - + ][ - + ]: 330171 : Assert(pf->isClosed());
[ - - ]
426 : 330171 : pfg = this;
427 : : // set the proof for the conflict or lemma, which can be queried later
428 [ + + ][ + - ]: 330171 : switch (tnk)
429 : : {
430 : 16957 : case TrustNodeKind::CONFLICT: setProofForConflict(formula, pf); break;
431 : 17281 : case TrustNodeKind::LEMMA: setProofForLemma(formula, pf); break;
432 : 295933 : case TrustNodeKind::PROP_EXP: setProofForPropExp(conc, exp, pf); break;
433 : 0 : default:
434 : 0 : pfg = nullptr;
435 : 0 : Unhandled() << "Unhandled trust node kind " << tnk;
436 : : break;
437 : : }
438 [ + - ]: 660342 : Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
439 : 330171 : << std::endl;
440 : : // we can provide a proof for conflict, lemma or explained propagation
441 [ + + ][ + - ]: 330171 : switch (tnk)
442 : : {
443 : 16957 : case TrustNodeKind::CONFLICT:
444 : 16957 : return TrustNode::mkTrustConflict(formula, pfg);
445 : 17281 : case TrustNodeKind::LEMMA: return TrustNode::mkTrustLemma(formula, pfg);
446 : 295933 : case TrustNodeKind::PROP_EXP:
447 : 295933 : return TrustNode::mkTrustPropExp(conc, exp, pfg);
448 : 0 : default: Unhandled() << "Unhandled trust node kind " << tnk; break;
449 : : }
450 : : return TrustNode::null();
451 : : }
452 : :
453 : 998741 : bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
454 : : {
455 [ + - ]: 1997480 : Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
456 : 998741 : << " " << reason << std::endl;
457 : : bool ret;
458 [ + + ]: 998741 : if (atom.getKind() == Kind::EQUAL)
459 : : {
460 : 981417 : ret = d_ee.assertEquality(atom, polarity, reason);
461 : : }
462 : : else
463 : : {
464 : 17324 : ret = d_ee.assertPredicate(atom, polarity, reason);
465 : : }
466 [ + - ]: 998741 : if (ret)
467 : : {
468 : : // must reference count the new atom and explanation
469 : 998741 : d_keep.insert(atom);
470 : 998741 : d_keep.insert(reason);
471 : : }
472 : 998741 : return ret;
473 : : }
474 : :
475 : 1414190 : bool ProofEqEngine::holds(TNode atom, bool polarity)
476 : : {
477 [ + + ]: 1414190 : if (atom.getKind() == Kind::EQUAL)
478 : : {
479 : 1396500 : if (!d_ee.hasTerm(atom[0]) || !d_ee.hasTerm(atom[1]))
480 : : {
481 : 619443 : return false;
482 : : }
483 : 1554120 : return polarity ? d_ee.areEqual(atom[0], atom[1])
484 : 777059 : : d_ee.areDisequal(atom[0], atom[1], false);
485 : : }
486 [ + + ]: 17690 : if (!d_ee.hasTerm(atom))
487 : : {
488 : 6900 : return false;
489 : : }
490 [ + + ]: 10790 : TNode b = polarity ? d_true : d_false;
491 : 10790 : return d_ee.areEqual(atom, b);
492 : : }
493 : :
494 : 353731 : void ProofEqEngine::explainWithProof(Node lit,
495 : : std::vector<TNode>& assumps,
496 : : LazyCDProof* curr)
497 : : {
498 [ + + ]: 353731 : if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
499 : : {
500 : 170 : return;
501 : : }
502 : 353561 : std::shared_ptr<eq::EqProof> pf = std::make_shared<eq::EqProof>();
503 [ + - ]: 353561 : Trace("pfee-proof") << "pfee::explainWithProof: " << lit << std::endl;
504 : 353561 : bool polarity = lit.getKind() != Kind::NOT;
505 [ + + ]: 353561 : TNode atom = polarity ? lit : lit[0];
506 [ - + ][ - + ]: 353561 : Assert(atom.getKind() != Kind::AND);
[ - - ]
507 : 353561 : std::vector<TNode> tassumps;
508 [ + + ]: 353561 : if (atom.getKind() == Kind::EQUAL)
509 : : {
510 [ - + ]: 342667 : if (atom[0] == atom[1])
511 : : {
512 : 0 : return;
513 : : }
514 [ - + ][ - + ]: 342667 : Assert(d_ee.hasTerm(atom[0]));
[ - - ]
515 [ - + ][ - + ]: 342667 : Assert(d_ee.hasTerm(atom[1]));
[ - - ]
516 [ + + ]: 342667 : if (!polarity)
517 : : {
518 : : // ensure the explanation exists
519 [ - + ][ - + ]: 20245 : AlwaysAssert(d_ee.areDisequal(atom[0], atom[1], true));
[ - - ]
520 : : }
521 : 342667 : d_ee.explainEquality(atom[0], atom[1], polarity, tassumps, pf.get());
522 : : }
523 : : else
524 : : {
525 [ - + ][ - + ]: 10894 : Assert(d_ee.hasTerm(atom));
[ - - ]
526 : 10894 : d_ee.explainPredicate(atom, polarity, tassumps, pf.get());
527 : : }
528 [ + - ]: 353561 : Trace("pfee-proof") << "...got " << tassumps << std::endl;
529 : : // avoid duplicates
530 [ + + ]: 1985310 : for (TNode a : tassumps)
531 : : {
532 [ + + ]: 1631750 : if (a == lit)
533 : : {
534 : 16344 : assumps.push_back(a);
535 : : }
536 [ + + ]: 1615410 : else if (std::find(assumps.begin(), assumps.end(), a) == assumps.end())
537 : : {
538 : 1289780 : assumps.push_back(a);
539 : : }
540 : : }
541 [ - + ]: 353561 : if (TraceIsOn("pfee-proof"))
542 : : {
543 [ - - ]: 0 : Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
544 : 0 : << std::endl;
545 : 0 : std::stringstream sse;
546 : 0 : pf->debug_print(sse);
547 : 0 : Trace("pfee-proof") << sse.str() << std::endl;
548 [ - - ]: 0 : Trace("pfee-proof") << "---" << std::endl;
549 : : }
550 : : // add the steps in the equality engine proof to the Proof
551 : 353561 : pf->addToProof(curr);
552 [ + - ]: 353561 : Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
553 : : }
554 : :
555 : : } // namespace eq
556 : : } // namespace theory
557 : : } // namespace cvc5::internal
|
