1 /********************* */
2 /*! \file bitvector_proof.cpp
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
12 ** Contains implementions (e.g. code for printing bitblasting bindings that is
13 ** common to all kinds of bitvector proofs.
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"
28 BitVectorProof::BitVectorProof(theory::bv::TheoryBV
* bv
,
29 TheoryProofEngine
* proofEngine
)
30 : TheoryProof(bv
, proofEngine
),
35 d_bitblaster(nullptr),
36 d_useConstantLetification(false),
41 void BitVectorProof::setBitblaster(theory::bv::TBitblaster
<Node
>* bb
)
43 Assert(d_bitblaster
== NULL
);
47 void BitVectorProof::registerTermBB(Expr term
)
49 Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term
52 if (d_seenBBTerms
.find(term
) != d_seenBBTerms
.end()) return;
54 d_seenBBTerms
.insert(term
);
55 d_bbTerms
.push_back(term
);
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.
62 if (theory::Theory::theoryOf(term
) != theory::THEORY_BV
)
64 Debug("pf::bv") << "\tMarking term " << term
65 << " for future BV registration" << std::endl
;
66 d_proofEngine
->markTermForFutureRegistration(term
, theory::THEORY_BV
);
70 void BitVectorProof::registerAtomBB(Expr atom
, Expr atom_bb
) {
71 Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom
72 << ", " << atom_bb
<< " )" << std::endl
;
74 Expr def
= atom
.eqExpr(atom_bb
);
75 d_bbAtoms
.insert(std::make_pair(atom
, def
));
78 // Register the atom's terms for bitblasting
79 registerTermBB(atom
[0]);
80 registerTermBB(atom
[1]);
83 void BitVectorProof::registerTerm(Expr term
) {
84 Debug("pf::bv") << "BitVectorProof::registerTerm( " << term
<< " )"
87 if (options::lfscLetification() && term
.isConst()
88 && term
.getType().isBitVector())
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();
97 d_usedBB
.insert(term
);
99 if (theory::Theory::isLeafOf(term
, theory::THEORY_BV
) && !term
.isConst())
101 d_declarations
.insert(term
);
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
;
109 // don't care about parametric operators for bv?
110 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
111 d_proofEngine
->registerTerm(term
[i
]);
115 std::string
BitVectorProof::getBBTermName(Expr expr
)
117 Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr
<< " ) = bt"
118 << expr
.getId() << std::endl
;
119 std::ostringstream os
;
120 os
<< "bt" << expr
.getId();
124 void BitVectorProof::printOwnedTermAsType(Expr term
,
126 const ProofLetMap
& map
,
127 TypeNode expectedType
)
129 Debug("pf::bv") << std::endl
130 << "(pf::bv) BitVectorProof::printOwnedTerm( " << term
131 << " ), theory is: " << theory::Theory::theoryOf(term
)
134 Assert(theory::Theory::theoryOf(term
) == theory::THEORY_BV
);
136 // peel off eager bit-blasting trick
137 if (term
.getKind() == kind::BITVECTOR_EAGER_ATOM
) {
138 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
142 switch (term
.getKind()) {
143 case kind::CONST_BITVECTOR
: {
144 printConstant(term
, os
);
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
);
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
);
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
);
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
);
197 case kind::BITVECTOR_BITOF
: {
198 printBitOf(term
, os
, map
);
202 case kind::VARIABLE
: {
203 os
<< "(a_var_bv " << utils::getSize(term
)<< " " << ProofManager::sanitize(term
) << ")";
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?
212 if (ProofManager::getSkolemizationManager()->isSkolem(term
)) {
213 os
<< ProofManager::sanitize(term
);
215 os
<< "(a_var_bv " << utils::getSize(term
)<< " " << ProofManager::sanitize(term
) << ")";
225 void BitVectorProof::printEmptyClauseProof(std::ostream
& os
,
228 Assert(options::bitblastMode() == options::BitblastMode::EAGER
)
229 << "the BV theory should only be proving bottom directly in the eager "
233 void BitVectorProof::printBitOf(Expr term
,
235 const ProofLetMap
& map
)
237 Assert(term
.getKind() == kind::BITVECTOR_BITOF
);
238 unsigned bit
= term
.getOperator().getConst
<BitVectorBitOf
>().d_bitIndex
;
241 Debug("pf::bv") << "BitVectorProof::printBitOf( " << term
<< " ), "
242 << "bit = " << bit
<< ", var = " << var
<< std::endl
;
245 os
<< d_exprToVariableName
[var
];
246 os
<< " " << bit
<< ")";
249 void BitVectorProof::printConstant(Expr term
, std::ostream
& os
)
251 Assert(term
.isConst());
252 os
<< "(a_bv " << utils::getSize(term
) << " ";
254 if (d_useConstantLetification
) {
255 os
<< d_constantLetMap
[term
] << ")";
257 std::ostringstream paren
;
258 int size
= utils::getSize(term
);
259 for (int i
= size
- 1; i
>= 0; --i
) {
261 os
<< (utils::getBit(term
, i
) ? "b1" : "b0") <<" ";
269 void BitVectorProof::printOperatorNary(Expr term
,
271 const ProofLetMap
& map
)
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
279 for (unsigned i
= 0; i
< term
.getNumChildren() - 1; ++i
) {
280 os
<<"("<< op
<<" " << size
<<" " << holes
;
282 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
284 for (unsigned i
= 1; i
< term
.getNumChildren(); ++i
) {
285 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
290 void BitVectorProof::printOperatorUnary(Expr term
,
292 const ProofLetMap
& map
)
295 os
<< utils::toLFSCKindTerm(term
) << " " << utils::getSize(term
) <<" ";
297 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
301 void BitVectorProof::printPredicate(Expr term
,
303 const ProofLetMap
& map
)
306 os
<< utils::toLFSCKindTerm(term
) << " " << utils::getSize(term
[0]) <<" ";
308 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
310 d_proofEngine
->printBoundTerm(term
[1], os
, map
);
314 void BitVectorProof::printOperatorParametric(Expr term
,
316 const ProofLetMap
& map
)
319 os
<< utils::toLFSCKindTerm(term
) << " " << utils::getSize(term
) <<" ";
321 if (term
.getKind() == kind::BITVECTOR_REPEAT
) {
323 term
.getOperator().getConst
<BitVectorRepeat
>().d_repeatAmount
;
324 os
<< amount
<<" _ ";
326 if (term
.getKind() == kind::BITVECTOR_SIGN_EXTEND
) {
328 term
.getOperator().getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
329 os
<< amount
<<" _ ";
332 if (term
.getKind() == kind::BITVECTOR_ZERO_EXTEND
) {
334 term
.getOperator().getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
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]);
343 Assert(term
.getNumChildren() == 1);
344 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
348 void BitVectorProof::printOwnedSort(Type type
, std::ostream
& os
)
350 Debug("pf::bv") << std::endl
351 << "(pf::bv) BitVectorProof::printOwnedSort( " << type
<< " )"
353 Assert(type
.isBitVector());
354 unsigned width
= utils::getSize(type
);
355 os
<< "(BitVec " << width
<< ")";
358 void BitVectorProof::printSortDeclarations(std::ostream
& os
,
361 // Nothing to do here at this point.
364 void BitVectorProof::printTermDeclarations(std::ostream
& os
,
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
);
373 std::string newAlias
= assignAlias(*it
);
374 d_exprToVariableName
[*it
] = newAlias
;
377 os
<< "(% " << d_exprToVariableName
[*it
] <<" var_bv" << "\n";
382 void BitVectorProof::printDeferredDeclarations(std::ostream
& os
,
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
) {
394 os
<< (utils::getBit(it
->first
, i
) ? "b1" : "b0") << " ";
398 os
<< localParen
.str();
403 d_useConstantLetification
= true;
407 void BitVectorProof::printAliasingDeclarations(std::ostream
& os
,
409 const ProofLetMap
& globalLetMap
)
411 // Print "trust" statements to bind complex bv variables to their associated terms
413 ExprToString::const_iterator it
= d_assignedAliases
.begin();
414 ExprToString::const_iterator end
= d_assignedAliases
.end();
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();
422 os
<< "(th_let_pf _ ";
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
);
429 os
<< "(\\ "<< d_aliasToBindDeclaration
[it
->second
] << "\n";
436 void BitVectorProof::printTermBitblasting(Expr term
, std::ostream
& os
)
438 // TODO: once we have the operator elimination rules remove those that we
440 Assert(term
.getType().isBitVector());
441 Kind kind
= term
.getKind();
443 if (theory::Theory::isLeafOf(term
, theory::THEORY_BV
) && !term
.isConst())
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
];
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
] << ")";
459 for (int i
= size
- 1; i
>= 0; --i
) {
461 os
<< (utils::getBit(term
, i
) ? "b1" : "b0") <<" ";
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
;
483 for (int i
= term
.getNumChildren() - 1; i
> 0; --i
) {
484 os
<<"(bv_bbl_"<< utils::toLFSCKind(kind
);
486 if (kind
== kind::BITVECTOR_CONCAT
) {
487 os
<< " " << utils::getSize(term
) << " _";
489 os
<< " _ _ _ _ _ _ ";
492 os
<< getBBTermName(term
[0]) << " ";
494 for (unsigned i
= 1; i
< term
.getNumChildren(); ++i
) {
495 os
<< getBBTermName(term
[i
]);
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
);
507 os
<< getBBTermName(term
[0]);
511 case kind::BITVECTOR_EXTRACT
: {
512 os
<<"(bv_bbl_"<<utils::toLFSCKind(kind
);
514 os
<< " " << utils::getSize(term
) << " ";
515 os
<< utils::getExtractHigh(term
) << " ";
516 os
<< utils::getExtractLow(term
) << " ";
519 os
<< getBBTermName(term
[0]);
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
) {
530 term
.getOperator().getConst
<BitVectorRepeat
>().d_repeatAmount
;
533 if (term
.getKind() == kind::BITVECTOR_SIGN_EXTEND
) {
535 term
.getOperator().getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
539 if (term
.getKind() == kind::BITVECTOR_ZERO_EXTEND
) {
541 term
.getOperator().getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
546 os
<< getBBTermName(term
[0]);
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 _ ";
564 d_proofEngine
->printLetTerm(term
, os
);
566 std::vector
<Node
> bits
;
567 d_bitblaster
->bbTerm(term
, bits
);
569 for (int i
= utils::getSize(term
) - 1; i
>= 0; --i
) {
571 d_proofEngine
->printLetTerm((bits
[i
]).toExpr(), os
);
574 os
<< "bbltn" << paren
.str();
578 default: Unreachable() << "BitVectorProof Unknown operator";
582 void BitVectorProof::printAtomBitblasting(Expr atom
,
586 Kind kind
= atom
.getKind();
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
:
597 Debug("pf::bv") << "Bitblasing kind = " << kind
<< std::endl
;
599 os
<< "(bv_bbl_" << utils::toLFSCKindTerm(atom
);
601 if (swap
) {os
<< "_swap";}
603 os
<< " _ _ _ _ _ _ ";
604 os
<< getBBTermName(atom
[0]);
606 os
<< getBBTermName(atom
[1]);
611 default: Unreachable() << "BitVectorProof Unknown atom kind";
615 void BitVectorProof::printAtomBitblastingToFalse(Expr atom
, std::ostream
& os
)
617 Assert(atom
.getKind() == kind::EQUAL
);
619 os
<< "(bv_bbl_=_false";
620 os
<< " _ _ _ _ _ _ ";
621 os
<< getBBTermName(atom
[0]);
625 os
<< getBBTermName(atom
[1]);
630 void BitVectorProof::printBitblasting(std::ostream
& os
, std::ostream
& paren
)
635 << "BitVectorProof::printBitblasting: the bitblasted terms are: "
637 std::vector
<Expr
>::const_iterator it
= d_bbTerms
.begin();
638 std::vector
<Expr
>::const_iterator end
= d_bbTerms
.end();
640 for (; it
!= end
; ++it
) {
641 if (d_usedBB
.find(*it
) == d_usedBB
.end()) {
642 Debug("pf::bv") << "\t" << *it
<< "\t(UNUSED)" << std::endl
;
644 Debug("pf::bv") << "\t" << *it
<< std::endl
;
648 Debug("pf::bv") << std::endl
;
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
)
658 // Is this term has an alias, we inject it through the decl_bblast statement
660 os
<< "(decl_bblast_with_alias _ _ _ _ ";
661 printTermBitblasting(*it
, os
);
662 os
<< " " << d_aliasToBindDeclaration
[d_assignedAliases
[*it
]] << " ";
663 os
<< "(\\ "<< getBBTermName(*it
);
667 os
<< "(decl_bblast _ _ _ ";
668 printTermBitblasting(*it
, os
);
669 os
<< "(\\ "<< getBBTermName(*it
);
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
)
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" ) << ")";
687 Assert(ait
->first
== ait
->second
[0]);
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
);
695 if (bitwiseEquivalence
.getKind() != kind::AND
) {
697 if (bitwiseEquivalence
.getNumChildren() > 0 && bitwiseEquivalence
[0].getKind() == kind::BITVECTOR_BITOF
) {
698 swap
= (ait
->first
[1] == bitwiseEquivalence
[0][0]);
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]);
711 printAtomBitblasting(ait
->first
, os
, swap
);
714 printAtomBitblasting(ait
->first
, os
, swap
);
718 os
<<"(\\ " << ProofManager::getPreprocessedAssertionName(ait
->second
) <<"\n";
723 theory::TheoryId
BitVectorProof::getTheoryId() { return theory::THEORY_BV
; }
725 const std::set
<Node
>* BitVectorProof::getAtomsInBitblastingProof()
727 return &d_atomsInBitblastingProof
;
730 std::string
BitVectorProof::assignAlias(Expr expr
)
732 Assert(d_exprToVariableName
.find(expr
) == d_exprToVariableName
.end());
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();
741 bool BitVectorProof::hasAlias(Expr expr
)
743 return d_assignedAliases
.find(expr
) != d_assignedAliases
.end();
746 void BitVectorProof::printConstantDisequalityProof(
747 std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
& globalLetMap
)
749 Assert(c1
.isConst());
750 Assert(c2
.isConst());
751 Assert(utils::getSize(c1
) == utils::getSize(c2
));
753 os
<< "(bv_disequal_constants " << utils::getSize(c1
) << " ";
755 std::ostringstream paren
;
757 for (int i
= utils::getSize(c1
) - 1; i
>= 0; --i
) {
759 os
<< (utils::getBit(c1
, i
) ? "b1" : "b0") << " ";
767 for (int i
= utils::getSize(c2
) - 1; i
>= 0; --i
) {
769 os
<< (utils::getBit(c2
, i
) ? "b1" : "b0") << " ";
778 void BitVectorProof::printRewriteProof(std::ostream
& os
,
782 ProofLetMap emptyMap
;
783 os
<< "(rr_bv_default ";
784 d_proofEngine
->printBoundTerm(n2
.toExpr(), os
, emptyMap
);
786 d_proofEngine
->printBoundTerm(n1
.toExpr(), os
, emptyMap
);