From: yoni206 Date: Mon, 29 Jul 2019 15:30:25 +0000 (-0700) Subject: Refactoring of bit-vector elimination rules (#3105) X-Git-Tag: cvc5-1.0.0~4073 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b83b9c3ee265881c24ee6845cef011ebad1e1da;p=cvc5.git Refactoring of bit-vector elimination rules (#3105) This commit makes the following minor refactors to src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h: - Including options/bv_options.h: this is needed because this header file is being used. - Marking all functions as inline: details in a discussion inside the PR. --- diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 80974b2a5..0ae082adc 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -19,6 +19,7 @@ #pragma once +#include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" @@ -26,13 +27,14 @@ namespace CVC4 { namespace theory { namespace bv { -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_UGT); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -42,13 +44,14 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_UGE); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -58,13 +61,14 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SGT); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -74,13 +78,14 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SGE); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -91,12 +96,13 @@ Node RewriteRule::apply(TNode node) } template <> -bool RewriteRule::applies(TNode node) { +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SLT); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -111,12 +117,13 @@ Node RewriteRule::apply(TNode node) } template <> -bool RewriteRule::applies(TNode node) { +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SLE); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -128,12 +135,13 @@ Node RewriteRule::apply(TNode node) } template <> -bool RewriteRule::applies(TNode node) { +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_ULE); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -145,12 +153,13 @@ Node RewriteRule::apply(TNode node) } template <> -bool RewriteRule::applies(TNode node) { +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_COMP); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -163,12 +172,13 @@ Node RewriteRule::apply(TNode node) } template <> -bool RewriteRule::applies(TNode node) { +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SUB); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -179,13 +189,15 @@ Node RewriteRule::apply(TNode node) return nm->mkNode(kind::BITVECTOR_PLUS, a, negb); } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_REPEAT); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode a = node[0]; unsigned amount = node.getOperator().getConst().repeatAmount; @@ -201,13 +213,15 @@ Node RewriteRule::apply(TNode node) { return resultNode; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode a = node[0]; unsigned amount = node.getOperator().getConst().rotateLeftAmount; @@ -223,13 +237,15 @@ Node RewriteRule::apply(TNode node) { return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode a = node[0]; unsigned amount = node.getOperator().getConst().rotateRightAmount; @@ -245,13 +261,15 @@ Node RewriteRule::apply(TNode node) { return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_TO_NAT); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; //if( node[0].isConst() ){ @@ -273,13 +291,15 @@ Node RewriteRule::apply(TNode node) { return Node(result); } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::INT_TO_BITVECTOR); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; //if( node[0].isConst() ){ @@ -304,14 +324,15 @@ Node RewriteRule::apply(TNode node) { return Node(result); } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_NAND && node.getNumChildren() == 2); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -324,13 +345,13 @@ Node RewriteRule::apply(TNode node) } template <> -bool RewriteRule::applies(TNode node) +inline bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_NOR && node.getNumChildren() == 2); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -342,14 +363,15 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_XNOR && node.getNumChildren() == 2); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -361,13 +383,14 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SDIV); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -400,13 +423,14 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SREM); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -437,13 +461,14 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SMOD); } template <> -Node RewriteRule::apply(TNode node) +inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; @@ -498,13 +523,15 @@ Node RewriteRule::apply(TNode node) return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode bv = node[0]; @@ -518,13 +545,15 @@ Node RewriteRule::apply(TNode node) { return result; } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; unsigned amount = node.getOperator().getConst().signExtendAmount; @@ -538,13 +567,15 @@ Node RewriteRule::apply(TNode node) { return utils::mkConcat(extension, node[0]); } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_REDOR); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode a = node[0]; unsigned size = utils::getSize(node[0]); @@ -552,13 +583,15 @@ Node RewriteRule::apply(TNode node) { return result.negate(); } -template<> -bool RewriteRule::applies(TNode node) { +template <> +inline bool RewriteRule::applies(TNode node) +{ return (node.getKind() == kind::BITVECTOR_REDAND); } -template<> -Node RewriteRule::apply(TNode node) { +template <> +inline Node RewriteRule::apply(TNode node) +{ Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode a = node[0]; unsigned size = utils::getSize(node[0]);