src/proof/bitvector_proof.cpp

   1 /*********************                                                        */
   2 /*! \file bitvector_proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, Alex Ozdemir
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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  ** Contains implementions (e.g. code for printing bitblasting bindings that is
  13  ** common to all kinds of bitvector proofs.
  14  **/
  15
  16 #include "proof/bitvector_proof.h"
  17 #include "options/bv_options.h"
  18 #include "options/proof_options.h"
  19 #include "proof/proof_output_channel.h"
  20 #include "proof/theory_proof.h"
  21 #include "prop/sat_solver_types.h"
  22 #include "theory/bv/bitblast/bitblaster.h"
  23 #include "theory/bv/theory_bv.h"
  24
  25 namespace CVC4 {
  26
  27 namespace proof {
  28 BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
  29                                TheoryProofEngine* proofEngine)
  30     : TheoryProof(bv, proofEngine),
  31       d_declarations(),
  32       d_seenBBTerms(),
  33       d_bbTerms(),
  34       d_bbAtoms(),
  35       d_bitblaster(nullptr),
  36       d_useConstantLetification(false),
  37       d_cnfProof()
  38 {
  39 }
  40
  41 void BitVectorProof::setBitblaster(theory::bv::TBitblaster<Node>* bb)
  42 {
  43   Assert(d_bitblaster == NULL);
  44   d_bitblaster = bb;
  45 }
  46
  47 void BitVectorProof::registerTermBB(Expr term)
  48 {
  49   Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term
  50                   << " )" << std::endl;
  51
  52   if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) return;
  53
  54   d_seenBBTerms.insert(term);
  55   d_bbTerms.push_back(term);
  56
  57   // If this term gets used in the final proof, we will want to register it.
  58   // However, we don't know this at this point; and when the theory proof engine
  59   // sees it, if it belongs to another theory, it won't register it with this
  60   // proof. So, we need to tell the engine to inform us.
  61
  62   if (theory::Theory::theoryOf(term) != theory::THEORY_BV)
  63   {
  64     Debug("pf::bv") << "\tMarking term " << term
  65                     << " for future BV registration" << std::endl;
  66     d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV);
  67   }
  68 }
  69
  70 void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
  71   Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom
  72                   << ", " << atom_bb << " )" << std::endl;
  73
  74   Expr def = atom.eqExpr(atom_bb);
  75   d_bbAtoms.insert(std::make_pair(atom, def));
  76   registerTerm(atom);
  77
  78   // Register the atom's terms for bitblasting
  79   registerTermBB(atom[0]);
  80   registerTermBB(atom[1]);
  81 }
  82
  83 void BitVectorProof::registerTerm(Expr term) {
  84   Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )"
  85                   << std::endl;
  86
  87   if (options::lfscLetification() && term.isConst()
  88       && term.getType().isBitVector())
  89   {
  90     if (d_constantLetMap.find(term) == d_constantLetMap.end()) {
  91       std::ostringstream name;
  92       name << "letBvc" << d_constantLetMap.size();
  93       d_constantLetMap[term] = name.str();
  94     }
  95   }
  96
  97   d_usedBB.insert(term);
  98
  99   if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst())
 100   {
 101     d_declarations.insert(term);
 102   }
 103
 104   Debug("pf::bv") << "Going to register children: " << std::endl;
 105   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 106     Debug("pf::bv") << "\t" << term[i] << std::endl;
 107   }
 108
 109   // don't care about parametric operators for bv?
 110   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 111      d_proofEngine->registerTerm(term[i]);
 112   }
 113 }
 114
 115 std::string BitVectorProof::getBBTermName(Expr expr)
 116 {
 117   Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt"
 118                   << expr.getId() << std::endl;
 119   std::ostringstream os;
 120   os << "bt" << expr.getId();
 121   return os.str();
 122 }
 123
 124 void BitVectorProof::printOwnedTerm(Expr term,
 125                                     std::ostream& os,
 126                                     const ProofLetMap& map)
 127 {
 128   Debug("pf::bv") << std::endl
 129                   << "(pf::bv) BitVectorProof::printOwnedTerm( " << term
 130                   << " ), theory is: " << theory::Theory::theoryOf(term)
 131                   << std::endl;
 132
 133   Assert(theory::Theory::theoryOf(term) == theory::THEORY_BV);
 134
 135   // peel off eager bit-blasting trick
 136   if (term.getKind() == kind::BITVECTOR_EAGER_ATOM) {
 137     d_proofEngine->printBoundTerm(term[0], os, map);
 138     return;
 139   }
 140
 141   switch (term.getKind()) {
 142   case kind::CONST_BITVECTOR : {
 143     printConstant(term, os);
 144     return;
 145   }
 146   case kind::BITVECTOR_AND :
 147   case kind::BITVECTOR_OR :
 148   case kind::BITVECTOR_XOR :
 149   case kind::BITVECTOR_NAND :
 150   case kind::BITVECTOR_NOR :
 151   case kind::BITVECTOR_XNOR :
 152   case kind::BITVECTOR_COMP :
 153   case kind::BITVECTOR_MULT :
 154   case kind::BITVECTOR_PLUS :
 155   case kind::BITVECTOR_SUB :
 156   case kind::BITVECTOR_UDIV :
 157   case kind::BITVECTOR_UREM :
 158   case kind::BITVECTOR_UDIV_TOTAL :
 159   case kind::BITVECTOR_UREM_TOTAL :
 160   case kind::BITVECTOR_SDIV :
 161   case kind::BITVECTOR_SREM :
 162   case kind::BITVECTOR_SMOD :
 163   case kind::BITVECTOR_SHL :
 164   case kind::BITVECTOR_LSHR :
 165   case kind::BITVECTOR_ASHR :
 166   case kind::BITVECTOR_CONCAT : {
 167     printOperatorNary(term, os, map);
 168     return;
 169   }
 170   case kind::BITVECTOR_NEG :
 171   case kind::BITVECTOR_NOT :
 172   case kind::BITVECTOR_ROTATE_LEFT :
 173   case kind::BITVECTOR_ROTATE_RIGHT : {
 174     printOperatorUnary(term, os, map);
 175     return;
 176   }
 177   case kind::EQUAL :
 178   case kind::BITVECTOR_ULT :
 179   case kind::BITVECTOR_ULE :
 180   case kind::BITVECTOR_UGT :
 181   case kind::BITVECTOR_UGE :
 182   case kind::BITVECTOR_SLT :
 183   case kind::BITVECTOR_SLE :
 184   case kind::BITVECTOR_SGT :
 185   case kind::BITVECTOR_SGE : {
 186     printPredicate(term, os, map);
 187     return;
 188   }
 189   case kind::BITVECTOR_EXTRACT :
 190   case kind::BITVECTOR_REPEAT :
 191   case kind::BITVECTOR_ZERO_EXTEND :
 192   case kind::BITVECTOR_SIGN_EXTEND : {
 193     printOperatorParametric(term, os, map);
 194     return;
 195   }
 196   case kind::BITVECTOR_BITOF : {
 197     printBitOf(term, os, map);
 198     return;
 199   }
 200
 201   case kind::VARIABLE: {
 202     os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
 203     return;
 204   }
 205
 206   case kind::SKOLEM: {
 207
 208     // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems,
 209     // like ITE terms. Is there a more elegant way?
 210
 211     if (ProofManager::getSkolemizationManager()->isSkolem(term)) {
 212       os << ProofManager::sanitize(term);
 213     } else {
 214       os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
 215     }
 216     return;
 217   }
 218
 219   default:
 220     Unreachable();
 221   }
 222 }
 223
 224 void BitVectorProof::printEmptyClauseProof(std::ostream& os,
 225                                            std::ostream& paren)
 226 {
 227   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
 228       << "the BV theory should only be proving bottom directly in the eager "
 229          "bitblasting mode";
 230 }
 231
 232 void BitVectorProof::printBitOf(Expr term,
 233                                 std::ostream& os,
 234                                 const ProofLetMap& map)
 235 {
 236   Assert(term.getKind() == kind::BITVECTOR_BITOF);
 237   unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex;
 238   Expr var = term[0];
 239
 240   Debug("pf::bv") << "BitVectorProof::printBitOf( " << term << " ), "
 241                   << "bit = " << bit << ", var = " << var << std::endl;
 242
 243   os << "(bitof ";
 244   os << d_exprToVariableName[var];
 245   os << " " << bit << ")";
 246 }
 247
 248 void BitVectorProof::printConstant(Expr term, std::ostream& os)
 249 {
 250   Assert(term.isConst());
 251   os << "(a_bv " << utils::getSize(term) << " ";
 252
 253   if (d_useConstantLetification) {
 254     os << d_constantLetMap[term] << ")";
 255   } else {
 256     std::ostringstream paren;
 257     int size = utils::getSize(term);
 258     for (int i = size - 1; i >= 0; --i) {
 259       os << "(bvc ";
 260       os << (utils::getBit(term, i) ? "b1" : "b0") <<" ";
 261       paren << ")";
 262     }
 263     os << " bvn)";
 264     os << paren.str();
 265   }
 266 }
 267
 268 void BitVectorProof::printOperatorNary(Expr term,
 269                                        std::ostream& os,
 270                                        const ProofLetMap& map)
 271 {
 272   std::string op = utils::toLFSCKindTerm(term);
 273   std::ostringstream paren;
 274   std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : "";
 275   unsigned size = term.getKind() == kind::BITVECTOR_CONCAT? utils::getSize(term) :
 276                                                             utils::getSize(term[0]); // cause of COMP
 277
 278   for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
 279     os <<"("<< op <<" " <<  size <<" " << holes;
 280   }
 281   d_proofEngine->printBoundTerm(term[0], os, map);
 282   os <<" ";
 283   for (unsigned i = 1; i < term.getNumChildren(); ++i) {
 284     d_proofEngine->printBoundTerm(term[i], os, map);
 285     os << ")";
 286   }
 287 }
 288
 289 void BitVectorProof::printOperatorUnary(Expr term,
 290                                         std::ostream& os,
 291                                         const ProofLetMap& map)
 292 {
 293   os <<"(";
 294   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
 295   os << " ";
 296   d_proofEngine->printBoundTerm(term[0], os, map);
 297   os <<")";
 298 }
 299
 300 void BitVectorProof::printPredicate(Expr term,
 301                                     std::ostream& os,
 302                                     const ProofLetMap& map)
 303 {
 304   os <<"(";
 305   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" ";
 306   os << " ";
 307   d_proofEngine->printBoundTerm(term[0], os, map);
 308   os << " ";
 309   d_proofEngine->printBoundTerm(term[1], os, map);
 310   os <<")";
 311 }
 312
 313 void BitVectorProof::printOperatorParametric(Expr term,
 314                                              std::ostream& os,
 315                                              const ProofLetMap& map)
 316 {
 317   os <<"(";
 318   os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" ";
 319   os <<" ";
 320   if (term.getKind() == kind::BITVECTOR_REPEAT) {
 321     unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
 322     os << amount <<" _ ";
 323   }
 324   if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) {
 325     unsigned amount = term.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
 326     os << amount <<" _ ";
 327   }
 328
 329   if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) {
 330     unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
 331     os << amount<<" _ ";
 332   }
 333   if (term.getKind() == kind::BITVECTOR_EXTRACT) {
 334     unsigned low = utils::getExtractLow(term);
 335     unsigned high = utils::getExtractHigh(term);
 336     os << high <<" " << low << " " << utils::getSize(term[0]);
 337   }
 338   os <<" ";
 339   Assert(term.getNumChildren() == 1);
 340   d_proofEngine->printBoundTerm(term[0], os, map);
 341   os <<")";
 342 }
 343
 344 void BitVectorProof::printOwnedSort(Type type, std::ostream& os)
 345 {
 346   Debug("pf::bv") << std::endl
 347                   << "(pf::bv) BitVectorProof::printOwnedSort( " << type << " )"
 348                   << std::endl;
 349   Assert(type.isBitVector());
 350   unsigned width = utils::getSize(type);
 351   os << "(BitVec " << width << ")";
 352 }
 353
 354 void BitVectorProof::printSortDeclarations(std::ostream& os,
 355                                            std::ostream& paren)
 356 {
 357   // Nothing to do here at this point.
 358 }
 359
 360 void BitVectorProof::printTermDeclarations(std::ostream& os,
 361                                            std::ostream& paren)
 362 {
 363   ExprSet::const_iterator it = d_declarations.begin();
 364   ExprSet::const_iterator end = d_declarations.end();
 365   for (; it != end; ++it) {
 366     if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) {
 367       d_exprToVariableName[*it] = ProofManager::sanitize(*it);
 368     } else {
 369       std::string newAlias = assignAlias(*it);
 370       d_exprToVariableName[*it] = newAlias;
 371     }
 372
 373     os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n";
 374     paren <<")";
 375   }
 376 }
 377
 378 void BitVectorProof::printDeferredDeclarations(std::ostream& os,
 379                                                std::ostream& paren)
 380 {
 381   if (options::lfscLetification()) {
 382     os << std::endl << ";; BV const letification\n" << std::endl;
 383     std::map<Expr,std::string>::const_iterator it;
 384     for (it = d_constantLetMap.begin(); it != d_constantLetMap.end(); ++it) {
 385       os << "\n(@ " << it->second << " ";
 386       std::ostringstream localParen;
 387       int size = utils::getSize(it->first);
 388       for (int i = size - 1; i >= 0; --i) {
 389         os << "(bvc ";
 390         os << (utils::getBit(it->first, i) ? "b1" : "b0") << " ";
 391         localParen << ")";
 392       }
 393       os << "bvn";
 394       os << localParen.str();
 395       paren << ")";
 396     }
 397     os << std::endl;
 398
 399     d_useConstantLetification = true;
 400   }
 401 }
 402
 403 void BitVectorProof::printAliasingDeclarations(std::ostream& os,
 404                                                std::ostream& paren,
 405                                                const ProofLetMap& globalLetMap)
 406 {
 407   // Print "trust" statements to bind complex bv variables to their associated terms
 408
 409   ExprToString::const_iterator it = d_assignedAliases.begin();
 410   ExprToString::const_iterator end = d_assignedAliases.end();
 411
 412   for (; it != end; ++it) {
 413     Debug("pf::bv") << "Printing aliasing declaration for: " << *it << std::endl;
 414     std::stringstream declaration;
 415     declaration << ".fbvd" << d_aliasToBindDeclaration.size();
 416     d_aliasToBindDeclaration[it->second] = declaration.str();
 417
 418     os << "(th_let_pf _ ";
 419
 420     os << "(trust_f ";
 421     os << "(= (BitVec " << utils::getSize(it->first) << ") ";
 422     os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") ";
 423     d_proofEngine->printBoundTerm(it->first, os, globalLetMap);
 424     os << ")) ";
 425     os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n";
 426     paren << "))";
 427   }
 428
 429   os << "\n";
 430 }
 431
 432 void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os)
 433 {
 434   // TODO: once we have the operator elimination rules remove those that we
 435   // eliminated
 436   Assert(term.getType().isBitVector());
 437   Kind kind = term.getKind();
 438
 439   if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst())
 440   {
 441     // A term is a leaf if it has no children, or if it belongs to another theory
 442     os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term];
 443     os << " _)";
 444     return;
 445   }
 446
 447   switch(kind) {
 448   case kind::CONST_BITVECTOR : {
 449     os << "(bv_bbl_const "<< utils::getSize(term) <<" _ ";
 450     std::ostringstream paren;
 451     int size = utils::getSize(term);
 452     if (d_useConstantLetification) {
 453       os << d_constantLetMap[term] << ")";
 454     } else {
 455       for (int i = size - 1; i>= 0; --i) {
 456         os << "(bvc ";
 457         os << (utils::getBit(term, i) ? "b1" : "b0") <<" ";
 458         paren << ")";
 459       }
 460       os << " bvn)";
 461       os << paren.str();
 462     }
 463     return;
 464   }
 465
 466   case kind::BITVECTOR_AND :
 467   case kind::BITVECTOR_OR :
 468   case kind::BITVECTOR_XOR :
 469   case kind::BITVECTOR_NAND :
 470   case kind::BITVECTOR_NOR :
 471   case kind::BITVECTOR_XNOR :
 472   case kind::BITVECTOR_COMP :
 473   case kind::BITVECTOR_MULT :
 474   case kind::BITVECTOR_PLUS :
 475   case kind::BITVECTOR_SUB :
 476   case kind::BITVECTOR_CONCAT : {
 477     Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
 478
 479     for (int i = term.getNumChildren() - 1; i > 0; --i) {
 480       os <<"(bv_bbl_"<< utils::toLFSCKind(kind);
 481
 482       if (kind == kind::BITVECTOR_CONCAT) {
 483         os << " " << utils::getSize(term) << " _";
 484       }
 485       os << " _ _ _ _ _ _ ";
 486     }
 487
 488     os << getBBTermName(term[0]) << " ";
 489
 490     for (unsigned i = 1; i < term.getNumChildren(); ++i) {
 491       os << getBBTermName(term[i]);
 492       os << ") ";
 493     }
 494     return;
 495   }
 496
 497   case kind::BITVECTOR_NEG :
 498   case kind::BITVECTOR_NOT :
 499   case kind::BITVECTOR_ROTATE_LEFT :
 500   case kind::BITVECTOR_ROTATE_RIGHT : {
 501     os << "(bv_bbl_"<<utils::toLFSCKind(kind);
 502     os << " _ _ _ _ ";
 503     os << getBBTermName(term[0]);
 504     os << ")";
 505     return;
 506   }
 507   case kind::BITVECTOR_EXTRACT : {
 508     os <<"(bv_bbl_"<<utils::toLFSCKind(kind);
 509
 510     os << " " << utils::getSize(term) << " ";
 511     os << utils::getExtractHigh(term) << " ";
 512     os << utils::getExtractLow(term) << " ";
 513     os << " _ _ _ _ ";
 514
 515     os << getBBTermName(term[0]);
 516     os <<")";
 517     return;
 518   }
 519   case kind::BITVECTOR_REPEAT :
 520   case kind::BITVECTOR_ZERO_EXTEND :
 521   case kind::BITVECTOR_SIGN_EXTEND : {
 522     os << "(bv_bbl_" << utils::toLFSCKind(kind) << " ";
 523     os << utils::getSize(term) << " ";
 524     if (term.getKind() == kind::BITVECTOR_REPEAT) {
 525       unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
 526       os << amount;
 527     }
 528     if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) {
 529       unsigned amount = term.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
 530       os << amount;
 531     }
 532
 533     if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) {
 534       unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
 535       os << amount;
 536     }
 537
 538     os <<" _ _ _ _ ";
 539     os << getBBTermName(term[0]);
 540     os <<")";
 541     return;
 542   }
 543   case kind::BITVECTOR_UDIV :
 544   case kind::BITVECTOR_UREM :
 545   case kind::BITVECTOR_UDIV_TOTAL :
 546   case kind::BITVECTOR_UREM_TOTAL :
 547   case kind::BITVECTOR_SDIV :
 548   case kind::BITVECTOR_SREM :
 549   case kind::BITVECTOR_SMOD :
 550   case kind::BITVECTOR_SHL :
 551   case kind::BITVECTOR_LSHR :
 552   case kind::BITVECTOR_ASHR : {
 553         // these are terms for which bit-blasting is not supported yet
 554     std::ostringstream paren;
 555     os <<"(trust_bblast_term _ ";
 556     paren <<")";
 557     d_proofEngine->printLetTerm(term, os);
 558     os <<" ";
 559     std::vector<Node> bits;
 560     d_bitblaster->bbTerm(term, bits);
 561
 562     for (int i = utils::getSize(term) - 1; i >= 0; --i) {
 563       os << "(bbltc ";
 564       d_proofEngine->printLetTerm((bits[i]).toExpr(), os);
 565       paren << ")";
 566     }
 567     os << "bbltn" << paren.str();
 568     return;
 569   }
 570
 571   default: Unreachable() << "BitVectorProof Unknown operator";
 572   }
 573 }
 574
 575 void BitVectorProof::printAtomBitblasting(Expr atom,
 576                                           std::ostream& os,
 577                                           bool swap)
 578 {
 579   Kind kind = atom.getKind();
 580   switch(kind) {
 581   case kind::BITVECTOR_ULT :
 582   case kind::BITVECTOR_ULE :
 583   case kind::BITVECTOR_UGT :
 584   case kind::BITVECTOR_UGE :
 585   case kind::BITVECTOR_SLT :
 586   case kind::BITVECTOR_SLE :
 587   case kind::BITVECTOR_SGT :
 588   case kind::BITVECTOR_SGE :
 589   case kind::EQUAL: {
 590     Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
 591
 592     os << "(bv_bbl_" << utils::toLFSCKindTerm(atom);
 593
 594     if (swap) {os << "_swap";}
 595
 596     os << " _ _ _ _ _ _ ";
 597     os << getBBTermName(atom[0]);
 598     os << " ";
 599     os << getBBTermName(atom[1]);
 600     os << ")";
 601
 602     return;
 603   }
 604   default: Unreachable() << "BitVectorProof Unknown atom kind";
 605   }
 606 }
 607
 608 void BitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os)
 609 {
 610   Assert(atom.getKind() == kind::EQUAL);
 611
 612   os << "(bv_bbl_=_false";
 613   os << " _ _ _ _ _ _ ";
 614   os << getBBTermName(atom[0]);
 615
 616   os << " ";
 617
 618   os << getBBTermName(atom[1]);
 619
 620   os << ")";
 621 }
 622
 623 void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
 624 {
 625   // bit-blast terms
 626   {
 627     Debug("pf::bv")
 628         << "BitVectorProof::printBitblasting: the bitblasted terms are: "
 629         << std::endl;
 630     std::vector<Expr>::const_iterator it = d_bbTerms.begin();
 631     std::vector<Expr>::const_iterator end = d_bbTerms.end();
 632
 633     for (; it != end; ++it) {
 634       if (d_usedBB.find(*it) == d_usedBB.end()) {
 635         Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl;
 636       } else {
 637         Debug("pf::bv") << "\t" << *it << std::endl;
 638       }
 639     }
 640
 641     Debug("pf::bv") << std::endl;
 642   }
 643
 644   std::vector<Expr>::const_iterator it = d_bbTerms.begin();
 645   std::vector<Expr>::const_iterator end = d_bbTerms.end();
 646   for (; it != end; ++it) {
 647     if (d_usedBB.find(*it) == d_usedBB.end() &&
 648         options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
 649       continue;
 650
 651     // Is this term has an alias, we inject it through the decl_bblast statement
 652     if (hasAlias(*it)) {
 653       os << "(decl_bblast_with_alias _ _ _ _ ";
 654       printTermBitblasting(*it, os);
 655       os << " " << d_aliasToBindDeclaration[d_assignedAliases[*it]] << " ";
 656       os << "(\\ "<< getBBTermName(*it);
 657       os << "\n";
 658       paren <<"))";
 659     } else {
 660       os << "(decl_bblast _ _ _ ";
 661       printTermBitblasting(*it, os);
 662       os << "(\\ "<< getBBTermName(*it);
 663       os << "\n";
 664       paren <<"))";
 665     }
 666   }
 667   // bit-blast atoms
 668   ExprToExpr::const_iterator ait = d_bbAtoms.begin();
 669   ExprToExpr::const_iterator aend = d_bbAtoms.end();
 670   for (; ait != aend; ++ait) {
 671     if (d_usedBB.find(ait->first) == d_usedBB.end() &&
 672         options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
 673       continue;
 674
 675     os << "(th_let_pf _ ";
 676     if (ait->first.getKind() == kind::CONST_BOOLEAN) {
 677       bool val = ait->first.getConst<bool>();
 678       os << "(iff_symm " << (val ? "true" : "false" ) << ")";
 679     } else {
 680       Assert(ait->first == ait->second[0]);
 681
 682       bool swap = false;
 683       if (ait->first.getKind() == kind::EQUAL) {
 684         Expr bitwiseEquivalence = ait->second[1];
 685         if ((bitwiseEquivalence.getKind() == kind::CONST_BOOLEAN) && !bitwiseEquivalence.getConst<bool>()) {
 686           printAtomBitblastingToFalse(ait->first, os);
 687         } else {
 688           if (bitwiseEquivalence.getKind() != kind::AND) {
 689             // Just one bit
 690             if (bitwiseEquivalence.getNumChildren() > 0 && bitwiseEquivalence[0].getKind() == kind::BITVECTOR_BITOF) {
 691               swap = (ait->first[1] == bitwiseEquivalence[0][0]);
 692             }
 693           } else {
 694             // Multiple bits
 695             if (bitwiseEquivalence[0].getNumChildren() > 0 &&
 696                 bitwiseEquivalence[0][0].getKind() == kind::BITVECTOR_BITOF) {
 697               swap = (ait->first[1] == bitwiseEquivalence[0][0][0]);
 698             } else if (bitwiseEquivalence[0].getNumChildren() > 0 &&
 699                        bitwiseEquivalence[0][1].getKind() == kind::BITVECTOR_BITOF) {
 700               swap = (ait->first[0] == bitwiseEquivalence[0][1][0]);
 701             }
 702           }
 703
 704           printAtomBitblasting(ait->first, os, swap);
 705         }
 706       } else {
 707         printAtomBitblasting(ait->first, os, swap);
 708       }
 709     }
 710
 711     os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n";
 712     paren <<"))";
 713   }
 714 }
 715
 716 theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
 717
 718 const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof()
 719 {
 720   return &d_atomsInBitblastingProof;
 721 }
 722
 723 std::string BitVectorProof::assignAlias(Expr expr)
 724 {
 725   Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end());
 726
 727   std::stringstream ss;
 728   ss << "fbv" << d_assignedAliases.size();
 729   Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl;
 730   d_assignedAliases[expr] = ss.str();
 731   return ss.str();
 732 }
 733
 734 bool BitVectorProof::hasAlias(Expr expr)
 735 {
 736   return d_assignedAliases.find(expr) != d_assignedAliases.end();
 737 }
 738
 739 void BitVectorProof::printConstantDisequalityProof(
 740     std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap)
 741 {
 742   Assert(c1.isConst());
 743   Assert(c2.isConst());
 744   Assert(utils::getSize(c1) == utils::getSize(c2));
 745
 746   os << "(bv_disequal_constants " << utils::getSize(c1) << " ";
 747
 748   std::ostringstream paren;
 749
 750   for (int i = utils::getSize(c1) - 1; i >= 0; --i) {
 751     os << "(bvc ";
 752     os << (utils::getBit(c1, i) ? "b1" : "b0") << " ";
 753     paren << ")";
 754   }
 755   os << "bvn";
 756   os << paren.str();
 757
 758   os << " ";
 759
 760   for (int i = utils::getSize(c2) - 1; i >= 0; --i) {
 761     os << "(bvc ";
 762     os << (utils::getBit(c2, i) ? "b1" : "b0") << " ";
 763
 764   }
 765   os << "bvn";
 766   os << paren.str();
 767
 768   os << ")";
 769 }
 770
 771 void BitVectorProof::printRewriteProof(std::ostream& os,
 772                                        const Node& n1,
 773                                        const Node& n2)
 774 {
 775   ProofLetMap emptyMap;
 776   os << "(rr_bv_default ";
 777   d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap);
 778   os << " ";
 779   d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap);
 780   os << ")";
 781 }
 782
 783 }  // namespace proof
 784
 785 }  // namespace CVC4