Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Aina Niemetz
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 : : * Implementation of proof.
14 : : */
15 : :
16 : : #include "proof/proof.h"
17 : :
18 : : #include "proof/proof_checker.h"
19 : : #include "proof/proof_node.h"
20 : : #include "proof/proof_node_manager.h"
21 : : #include "rewriter/rewrites.h"
22 : : #include "smt/env.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : :
28 : 7615740 : CDProof::CDProof(Env& env,
29 : : context::Context* c,
30 : : const std::string& name,
31 : 7615740 : bool autoSymm)
32 : : : EnvObj(env),
33 : : d_context(),
34 : : d_nodes(c ? c : &d_context),
35 : : d_name(name),
36 [ + + ]: 7615740 : d_autoSymm(autoSymm)
37 : : {
38 : 7615740 : }
39 : :
40 : 7625413 : CDProof::~CDProof() {}
41 : :
42 : 16166500 : std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact)
43 : : {
44 : 32333000 : std::shared_ptr<ProofNode> pf = getProofSymm(fact);
45 [ + + ]: 16166500 : if (pf != nullptr)
46 : : {
47 : 10642900 : return pf;
48 : : }
49 : : // add as assumption
50 : 22094500 : std::vector<Node> pargs = {fact};
51 : 11047200 : std::vector<std::shared_ptr<ProofNode>> passume;
52 : 5523610 : ProofNodeManager* pnm = getManager();
53 : : std::shared_ptr<ProofNode> pfa =
54 : 11047200 : pnm->mkNode(ProofRule::ASSUME, passume, pargs, fact);
55 : 5523610 : d_nodes.insert(fact, pfa);
56 : 5523610 : return pfa;
57 : : }
58 : :
59 : 164399000 : std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
60 : : {
61 : 164399000 : NodeProofNodeMap::iterator it = d_nodes.find(fact);
62 [ + + ]: 164399000 : if (it != d_nodes.end())
63 : : {
64 : 79326900 : return (*it).second;
65 : : }
66 : 85072400 : return nullptr;
67 : : }
68 : :
69 : 124531000 : std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
70 : : {
71 [ + - ]: 124531000 : Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl;
72 : 249061000 : std::shared_ptr<ProofNode> pf = getProof(fact);
73 [ + + ][ + + ]: 124531000 : if (pf != nullptr && !isAssumption(pf.get()))
[ + + ]
74 : : {
75 [ + - ]: 51530500 : Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
76 : 51530500 : return pf;
77 : : }
78 [ + + ]: 73000100 : else if (!d_autoSymm)
79 : : {
80 [ + - ]: 41144300 : Trace("cdproof") << "...not auto considering symmetry" << std::endl;
81 : 41144300 : return pf;
82 : : }
83 : 63711700 : Node symFact = getSymmFact(fact);
84 [ + + ]: 31855800 : if (symFact.isNull())
85 : : {
86 [ + - ]: 16223400 : Trace("cdproof") << "...no possible symm" << std::endl;
87 : : // no symmetry possible, return original proof (possibly assumption)
88 : 16223400 : return pf;
89 : : }
90 : : // See if a proof exists for the opposite direction, if so, add the step.
91 : : // Notice that SYMM is also disallowed.
92 : 31265000 : std::shared_ptr<ProofNode> pfs = getProof(symFact);
93 [ + + ]: 15632500 : if (pfs != nullptr)
94 : : {
95 : : // The symmetric fact exists, and the current one either does not, or is
96 : : // an assumption. We make a new proof that applies SYMM to pfs.
97 : 2111770 : std::vector<std::shared_ptr<ProofNode>> pschild;
98 : 2111770 : pschild.push_back(pfs);
99 : 2111770 : std::vector<Node> args;
100 : 2111770 : ProofNodeManager* pnm = getManager();
101 [ + + ]: 2111770 : if (pf == nullptr)
102 : : {
103 [ + - ]: 1581360 : Trace("cdproof") << "...fresh make symm" << std::endl;
104 : 4744090 : std::shared_ptr<ProofNode> psym = pnm->mkSymm(pfs, fact);
105 [ - + ][ - + ]: 1581360 : Assert(psym != nullptr);
[ - - ]
106 : 1581360 : d_nodes.insert(fact, psym);
107 : 1581360 : return psym;
108 : : }
109 [ + + ]: 530410 : else if (!isAssumption(pfs.get()))
110 : : {
111 : : // if its not an assumption, make the connection
112 [ + - ]: 8 : Trace("cdproof") << "...update symm" << std::endl;
113 : : // update pf
114 : 8 : bool sret = pnm->updateNode(pf.get(), ProofRule::SYMM, pschild, args);
115 [ - + ][ - + ]: 8 : AlwaysAssert(sret);
[ - - ]
116 : : }
117 : : }
118 : : else
119 : : {
120 [ + - ]: 27041400 : Trace("cdproof") << "...no symm, return "
121 [ - - ]: 13520700 : << (pf == nullptr ? "null" : "non-null") << std::endl;
122 : : }
123 : : // return original proof (possibly assumption)
124 : 14051100 : return pf;
125 : : }
126 : :
127 : 35794200 : bool CDProof::addStep(Node expected,
128 : : ProofRule id,
129 : : const std::vector<Node>& children,
130 : : const std::vector<Node>& args,
131 : : bool ensureChildren,
132 : : CDPOverwrite opolicy)
133 : : {
134 [ + - ][ - + ]: 71588500 : Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " "
[ - - ]
135 : 0 : << expected << ", ensureChildren = " << ensureChildren
136 : 35794200 : << ", overwrite policy = " << opolicy << std::endl;
137 [ + - ][ - + ]: 71588500 : Trace("cdproof-debug") << "CDProof::addStep: " << identify()
[ - - ]
138 : 35794200 : << " : children: " << children << "\n";
139 [ + - ][ - + ]: 71588500 : Trace("cdproof-debug") << "CDProof::addStep: " << identify()
[ - - ]
140 : 35794200 : << " : args: " << args << "\n";
141 : : // We must always provide expected to this method
142 [ - + ][ - + ]: 35794200 : Assert(!expected.isNull());
[ - - ]
143 : :
144 : 71588500 : std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
145 [ + + ]: 35794200 : if (pprev != nullptr)
146 : : {
147 [ + + ]: 9617890 : if (!shouldOverwrite(pprev.get(), id, opolicy))
148 : : {
149 : : // we should not overwrite the current step
150 [ + - ]: 9335430 : Trace("cdproof") << "...success, no overwrite" << std::endl;
151 : 9335430 : return true;
152 : : }
153 [ + - ]: 564918 : Trace("cdproof") << "existing proof " << pprev->getRule()
154 : 282459 : << ", overwrite..." << std::endl;
155 : : // we will overwrite the existing proof node by updating its contents below
156 : : }
157 : : // collect the child proofs, for each premise
158 : 26458800 : ProofNodeManager* pnm = getManager();
159 : 52917600 : std::vector<std::shared_ptr<ProofNode>> pchildren;
160 [ + + ]: 72402900 : for (const Node& c : children)
161 : : {
162 [ + - ]: 45944100 : Trace("cdproof") << "- get child " << c << std::endl;
163 : 45944100 : std::shared_ptr<ProofNode> pc = getProofSymm(c);
164 [ + + ]: 45944100 : if (pc == nullptr)
165 : : {
166 [ - + ]: 3061200 : if (ensureChildren)
167 : : {
168 : : // failed to get a proof for a child, fail
169 [ - - ]: 0 : Trace("cdproof") << "...fail, no child" << std::endl;
170 : 0 : return false;
171 : : }
172 [ + - ]: 3061200 : Trace("cdproof") << "--- add assume" << std::endl;
173 : : // otherwise, we initialize it as an assumption
174 : 12244800 : std::vector<Node> pcargs = {c};
175 : 6122400 : std::vector<std::shared_ptr<ProofNode>> pcassume;
176 : 3061200 : pc = pnm->mkNode(ProofRule::ASSUME, pcassume, pcargs, c);
177 : : // assumptions never fail to check
178 [ - + ][ - + ]: 3061200 : Assert(pc != nullptr);
[ - - ]
179 : 3061200 : d_nodes.insert(c, pc);
180 : : }
181 : 45944100 : pchildren.push_back(pc);
182 : : }
183 : :
184 : : // The user may have provided SYMM of an assumption. This block is only
185 : : // necessary if d_autoSymm is enabled.
186 [ + + ][ + + ]: 26458800 : if (d_autoSymm && id == ProofRule::SYMM)
187 : : {
188 [ - + ][ - + ]: 10 : Assert(pchildren.size() == 1);
[ - - ]
189 [ + - ]: 10 : if (isAssumption(pchildren[0].get()))
190 : : {
191 : : // the step we are constructing is a (symmetric fact of an) assumption, so
192 : : // there is no use adding it to the proof.
193 : 10 : return true;
194 : : }
195 : : }
196 : :
197 : 26458800 : bool ret = true;
198 : : // create or update it
199 : 26458800 : std::shared_ptr<ProofNode> pthis;
200 [ + + ]: 26458800 : if (pprev == nullptr)
201 : : {
202 [ + - ]: 26176300 : Trace("cdproof") << " new node " << expected << "..." << std::endl;
203 : 26176300 : pthis = pnm->mkNode(id, pchildren, args, expected);
204 [ - + ]: 26176300 : if (pthis == nullptr)
205 : : {
206 : : // failed to construct the node, perhaps due to a proof checking failure
207 [ - - ]: 0 : Trace("cdproof") << "...fail, proof checking" << std::endl;
208 : 0 : return false;
209 : : }
210 : 26176300 : d_nodes.insert(expected, pthis);
211 : : }
212 : : else
213 : : {
214 [ + - ]: 282459 : Trace("cdproof") << " update node " << expected << "..." << std::endl;
215 : : // update its value
216 : 282459 : pthis = pprev;
217 : : // We return the value of updateNode here. This means this method may return
218 : : // false if this call failed, regardless of whether we already have a proof
219 : : // step for expected.
220 : 282459 : ret = pnm->updateNode(pthis.get(), id, pchildren, args);
221 : : }
222 [ + - ]: 26458800 : if (ret)
223 : : {
224 : : // the result of the proof node should be expected
225 [ - + ][ - + ]: 26458800 : Assert(pthis->getResult() == expected);
[ - - ]
226 : :
227 : : // notify new proof
228 : 26458800 : notifyNewProof(expected);
229 : : }
230 : :
231 [ + - ]: 26458800 : Trace("cdproof") << "...return " << ret << std::endl;
232 : 26458800 : return ret;
233 : : }
234 : :
235 : 53081800 : void CDProof::notifyNewProof(Node expected)
236 : : {
237 [ + + ]: 53081800 : if (!d_autoSymm)
238 : : {
239 : 28695700 : return;
240 : : }
241 : : // ensure SYMM proof is also linked to an existing proof, if it is an
242 : : // assumption.
243 : 48772100 : Node symExpected = getSymmFact(expected);
244 [ + + ]: 24386000 : if (!symExpected.isNull())
245 : : {
246 [ + - ]: 10438600 : Trace("cdproof") << " check connect symmetry " << symExpected << std::endl;
247 : : // if it exists, we may need to update it
248 : 20877300 : std::shared_ptr<ProofNode> pfs = getProof(symExpected);
249 [ + + ]: 10438600 : if (pfs != nullptr)
250 : : {
251 [ + - ]: 2826 : Trace("cdproof") << " connect via getProofSymm method..." << std::endl;
252 : : // call the get function with symmetry, which will do the update
253 : 5652 : std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected);
254 : : }
255 : : else
256 : : {
257 [ + - ]: 10435800 : Trace("cdproof") << " no connect" << std::endl;
258 : : }
259 : : }
260 : : }
261 : :
262 : 53855 : bool CDProof::addTrustedStep(Node expected,
263 : : TrustId id,
264 : : const std::vector<Node>& children,
265 : : const std::vector<Node>& args,
266 : : bool ensureChildren,
267 : : CDPOverwrite opolicy)
268 : : {
269 : 53855 : std::vector<Node> sargs;
270 : 53855 : sargs.push_back(mkTrustId(id));
271 : 53855 : sargs.push_back(expected);
272 : 53855 : sargs.insert(sargs.end(), args.begin(), args.end());
273 : 107710 : return addStep(
274 : 107710 : expected, ProofRule::TRUST, children, sargs, ensureChildren, opolicy);
275 : : }
276 : :
277 : 15689 : bool CDProof::addTheoryRewriteStep(Node expected,
278 : : ProofRewriteRule id,
279 : : bool ensureChildren,
280 : : CDPOverwrite opolicy)
281 : : {
282 [ - + ]: 15689 : if (expected.getKind() != Kind::EQUAL)
283 : : {
284 : 0 : return false;
285 : : }
286 : 15689 : std::vector<Node> sargs;
287 : 15689 : sargs.push_back(rewriter::mkRewriteRuleNode(id));
288 : 15689 : sargs.push_back(expected);
289 : 31378 : return addStep(
290 : 15689 : expected, ProofRule::THEORY_REWRITE, {}, sargs, ensureChildren, opolicy);
291 : : }
292 : :
293 : 13978600 : bool CDProof::addStep(Node expected,
294 : : const ProofStep& step,
295 : : bool ensureChildren,
296 : : CDPOverwrite opolicy)
297 : : {
298 : 27957100 : return addStep(expected,
299 : 13978600 : step.d_rule,
300 : 13978600 : step.d_children,
301 : 13978600 : step.d_args,
302 : : ensureChildren,
303 : 27957100 : opolicy);
304 : : }
305 : :
306 : 106771 : bool CDProof::addSteps(const ProofStepBuffer& psb,
307 : : bool ensureChildren,
308 : : CDPOverwrite opolicy)
309 : : {
310 : 106771 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
311 [ + + ]: 671655 : for (const std::pair<Node, ProofStep>& ps : steps)
312 : : {
313 [ - + ]: 564884 : if (!addStep(ps.first, ps.second, ensureChildren, opolicy))
314 : : {
315 : 0 : return false;
316 : : }
317 : : }
318 : 106771 : return true;
319 : : }
320 : :
321 : 26623000 : bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
322 : : CDPOverwrite opolicy,
323 : : bool doCopy)
324 : : {
325 [ + - ]: 26623000 : if (!doCopy)
326 : : {
327 : : // If we are automatically managing symmetry, we strip off SYMM steps.
328 : : // This avoids cyclic proofs in cases where P and (SYMM P) are added as
329 : : // proofs to the same CDProof.
330 [ + + ]: 26623000 : if (d_autoSymm)
331 : : {
332 : 22504700 : std::vector<std::shared_ptr<ProofNode>> processed;
333 [ + + ]: 11381300 : while (pn->getRule() == ProofRule::SYMM)
334 : : {
335 : 128914 : pn = pn->getChildren()[0];
336 : 128914 : if (std::find(processed.begin(), processed.end(), pn)
337 [ - + ]: 257828 : != processed.end())
338 : : {
339 : 0 : Unreachable() << "Cyclic proof encountered when cancelling symmetry "
340 : 0 : "steps during addProof";
341 : : }
342 : 128914 : processed.push_back(pn);
343 : : }
344 : : }
345 : : // If we aren't doing a deep copy, we either store pn or link its top
346 : : // node into the existing pointer
347 : 53245900 : Node curFact = pn->getResult();
348 : 53245900 : std::shared_ptr<ProofNode> cur = getProofSymm(curFact);
349 [ + + ]: 26623000 : if (cur == nullptr)
350 : : {
351 : : // Assert that the checker of this class agrees with (the externally
352 : : // provided) pn. This ensures that if pn was checked by a different
353 : : // checker than the one of the manager in this class, then it is double
354 : : // checked here, so that this class maintains the invariant that all of
355 : : // its nodes in d_nodes have been checked by the underlying checker.
356 : 23108400 : Assert(getManager()->getChecker() == nullptr
357 : : || getManager()->getChecker()->check(pn.get(), curFact)
358 : : == curFact);
359 : : // just store the proof for fact
360 : 23108400 : d_nodes.insert(curFact, pn);
361 : : }
362 [ + + ]: 3514520 : else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy))
363 : : {
364 : : // We update cur to have the structure of the top node of pn. Notice that
365 : : // the interface to update this node will ensure that the proof apf is a
366 : : // proof of the assumption. If it does not, then pn was wrong.
367 [ - + ]: 681 : if (!getManager()->updateNode(
368 : : cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
369 : : {
370 : 0 : return false;
371 : : }
372 : : }
373 : : // also need to connect via SYMM if necessary
374 : 26623000 : notifyNewProof(curFact);
375 : 26623000 : return true;
376 : : }
377 : 0 : std::unordered_map<ProofNode*, bool> visited;
378 : 0 : std::unordered_map<ProofNode*, bool>::iterator it;
379 : 0 : std::vector<ProofNode*> visit;
380 : : ProofNode* cur;
381 : 0 : Node curFact;
382 : 0 : visit.push_back(pn.get());
383 : 0 : bool retValue = true;
384 : 0 : do
385 : : {
386 : 0 : cur = visit.back();
387 : 0 : curFact = cur->getResult();
388 : 0 : visit.pop_back();
389 : 0 : it = visited.find(cur);
390 [ - - ]: 0 : if (it == visited.end())
391 : : {
392 : : // visit the children
393 : 0 : visited[cur] = false;
394 : 0 : visit.push_back(cur);
395 : 0 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
396 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& c : cs)
397 : : {
398 : 0 : visit.push_back(c.get());
399 : : }
400 : : }
401 [ - - ]: 0 : else if (!it->second)
402 : : {
403 : : // we always call addStep, which may or may not overwrite the
404 : : // current step
405 : 0 : std::vector<Node> pexp;
406 : 0 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
407 [ - - ]: 0 : for (const std::shared_ptr<ProofNode>& c : cs)
408 : : {
409 : 0 : Assert(!c->getResult().isNull());
410 : 0 : pexp.push_back(c->getResult());
411 : : }
412 : : // can ensure children at this point
413 : 0 : bool res = addStep(
414 : : curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
415 : : // should always succeed
416 : 0 : Assert(res);
417 [ - - ][ - - ]: 0 : retValue = retValue && res;
418 : 0 : visited[cur] = true;
419 : : }
420 [ - - ]: 0 : } while (!visit.empty());
421 : :
422 : 0 : return retValue;
423 : : }
424 : :
425 : 1896420 : bool CDProof::hasStep(Node fact)
426 : : {
427 : 3792840 : std::shared_ptr<ProofNode> pf = getProof(fact);
428 [ + + ][ + + ]: 1896420 : if (pf != nullptr && !isAssumption(pf.get()))
[ + + ]
429 : : {
430 : 1058800 : return true;
431 : : }
432 [ + + ]: 837624 : else if (!d_autoSymm)
433 : : {
434 : 252862 : return false;
435 : : }
436 : 1169520 : Node symFact = getSymmFact(fact);
437 [ + + ]: 584762 : if (symFact.isNull())
438 : : {
439 : 11438 : return false;
440 : : }
441 : 573324 : pf = getProof(symFact);
442 [ + + ][ + + ]: 573324 : if (pf != nullptr && !isAssumption(pf.get()))
[ + + ]
443 : : {
444 : 64 : return true;
445 : : }
446 : 573260 : return false;
447 : : }
448 : :
449 : 134408 : size_t CDProof::getNumProofNodes() const { return d_nodes.size(); }
450 : :
451 : 84363900 : ProofNodeManager* CDProof::getManager() const
452 : : {
453 : 84363900 : ProofNodeManager* pnm = d_env.getProofNodeManager();
454 [ - + ][ - + ]: 84363900 : Assert(pnm != nullptr);
[ - - ]
455 : 84363900 : return pnm;
456 : : }
457 : :
458 : 13132400 : bool CDProof::shouldOverwrite(ProofNode* pn, ProofRule newId, CDPOverwrite opol)
459 : : {
460 [ - + ][ - + ]: 13132400 : Assert(pn != nullptr);
[ - - ]
461 : : // we overwrite only if opol is CDPOverwrite::ALWAYS, or if
462 : : // opol is CDPOverwrite::ASSUME_ONLY and the previously
463 : : // provided proof pn was an assumption and the currently provided step is not
464 : : return opol == CDPOverwrite::ALWAYS
465 [ + - ][ + - ]: 15157700 : || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn)
[ + + ]
466 [ + + ]: 15157700 : && newId != ProofRule::ASSUME);
467 : : }
468 : :
469 : 79806400 : bool CDProof::isAssumption(ProofNode* pn)
470 : : {
471 : 79806400 : ProofRule rule = pn->getRule();
472 [ + + ]: 79806400 : if (rule == ProofRule::ASSUME)
473 : : {
474 : 15252600 : return true;
475 : : }
476 [ + + ]: 64553800 : else if (rule != ProofRule::SYMM)
477 : : {
478 : 63278300 : return false;
479 : : }
480 : 1275510 : pn = ProofNodeManager::cancelDoubleSymm(pn);
481 : 1275510 : rule = pn->getRule();
482 [ + + ]: 1275510 : if (rule == ProofRule::ASSUME)
483 : : {
484 : 47501 : return true;
485 : : }
486 [ + + ]: 1228000 : else if (rule != ProofRule::SYMM)
487 : : {
488 : 824 : return false;
489 : : }
490 : 1227180 : const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
491 [ - + ][ - + ]: 1227180 : Assert(pc.size() == 1);
[ - - ]
492 : 1227180 : return pc[0]->getRule() == ProofRule::ASSUME;
493 : : }
494 : :
495 : 4268920 : bool CDProof::isSame(TNode f, TNode g)
496 : : {
497 [ + + ]: 4268920 : if (f == g)
498 : : {
499 : 1996010 : return true;
500 : : }
501 : 2272910 : Kind fk = f.getKind();
502 : 2272910 : Kind gk = g.getKind();
503 : 2272910 : if (fk == Kind::EQUAL && gk == Kind::EQUAL && f[0] == g[1] && f[1] == g[0])
504 : : {
505 : : // symmetric equality
506 : 644172 : return true;
507 : : }
508 [ + + ][ + + ]: 2148010 : if (fk == Kind::NOT && gk == Kind::NOT && f[0].getKind() == Kind::EQUAL
[ + + ][ - - ]
509 : 1904970 : && g[0].getKind() == Kind::EQUAL && f[0][0] == g[0][1]
510 : 2148010 : && f[0][1] == g[0][0])
511 : : {
512 : : // symmetric disequality
513 : 1658 : return true;
514 : : }
515 : 1627080 : return false;
516 : : }
517 : :
518 : 64799700 : Node CDProof::getSymmFact(TNode f)
519 : : {
520 : 64799700 : bool polarity = f.getKind() != Kind::NOT;
521 [ + + ]: 129599000 : TNode fatom = polarity ? f : f[0];
522 : 64799700 : if (fatom.getKind() != Kind::EQUAL || fatom[0] == fatom[1])
523 : : {
524 : 31872400 : return Node::null();
525 : : }
526 : 98782100 : Node symFact = fatom[1].eqNode(fatom[0]);
527 [ + + ]: 32927400 : return polarity ? symFact : symFact.notNode();
528 : : }
529 : :
530 : 3527 : std::string CDProof::identify() const { return d_name; }
531 : :
532 : : } // namespace cvc5::internal
|
