From 23eef2bd8083600babd8498ec779d681620e97df Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 3 Aug 2018 16:43:10 -0700 Subject: [PATCH] Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268) --- src/theory/bv/theory_bv_rewrite_rules.h | 261 +++++++++--------- .../theory_bv_rewrite_rules_simplification.h | 28 +- 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 rule00; - RewriteRule rule01; - RewriteRule rule02; - RewriteRule rule03; - RewriteRule rule04; - RewriteRule rule05; - RewriteRule rule06; - RewriteRule rule07; - RewriteRule rule08; - RewriteRule rule09; - RewriteRule rule10; - RewriteRule rule11; - RewriteRule rule12; - RewriteRule rule13; - RewriteRule rule14; - RewriteRule rule15; - RewriteRule rule16; - RewriteRule rule17; - RewriteRule rule18; - RewriteRule rule19; - RewriteRule rule20; - RewriteRule rule21; - RewriteRule rule22; - RewriteRule rule23; - RewriteRule rule24; - RewriteRule rule25; - RewriteRule rule26; - RewriteRule rule27; - RewriteRule rule28; - RewriteRule rule29; - RewriteRule rule30; - RewriteRule rule31; - RewriteRule rule32; - RewriteRule rule33; - RewriteRule rule34; - RewriteRule rule35; - RewriteRule rule36; - RewriteRule rule37; - RewriteRule rule38; - RewriteRule rule39; - RewriteRule rule40; - RewriteRule rule41; - RewriteRule rule43; - RewriteRule rule44; - RewriteRule rule45; - RewriteRule rule46; - RewriteRule rule47; - RewriteRule rule48; - RewriteRule rule49; - RewriteRule rule50; - RewriteRule rule51; - RewriteRule rule52; - RewriteRule rule53; - RewriteRule rule54; - RewriteRule rule55; - RewriteRule rule56; - RewriteRule rule57; - RewriteRule rule58; - RewriteRule rule59; - RewriteRule rule60; - RewriteRule rule61; - RewriteRule rule62; - RewriteRule rule63; - RewriteRule rule64; - RewriteRule rule65; - RewriteRule rule66; - RewriteRule rule67; - RewriteRule rule68; - RewriteRule rule69; - RewriteRule rule70; - RewriteRule rule71; - RewriteRule rule72; - RewriteRule rule73; - RewriteRule rule74; - RewriteRule rule75; - RewriteRule rule76; - RewriteRule rule77; - RewriteRule rule78; - RewriteRule rule79; - RewriteRule rule80; - RewriteRule rule81; - RewriteRule rule82; - RewriteRule rule83; - RewriteRule rule84; - RewriteRule rule85; + RewriteRule rule00; + RewriteRule rule01; + RewriteRule rule02; + RewriteRule rule03; + RewriteRule rule04; + RewriteRule rule05; + RewriteRule rule06; + RewriteRule rule07; + RewriteRule rule08; + RewriteRule rule09; + RewriteRule rule10; + RewriteRule rule11; + RewriteRule rule12; + RewriteRule rule13; + RewriteRule rule14; + RewriteRule rule15; + RewriteRule rule16; + RewriteRule rule17; + RewriteRule rule18; + RewriteRule rule19; + RewriteRule rule20; + RewriteRule rule21; + RewriteRule rule22; + RewriteRule rule23; + RewriteRule rule24; + RewriteRule rule25; + RewriteRule rule26; + RewriteRule rule27; + RewriteRule rule28; + RewriteRule rule29; + RewriteRule rule30; + RewriteRule rule31; + RewriteRule rule32; + RewriteRule rule33; + RewriteRule rule34; + RewriteRule rule35; + RewriteRule rule36; + RewriteRule rule37; + RewriteRule rule38; + RewriteRule rule39; + RewriteRule rule40; + RewriteRule rule41; + RewriteRule rule43; + RewriteRule rule44; + RewriteRule rule45; + RewriteRule rule46; + RewriteRule rule47; + RewriteRule rule48; + RewriteRule rule50; + RewriteRule rule51; + RewriteRule rule52; + RewriteRule rule53; + RewriteRule rule54; + RewriteRule rule55; + RewriteRule rule56; + RewriteRule rule57; + RewriteRule rule58; + RewriteRule rule59; + RewriteRule rule60; + RewriteRule rule61; + RewriteRule rule62; + RewriteRule rule63; + RewriteRule rule64; + RewriteRule rule65; + RewriteRule rule66; + RewriteRule rule67; + RewriteRule rule68; + RewriteRule rule69; + RewriteRule rule70; + RewriteRule rule71; + RewriteRule rule72; + RewriteRule rule73; + RewriteRule rule74; + RewriteRule rule75; + RewriteRule rule76; + RewriteRule rule77; + RewriteRule rule78; + RewriteRule rule79; + RewriteRule rule80; + RewriteRule rule81; + RewriteRule rule82; + RewriteRule rule83; + RewriteRule rule84; + RewriteRule rule85; RewriteRule rule86; - RewriteRule rule87; - RewriteRule rule88; - RewriteRule rule91; - RewriteRule rule92; - RewriteRule rule93; - RewriteRule rule94; - RewriteRule rule95; - RewriteRule rule96; - RewriteRule rule97; - RewriteRule rule98; - RewriteRule rule99; - RewriteRule rule100; - RewriteRule rule101; - RewriteRule rule102; - RewriteRule rule103; - RewriteRule rule104; - RewriteRule rule105; - RewriteRule rule106; - RewriteRule rule107; - RewriteRule rule108; - RewriteRule rule109; - RewriteRule rule110; - RewriteRule rule111; - RewriteRule rule112; - RewriteRule rule113; - RewriteRule rule114; - RewriteRule rule115; - RewriteRule rule116; - RewriteRule rule117; - RewriteRule rule118; - RewriteRule rule119; - RewriteRule rule120; - RewriteRule rule121; - RewriteRule rule122; - RewriteRule rule123; - RewriteRule rule124; - RewriteRule rule125; - RewriteRule rule126; - RewriteRule rule127; - RewriteRule rule128; - RewriteRule rule129; - RewriteRule rule130; + RewriteRule rule87; + RewriteRule rule88; + RewriteRule rule91; + RewriteRule rule92; + RewriteRule rule93; + RewriteRule rule94; + RewriteRule rule95; + RewriteRule rule96; + RewriteRule rule97; + RewriteRule rule98; + RewriteRule rule99; + RewriteRule rule100; + RewriteRule rule101; + RewriteRule rule102; + RewriteRule rule103; + RewriteRule rule104; + RewriteRule rule105; + RewriteRule rule106; + RewriteRule rule107; + RewriteRule rule108; + RewriteRule rule109; + RewriteRule rule110; + RewriteRule rule111; + RewriteRule rule112; + RewriteRule rule113; + RewriteRule rule114; + RewriteRule rule115; + RewriteRule rule116; + RewriteRule rule117; + RewriteRule rule118; + RewriteRule rule119; + RewriteRule rule120; + RewriteRule rule121; + RewriteRule rule122; + RewriteRule rule123; + RewriteRule rule124; + RewriteRule rule125; + RewriteRule rule126; + RewriteRule rule127; + RewriteRule rule128; + RewriteRule rule129; + RewriteRule rule130; + RewriteRule rule131; + RewriteRule 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,23 +30,43 @@ namespace bv { // FIXME: this rules subsume the constant evaluation ones /** - * BvIte + * BvIteConstCond * * BITVECTOR_ITE with constant condition */ template <> -inline bool RewriteRule::applies(TNode node) +inline bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst()); } template <> -inline Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; return utils::isZero(node[0]) ? node[2] : node[1]; } +/** + * BvIteChildren + * + * BITVECTOR_ITE with term_then = term_else + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" + << std::endl; + return node[1]; +} + /** * BvComp * 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 >::apply( - node); + LinearRewriteStrategy, + RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } -- 2.30.2