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