From 9e5dcf3ecb348460bda8b5ff7da89c37fa364919 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Jul 2021 16:17:59 +0200
Subject: [PATCH] bound length of ubv2s

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_axioms.cpp   | 18 ++++++++++++++++++
 src/ast/rewriter/seq_axioms.h     |  1 +
 src/ast/rewriter/seq_rewriter.cpp |  1 +
 src/smt/seq_axioms.h              |  1 +
 src/smt/theory_seq.cpp            |  1 +
 5 files changed, 22 insertions(+)

diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 4c8cd932d..d3bc217a3 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -799,6 +799,24 @@ namespace seq {
             add_clause(~ge10k, ge10k1, eq);
     }
 
+    /*
+    * 1 <= len(ubv2s(b)) <= k, where k is min such that 10^k > 2^sz
+    */
+    void axioms::ubv2s_len_axiom(expr* b) {
+        bv_util bv(m);
+        sort* bv_sort = b->get_sort();
+        unsigned sz = bv.get_bv_size(bv_sort);
+        unsigned k = 1;
+        rational pow(10);
+        while (pow <= rational::power_of_two(sz))
+            ++k, pow *= 10;
+        expr_ref len(seq.str.mk_length(seq.str.mk_ubv2s(b)), m);
+        expr_ref ge(a.mk_ge(len, a.mk_int(1)), m);
+        expr_ref le(a.mk_le(len, a.mk_int(k)), m);
+        add_clause(le);
+        add_clause(ge);
+    }
+
     /*
     *   len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k}   k > 1
     *   len(ubv2s(b)) = 1 =>  b < 10^{1}   k = 1
diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h
index c9cdbfc9a..6cd83b00f 100644
--- a/src/ast/rewriter/seq_axioms.h
+++ b/src/ast/rewriter/seq_axioms.h
@@ -96,6 +96,7 @@ namespace seq {
         void itos_axiom(expr* s, unsigned k);
         void ubv2s_axiom(expr* b, unsigned k);
         void ubv2s_len_axiom(expr* b, unsigned k);
+        void ubv2s_len_axiom(expr* b);
         void ubv2ch_axiom(sort* bv_sort);
         void lt_axiom(expr* n);
         void le_axiom(expr* n);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 5555f8439..dcea166cd 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3363,6 +3363,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         }
         expr* e1 = nullptr, *e2 = nullptr;
         if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) {
+  	    SASSERT(u().is_char(e1));
             // Use mk_der_cond to normalize
             STRACE("seq_verbose", tout << "deriv range str" << std::endl;);
             expr_ref p1(u().mk_le(e1, ele), m());
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index c5aa68e0a..e9fc3cb53 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -81,6 +81,7 @@ namespace smt {
         void add_itos_axiom(expr* s, unsigned k) { m_ax.itos_axiom(s, k); }
         void add_ubv2s_axiom(expr* b, unsigned k) { m_ax.ubv2s_axiom(b, k); }
         void add_ubv2s_len_axiom(expr* b, unsigned k) { m_ax.ubv2s_len_axiom(b, k); }
+        void add_ubv2s_len_axiom(expr* b) { m_ax.ubv2s_len_axiom(b); }
         void add_ubv2ch_axioms(sort* s) { m_ax.ubv2ch_axiom(s); }
         void add_lt_axiom(expr* n) { m_ax.lt_axiom(n); }
         void add_le_axiom(expr* n) { m_ax.le_axiom(n); }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 436752aa7..ba9f7c8fd 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1542,6 +1542,7 @@ void theory_seq::add_ubv_string(expr* e) {
     }
     if (!has_sort)
         m_ax.add_ubv2ch_axioms(b->get_sort());
+    m_ax.add_ubv2s_len_axiom(b);
     m_ubv_string.push_back(e);
     m_trail_stack.push(push_back_vector<expr_ref_vector>(m_ubv_string));
     add_length_to_eqc(e);