added command line option for extractArith bv rewrite

diff --git a/src/theory/bv/options b/src/theory/bv/options
index 775a460880a9082d3b9640c44a97150938b08ce7..801dec0db9ba562dafa0c291b4e5009eb18d8f1d 100644 (file)
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -45,6 +45,9 @@ option bitvectorToBool --bv-to-bool bool :default false :read-write
 option bitvectorDivByZeroConst --bv-div-zero-const bool :default false
  always return -1 on division by zero
 
+expert-option bvExtractArithRewrite --bv-extract-arith bool :default false :read-write
+ enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)
+ 
 expert-option bvAbstraction --bv-abstraction bool :default false :read-write
  mcm benchmark abstraction 
 

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index dc91c338b23ca1db19f001a880e184e66681b885..86f2c676017031d62c91cef0a2492014b8fea8d3 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -16,6 +16,7 @@
  **/
 
 #include "theory/theory.h"
+#include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_rewrite_rules_core.h"
@@ -178,10 +179,12 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
 
-  // if (RewriteRule<ExtractArith>::applies(node)) {
-  //   resultNode = RewriteRule<ExtractArith>::run<false>(node);
-  //   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  // }
+  if (options::bvExtractArithRewrite()) {
+    if (RewriteRule<ExtractArith>::applies(node)) {
+      resultNode = RewriteRule<ExtractArith>::run<false>(node);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
+  }
 
   
   resultNode = LinearRewriteStrategy