src/prop/sat_proof_manager.cpp

   1 /*********************                                                        */
   2 /*! \file sat_proof_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa
   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 manager for Minisat
  13  **/
  14
  15 #include "prop/sat_proof_manager.h"
  16
  17 #include "expr/proof_node_algorithm.h"
  18 #include "options/smt_options.h"
  19 #include "prop/cnf_stream.h"
  20 #include "prop/minisat/minisat.h"
  21 #include "theory/theory_proof_step_buffer.h"
  22
  23 namespace CVC4 {
  24 namespace prop {
  25
  26 SatProofManager::SatProofManager(Minisat::Solver* solver,
  27                                  CnfStream* cnfStream,
  28                                  context::UserContext* userContext,
  29                                  ProofNodeManager* pnm)
  30     : d_solver(solver),
  31       d_cnfStream(cnfStream),
  32       d_pnm(pnm),
  33       d_resChains(pnm, true, userContext),
  34       d_resChainPg(userContext, pnm),
  35       d_assumptions(userContext),
  36       d_conflictLit(undefSatVariable)
  37 {
  38   d_false = NodeManager::currentNM()->mkConst(false);
  39 }
  40
  41 void SatProofManager::printClause(const Minisat::Clause& clause)
  42 {
  43   for (unsigned i = 0, size = clause.size(); i < size; ++i)
  44   {
  45     SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
  46     Trace("sat-proof") << satLit << " ";
  47   }
  48 }
  49
  50 Node SatProofManager::getClauseNode(SatLiteral satLit)
  51 {
  52   Assert(d_cnfStream->getNodeCache().find(satLit)
  53          != d_cnfStream->getNodeCache().end())
  54       << "SatProofManager::getClauseNode: literal " << satLit
  55       << " undefined.\n";
  56   return d_cnfStream->getNodeCache()[satLit];
  57 }
  58
  59 Node SatProofManager::getClauseNode(const Minisat::Clause& clause)
  60 {
  61   std::vector<Node> clauseNodes;
  62   for (unsigned i = 0, size = clause.size(); i < size; ++i)
  63   {
  64     SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
  65     Assert(d_cnfStream->getNodeCache().find(satLit)
  66            != d_cnfStream->getNodeCache().end())
  67         << "SatProofManager::getClauseNode: literal " << satLit
  68         << " undefined\n";
  69     clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]);
  70   }
  71   // order children by node id
  72   std::sort(clauseNodes.begin(), clauseNodes.end());
  73   return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes);
  74 }
  75
  76 void SatProofManager::startResChain(const Minisat::Clause& start)
  77 {
  78   if (Trace.isOn("sat-proof"))
  79   {
  80     Trace("sat-proof") << "SatProofManager::startResChain: ";
  81     printClause(start);
  82     Trace("sat-proof") << "\n";
  83   }
  84   d_resLinks.push_back(
  85       std::pair<Node, Node>(getClauseNode(start), Node::null()));
  86 }
  87
  88 void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant)
  89 {
  90   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
  91   if (!redundant)
  92   {
  93     Trace("sat-proof") << "SatProofManager::addResolutionStep: [" << satLit
  94                        << "] " << ~satLit << "\n";
  95     d_resLinks.push_back(
  96         std::pair<Node, Node>(d_cnfStream->getNodeCache()[~satLit],
  97                               d_cnfStream->getNodeCache()[satLit]));
  98   }
  99   else
 100   {
 101     Trace("sat-proof") << "SatProofManager::addResolutionStep: redundant lit "
 102                        << satLit << " stored\n";
 103     d_redundantLits.push_back(satLit);
 104   }
 105 }
 106
 107 void SatProofManager::addResolutionStep(const Minisat::Clause& clause,
 108                                         Minisat::Lit lit)
 109 {
 110   // the given clause is supposed to be the second in a resolution, with the
 111   // given literal as the pivot occurring positive in the first and negatively
 112   // in the second clause. Thus, we store its negation
 113   SatLiteral satLit = MinisatSatSolver::toSatLiteral(~lit);
 114   Node clauseNode = getClauseNode(clause);
 115   d_resLinks.push_back(
 116       std::pair<Node, Node>(clauseNode, d_cnfStream->getNodeCache()[satLit]));
 117   if (Trace.isOn("sat-proof"))
 118   {
 119     Trace("sat-proof") << "SatProofManager::addResolutionStep: [" << satLit
 120                        << "] ";
 121     printClause(clause);
 122     Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t"
 123                        << clauseNode << "\n";
 124   }
 125 }
 126
 127 void SatProofManager::endResChain(Minisat::Lit lit)
 128 {
 129   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
 130   Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
 131                      << satLit;
 132   endResChain(getClauseNode(satLit), {satLit});
 133 }
 134
 135 void SatProofManager::endResChain(const Minisat::Clause& clause)
 136 {
 137   if (Trace.isOn("sat-proof"))
 138   {
 139     Trace("sat-proof") << "SatProofManager::endResChain: chain_res for ";
 140     printClause(clause);
 141   }
 142   std::set<SatLiteral> clauseLits;
 143   for (unsigned i = 0, size = clause.size(); i < size; ++i)
 144   {
 145     clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i]));
 146   }
 147   endResChain(getClauseNode(clause), clauseLits);
 148 }
 149
 150 void SatProofManager::endResChain(Node conclusion,
 151                                   const std::set<SatLiteral>& conclusionLits)
 152 {
 153   Trace("sat-proof") << ", " << conclusion << "\n";
 154   // first process redundant literals
 155   std::set<SatLiteral> visited;
 156   unsigned pos = d_resLinks.size();
 157   for (SatLiteral satLit : d_redundantLits)
 158   {
 159     processRedundantLit(satLit, conclusionLits, visited, pos);
 160   }
 161   d_redundantLits.clear();
 162   // build resolution chain
 163   std::vector<Node> children, args;
 164   for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i)
 165   {
 166     children.push_back(d_resLinks[i].first);
 167     Trace("sat-proof") << "SatProofManager::endResChain:   ";
 168     if (i > 0)
 169     {
 170       Trace("sat-proof")
 171           << "[" << d_cnfStream->getTranslationCache()[d_resLinks[i].second]
 172           << "] ";
 173     }
 174     // special case for clause (or l1 ... ln) being a single literal
 175     // corresponding itself to a clause, which is indicated by the pivot being
 176     // of the form (not (or l1 ... ln))
 177     if (d_resLinks[i].first.getKind() == kind::OR
 178         && !(d_resLinks[i].second.getKind() == kind::NOT
 179              && d_resLinks[i].second[0].getKind() == kind::OR
 180              && d_resLinks[i].second[0] == d_resLinks[i].first))
 181     {
 182       for (unsigned j = 0, sizeJ = d_resLinks[i].first.getNumChildren();
 183            j < sizeJ;
 184            ++j)
 185       {
 186         Trace("sat-proof")
 187             << d_cnfStream->getTranslationCache()[d_resLinks[i].first[j]];
 188         if (j < sizeJ - 1)
 189         {
 190           Trace("sat-proof") << ", ";
 191         }
 192       }
 193     }
 194     else
 195     {
 196       Assert(d_cnfStream->getTranslationCache().find(d_resLinks[i].first)
 197              != d_cnfStream->getTranslationCache().end())
 198           << "clause node " << d_resLinks[i].first
 199           << " treated as unit has no literal. Pivot is "
 200           << d_resLinks[i].second << "\n";
 201       Trace("sat-proof")
 202           << d_cnfStream->getTranslationCache()[d_resLinks[i].first];
 203     }
 204     Trace("sat-proof") << " : ";
 205     if (i > 0)
 206     {
 207       args.push_back(d_resLinks[i].second);
 208       Trace("sat-proof") << "[" << d_resLinks[i].second << "] ";
 209     }
 210     Trace("sat-proof") << d_resLinks[i].first << "\n";
 211   }
 212   // clearing
 213   d_resLinks.clear();
 214   // whether no-op
 215   if (children.size() == 1)
 216   {
 217     Trace("sat-proof") << "SatProofManager::endResChain: no-op. The conclusion "
 218                        << conclusion << " is set-equal to premise "
 219                        << children[0] << "\n";
 220     return;
 221   }
 222   if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion))
 223   {
 224     Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of "
 225                        << conclusion << "\n";
 226   }
 227   // since the conclusion can be both reordered and without duplicates and the
 228   // SAT solver does not record this information, we must recompute it here so
 229   // the proper CHAIN_RESOLUTION step can be created
 230   // compute chain resolution conclusion
 231   Node chainConclusion = d_pnm->getChecker()->checkDebug(
 232       PfRule::CHAIN_RESOLUTION, children, args, Node::null(), "");
 233   Trace("sat-proof")
 234       << "SatProofManager::endResChain: creating step for computed conclusion "
 235       << chainConclusion << "\n";
 236   // buffer steps
 237   theory::TheoryProofStepBuffer psb;
 238   psb.addStep(PfRule::CHAIN_RESOLUTION, children, args, chainConclusion);
 239   if (chainConclusion != conclusion)
 240   {
 241     // if this happens that chainConclusion needs to be factored and/or
 242     // reordered, which in either case can be done only if it's not a unit
 243     // clause.
 244     CVC4_UNUSED Node reducedChainConclusion =
 245         psb.factorReorderElimDoubleNeg(chainConclusion);
 246     Assert(reducedChainConclusion == conclusion)
 247         << "original conclusion " << conclusion
 248         << "\nis different from computed conclusion " << chainConclusion
 249         << "\nafter factorReorderElimDoubleNeg " << reducedChainConclusion;
 250   }
 251   // buffer the steps in the resolution chain proof generator
 252   const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
 253   for (const std::pair<Node, ProofStep>& step : steps)
 254   {
 255     Trace("sat-proof") << "SatProofManager::endResChain: adding for "
 256                        << step.first << " step " << step.second << "\n";
 257     d_resChainPg.addStep(step.first, step.second);
 258     // the premises of this resolution may not have been justified yet, so we do
 259     // not pass assumptions to check closedness
 260     d_resChains.addLazyStep(step.first, &d_resChainPg);
 261   }
 262 }
 263
 264 void SatProofManager::processRedundantLit(
 265     SatLiteral lit,
 266     const std::set<SatLiteral>& conclusionLits,
 267     std::set<SatLiteral>& visited,
 268     unsigned pos)
 269 {
 270   Trace("sat-proof") << push
 271                      << "SatProofManager::processRedundantLit: Lit: " << lit
 272                      << "\n";
 273   if (visited.count(lit))
 274   {
 275     Trace("sat-proof") << "already visited\n" << pop;
 276     return;
 277   }
 278   Minisat::Solver::TCRef reasonRef =
 279       d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
 280   if (reasonRef == Minisat::Solver::TCRef_Undef)
 281   {
 282     Trace("sat-proof") << "unit, add link to lit " << lit << " at pos: " << pos
 283                        << "\n"
 284                        << pop;
 285     visited.insert(lit);
 286     d_resLinks.insert(d_resLinks.begin() + pos,
 287                       std::pair<Node, Node>(d_cnfStream->getNodeCache()[~lit],
 288                                             d_cnfStream->getNodeCache()[lit]));
 289     return;
 290   }
 291   Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size())
 292       << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
 293       << d_solver->ca.size() << "\n";
 294   const Minisat::Clause& reason = d_solver->ca[reasonRef];
 295   if (Trace.isOn("sat-proof"))
 296   {
 297     Trace("sat-proof") << "reason: ";
 298     printClause(reason);
 299     Trace("sat-proof") << "\n";
 300   }
 301   // check if redundant literals in the reason. The first literal is the one we
 302   // will be eliminating, so we check the others
 303   for (unsigned i = 1, size = reason.size(); i < size; ++i)
 304   {
 305     SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]);
 306     // if literal does not occur in the conclusion we process it as well
 307     if (!conclusionLits.count(satLit))
 308     {
 309       processRedundantLit(satLit, conclusionLits, visited, pos);
 310     }
 311   }
 312   Assert(!visited.count(lit));
 313   visited.insert(lit);
 314   Trace("sat-proof") << "clause, add link to lit " << lit << " at pos: " << pos
 315                      << "\n"
 316                      << pop;
 317   // add the step before steps for children. Note that the step is with the
 318   // reason, not only with ~lit, since the learned clause is built under the
 319   // assumption that the redundant literal is removed via the resolution with
 320   // the explanation of its negation
 321   Node clauseNode = getClauseNode(reason);
 322   d_resLinks.insert(
 323       d_resLinks.begin() + pos,
 324       std::pair<Node, Node>(clauseNode, d_cnfStream->getNodeCache()[lit]));
 325 }
 326
 327 void SatProofManager::explainLit(
 328     SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& premises)
 329 {
 330   Node litNode = getClauseNode(lit);
 331   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit
 332                      << " [" << litNode << "]\n";
 333   Minisat::Solver::TCRef reasonRef =
 334       d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
 335   if (reasonRef == Minisat::Solver::TCRef_Undef)
 336   {
 337     Trace("sat-proof") << "SatProofManager::explainLit: no SAT reason\n" << pop;
 338     return;
 339   }
 340   Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size())
 341       << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
 342       << d_solver->ca.size() << "\n";
 343   const Minisat::Clause& reason = d_solver->ca[reasonRef];
 344   unsigned size = reason.size();
 345   if (Trace.isOn("sat-proof"))
 346   {
 347     Trace("sat-proof") << "SatProofManager::explainLit: with clause: ";
 348     printClause(reason);
 349     Trace("sat-proof") << "\n";
 350   }
 351   // pedantically check that the negation of the literal to explain *does not*
 352   // occur in the reason, otherwise we will loop forever
 353   for (unsigned i = 0; i < size; ++i)
 354   {
 355     AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit)
 356         << "cyclic justification\n";
 357   }
 358   // add the reason clause first
 359   std::vector<Node> children{getClauseNode(reason)}, args;
 360   // save in the premises
 361   premises.insert(children.back());
 362   Trace("sat-proof") << push;
 363   for (unsigned i = 0; i < size; ++i)
 364   {
 365     SatLiteral curr_lit = MinisatSatSolver::toSatLiteral(reason[i]);
 366     // ignore the lit we are trying to explain...
 367     if (curr_lit == lit)
 368     {
 369       continue;
 370     }
 371     std::unordered_set<TNode, TNodeHashFunction> childPremises;
 372     explainLit(~curr_lit, childPremises);
 373     // save to resolution chain premises / arguments
 374     Assert(d_cnfStream->getNodeCache().find(curr_lit)
 375            != d_cnfStream->getNodeCache().end());
 376     children.push_back(d_cnfStream->getNodeCache()[~curr_lit]);
 377     args.push_back(d_cnfStream->getNodeCache()[curr_lit]);
 378     // add child premises and the child itself
 379     premises.insert(childPremises.begin(), childPremises.end());
 380     premises.insert(d_cnfStream->getNodeCache()[~curr_lit]);
 381   }
 382   if (Trace.isOn("sat-proof"))
 383   {
 384     Trace("sat-proof") << pop << "SatProofManager::explainLit: chain_res for "
 385                        << lit << ", " << litNode << " with clauses:\n";
 386     for (unsigned i = 0, csize = children.size(); i < csize; ++i)
 387     {
 388       Trace("sat-proof") << "SatProofManager::explainLit:   " << children[i];
 389       if (i > 0)
 390       {
 391         Trace("sat-proof") << " [" << args[i - 1] << "]";
 392       }
 393       Trace("sat-proof") << "\n";
 394     }
 395   }
 396   // if justification of children contains the expected conclusion, avoid the
 397   // cyclic proof by aborting.
 398   if (premises.count(litNode))
 399   {
 400     Trace("sat-proof") << "SatProofManager::explainLit: CYCLIC PROOF of " << lit
 401                        << " [" << litNode << "], ABORT\n"
 402                        << pop;
 403     return;
 404   }
 405   Trace("sat-proof") << pop;
 406   // create step
 407   ProofStep ps(PfRule::CHAIN_RESOLUTION, children, args);
 408   d_resChainPg.addStep(litNode, ps);
 409   // the premises in the limit of the justification may correspond to other
 410   // links in the chain which have, themselves, literals yet to be justified. So
 411   // we are not ready yet to check closedness w.r.t. CNF transformation of the
 412   // preprocessed assertions
 413   d_resChains.addLazyStep(litNode, &d_resChainPg);
 414 }
 415
 416 void SatProofManager::finalizeProof(Node inConflictNode,
 417                                     const std::vector<SatLiteral>& inConflict)
 418 {
 419   Trace("sat-proof")
 420       << "SatProofManager::finalizeProof: conflicting clause node: "
 421       << inConflictNode << "\n";
 422   // nothing to do
 423   if (inConflictNode == d_false)
 424   {
 425     return;
 426   }
 427   if (Trace.isOn("sat-proof-debug2"))
 428   {
 429     Trace("sat-proof-debug2")
 430         << push << "SatProofManager::finalizeProof: saved proofs in chain:\n";
 431     std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
 432     std::unordered_set<Node, NodeHashFunction> skip;
 433     for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links)
 434     {
 435       if (skip.count(link.first))
 436       {
 437         continue;
 438       }
 439       auto it = d_cnfStream->getTranslationCache().find(link.first);
 440       if (it != d_cnfStream->getTranslationCache().end())
 441       {
 442         Trace("sat-proof-debug2")
 443             << "SatProofManager::finalizeProof:  " << it->second;
 444       }
 445       // a refl step added due to double elim negation, ignore
 446       else if (link.second->getRule() == PfRule::REFL)
 447       {
 448         continue;
 449       }
 450       // a clause
 451       else
 452       {
 453         Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:";
 454         Assert(link.first.getKind() == kind::OR) << link.first;
 455         for (const Node& n : link.first)
 456         {
 457           it = d_cnfStream->getTranslationCache().find(n);
 458           Assert(it != d_cnfStream->getTranslationCache().end());
 459           Trace("sat-proof-debug2") << it->second << " ";
 460         }
 461       }
 462       Trace("sat-proof-debug2") << "\n";
 463       Trace("sat-proof-debug2")
 464           << "SatProofManager::finalizeProof: " << link.first << "\n";
 465       // get resolution
 466       Node cur = link.first;
 467       std::shared_ptr<ProofNode> pfn = link.second;
 468       while (pfn->getRule() != PfRule::CHAIN_RESOLUTION)
 469       {
 470         Assert(pfn->getChildren().size() == 1
 471                && pfn->getChildren()[0]->getRule() == PfRule::ASSUME)
 472             << *link.second.get() << "\n"
 473             << *pfn.get();
 474         cur = pfn->getChildren()[0]->getResult();
 475         // retrieve justification of assumption in the links
 476         Assert(links.find(cur) != links.end());
 477         pfn = links[cur];
 478         // ignore it in the rest of the outside loop
 479         skip.insert(cur);
 480       }
 481       std::vector<Node> fassumps;
 482       expr::getFreeAssumptions(pfn.get(), fassumps);
 483       Trace("sat-proof-debug2") << push;
 484       for (const Node& fa : fassumps)
 485       {
 486         Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:   - ";
 487         it = d_cnfStream->getTranslationCache().find(fa);
 488         if (it != d_cnfStream->getTranslationCache().end())
 489         {
 490           Trace("sat-proof-debug2") << it->second << "\n";
 491           continue;
 492         }
 493         // then it's a clause
 494         Assert(fa.getKind() == kind::OR);
 495         for (const Node& n : fa)
 496         {
 497           it = d_cnfStream->getTranslationCache().find(n);
 498           Assert(it != d_cnfStream->getTranslationCache().end());
 499           Trace("sat-proof-debug2") << it->second << " ";
 500         }
 501         Trace("sat-proof-debug2") << "\n";
 502       }
 503       Trace("sat-proof-debug2") << pop;
 504       Trace("sat-proof-debug2")
 505           << "SatProofManager::finalizeProof:  " << *pfn.get() << "\n=======\n";
 506       ;
 507     }
 508     Trace("sat-proof-debug2") << pop;
 509   }
 510   // We will resolve away of the literals l_1...l_n in inConflict. At this point
 511   // each ~l_i must be either explainable, the result of a previously saved
 512   // resolution chain, or an input. In account of it possibly being the first,
 513   // we call explainLit on each ~l_i while accumulating the children and
 514   // arguments for the resolution step to conclude false.
 515   std::vector<Node> children{inConflictNode}, args;
 516   std::unordered_set<TNode, TNodeHashFunction> premises;
 517   for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
 518   {
 519     Assert(d_cnfStream->getNodeCache().find(inConflict[i])
 520            != d_cnfStream->getNodeCache().end());
 521     std::unordered_set<TNode, TNodeHashFunction> childPremises;
 522     explainLit(~inConflict[i], childPremises);
 523     Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]];
 524     // save to resolution chain premises / arguments
 525     children.push_back(negatedLitNode);
 526     args.push_back(d_cnfStream->getNodeCache()[inConflict[i]]);
 527     // add child premises and the child itself
 528     premises.insert(childPremises.begin(), childPremises.end());
 529     premises.insert(negatedLitNode);
 530     Trace("sat-proof") << "===========\n";
 531   }
 532   if (Trace.isOn("sat-proof"))
 533   {
 534     Trace("sat-proof") << "SatProofManager::finalizeProof: chain_res for false "
 535                           "with clauses:\n";
 536     for (unsigned i = 0, size = children.size(); i < size; ++i)
 537     {
 538       Trace("sat-proof") << "SatProofManager::finalizeProof:   " << children[i];
 539       if (i > 0)
 540       {
 541         Trace("sat-proof") << " [" << args[i - 1] << "]";
 542       }
 543       Trace("sat-proof") << "\n";
 544     }
 545   }
 546   // create step
 547   ProofStep ps(PfRule::CHAIN_RESOLUTION, children, args);
 548   d_resChainPg.addStep(d_false, ps);
 549   // not yet ready to check closedness because maybe only now we will justify
 550   // literals used in resolutions
 551   d_resChains.addLazyStep(d_false, &d_resChainPg);
 552   // Fix point justification of literals in leaves of the proof of false
 553   bool expanded;
 554   do
 555   {
 556     expanded = false;
 557     Trace("sat-proof") << "expand assumptions to prove false\n";
 558     std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
 559     Assert(pfn);
 560     Trace("sat-proof-debug") << "sat proof of flase: " << *pfn.get() << "\n";
 561     std::vector<Node> fassumps;
 562     expr::getFreeAssumptions(pfn.get(), fassumps);
 563     if (Trace.isOn("sat-proof"))
 564     {
 565       for (const Node& fa : fassumps)
 566       {
 567         Trace("sat-proof") << "- ";
 568         auto it = d_cnfStream->getTranslationCache().find(fa);
 569         if (it != d_cnfStream->getTranslationCache().end())
 570         {
 571           Trace("sat-proof") << it->second << "\n";
 572           Trace("sat-proof") << "- " << fa << "\n";
 573           continue;
 574         }
 575         // then it's a clause
 576         Assert(fa.getKind() == kind::OR);
 577         for (const Node& n : fa)
 578         {
 579           it = d_cnfStream->getTranslationCache().find(n);
 580           Assert(it != d_cnfStream->getTranslationCache().end());
 581           Trace("sat-proof") << it->second << " ";
 582         }
 583         Trace("sat-proof") << "\n";
 584         Trace("sat-proof") << "- " << fa << "\n";
 585       }
 586     }
 587
 588     // for each assumption, see if it has a reason
 589     for (const Node& fa : fassumps)
 590     {
 591       // ignore already processed assumptions
 592       if (premises.count(fa))
 593       {
 594         Trace("sat-proof") << "already processed assumption " << fa << "\n";
 595         continue;
 596       }
 597       // ignore input assumptions. This is necessary to avoid rare collisions
 598       // between input clauses and literals that are equivalent at the node
 599       // level. In trying to justify the literal below if, it was previously
 600       // propagated (say, in a previous check-sat call that survived the
 601       // user-context changes) but no longer holds, then we may introduce a
 602       // bogus proof for it, rather than keeping it as an input.
 603       if (d_assumptions.contains(fa))
 604       {
 605         Trace("sat-proof") << "input assumption " << fa << "\n";
 606         continue;
 607       }
 608       // ignore non-literals
 609       auto it = d_cnfStream->getTranslationCache().find(fa);
 610       if (it == d_cnfStream->getTranslationCache().end())
 611       {
 612         Trace("sat-proof") << "no lit assumption " << fa << "\n";
 613         premises.insert(fa);
 614         continue;
 615       }
 616       Trace("sat-proof") << "lit assumption (" << it->second << "), " << fa
 617                          << "\n";
 618       // mark another iteration for the loop, as some resolution link may be
 619       // connected because of the new justifications
 620       expanded = true;
 621       std::unordered_set<TNode, TNodeHashFunction> childPremises;
 622       explainLit(it->second, childPremises);
 623       // add the premises used in the justification. We know they will have
 624       // been as expanded as possible
 625       premises.insert(childPremises.begin(), childPremises.end());
 626       // add free assumption itself
 627       premises.insert(fa);
 628     }
 629   } while (expanded);
 630   // now we should be able to close it
 631   if (options::proofNewEagerChecking())
 632   {
 633     std::vector<Node> assumptionsVec;
 634     for (const Node& a : d_assumptions)
 635     {
 636       assumptionsVec.push_back(a);
 637     }
 638     d_resChains.addLazyStep(d_false, &d_resChainPg, assumptionsVec);
 639   }
 640 }
 641
 642 void SatProofManager::storeUnitConflict(Minisat::Lit inConflict)
 643 {
 644   Assert(d_conflictLit == undefSatVariable);
 645   d_conflictLit = MinisatSatSolver::toSatLiteral(inConflict);
 646 }
 647
 648 void SatProofManager::finalizeProof()
 649 {
 650   Assert(d_conflictLit != undefSatVariable);
 651   Trace("sat-proof")
 652       << "SatProofManager::finalizeProof: conflicting (lazy) satLit: "
 653       << d_conflictLit << "\n";
 654   finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit});
 655 }
 656
 657 void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding)
 658 {
 659   SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict);
 660   Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: "
 661                      << satLit << "\n";
 662   Node clauseNode = getClauseNode(satLit);
 663   if (adding)
 664   {
 665     registerSatAssumptions({clauseNode});
 666   }
 667   finalizeProof(clauseNode, {satLit});
 668 }
 669
 670 void SatProofManager::finalizeProof(const Minisat::Clause& inConflict,
 671                                     bool adding)
 672 {
 673   if (Trace.isOn("sat-proof"))
 674   {
 675     Trace("sat-proof")
 676         << "SatProofManager::finalizeProof: conflicting clause: ";
 677     printClause(inConflict);
 678     Trace("sat-proof") << "\n";
 679   }
 680   std::vector<SatLiteral> clause;
 681   for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
 682   {
 683     clause.push_back(MinisatSatSolver::toSatLiteral(inConflict[i]));
 684   }
 685   Node clauseNode = getClauseNode(inConflict);
 686   if (adding)
 687   {
 688     registerSatAssumptions({clauseNode});
 689   }
 690   finalizeProof(clauseNode, clause);
 691 }
 692
 693 std::shared_ptr<ProofNode> SatProofManager::getProof()
 694 {
 695   std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
 696   if (!pfn)
 697   {
 698     pfn = d_pnm->mkAssume(d_false);
 699   }
 700   return pfn;
 701 }
 702
 703 void SatProofManager::registerSatLitAssumption(Minisat::Lit lit)
 704 {
 705   Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - "
 706                      << getClauseNode(MinisatSatSolver::toSatLiteral(lit))
 707                      << "\n";
 708   d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit)));
 709 }
 710
 711 void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
 712 {
 713   for (const Node& a : assumps)
 714   {
 715     Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a
 716                        << "\n";
 717     d_assumptions.insert(a);
 718   }
 719 }
 720
 721 }  // namespace prop
 722 }  // namespace CVC4