diff options
author | Tim King <taking@cs.nyu.edu> | 2013-02-14 16:11:42 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-02-14 16:11:42 -0500 |
commit | fc4121b761dd524ad5fe37789381e5814737e6b9 (patch) | |
tree | fec292ebddd652d5938c7e9f266b52a4770bfae1 /src/theory/bv/bitblast_strategies.cpp | |
parent | 63ca7c0a10dcd6b3be42d4d513f842db76733392 (diff) |
Removing BVDebug and replacing with Debug.
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index c25c40c22..a952b2929 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -191,13 +191,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) { Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) { - BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " + Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " << node.getKind() << "\n"; Unreachable(); } Node DefaultEqBB(TNode node, Bitblaster* bb) { - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::EQUAL); Bits lhs, rhs; @@ -219,7 +219,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) { Node AdderUltBB(TNode node, Bitblaster* bb) { - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_ULT); Bits a, b; bb->bbTerm(node[0], a); @@ -241,7 +241,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) { Node DefaultUltBB(TNode node, Bitblaster* bb) { - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_ULT); Bits a, b; bb->bbTerm(node[0], a); @@ -254,7 +254,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) { } Node DefaultUleBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_ULE); Bits a, b; @@ -267,31 +267,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){ } Node DefaultUgtBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } Node DefaultUgeBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } // Node DefaultSltBB(TNode node, Bitblaster* bb){ -// BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; +// Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; // // shoudl be rewritten in terms of ult // Unimplemented(); // } // Node DefaultSleBB(TNode node, Bitblaster* bb){ -// BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; +// Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; // // shoudl be rewritten in terms of ule // Unimplemented(); // } Node DefaultSltBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; Bits a, b; bb->bbTerm(node[0], a); @@ -303,7 +303,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){ } Node DefaultSleBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; Bits a, b; bb->bbTerm(node[0], a); @@ -315,13 +315,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){ } Node DefaultSgtBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } Node DefaultSgeBB(TNode node, Bitblaster* bb){ - BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } @@ -330,7 +330,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){ /// Term bitblasting strategies void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " + Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " << node.getKind() << "\n"; Unreachable(); } @@ -342,15 +342,15 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { } if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; - BVDebug("bitvector-bb") << " with bits " << toString(bits); + Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << " with bits " << toString(bits); } bb->storeVariable(node); } void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::CONST_BITVECTOR); Assert(bits.size() == 0); @@ -364,13 +364,13 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { } } if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; } } void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_NOT); Assert(bits.size() == 0); Bits bv; @@ -379,7 +379,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; Assert(bits.size() == 0); Assert (node.getKind() == kind::BITVECTOR_CONCAT); @@ -394,12 +394,12 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) { } Assert (bits.size() == utils::getSize(node)); if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; } } void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0); @@ -417,7 +417,7 @@ void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0); @@ -435,7 +435,7 @@ void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0); @@ -456,7 +456,7 @@ void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; Assert(node.getNumChildren() == 2 && node.getKind() == kind::BITVECTOR_XNOR && @@ -473,17 +473,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) { void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; + Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP); Bits a, b; @@ -501,7 +501,7 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; + Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; Assert(res.size() == 0 && node.getKind() == kind::BITVECTOR_MULT); @@ -517,12 +517,12 @@ void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { res = newres; } if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0); @@ -543,7 +543,7 @@ void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_SUB && node.getNumChildren() == 2 && bits.size() == 0); @@ -561,7 +561,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_NEG); Bits a; @@ -639,7 +639,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid } void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); Bits a, b; @@ -666,7 +666,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); Bits a, b; @@ -694,23 +694,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); Bits a, b; @@ -738,12 +738,12 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { } } if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); Bits a, b; @@ -771,13 +771,13 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { } } if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); Bits a, b; @@ -806,7 +806,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { } } if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } } @@ -825,14 +825,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) { Assert (bits.size() == high - low + 1); if(Debug.isOn("bitvector-bb")) { - BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; - BVDebug("bitvector-bb") << " with bits " << toString(bits); + Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << " with bits " << toString(bits); } } void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; // this should be rewritten Unimplemented(); @@ -840,7 +840,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) { void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; // this should be rewritten Unimplemented(); @@ -848,7 +848,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { } void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { - BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0); @@ -871,14 +871,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { } void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) { - BVDebug("bitvector") << "theory::bv:: Unimplemented kind " + Debug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } |