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 80974b2a577738c160765323df12124784aa6c8e..0ae082adc5b43a8741245124d7806acb6c02abb6 100644 (file)
--- 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<UgtEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<UgtEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_UGT);
 }
 
 template <>
-Node RewriteRule<UgtEliminate>::apply(TNode node)
+inline Node RewriteRule<UgtEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<UgtEliminate>(" << node << ")"
                       << std::endl;
@@ -42,13 +44,14 @@ Node RewriteRule<UgtEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<UgeEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<UgeEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_UGE);
 }
 
 template <>
-Node RewriteRule<UgeEliminate>::apply(TNode node)
+inline Node RewriteRule<UgeEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<UgeEliminate>(" << node << ")"
                       << std::endl;
@@ -58,13 +61,14 @@ Node RewriteRule<UgeEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<SgtEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SgtEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SGT);
 }
 
 template <>
-Node RewriteRule<SgtEliminate>::apply(TNode node)
+inline Node RewriteRule<SgtEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")"
                       << std::endl;
@@ -74,13 +78,14 @@ Node RewriteRule<SgtEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<SgeEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SgeEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SGE);
 }
 
 template <>
-Node RewriteRule<SgeEliminate>::apply(TNode node)
+inline Node RewriteRule<SgeEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SgeEliminate>(" << node << ")"
                       << std::endl;
@@ -91,12 +96,13 @@ Node RewriteRule<SgeEliminate>::apply(TNode node)
 }
 
 template <>
-bool RewriteRule<SltEliminate>::applies(TNode node) {
+inline bool RewriteRule<SltEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SLT); 
 }
 
 template <>
-Node RewriteRule<SltEliminate>::apply(TNode node)
+inline Node RewriteRule<SltEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SltEliminate>(" << node << ")"
                       << std::endl;
@@ -111,12 +117,13 @@ Node RewriteRule<SltEliminate>::apply(TNode node)
 }
 
 template <>
-bool RewriteRule<SleEliminate>::applies(TNode node) {
+inline bool RewriteRule<SleEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SLE); 
 }
 
 template <>
-Node RewriteRule<SleEliminate>::apply(TNode node)
+inline Node RewriteRule<SleEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")"
                       << std::endl;
@@ -128,12 +135,13 @@ Node RewriteRule<SleEliminate>::apply(TNode node)
 }
 
 template <>
-bool RewriteRule<UleEliminate>::applies(TNode node) {
+inline bool RewriteRule<UleEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_ULE); 
 }
 
 template <>
-Node RewriteRule<UleEliminate>::apply(TNode node)
+inline Node RewriteRule<UleEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")"
                       << std::endl;
@@ -145,12 +153,13 @@ Node RewriteRule<UleEliminate>::apply(TNode node)
 }
 
 template <>
-bool RewriteRule<CompEliminate>::applies(TNode node) {
+inline bool RewriteRule<CompEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_COMP); 
 }
 
 template <>
-Node RewriteRule<CompEliminate>::apply(TNode node)
+inline Node RewriteRule<CompEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<CompEliminate>(" << node << ")"
                       << std::endl;
@@ -163,12 +172,13 @@ Node RewriteRule<CompEliminate>::apply(TNode node)
 }
 
 template <>
-bool RewriteRule<SubEliminate>::applies(TNode node) {
+inline bool RewriteRule<SubEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SUB); 
 }
 
 template <>
-Node RewriteRule<SubEliminate>::apply(TNode node)
+inline Node RewriteRule<SubEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SubEliminate>(" << node << ")"
                       << std::endl;
@@ -179,13 +189,15 @@ Node RewriteRule<SubEliminate>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_PLUS, a, negb);
 }
 
-template<>
-bool RewriteRule<RepeatEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<RepeatEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_REPEAT);
 }
 
-template<>
-Node RewriteRule<RepeatEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<RepeatEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<RepeatEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRepeat>().repeatAmount;
@@ -201,13 +213,15 @@ Node RewriteRule<RepeatEliminate>::apply(TNode node) {
   return resultNode;
 }
 
-template<>
-bool RewriteRule<RotateLeftEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<RotateLeftEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT);
 }
 
-template<>
-Node RewriteRule<RotateLeftEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<RotateLeftEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<RotateLeftEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
@@ -223,13 +237,15 @@ Node RewriteRule<RotateLeftEliminate>::apply(TNode node) {
   return result;
 }
 
-template<>
-bool RewriteRule<RotateRightEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<RotateRightEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT);
 }
 
-template<>
-Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<RotateRightEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<RotateRightEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned amount = node.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
@@ -245,13 +261,15 @@ Node RewriteRule<RotateRightEliminate>::apply(TNode node) {
   return result;
 }
 
-template<>
-bool RewriteRule<BVToNatEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<BVToNatEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_TO_NAT);
 }
 
-template<>
-Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<BVToNatEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
 
   //if( node[0].isConst() ){
@@ -273,13 +291,15 @@ Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
   return Node(result);
 }
 
-template<>
-bool RewriteRule<IntToBVEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<IntToBVEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::INT_TO_BITVECTOR);
 }
 
-template<>
-Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<IntToBVEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
 
   //if( node[0].isConst() ){
@@ -304,14 +324,15 @@ Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
   return Node(result);
 }
 
-template<>
-bool RewriteRule<NandEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<NandEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_NAND &&
           node.getNumChildren() == 2);
 }
 
 template <>
-Node RewriteRule<NandEliminate>::apply(TNode node)
+inline Node RewriteRule<NandEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<NandEliminate>(" << node << ")"
                       << std::endl;
@@ -324,13 +345,13 @@ Node RewriteRule<NandEliminate>::apply(TNode node)
 }
 
 template <>
-bool RewriteRule<NorEliminate>::applies(TNode node)
+inline bool RewriteRule<NorEliminate>::applies(TNode node)
 {
   return (node.getKind() == kind::BITVECTOR_NOR && node.getNumChildren() == 2);
 }
 
 template <>
-Node RewriteRule<NorEliminate>::apply(TNode node)
+inline Node RewriteRule<NorEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<NorEliminate>(" << node << ")"
                       << std::endl;
@@ -342,14 +363,15 @@ Node RewriteRule<NorEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<XnorEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<XnorEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_XNOR &&
           node.getNumChildren() == 2);
 }
 
 template <>
-Node RewriteRule<XnorEliminate>::apply(TNode node)
+inline Node RewriteRule<XnorEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<XnorEliminate>(" << node << ")"
                       << std::endl;
@@ -361,13 +383,14 @@ Node RewriteRule<XnorEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<SdivEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SdivEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SDIV);
 }
 
 template <>
-Node RewriteRule<SdivEliminate>::apply(TNode node)
+inline Node RewriteRule<SdivEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SdivEliminate>(" << node << ")"
                       << std::endl;
@@ -400,13 +423,14 @@ Node RewriteRule<SdivEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<SremEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SremEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SREM);
 }
 
 template <>
-Node RewriteRule<SremEliminate>::apply(TNode node)
+inline Node RewriteRule<SremEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SremEliminate>(" << node << ")"
                       << std::endl;
@@ -437,13 +461,14 @@ Node RewriteRule<SremEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<SmodEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SmodEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SMOD);
 }
 
 template <>
-Node RewriteRule<SmodEliminate>::apply(TNode node)
+inline Node RewriteRule<SmodEliminate>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<SmodEliminate>(" << node << ")"
                       << std::endl;
@@ -498,13 +523,15 @@ Node RewriteRule<SmodEliminate>::apply(TNode node)
   return result;
 }
 
-template<>
-bool RewriteRule<ZeroExtendEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<ZeroExtendEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); 
 }
 
-template<>
-Node RewriteRule<ZeroExtendEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<ZeroExtendEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<ZeroExtendEliminate>(" << node << ")" << std::endl;
 
   TNode bv = node[0];
@@ -518,13 +545,15 @@ Node RewriteRule<ZeroExtendEliminate>::apply(TNode node) {
   return result;
 }
 
-template<>
-bool RewriteRule<SignExtendEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<SignExtendEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND); 
 }
 
-template<>
-Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<SignExtendEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<SignExtendEliminate>(" << node << ")" << std::endl;
 
   unsigned amount = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
@@ -538,13 +567,15 @@ Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
   return utils::mkConcat(extension, node[0]);
 }
 
-template<>
-bool RewriteRule<RedorEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<RedorEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_REDOR);
 }
 
-template<>
-Node RewriteRule<RedorEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<RedorEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned size = utils::getSize(node[0]); 
@@ -552,13 +583,15 @@ Node RewriteRule<RedorEliminate>::apply(TNode node) {
   return result.negate();
 }
 
-template<>
-bool RewriteRule<RedandEliminate>::applies(TNode node) {
+template <>
+inline bool RewriteRule<RedandEliminate>::applies(TNode node)
+{
   return (node.getKind() == kind::BITVECTOR_REDAND);
 }
 
-template<>
-Node RewriteRule<RedandEliminate>::apply(TNode node) {
+template <>
+inline Node RewriteRule<RedandEliminate>::apply(TNode node)
+{
   Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned size = utils::getSize(node[0]);