diff options
-rw-r--r-- | src/theory/bv/options | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 11 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/bv/options b/src/theory/bv/options index 775a46088..801dec0db 100644 --- 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 dc91c338b..86f2c6760 100644 --- 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 |