Add option for enabling/disabling lazy extended function reduction in bitvectors.

diff --git a/src/options/bv_options b/src/options/bv_options
index 2e6fa2e7a1e27c0e3d15dd75f66d9169c2820ba8..341060b374a5a35caccc36bcf86ea3a1986892df 100644 (file)
--- a/src/options/bv_options
+++ b/src/options/bv_options
@@ -69,4 +69,7 @@ expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false
 expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false
  introduce bitvector powers of two as a preprocessing pass
 
+option bvLazyRewriteExtf --bv-lazy-rewrite-extf bool :default true :read-write
+ lazily rewrite extended functions like bv2nat and int2bv
+ 
 endmodule

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d726b836fc1a44b842c038326c6764cede5698e5..e46511e59e863ffbe810b2b98c916247f3494ec8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1594,6 +1594,11 @@ void SmtEngine::setDefaults() {
     Trace("smt") << "enabling eager bit-vector explanations " << endl;
     options::bvEagerExplanations.set(true);
   }
+  
+  if( !options::bitvectorEqualitySolver() ){
+    Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << endl;
+    options::bvLazyRewriteExtf.set(false);
+  }
 
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! options::arithRewriteEq.wasSetByUser()) {

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 7b9bdf14fe89d2f11ce741ce0dfef7c3133a89e1..4c6afa7b9142a141ea4dc1efe93f22398c9a4d23 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -571,7 +571,7 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
 
 RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
   //do not use lazy rewrite strategy if equality solver is disabled
-  if( node[0].isConst() || !options::bitvectorEqualitySolver() ){
+  if( node[0].isConst() || !options::bvLazyRewriteExtf() ){
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<BVToNatEliminate>
       >::apply(node);
@@ -583,7 +583,7 @@ RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
 
 RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
   //do not use lazy rewrite strategy if equality solver is disabled
-  if( node[0].isConst() || !options::bitvectorEqualitySolver() ){
+  if( node[0].isConst() || !options::bvLazyRewriteExtf() ){
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<IntToBVEliminate>
       >::apply(node);