Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268)

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);
 }