src/prop/sat_proof_manager.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Haniel Barbosa, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Implementation of the proof manager for Minisat.
  14  */
  15
  16 #include "prop/sat_proof_manager.h"
  17
  18 #include "options/proof_options.h"
  19 #include "proof/proof_node_algorithm.h"
  20 #include "proof/theory_proof_step_buffer.h"
  21 #include "prop/cnf_stream.h"
  22 #include "prop/minisat/minisat.h"
  23
  24 namespace cvc5 {
  25 namespace prop {
  26
  27 SatProofManager::SatProofManager(Env& env,
  28                                  Minisat::Solver* solver,
  29                                  CnfStream* cnfStream)
  30     : EnvObj(env),
  31       d_solver(solver),
  32       d_cnfStream(cnfStream),
  33       d_resChains(d_env.getProofNodeManager(), true, userContext()),
  34       d_resChainPg(userContext(), d_env.getProofNodeManager()),
  35       d_assumptions(userContext()),
  36       d_conflictLit(undefSatVariable),
  37       d_optResLevels(userContext()),
  38       d_optResManager(userContext(), &d_resChains, d_optResProofs)
  39 {
  40   d_true = NodeManager::currentNM()->mkConst(true);
  41   d_false = NodeManager::currentNM()->mkConst(false);
  42 }
  43
  44 void SatProofManager::printClause(const Minisat::Clause& clause)
  45 {
  46   for (size_t i = 0, size = clause.size(); i < size; ++i)
  47   {
  48     SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
  49     Trace("sat-proof") << satLit << " ";
  50   }
  51 }
  52
  53 Node SatProofManager::getClauseNode(const Minisat::Clause& clause)
  54 {
  55   std::vector<Node> clauseNodes;
  56   for (size_t i = 0, size = clause.size(); i < size; ++i)
  57   {
  58     SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
  59     clauseNodes.push_back(d_cnfStream->getNode(satLit));
  60   }
  61   // order children by node id
  62   std::sort(clauseNodes.begin(), clauseNodes.end());
  63   return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes);
  64 }
  65
  66 void SatProofManager::startResChain(const Minisat::Clause& start)
  67 {
  68   if (TraceIsOn("sat-proof"))
  69   {
  70     Trace("sat-proof") << "SatProofManager::startResChain: ";
  71     printClause(start);
  72     Trace("sat-proof") << "\n";
  73   }
  74   d_resLinks.emplace_back(getClauseNode(start), Node::null(), true);
  75 }
  76
  77 void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant)
  78 {
  79   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
  80   Node litNode = d_cnfStream->getNodeCache()[satLit];
  81   bool negated = satLit.isNegated();
  82   Assert(!negated || litNode.getKind() == kind::NOT);
  83   if (!redundant)
  84   {
  85     Trace("sat-proof") << "SatProofManager::addResolutionStep: {"
  86                        << satLit.isNegated() << "} [" << satLit << "] "
  87                        << ~satLit << "\n";
  88     // if lit is negated then the chain resolution construction will use it as a
  89     // pivot occurring as is in the second clause and the node under the
  90     // negation in the first clause
  91     d_resLinks.emplace_back(d_cnfStream->getNodeCache()[~satLit],
  92                             negated ? litNode[0] : litNode,
  93                             !satLit.isNegated());
  94   }
  95   else
  96   {
  97     Trace("sat-proof") << "SatProofManager::addResolutionStep: redundant lit "
  98                        << satLit << " stored\n";
  99     d_redundantLits.push_back(satLit);
 100   }
 101 }
 102
 103 void SatProofManager::addResolutionStep(const Minisat::Clause& clause,
 104                                         Minisat::Lit lit)
 105 {
 106   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
 107   Node litNode = d_cnfStream->getNodeCache()[satLit];
 108   bool negated = satLit.isNegated();
 109   Assert(!negated || litNode.getKind() == kind::NOT);
 110   Node clauseNode = getClauseNode(clause);
 111   // if lit is negative then the chain resolution construction will use it as a
 112   // pivot occurring as is in the second clause and the node under the
 113   // negation in the first clause, which means that the third argument of the
 114   // tuple must be false
 115   d_resLinks.emplace_back(clauseNode, negated ? litNode[0] : litNode, negated);
 116   if (TraceIsOn("sat-proof"))
 117   {
 118     Trace("sat-proof") << "SatProofManager::addResolutionStep: {"
 119                        << satLit.isNegated() << "} [" << ~satLit << "] ";
 120     printClause(clause);
 121     Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t"
 122                        << clauseNode << " - lvl " << clause.level() + 1 << "\n";
 123   }
 124 }
 125
 126 void SatProofManager::endResChain(Minisat::Lit lit)
 127 {
 128   SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
 129   Trace("sat-proof") << "SatProofManager::endResChain: curr user level: "
 130                      << userContext()->getLevel() << "\n";
 131   Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
 132                      << satLit;
 133   endResChain(d_cnfStream->getNode(satLit), {satLit});
 134 }
 135
 136 void SatProofManager::endResChain(const Minisat::Clause& clause)
 137 {
 138   if (TraceIsOn("sat-proof"))
 139   {
 140     Trace("sat-proof") << "SatProofManager::endResChain: curr user level: "
 141                        << userContext()->getLevel() << "\n";
 142     Trace("sat-proof") << "SatProofManager::endResChain: chain_res for ";
 143     printClause(clause);
 144   }
 145   std::set<SatLiteral> clauseLits;
 146   for (unsigned i = 0, size = clause.size(); i < size; ++i)
 147   {
 148     clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i]));
 149   }
 150   Node conclusion = getClauseNode(clause);
 151   int clauseLevel = clause.level() + 1;
 152   if (clauseLevel < userContext()->getLevel())
 153   {
 154     Assert(!d_optResLevels.count(conclusion));
 155     d_optResLevels[conclusion] = clauseLevel;
 156     Trace("sat-proof") << "SatProofManager::endResChain: ..clause's lvl "
 157                        << clause.level() + 1 << " below curr user level "
 158                        << userContext()->getLevel() << "\n";
 159   }
 160   endResChain(conclusion, clauseLits);
 161 }
 162
 163 void SatProofManager::endResChain(Node conclusion,
 164                                   const std::set<SatLiteral>& conclusionLits)
 165 {
 166   Trace("sat-proof") << ", " << conclusion << "\n";
 167   if (d_resChains.hasGenerator(conclusion))
 168   {
 169     Trace("sat-proof")
 170         << "SatProofManager::endResChain: skip repeated proof of " << conclusion
 171         << "\n";
 172     // clearing
 173     d_resLinks.clear();
 174     d_redundantLits.clear();
 175     return;
 176   }
 177   // first process redundant literals
 178   std::set<SatLiteral> visited;
 179   unsigned pos = d_resLinks.size();
 180   for (SatLiteral satLit : d_redundantLits)
 181   {
 182     processRedundantLit(satLit, conclusionLits, visited, pos);
 183   }
 184   d_redundantLits.clear();
 185   // build resolution chain
 186   // the conclusion is stored already in the arguments because of the
 187   // possibility of reordering
 188   std::vector<Node> children, args{conclusion};
 189   for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i)
 190   {
 191     Node clause, pivot;
 192     bool posFirst;
 193     std::tie(clause, pivot, posFirst) = d_resLinks[i];
 194     children.push_back(clause);
 195     Trace("sat-proof") << "SatProofManager::endResChain:   ";
 196     if (i > 0)
 197     {
 198       Trace("sat-proof") << "{" << posFirst << "} ["
 199                          << d_cnfStream->getTranslationCache()[pivot] << "] ";
 200     }
 201     // special case for clause (or l1 ... ln) being a single literal
 202     // corresponding itself to a clause, which is indicated by the pivot being
 203     // of the form (not (or l1 ... ln))
 204     if (clause.getKind() == kind::OR
 205         && !(pivot.getKind() == kind::NOT && pivot[0].getKind() == kind::OR
 206              && pivot[0] == clause))
 207     {
 208       for (unsigned j = 0, sizeJ = clause.getNumChildren(); j < sizeJ; ++j)
 209       {
 210         Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause[j]];
 211         if (j < sizeJ - 1)
 212         {
 213           Trace("sat-proof") << ", ";
 214         }
 215       }
 216     }
 217     else
 218     {
 219       Assert(d_cnfStream->getTranslationCache().find(clause)
 220              != d_cnfStream->getTranslationCache().end())
 221           << "clause node " << clause
 222           << " treated as unit has no literal. Pivot is " << pivot << "\n";
 223       Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause];
 224     }
 225     Trace("sat-proof") << " : ";
 226     if (i > 0)
 227     {
 228       args.push_back(posFirst ? d_true : d_false);
 229       args.push_back(pivot);
 230       Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] ";
 231     }
 232     Trace("sat-proof") << clause << "\n";
 233   }
 234   // clearing
 235   d_resLinks.clear();
 236   // whether no-op
 237   if (children.size() == 1)
 238   {
 239     Trace("sat-proof") << "SatProofManager::endResChain: no-op. The conclusion "
 240                        << conclusion << " is set-equal to premise "
 241                        << children[0] << "\n";
 242     return;
 243   }
 244   // whether trivial cycle
 245   for (const Node& child : children)
 246   {
 247     if (conclusion == child)
 248     {
 249       Trace("sat-proof")
 250           << "SatProofManager::endResChain: no-op. The conclusion "
 251           << conclusion << " is equal to a premise\n";
 252       return;
 253     }
 254   }
 255   // since the conclusion can be both reordered and without duplicates and the
 256   // SAT solver does not record this information, we use a MACRO_RESOLUTION
 257   // step, which bypasses these. Note that we could generate a chain resolution
 258   // rule here by explicitly computing the detailed steps, but leave this for
 259   // post-processing.
 260   ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
 261   // note that we must tell the proof generator to overwrite if repeated
 262   d_resChainPg.addStep(conclusion, ps);
 263   // the premises of this resolution may not have been justified yet, so we do
 264   // not pass assumptions to check closedness
 265   d_resChains.addLazyStep(conclusion, &d_resChainPg);
 266 }
 267
 268 void SatProofManager::processRedundantLit(
 269     SatLiteral lit,
 270     const std::set<SatLiteral>& conclusionLits,
 271     std::set<SatLiteral>& visited,
 272     unsigned pos)
 273 {
 274   Trace("sat-proof") << push
 275                      << "SatProofManager::processRedundantLit: Lit: " << lit
 276                      << "\n";
 277   if (visited.count(lit))
 278   {
 279     Trace("sat-proof") << "already visited\n" << pop;
 280     return;
 281   }
 282   Minisat::Solver::TCRef reasonRef =
 283       d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
 284   if (reasonRef == Minisat::Solver::TCRef_Undef)
 285   {
 286     Trace("sat-proof") << "unit, add link to lit " << lit << " at pos: " << pos
 287                        << "\n"
 288                        << pop;
 289     visited.insert(lit);
 290     Node litNode = d_cnfStream->getNodeCache()[lit];
 291     bool negated = lit.isNegated();
 292     Assert(!negated || litNode.getKind() == kind::NOT);
 293
 294     d_resLinks.emplace(d_resLinks.begin() + pos,
 295                        d_cnfStream->getNodeCache()[~lit],
 296                        negated ? litNode[0] : litNode,
 297                        !negated);
 298     return;
 299   }
 300   Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size())
 301       << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
 302       << d_solver->ca.size() << "\n";
 303   const Minisat::Clause& reason = d_solver->ca[reasonRef];
 304   if (TraceIsOn("sat-proof"))
 305   {
 306     Trace("sat-proof") << "reason: ";
 307     printClause(reason);
 308     Trace("sat-proof") << "\n";
 309   }
 310   // Since processRedundantLit calls can reallocate memory in the SAT solver due
 311   // to explaining stuff, we directly get the literals and the clause node here
 312   std::vector<SatLiteral> toProcess;
 313   for (unsigned i = 1, size = reason.size(); i < size; ++i)
 314   {
 315     toProcess.push_back(MinisatSatSolver::toSatLiteral(reason[i]));
 316   }
 317   Node clauseNode = getClauseNode(reason);
 318     // check if redundant literals in the reason. The first literal is the one we
 319   // will be eliminating, so we check the others
 320   for (unsigned i = 0, size = toProcess.size(); i < size; ++i)
 321   {
 322     SatLiteral satLit = toProcess[i];
 323     // if literal does not occur in the conclusion we process it as well
 324     if (!conclusionLits.count(satLit))
 325     {
 326       processRedundantLit(satLit, conclusionLits, visited, pos);
 327     }
 328   }
 329   Assert(!visited.count(lit));
 330   visited.insert(lit);
 331   Trace("sat-proof") << "clause, add link to lit " << lit << " at pos: " << pos
 332                      << "\n"
 333                      << pop;
 334   // add the step before steps for children. Note that the step is with the
 335   // reason, not only with ~lit, since the learned clause is built under the
 336   // assumption that the redundant literal is removed via the resolution with
 337   // the explanation of its negation
 338   Node litNode = d_cnfStream->getNodeCache()[lit];
 339   bool negated = lit.isNegated();
 340   Assert(!negated || litNode.getKind() == kind::NOT);
 341   d_resLinks.emplace(d_resLinks.begin() + pos,
 342                      clauseNode,
 343                      negated ? litNode[0] : litNode,
 344                      !negated);
 345 }
 346
 347 void SatProofManager::explainLit(SatLiteral lit,
 348                                  std::unordered_set<TNode>& premises)
 349 {
 350   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
 351   Node litNode = d_cnfStream->getNode(lit);
 352   Trace("sat-proof") << " [" << litNode << "]\n";
 353   // We don't need to explain nodes who are inputs. Note that it's *necessary*
 354   // to avoid attempting such explanations because they can introduce cycles at
 355   // the node level. For example, if a literal l depends on an input clause C
 356   // but a literal l', node-equivalent to C, depends on l, we may have a cycle
 357   // when building the overall SAT proof.
 358   if (d_assumptions.contains(litNode))
 359   {
 360     Trace("sat-proof")
 361         << "SatProofManager::explainLit: input assumption, ABORT\n"
 362         << pop;
 363     return;
 364   }
 365   // We don't need to explain nodes who already have proofs.
 366   //
 367   // Note that if we had two literals for (= a b) and (= b a) and we had already
 368   // a proof for (= a b) this test would return true for (= b a), which could
 369   // lead to open proof. However we should never have two literals like this in
 370   // the SAT solver since they'd be rewritten to the same one
 371   if (d_resChainPg.hasProofFor(litNode))
 372   {
 373     Trace("sat-proof") << "SatProofManager::explainLit: already justified "
 374                        << lit << ", ABORT\n"
 375                        << pop;
 376     return;
 377   }
 378   Minisat::Solver::TCRef reasonRef =
 379       d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
 380   if (reasonRef == Minisat::Solver::TCRef_Undef)
 381   {
 382     Trace("sat-proof") << "SatProofManager::explainLit: no SAT reason\n" << pop;
 383     return;
 384   }
 385   Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size())
 386       << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
 387       << d_solver->ca.size() << "\n";
 388   const Minisat::Clause& reason = d_solver->ca[reasonRef];
 389   unsigned size = reason.size();
 390   if (TraceIsOn("sat-proof"))
 391   {
 392     Trace("sat-proof") << "SatProofManager::explainLit: with clause: ";
 393     printClause(reason);
 394     Trace("sat-proof") << "\n";
 395   }
 396 #ifdef CVC5_ASSERTIONS
 397   // pedantically check that the negation of the literal to explain *does not*
 398   // occur in the reason, otherwise we will loop forever
 399   for (unsigned i = 0; i < size; ++i)
 400   {
 401     AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit)
 402         << "cyclic justification\n";
 403   }
 404 #endif
 405   // add the reason clause first
 406   std::vector<Node> children{getClauseNode(reason)}, args;
 407   // save in the premises
 408   premises.insert(children.back());
 409   // Since explainLit calls can reallocate memory in the
 410   // SAT solver, we directly get the literals we need to explain so we no
 411   // longer depend on the reference to reason
 412   std::vector<Node> toExplain{children.back().begin(), children.back().end()};
 413   Trace("sat-proof") << push;
 414   for (unsigned i = 0; i < size; ++i)
 415   {
 416 #ifdef CVC5_ASSERTIONS
 417     // pedantically make sure that the reason stays the same
 418     const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef];
 419     AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size()));
 420     AlwaysAssert(children[0] == getClauseNode(reloadedReason));
 421 #endif
 422     SatLiteral currLit = d_cnfStream->getTranslationCache()[toExplain[i]];
 423     // ignore the lit we are trying to explain...
 424     if (currLit == lit)
 425     {
 426       continue;
 427     }
 428     std::unordered_set<TNode> childPremises;
 429     explainLit(~currLit, childPremises);
 430     // save to resolution chain premises / arguments
 431     Assert(d_cnfStream->getNodeCache().find(currLit)
 432            != d_cnfStream->getNodeCache().end());
 433     children.push_back(d_cnfStream->getNodeCache()[~currLit]);
 434     Node currLitNode = d_cnfStream->getNodeCache()[currLit];
 435     bool negated = currLit.isNegated();
 436     Assert(!negated || currLitNode.getKind() == kind::NOT);
 437     // note this is the opposite of what is done in addResolutionStep. This is
 438     // because here the clause, which contains the literal being analyzed, is
 439     // the first clause rather than the second
 440     args.push_back(!negated ? d_true : d_false);
 441     args.push_back(negated ? currLitNode[0] : currLitNode);
 442     // add child premises and the child itself
 443     premises.insert(childPremises.begin(), childPremises.end());
 444     premises.insert(d_cnfStream->getNodeCache()[~currLit]);
 445   }
 446   if (TraceIsOn("sat-proof"))
 447   {
 448     Trace("sat-proof") << pop << "SatProofManager::explainLit: chain_res for "
 449                        << lit << ", " << litNode << " with clauses:\n";
 450     for (unsigned i = 0, csize = children.size(); i < csize; ++i)
 451     {
 452       Trace("sat-proof") << "SatProofManager::explainLit:   " << children[i];
 453       if (i > 0)
 454       {
 455         Trace("sat-proof") << " [" << args[(2 * i) - 2] << ", "
 456                            << args[(2 * i) - 1] << "]";
 457       }
 458       Trace("sat-proof") << "\n";
 459     }
 460   }
 461   // if justification of children contains the expected conclusion, avoid the
 462   // cyclic proof by aborting.
 463   if (premises.count(litNode))
 464   {
 465     Trace("sat-proof") << "SatProofManager::explainLit: CYCLIC PROOF of " << lit
 466                        << " [" << litNode << "], ABORT\n"
 467                        << pop;
 468     return;
 469   }
 470   Trace("sat-proof") << pop;
 471   // create step
 472   args.insert(args.begin(), litNode);
 473   ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
 474   d_resChainPg.addStep(litNode, ps);
 475   // the premises in the limit of the justification may correspond to other
 476   // links in the chain which have, themselves, literals yet to be justified. So
 477   // we are not ready yet to check closedness w.r.t. CNF transformation of the
 478   // preprocessed assertions
 479   d_resChains.addLazyStep(litNode, &d_resChainPg);
 480 }
 481
 482 void SatProofManager::finalizeProof(Node inConflictNode,
 483                                     const std::vector<SatLiteral>& inConflict)
 484 {
 485   Trace("sat-proof")
 486       << "SatProofManager::finalizeProof: conflicting clause node: "
 487       << inConflictNode << "\n";
 488   // nothing to do
 489   if (inConflictNode == d_false)
 490   {
 491     return;
 492   }
 493   if (TraceIsOn("sat-proof-debug2"))
 494   {
 495     Trace("sat-proof-debug2")
 496         << push << "SatProofManager::finalizeProof: saved proofs in chain:\n";
 497     std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
 498     std::unordered_set<Node> skip;
 499     for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links)
 500     {
 501       if (skip.count(link.first))
 502       {
 503         continue;
 504       }
 505       auto it = d_cnfStream->getTranslationCache().find(link.first);
 506       if (it != d_cnfStream->getTranslationCache().end())
 507       {
 508         Trace("sat-proof-debug2")
 509             << "SatProofManager::finalizeProof:  " << it->second;
 510       }
 511       // a refl step added due to double elim negation, ignore
 512       else if (link.second->getRule() == PfRule::REFL)
 513       {
 514         continue;
 515       }
 516       // a clause
 517       else
 518       {
 519         Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:";
 520         Assert(link.first.getKind() == kind::OR) << link.first;
 521         for (const Node& n : link.first)
 522         {
 523           it = d_cnfStream->getTranslationCache().find(n);
 524           Assert(it != d_cnfStream->getTranslationCache().end());
 525           Trace("sat-proof-debug2") << it->second << " ";
 526         }
 527       }
 528       Trace("sat-proof-debug2") << "\n";
 529       Trace("sat-proof-debug2")
 530           << "SatProofManager::finalizeProof: " << link.first << "\n";
 531       // get resolution
 532       Node cur = link.first;
 533       std::shared_ptr<ProofNode> pfn = link.second;
 534       while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST)
 535       {
 536         Assert(pfn->getChildren().size() == 1
 537                && pfn->getChildren()[0]->getRule() == PfRule::ASSUME)
 538             << *link.second.get() << "\n"
 539             << *pfn.get();
 540         cur = pfn->getChildren()[0]->getResult();
 541         // retrieve justification of assumption in the links
 542         Assert(links.find(cur) != links.end());
 543         pfn = links[cur];
 544         // ignore it in the rest of the outside loop
 545         skip.insert(cur);
 546       }
 547       std::vector<Node> fassumps;
 548       expr::getFreeAssumptions(pfn.get(), fassumps);
 549       Trace("sat-proof-debug2") << push;
 550       for (const Node& fa : fassumps)
 551       {
 552         Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:   - ";
 553         it = d_cnfStream->getTranslationCache().find(fa);
 554         if (it != d_cnfStream->getTranslationCache().end())
 555         {
 556           Trace("sat-proof-debug2") << it->second << "\n";
 557           continue;
 558         }
 559         // then it's a clause
 560         Assert(fa.getKind() == kind::OR);
 561         for (const Node& n : fa)
 562         {
 563           it = d_cnfStream->getTranslationCache().find(n);
 564           Assert(it != d_cnfStream->getTranslationCache().end());
 565           Trace("sat-proof-debug2") << it->second << " ";
 566         }
 567         Trace("sat-proof-debug2") << "\n";
 568       }
 569       Trace("sat-proof-debug2") << pop;
 570       Trace("sat-proof-debug2")
 571           << "SatProofManager::finalizeProof:  " << *pfn.get() << "\n=======\n";
 572       ;
 573     }
 574     Trace("sat-proof-debug2") << pop;
 575   }
 576   // We will resolve away of the literals l_1...l_n in inConflict. At this point
 577   // each ~l_i must be either explainable, the result of a previously saved
 578   // resolution chain, or an input. In account of it possibly being the first,
 579   // we call explainLit on each ~l_i while accumulating the children and
 580   // arguments for the resolution step to conclude false.
 581   std::vector<Node> children{inConflictNode}, args;
 582   std::unordered_set<TNode> premises;
 583   for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
 584   {
 585     Assert(d_cnfStream->getNodeCache().find(inConflict[i])
 586            != d_cnfStream->getNodeCache().end());
 587     std::unordered_set<TNode> childPremises;
 588     explainLit(~inConflict[i], childPremises);
 589     Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]];
 590     // save to resolution chain premises / arguments
 591     children.push_back(negatedLitNode);
 592     Node litNode = d_cnfStream->getNodeCache()[inConflict[i]];
 593     bool negated = inConflict[i].isNegated();
 594     Assert(!negated || litNode.getKind() == kind::NOT);
 595     // note this is the opposite of what is done in addResolutionStep. This is
 596     // because here the clause, which contains the literal being analyzed, is
 597     // the first clause rather than the second
 598     args.push_back(!negated ? d_true : d_false);
 599     args.push_back(negated ? litNode[0] : litNode);
 600     // add child premises and the child itself
 601     premises.insert(childPremises.begin(), childPremises.end());
 602     premises.insert(negatedLitNode);
 603     Trace("sat-proof") << "===========\n";
 604   }
 605   if (TraceIsOn("sat-proof"))
 606   {
 607     Trace("sat-proof") << "SatProofManager::finalizeProof: chain_res for false "
 608                           "with clauses:\n";
 609     for (unsigned i = 0, size = children.size(); i < size; ++i)
 610     {
 611       Trace("sat-proof") << "SatProofManager::finalizeProof:   " << children[i];
 612       if (i > 0)
 613       {
 614         Trace("sat-proof") << " [" << args[i - 1] << "]";
 615       }
 616       Trace("sat-proof") << "\n";
 617     }
 618   }
 619   // create step
 620   args.insert(args.begin(), d_false);
 621   ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
 622   d_resChainPg.addStep(d_false, ps);
 623   // not yet ready to check closedness because maybe only now we will justify
 624   // literals used in resolutions
 625   d_resChains.addLazyStep(d_false, &d_resChainPg);
 626   // Fix point justification of literals in leaves of the proof of false
 627   bool expanded;
 628   do
 629   {
 630     expanded = false;
 631     Trace("sat-proof") << "expand assumptions to prove false\n";
 632     std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
 633     Assert(pfn);
 634     Trace("sat-proof-debug") << "sat proof of flase: " << *pfn.get() << "\n";
 635     std::vector<Node> fassumps;
 636     expr::getFreeAssumptions(pfn.get(), fassumps);
 637     if (TraceIsOn("sat-proof"))
 638     {
 639       for (const Node& fa : fassumps)
 640       {
 641         auto it = d_cnfStream->getTranslationCache().find(fa);
 642         if (it != d_cnfStream->getTranslationCache().end())
 643         {
 644           Trace("sat-proof") << "- " << it->second << "\n";
 645           Trace("sat-proof") << "  - " << fa << "\n";
 646           continue;
 647         }
 648         // then it's a clause
 649         std::stringstream ss;
 650         Assert(fa.getKind() == kind::OR);
 651         for (const Node& n : fa)
 652         {
 653           it = d_cnfStream->getTranslationCache().find(n);
 654           Assert(it != d_cnfStream->getTranslationCache().end());
 655           ss << it->second << " ";
 656         }
 657         Trace("sat-proof") << "- " << ss.str() << "\n";
 658         Trace("sat-proof") << "  - " << fa << "\n";
 659       }
 660     }
 661
 662     // for each assumption, see if it has a reason
 663     for (const Node& fa : fassumps)
 664     {
 665       // ignore already processed assumptions
 666       if (premises.count(fa))
 667       {
 668         Trace("sat-proof") << "already processed assumption " << fa << "\n";
 669         continue;
 670       }
 671       // ignore input assumptions. This is necessary to avoid rare collisions
 672       // between input clauses and literals that are equivalent at the node
 673       // level. In trying to justify the literal below, if it was previously
 674       // propagated (say, in a previous check-sat call that survived the
 675       // user-context changes) but no longer holds, then we may introduce a
 676       // bogus proof for it, rather than keeping it as an input.
 677       if (d_assumptions.contains(fa))
 678       {
 679         Trace("sat-proof") << "input assumption " << fa << "\n";
 680         continue;
 681       }
 682       // ignore non-literals
 683       auto it = d_cnfStream->getTranslationCache().find(fa);
 684       if (it == d_cnfStream->getTranslationCache().end())
 685       {
 686         Trace("sat-proof") << "no lit assumption " << fa << "\n";
 687         premises.insert(fa);
 688         continue;
 689       }
 690       Trace("sat-proof") << "lit assumption (" << it->second << "), " << fa
 691                          << "\n";
 692       // mark another iteration for the loop, as some resolution link may be
 693       // connected because of the new justifications
 694       expanded = true;
 695       std::unordered_set<TNode> childPremises;
 696       explainLit(it->second, childPremises);
 697       // add the premises used in the justification. We know they will have
 698       // been as expanded as possible
 699       premises.insert(childPremises.begin(), childPremises.end());
 700       // add free assumption itself
 701       premises.insert(fa);
 702     }
 703   } while (expanded);
 704   // now we should be able to close it
 705   if (options::proofCheck() == options::ProofCheckMode::EAGER)
 706   {
 707     std::vector<Node> assumptionsVec;
 708     for (const Node& a : d_assumptions)
 709     {
 710       assumptionsVec.push_back(a);
 711     }
 712     d_resChains.addLazyStep(d_false, &d_resChainPg, assumptionsVec);
 713   }
 714 }
 715
 716 void SatProofManager::storeUnitConflict(Minisat::Lit inConflict)
 717 {
 718   Assert(d_conflictLit == undefSatVariable);
 719   d_conflictLit = MinisatSatSolver::toSatLiteral(inConflict);
 720 }
 721
 722 void SatProofManager::finalizeProof()
 723 {
 724   Assert(d_conflictLit != undefSatVariable);
 725   Trace("sat-proof")
 726       << "SatProofManager::finalizeProof: conflicting (lazy) satLit: "
 727       << d_conflictLit << "\n";
 728   finalizeProof(d_cnfStream->getNode(d_conflictLit), {d_conflictLit});
 729   // reset since if in incremental mode this may be used again
 730   d_conflictLit = undefSatVariable;
 731 }
 732
 733 void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding)
 734 {
 735   SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict);
 736   Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: "
 737                      << satLit << "\n";
 738   Node clauseNode = d_cnfStream->getNode(satLit);
 739   if (adding)
 740   {
 741     registerSatAssumptions({clauseNode});
 742   }
 743   finalizeProof(clauseNode, {satLit});
 744 }
 745
 746 void SatProofManager::finalizeProof(const Minisat::Clause& inConflict,
 747                                     bool adding)
 748 {
 749   if (TraceIsOn("sat-proof"))
 750   {
 751     Trace("sat-proof")
 752         << "SatProofManager::finalizeProof: conflicting clause: ";
 753     printClause(inConflict);
 754     Trace("sat-proof") << "\n";
 755   }
 756   std::vector<SatLiteral> clause;
 757   for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
 758   {
 759     clause.push_back(MinisatSatSolver::toSatLiteral(inConflict[i]));
 760   }
 761   Node clauseNode = getClauseNode(inConflict);
 762   if (adding)
 763   {
 764     registerSatAssumptions({clauseNode});
 765   }
 766   finalizeProof(clauseNode, clause);
 767 }
 768
 769 std::shared_ptr<ProofNode> SatProofManager::getProof()
 770 {
 771   std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
 772   if (!pfn)
 773   {
 774     pfn = d_env.getProofNodeManager()->mkAssume(d_false);
 775   }
 776   return pfn;
 777 }
 778
 779 void SatProofManager::registerSatLitAssumption(Minisat::Lit lit)
 780 {
 781   Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - "
 782                      << d_cnfStream->getNode(
 783                             MinisatSatSolver::toSatLiteral(lit))
 784                      << "\n";
 785   d_assumptions.insert(
 786       d_cnfStream->getNode(MinisatSatSolver::toSatLiteral(lit)));
 787 }
 788
 789 void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
 790 {
 791   for (const Node& a : assumps)
 792   {
 793     Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a
 794                        << "\n";
 795     d_assumptions.insert(a);
 796   }
 797 }
 798
 799 void SatProofManager::notifyPop()
 800 {
 801   for (context::CDHashMap<Node, int>::const_iterator it =
 802            d_optResLevels.begin();
 803        it != d_optResLevels.end();
 804        ++it)
 805   {
 806     // Save into map the proof of the resolution chain. We copy to prevent the
 807     // proof node saved to be restored to suffering unintended updates. This is
 808     // *necessary*.
 809     std::shared_ptr<ProofNode> clauseResPf =
 810         d_env.getProofNodeManager()->clone(d_resChains.getProofFor(it->first));
 811     Assert(clauseResPf && clauseResPf->getRule() != PfRule::ASSUME);
 812     d_optResProofs[it->second].push_back(clauseResPf);
 813   }
 814 }
 815
 816 }  // namespace prop
 817 }  // namespace cvc5