diff options
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 261 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 28 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 5 |
3 files changed, 159 insertions, 135 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 1eb815ef9..0ce9e6d5a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -104,7 +104,8 @@ enum RewriteRuleId /// simplification rules /// all of these rules decrease formula size - BvIte, + BvIteConstCond, + BvIteChildren, BvComp, ShlByConst, LshrByConst, @@ -242,7 +243,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalRotateLeft : out << "EvalRotateLeft"; return out; case EvalRotateRight : out << "EvalRotateRight"; return out; case EvalNeg : out << "EvalNeg"; return out; - case BvIte : out << "BvIte"; return out; + case BvIteConstCond : out << "BvIteConstCond"; return out; + case BvIteChildren : out << "BvIteChildren"; return out; case BvComp : out << "BvComp"; return out; case ShlByConst : out << "ShlByConst"; return out; case LshrByConst : out << "LshrByConst"; return out; @@ -430,134 +432,135 @@ public: /** Have to list all the rewrite rules to get the statistics out */ struct AllRewriteRules { - RewriteRule<EmptyRule> rule00; - RewriteRule<ConcatFlatten> rule01; - RewriteRule<ConcatExtractMerge> rule02; - RewriteRule<ConcatConstantMerge> rule03; - RewriteRule<ExtractExtract> rule04; - RewriteRule<ExtractWhole> rule05; - RewriteRule<ExtractConcat> rule06; - RewriteRule<ExtractConstant> rule07; - RewriteRule<FailEq> rule08; - RewriteRule<SimplifyEq> rule09; - RewriteRule<ReflexivityEq> rule10; - RewriteRule<UgtEliminate> rule11; - RewriteRule<SgtEliminate> rule12; - RewriteRule<UgeEliminate> rule13; - RewriteRule<SgeEliminate> rule14; - RewriteRule<NegMult> rule15; - RewriteRule<NegSub> rule16; - RewriteRule<RepeatEliminate> rule17; - RewriteRule<RotateLeftEliminate> rule18; - RewriteRule<RotateRightEliminate> rule19; - RewriteRule<NandEliminate> rule20; - RewriteRule<NorEliminate> rule21; - RewriteRule<SdivEliminate> rule22; - RewriteRule<SremEliminate> rule23; - RewriteRule<SmodEliminate> rule24; - RewriteRule<EvalConcat> rule25; - RewriteRule<EvalAnd> rule26; - 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; - RewriteRule<EvalLshr> rule37; - RewriteRule<EvalAshr> rule38; - RewriteRule<EvalUlt> rule39; - RewriteRule<EvalUle> rule40; - RewriteRule<EvalSle> rule41; - RewriteRule<EvalExtract> rule43; - RewriteRule<EvalSignExtend> rule44; - RewriteRule<EvalRotateLeft> rule45; - RewriteRule<EvalRotateRight> rule46; - RewriteRule<EvalEquals> rule47; - RewriteRule<EvalNeg> rule48; - RewriteRule<BvIte> rule49; - RewriteRule<ShlByConst> rule50; - RewriteRule<LshrByConst> rule51; - RewriteRule<AshrByConst> rule52; - RewriteRule<ExtractBitwise> rule53; - RewriteRule<ExtractNot> rule54; - RewriteRule<ExtractArith> rule55; - RewriteRule<DoubleNeg> rule56; - RewriteRule<NotConcat> rule57; - RewriteRule<NotAnd> rule58; - RewriteRule<NotOr> rule59; - RewriteRule<NotXor> rule60; - RewriteRule<BitwiseIdemp> rule61; - RewriteRule<XorDuplicate> rule62; - RewriteRule<BitwiseNotAnd> rule63; - RewriteRule<BitwiseNotOr> rule64; - RewriteRule<XorNot> rule65; - RewriteRule<LtSelf> rule66; - RewriteRule<LtSelf> rule67; - RewriteRule<UltZero> rule68; - RewriteRule<UleZero> rule69; - RewriteRule<ZeroUle> rule70; - RewriteRule<NotUlt> rule71; - RewriteRule<NotUle> rule72; - RewriteRule<ZeroExtendEliminate> rule73; - RewriteRule<UleMax> rule74; - RewriteRule<LteSelf> rule75; - RewriteRule<SltEliminate> rule76; - RewriteRule<SleEliminate> rule77; - RewriteRule<AndZero> rule78; - RewriteRule<AndOne> rule79; - RewriteRule<OrZero> rule80; - RewriteRule<OrOne> rule81; - RewriteRule<SubEliminate> rule82; - RewriteRule<XorOne> rule83; - RewriteRule<XorZero> rule84; - RewriteRule<MultSlice> rule85; + RewriteRule<EmptyRule> rule00; + RewriteRule<ConcatFlatten> rule01; + RewriteRule<ConcatExtractMerge> rule02; + RewriteRule<ConcatConstantMerge> rule03; + RewriteRule<ExtractExtract> rule04; + RewriteRule<ExtractWhole> rule05; + RewriteRule<ExtractConcat> rule06; + RewriteRule<ExtractConstant> rule07; + RewriteRule<FailEq> rule08; + RewriteRule<SimplifyEq> rule09; + RewriteRule<ReflexivityEq> rule10; + RewriteRule<UgtEliminate> rule11; + RewriteRule<SgtEliminate> rule12; + RewriteRule<UgeEliminate> rule13; + RewriteRule<SgeEliminate> rule14; + RewriteRule<NegMult> rule15; + RewriteRule<NegSub> rule16; + RewriteRule<RepeatEliminate> rule17; + RewriteRule<RotateLeftEliminate> rule18; + RewriteRule<RotateRightEliminate> rule19; + RewriteRule<NandEliminate> rule20; + RewriteRule<NorEliminate> rule21; + RewriteRule<SdivEliminate> rule22; + RewriteRule<SremEliminate> rule23; + RewriteRule<SmodEliminate> rule24; + RewriteRule<EvalConcat> rule25; + RewriteRule<EvalAnd> rule26; + 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; + RewriteRule<EvalLshr> rule37; + RewriteRule<EvalAshr> rule38; + RewriteRule<EvalUlt> rule39; + RewriteRule<EvalUle> rule40; + RewriteRule<EvalSle> rule41; + RewriteRule<EvalExtract> rule43; + RewriteRule<EvalSignExtend> rule44; + RewriteRule<EvalRotateLeft> rule45; + RewriteRule<EvalRotateRight> rule46; + RewriteRule<EvalEquals> rule47; + RewriteRule<EvalNeg> rule48; + RewriteRule<ShlByConst> rule50; + RewriteRule<LshrByConst> rule51; + RewriteRule<AshrByConst> rule52; + RewriteRule<ExtractBitwise> rule53; + RewriteRule<ExtractNot> rule54; + RewriteRule<ExtractArith> rule55; + RewriteRule<DoubleNeg> rule56; + RewriteRule<NotConcat> rule57; + RewriteRule<NotAnd> rule58; + RewriteRule<NotOr> rule59; + RewriteRule<NotXor> rule60; + RewriteRule<BitwiseIdemp> rule61; + RewriteRule<XorDuplicate> rule62; + RewriteRule<BitwiseNotAnd> rule63; + RewriteRule<BitwiseNotOr> rule64; + RewriteRule<XorNot> rule65; + RewriteRule<LtSelf> rule66; + RewriteRule<LtSelf> rule67; + RewriteRule<UltZero> rule68; + RewriteRule<UleZero> rule69; + RewriteRule<ZeroUle> rule70; + RewriteRule<NotUlt> rule71; + RewriteRule<NotUle> rule72; + RewriteRule<ZeroExtendEliminate> rule73; + RewriteRule<UleMax> rule74; + RewriteRule<LteSelf> rule75; + RewriteRule<SltEliminate> rule76; + RewriteRule<SleEliminate> rule77; + RewriteRule<AndZero> rule78; + RewriteRule<AndOne> rule79; + RewriteRule<OrZero> rule80; + RewriteRule<OrOne> rule81; + RewriteRule<SubEliminate> rule82; + RewriteRule<XorOne> rule83; + RewriteRule<XorZero> rule84; + RewriteRule<MultSlice> rule85; RewriteRule<FlattenAssocCommutNoDuplicates> rule86; - RewriteRule<MultPow2> rule87; - RewriteRule<ExtractMultLeadingBit> rule88; - RewriteRule<NegIdemp> rule91; - RewriteRule<UdivPow2> rule92; - RewriteRule<UdivZero> rule93; - RewriteRule<UdivOne> rule94; - RewriteRule<UremPow2> rule95; - RewriteRule<UremOne> rule96; - RewriteRule<UremSelf> rule97; - RewriteRule<ShiftZero> rule98; - RewriteRule<CompEliminate> rule99; - RewriteRule<XnorEliminate> rule100; - 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; - RewriteRule<SolveEq> rule112; - RewriteRule<BitwiseEq> rule113; - RewriteRule<UltOne> rule114; - RewriteRule<SltZero> rule115; - RewriteRule<BVToNatEliminate> rule116; - RewriteRule<IntToBVEliminate> rule117; - RewriteRule<MultDistrib> rule118; - RewriteRule<UltPlusOne> rule119; - RewriteRule<ConcatToMult> rule120; - RewriteRule<IsPowerOfTwo> rule121; - RewriteRule<RedorEliminate> rule122; - RewriteRule<RedandEliminate> rule123; - RewriteRule<SignExtendEqConst> rule124; - RewriteRule<ZeroExtendEqConst> rule125; - RewriteRule<SignExtendUltConst> rule126; - RewriteRule<ZeroExtendUltConst> rule127; - RewriteRule<MultSltMult> rule128; - RewriteRule<NormalizeEqPlusNeg> rule129; - RewriteRule<BvComp> rule130; + RewriteRule<MultPow2> rule87; + RewriteRule<ExtractMultLeadingBit> rule88; + RewriteRule<NegIdemp> rule91; + RewriteRule<UdivPow2> rule92; + RewriteRule<UdivZero> rule93; + RewriteRule<UdivOne> rule94; + RewriteRule<UremPow2> rule95; + RewriteRule<UremOne> rule96; + RewriteRule<UremSelf> rule97; + RewriteRule<ShiftZero> rule98; + RewriteRule<CompEliminate> rule99; + RewriteRule<XnorEliminate> rule100; + 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; + RewriteRule<SolveEq> rule112; + RewriteRule<BitwiseEq> rule113; + RewriteRule<UltOne> rule114; + RewriteRule<SltZero> rule115; + RewriteRule<BVToNatEliminate> rule116; + RewriteRule<IntToBVEliminate> rule117; + RewriteRule<MultDistrib> rule118; + RewriteRule<UltPlusOne> rule119; + RewriteRule<ConcatToMult> rule120; + RewriteRule<IsPowerOfTwo> rule121; + RewriteRule<RedorEliminate> rule122; + RewriteRule<RedandEliminate> rule123; + RewriteRule<SignExtendEqConst> rule124; + RewriteRule<ZeroExtendEqConst> rule125; + RewriteRule<SignExtendUltConst> rule126; + RewriteRule<ZeroExtendUltConst> rule127; + RewriteRule<MultSltMult> rule128; + RewriteRule<NormalizeEqPlusNeg> rule129; + RewriteRule<BvComp> rule130; + RewriteRule<BvIteConstCond> rule131; + RewriteRule<BvIteChildren> rule132; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 9649fec77..6f9480489 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -30,24 +30,44 @@ namespace bv { // FIXME: this rules subsume the constant evaluation ones /** - * BvIte + * BvIteConstCond * * BITVECTOR_ITE with constant condition */ template <> -inline bool RewriteRule<BvIte>::applies(TNode node) +inline bool RewriteRule<BvIteConstCond>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst()); } template <> -inline Node RewriteRule<BvIte>::apply(TNode node) +inline Node RewriteRule<BvIteConstCond>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<BvIte>(" << node << ")" << std::endl; + Debug("bv-rewrite") << "RewriteRule<BvIteConstCond>(" << node << ")" + << std::endl; return utils::isZero(node[0]) ? node[2] : node[1]; } /** + * BvIteChildren + * + * BITVECTOR_ITE with term_then = term_else + */ +template <> +inline bool RewriteRule<BvIteChildren>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]); +} + +template <> +inline Node RewriteRule<BvIteChildren>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<BvIteChildren>(" << node << ")" + << std::endl; + return node[1]; +} + +/** * BvComp * * BITVECTOR_COMP of children of size 1 with one constant child diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 6355da07d..06ff8e77f 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -169,8 +169,9 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) { Node resultNode = - LinearRewriteStrategy<RewriteRule<EvalITEBv>, RewriteRule<BvIte> >::apply( - node); + LinearRewriteStrategy<RewriteRule<EvalITEBv>, + RewriteRule<BvIteConstCond>, + RewriteRule<BvIteChildren> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } |