diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/theory | |
parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 237 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.cpp | 100 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.h | 13 | ||||
-rw-r--r-- | src/theory/bv/kinds | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 109 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 50 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 144 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 40 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 577 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 355 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 256 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 78 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 45 |
14 files changed, 1502 insertions, 522 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(); } diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index 6f91335ce..f5c43688a 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -23,6 +23,7 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "theory_bv_rewrite_rules_simplification.h" using namespace std; @@ -57,7 +58,7 @@ Bitblaster::Bitblaster(context::Context* c) : d_assertedAtoms(c), d_statistics() { - d_satSolver = prop::SatSolverFactory::createMinisat(); + d_satSolver = prop::SatSolverFactory::createMinisat(c); d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); // initializing the bit-blasting strategies @@ -83,7 +84,7 @@ void Bitblaster::bbAtom(TNode node) { } BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; - + ++d_statistics.d_numAtoms; // the bitblasted definition of the atom Node atom_bb = d_atomBBStrategies[node.getKind()](node, this); // asserting that the atom is true iff the definition holds @@ -101,14 +102,78 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) { return; } BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; - d_termBBStrategies[node.getKind()] (node, bits,this); + ++d_statistics.d_numTerms; + + Node optimized = bbOptimize(node); + + // if we already bitblasted the optimized version + if(hasBBTerm(optimized)) { + getBBTerm(optimized, bits); + // cache it as the same for this node + cacheTermDef(node, bits); + return; + } + + d_termBBStrategies[optimized.getKind()] (optimized, bits,this); - Assert (bits.size() == utils::getSize(node)); + Assert (bits.size() == utils::getSize(node) && + bits.size() == utils::getSize(optimized)); + + if(optimized != node) { + cacheTermDef(optimized, bits); + } cacheTermDef(node, bits); } +Node Bitblaster::bbOptimize(TNode node) { + std::vector<Node> children; + + if (node.getKind() == kind::BITVECTOR_PLUS) { + if (RewriteRule<BBPlusNeg>::applies(node)) { + Node res = RewriteRule<BBPlusNeg>::run<false>(node); + return res; + } + // if (RewriteRule<BBFactorOut>::applies(node)) { + // Node res = RewriteRule<BBFactorOut>::run<false>(node); + // return res; + // } + + } else if (node.getKind() == kind::BITVECTOR_MULT) { + if (RewriteRule<MultPow2>::applies(node)) { + Node res = RewriteRule<MultPow2>::run<false>(node); + return res; + } + } + + return node; +} + /// Public methods +void Bitblaster::addAtom(TNode atom) { + d_cnfStream->ensureLiteral(atom); + SatLiteral lit = d_cnfStream->getLiteral(atom); + d_satSolver->addMarkerLiteral(lit); +} +bool Bitblaster::getPropagations(std::vector<TNode>& propagations) { + std::vector<SatLiteral> propagated_literals; + if (d_satSolver->getPropagations(propagated_literals)) { + for (unsigned i = 0; i < propagated_literals.size(); ++i) { + propagations.push_back(d_cnfStream->getNode(propagated_literals[i])); + } + return true; + } + return false; +} + +void Bitblaster::explainPropagation(TNode atom, std::vector<Node>& explanation) { + std::vector<SatLiteral> literal_explanation; + d_satSolver->explainPropagation(d_cnfStream->getLiteral(atom), literal_explanation); + for (unsigned i = 0; i < literal_explanation.size(); ++i) { + explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); + } +} + /** * Called from preregistration bitblasts the node * @@ -153,7 +218,7 @@ void Bitblaster::bitblast(TNode node) { * */ -void Bitblaster::assertToSat(TNode lit) { +bool Bitblaster::assertToSat(TNode lit, bool propagate) { // strip the not TNode atom; if (lit.getKind() == kind::NOT) { @@ -163,17 +228,22 @@ void Bitblaster::assertToSat(TNode lit) { } Assert (hasBBAtom(atom)); - Node rewr_atom = Rewriter::rewrite(atom); + SatLiteral markerLit = d_cnfStream->getLiteral(atom); if(lit.getKind() == kind::NOT) { markerLit = ~markerLit; } - Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; - Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; + BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; + BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; + + SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); d_assertedAtoms.push_back(markerLit); + + Assert(ret != prop::SAT_VALUE_UNKNOWN); + return ret == prop::SAT_VALUE_TRUE; } /** @@ -183,9 +253,9 @@ void Bitblaster::assertToSat(TNode lit) { * @return true for sat, and false for unsat */ -bool Bitblaster::solve() { - Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; - return SAT_VALUE_TRUE == d_satSolver->solve(d_assertedAtoms); +bool Bitblaster::solve(bool quick_solve) { + BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; + return SAT_VALUE_TRUE == d_satSolver->solve(); } void Bitblaster::getConflict(std::vector<TNode>& conflict) { @@ -287,11 +357,15 @@ void Bitblaster::getBBTerm(TNode node, Bits& bits) { Bitblaster::Statistics::Statistics() : d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0), - d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), + d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), + d_numTerms("theory::bv::NumberOfBitblastedTerms", 0), + d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), d_bitblastTimer("theory::bv::BitblastTimer") { StatisticsRegistry::registerStat(&d_numTermClauses); StatisticsRegistry::registerStat(&d_numAtomClauses); + StatisticsRegistry::registerStat(&d_numTerms); + StatisticsRegistry::registerStat(&d_numAtoms); StatisticsRegistry::registerStat(&d_bitblastTimer); } @@ -299,6 +373,8 @@ Bitblaster::Statistics::Statistics() : Bitblaster::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_numTermClauses); StatisticsRegistry::unregisterStat(&d_numAtomClauses); + StatisticsRegistry::unregisterStat(&d_numTerms); + StatisticsRegistry::unregisterStat(&d_numAtoms); StatisticsRegistry::unregisterStat(&d_bitblastTimer); } diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index c0f3b75ed..647e4fe9f 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -97,6 +97,8 @@ class Bitblaster { void initAtomBBStrategies(); void initTermBBStrategies(); + // returns a node that might be easier to bitblast + Node bbOptimize(TNode node); void bbAtom(TNode node); // division is bitblasted in terms of constraints @@ -110,17 +112,20 @@ public: public: Bitblaster(context::Context* c); ~Bitblaster(); - void assertToSat(TNode node); - bool solve(); + bool assertToSat(TNode node, bool propagate = true); + bool solve(bool quick_solve = false); void bitblast(TNode node); void getConflict(std::vector<TNode>& conflict); - + void addAtom(TNode atom); + bool getPropagations(std::vector<TNode>& propagations); + void explainPropagation(TNode atom, std::vector<Node>& explanation); private: class Statistics { public: - IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTerms, d_numAtoms; TimerStat d_bitblastTimer; Statistics(); ~Statistics(); diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 36d25de2a..6ef2cb0a9 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -28,16 +28,16 @@ constant CONST_BITVECTOR \ "a fixed-width bit-vector constant" operator BITVECTOR_CONCAT 2: "bit-vector concatenation" -operator BITVECTOR_AND 2 "bitwise and" -operator BITVECTOR_OR 2 "bitwise or" -operator BITVECTOR_XOR 2 "bitwise xor" +operator BITVECTOR_AND 2: "bitwise and" +operator BITVECTOR_OR 2: "bitwise or" +operator BITVECTOR_XOR 2: "bitwise xor" operator BITVECTOR_NOT 1 "bitwise not" operator BITVECTOR_NAND 2 "bitwise nand" operator BITVECTOR_NOR 2 "bitwise nor" operator BITVECTOR_XNOR 2 "bitwise xnor" operator BITVECTOR_COMP 2 "equality comparison (returns one bit)" -operator BITVECTOR_MULT 2 "bit-vector multiplication" -operator BITVECTOR_PLUS 2 "bit-vector addition" +operator BITVECTOR_MULT 2: "bit-vector multiplication" +operator BITVECTOR_PLUS 2: "bit-vector addition" operator BITVECTOR_SUB 2 "bit-vector subtraction" operator BITVECTOR_NEG 1 "bit-vector unary negation" operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 45d99f9c9..e8e1aead6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -32,12 +32,13 @@ using namespace std; using namespace CVC4::theory::bv::utils; TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) - : Theory(THEORY_BV, c, u, out, valuation), + : Theory(THEORY_BV, c, u, out, valuation), d_context(c), d_assertions(c), d_bitblaster(new Bitblaster(c) ), - d_statistics() - { + d_statistics(), + d_alreadyPropagatedSet(c) + { d_true = utils::mkTrue(); } TheoryBV::~TheoryBV() { @@ -61,35 +62,54 @@ TheoryBV::Statistics::~Statistics() { void TheoryBV::preRegisterTerm(TNode node) { BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - //marker literal: bitblast all terms before we start - //d_bitblaster->bitblast(node); + if (node.getKind() == kind::EQUAL || + node.getKind() == kind::BITVECTOR_ULT || + node.getKind() == kind::BITVECTOR_ULE || + node.getKind() == kind::BITVECTOR_SLT || + node.getKind() == kind::BITVECTOR_SLE) { + d_bitblaster->bitblast(node); + d_bitblaster->addAtom(node); + } } void TheoryBV::check(Effort e) { - if (fullEffort(e) && !done()) { - Trace("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; - std::vector<TNode> assertions; - + if (e == EFFORT_STANDARD) { + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; + BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; while (!done()) { TNode assertion = get(); - Trace("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; - d_bitblaster->bitblast(assertion); - d_bitblaster->assertToSat(assertion); + // make sure we do not assert things we propagated + if (!hasBeenPropagated(assertion)) { + BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n"; + bool ok = d_bitblaster->assertToSat(assertion, true); + if (!ok) { + std::vector<TNode> conflictAtoms; + d_bitblaster->getConflict(conflictAtoms); + d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); + Node conflict = mkConjunction(conflictAtoms); + d_out->conflict(conflict); + BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n "; + return; + } + } } + } - TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); - bool res = d_bitblaster->solve(); - if (res == false) { + if (e == EFFORT_FULL) { + BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; + // in standard effort we only do boolean constraint propagation + bool ok = d_bitblaster->solve(false); + if (!ok) { std::vector<TNode> conflictAtoms; d_bitblaster->getConflict(conflictAtoms); d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - Node conflict = mkConjunction(conflictAtoms); d_out->conflict(conflict); - Trace("bitvector") << "TheoryBV::check returns conflict. \n "; + BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n "; return; } } + } @@ -109,19 +129,56 @@ Node TheoryBV::getValue(TNode n) { } } -Node TheoryBV::explain(TNode node) { - BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; +bool TheoryBV::hasBeenPropagated(TNode node) { + return d_alreadyPropagatedSet.count(node); +} - TNode equality = node.getKind() == kind::NOT ? node[0] : node; - Assert(equality.getKind() == kind::EQUAL); - Assert(0); - return node; +void TheoryBV::propagate(Effort e) { + BVDebug("bitvector") << "TheoryBV::propagate() \n"; + + // get new propagations from the sat solver + std::vector<TNode> propagations; + d_bitblaster->getPropagations(propagations); + + // propagate the facts on the propagation queue + for (unsigned i = 0; i < propagations.size(); ++ i) { + TNode node = propagations[i]; + BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n"; + if (d_valuation.getSatValue(node) == Node::null()) { + vector<Node> explanation; + d_bitblaster->explainPropagation(node, explanation); + if (explanation.size() == 0) { + d_out->lemma(node); + } else { + NodeBuilder<> nb(kind::OR); + nb << node; + for (unsigned i = 0; i < explanation.size(); ++ i) { + nb << explanation[i].notNode(); + } + Node lemma = nb; + d_out->lemma(lemma); + } + d_alreadyPropagatedSet.insert(node); + } + } } -// Node TheoryBV::preprocessTerm(TNode term) { -// return term; //d_staticEqManager.find(term); -// } +Node TheoryBV::explain(TNode n) { + BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; + std::vector<Node> explanation; + d_bitblaster->explainPropagation(n, explanation); + Node exp; + + if (explanation.size() == 0) { + return utils::mkTrue(); + } + + exp = utils::mkAnd(explanation); + + BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; + return exp; +} Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 36ba17b52..d147c8bb5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,6 +24,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdlist.h" +#include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" @@ -41,7 +42,6 @@ class Bitblaster; class TheoryBV : public Theory { -public: private: @@ -54,7 +54,11 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; Node d_true; - + + /** Context dependent set of atoms we already propagated */ + context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; + + bool hasBeenPropagated(TNode node); public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); @@ -66,7 +70,7 @@ public: void check(Effort e); - void propagate(Effort e) { } + void propagate(Effort e); Node explain(TNode n); diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index b01a0646c..30437a76e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -87,7 +87,9 @@ enum RewriteRuleId { EvalRotateLeft, EvalRotateRight, EvalNeg, - + EvalSlt, + EvalSle, + /// simplification rules /// all of these rules decrease formula size ShlByConst, @@ -136,12 +138,26 @@ enum RewriteRuleId { ExtractArith, ExtractArith2, DoubleNeg, + NegMult, + NegSub, + NegPlus, NotConcat, NotAnd, // not sure why this would help (not done) NotOr, // not sure why this would help (not done) - NotXor // not sure why this would help (not done) + NotXor, // not sure why this would help (not done) + FlattenAssocCommut, + PlusCombineLikeTerms, + MultSimplify, + MultDistribConst, + AndSimplify, + OrSimplify, + XorSimplify, + + // rules to simplify bitblasting + BBPlusNeg }; + inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { switch (ruleId) { case EmptyRule: out << "EmptyRule"; return out; @@ -183,6 +199,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalAshr : out << "EvalAshr"; return out; case EvalUlt : out << "EvalUlt"; return out; case EvalUle : out << "EvalUle"; return out; + case EvalSlt : out << "EvalSlt"; return out; + case EvalSle : out << "EvalSle"; return out; case EvalExtract : out << "EvalExtract"; return out; case EvalSignExtend : out << "EvalSignExtend"; return out; case EvalRotateLeft : out << "EvalRotateLeft"; return out; @@ -241,6 +259,17 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case SignExtendEliminate : out << "SignExtendEliminate"; return out; case NotIdemp : out << "NotIdemp"; return out; case UleSelf: out << "UleSelf"; return out; + case FlattenAssocCommut: out << "FlattenAssocCommut"; return out; + case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out; + case MultSimplify: out << "MultSimplify"; return out; + case MultDistribConst: out << "MultDistribConst"; return out; + case NegMult : out << "NegMult"; return out; + case NegSub : out << "NegSub"; return out; + case AndSimplify : out << "AndSimplify"; return out; + case OrSimplify : out << "OrSimplify"; return out; + case XorSimplify : out << "XorSimplify"; return out; + case NegPlus : out << "NegPlus"; return out; + case BBPlusNeg : out << "BBPlusNeg"; return out; default: Unreachable(); } @@ -346,6 +375,8 @@ struct AllRewriteRules { RewriteRule<SgtEliminate> rule12; RewriteRule<UgeEliminate> rule13; RewriteRule<SgeEliminate> rule14; + RewriteRule<NegMult> rule15; + RewriteRule<NegSub> rule16; RewriteRule<RepeatEliminate> rule17; RewriteRule<RotateLeftEliminate> rule18; RewriteRule<RotateRightEliminate> rule19; @@ -359,8 +390,10 @@ struct AllRewriteRules { RewriteRule<EvalOr> rule27; RewriteRule<EvalXor> rule28; RewriteRule<EvalNot> rule29; + RewriteRule<EvalSlt> rule30; RewriteRule<EvalMult> rule31; RewriteRule<EvalPlus> rule32; + RewriteRule<XorSimplify> rule33; RewriteRule<EvalUdiv> rule34; RewriteRule<EvalUrem> rule35; RewriteRule<EvalShl> rule36; @@ -368,6 +401,7 @@ struct AllRewriteRules { RewriteRule<EvalAshr> rule38; RewriteRule<EvalUlt> rule39; RewriteRule<EvalUle> rule40; + RewriteRule<EvalSle> rule41; RewriteRule<EvalExtract> rule43; RewriteRule<EvalSignExtend> rule44; RewriteRule<EvalRotateLeft> rule45; @@ -428,14 +462,22 @@ struct AllRewriteRules { RewriteRule<SignExtendEliminate> rule101; RewriteRule<NotIdemp> rule102; RewriteRule<UleSelf> rule103; + RewriteRule<FlattenAssocCommut> rule104; + RewriteRule<PlusCombineLikeTerms> rule105; + RewriteRule<MultSimplify> rule106; + RewriteRule<MultDistribConst> rule107; + RewriteRule<AndSimplify> rule108; + RewriteRule<OrSimplify> rule109; + RewriteRule<NegPlus> rule110; + RewriteRule<BBPlusNeg> rule111; }; -template<> +template<> inline bool RewriteRule<EmptyRule>::applies(Node node) { return false; } -template<> +template<> inline Node RewriteRule<EmptyRule>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EmptyRule> for " << node.getKind() <<"\n"; Unreachable(); diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 1dc053b5d..da3ef4485 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -28,13 +28,13 @@ namespace CVC4 { namespace theory { namespace bv { -template<> +template<> inline bool RewriteRule<EvalAnd>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_AND && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalAnd>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -44,13 +44,13 @@ Node RewriteRule<EvalAnd>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalOr>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_OR && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalOr>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -60,13 +60,13 @@ Node RewriteRule<EvalOr>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalXor>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_XOR && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalXor>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -76,13 +76,13 @@ Node RewriteRule<EvalXor>::apply(Node node) { return utils::mkConst(res); } -// template<> +// template<> inline // bool RewriteRule<EvalXnor>::applies(Node node) { // return (node.getKind() == kind::BITVECTOR_XNOR && // utils::isBVGroundTerm(node)); // } -// template<> +// template<> inline // Node RewriteRule<EvalXnor>::apply(Node node) { // BVDebug("bv-rewrite") << "RewriteRule<EvalXnor>(" << node << ")" << std::endl; // BitVector a = node[0].getConst<BitVector>(); @@ -91,13 +91,13 @@ Node RewriteRule<EvalXor>::apply(Node node) { // return utils::mkConst(res); // } -template<> +template<> inline bool RewriteRule<EvalNot>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_NOT && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalNot>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -105,13 +105,13 @@ Node RewriteRule<EvalNot>::apply(Node node) { return utils::mkConst(res); } -// template<> +// template<> inline // bool RewriteRule<EvalComp>::applies(Node node) { // return (node.getKind() == kind::BITVECTOR_COMP && // utils::isBVGroundTerm(node)); // } -// template<> +// template<> inline // Node RewriteRule<EvalComp>::apply(Node node) { // BVDebug("bv-rewrite") << "RewriteRule<EvalComp>(" << node << ")" << std::endl; // BitVector a = node[0].getConst<BitVector>(); @@ -126,13 +126,13 @@ Node RewriteRule<EvalNot>::apply(Node node) { // return utils::mkConst(res); // } -template<> +template<> inline bool RewriteRule<EvalMult>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_MULT && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalMult>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -142,13 +142,13 @@ Node RewriteRule<EvalMult>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalPlus>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_PLUS && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalPlus>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -158,13 +158,13 @@ Node RewriteRule<EvalPlus>::apply(Node node) { return utils::mkConst(res); } -// template<> +// template<> inline // bool RewriteRule<EvalSub>::applies(Node node) { // return (node.getKind() == kind::BITVECTOR_SUB && // utils::isBVGroundTerm(node)); // } -// template<> +// template<> inline // Node RewriteRule<EvalSub>::apply(Node node) { // BVDebug("bv-rewrite") << "RewriteRule<EvalSub>(" << node << ")" << std::endl; // BitVector a = node[0].getConst<BitVector>(); @@ -173,13 +173,13 @@ Node RewriteRule<EvalPlus>::apply(Node node) { // return utils::mkConst(res); // } -template<> +template<> inline bool RewriteRule<EvalNeg>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_NEG && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalNeg>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalNeg>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -187,13 +187,13 @@ Node RewriteRule<EvalNeg>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalUdiv>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UDIV && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalUdiv>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -202,13 +202,13 @@ Node RewriteRule<EvalUdiv>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalUrem>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UREM && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalUrem>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -217,13 +217,13 @@ Node RewriteRule<EvalUrem>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalShl>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_SHL && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalShl>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalShl>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -233,13 +233,13 @@ Node RewriteRule<EvalShl>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalLshr>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_LSHR && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalLshr>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalLshr>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -249,13 +249,13 @@ Node RewriteRule<EvalLshr>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalAshr>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ASHR && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalAshr>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalAshr>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -265,13 +265,13 @@ Node RewriteRule<EvalAshr>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalUlt>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULT && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalUlt>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalUlt>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -283,32 +283,32 @@ Node RewriteRule<EvalUlt>::apply(Node node) { return utils::mkFalse(); } -// template<> -// bool RewriteRule<EvalSlt>::applies(Node node) { -// return (node.getKind() == kind::BITVECTOR_SLT && -// utils::isBVGroundTerm(node)); -// } +template<> inline +bool RewriteRule<EvalSlt>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SLT && + utils::isBVGroundTerm(node)); +} -// template<> -// Node RewriteRule<EvalSlt>::apply(Node node) { -// BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl; -// BitVector a = node[0].getConst<BitVector>(); -// BitVector b = node[1].getConst<BitVector>(); +template<> inline +Node RewriteRule<EvalSlt>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<EvalSlt>(" << node << ")" << std::endl; + BitVector a = node[0].getConst<BitVector>(); + BitVector b = node[1].getConst<BitVector>(); -// if (a.signedLessThan(b)) { -// return utils::mkTrue(); -// } -// return utils::mkFalse(); + if (a.signedLessThan(b)) { + return utils::mkTrue(); + } + return utils::mkFalse(); -// } +} -template<> +template<> inline bool RewriteRule<EvalUle>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULE && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalUle>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalUle>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -320,31 +320,31 @@ Node RewriteRule<EvalUle>::apply(Node node) { return utils::mkFalse(); } -// template<> -// bool RewriteRule<EvalSle>::applies(Node node) { -// return (node.getKind() == kind::BITVECTOR_SLE && -// utils::isBVGroundTerm(node)); -// } +template<> inline +bool RewriteRule<EvalSle>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SLE && + utils::isBVGroundTerm(node)); +} -// template<> -// Node RewriteRule<EvalSle>::apply(Node node) { -// BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl; -// BitVector a = node[0].getConst<BitVector>(); -// BitVector b = node[1].getConst<BitVector>(); +template<> inline +Node RewriteRule<EvalSle>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<EvalSle>(" << node << ")" << std::endl; + BitVector a = node[0].getConst<BitVector>(); + BitVector b = node[1].getConst<BitVector>(); -// if (a.signedLessThanEq(b)) { -// return utils::mkTrue(); -// } -// return utils::mkFalse(); -// } + if (a.signedLessThanEq(b)) { + return utils::mkTrue(); + } + return utils::mkFalse(); +} -template<> +template<> inline bool RewriteRule<EvalExtract>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_EXTRACT && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalExtract>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalExtract>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -356,13 +356,13 @@ Node RewriteRule<EvalExtract>::apply(Node node) { } -template<> +template<> inline bool RewriteRule<EvalConcat>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_CONCAT && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalConcat>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalConcat>(" << node << ")" << std::endl; unsigned num = node.getNumChildren(); @@ -374,13 +374,13 @@ Node RewriteRule<EvalConcat>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalSignExtend>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalSignExtend>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalSignExtend>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); @@ -390,13 +390,13 @@ Node RewriteRule<EvalSignExtend>::apply(Node node) { return utils::mkConst(res); } -template<> +template<> inline bool RewriteRule<EvalEquals>::applies(Node node) { return (node.getKind() == kind::EQUAL && utils::isBVGroundTerm(node)); } -template<> +template<> inline Node RewriteRule<EvalEquals>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<EvalEquals>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 3240ef5f3..f3d28072e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -28,12 +28,12 @@ namespace CVC4 { namespace theory { namespace bv { -template<> +template<> inline bool RewriteRule<ConcatFlatten>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_CONCAT); } -template<> +template<> inline Node RewriteRule<ConcatFlatten>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl; NodeBuilder<> result(kind::BITVECTOR_CONCAT); @@ -54,12 +54,12 @@ Node RewriteRule<ConcatFlatten>::apply(Node node) { return resultNode; } -template<> +template<> inline bool RewriteRule<ConcatExtractMerge>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_CONCAT); } -template<> +template<> inline Node RewriteRule<ConcatExtractMerge>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl; @@ -115,12 +115,12 @@ Node RewriteRule<ConcatExtractMerge>::apply(Node node) { return utils::mkConcat(mergedExtracts); } -template<> +template<> inline bool RewriteRule<ConcatConstantMerge>::applies(Node node) { return node.getKind() == kind::BITVECTOR_CONCAT; } -template<> +template<> inline Node RewriteRule<ConcatConstantMerge>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl; @@ -157,7 +157,7 @@ Node RewriteRule<ConcatConstantMerge>::apply(Node node) { return utils::mkConcat(mergedConstants); } -template<> +template<> inline bool RewriteRule<ExtractWhole>::applies(Node node) { if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; unsigned length = utils::getSize(node[0]); @@ -168,20 +168,20 @@ bool RewriteRule<ExtractWhole>::applies(Node node) { return true; } -template<> +template<> inline Node RewriteRule<ExtractWhole>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl; return node[0]; } -template<> +template<> inline bool RewriteRule<ExtractConstant>::applies(Node node) { if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; if (node[0].getKind() != kind::CONST_BITVECTOR) return false; return true; } -template<> +template<> inline Node RewriteRule<ExtractConstant>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl; Node child = node[0]; @@ -189,7 +189,7 @@ Node RewriteRule<ExtractConstant>::apply(Node node) { return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node))); } -template<> +template<> inline bool RewriteRule<ExtractConcat>::applies(Node node) { //BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl; if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; @@ -197,7 +197,7 @@ bool RewriteRule<ExtractConcat>::applies(Node node) { return true; } -template<> +template<> inline Node RewriteRule<ExtractConcat>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl; int extract_high = utils::getExtractHigh(node); @@ -223,14 +223,14 @@ Node RewriteRule<ExtractConcat>::apply(Node node) { return utils::mkConcat(resultChildren); } -template<> +template<> inline bool RewriteRule<ExtractExtract>::applies(Node node) { if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false; return true; } -template<> +template<> inline Node RewriteRule<ExtractExtract>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl; @@ -244,7 +244,7 @@ Node RewriteRule<ExtractExtract>::apply(Node node) { return result; } -template<> +template<> inline bool RewriteRule<FailEq>::applies(Node node) { //BVDebug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl; if (node.getKind() != kind::EQUAL) return false; @@ -253,29 +253,29 @@ bool RewriteRule<FailEq>::applies(Node node) { return node[0] != node[1]; } -template<> +template<> inline Node RewriteRule<FailEq>::apply(Node node) { return utils::mkFalse(); } -template<> +template<> inline bool RewriteRule<SimplifyEq>::applies(Node node) { if (node.getKind() != kind::EQUAL) return false; return node[0] == node[1]; } -template<> +template<> inline Node RewriteRule<SimplifyEq>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl; return utils::mkTrue(); } -template<> +template<> inline bool RewriteRule<ReflexivityEq>::applies(Node node) { return (node.getKind() == kind::EQUAL && node[0] < node[1]); } -template<> +template<> inline Node RewriteRule<ReflexivityEq>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl; return node[1].eqNode(node[0]); diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4e974881c..5587e25eb 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -33,7 +33,7 @@ namespace bv { * (x bvop y) [i:j] ==> x[i:j] bvop y[i:j] * where bvop is bvand,bvor, bvxor */ -template<> +template<> inline bool RewriteRule<ExtractBitwise>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_EXTRACT && (node[0].getKind() == kind::BITVECTOR_AND || @@ -41,7 +41,7 @@ bool RewriteRule<ExtractBitwise>::applies(Node node) { node[0].getKind() == kind::BITVECTOR_XOR )); } -template<> +template<> inline Node RewriteRule<ExtractBitwise>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractBitwise>(" << node << ")" << std::endl; unsigned high = utils::getExtractHigh(node); @@ -57,13 +57,13 @@ Node RewriteRule<ExtractBitwise>::apply(Node node) { * * (~ a) [i:j] ==> ~ (a[i:j]) */ -template<> +template<> inline bool RewriteRule<ExtractNot>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_EXTRACT && node[0].getKind() == kind::BITVECTOR_NOT); } -template<> +template<> inline Node RewriteRule<ExtractNot>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractNot>(" << node << ")" << std::endl; unsigned low = utils::getExtractLow(node); @@ -78,7 +78,7 @@ Node RewriteRule<ExtractNot>::apply(Node node) { * (a bvop b) [k:0] ==> (a[k:0] bvop b[k:0]) */ -template<> +template<> inline bool RewriteRule<ExtractArith>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_EXTRACT && utils::getExtractLow(node) == 0 && @@ -86,7 +86,7 @@ bool RewriteRule<ExtractArith>::applies(Node node) { node[0].getKind() == kind::BITVECTOR_MULT)); } -template<> +template<> inline Node RewriteRule<ExtractArith>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractArith>(" << node << ")" << std::endl; unsigned low = utils::getExtractLow(node); @@ -107,14 +107,14 @@ Node RewriteRule<ExtractArith>::apply(Node node) { */ // careful not to apply in a loop -template<> +template<> inline bool RewriteRule<ExtractArith2>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_EXTRACT && (node[0].getKind() == kind::BITVECTOR_PLUS || node[0].getKind() == kind::BITVECTOR_MULT)); } -template<> +template<> inline Node RewriteRule<ExtractArith2>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ExtractArith2>(" << node << ")" << std::endl; unsigned low = utils::getExtractLow(node); @@ -128,13 +128,570 @@ Node RewriteRule<ExtractArith2>::apply(Node node) { return utils::mkExtract(a_op_b, high, low); } +template<> inline +bool RewriteRule<FlattenAssocCommut>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_PLUS || + node.getKind() == kind::BITVECTOR_MULT || + node.getKind() == kind::BITVECTOR_OR || + node.getKind() == kind::BITVECTOR_XOR || + node.getKind() == kind::BITVECTOR_AND); +} + + +template<> inline +Node RewriteRule<FlattenAssocCommut>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; + std::vector<Node> processingStack; + processingStack.push_back(node); + std::vector<Node> children; + Kind kind = node.getKind(); + + while (! processingStack.empty()) { + TNode current = processingStack.back(); + processingStack.pop_back(); + + // flatten expression + if (current.getKind() == kind) { + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + processingStack.push_back(current[i]); + } + } else { + children.push_back(current); + } + } + return utils::mkSortedNode(kind, children); +} + +static inline void addToCoefMap(std::map<Node, BitVector>& map, + TNode term, const BitVector& coef) { + if (map.find(term) != map.end()) { + map[term] = map[term] + coef; + } else { + map[term] = coef; + } +} + + +template<> inline +bool RewriteRule<PlusCombineLikeTerms>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_PLUS); +} + +template<> inline +Node RewriteRule<PlusCombineLikeTerms>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<PlusCombineLikeTerms>(" << node << ")" << std::endl; + unsigned size = utils::getSize(node); + BitVector constSum(size, (unsigned)0); + std::map<Node, BitVector> factorToCoefficient; + + // combine like-terms + for(unsigned i= 0; i < node.getNumChildren(); ++i) { + TNode current = node[i]; + + // look for c * x, where c is a constant + if (current.getKind() == kind::BITVECTOR_MULT && + (current[0].getKind() == kind::CONST_BITVECTOR || + current[1].getKind() == kind::CONST_BITVECTOR)) { + // if we are multiplying by a constant + BitVector coeff; + TNode term; + // figure out which part is the constant + if (current[0].getKind() == kind::CONST_BITVECTOR) { + coeff = current[0].getConst<BitVector>(); + term = current[1]; + } else { + coeff = current[1].getConst<BitVector>(); + term = current[0]; + } + if(term.getKind() == kind::BITVECTOR_SUB) { + TNode a = term[0]; + TNode b = term[1]; + addToCoefMap(factorToCoefficient, a, coeff); + addToCoefMap(factorToCoefficient, b, -coeff); + } + else if(term.getKind() == kind::BITVECTOR_NEG) { + addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff)); + } + else { + addToCoefMap(factorToCoefficient, term, coeff); + } + } + else if (current.getKind() == kind::BITVECTOR_SUB) { + // turn into a + (-1)*b + addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); + addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); + } + else if (current.getKind() == kind::BITVECTOR_NEG) { + addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1)); + } + else if (current.getKind() == kind::CONST_BITVECTOR) { + BitVector constValue = current.getConst<BitVector>(); + constSum = constSum + constValue; + } + else { + // store as 1 * current + addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1)); + } + } + + std::vector<Node> children; + if ( constSum!= BitVector(size, (unsigned)0)) { + children.push_back(utils::mkConst(constSum)); + } + + // construct result + std::map<Node, BitVector>::const_iterator it = factorToCoefficient.begin(); + + for (; it != factorToCoefficient.end(); ++it) { + BitVector bv_coeff = it->second; + TNode term = it->first; + if(bv_coeff == BitVector(size, (unsigned)0)) { + continue; + } + else if (bv_coeff == BitVector(size, (unsigned)1)) { + children.push_back(term); + } + else if (bv_coeff == -BitVector(size, (unsigned)1)) { + // avoid introducing an extra multiplication + children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term)); + } + else { + Node coeff = utils::mkConst(bv_coeff); + Node product = utils::mkSortedNode(kind::BITVECTOR_MULT, coeff, term); + children.push_back(product); + } + } + + if(children.size() == 0) { + return utils::mkConst(size, (unsigned)0); + } + + return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); +} + + +template<> inline +bool RewriteRule<MultSimplify>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_MULT); +} + +template<> inline +Node RewriteRule<MultSimplify>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<MultSimplify>(" << node << ")" << std::endl; + unsigned size = utils::getSize(node); + BitVector constant(size, Integer(1)); + + std::vector<Node> children; + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + TNode current = node[i]; + if (current.getKind() == kind::CONST_BITVECTOR) { + BitVector value = current.getConst<BitVector>(); + if(value == BitVector(size, (unsigned) 0)) { + return utils::mkConst(size, 0); + } + constant = constant * current.getConst<BitVector>(); + } else { + children.push_back(current); + } + } + + + if(constant != BitVector(size, (unsigned)1)) { + children.push_back(utils::mkConst(constant)); + } + + + if(children.size() == 0) { + return utils::mkConst(size, (unsigned)1); + } + + return utils::mkSortedNode(kind::BITVECTOR_MULT, children); +} + +template<> inline +bool RewriteRule<MultDistribConst>::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_MULT) + return false; + + TNode factor; + if (node[0].getKind() == kind::CONST_BITVECTOR) { + factor = node[1]; + } else if (node[1].getKind() == kind::CONST_BITVECTOR) { + factor = node[0]; + } else { + return false; + } + + return (factor.getKind() == kind::BITVECTOR_PLUS || + factor.getKind() == kind::BITVECTOR_SUB || + factor.getKind() == kind::BITVECTOR_NEG); +} + +template<> inline +Node RewriteRule<MultDistribConst>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl; + + TNode constant; + TNode factor; + if (node[0].getKind() == kind::CONST_BITVECTOR) { + constant = node[0]; + factor = node[1]; + } else { + Assert(node[1].getKind() == kind::CONST_BITVECTOR); + constant = node[1]; + factor = node[0]; + } + + if (factor.getKind() == kind::BITVECTOR_NEG) { + // push negation on the constant part + BitVector const_bv = constant.getConst<BitVector>(); + return utils::mkSortedNode(kind::BITVECTOR_MULT, + utils::mkConst(-const_bv), + factor[0]); + } + + std::vector<Node> children; + for(unsigned i = 0; i < factor.getNumChildren(); ++i) { + children.push_back(utils::mkSortedNode(kind::BITVECTOR_MULT, constant, factor[i])); + } + + return utils::mkSortedNode(factor.getKind(), children); + +} + + +/** + * -(c * expr) ==> (-c * expr) + * where c is a constant + */ +template<> inline +bool RewriteRule<NegMult>::applies(Node node) { + if(node.getKind()!= kind::BITVECTOR_NEG || + node[0].getKind() != kind::BITVECTOR_MULT) { + return false; + } + TNode mult = node[0]; + for (unsigned i = 0; i < mult.getNumChildren(); ++i) { + if (mult[i].getKind() == kind::CONST_BITVECTOR) { + return true; + } + } + return false; +} + +template<> inline +Node RewriteRule<NegMult>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl; + TNode mult = node[0]; + std::vector<Node> children; + bool has_const = false; + for(unsigned i = 0; i < mult.getNumChildren(); ++i) { + if(mult[i].getKind() == kind::CONST_BITVECTOR) { + Assert(has_const == false); + has_const = true; + BitVector bv = mult[i].getConst<BitVector>(); + children.push_back(utils::mkConst(-bv)); + } else { + children.push_back(mult[i]); + } + } + Assert (has_const); + return utils::mkSortedNode(kind::BITVECTOR_MULT, children); +} + +template<> inline +bool RewriteRule<NegSub>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_NEG && + node[0].getKind() == kind::BITVECTOR_SUB); +} + +template<> inline +Node RewriteRule<NegSub>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<NegSub>(" << node << ")" << std::endl; + return utils::mkNode(kind::BITVECTOR_SUB, node[0][1], node[0][0]); +} + +template<> inline +bool RewriteRule<NegPlus>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_NEG && + node[0].getKind() == kind::BITVECTOR_PLUS); +} + +template<> inline +Node RewriteRule<NegPlus>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<NegPlus>(" << node << ")" << std::endl; + std::vector<Node> children; + for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { + children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i])); + } + return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); +} + + + + +struct Count { + unsigned pos; + unsigned neg; + Count() : pos(0), neg(0) {} + Count(unsigned p, unsigned n): + pos(p), + neg(n) + {} +}; + +inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { + if(map.find(node) == map.end()) { + Count c = neg? Count(0,1) : Count(1, 0); + map[node] = c; + } else { + if (neg) { + ++(map[node].neg); + } else { + ++(map[node].pos); + } + } +} + +template<> inline +bool RewriteRule<AndSimplify>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_AND); +} + +template<> inline +Node RewriteRule<AndSimplify>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; + + // this will remove duplicates + std::hash_map<TNode, Count, TNodeHashFunction> subterms; + unsigned size = utils::getSize(node); + BitVector constant = utils::mkBitVectorOnes(size); + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + TNode current = node[i]; + // simplify constants + if (current.getKind() == kind::CONST_BITVECTOR) { + BitVector bv = current.getConst<BitVector>(); + constant = constant & bv; + } else { + if (current.getKind() == kind::BITVECTOR_NOT) { + insert(subterms, current[0], true); + } else { + insert(subterms, current, false); + } + } + } + + std::vector<Node> children; + + if (constant == BitVector(size, (unsigned)0)) { + return utils::mkConst(BitVector(size, (unsigned)0)); + } + + if (constant != utils::mkBitVectorOnes(size)) { + children.push_back(utils::mkConst(constant)); + } + + std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + + for (; it != subterms.end(); ++it) { + if (it->second.pos > 0 && it->second.neg > 0) { + // if we have a and ~a + return utils::mkConst(BitVector(size, (unsigned)0)); + } else { + // idempotence + if (it->second.neg > 0) { + // if it only occured negated + children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); + } else { + // if it only occured positive + children.push_back(it->first); + } + } + } + if (children.size() == 0) { + return utils::mkOnes(size); + } + + return utils::mkSortedNode(kind::BITVECTOR_AND, children); +} + +template<> inline +bool RewriteRule<OrSimplify>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_OR); +} + +template<> inline +Node RewriteRule<OrSimplify>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl; + + // this will remove duplicates + std::hash_map<TNode, Count, TNodeHashFunction> subterms; + unsigned size = utils::getSize(node); + BitVector constant(size, (unsigned)0); + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + TNode current = node[i]; + // simplify constants + if (current.getKind() == kind::CONST_BITVECTOR) { + BitVector bv = current.getConst<BitVector>(); + constant = constant | bv; + } else { + if (current.getKind() == kind::BITVECTOR_NOT) { + insert(subterms, current[0], true); + } else { + insert(subterms, current, false); + } + } + } + + std::vector<Node> children; + + if (constant == utils::mkBitVectorOnes(size)) { + return utils::mkOnes(size); + } + + if (constant != BitVector(size, (unsigned)0)) { + children.push_back(utils::mkConst(constant)); + } + + std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + + for (; it != subterms.end(); ++it) { + if (it->second.pos > 0 && it->second.neg > 0) { + // if we have a or ~a + return utils::mkOnes(size); + } else { + // idempotence + if (it->second.neg > 0) { + // if it only occured negated + children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); + } else { + // if it only occured positive + children.push_back(it->first); + } + } + } + + if (children.size() == 0) { + return utils::mkConst(BitVector(size, (unsigned)0)); + } + return utils::mkSortedNode(kind::BITVECTOR_OR, children); +} + +template<> inline +bool RewriteRule<XorSimplify>::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_XOR); +} + +template<> inline +Node RewriteRule<XorSimplify>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl; + + + std::hash_map<TNode, Count, TNodeHashFunction> subterms; + unsigned size = utils::getSize(node); + BitVector constant; + bool const_set = false; + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + TNode current = node[i]; + // simplify constants + if (current.getKind() == kind::CONST_BITVECTOR) { + BitVector bv = current.getConst<BitVector>(); + if (const_set) { + constant = constant ^ bv; + } else { + const_set = true; + constant = bv; + } + } else { + // collect number of occurances of each term and its negation + if (current.getKind() == kind::BITVECTOR_NOT) { + insert(subterms, current[0], true); + } else { + insert(subterms, current, false); + } + } + } + + std::vector<Node> children; + + std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + unsigned true_count = 0; + bool seen_false = false; + for (; it != subterms.end(); ++it) { + unsigned pos = it->second.pos; // number of positive occurances + unsigned neg = it->second.neg; // number of negated occurances + + // remove duplicates using the following rules + // a xor a ==> false + // false xor false ==> false + seen_false = seen_false? seen_false : (pos > 1 || neg > 1); + // check what did not reduce + if (pos % 2 && neg % 2) { + // we have a xor ~a ==> true + ++true_count; + } else if (pos % 2) { + // we had a positive occurence left + children.push_back(it->first); + } else if (neg % 2) { + // we had a negative occurence left + children.push_back(utils::mkNode(kind::BITVECTOR_NOT, it->first)); + } + // otherwise both reduced to false + } + + std::vector<BitVector> xorConst; + BitVector true_bv = utils::mkBitVectorOnes(size); + BitVector false_bv(size, (unsigned)0); + + if (true_count) { + // true xor ... xor true ==> true (odd) + // ==> false (even) + xorConst.push_back(true_count % 2? true_bv : false_bv); + } + if (seen_false) { + xorConst.push_back(false_bv); + } + if(const_set) { + xorConst.push_back(constant); + } + + if (xorConst.size() > 0) { + BitVector result = xorConst[0]; + for (unsigned i = 1; i < xorConst.size(); ++i) { + result = result ^ xorConst[i]; + } + children.push_back(utils::mkConst(result)); + } + + Assert(children.size()); + + return utils::mkSortedNode(kind::BITVECTOR_XOR, children); +} + + + + +// template<> inline +// bool RewriteRule<AndSimplify>::applies(Node node) { +// return (node.getKind() == kind::BITVECTOR_AND); +// } + +// template<> inline +// Node RewriteRule<AndSimplify>::apply(Node node) { +// BVDebug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; +// return resultNode; +// } + -// template<> +// template<> inline // bool RewriteRule<>::applies(Node node) { // return (node.getKind() == kind::BITVECTOR_CONCAT); // } -// template<> +// template<> inline // Node RewriteRule<>::apply(Node node) { // BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl; // return resultNode; diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 507f98c91..cf8310e5a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -36,14 +36,14 @@ namespace bv { * * Left Shift by constant amount */ -template<> +template<> inline bool RewriteRule<ShlByConst>::applies(Node node) { // if the shift amount is constant return (node.getKind() == kind::BITVECTOR_SHL && node[1].getKind() == kind::CONST_BITVECTOR); } -template<> +template<> inline Node RewriteRule<ShlByConst>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); @@ -72,14 +72,14 @@ Node RewriteRule<ShlByConst>::apply(Node node) { * Right Logical Shift by constant amount */ -template<> +template<> inline bool RewriteRule<LshrByConst>::applies(Node node) { // if the shift amount is constant return (node.getKind() == kind::BITVECTOR_LSHR && node[1].getKind() == kind::CONST_BITVECTOR); } -template<> +template<> inline Node RewriteRule<LshrByConst>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); @@ -108,14 +108,14 @@ Node RewriteRule<LshrByConst>::apply(Node node) { * Right Arithmetic Shift by constant amount */ -template<> +template<> inline bool RewriteRule<AshrByConst>::applies(Node node) { // if the shift amount is constant return (node.getKind() == kind::BITVECTOR_ASHR && node[1].getKind() == kind::CONST_BITVECTOR); } -template<> +template<> inline Node RewriteRule<AshrByConst>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); @@ -150,14 +150,14 @@ Node RewriteRule<AshrByConst>::apply(Node node) { * (a bvor a) ==> a */ -template<> +template<> inline bool RewriteRule<BitwiseIdemp>::applies(Node node) { return ((node.getKind() == kind::BITVECTOR_AND || node.getKind() == kind::BITVECTOR_OR) && node[0] == node[1]); } -template<> +template<> inline Node RewriteRule<BitwiseIdemp>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl; return node[0]; @@ -169,7 +169,7 @@ Node RewriteRule<BitwiseIdemp>::apply(Node node) { * (a bvand 0) ==> 0 */ -template<> +template<> inline bool RewriteRule<AndZero>::applies(Node node) { unsigned size = utils::getSize(node); return (node.getKind() == kind::BITVECTOR_AND && @@ -177,7 +177,7 @@ bool RewriteRule<AndZero>::applies(Node node) { node[1] == utils::mkConst(size, 0))); } -template<> +template<> inline Node RewriteRule<AndZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 0); @@ -189,7 +189,7 @@ Node RewriteRule<AndZero>::apply(Node node) { * (a bvand 1) ==> a */ -template<> +template<> inline bool RewriteRule<AndOne>::applies(Node node) { unsigned size = utils::getSize(node); Node ones = utils::mkOnes(size); @@ -198,7 +198,7 @@ bool RewriteRule<AndOne>::applies(Node node) { node[1] == ones)); } -template<> +template<> inline Node RewriteRule<AndOne>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl; unsigned size = utils::getSize(node); @@ -217,7 +217,7 @@ Node RewriteRule<AndOne>::apply(Node node) { * (a bvor 0) ==> a */ -template<> +template<> inline bool RewriteRule<OrZero>::applies(Node node) { unsigned size = utils::getSize(node); return (node.getKind() == kind::BITVECTOR_OR && @@ -225,7 +225,7 @@ bool RewriteRule<OrZero>::applies(Node node) { node[1] == utils::mkConst(size, 0))); } -template<> +template<> inline Node RewriteRule<OrZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl; @@ -244,7 +244,7 @@ Node RewriteRule<OrZero>::apply(Node node) { * (a bvor 1) ==> 1 */ -template<> +template<> inline bool RewriteRule<OrOne>::applies(Node node) { unsigned size = utils::getSize(node); Node ones = utils::mkOnes(size); @@ -253,7 +253,7 @@ bool RewriteRule<OrOne>::applies(Node node) { node[1] == ones)); } -template<> +template<> inline Node RewriteRule<OrOne>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl; return utils::mkOnes(utils::getSize(node)); @@ -266,13 +266,13 @@ Node RewriteRule<OrOne>::apply(Node node) { * (a bvxor a) ==> 0 */ -template<> +template<> inline bool RewriteRule<XorDuplicate>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_XOR && node[0] == node[1]); } -template<> +template<> inline Node RewriteRule<XorDuplicate>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl; return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); @@ -284,27 +284,39 @@ Node RewriteRule<XorDuplicate>::apply(Node node) { * (a bvxor 1) ==> ~a */ -template<> +template<> inline bool RewriteRule<XorOne>::applies(Node node) { - Node ones = utils::mkOnes(utils::getSize(node)); - return (node.getKind() == kind::BITVECTOR_XOR && - (node[0] == ones || - node[1] == ones)); + if (node.getKind() != kind::BITVECTOR_XOR) { + return false; + } + Node ones = utils::mkOnes(utils::getSize(node)); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i] == ones) { + return true; + } + } + return false; } -template<> +template<> inline Node RewriteRule<XorOne>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorOne>(" << node << ")" << std::endl; Node ones = utils::mkOnes(utils::getSize(node)); - Node a; - if (node[0] == ones) { - a = node[1]; - } else { - Assert(node[1] == ones); - a = node[0]; + std::vector<Node> children; + bool found_ones = false; + // XorSimplify should have been called before + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i] == ones) { + // make sure only ones occurs only once + Assert(!found_ones); + found_ones = true; + } else { + children.push_back(node[i]); + } } - return utils::mkNode(kind::BITVECTOR_NOT, a); + children[0] = utils::mkNode(kind::BITVECTOR_NOT, children[0]); + return utils::mkSortedNode(kind::BITVECTOR_XOR, children); } @@ -314,24 +326,39 @@ Node RewriteRule<XorOne>::apply(Node node) { * (a bvxor 0) ==> a */ -template<> +template<> inline bool RewriteRule<XorZero>::applies(Node node) { - Node zero = utils::mkConst(utils::getSize(node), 0); - return (node.getKind() == kind::BITVECTOR_XOR && - (node[0] == zero || - node[1] == zero)); + if (node.getKind() != kind::BITVECTOR_XOR) { + return false; + } + Node zero = utils::mkConst(utils::getSize(node), 0); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i] == zero) { + return true; + } + } + return false; } -template<> +template<> inline Node RewriteRule<XorZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl; - Node zero = utils::mkConst(utils::getSize(node), 0); - if (node[0] == zero) { - return node[1]; + std::vector<Node> children; + bool found_zero = false; + Node zero = utils::mkConst(utils::getSize(node), 0); + + // XorSimplify should have been called before + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i] == zero) { + // make sure zero occurs only once + Assert(!found_zero); + found_zero = true; + } else { + children.push_back(node[i]); + } } - - Assert(node[1] == zero); - return node[0]; + + return utils::mkNode(kind::BITVECTOR_XOR, children); } @@ -341,14 +368,14 @@ Node RewriteRule<XorZero>::apply(Node node) { * (a bvand (~ a)) ==> 0 */ -template<> +template<> inline bool RewriteRule<BitwiseNotAnd>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_AND && ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) || (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); } -template<> +template<> inline Node RewriteRule<BitwiseNotAnd>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl; return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); @@ -360,14 +387,14 @@ Node RewriteRule<BitwiseNotAnd>::apply(Node node) { * (a bvor (~ a)) ==> 1 */ -template<> +template<> inline bool RewriteRule<BitwiseNotOr>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_OR && ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) || (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); } -template<> +template<> inline Node RewriteRule<BitwiseNotOr>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl; uint32_t size = utils::getSize(node); @@ -381,14 +408,14 @@ Node RewriteRule<BitwiseNotOr>::apply(Node node) { * ((~ a) bvxor (~ b)) ==> (a bvxor b) */ -template<> +template<> inline bool RewriteRule<XorNot>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_XOR && node[0].getKind() == kind::BITVECTOR_NOT && node[1].getKind() == kind::BITVECTOR_NOT); } -template<> +template<> inline Node RewriteRule<XorNot>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl; Node a = node[0][0]; @@ -402,19 +429,19 @@ Node RewriteRule<XorNot>::apply(Node node) { * ~(a bvxor b) ==> (~ a bvxor b) */ -template<> +template<> inline bool RewriteRule<NotXor>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_NOT && node[0].getKind() == kind::BITVECTOR_XOR); } -template<> +template<> inline Node RewriteRule<NotXor>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl; Node a = node[0][0]; Node b = node[0][1]; Node nota = utils::mkNode(kind::BITVECTOR_NOT, a); - return utils::mkNode(kind::BITVECTOR_XOR, nota, b); + return utils::mkSortedNode(kind::BITVECTOR_XOR, nota, b); } /** @@ -423,13 +450,13 @@ Node RewriteRule<NotXor>::apply(Node node) { * ~ (~ a) ==> a */ -template<> +template<> inline bool RewriteRule<NotIdemp>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_NOT && node[0].getKind() == kind::BITVECTOR_NOT); } -template<> +template<> inline Node RewriteRule<NotIdemp>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl; return node[0][0]; @@ -443,14 +470,14 @@ Node RewriteRule<NotIdemp>::apply(Node node) { * a < a ==> false */ -template<> +template<> inline bool RewriteRule<LtSelf>::applies(Node node) { return ((node.getKind() == kind::BITVECTOR_ULT || node.getKind() == kind::BITVECTOR_SLT) && node[0] == node[1]); } -template<> +template<> inline Node RewriteRule<LtSelf>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<LtSelf>(" << node << ")" << std::endl; return utils::mkFalse(); @@ -462,14 +489,14 @@ Node RewriteRule<LtSelf>::apply(Node node) { * a <= a ==> true */ -template<> +template<> inline bool RewriteRule<LteSelf>::applies(Node node) { return ((node.getKind() == kind::BITVECTOR_ULE || node.getKind() == kind::BITVECTOR_SLE) && node[0] == node[1]); } -template<> +template<> inline Node RewriteRule<LteSelf>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<LteSelf>(" << node << ")" << std::endl; return utils::mkTrue(); @@ -481,13 +508,13 @@ Node RewriteRule<LteSelf>::apply(Node node) { * a < 0 ==> false */ -template<> +template<> inline bool RewriteRule<UltZero>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULT && node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); } -template<> +template<> inline Node RewriteRule<UltZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl; return utils::mkFalse(); @@ -499,13 +526,13 @@ Node RewriteRule<UltZero>::apply(Node node) { * a < a ==> false */ -template<> +template<> inline bool RewriteRule<UltSelf>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULT && node[1] == node[0]); } -template<> +template<> inline Node RewriteRule<UltSelf>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UltSelf>(" << node << ")" << std::endl; return utils::mkFalse(); @@ -518,13 +545,13 @@ Node RewriteRule<UltSelf>::apply(Node node) { * a <= 0 ==> a = 0 */ -template<> +template<> inline bool RewriteRule<UleZero>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULE && node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); } -template<> +template<> inline Node RewriteRule<UleZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UleZero>(" << node << ")" << std::endl; return utils::mkNode(kind::EQUAL, node[0], node[1]); @@ -536,13 +563,13 @@ Node RewriteRule<UleZero>::apply(Node node) { * a <= a ==> true */ -template<> +template<> inline bool RewriteRule<UleSelf>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULE && node[1] == node[0]); } -template<> +template<> inline Node RewriteRule<UleSelf>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UleSelf>(" << node << ")" << std::endl; return utils::mkTrue(); @@ -555,13 +582,13 @@ Node RewriteRule<UleSelf>::apply(Node node) { * 0 <= a ==> true */ -template<> +template<> inline bool RewriteRule<ZeroUle>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_ULE && node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); } -template<> +template<> inline Node RewriteRule<ZeroUle>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ZeroUle>(" << node << ")" << std::endl; return utils::mkTrue(); @@ -573,7 +600,7 @@ Node RewriteRule<ZeroUle>::apply(Node node) { * a <= 11..1 ==> true */ -template<> +template<> inline bool RewriteRule<UleMax>::applies(Node node) { if (node.getKind()!= kind::BITVECTOR_ULE) { return false; @@ -584,7 +611,7 @@ bool RewriteRule<UleMax>::applies(Node node) { node[1] == utils::mkConst(BitVector(size, ones))); } -template<> +template<> inline Node RewriteRule<UleMax>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UleMax>(" << node << ")" << std::endl; return utils::mkTrue(); @@ -596,13 +623,13 @@ Node RewriteRule<UleMax>::apply(Node node) { * ~ ( a < b) ==> b <= a */ -template<> +template<> inline bool RewriteRule<NotUlt>::applies(Node node) { return (node.getKind() == kind::NOT && node[0].getKind() == kind::BITVECTOR_ULT); } -template<> +template<> inline Node RewriteRule<NotUlt>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<NotUlt>(" << node << ")" << std::endl; Node ult = node[0]; @@ -617,13 +644,13 @@ Node RewriteRule<NotUlt>::apply(Node node) { * ~ ( a <= b) ==> b < a */ -template<> +template<> inline bool RewriteRule<NotUle>::applies(Node node) { return (node.getKind() == kind::NOT && node[0].getKind() == kind::BITVECTOR_ULE); } -template<> +template<> inline Node RewriteRule<NotUle>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<NotUle>(" << node << ")" << std::endl; Node ult = node[0]; @@ -638,7 +665,7 @@ Node RewriteRule<NotUle>::apply(Node node) { * (a * 1) ==> a */ -template<> +template<> inline bool RewriteRule<MultOne>::applies(Node node) { unsigned size = utils::getSize(node); return (node.getKind() == kind::BITVECTOR_MULT && @@ -646,7 +673,7 @@ bool RewriteRule<MultOne>::applies(Node node) { node[1] == utils::mkConst(size, 1))); } -template<> +template<> inline Node RewriteRule<MultOne>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node << ")" << std::endl; unsigned size = utils::getSize(node); @@ -663,7 +690,7 @@ Node RewriteRule<MultOne>::apply(Node node) { * (a * 0) ==> 0 */ -template<> +template<> inline bool RewriteRule<MultZero>::applies(Node node) { unsigned size = utils::getSize(node); return (node.getKind() == kind::BITVECTOR_MULT && @@ -671,7 +698,7 @@ bool RewriteRule<MultZero>::applies(Node node) { node[1] == utils::mkConst(size, 0))); } -template<> +template<> inline Node RewriteRule<MultZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 0); @@ -683,33 +710,39 @@ Node RewriteRule<MultZero>::apply(Node node) { * (a * 2^k) ==> a[n-k-1:0] 0_k */ -template<> +template<> inline bool RewriteRule<MultPow2>::applies(Node node) { - return (node.getKind() == kind::BITVECTOR_MULT && - (utils::isPow2Const(node[0]) || - utils::isPow2Const(node[1]))); + if (node.getKind() != kind::BITVECTOR_MULT) + return false; + + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + if (utils::isPow2Const(node[i])) { + return true; + } + } + return false; } -template<> +template<> inline Node RewriteRule<MultPow2>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<MultPow2>(" << node << ")" << std::endl; - Node a; - unsigned power; - power = utils::isPow2Const(node[0]); - - if (power != 0) { - a = node[1]; - // isPow2Const returns the power + 1 - --power; - } else { - power = utils::isPow2Const(node[1]); - Assert(power != 0); - a = node[0]; - power--; + + std::vector<Node> children; + unsigned exponent = 0; + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + unsigned exp = utils::isPow2Const(node[i]); + if (exp) { + exponent += exp - 1; + } + else { + children.push_back(node[i]); + } } - Node extract = utils::mkExtract(a, utils::getSize(node) - power - 1, 0); - Node zeros = utils::mkConst(power, 0); + Node a = utils::mkSortedNode(kind::BITVECTOR_MULT, children); + + Node extract = utils::mkExtract(a, utils::getSize(node) - exponent - 1, 0); + Node zeros = utils::mkConst(exponent, 0); return utils::mkConcat(extract, zeros); } @@ -719,7 +752,7 @@ Node RewriteRule<MultPow2>::apply(Node node) { * (a + 0) ==> a */ -template<> +template<> inline bool RewriteRule<PlusZero>::applies(Node node) { Node zero = utils::mkConst(utils::getSize(node), 0); return (node.getKind() == kind::BITVECTOR_PLUS && @@ -727,7 +760,7 @@ bool RewriteRule<PlusZero>::applies(Node node) { node[1] == zero)); } -template<> +template<> inline Node RewriteRule<PlusZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node << ")" << std::endl; Node zero = utils::mkConst(utils::getSize(node), 0); @@ -744,13 +777,13 @@ Node RewriteRule<PlusZero>::apply(Node node) { * -(-a) ==> a */ -template<> +template<> inline bool RewriteRule<NegIdemp>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_NEG && node[0].getKind() == kind::BITVECTOR_NEG); } -template<> +template<> inline Node RewriteRule<NegIdemp>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<NegIdemp>(" << node << ")" << std::endl; return node[0][0]; @@ -762,13 +795,13 @@ Node RewriteRule<NegIdemp>::apply(Node node) { * (a udiv 2^k) ==> 0_k a[n-1: k] */ -template<> +template<> inline bool RewriteRule<UdivPow2>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UDIV && utils::isPow2Const(node[1])); } -template<> +template<> inline Node RewriteRule<UdivPow2>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl; Node a = node[0]; @@ -786,13 +819,13 @@ Node RewriteRule<UdivPow2>::apply(Node node) { * (a udiv 1) ==> a */ -template<> +template<> inline bool RewriteRule<UdivOne>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UDIV && node[1] == utils::mkConst(utils::getSize(node), 1)); } -template<> +template<> inline Node RewriteRule<UdivOne>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UdivOne>(" << node << ")" << std::endl; return node[0]; @@ -804,13 +837,13 @@ Node RewriteRule<UdivOne>::apply(Node node) { * (a udiv a) ==> 1 */ -template<> +template<> inline bool RewriteRule<UdivSelf>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UDIV && node[0] == node[1]); } -template<> +template<> inline Node RewriteRule<UdivSelf>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UdivSelf>(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 1); @@ -822,13 +855,13 @@ Node RewriteRule<UdivSelf>::apply(Node node) { * (a urem 2^k) ==> 0_(n-k) a[k-1:0] */ -template<> +template<> inline bool RewriteRule<UremPow2>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UREM && utils::isPow2Const(node[1])); } -template<> +template<> inline Node RewriteRule<UremPow2>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl; TNode a = node[0]; @@ -844,13 +877,13 @@ Node RewriteRule<UremPow2>::apply(Node node) { * (a urem 1) ==> 0 */ -template<> +template<> inline bool RewriteRule<UremOne>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UREM && node[1] == utils::mkConst(utils::getSize(node), 1)); } -template<> +template<> inline Node RewriteRule<UremOne>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UremOne>(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 0); @@ -862,13 +895,13 @@ Node RewriteRule<UremOne>::apply(Node node) { * (a urem a) ==> 0 */ -template<> +template<> inline bool RewriteRule<UremSelf>::applies(Node node) { return (node.getKind() == kind::BITVECTOR_UREM && node[0] == node[1]); } -template<> +template<> inline Node RewriteRule<UremSelf>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<UremSelf>(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 0); @@ -880,7 +913,7 @@ Node RewriteRule<UremSelf>::apply(Node node) { * (0_k >> a) ==> 0_k */ -template<> +template<> inline bool RewriteRule<ShiftZero>::applies(Node node) { return ((node.getKind() == kind::BITVECTOR_SHL || node.getKind() == kind::BITVECTOR_LSHR || @@ -888,24 +921,110 @@ bool RewriteRule<ShiftZero>::applies(Node node) { node[0] == utils::mkConst(utils::getSize(node), 0)); } -template<> +template<> inline Node RewriteRule<ShiftZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ShiftZero>(" << node << ")" << std::endl; return node[0]; } +/** + * BBPlusNeg + * + * -a1 - a2 - ... - an + ak + .. ==> - (a1 + a2 + ... + an) + ak + * + */ + +template<> inline +bool RewriteRule<BBPlusNeg>::applies(Node node) { + if (node.getKind() != kind::BITVECTOR_PLUS) { + return false; + } + + unsigned neg_count = 0; + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind()== kind::BITVECTOR_NEG) { + ++neg_count; + } + } + return neg_count > 1; +} + +template<> inline +Node RewriteRule<BBPlusNeg>::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule<BBPlusNeg>(" << node << ")" << std::endl; + + std::vector<Node> children; + unsigned neg_count = 0; + for(unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::BITVECTOR_NEG) { + ++neg_count; + children.push_back(utils::mkNode(kind::BITVECTOR_NOT, node[i][0])); + } else { + children.push_back(node[i]); + } + } + Assert(neg_count!= 0); + children.push_back(utils::mkConst(utils::getSize(node), neg_count)); + + return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); +} + +// /** +// * +// * +// * +// */ + +// template<> inline +// bool RewriteRule<BBFactorOut>::applies(Node node) { +// if (node.getKind() != kind::BITVECTOR_PLUS) { +// return false; +// } + +// for (unsigned i = 0; i < node.getNumChildren(); ++i) { +// if (node[i].getKind() != kind::BITVECTOR_MULT) { +// return false; +// } +// } +// } + +// template<> inline +// Node RewriteRule<BBFactorOut>::apply(Node node) { +// BVDebug("bv-rewrite") << "RewriteRule<BBFactorOut>(" << node << ")" << std::endl; +// std::hash_set<TNode, TNodeHashFunction> factors; + +// for (unsigned i = 0; i < node.getNumChildren(); ++i) { +// Assert (node[i].getKind() == kind::BITVECTOR_MULT); +// for (unsigned j = 0; j < node[i].getNumChildren(); ++j) { +// factors.insert(node[i][j]); +// } +// } + +// std::vector<TNode> gcd; +// std::hash_set<TNode, TNodeHashFunction>::const_iterator it; +// for (it = factors.begin(); it != factors.end(); ++it) { +// // for each factor check if it occurs in all children +// TNode f = *it; +// for (unsigned i = 0; i < node.getNumChildren + +// } +// } +// return ; +// } + + // /** // * // * // * // */ -// template<> +// template<> inline // bool RewriteRule<>::applies(Node node) { // return (node.getKind() == ); // } -// template<> +// template<> inline // Node RewriteRule<>::apply(Node node) { // BVDebug("bv-rewrite") << "RewriteRule<>(" << node << ")" << std::endl; // return ; diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 2b48977b6..c2649e881 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -49,19 +49,31 @@ void TheoryBVRewriter::shutdown() { } RewriteResponse TheoryBVRewriter::preRewrite(TNode node) { - Debug("bitvector-rewrite") << "TheoryBV::preRewrite(" << node << ")" << std::endl; - //return d_rewriteTable[node.getKind()](node); - return RewriteResponse(REWRITE_DONE, node); + RewriteResponse res = d_rewriteTable[node.getKind()](node, true); + if(res.node != node) { + Debug("bitvector-rewrite") << "TheoryBV::preRewrite " << node << std::endl; + Debug("bitvector-rewrite") << "TheoryBV::preRewrite to " << res.node << std::endl; + } + return res; } RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { - //TimerStat::CodeTimer codeTimer(*d_rewriteTimer); - Debug("bitvector-rewrite") << "TheoryBV::postRewrite(" << node << ")" << std::endl; - RewriteResponse res = d_rewriteTable[node.getKind()](node); + RewriteResponse res = d_rewriteTable[node.getKind()](node, false); + if(res.node!= node) { + Debug("bitvector-rewrite") << "TheoryBV::postRewrite " << node << std::endl; + Debug("bitvector-rewrite") << "TheoryBV::postRewrite to " << res.node << std::endl; + } + // if (res.status == REWRITE_DONE) { + // Node rewr = res.node; + // Node rerewr = d_rewriteTable[rewr.getKind()](rewr, false).node; + // Assert(rewr == rerewr); + // } + return res; } -RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { + // reduce common subexpressions on both sides Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUlt>, // if both arguments are constants evaluates @@ -72,8 +84,13 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node){ - return RewriteResponse(REWRITE_DONE, node); +RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ + Node resultNode = LinearRewriteStrategy + < RewriteRule < EvalSlt > + >::apply(node); + + return RewriteResponse(REWRITE_DONE, resultNode); + // Node resultNode = LinearRewriteStrategy // < RewriteRule < SltEliminate > // // a <_s b ==> a + 2^{n-1} <_u b + 2^{n-1} @@ -82,7 +99,7 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node){ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUle(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUle>, RewriteRule<UleMax>, @@ -93,16 +110,15 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSle(TNode node){ - return RewriteResponse(REWRITE_DONE, node); - // Node resultNode = LinearRewriteStrategy - // < RewriteRule<SleEliminate> - // >::apply(node); +RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ + Node resultNode = LinearRewriteStrategy + < RewriteRule < EvalSle > + >::apply(node); - // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<UgtEliminate> >::apply(node); @@ -110,16 +126,16 @@ RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<SgtEliminate> //RewriteRule<SltEliminate> >::apply(node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUge(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<UgeEliminate> >::apply(node); @@ -127,7 +143,7 @@ RewriteResponse TheoryBVRewriter::RewriteUge(TNode node){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSge(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<SgeEliminate> // RewriteRule<SleEliminate> @@ -136,8 +152,9 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNot(TNode node){ - Node resultNode = node; +RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){ + Node resultNode = node; + if(RewriteRule<NotXor>::applies(node)) { resultNode = RewriteRule<NotXor>::run<false>(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -150,8 +167,9 @@ RewriteResponse TheoryBVRewriter::RewriteNot(TNode node){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { Node resultNode = node; + if (RewriteRule<ExtractConcat>::applies(node)) { resultNode = RewriteRule<ExtractConcat>::run<false>(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -184,7 +202,8 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node) { } -RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) { + Node resultNode = LinearRewriteStrategy < RewriteRule<ConcatFlatten>, // Flatten the top level concatenations @@ -197,45 +216,53 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node){ - Node resultNode = LinearRewriteStrategy - < RewriteRule<EvalAnd>, - RewriteRule<BitwiseIdemp>, - RewriteRule<AndZero>, - RewriteRule<AndOne> +RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ + Node resultNode = node; + + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, + RewriteRule<AndSimplify> + // RewriteRule<EvalAnd>, + // RewriteRule<BitwiseIdemp>, + // //RewriteRule<BitwiseSlice>, -> might need rw again + // RewriteRule<AndZero>, + // RewriteRule<AndOne> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteOr(TNode node){ - Node resultNode = LinearRewriteStrategy - < RewriteRule<EvalOr>, - RewriteRule<BitwiseIdemp>, - RewriteRule<OrZero>, - RewriteRule<OrOne> +RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ + Node resultNode = node; + + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, + RewriteRule<OrSimplify> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXor(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { Node resultNode = node; - if (RewriteRule<XorOne>::applies(node)) { - resultNode = RewriteRule<XorOne>::run<false> (node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - } + resultNode = LinearRewriteStrategy - < RewriteRule<XorNot>, - RewriteRule<EvalXor>, - RewriteRule<XorDuplicate>, - RewriteRule<XorZero> + < RewriteRule<FlattenAssocCommut>, // flatten the expression + RewriteRule<XorSimplify>, // simplify duplicates and constants + RewriteRule<XorZero> // checks if the constant part is zero and eliminates it >::apply(node); - + + // this simplification introduces new terms and might require further + // rewriting + if (RewriteRule<XorOne>::applies(resultNode)) { + resultNode = RewriteRule<XorOne>::run<false> (resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<XnorEliminate> >::apply(node); @@ -243,7 +270,7 @@ RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNand(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<NandEliminate> >::apply(node); @@ -251,7 +278,7 @@ RewriteResponse TheoryBVRewriter::RewriteNand(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNor(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<NorEliminate> >::apply(node); @@ -259,7 +286,7 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteComp(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<CompEliminate> >::apply(node); @@ -267,54 +294,81 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteMult(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { Node resultNode = node; - if(RewriteRule<MultPow2>::applies(node)) { - resultNode = RewriteRule<MultPow2>::run <false> (node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - } resultNode = LinearRewriteStrategy - < RewriteRule<EvalMult>, - RewriteRule<MultOne>, - RewriteRule<MultZero> + < RewriteRule<FlattenAssocCommut>, // flattens and sorts + RewriteRule<MultSimplify> // multiplies constant part and checks for 0 >::apply(node); + // only apply if every subterm was already rewritten + if (!preregister) { + // distributes multiplication by constant over +, - and unary - + if(RewriteRule<MultDistribConst>::applies(resultNode)) { + resultNode = RewriteRule<MultDistribConst>::run<false>(resultNode); + // creating new terms that might simplify further + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } + + if(resultNode == node) { + return RewriteResponse(REWRITE_DONE, resultNode); + } return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewritePlus(TNode node) { - Node resultNode = LinearRewriteStrategy - < RewriteRule<EvalPlus>, - RewriteRule<PlusZero> - // RewriteRule<PlusSelf>, - // RewriteRule<PlusNegSelf> - // RewriteRule<PlusLiftConcat> - >::apply(node); +RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { + Node resultNode = node; - return RewriteResponse(REWRITE_DONE, resultNode); + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, + RewriteRule<PlusCombineLikeTerms> + // RewriteRule<PlusLiftConcat> + >::apply(resultNode); + if (resultNode == node) { + return RewriteResponse(REWRITE_DONE, resultNode); + } else { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } } -RewriteResponse TheoryBVRewriter::RewriteSub(TNode node){ - return RewriteResponse(REWRITE_DONE, node); - // Node resultNode = LinearRewriteStrategy - // < RewriteRule<SubEliminate> - // >::apply(node); +RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){ + // return RewriteResponse(REWRITE_DONE, node); + Node resultNode = LinearRewriteStrategy + < RewriteRule<SubEliminate> + >::apply(node); - // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node) { - Node resultNode = LinearRewriteStrategy +RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { + Node resultNode = node; + + resultNode = LinearRewriteStrategy < RewriteRule<EvalNeg>, - RewriteRule<NegIdemp> - >::apply(node); + RewriteRule<NegIdemp>, + RewriteRule<NegSub> + >::apply(node); + + if (RewriteRule<NegPlus>::applies(node)) { + resultNode = RewriteRule<NegPlus>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + if(!preregister) { + if (RewriteRule<NegMult>::applies(node)) { + resultNode = RewriteRule<NegMult>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } + return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node){ - Node resultNode = node; +RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){ + Node resultNode = node; + if(RewriteRule<UdivPow2>::applies(node)) { resultNode = RewriteRule<UdivPow2>::run <false> (node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -329,8 +383,10 @@ RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node) { - Node resultNode = node; +RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool preregister) { + Node resultNode = node; + return RewriteResponse(REWRITE_DONE, resultNode); + if(RewriteRule<UremPow2>::applies(node)) { resultNode = RewriteRule<UremPow2>::run <false> (node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -344,7 +400,7 @@ RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<SmodEliminate> >::apply(node); @@ -352,7 +408,7 @@ RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<SdivEliminate> >::apply(node); @@ -360,14 +416,14 @@ RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<SremEliminate> >::apply(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteShl(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) { Node resultNode = node; if(RewriteRule<ShlByConst>::applies(node)) { resultNode = RewriteRule<ShlByConst>::run <false> (node); @@ -382,7 +438,7 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) { Node resultNode = node; if(RewriteRule<LshrByConst>::applies(node)) { resultNode = RewriteRule<LshrByConst>::run <false> (node); @@ -397,7 +453,7 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) { Node resultNode = node; if(RewriteRule<AshrByConst>::applies(node)) { resultNode = RewriteRule<AshrByConst>::run <false> (node); @@ -413,7 +469,7 @@ RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node) { } -RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<RepeatEliminate > >::apply(node); @@ -421,7 +477,7 @@ RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<ZeroExtendEliminate > >::apply(node); @@ -429,17 +485,17 @@ RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node) { - // Node resultNode = LinearRewriteStrategy - // < RewriteRule<SignExtendEliminate > - // >::apply(node); +RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister) { + Node resultNode = LinearRewriteStrategy + < RewriteRule<EvalSignExtend> + >::apply(node); // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - return RewriteResponse(REWRITE_DONE, node); + return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<RotateRightEliminate > >::apply(node); @@ -447,7 +503,7 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node){ +RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule<RotateLeftEliminate > >::apply(node); @@ -455,7 +511,7 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node) { +RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, @@ -466,11 +522,11 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node) { } -RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node) { +RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node, bool prerewrite) { return RewriteResponse(REWRITE_DONE, node); } -RewriteResponse TheoryBVRewriter::UndefinedRewrite(TNode node) { +RewriteResponse TheoryBVRewriter::UndefinedRewrite(TNode node, bool prerewrite) { Debug("bv-rewrite") << "TheoryBV::UndefinedRewrite for" << node; Unimplemented(); } diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 7ce914477..0ce3fa303 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -30,7 +30,7 @@ namespace theory { namespace bv { struct AllRewriteRules; -typedef RewriteResponse (*RewriteFunction) (TNode); +typedef RewriteResponse (*RewriteFunction) (TNode, bool); class TheoryBVRewriter { // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules; @@ -39,47 +39,47 @@ class TheoryBVRewriter { #warning "TODO: Double check thread safety and make sure the fix compiles on mac." static RewriteFunction d_rewriteTable[kind::LAST_KIND]; - static RewriteResponse IdentityRewrite(TNode node); - static RewriteResponse UndefinedRewrite(TNode node); + static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false); + static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); static void initializeRewrites(); - static RewriteResponse RewriteEqual(TNode node); - static RewriteResponse RewriteUlt(TNode node); - static RewriteResponse RewriteSlt(TNode node); - static RewriteResponse RewriteUle(TNode node); - static RewriteResponse RewriteSle(TNode node); - static RewriteResponse RewriteUgt(TNode node); - static RewriteResponse RewriteSgt(TNode node); - static RewriteResponse RewriteUge(TNode node); - static RewriteResponse RewriteSge(TNode node); - static RewriteResponse RewriteNot(TNode node); - static RewriteResponse RewriteConcat(TNode node); - static RewriteResponse RewriteAnd(TNode node); - static RewriteResponse RewriteOr(TNode node); - static RewriteResponse RewriteXnor(TNode node); - static RewriteResponse RewriteXor(TNode node); - static RewriteResponse RewriteNand(TNode node); - static RewriteResponse RewriteNor(TNode node); - static RewriteResponse RewriteComp(TNode node); - static RewriteResponse RewriteMult(TNode node); - static RewriteResponse RewritePlus(TNode node); - static RewriteResponse RewriteSub(TNode node); - static RewriteResponse RewriteNeg(TNode node); - static RewriteResponse RewriteUdiv(TNode node); - static RewriteResponse RewriteUrem(TNode node); - static RewriteResponse RewriteSmod(TNode node); - static RewriteResponse RewriteSdiv(TNode node); - static RewriteResponse RewriteSrem(TNode node); - static RewriteResponse RewriteShl(TNode node); - static RewriteResponse RewriteLshr(TNode node); - static RewriteResponse RewriteAshr(TNode node); - static RewriteResponse RewriteExtract(TNode node); - static RewriteResponse RewriteRepeat(TNode node); - static RewriteResponse RewriteZeroExtend(TNode node); - static RewriteResponse RewriteSignExtend(TNode node); - static RewriteResponse RewriteRotateRight(TNode node); - static RewriteResponse RewriteRotateLeft(TNode node); + static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUle(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSle(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUge(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSge(TNode node, bool prerewrite = false); + static RewriteResponse RewriteNot(TNode node, bool prerewrite = false); + static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false); + static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false); + static RewriteResponse RewriteOr(TNode node, bool prerewrite = false); + static RewriteResponse RewriteXnor(TNode node, bool prerewrite = false); + static RewriteResponse RewriteXor(TNode node, bool prerewrite = false); + static RewriteResponse RewriteNand(TNode node, bool prerewrite = false); + static RewriteResponse RewriteNor(TNode node, bool prerewrite = false); + static RewriteResponse RewriteComp(TNode node, bool prerewrite = false); + static RewriteResponse RewriteMult(TNode node, bool prerewrite = false); + static RewriteResponse RewritePlus(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSub(TNode node, bool prerewrite = false); + static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false); + static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false); + static RewriteResponse RewriteShl(TNode node, bool prerewrite = false); + static RewriteResponse RewriteLshr(TNode node, bool prerewrite = false); + static RewriteResponse RewriteAshr(TNode node, bool prerewrite = false); + static RewriteResponse RewriteExtract(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRepeat(TNode node, bool prerewrite = false); + static RewriteResponse RewriteZeroExtend(TNode node, bool prerewrite = false); + static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); public: diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 60e459958..8b5dd0499 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -79,6 +79,27 @@ inline Node mkAnd(std::vector<TNode>& children) { } } +inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { + Assert (kind == kind::BITVECTOR_PLUS || + kind == kind::BITVECTOR_MULT || + kind == kind::BITVECTOR_AND || + kind == kind::BITVECTOR_OR || + kind == kind::BITVECTOR_XOR); + + if (children.size() == 1) { + return children[0]; + } + std::sort(children.begin(), children.end()); + return NodeManager::currentNM()->mkNode(kind, children); +} + + +inline Node mkNode(Kind kind, std::vector<Node>& children) { + if (children.size() == 1) { + return children[0]; + } + return NodeManager::currentNM()->mkNode(kind, children); +} inline Node mkNode(Kind kind, TNode child) { return NodeManager::currentNM()->mkNode(kind, child); @@ -88,6 +109,21 @@ inline Node mkNode(Kind kind, TNode child1, TNode child2) { return NodeManager::currentNM()->mkNode(kind, child1, child2); } + +inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) { + Assert (kind == kind::BITVECTOR_PLUS || + kind == kind::BITVECTOR_MULT || + kind == kind::BITVECTOR_AND || + kind == kind::BITVECTOR_OR || + kind == kind::BITVECTOR_XOR); + + if (child1 < child2) { + return NodeManager::currentNM()->mkNode(kind, child1, child2); + } else { + return NodeManager::currentNM()->mkNode(kind, child2, child1); + } +} + inline Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { return NodeManager::currentNM()->mkNode(kind, child1, child2, child3); } @@ -156,8 +192,14 @@ inline Node mkConcat(TNode t1, TNode t2) { return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2); } + +inline BitVector mkBitVectorOnes(unsigned size) { + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); +} + inline Node mkOnes(unsigned size) { - BitVector val = BitVector(1, Integer(1)).signExtend(size-1); + BitVector val = mkBitVectorOnes(size); return NodeManager::currentNM()->mkConst<BitVector>(val); } @@ -276,6 +318,7 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) { std::vector<TNode>::const_iterator it_end = nodes.end(); while (it != it_end) { TNode current = *it; + if (current != mkTrue()) { Assert(isBVPredicate(current)); expandedNodes.push_back(current); |