src/proof/resolution_bitvector_proof.cpp

   1 /*********************                                                        */
   2 /*! \file resolution_bitvector_proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, Paul Meng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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  ** [[ Add lengthier description here ]]
  13
  14  ** \todo document this file
  15
  16 **/
  17
  18 #include "proof/resolution_bitvector_proof.h"
  19 #include "options/bv_options.h"
  20 #include "options/proof_options.h"
  21 #include "proof/array_proof.h"
  22 #include "proof/bitvector_proof.h"
  23 #include "proof/clause_id.h"
  24 #include "proof/lfsc_proof_printer.h"
  25 #include "proof/proof_output_channel.h"
  26 #include "proof/proof_utils.h"
  27 #include "proof/sat_proof_implementation.h"
  28 #include "prop/bvminisat/bvminisat.h"
  29 #include "theory/bv/bitblast/bitblaster.h"
  30 #include "theory/bv/theory_bv.h"
  31 #include "theory/bv/theory_bv_rewrite_rules.h"
  32
  33 #include <iostream>
  34 #include <sstream>
  35
  36 using namespace CVC4::theory;
  37 using namespace CVC4::theory::bv;
  38
  39 namespace CVC4 {
  40
  41 namespace proof {
  42
  43 ResolutionBitVectorProof::ResolutionBitVectorProof(
  44     theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
  45     : BitVectorProof(bv, proofEngine),
  46       d_resolutionProof(),
  47       d_isAssumptionConflict(false)
  48 {
  49 }
  50
  51 void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver)
  52 {
  53   Assert(d_resolutionProof == NULL);
  54   d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true));
  55 }
  56
  57 theory::TheoryId ResolutionBitVectorProof::getTheoryId()
  58 {
  59   return theory::THEORY_BV;
  60 }
  61
  62 void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
  63                                             context::Context* cnf)
  64 {
  65   Assert(d_resolutionProof != NULL);
  66   BitVectorProof::initCnfProof(cnfStream, cnf);
  67
  68   // true and false have to be setup in a special way
  69   Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
  70   Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
  71
  72   d_cnfProof->pushCurrentAssertion(true_node);
  73   d_cnfProof->pushCurrentDefinition(true_node);
  74   d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit());
  75   d_cnfProof->popCurrentAssertion();
  76   d_cnfProof->popCurrentDefinition();
  77
  78   d_cnfProof->pushCurrentAssertion(false_node);
  79   d_cnfProof->pushCurrentDefinition(false_node);
  80   d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit());
  81   d_cnfProof->popCurrentAssertion();
  82   d_cnfProof->popCurrentDefinition();
  83 }
  84
  85 BVSatProof* ResolutionBitVectorProof::getSatProof()
  86 {
  87   Assert(d_resolutionProof != NULL);
  88   return d_resolutionProof.get();
  89 }
  90
  91 void ResolutionBitVectorProof::startBVConflict(
  92     CVC4::BVMinisat::Solver::TCRef cr)
  93 {
  94   d_resolutionProof->startResChain(cr);
  95 }
  96
  97 void ResolutionBitVectorProof::startBVConflict(
  98     CVC4::BVMinisat::Solver::TLit lit)
  99 {
 100   d_resolutionProof->startResChain(lit);
 101 }
 102
 103 void ResolutionBitVectorProof::endBVConflict(
 104     const CVC4::BVMinisat::Solver::TLitVec& confl)
 105 {
 106   Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict called"
 107                   << std::endl;
 108
 109   std::vector<Expr> expr_confl;
 110   for (int i = 0; i < confl.size(); ++i)
 111   {
 112     prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]);
 113     Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
 114     Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
 115     expr_confl.push_back(expr_lit);
 116   }
 117
 118   Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl);
 119   Debug("pf::bv") << "Make conflict for " << conflict << std::endl;
 120
 121   if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end())
 122   {
 123     Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl;
 124     // This can only happen when we have eager explanations in the bv solver
 125     // if we don't get to propagate p before ~p is already asserted
 126     d_resolutionProof->cancelResChain();
 127     return;
 128   }
 129
 130   // we don't need to check for uniqueness in the sat solver then
 131   ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl);
 132   d_bbConflictMap[conflict] = clause_id;
 133   d_resolutionProof->endResChain(clause_id);
 134   Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict id" << clause_id
 135                   << " => " << conflict << "\n";
 136   d_isAssumptionConflict = false;
 137 }
 138
 139 void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts)
 140 {
 141   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
 142   {
 143     Debug("pf::bv") << "Construct full proof." << std::endl;
 144     d_resolutionProof->constructProof();
 145     return;
 146   }
 147
 148   for (unsigned i = 0; i < conflicts.size(); ++i)
 149   {
 150     Expr confl = conflicts[i];
 151     Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl;
 152
 153     // Special case: if the conflict has a (true) or a (not false) in it, it is
 154     // trivial...
 155     bool ignoreConflict = false;
 156     if ((confl.isConst() && confl.getConst<bool>())
 157         || (confl.getKind() == kind::NOT && confl[0].isConst()
 158             && !confl[0].getConst<bool>()))
 159     {
 160       ignoreConflict = true;
 161     }
 162     else if (confl.getKind() == kind::OR)
 163     {
 164       for (unsigned k = 0; k < confl.getNumChildren(); ++k)
 165       {
 166         if ((confl[k].isConst() && confl[k].getConst<bool>())
 167             || (confl[k].getKind() == kind::NOT && confl[k][0].isConst()
 168                 && !confl[k][0].getConst<bool>()))
 169         {
 170           ignoreConflict = true;
 171         }
 172       }
 173     }
 174     if (ignoreConflict)
 175     {
 176       Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)"
 177                       << std::endl;
 178       continue;
 179     }
 180
 181     if (d_bbConflictMap.find(confl) != d_bbConflictMap.end())
 182     {
 183       ClauseId id = d_bbConflictMap[confl];
 184       d_resolutionProof->collectClauses(id);
 185     }
 186     else
 187     {
 188       // There is no exact match for our conflict, but maybe it is a subset of
 189       // another conflict
 190       ExprToClauseId::const_iterator it;
 191       bool matchFound = false;
 192       for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
 193       {
 194         Expr possibleMatch = it->first;
 195         if (possibleMatch.getKind() != kind::OR)
 196         {
 197           // This is a single-node conflict. If this node is in the conflict
 198           // we're trying to prove, we have a match.
 199           for (unsigned k = 0; k < confl.getNumChildren(); ++k)
 200           {
 201             if (confl[k] == possibleMatch)
 202             {
 203               matchFound = true;
 204               d_resolutionProof->collectClauses(it->second);
 205               break;
 206             }
 207           }
 208         }
 209         else
 210         {
 211           if (possibleMatch.getNumChildren() > confl.getNumChildren()) continue;
 212
 213           unsigned k = 0;
 214           bool matching = true;
 215           for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j)
 216           {
 217             // j is the index in possibleMatch
 218             // k is the index in confl
 219             while (k < confl.getNumChildren() && confl[k] != possibleMatch[j])
 220             {
 221               ++k;
 222             }
 223             if (k == confl.getNumChildren())
 224             {
 225               // We couldn't find a match for possibleMatch[j], so not a match
 226               matching = false;
 227               break;
 228             }
 229           }
 230
 231           if (matching)
 232           {
 233             Debug("pf::bv")
 234                 << "Collecting info from a sub-conflict" << std::endl;
 235             d_resolutionProof->collectClauses(it->second);
 236             matchFound = true;
 237             break;
 238           }
 239         }
 240       }
 241
 242       if (!matchFound)
 243       {
 244         Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl
 245                         << "Dumping existing conflicts:" << std::endl;
 246
 247         i = 0;
 248         for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
 249         {
 250           ++i;
 251           Debug("pf::bv") << "\tConflict #" << i << ": " << it->first
 252                           << std::endl;
 253         }
 254
 255         Unreachable();
 256       }
 257     }
 258   }
 259 }
 260
 261 void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
 262                                                std::ostream& os,
 263                                                std::ostream& paren,
 264                                                const ProofLetMap& map)
 265 {
 266   Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called"
 267                   << std::endl;
 268   Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
 269   Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
 270
 271   if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end())
 272   {
 273     std::ostringstream lemma_paren;
 274     for (unsigned i = 0; i < lemma.size(); ++i)
 275     {
 276       Expr lit = lemma[i];
 277
 278       if (lit.getKind() == kind::NOT)
 279       {
 280         os << "(intro_assump_t _ _ _ ";
 281       }
 282       else
 283       {
 284         os << "(intro_assump_f _ _ _ ";
 285       }
 286       lemma_paren << ")";
 287       // print corresponding literal in main sat solver
 288       ProofManager* pm = ProofManager::currentPM();
 289       CnfProof* cnf = pm->getCnfProof();
 290       prop::SatLiteral main_lit = cnf->getLiteral(lit);
 291       os << pm->getLitName(main_lit);
 292       os << " ";
 293       // print corresponding literal in bv sat solver
 294       prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
 295       os << pm->getAtomName(bb_var, "bb");
 296       os << "(\\ unit" << bb_var << "\n";
 297       lemma_paren << ")";
 298     }
 299     Expr lem = utils::mkOr(lemma);
 300     Assert(d_bbConflictMap.find(lem) != d_bbConflictMap.end());
 301     ClauseId lemma_id = d_bbConflictMap[lem];
 302     proof::LFSCProofPrinter::printAssumptionsResolution(
 303         d_resolutionProof.get(), lemma_id, os, lemma_paren);
 304     os << lemma_paren.str();
 305   }
 306   else
 307   {
 308     Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching "
 309                        "sub-conflict..."
 310                     << std::endl;
 311
 312     bool matching;
 313
 314     ExprToClauseId::const_iterator it;
 315     unsigned i = 0;
 316     for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
 317     {
 318       // Our conflict is sorted, and the records are also sorted.
 319       ++i;
 320       Expr possibleMatch = it->first;
 321
 322       if (possibleMatch.getKind() != kind::OR)
 323       {
 324         // This is a single-node conflict. If this node is in the conflict we're
 325         // trying to prove, we have a match.
 326         matching = false;
 327
 328         for (unsigned k = 0; k < conflict.getNumChildren(); ++k)
 329         {
 330           if (conflict[k] == possibleMatch)
 331           {
 332             matching = true;
 333             break;
 334           }
 335         }
 336       }
 337       else
 338       {
 339         if (possibleMatch.getNumChildren() > conflict.getNumChildren())
 340           continue;
 341
 342         unsigned k = 0;
 343
 344         matching = true;
 345         for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j)
 346         {
 347           // j is the index in possibleMatch
 348           // k is the index in conflict
 349           while (k < conflict.getNumChildren()
 350                  && conflict[k] != possibleMatch[j])
 351           {
 352             ++k;
 353           }
 354           if (k == conflict.getNumChildren())
 355           {
 356             // We couldn't find a match for possibleMatch[j], so not a match
 357             matching = false;
 358             break;
 359           }
 360         }
 361       }
 362
 363       if (matching)
 364       {
 365         Debug("pf::bv") << "Found a match with conflict #" << i << ": "
 366                         << std::endl
 367                         << possibleMatch << std::endl;
 368         // The rest is just a copy of the usual handling, if a precise match is
 369         // found. We only use the literals that appear in the matching conflict,
 370         // though, and not in the original lemma - as these may not have even
 371         // been bit blasted!
 372         std::ostringstream lemma_paren;
 373
 374         if (possibleMatch.getKind() == kind::OR)
 375         {
 376           for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i)
 377           {
 378             Expr lit = possibleMatch[i];
 379
 380             if (lit.getKind() == kind::NOT)
 381             {
 382               os << "(intro_assump_t _ _ _ ";
 383             }
 384             else
 385             {
 386               os << "(intro_assump_f _ _ _ ";
 387             }
 388             lemma_paren << ")";
 389             // print corresponding literal in main sat solver
 390             ProofManager* pm = ProofManager::currentPM();
 391             CnfProof* cnf = pm->getCnfProof();
 392             prop::SatLiteral main_lit = cnf->getLiteral(lit);
 393             os << pm->getLitName(main_lit);
 394             os << " ";
 395             // print corresponding literal in bv sat solver
 396             prop::SatVariable bb_var =
 397                 d_cnfProof->getLiteral(lit).getSatVariable();
 398             os << pm->getAtomName(bb_var, "bb");
 399             os << "(\\ unit" << bb_var << "\n";
 400             lemma_paren << ")";
 401           }
 402         }
 403         else
 404         {
 405           // The conflict only consists of one node, either positive or
 406           // negative.
 407           Expr lit = possibleMatch;
 408           if (lit.getKind() == kind::NOT)
 409           {
 410             os << "(intro_assump_t _ _ _ ";
 411           }
 412           else
 413           {
 414             os << "(intro_assump_f _ _ _ ";
 415           }
 416           lemma_paren << ")";
 417           // print corresponding literal in main sat solver
 418           ProofManager* pm = ProofManager::currentPM();
 419           CnfProof* cnf = pm->getCnfProof();
 420           prop::SatLiteral main_lit = cnf->getLiteral(lit);
 421           os << pm->getLitName(main_lit);
 422           os << " ";
 423           // print corresponding literal in bv sat solver
 424           prop::SatVariable bb_var =
 425               d_cnfProof->getLiteral(lit).getSatVariable();
 426           os << pm->getAtomName(bb_var, "bb");
 427           os << "(\\ unit" << bb_var << "\n";
 428           lemma_paren << ")";
 429         }
 430
 431         ClauseId lemma_id = it->second;
 432         proof::LFSCProofPrinter::printAssumptionsResolution(
 433             d_resolutionProof.get(), lemma_id, os, lemma_paren);
 434         os << lemma_paren.str();
 435
 436         return;
 437       }
 438     }
 439
 440     // We failed to find a matching sub conflict. The last hope is that the
 441     // conflict has a FALSE assertion in it; this can happen in some corner
 442     // cases, where the FALSE is the result of a rewrite.
 443
 444     for (unsigned i = 0; i < lemma.size(); ++i)
 445     {
 446       if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse())
 447       {
 448         Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl;
 449         os << "(clausify_false ";
 450         os << ProofManager::getLitName(lemma[i]);
 451         os << ")";
 452         return;
 453       }
 454     }
 455
 456     Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl
 457                     << "Dumping existing conflicts:" << std::endl;
 458
 459     i = 0;
 460     for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it)
 461     {
 462       ++i;
 463       Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
 464     }
 465
 466     Unreachable();
 467   }
 468 }
 469
 470 void LFSCBitVectorProof::calculateAtomsInBitblastingProof()
 471 {
 472   // Collect the input clauses used
 473   IdToSatClause used_lemmas;
 474   IdToSatClause used_inputs;
 475   d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
 476   d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof);
 477   Assert(used_lemmas.empty());
 478 }
 479
 480 void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
 481                                               std::ostream& paren,
 482                                               ProofLetMap& letMap)
 483 {
 484   // print mapping between theory atoms and internal SAT variables
 485   os << std::endl << ";; BB atom mapping\n" << std::endl;
 486
 487   std::set<Node>::iterator atomIt;
 488   Debug("pf::bv") << std::endl
 489                   << "BV Dumping atoms from inputs: " << std::endl
 490                   << std::endl;
 491   for (atomIt = d_atomsInBitblastingProof.begin();
 492        atomIt != d_atomsInBitblastingProof.end();
 493        ++atomIt)
 494   {
 495     Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
 496   }
 497   Debug("pf::bv") << std::endl;
 498
 499   // first print bit-blasting
 500   printBitblasting(os, paren);
 501
 502   // print CNF conversion proof for bit-blasted facts
 503   IdToSatClause used_lemmas;
 504   IdToSatClause used_inputs;
 505   d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
 506
 507   d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
 508   os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
 509   for (IdToSatClause::iterator it = used_inputs.begin();
 510        it != used_inputs.end();
 511        ++it)
 512   {
 513     d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren);
 514   }
 515
 516   os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
 517   proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren);
 518 }
 519
 520 } /* namespace proof */
 521
 522 } /* namespace CVC4 */