1 /********************* */
2 /*! \file proof_equality_engine.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of the proof-producing equality engine
15 #include "theory/uf/proof_equality_engine.h"
17 #include "theory/rewriter.h"
18 #include "theory/uf/proof_checker.h"
20 using namespace CVC4::kind
;
26 ProofEqEngine::ProofEqEngine(context::Context
* c
,
27 context::UserContext
* u
,
29 ProofNodeManager
* pnm
)
30 : EagerProofGenerator(pnm
, u
, "pfee::" + ee
.identify()),
34 d_proof(pnm
, nullptr, c
, "pfee::LazyCDProof::" + ee
.identify()),
36 d_pfEnabled(pnm
!= nullptr)
38 NodeManager
* nm
= NodeManager::currentNM();
39 d_true
= nm
->mkConst(true);
40 d_false
= nm
->mkConst(false);
43 bool ProofEqEngine::assertAssume(TNode lit
)
45 Trace("pfee") << "pfee::assertAssume " << lit
<< std::endl
;
46 // don't need to explicitly add anything to the proof here, since ASSUME
47 // nodes are constructed lazily
48 TNode atom
= lit
.getKind() == NOT
? lit
[0] : lit
;
49 bool polarity
= lit
.getKind() != NOT
;
51 // Second, assert it directly to the equality engine, where it is its own
52 // explanation. Notice we do not reference count atom/lit.
53 if (atom
.getKind() == EQUAL
)
57 // If proofs are enabled, we check if lit is an assertion of the form
58 // (= P true), (= P false), (= false P) or (= true P).
59 // Such literals must be handled as a special case here, since equality
60 // with Boolean constants have a special status internally within equality
61 // engine. In particular, the proofs constructed by EqProof conversion
62 // always produce proofs involving equalities with Boolean constants, and
63 // whose assumptions are only of the form P or (not P). However, in the
64 // case that (= P true) (resp (= P false)) is itself an input to the
65 // equality engine, we will explain in terms of P (resp. (not P)), which
66 // leads to a bogus proof, typically encountered in
67 // ProofNodeManager::mkScope.
69 // To correct this, we add an explicit *fact* that P holds by (= P true)
70 // here. This means that EqProof conversion may generate a proof where
71 // the internal equality (= P true) is justified by assumption P, and that
72 // afterwards, P is explained in terms of the original (external) equality
73 // (= P true) by the step provided here. This means that the proof may end
74 // up using (= P true) in a roundabout way (through two redundant steps),
75 // but regardless this allows the core proof utilities (EqProof
76 // conversion, proof equality engine, lazy proof, etc.) to be unconcerned
77 // with this case. Multiple users of the proof equality engine
78 // (SharedTermDatabase and TheoryArrays) require this special case.
79 if (atom
[0].getKind() == kind::CONST_BOOLEAN
80 || atom
[1].getKind() == kind::CONST_BOOLEAN
)
82 Node nlit
= Rewriter::rewrite(lit
);
83 if (!CDProof::isSame(lit
, nlit
))
85 // use a rewrite step as a fact
86 std::vector
<Node
> pfChildren
;
87 pfChildren
.push_back(lit
);
88 return assertFact(nlit
, PfRule::MACRO_SR_PRED_ELIM
, pfChildren
, {});
92 return d_ee
.assertEquality(atom
, polarity
, lit
);
94 return d_ee
.assertPredicate(atom
, polarity
, lit
);
97 bool ProofEqEngine::assertFact(Node lit
,
99 const std::vector
<Node
>& exp
,
100 const std::vector
<Node
>& args
)
102 Trace("pfee") << "pfee::assertFact " << lit
<< " " << id
<< ", exp = " << exp
103 << ", args = " << args
<< std::endl
;
105 Node atom
= lit
.getKind() == NOT
? lit
[0] : lit
;
106 bool polarity
= lit
.getKind() != NOT
;
107 // register the step in the proof
110 if (holds(atom
, polarity
))
112 // we do not process this fact if it already holds
115 // Buffer the step in the fact proof generator. We do this instead of
116 // adding explict steps to the lazy proof d_proof since CDProof has
117 // (at most) one proof for each formula. Thus, we "claim" only the
118 // formula that is proved by this fact. Otherwise, aliasing may occur,
119 // which leads to cyclic or bogus proofs.
124 d_factPg
.addStep(lit
, ps
);
125 // add lazy step to proof
126 d_proof
.addLazyStep(lit
, &d_factPg
, false);
128 // second, assert it to the equality engine
129 Node reason
= NodeManager::currentNM()->mkAnd(exp
);
130 return assertFactInternal(atom
, polarity
, reason
);
133 bool ProofEqEngine::assertFact(Node lit
,
136 const std::vector
<Node
>& args
)
138 Trace("pfee") << "pfee::assertFact " << lit
<< " " << id
<< ", exp = " << exp
139 << ", args = " << args
<< std::endl
;
140 Node atom
= lit
.getKind() == NOT
? lit
[0] : lit
;
141 bool polarity
= lit
.getKind() != NOT
;
142 // register the step in the proof
145 if (holds(atom
, polarity
))
147 // we do not process this fact if it already holds
150 // must extract the explanation as a vector
151 std::vector
<Node
> expv
;
152 // Flatten (single occurrences) of AND. We do not allow nested AND, it is
153 // the responsibilty of the caller to ensure these do not occur.
156 if (exp
.getKind() == AND
)
158 for (const Node
& expc
: exp
)
160 // should not have doubly nested AND
161 Assert(expc
.getKind() != AND
);
162 expv
.push_back(expc
);
170 // buffer the step in the fact proof generator
173 ps
.d_children
= expv
;
175 d_factPg
.addStep(lit
, ps
);
176 // add lazy step to proof
177 d_proof
.addLazyStep(lit
, &d_factPg
, false);
179 // second, assert it to the equality engine
180 return assertFactInternal(atom
, polarity
, exp
);
183 bool ProofEqEngine::assertFact(Node lit
, Node exp
, ProofStepBuffer
& psb
)
185 Trace("pfee") << "pfee::assertFact " << lit
<< ", exp = " << exp
186 << " via buffer with " << psb
.getNumSteps() << " steps"
188 Node atom
= lit
.getKind() == NOT
? lit
[0] : lit
;
189 bool polarity
= lit
.getKind() != NOT
;
192 if (holds(atom
, polarity
))
194 // we do not process this fact if it already holds
197 // buffer the steps in the fact proof generator
198 const std::vector
<std::pair
<Node
, ProofStep
>>& steps
= psb
.getSteps();
199 for (const std::pair
<Node
, ProofStep
>& step
: steps
)
201 d_factPg
.addStep(step
.first
, step
.second
);
203 // add lazy step to proof
204 d_proof
.addLazyStep(lit
, &d_factPg
, false);
206 // second, assert it to the equality engine
207 return assertFactInternal(atom
, polarity
, exp
);
210 bool ProofEqEngine::assertFact(Node lit
, Node exp
, ProofGenerator
* pg
)
212 Trace("pfee") << "pfee::assertFact " << lit
<< ", exp = " << exp
213 << " via generator" << std::endl
;
214 Node atom
= lit
.getKind() == NOT
? lit
[0] : lit
;
215 bool polarity
= lit
.getKind() != NOT
;
218 if (holds(atom
, polarity
))
220 // we do not process this fact if it already holds
223 // note the proof generator is responsible for remembering the explanation
224 d_proof
.addLazyStep(lit
, pg
, false);
226 // second, assert it to the equality engine
227 return assertFactInternal(atom
, polarity
, exp
);
230 TrustNode
ProofEqEngine::assertConflict(Node lit
)
232 Trace("pfee") << "pfee::assertConflict " << lit
<< std::endl
;
233 std::vector
<TNode
> assumps
;
234 explainWithProof(lit
, assumps
, &d_proof
);
237 // lit may not be equivalent to false, but should rewrite to false
240 Assert(Rewriter::rewrite(lit
) == d_false
)
241 << "pfee::assertConflict: conflict literal is not rewritable to "
243 std::vector
<Node
> exp
;
245 std::vector
<Node
> args
;
246 if (!d_proof
.addStep(d_false
, PfRule::MACRO_SR_PRED_ELIM
, exp
, args
))
248 Assert(false) << "pfee::assertConflict: failed conflict step";
249 return TrustNode::null();
253 return ensureProofForFact(
254 d_false
, assumps
, TrustNodeKind::CONFLICT
, &d_proof
);
257 TrustNode
ProofEqEngine::assertConflict(PfRule id
,
258 const std::vector
<Node
>& exp
,
259 const std::vector
<Node
>& args
)
261 Trace("pfee") << "pfee::assertConflict " << id
<< ", exp = " << exp
262 << ", args = " << args
<< std::endl
;
263 // conflict is same as proof of false
264 std::vector
<Node
> empVec
;
265 return assertLemma(d_false
, id
, exp
, empVec
, args
);
268 TrustNode
ProofEqEngine::assertConflict(const std::vector
<Node
>& exp
,
269 ProofStepBuffer
& psb
)
271 Trace("pfee") << "pfee::assertConflict " << exp
<< " via buffer with "
272 << psb
.getNumSteps() << " steps" << std::endl
;
275 if (!d_proof
.addSteps(psb
))
277 return TrustNode::null();
280 std::vector
<Node
> empVec
;
281 return assertLemmaInternal(d_false
, exp
, empVec
, &d_proof
);
284 TrustNode
ProofEqEngine::assertLemma(Node conc
,
286 const std::vector
<Node
>& exp
,
287 const std::vector
<Node
>& noExplain
,
288 const std::vector
<Node
>& args
)
290 Trace("pfee") << "pfee::assertLemma " << conc
<< " " << id
291 << ", exp = " << exp
<< ", noExplain = " << noExplain
292 << ", args = " << args
<< std::endl
;
293 Assert(conc
!= d_true
);
296 LazyCDProof
tmpProof(d_pnm
, &d_proof
);
300 // optimization: we can use the main lazy proof directly, because we
301 // know we will backtrack immediately after this call.
306 // use a lazy proof that always links to d_proof
309 // Register the proof step.
310 if (!curr
->addStep(conc
, id
, exp
, args
))
312 // a step went wrong, e.g. during checking
313 Assert(false) << "pfee::assertConflict: register proof step";
314 return TrustNode::null();
316 // We've now decided which lazy proof to use (curr), now get the proof
318 return assertLemmaInternal(conc
, exp
, noExplain
, curr
);
321 return assertLemmaInternal(conc
, exp
, noExplain
, nullptr);
324 TrustNode
ProofEqEngine::assertLemma(Node conc
,
325 const std::vector
<Node
>& exp
,
326 const std::vector
<Node
>& noExplain
,
327 ProofStepBuffer
& psb
)
329 Trace("pfee") << "pfee::assertLemma " << conc
<< ", exp = " << exp
330 << ", noExplain = " << noExplain
<< " via buffer with "
331 << psb
.getNumSteps() << " steps" << std::endl
;
334 LazyCDProof
tmpProof(d_pnm
, &d_proof
);
336 // same policy as above: for conflicts, use existing lazy proof
345 // add all steps to the proof
346 const std::vector
<std::pair
<Node
, ProofStep
>>& steps
= psb
.getSteps();
347 for (const std::pair
<Node
, ProofStep
>& ps
: steps
)
349 if (!curr
->addStep(ps
.first
, ps
.second
))
351 return TrustNode::null();
354 return assertLemmaInternal(conc
, exp
, noExplain
, curr
);
356 return assertLemmaInternal(conc
, exp
, noExplain
, nullptr);
359 TrustNode
ProofEqEngine::assertLemma(Node conc
,
360 const std::vector
<Node
>& exp
,
361 const std::vector
<Node
>& noExplain
,
364 Trace("pfee") << "pfee::assertLemma " << conc
<< ", exp = " << exp
365 << ", noExplain = " << noExplain
<< " via buffer with generator"
369 LazyCDProof
tmpProof(d_pnm
, &d_proof
);
371 // same policy as above: for conflicts, use existing lazy proof
380 // Register the proof step.
381 if (!pg
->addProofTo(conc
, curr
))
383 // a step went wrong, e.g. during checking
384 Assert(false) << "pfee::assertConflict: register proof step";
385 return TrustNode::null();
387 return assertLemmaInternal(conc
, exp
, noExplain
, curr
);
389 return assertLemmaInternal(conc
, exp
, noExplain
, nullptr);
392 TrustNode
ProofEqEngine::explain(Node conc
)
394 Trace("pfee") << "pfee::explain " << conc
<< std::endl
;
397 LazyCDProof
tmpProof(d_pnm
, &d_proof
);
398 std::vector
<TNode
> assumps
;
399 explainWithProof(conc
, assumps
, &tmpProof
);
400 return ensureProofForFact(
401 conc
, assumps
, TrustNodeKind::PROP_EXP
, &tmpProof
);
403 std::vector
<TNode
> assumps
;
404 explainWithProof(conc
, assumps
, nullptr);
405 return ensureProofForFact(conc
, assumps
, TrustNodeKind::PROP_EXP
, nullptr);
408 TrustNode
ProofEqEngine::assertLemmaInternal(Node conc
,
409 const std::vector
<Node
>& exp
,
410 const std::vector
<Node
>& noExplain
,
413 // We are a conflict if the conclusion is false and all literals are
416 conc
== d_false
? TrustNodeKind::CONFLICT
: TrustNodeKind::LEMMA
;
418 // get the explanation, with proofs
419 std::vector
<TNode
> assumps
;
420 std::vector
<Node
> expn
;
421 for (const Node
& e
: exp
)
423 if (std::find(noExplain
.begin(), noExplain
.end(), e
) == noExplain
.end())
425 explainWithProof(e
, assumps
, curr
);
429 // it did not have a proof; it was an assumption of the previous rule
430 assumps
.push_back(e
);
431 // it is not a conflict, since it may involve new literals
432 tnk
= TrustNodeKind::LEMMA
;
435 return ensureProofForFact(conc
, assumps
, tnk
, curr
);
438 TrustNode
ProofEqEngine::ensureProofForFact(Node conc
,
439 const std::vector
<TNode
>& assumps
,
443 Trace("pfee-proof") << std::endl
;
444 Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc
<< " via "
445 << assumps
<< ", TrustNodeKind=" << tnk
<< std::endl
;
446 NodeManager
* nm
= NodeManager::currentNM();
448 std::shared_ptr
<ProofNode
> pf
;
449 ProofGenerator
* pfg
= nullptr;
450 // the explanation is the conjunction of assumptions
452 // If proofs are enabled, generate the proof and possibly modify the
453 // assumptions to match SCOPE.
456 Assert(curr
!= nullptr);
457 Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
459 // get the proof for conc
460 std::shared_ptr
<ProofNode
> pfBody
= curr
->getProofFor(conc
);
461 if (pfBody
== nullptr)
464 << "pfee::ensureProofForFact: failed to make proof for fact"
467 // should have existed
468 Assert(false) << "pfee::assertConflict: failed to get proof for " << conc
;
469 return TrustNode::null();
471 // clone it so that we have a fresh copy
472 pfBody
= pfBody
->clone();
473 Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl
;
474 // The free assumptions must be closed by assumps, which should be passed
475 // as arguments of SCOPE. However, some of the free assumptions may not
476 // literally be equal to assumps, for instance, due to symmetry. In other
477 // words, the SCOPE could be closing (= x y) in a proof with free
478 // assumption (= y x). We modify the proof leaves to account for this
481 std::vector
<Node
> scopeAssumps
;
482 // we first ensure the assumptions are flattened
483 for (const TNode
& a
: assumps
)
485 if (a
.getKind() == AND
)
487 scopeAssumps
.insert(scopeAssumps
.end(), a
.begin(), a
.end());
491 scopeAssumps
.push_back(a
);
494 // scope the proof constructed above, and connect the formula with the proof
495 // minimize the assumptions
496 pf
= d_pnm
->mkScope(pfBody
, scopeAssumps
, true, true);
497 exp
= nm
->mkAnd(scopeAssumps
);
501 exp
= nm
->mkAnd(assumps
);
503 // Make the lemma or conflict node. This must exactly match the conclusion
506 if (tnk
== TrustNodeKind::CONFLICT
)
508 // conflict is negated
509 Assert(conc
== d_false
);
517 : (conc
== d_false
? exp
.negate() : nm
->mkNode(IMPLIES
, exp
, conc
));
519 Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
523 // should always be non-null
524 Assert(pf
!= nullptr);
525 if (Trace
.isOn("pfee-proof") || Trace
.isOn("pfee-proof-final"))
527 Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
529 std::stringstream ss
;
531 Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss
.str()
534 // Should be a closed proof now. If it is not, then the overall proof
536 Assert(pf
->isClosed());
538 // set the proof for the conflict or lemma, which can be queried later
541 case TrustNodeKind::CONFLICT
: setProofForConflict(formula
, pf
); break;
542 case TrustNodeKind::LEMMA
: setProofForLemma(formula
, pf
); break;
543 case TrustNodeKind::PROP_EXP
: setProofForPropExp(conc
, exp
, pf
); break;
546 Unhandled() << "Unhandled trust node kind " << tnk
;
550 Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
552 // we can provide a proof for conflict, lemma or explained propagation
555 case TrustNodeKind::CONFLICT
:
556 return TrustNode::mkTrustConflict(formula
, pfg
);
557 case TrustNodeKind::LEMMA
: return TrustNode::mkTrustLemma(formula
, pfg
);
558 case TrustNodeKind::PROP_EXP
:
559 return TrustNode::mkTrustPropExp(conc
, exp
, pfg
);
560 default: Unhandled() << "Unhandled trust node kind " << tnk
; break;
562 return TrustNode::null();
565 bool ProofEqEngine::assertFactInternal(TNode atom
, bool polarity
, TNode reason
)
567 Trace("pfee-debug") << "pfee::assertFactInternal: " << atom
<< " " << polarity
568 << " " << reason
<< std::endl
;
570 if (atom
.getKind() == EQUAL
)
572 ret
= d_ee
.assertEquality(atom
, polarity
, reason
);
576 ret
= d_ee
.assertPredicate(atom
, polarity
, reason
);
580 // must reference count the new atom and explanation
582 d_keep
.insert(reason
);
587 bool ProofEqEngine::holds(TNode atom
, bool polarity
)
589 if (atom
.getKind() == EQUAL
)
591 if (!d_ee
.hasTerm(atom
[0]) || !d_ee
.hasTerm(atom
[1]))
595 return polarity
? d_ee
.areEqual(atom
[0], atom
[1])
596 : d_ee
.areDisequal(atom
[0], atom
[1], false);
598 if (!d_ee
.hasTerm(atom
))
602 TNode b
= polarity
? d_true
: d_false
;
603 return d_ee
.areEqual(atom
, b
);
606 void ProofEqEngine::explainWithProof(Node lit
,
607 std::vector
<TNode
>& assumps
,
610 if (std::find(assumps
.begin(), assumps
.end(), lit
) != assumps
.end())
614 std::shared_ptr
<eq::EqProof
> pf
=
615 d_pfEnabled
? std::make_shared
<eq::EqProof
>() : nullptr;
616 Trace("pfee-proof") << "pfee::explainWithProof: " << lit
<< std::endl
;
617 bool polarity
= lit
.getKind() != NOT
;
618 TNode atom
= polarity
? lit
: lit
[0];
619 Assert(atom
.getKind() != AND
);
620 std::vector
<TNode
> tassumps
;
621 if (atom
.getKind() == EQUAL
)
623 if (atom
[0] == atom
[1])
627 Assert(d_ee
.hasTerm(atom
[0]));
628 Assert(d_ee
.hasTerm(atom
[1]));
631 // ensure the explanation exists
632 AlwaysAssert(d_ee
.areDisequal(atom
[0], atom
[1], true));
634 d_ee
.explainEquality(atom
[0], atom
[1], polarity
, tassumps
, pf
.get());
638 Assert(d_ee
.hasTerm(atom
));
639 d_ee
.explainPredicate(atom
, polarity
, tassumps
, pf
.get());
641 Trace("pfee-proof") << "...got " << tassumps
<< std::endl
;
643 for (const TNode a
: tassumps
)
647 assumps
.push_back(a
);
649 else if (std::find(assumps
.begin(), assumps
.end(), a
) == assumps
.end())
651 assumps
.push_back(a
);
656 if (Trace
.isOn("pfee-proof"))
658 Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
660 std::stringstream sse
;
661 pf
->debug_print(sse
);
662 Trace("pfee-proof") << sse
.str() << std::endl
;
663 Trace("pfee-proof") << "---" << std::endl
;
665 // add the steps in the equality engine proof to the Proof
666 pf
->addToProof(curr
);
668 Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl
;
671 ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context
* c
,
672 ProofNodeManager
* pnm
)
673 : ProofGenerator(), d_facts(c
), d_pnm(pnm
)
677 bool ProofEqEngine::FactProofGenerator::addStep(Node fact
, ProofStep ps
)
679 if (d_facts
.find(fact
) != d_facts
.end())
684 Node symFact
= CDProof::getSymmFact(fact
);
685 if (!symFact
.isNull())
687 if (d_facts
.find(symFact
) != d_facts
.end())
689 // duplicate due to symmetry
693 d_facts
.insert(fact
, std::make_shared
<ProofStep
>(ps
));
697 std::shared_ptr
<ProofNode
> ProofEqEngine::FactProofGenerator::getProofFor(
700 Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact
702 NodeProofStepMap::iterator it
= d_facts
.find(fact
);
703 if (it
== d_facts
.end())
705 Node symFact
= CDProof::getSymmFact(fact
);
706 if (symFact
.isNull())
708 Trace("pfee-fact-gen") << "...cannot find step" << std::endl
;
712 it
= d_facts
.find(symFact
);
713 if (it
== d_facts
.end())
716 Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl
;
720 Trace("pfee-fact-gen") << "...return via step " << *(*it
).second
<< std::endl
;
722 cdp
.addStep(fact
, *(*it
).second
);
723 return cdp
.getProofFor(fact
);
727 } // namespace theory