diff options
author | lianah <lianahady@gmail.com> | 2014-11-17 18:40:26 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-11-17 18:40:26 -0500 |
commit | d9923e1928a158c915a71ce0addb766a1e9986ca (patch) | |
tree | c74f985ee34b55c3a1e79bd277aca237fe992914 /src/theory/bv | |
parent | e5e33a2de5419da0d9e43746871224eeb48bd5ed (diff) |
added command line option for extractArith bv rewrite
Diffstat (limited to 'src/theory/bv')
-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 |