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::printOwnedTerm(Expr term
,
126 const ProofLetMap
& map
)
128 Debug("pf::bv") << std::endl
129 << "(pf::bv) BitVectorProof::printOwnedTerm( " << term
130 << " ), theory is: " << theory::Theory::theoryOf(term
)
133 Assert(theory::Theory::theoryOf(term
) == theory::THEORY_BV
);
135 // peel off eager bit-blasting trick
136 if (term
.getKind() == kind::BITVECTOR_EAGER_ATOM
) {
137 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
141 switch (term
.getKind()) {
142 case kind::CONST_BITVECTOR
: {
143 printConstant(term
, os
);
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
);
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
);
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
);
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
);
196 case kind::BITVECTOR_BITOF
: {
197 printBitOf(term
, os
, map
);
201 case kind::VARIABLE
: {
202 os
<< "(a_var_bv " << utils::getSize(term
)<< " " << ProofManager::sanitize(term
) << ")";
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?
211 if (ProofManager::getSkolemizationManager()->isSkolem(term
)) {
212 os
<< ProofManager::sanitize(term
);
214 os
<< "(a_var_bv " << utils::getSize(term
)<< " " << ProofManager::sanitize(term
) << ")";
224 void BitVectorProof::printEmptyClauseProof(std::ostream
& os
,
227 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
)
228 << "the BV theory should only be proving bottom directly in the eager "
232 void BitVectorProof::printBitOf(Expr term
,
234 const ProofLetMap
& map
)
236 Assert(term
.getKind() == kind::BITVECTOR_BITOF
);
237 unsigned bit
= term
.getOperator().getConst
<BitVectorBitOf
>().bitIndex
;
240 Debug("pf::bv") << "BitVectorProof::printBitOf( " << term
<< " ), "
241 << "bit = " << bit
<< ", var = " << var
<< std::endl
;
244 os
<< d_exprToVariableName
[var
];
245 os
<< " " << bit
<< ")";
248 void BitVectorProof::printConstant(Expr term
, std::ostream
& os
)
250 Assert(term
.isConst());
251 os
<< "(a_bv " << utils::getSize(term
) << " ";
253 if (d_useConstantLetification
) {
254 os
<< d_constantLetMap
[term
] << ")";
256 std::ostringstream paren
;
257 int size
= utils::getSize(term
);
258 for (int i
= size
- 1; i
>= 0; --i
) {
260 os
<< (utils::getBit(term
, i
) ? "b1" : "b0") <<" ";
268 void BitVectorProof::printOperatorNary(Expr term
,
270 const ProofLetMap
& map
)
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
278 for (unsigned i
= 0; i
< term
.getNumChildren() - 1; ++i
) {
279 os
<<"("<< op
<<" " << size
<<" " << holes
;
281 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
283 for (unsigned i
= 1; i
< term
.getNumChildren(); ++i
) {
284 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
289 void BitVectorProof::printOperatorUnary(Expr term
,
291 const ProofLetMap
& map
)
294 os
<< utils::toLFSCKindTerm(term
) << " " << utils::getSize(term
) <<" ";
296 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
300 void BitVectorProof::printPredicate(Expr term
,
302 const ProofLetMap
& map
)
305 os
<< utils::toLFSCKindTerm(term
) << " " << utils::getSize(term
[0]) <<" ";
307 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
309 d_proofEngine
->printBoundTerm(term
[1], os
, map
);
313 void BitVectorProof::printOperatorParametric(Expr term
,
315 const ProofLetMap
& map
)
318 os
<< utils::toLFSCKindTerm(term
) << " " << utils::getSize(term
) <<" ";
320 if (term
.getKind() == kind::BITVECTOR_REPEAT
) {
321 unsigned amount
= term
.getOperator().getConst
<BitVectorRepeat
>().repeatAmount
;
322 os
<< amount
<<" _ ";
324 if (term
.getKind() == kind::BITVECTOR_SIGN_EXTEND
) {
325 unsigned amount
= term
.getOperator().getConst
<BitVectorSignExtend
>().signExtendAmount
;
326 os
<< amount
<<" _ ";
329 if (term
.getKind() == kind::BITVECTOR_ZERO_EXTEND
) {
330 unsigned amount
= term
.getOperator().getConst
<BitVectorZeroExtend
>().zeroExtendAmount
;
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]);
339 Assert(term
.getNumChildren() == 1);
340 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
344 void BitVectorProof::printOwnedSort(Type type
, std::ostream
& os
)
346 Debug("pf::bv") << std::endl
347 << "(pf::bv) BitVectorProof::printOwnedSort( " << type
<< " )"
349 Assert(type
.isBitVector());
350 unsigned width
= utils::getSize(type
);
351 os
<< "(BitVec " << width
<< ")";
354 void BitVectorProof::printSortDeclarations(std::ostream
& os
,
357 // Nothing to do here at this point.
360 void BitVectorProof::printTermDeclarations(std::ostream
& os
,
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
);
369 std::string newAlias
= assignAlias(*it
);
370 d_exprToVariableName
[*it
] = newAlias
;
373 os
<< "(% " << d_exprToVariableName
[*it
] <<" var_bv" << "\n";
378 void BitVectorProof::printDeferredDeclarations(std::ostream
& os
,
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
) {
390 os
<< (utils::getBit(it
->first
, i
) ? "b1" : "b0") << " ";
394 os
<< localParen
.str();
399 d_useConstantLetification
= true;
403 void BitVectorProof::printAliasingDeclarations(std::ostream
& os
,
405 const ProofLetMap
& globalLetMap
)
407 // Print "trust" statements to bind complex bv variables to their associated terms
409 ExprToString::const_iterator it
= d_assignedAliases
.begin();
410 ExprToString::const_iterator end
= d_assignedAliases
.end();
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();
418 os
<< "(th_let_pf _ ";
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
);
425 os
<< "(\\ "<< d_aliasToBindDeclaration
[it
->second
] << "\n";
432 void BitVectorProof::printTermBitblasting(Expr term
, std::ostream
& os
)
434 // TODO: once we have the operator elimination rules remove those that we
436 Assert(term
.getType().isBitVector());
437 Kind kind
= term
.getKind();
439 if (theory::Theory::isLeafOf(term
, theory::THEORY_BV
) && !term
.isConst())
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
];
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
] << ")";
455 for (int i
= size
- 1; i
>= 0; --i
) {
457 os
<< (utils::getBit(term
, i
) ? "b1" : "b0") <<" ";
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
;
479 for (int i
= term
.getNumChildren() - 1; i
> 0; --i
) {
480 os
<<"(bv_bbl_"<< utils::toLFSCKind(kind
);
482 if (kind
== kind::BITVECTOR_CONCAT
) {
483 os
<< " " << utils::getSize(term
) << " _";
485 os
<< " _ _ _ _ _ _ ";
488 os
<< getBBTermName(term
[0]) << " ";
490 for (unsigned i
= 1; i
< term
.getNumChildren(); ++i
) {
491 os
<< getBBTermName(term
[i
]);
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
);
503 os
<< getBBTermName(term
[0]);
507 case kind::BITVECTOR_EXTRACT
: {
508 os
<<"(bv_bbl_"<<utils::toLFSCKind(kind
);
510 os
<< " " << utils::getSize(term
) << " ";
511 os
<< utils::getExtractHigh(term
) << " ";
512 os
<< utils::getExtractLow(term
) << " ";
515 os
<< getBBTermName(term
[0]);
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
;
528 if (term
.getKind() == kind::BITVECTOR_SIGN_EXTEND
) {
529 unsigned amount
= term
.getOperator().getConst
<BitVectorSignExtend
>().signExtendAmount
;
533 if (term
.getKind() == kind::BITVECTOR_ZERO_EXTEND
) {
534 unsigned amount
= term
.getOperator().getConst
<BitVectorZeroExtend
>().zeroExtendAmount
;
539 os
<< getBBTermName(term
[0]);
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 _ ";
557 d_proofEngine
->printLetTerm(term
, os
);
559 std::vector
<Node
> bits
;
560 d_bitblaster
->bbTerm(term
, bits
);
562 for (int i
= utils::getSize(term
) - 1; i
>= 0; --i
) {
564 d_proofEngine
->printLetTerm((bits
[i
]).toExpr(), os
);
567 os
<< "bbltn" << paren
.str();
571 default: Unreachable() << "BitVectorProof Unknown operator";
575 void BitVectorProof::printAtomBitblasting(Expr atom
,
579 Kind kind
= atom
.getKind();
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
:
590 Debug("pf::bv") << "Bitblasing kind = " << kind
<< std::endl
;
592 os
<< "(bv_bbl_" << utils::toLFSCKindTerm(atom
);
594 if (swap
) {os
<< "_swap";}
596 os
<< " _ _ _ _ _ _ ";
597 os
<< getBBTermName(atom
[0]);
599 os
<< getBBTermName(atom
[1]);
604 default: Unreachable() << "BitVectorProof Unknown atom kind";
608 void BitVectorProof::printAtomBitblastingToFalse(Expr atom
, std::ostream
& os
)
610 Assert(atom
.getKind() == kind::EQUAL
);
612 os
<< "(bv_bbl_=_false";
613 os
<< " _ _ _ _ _ _ ";
614 os
<< getBBTermName(atom
[0]);
618 os
<< getBBTermName(atom
[1]);
623 void BitVectorProof::printBitblasting(std::ostream
& os
, std::ostream
& paren
)
628 << "BitVectorProof::printBitblasting: the bitblasted terms are: "
630 std::vector
<Expr
>::const_iterator it
= d_bbTerms
.begin();
631 std::vector
<Expr
>::const_iterator end
= d_bbTerms
.end();
633 for (; it
!= end
; ++it
) {
634 if (d_usedBB
.find(*it
) == d_usedBB
.end()) {
635 Debug("pf::bv") << "\t" << *it
<< "\t(UNUSED)" << std::endl
;
637 Debug("pf::bv") << "\t" << *it
<< std::endl
;
641 Debug("pf::bv") << std::endl
;
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
)
651 // Is this term has an alias, we inject it through the decl_bblast statement
653 os
<< "(decl_bblast_with_alias _ _ _ _ ";
654 printTermBitblasting(*it
, os
);
655 os
<< " " << d_aliasToBindDeclaration
[d_assignedAliases
[*it
]] << " ";
656 os
<< "(\\ "<< getBBTermName(*it
);
660 os
<< "(decl_bblast _ _ _ ";
661 printTermBitblasting(*it
, os
);
662 os
<< "(\\ "<< getBBTermName(*it
);
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
)
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" ) << ")";
680 Assert(ait
->first
== ait
->second
[0]);
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
);
688 if (bitwiseEquivalence
.getKind() != kind::AND
) {
690 if (bitwiseEquivalence
.getNumChildren() > 0 && bitwiseEquivalence
[0].getKind() == kind::BITVECTOR_BITOF
) {
691 swap
= (ait
->first
[1] == bitwiseEquivalence
[0][0]);
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]);
704 printAtomBitblasting(ait
->first
, os
, swap
);
707 printAtomBitblasting(ait
->first
, os
, swap
);
711 os
<<"(\\ " << ProofManager::getPreprocessedAssertionName(ait
->second
) <<"\n";
716 theory::TheoryId
BitVectorProof::getTheoryId() { return theory::THEORY_BV
; }
718 const std::set
<Node
>* BitVectorProof::getAtomsInBitblastingProof()
720 return &d_atomsInBitblastingProof
;
723 std::string
BitVectorProof::assignAlias(Expr expr
)
725 Assert(d_exprToVariableName
.find(expr
) == d_exprToVariableName
.end());
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();
734 bool BitVectorProof::hasAlias(Expr expr
)
736 return d_assignedAliases
.find(expr
) != d_assignedAliases
.end();
739 void BitVectorProof::printConstantDisequalityProof(
740 std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
& globalLetMap
)
742 Assert(c1
.isConst());
743 Assert(c2
.isConst());
744 Assert(utils::getSize(c1
) == utils::getSize(c2
));
746 os
<< "(bv_disequal_constants " << utils::getSize(c1
) << " ";
748 std::ostringstream paren
;
750 for (int i
= utils::getSize(c1
) - 1; i
>= 0; --i
) {
752 os
<< (utils::getBit(c1
, i
) ? "b1" : "b0") << " ";
760 for (int i
= utils::getSize(c2
) - 1; i
>= 0; --i
) {
762 os
<< (utils::getBit(c2
, i
) ? "b1" : "b0") << " ";
771 void BitVectorProof::printRewriteProof(std::ostream
& os
,
775 ProofLetMap emptyMap
;
776 os
<< "(rr_bv_default ";
777 d_proofEngine
->printBoundTerm(n2
.toExpr(), os
, emptyMap
);
779 d_proofEngine
->printBoundTerm(n1
.toExpr(), os
, emptyMap
);