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 {
BitVectorProof(theory::bv::TheoryBV * bv,TheoryProofEngine * proofEngine)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 
setBitblaster(theory::bv::TBitblaster<Node> * bb)41 void BitVectorProof::setBitblaster(theory::bv::TBitblaster<Node>* bb)
42 {
43   Assert(d_bitblaster == NULL);
44   d_bitblaster = bb;
45 }
46 
registerTermBB(Expr term)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 
registerAtomBB(Expr atom,Expr atom_bb)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 
registerTerm(Expr term)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 
getBBTermName(Expr expr)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 
printOwnedTerm(Expr term,std::ostream & os,const ProofLetMap & map)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 
printEmptyClauseProof(std::ostream & os,std::ostream & paren)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 
printBitOf(Expr term,std::ostream & os,const ProofLetMap & map)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 
printConstant(Expr term,std::ostream & os)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 
printOperatorNary(Expr term,std::ostream & os,const ProofLetMap & map)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 
printOperatorUnary(Expr term,std::ostream & os,const ProofLetMap & map)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 
printPredicate(Expr term,std::ostream & os,const ProofLetMap & map)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 
printOperatorParametric(Expr term,std::ostream & os,const ProofLetMap & map)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 
printOwnedSort(Type type,std::ostream & os)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 
printSortDeclarations(std::ostream & os,std::ostream & paren)354 void BitVectorProof::printSortDeclarations(std::ostream& os,
355                                            std::ostream& paren)
356 {
357   // Nothing to do here at this point.
358 }
359 
printTermDeclarations(std::ostream & os,std::ostream & paren)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 
printDeferredDeclarations(std::ostream & os,std::ostream & paren)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 
printAliasingDeclarations(std::ostream & os,std::ostream & paren,const ProofLetMap & globalLetMap)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 
printTermBitblasting(Expr term,std::ostream & os)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 
printAtomBitblasting(Expr atom,std::ostream & os,bool swap)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 
printAtomBitblastingToFalse(Expr atom,std::ostream & os)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 
printBitblasting(std::ostream & os,std::ostream & paren)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 
getTheoryId()716 theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
717 
getAtomsInBitblastingProof()718 const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof()
719 {
720   return &d_atomsInBitblastingProof;
721 }
722 
assignAlias(Expr expr)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 
hasAlias(Expr expr)734 bool BitVectorProof::hasAlias(Expr expr)
735 {
736   return d_assignedAliases.find(expr) != d_assignedAliases.end();
737 }
738 
printConstantDisequalityProof(std::ostream & os,Expr c1,Expr c2,const ProofLetMap & globalLetMap)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 
printRewriteProof(std::ostream & os,const Node & n1,const Node & n2)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
786