not good

src/options/uf_options.toml

@@ -84,17 +84,16 @@ name   = "Uninterpreted Functions Theory"
   help       = "eagerly expand bit-vector to arithmetic conversions during preprocessing"
 
 [[option]]
-  name       = "bv2natPlusDistRR"
+  name       = "arithBvConvMode"
   category   = "expert"
-  long       = "bv2nat-plus-dist-rr"
-  type       = "bool"
-  default    = "false"
-  help       = "distribute bv2nat over addition in a rewrite rule"
-
-[[option]]
-  name       = "modelBasedArithBvConv"
-  category   = "expert"
-  long       = "model-based-arith-bv-conv"
-  type       = "bool"
-  default    = "false"
+  long       = "model-based-arith-bv-conv=MODE"
+  type       = "ArithBVConvMode"
+  default    = "VALUES"
   help       = "model-based inferences for bit-vector to arithmetic conversions"
+  help_mode  = "How to convert"
+[[option.mode.VALUES]]
+  name = "values"
+  help = "model values"
+[[option.mode.LEMMAS]]
+  name = "lemmas"
+  help = "lemmas"

src/theory/uf/conversions_solver.cpp

@@ -77,28 +77,35 @@ void ConversionsSolver::checkReduction(Node n)
     Trace("bv-convs") << "...already correct in model" << std::endl;
     return;
   }
-  if (options().uf.modelBasedArithBvConv)
+  NodeManager* nm = NodeManager::currentNM();
+  if (options().uf.arithBvConvMode == options::ArithBVConvMode::VALUES)
   {
-    NodeManager* nm = NodeManager::currentNM();
     Node argval = d_state.getModel()->getValue(n[0]);
     Trace("bv-convs-debug") << "  arg value = " << argval << std::endl;
     Node eval = rewrite(nm->mkNode(n.getOperator(), argval));
     Trace("bv-convs-debug") << "  evaluated = " << eval << std::endl;
     Node lem = nm->mkNode(Kind::IMPLIES, n[0].eqNode(argval), n.eqNode(eval));
     d_im.lemma(lem, InferenceId::UF_ARITH_BV_CONV_VALUE_REFINE);
 
-    if (n.getKind() == Kind::BITVECTOR_TO_NAT) {
-      Node zero = nm->mkConstInt(Rational(0));
-      uint32_t k = n[0].getType().getBitVectorSize();
-      Node max_val = nm->mkConstInt(Rational(Integer(2).pow(k)));
 
-      Node lower_bound = nm->mkNode(Kind::LEQ, zero, n);
-      Node upper_bound = nm->mkNode(Kind::LEQ, n, max_val);
-      Node range_lemma = nm->mkNode(Kind::AND, lower_bound, upper_bound);
+    return;
+  }
+
+
+  if ((options().uf.arithBvConvMode == options::ArithBVConvMode::LEMMAS) && n.getKind() == Kind::BITVECTOR_TO_NAT) {
+    Node zero = nm->mkConstInt(Rational(0));
+    uint32_t k = n[0].getType().getBitVectorSize();
+    Node max_val = nm->mkConstInt(Rational(Integer(2).pow(k)));
+
+    Node lower_bound = nm->mkNode(Kind::LEQ, zero, n);
+    Node upper_bound = nm->mkNode(Kind::LEQ, n, max_val);
+    Node range_lemma = nm->mkNode(Kind::AND, lower_bound, upper_bound);
+    std::cout << "panda " << d_state.getModel()->getValue(range_lemma)  << std::endl;
+    //if (d_state.getModel()->getValue(range_lemma) == nm->mkConst(false)) 
+    {
       d_im.lemma(range_lemma, InferenceId::UF_ARITH_BV_CONV_RANGE);
+      return;
     }
-
-    return;
   }
 
   Node lem;

src/theory/uf/theory_uf_rewriter.cpp

@@ -336,7 +336,7 @@ RewriteResponse TheoryUfRewriter::rewriteBVToNat(TNode node)
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
   }
   else if (node[0].getKind() == Kind::BITVECTOR_ADD) {
-    // if (options().uf.bv2natPlusDistRR) 
+    //if (options().uf.bv2natDistRR) 
     {
       std::vector<Node> bv2nats;
       for (Node child : node[0]) {
@@ -350,6 +350,45 @@ RewriteResponse TheoryUfRewriter::rewriteBVToNat(TNode node)
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
     }
   }
+  else if (node[0].getKind() == Kind::BITVECTOR_MULT) {
+    //if (options().uf.bv2natDistRR) 
+    {
+      std::vector<Node> bv2nats;
+      for (Node child : node[0]) {
+        Node bv2nat = nm->mkNode(Kind::BITVECTOR_TO_NAT, child);
+        bv2nats.push_back(bv2nat);
+      }
+      const uint32_t size = node[0].getType().getBitVectorSize();
+      Node twottsize = nm->mkConstInt(Rational(Integer(2).pow(size)));
+      Node multiplication = nm->mkNode(Kind::MULT, bv2nats);
+      Node resultNode = nm->mkNode(Kind::INTS_MODULUS_TOTAL, multiplication, twottsize);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+    }
+  }
+  else if (node[0].getKind() == Kind::BITVECTOR_NEG) {
+    //if (options().uf.bv2natDistRR) 
+    {
+      Node child = node[0][0];
+      Node bv2nat = nm->mkNode(Kind::BITVECTOR_TO_NAT, child);
+      Node plusOne = nm->mkNode(Kind::ADD, bv2nat, nm->mkConstInt(Rational(Integer(2))));
+      const uint32_t size = node[0].getType().getBitVectorSize();
+      Node twottsize = nm->mkConstInt(Rational(Integer(2).pow(size)));
+      Node resultNode = nm->mkNode(Kind::SUB, twottsize, plusOne);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+    }
+  }
+  else if (node[0].getKind() == Kind::BITVECTOR_NOT) {
+    //if (options().uf.bv2natDistRR) 
+    {
+      Node child = node[0][0];
+      Node bv2nat = nm->mkNode(Kind::BITVECTOR_TO_NAT, child);
+      const uint32_t size = node[0].getType().getBitVectorSize();
+      Node twottsize = nm->mkConstInt(Rational(Integer(2).pow(size)));
+      Node sub = nm->mkNode(Kind::SUB, twottsize, bv2nat);
+      Node resultNode = nm->mkNode(Kind::INTS_MODULUS_TOTAL, sub, twottsize);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+    }
+  }
   return RewriteResponse(REWRITE_DONE, node);
 }
 

test/regress/cli/regress0/bv-conv-value-refine.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --model-based-arith-bv-conv
+; COMMAND-LINE: --model-based-arith-bv-conv=values
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun x () (_ BitVec 8))

test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2

@@ -1,8 +1,8 @@
-; COMMAND-LINE: --model-based-arith-bv-conv
+; COMMAND-LINE: --model-based-arith-bv-conv=lemmas
 ; EXPECT: unsat
 (set-logic ALL)
-(declare-fun x () (_ BitVec 4000))
-(declare-fun y () (_ BitVec 4000))
+(declare-fun x () (_ BitVec 4))
+(declare-fun y () (_ BitVec 4))
 (assert (< (bv2nat x) (bv2nat y) ))
 (assert (= (+ (bv2nat x) (bv2nat y)) 0))
 (check-sat)

test/regress/cli/regress0/bv2nat_reflection1.smt2

@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --model-based-arith-bv-conv
+; COMMAND-LINE: --model-based-arith-bv-conv=values
 (set-logic ALL)
 (declare-fun x () (_ BitVec 4000))
 (declare-fun y () (_ BitVec 4000))