From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Nov 2016 14:55:14 +0000 (-0600)
Subject: Add option for enabling/disabling lazy extended function reduction in bitvectors.
X-Git-Tag: cvc5-1.0.0~5991
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8142799520aa07d6134314761de9d47ac14d27b0;p=cvc5.git

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

diff --git a/src/options/bv_options b/src/options/bv_options
index 2e6fa2e7a..341060b37 100644
--- 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 d726b836f..e46511e59 100644
--- 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 7b9bdf14f..4c6afa7b9 100644
--- 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);