Not working

The rewriter is not an envobj and so i don't have access to the options.
yoni206 · Aug 18, 2024 · c29ee6e · c29ee6e
1 parent 71f9fdd
commit c29ee6e
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 9 deletions.
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
@@ -23,7 +23,6 @@
 #include "theory/bv/bv_solver_bitblast_internal.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
 #include "theory/trust_substitutions.h"

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
@@ -15,8 +15,8 @@
 
 #include "theory/bv/theory_bv_rewriter.h"
 
-#include "options/smt_options.h"
 #include "options/bv_options.h"
+#include "options/smt_options.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h"
 #include "theory/bv/theory_bv_rewrite_rules_core.h"
@@ -28,7 +28,7 @@
 using namespace cvc5::internal;
 using namespace cvc5::internal::theory;
 using namespace cvc5::internal::theory::bv;
-using namespace cvc5::context;
+
 
 TheoryBVRewriter::TheoryBVRewriter(NodeManager* nm) : TheoryRewriter(nm)
 {
@@ -100,13 +100,16 @@ Node TheoryBVRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
 }
 
 TrustNode TheoryBVRewriter::expandDefinition(Node node) {
-  Node expanded = eliminateOverflows(node);
-    return TrustNode::mkTrustRewrite(node, expanded, nullptr);
+  Node expanded = node;
+  if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF) {
+    expanded = eliminateOverflows(node);
+  } 
+  return TrustNode::mkTrustRewrite(node, expanded, nullptr);
 }
 
 Node TheoryBVRewriter::eliminateOverflows(Node node) {
-  Node res = node;
-   if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF) {
+   Node res = node;
+   if (true) {
      if (RewriteRule<UaddoEliminate>::applies(node))
      {
        res = RewriteRule<UaddoEliminate>::run<false>(node);

diff --git a/test/regress/cli/regress0/bv/overflow/saddo3.smt2 b/test/regress/cli/regress0/bv/overflow/saddo3.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-const v (_ BitVec 6))
-(assert (and (bvsgt v (_ bv53 6)) (not (bvsaddo v v))))
+(assert (and (bvsgt v (_ bv28 6)) (not (bvsaddo v v))))
 (check-sat)
diff --git a/test/regress/cli/regress0/bv/overflow/ssubo1.smt2 b/test/regress/cli/regress0/bv/overflow/ssubo1.smt2
@@ -4,5 +4,5 @@
 (set-logic QF_BV)
 (declare-const u (_ BitVec 6))
 (declare-const v (_ BitVec 6))
-(assert (and (bvsgt v u) (not (bvssubo u v))))
+(assert (and (bvugt v (_ bv22 6)) (bvugt (_ bv0 6) u) (not (bvssubo v u))))
 (check-sat)