src/theory/uf/proof_equality_engine.cpp

   1 /*********************                                                        */
   2 /*! \file proof_equality_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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
  11  **
  12  ** \brief Implementation of the proof-producing equality engine
  13  **/
  14
  15 #include "theory/uf/proof_equality_engine.h"
  16
  17 #include "theory/rewriter.h"
  18 #include "theory/uf/proof_checker.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace eq {
  25
  26 ProofEqEngine::ProofEqEngine(context::Context* c,
  27                              context::UserContext* u,
  28                              EqualityEngine& ee,
  29                              ProofNodeManager* pnm)
  30     : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
  31       d_ee(ee),
  32       d_factPg(c, pnm),
  33       d_pnm(pnm),
  34       d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
  35       d_keep(c),
  36       d_pfEnabled(pnm != nullptr)
  37 {
  38   NodeManager* nm = NodeManager::currentNM();
  39   d_true = nm->mkConst(true);
  40   d_false = nm->mkConst(false);
  41 }
  42
  43 bool ProofEqEngine::assertAssume(TNode lit)
  44 {
  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;
  50
  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)
  54   {
  55     if (d_pfEnabled)
  56     {
  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.
  68       //
  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)
  81       {
  82         Node nlit = Rewriter::rewrite(lit);
  83         if (!CDProof::isSame(lit, nlit))
  84         {
  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, {});
  89         }
  90       }
  91     }
  92     return d_ee.assertEquality(atom, polarity, lit);
  93   }
  94   return d_ee.assertPredicate(atom, polarity, lit);
  95 }
  96
  97 bool ProofEqEngine::assertFact(Node lit,
  98                                PfRule id,
  99                                const std::vector<Node>& exp,
 100                                const std::vector<Node>& args)
 101 {
 102   Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
 103                 << ", args = " << args << std::endl;
 104
 105   Node atom = lit.getKind() == NOT ? lit[0] : lit;
 106   bool polarity = lit.getKind() != NOT;
 107   // register the step in the proof
 108   if (d_pfEnabled)
 109   {
 110     if (holds(atom, polarity))
 111     {
 112       // we do not process this fact if it already holds
 113       return false;
 114     }
 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.
 120     ProofStep ps;
 121     ps.d_rule = id;
 122     ps.d_children = exp;
 123     ps.d_args = args;
 124     d_factPg.addStep(lit, ps);
 125     // add lazy step to proof
 126     d_proof.addLazyStep(lit, &d_factPg, false);
 127   }
 128   // second, assert it to the equality engine
 129   Node reason = NodeManager::currentNM()->mkAnd(exp);
 130   return assertFactInternal(atom, polarity, reason);
 131 }
 132
 133 bool ProofEqEngine::assertFact(Node lit,
 134                                PfRule id,
 135                                Node exp,
 136                                const std::vector<Node>& args)
 137 {
 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
 143   if (d_pfEnabled)
 144   {
 145     if (holds(atom, polarity))
 146     {
 147       // we do not process this fact if it already holds
 148       return false;
 149     }
 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.
 154     if (exp != d_true)
 155     {
 156       if (exp.getKind() == AND)
 157       {
 158         for (const Node& expc : exp)
 159         {
 160           // should not have doubly nested AND
 161           Assert(expc.getKind() != AND);
 162           expv.push_back(expc);
 163         }
 164       }
 165       else
 166       {
 167         expv.push_back(exp);
 168       }
 169     }
 170     // buffer the step in the fact proof generator
 171     ProofStep ps;
 172     ps.d_rule = id;
 173     ps.d_children = expv;
 174     ps.d_args = args;
 175     d_factPg.addStep(lit, ps);
 176     // add lazy step to proof
 177     d_proof.addLazyStep(lit, &d_factPg, false);
 178   }
 179   // second, assert it to the equality engine
 180   return assertFactInternal(atom, polarity, exp);
 181 }
 182
 183 bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
 184 {
 185   Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
 186                 << " via buffer with " << psb.getNumSteps() << " steps"
 187                 << std::endl;
 188   Node atom = lit.getKind() == NOT ? lit[0] : lit;
 189   bool polarity = lit.getKind() != NOT;
 190   if (d_pfEnabled)
 191   {
 192     if (holds(atom, polarity))
 193     {
 194       // we do not process this fact if it already holds
 195       return false;
 196     }
 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)
 200     {
 201       d_factPg.addStep(step.first, step.second);
 202     }
 203     // add lazy step to proof
 204     d_proof.addLazyStep(lit, &d_factPg, false);
 205   }
 206   // second, assert it to the equality engine
 207   return assertFactInternal(atom, polarity, exp);
 208 }
 209
 210 bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
 211 {
 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;
 216   if (d_pfEnabled)
 217   {
 218     if (holds(atom, polarity))
 219     {
 220       // we do not process this fact if it already holds
 221       return false;
 222     }
 223     // note the proof generator is responsible for remembering the explanation
 224     d_proof.addLazyStep(lit, pg, false);
 225   }
 226   // second, assert it to the equality engine
 227   return assertFactInternal(atom, polarity, exp);
 228 }
 229
 230 TrustNode ProofEqEngine::assertConflict(Node lit)
 231 {
 232   Trace("pfee") << "pfee::assertConflict " << lit << std::endl;
 233   std::vector<TNode> assumps;
 234   explainWithProof(lit, assumps, &d_proof);
 235   if (d_pfEnabled)
 236   {
 237     // lit may not be equivalent to false, but should rewrite to false
 238     if (lit != d_false)
 239     {
 240       Assert(Rewriter::rewrite(lit) == d_false)
 241           << "pfee::assertConflict: conflict literal is not rewritable to "
 242              "false";
 243       std::vector<Node> exp;
 244       exp.push_back(lit);
 245       std::vector<Node> args;
 246       if (!d_proof.addStep(d_false, PfRule::MACRO_SR_PRED_ELIM, exp, args))
 247       {
 248         Assert(false) << "pfee::assertConflict: failed conflict step";
 249         return TrustNode::null();
 250       }
 251     }
 252   }
 253   return ensureProofForFact(
 254       d_false, assumps, TrustNodeKind::CONFLICT, &d_proof);
 255 }
 256
 257 TrustNode ProofEqEngine::assertConflict(PfRule id,
 258                                         const std::vector<Node>& exp,
 259                                         const std::vector<Node>& args)
 260 {
 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);
 266 }
 267
 268 TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
 269                                         ProofStepBuffer& psb)
 270 {
 271   Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with "
 272                 << psb.getNumSteps() << " steps" << std::endl;
 273   if (d_pfEnabled)
 274   {
 275     if (!d_proof.addSteps(psb))
 276     {
 277       return TrustNode::null();
 278     }
 279   }
 280   std::vector<Node> empVec;
 281   return assertLemmaInternal(d_false, exp, empVec, &d_proof);
 282 }
 283
 284 TrustNode ProofEqEngine::assertLemma(Node conc,
 285                                      PfRule id,
 286                                      const std::vector<Node>& exp,
 287                                      const std::vector<Node>& noExplain,
 288                                      const std::vector<Node>& args)
 289 {
 290   Trace("pfee") << "pfee::assertLemma " << conc << " " << id
 291                 << ", exp = " << exp << ", noExplain = " << noExplain
 292                 << ", args = " << args << std::endl;
 293   Assert(conc != d_true);
 294   if (d_pfEnabled)
 295   {
 296     LazyCDProof tmpProof(d_pnm, &d_proof);
 297     LazyCDProof* curr;
 298     if (conc == d_false)
 299     {
 300       // optimization: we can use the main lazy proof directly, because we
 301       // know we will backtrack immediately after this call.
 302       curr = &d_proof;
 303     }
 304     else
 305     {
 306       // use a lazy proof that always links to d_proof
 307       curr = &tmpProof;
 308     }
 309     // Register the proof step.
 310     if (!curr->addStep(conc, id, exp, args))
 311     {
 312       // a step went wrong, e.g. during checking
 313       Assert(false) << "pfee::assertConflict: register proof step";
 314       return TrustNode::null();
 315     }
 316     // We've now decided which lazy proof to use (curr), now get the proof
 317     // for conc.
 318     return assertLemmaInternal(conc, exp, noExplain, curr);
 319   }
 320   // not using a proof
 321   return assertLemmaInternal(conc, exp, noExplain, nullptr);
 322 }
 323
 324 TrustNode ProofEqEngine::assertLemma(Node conc,
 325                                      const std::vector<Node>& exp,
 326                                      const std::vector<Node>& noExplain,
 327                                      ProofStepBuffer& psb)
 328 {
 329   Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
 330                 << ", noExplain = " << noExplain << " via buffer with "
 331                 << psb.getNumSteps() << " steps" << std::endl;
 332   if (d_pfEnabled)
 333   {
 334     LazyCDProof tmpProof(d_pnm, &d_proof);
 335     LazyCDProof* curr;
 336     // same policy as above: for conflicts, use existing lazy proof
 337     if (conc == d_false)
 338     {
 339       curr = &d_proof;
 340     }
 341     else
 342     {
 343       curr = &tmpProof;
 344     }
 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)
 348     {
 349       if (!curr->addStep(ps.first, ps.second))
 350       {
 351         return TrustNode::null();
 352       }
 353     }
 354     return assertLemmaInternal(conc, exp, noExplain, curr);
 355   }
 356   return assertLemmaInternal(conc, exp, noExplain, nullptr);
 357 }
 358
 359 TrustNode ProofEqEngine::assertLemma(Node conc,
 360                                      const std::vector<Node>& exp,
 361                                      const std::vector<Node>& noExplain,
 362                                      ProofGenerator* pg)
 363 {
 364   Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
 365                 << ", noExplain = " << noExplain << " via buffer with generator"
 366                 << std::endl;
 367   if (d_pfEnabled)
 368   {
 369     LazyCDProof tmpProof(d_pnm, &d_proof);
 370     LazyCDProof* curr;
 371     // same policy as above: for conflicts, use existing lazy proof
 372     if (conc == d_false)
 373     {
 374       curr = &d_proof;
 375     }
 376     else
 377     {
 378       curr = &tmpProof;
 379     }
 380     // Register the proof step.
 381     if (!pg->addProofTo(conc, curr))
 382     {
 383       // a step went wrong, e.g. during checking
 384       Assert(false) << "pfee::assertConflict: register proof step";
 385       return TrustNode::null();
 386     }
 387     return assertLemmaInternal(conc, exp, noExplain, curr);
 388   }
 389   return assertLemmaInternal(conc, exp, noExplain, nullptr);
 390 }
 391
 392 TrustNode ProofEqEngine::explain(Node conc)
 393 {
 394   Trace("pfee") << "pfee::explain " << conc << std::endl;
 395   if (d_pfEnabled)
 396   {
 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);
 402   }
 403   std::vector<TNode> assumps;
 404   explainWithProof(conc, assumps, nullptr);
 405   return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, nullptr);
 406 }
 407
 408 TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
 409                                              const std::vector<Node>& exp,
 410                                              const std::vector<Node>& noExplain,
 411                                              LazyCDProof* curr)
 412 {
 413   // We are a conflict if the conclusion is false and all literals are
 414   // explained.
 415   TrustNodeKind tnk =
 416       conc == d_false ? TrustNodeKind::CONFLICT : TrustNodeKind::LEMMA;
 417
 418   // get the explanation, with proofs
 419   std::vector<TNode> assumps;
 420   std::vector<Node> expn;
 421   for (const Node& e : exp)
 422   {
 423     if (std::find(noExplain.begin(), noExplain.end(), e) == noExplain.end())
 424     {
 425       explainWithProof(e, assumps, curr);
 426     }
 427     else
 428     {
 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;
 433     }
 434   }
 435   return ensureProofForFact(conc, assumps, tnk, curr);
 436 }
 437
 438 TrustNode ProofEqEngine::ensureProofForFact(Node conc,
 439                                             const std::vector<TNode>& assumps,
 440                                             TrustNodeKind tnk,
 441                                             LazyCDProof* curr)
 442 {
 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();
 447   // The proof
 448   std::shared_ptr<ProofNode> pf;
 449   ProofGenerator* pfg = nullptr;
 450   // the explanation is the conjunction of assumptions
 451   Node exp;
 452   // If proofs are enabled, generate the proof and possibly modify the
 453   // assumptions to match SCOPE.
 454   if (d_pfEnabled)
 455   {
 456     Assert(curr != nullptr);
 457     Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
 458                         << std::endl;
 459     // get the proof for conc
 460     std::shared_ptr<ProofNode> pfBody = curr->getProofFor(conc);
 461     if (pfBody == nullptr)
 462     {
 463       Trace("pfee-proof")
 464           << "pfee::ensureProofForFact: failed to make proof for fact"
 465           << std::endl
 466           << std::endl;
 467       // should have existed
 468       Assert(false) << "pfee::assertConflict: failed to get proof for " << conc;
 469       return TrustNode::null();
 470     }
 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
 479     // below.
 480
 481     std::vector<Node> scopeAssumps;
 482     // we first ensure the assumptions are flattened
 483     for (const TNode& a : assumps)
 484     {
 485       if (a.getKind() == AND)
 486       {
 487         scopeAssumps.insert(scopeAssumps.end(), a.begin(), a.end());
 488       }
 489       else
 490       {
 491         scopeAssumps.push_back(a);
 492       }
 493     }
 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);
 498   }
 499   else
 500   {
 501     exp = nm->mkAnd(assumps);
 502   }
 503   // Make the lemma or conflict node. This must exactly match the conclusion
 504   // of SCOPE below.
 505   Node formula;
 506   if (tnk == TrustNodeKind::CONFLICT)
 507   {
 508     // conflict is negated
 509     Assert(conc == d_false);
 510     formula = exp;
 511   }
 512   else
 513   {
 514     formula =
 515         exp == d_true
 516             ? conc
 517             : (conc == d_false ? exp.negate() : nm->mkNode(IMPLIES, exp, conc));
 518   }
 519   Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
 520                       << std::endl;
 521   if (d_pfEnabled)
 522   {
 523     // should always be non-null
 524     Assert(pf != nullptr);
 525     if (Trace.isOn("pfee-proof") || Trace.isOn("pfee-proof-final"))
 526     {
 527       Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
 528                           << std::endl;
 529       std::stringstream ss;
 530       pf->printDebug(ss);
 531       Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss.str()
 532                           << std::endl;
 533     }
 534     // Should be a closed proof now. If it is not, then the overall proof
 535     // is malformed.
 536     Assert(pf->isClosed());
 537     pfg = this;
 538     // set the proof for the conflict or lemma, which can be queried later
 539     switch (tnk)
 540     {
 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;
 544       default:
 545         pfg = nullptr;
 546         Unhandled() << "Unhandled trust node kind " << tnk;
 547         break;
 548     }
 549   }
 550   Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
 551                       << std::endl;
 552   // we can provide a proof for conflict, lemma or explained propagation
 553   switch (tnk)
 554   {
 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;
 561   }
 562   return TrustNode::null();
 563 }
 564
 565 bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
 566 {
 567   Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
 568                       << " " << reason << std::endl;
 569   bool ret;
 570   if (atom.getKind() == EQUAL)
 571   {
 572     ret = d_ee.assertEquality(atom, polarity, reason);
 573   }
 574   else
 575   {
 576     ret = d_ee.assertPredicate(atom, polarity, reason);
 577   }
 578   if (ret)
 579   {
 580     // must reference count the new atom and explanation
 581     d_keep.insert(atom);
 582     d_keep.insert(reason);
 583   }
 584   return ret;
 585 }
 586
 587 bool ProofEqEngine::holds(TNode atom, bool polarity)
 588 {
 589   if (atom.getKind() == EQUAL)
 590   {
 591     if (!d_ee.hasTerm(atom[0]) || !d_ee.hasTerm(atom[1]))
 592     {
 593       return false;
 594     }
 595     return polarity ? d_ee.areEqual(atom[0], atom[1])
 596                     : d_ee.areDisequal(atom[0], atom[1], false);
 597   }
 598   if (!d_ee.hasTerm(atom))
 599   {
 600     return false;
 601   }
 602   TNode b = polarity ? d_true : d_false;
 603   return d_ee.areEqual(atom, b);
 604 }
 605
 606 void ProofEqEngine::explainWithProof(Node lit,
 607                                      std::vector<TNode>& assumps,
 608                                      LazyCDProof* curr)
 609 {
 610   if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
 611   {
 612     return;
 613   }
 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)
 622   {
 623     if (atom[0] == atom[1])
 624     {
 625       return;
 626     }
 627     Assert(d_ee.hasTerm(atom[0]));
 628     Assert(d_ee.hasTerm(atom[1]));
 629     if (!polarity)
 630     {
 631       // ensure the explanation exists
 632       AlwaysAssert(d_ee.areDisequal(atom[0], atom[1], true));
 633     }
 634     d_ee.explainEquality(atom[0], atom[1], polarity, tassumps, pf.get());
 635   }
 636   else
 637   {
 638     Assert(d_ee.hasTerm(atom));
 639     d_ee.explainPredicate(atom, polarity, tassumps, pf.get());
 640   }
 641   Trace("pfee-proof") << "...got " << tassumps << std::endl;
 642   // avoid duplicates
 643   for (const TNode a : tassumps)
 644   {
 645     if (a == lit)
 646     {
 647       assumps.push_back(a);
 648     }
 649     else if (std::find(assumps.begin(), assumps.end(), a) == assumps.end())
 650     {
 651       assumps.push_back(a);
 652     }
 653   }
 654   if (d_pfEnabled)
 655   {
 656     if (Trace.isOn("pfee-proof"))
 657     {
 658       Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
 659                           << std::endl;
 660       std::stringstream sse;
 661       pf->debug_print(sse);
 662       Trace("pfee-proof") << sse.str() << std::endl;
 663       Trace("pfee-proof") << "---" << std::endl;
 664     }
 665     // add the steps in the equality engine proof to the Proof
 666     pf->addToProof(curr);
 667   }
 668   Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
 669 }
 670
 671 ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c,
 672                                                       ProofNodeManager* pnm)
 673     : ProofGenerator(), d_facts(c), d_pnm(pnm)
 674 {
 675 }
 676
 677 bool ProofEqEngine::FactProofGenerator::addStep(Node fact, ProofStep ps)
 678 {
 679   if (d_facts.find(fact) != d_facts.end())
 680   {
 681     // duplicate
 682     return false;
 683   }
 684   Node symFact = CDProof::getSymmFact(fact);
 685   if (!symFact.isNull())
 686   {
 687     if (d_facts.find(symFact) != d_facts.end())
 688     {
 689       // duplicate due to symmetry
 690       return false;
 691     }
 692   }
 693   d_facts.insert(fact, std::make_shared<ProofStep>(ps));
 694   return true;
 695 }
 696
 697 std::shared_ptr<ProofNode> ProofEqEngine::FactProofGenerator::getProofFor(
 698     Node fact)
 699 {
 700   Trace("pfee-fact-gen") << "FactProofGenerator::getProofFor: " << fact
 701                          << std::endl;
 702   NodeProofStepMap::iterator it = d_facts.find(fact);
 703   if (it == d_facts.end())
 704   {
 705     Node symFact = CDProof::getSymmFact(fact);
 706     if (symFact.isNull())
 707     {
 708       Trace("pfee-fact-gen") << "...cannot find step" << std::endl;
 709       Assert(false);
 710       return nullptr;
 711     }
 712     it = d_facts.find(symFact);
 713     if (it == d_facts.end())
 714     {
 715       Assert(false);
 716       Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl;
 717       return nullptr;
 718     }
 719   }
 720   Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
 721   CDProof cdp(d_pnm);
 722   cdp.addStep(fact, *(*it).second);
 723   return cdp.getProofFor(fact);
 724 }
 725
 726 }  // namespace eq
 727 }  // namespace theory
 728 }  // namespace CVC4