diff options
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 237 |
1 files changed, 129 insertions, 108 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index c0855122e..edaf8c154 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -106,7 +106,7 @@ void inline makeZero(Bits& bits, unsigned width) { * @return the carry-out */ Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry) { - Assert(res.size() == 0 && a.size() == b.size()); + Assert(a.size() == b.size() && res.size() == 0); for (unsigned i = 0 ; i < a.size(); ++i) { Node sum = mkXor(mkXor(a[i], b[i]), carry); @@ -119,6 +119,24 @@ Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry) return carry; } +inline void shiftAddMultiplier(const Bits&a, const Bits&b, Bits& res) { + + for (unsigned i = 0; i < a.size(); ++i) { + res.push_back(mkNode(kind::AND, b[0], a[i])); + } + + for(unsigned k = 1; k < res.size(); ++k) { + Node carry_in = mkFalse(); + Node carry_out; + for(unsigned j = 0; j < res.size() -k; ++j) { + Node aj = mkAnd(a[j], b[k]); + carry_out = mkOr(mkAnd(res[j+k], aj), + mkAnd( mkXor(res[j+k], aj), carry_in)); + res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in); + carry_in = carry_out; + } + } +} Node inline uLessThanBB(const Bits&a, const Bits& b, bool orEqual) { Assert (a.size() && b.size()); @@ -175,13 +193,13 @@ Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) { Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) { - Trace("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " + BVDebug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " << node.getKind() << "\n"; Unreachable(); } Node DefaultEqBB(TNode node, Bitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::EQUAL); Bits lhs, rhs; @@ -203,7 +221,7 @@ Node DefaultEqBB(TNode node, Bitblaster* bb) { Node AdderUltBB(TNode node, Bitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_ULT); Bits a, b; bb->bbTerm(node[0], a); @@ -225,7 +243,7 @@ Node AdderUltBB(TNode node, Bitblaster* bb) { Node DefaultUltBB(TNode node, Bitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_ULT); Bits a, b; bb->bbTerm(node[0], a); @@ -238,7 +256,7 @@ Node DefaultUltBB(TNode node, Bitblaster* bb) { } Node DefaultUleBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_ULE); Bits a, b; @@ -251,31 +269,31 @@ Node DefaultUleBB(TNode node, Bitblaster* bb){ } Node DefaultUgtBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } Node DefaultUgeBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } // Node DefaultSltBB(TNode node, Bitblaster* bb){ -// Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; +// BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; // // shoudl be rewritten in terms of ult // Unimplemented(); // } // Node DefaultSleBB(TNode node, Bitblaster* bb){ -// Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; +// BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; // // shoudl be rewritten in terms of ule // Unimplemented(); // } Node DefaultSltBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; Bits a, b; bb->bbTerm(node[0], a); @@ -287,7 +305,7 @@ Node DefaultSltBB(TNode node, Bitblaster* bb){ } Node DefaultSleBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; Bits a, b; bb->bbTerm(node[0], a); @@ -299,13 +317,13 @@ Node DefaultSleBB(TNode node, Bitblaster* bb){ } Node DefaultSgtBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } Node DefaultSgeBB(TNode node, Bitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + BVDebug("bitvector-bb") << "Bitblasting node " << node << "\n"; // should be rewritten Unimplemented(); } @@ -314,7 +332,7 @@ Node DefaultSgeBB(TNode node, Bitblaster* bb){ /// Term bitblasting strategies void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { - Trace("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " + BVDebug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " << node.getKind() << "\n"; Unreachable(); } @@ -327,12 +345,12 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { bits.push_back(utils::mkBitOf(node, i)); } - Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; - Debug("bitvector-bb") << " with bits " << toString(bits); + BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << " with bits " << toString(bits); } void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::CONST_BITVECTOR); Assert(bits.size() == 0); @@ -345,12 +363,12 @@ void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { bits.push_back(utils::mkTrue()); } } - Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; } void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_NOT); Assert(bits.size() == 0); Bits bv; @@ -359,7 +377,7 @@ void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; Assert(bits.size() == 0); Assert (node.getKind() == kind::BITVECTOR_CONCAT); @@ -373,64 +391,68 @@ void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) { } } Assert (bits.size() == utils::getSize(node)); - Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + BVDebug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; } - void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; - - Assert(node.getNumChildren() == 2 && - node.getKind() == kind::BITVECTOR_AND && + BVDebug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; + + Assert(node.getKind() == kind::BITVECTOR_AND && bits.size() == 0); - Bits lhs, rhs; - bb->bbTerm(node[0], rhs); - bb->bbTerm(node[1], lhs); - - Assert (lhs.size() == rhs.size()); - for (unsigned i = 0; i < lhs.size(); ++i) { - bits.push_back(utils::mkAnd(lhs[i], rhs[i])); + for(unsigned j = 0; j < utils::getSize(node); ++j) { + NodeBuilder<> andBuilder(kind::AND); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + Bits current; + bb->bbTerm(node[i], current); + andBuilder << current[j]; + Assert(utils::getSize(node) == current.size()); + } + bits.push_back(andBuilder); } - } void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; - Assert(node.getNumChildren() == 2 && - node.getKind() == kind::BITVECTOR_OR && + Assert(node.getKind() == kind::BITVECTOR_OR && bits.size() == 0); - Bits lhs, rhs; - bb->bbTerm(node[0], lhs); - bb->bbTerm(node[1], rhs); - Assert(lhs.size() == rhs.size()); - - for (unsigned i = 0; i < lhs.size(); ++i) { - bits.push_back(utils::mkOr(lhs[i], rhs[i])); + for(unsigned j = 0; j < utils::getSize(node); ++j) { + NodeBuilder<> orBuilder(kind::OR); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + Bits current; + bb->bbTerm(node[i], current); + orBuilder << current[j]; + Assert(utils::getSize(node) == current.size()); + } + bits.push_back(orBuilder); } } void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; - Assert(node.getNumChildren() == 2 && - node.getKind() == kind::BITVECTOR_XOR && + Assert(node.getKind() == kind::BITVECTOR_XOR && bits.size() == 0); - Bits lhs, rhs; - bb->bbTerm(node[0], lhs); - bb->bbTerm(node[1], rhs); - Assert(lhs.size() == rhs.size()); - - for (unsigned i = 0; i < lhs.size(); ++i) { - bits.push_back(utils::mkXor(lhs[i], rhs[i])); + for(unsigned j = 0; j < utils::getSize(node); ++j) { + Bits first; + bb->bbTerm(node[0], first); + Node bitj = first[j]; + + for (unsigned i = 1; i < node.getNumChildren(); ++i) { + Bits current; + bb->bbTerm(node[i], current); + bitj = utils::mkNode(kind::XOR, bitj, current[j]); + Assert(utils::getSize(node) == current.size()); + } + bits.push_back(bitj); } } void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; Assert(node.getNumChildren() == 2 && node.getKind() == kind::BITVECTOR_XNOR && @@ -447,17 +469,17 @@ void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) { void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; + BVDebug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP); Bits a, b; @@ -475,51 +497,50 @@ void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; + BVDebug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; Assert(res.size() == 0 && node.getKind() == kind::BITVECTOR_MULT); - Bits a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - // constructs a simple shift and add multiplier building the result in - // in res - - for (unsigned i = 0; i < a.size(); ++i) { - res.push_back(mkNode(kind::AND, b[0], a[i])); - } - - for(unsigned k = 1; k < res.size(); ++k) { - Node carry_in = mkFalse(); - Node carry_out; - for(unsigned j = 0; j < res.size() -k; ++j) { - Node aj = mkAnd(a[j], b[k]); - carry_out = mkOr(mkAnd(res[j+k], aj), - mkAnd( mkXor(res[j+k], aj), carry_in)); - res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in); - carry_in = carry_out; - } + Bits newres; + bb->bbTerm(node[0], res); + for(unsigned i = 1; i < node.getNumChildren(); ++i) { + Bits current; + bb->bbTerm(node[i], current); + newres.clear(); + // constructs a simple shift and add multiplier building the result + // in res + shiftAddMultiplier(res, current, newres); + res = newres; } - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_PLUS && res.size() == 0); - Bits a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); + bb->bbTerm(node[0], res); - Assert(a.size() == b.size() && utils::getSize(node) == a.size()); - rippleCarryAdder(a, b, res, mkFalse()); + Bits newres; + + for(unsigned i = 1; i < node.getNumChildren(); ++i) { + Bits current; + bb->bbTerm(node[i], current); + newres.clear(); + rippleCarryAdder(res, current, newres, utils::mkFalse()); + res = newres; + } + + Assert(res.size() == utils::getSize(node)); } void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_SUB && bits.size() == 0); + BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SUB && + node.getNumChildren() == 2 && + bits.size() == 0); Bits a, b; bb->bbTerm(node[0], a); @@ -534,7 +555,7 @@ void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { } void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_NEG); Bits a; @@ -612,7 +633,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid } void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); Bits a, b; @@ -628,7 +649,7 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { } void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n"; Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); Bits a, b; @@ -645,23 +666,23 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); Bits a, b; @@ -688,11 +709,11 @@ void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { } } } - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); Bits a, b; @@ -719,12 +740,12 @@ void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { } } } - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); Bits a, b; @@ -752,7 +773,7 @@ void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { } } } - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + BVDebug("bitvector-bb") << "with bits: " << toString(res) << "\n"; } @@ -770,14 +791,14 @@ void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) { } Assert (bits.size() == high - low + 1); - Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; - Debug("bitvector-bb") << " with bits " << toString(bits); + BVDebug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << " with bits " << toString(bits); } void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; // this should be rewritten Unimplemented(); @@ -785,7 +806,7 @@ void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) { void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; // this should be rewritten Unimplemented(); @@ -793,7 +814,7 @@ void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { } void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; + BVDebug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && res_bits.size() == 0); @@ -816,14 +837,14 @@ void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { } void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " + BVDebug("bitvector") << "theory::bv:: Unimplemented kind " << node.getKind() << "\n"; Unimplemented(); } |