bound length of ubv2s

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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);

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());

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); }

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);