Added sbv2s (#5413)

* Added sbv2s

* Fixed indention

Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>

src/api/api_ast.cpp

@@ -1203,6 +1203,7 @@ extern "C" {
             case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
             case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
             case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
+            case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR;
             case OP_STRING_LT: return Z3_OP_STRING_LT;
             case OP_STRING_LE: return Z3_OP_STRING_LE;
 

src/api/api_seq.cpp

@@ -245,6 +245,7 @@ extern "C" {
     MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP);
     MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP);
     MK_UNARY(Z3_mk_ubv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_UBVTOS, SKIP);
+    MK_UNARY(Z3_mk_sbv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_SBVTOS, SKIP);
 
 
     Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {

src/api/c++/z3++.h

@@ -1447,6 +1447,11 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr sbvtos() const {
+            Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
  
         friend expr range(expr const& lo, expr const& hi);
         /**

src/api/dotnet/Context.cs

@@ -2405,6 +2405,15 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
         }
 
+        /// <summary>
+        /// Convert a bit-vector expression, represented as an signed number, to a string.
+        /// </summary>
+        public SeqExpr SbvToString(Expr e) {
+            Debug.Assert(e != null);
+            Debug.Assert(e is ArithExpr);
+            return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
+        }
+
         /// <summary>
         /// Convert an integer expression to a string.
         /// </summary>

src/api/java/Context.java

@@ -2036,6 +2036,14 @@ public class Context implements AutoCloseable {
 	return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
     }
     
+    /**
+     * Convert an signed bitvector expression to a string.
+     */
+    public SeqExpr<CharSort> sbvToString(Expr<BitVecSort> e)
+    {
+    return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
+    }
+    
     /**
      * Convert an integer expression to a string.
      */

src/api/z3_api.h

@@ -1203,6 +1203,7 @@ typedef enum {
     Z3_OP_STR_TO_INT,
     Z3_OP_INT_TO_STR,
     Z3_OP_UBV_TO_STR,
+    Z3_OP_SBV_TO_STR,
     Z3_OP_STRING_LT,
     Z3_OP_STRING_LE,
 
@@ -3655,6 +3656,12 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s);
   
+    /**
+       \brief Signed bit-vector to string conversion.
+
+       def_API('Z3_mk_sbv_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s);
 
     /**
        \brief Create a regular expression that accepts the sequence \c seq.

src/ast/bv_decl_plugin.h

@@ -406,6 +406,7 @@ public:
 
     app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); }
     app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); }
+    app * mk_slt(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLT, arg1, arg2); }
     app * mk_extract(unsigned high, unsigned low, expr * n) {
         parameter params[2] = { parameter(high), parameter(low) };
         return m_manager.mk_app(get_fid(), OP_EXTRACT, 2, params, 1, &n);

src/ast/rewriter/seq_rewriter.cpp

@@ -718,6 +718,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 1);
         st = mk_str_ubv2s(args[0], result);
         break;
+    case OP_STRING_SBVTOS:
+      SASSERT(num_args == 1);
+      st = mk_str_sbv2s(args[0], result);
+      break;
     case _OP_STRING_CONCAT:
     case _OP_STRING_PREFIX:
     case _OP_STRING_SUFFIX:
@@ -2218,6 +2222,30 @@ br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_str_sbv2s(expr *a, expr_ref &result) {
+    bv_util bv(m());
+    rational val;
+    unsigned bv_size = 0;
+    if (bv.is_numeral(a, val, bv_size)) {
+        rational r = mod(val, rational::power_of_two(bv_size));
+        SASSERT(!r.is_neg());
+        if (r >= rational::power_of_two(bv_size - 1)) {
+            r -= rational::power_of_two(bv_size);
+        }
+        result = str().mk_string(zstring(r));
+        return BR_DONE;
+    }
+    
+    bv_size = bv.get_bv_size(a);
+    result = m().mk_ite(
+        bv.mk_slt(a,bv.mk_numeral(0, bv_size)),
+        str().mk_concat(
+            str().mk_string(zstring("-")),
+            str().mk_ubv2s(bv.mk_bv_neg(a))
+        ),
+        str().mk_ubv2s(a));
+    return BR_REWRITE_FULL;
+}
 
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
     rational r;

src/ast/rewriter/seq_rewriter.h

@@ -229,6 +229,7 @@ class seq_rewriter {
     br_status mk_str_itos(expr* a, expr_ref& result);
     br_status mk_str_stoi(expr* a, expr_ref& result);
     br_status mk_str_ubv2s(expr* a, expr_ref& result);
+    br_status mk_str_sbv2s(expr* a, expr_ref& result);
     br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
     br_status mk_str_to_regexp(expr* a, expr_ref& result);
     br_status mk_str_le(expr* a, expr* b, expr_ref& result);

src/ast/seq_decl_plugin.cpp

@@ -350,7 +350,7 @@ func_decl* seq_decl_plugin::mk_left_assoc_fun(decl_kind k, unsigned arity, sort*
     return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, false);
 }
 
-func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) {
+func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) const {
     ast_manager& m = *m_manager;
     if (arity != 1)
         m.raise_exception("Invalid str.from_ubv expects one bit-vector argument");
@@ -361,6 +361,17 @@ func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) {
     return m.mk_func_decl(symbol("str.from_ubv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_UBVTOS));    
 }
 
+func_decl* seq_decl_plugin::mk_sbv2s(unsigned arity, sort* const* domain) const {
+    ast_manager &m = *m_manager;
+    if (arity != 1)
+        m.raise_exception("Invalid str.from_sbv expects one bit-vector argument");
+    bv_util bv(m);
+    if (!bv.is_bv_sort(domain[0]))
+        m.raise_exception("Invalid str.from_sbv expects one bit-vector argument");
+    sort *rng = m_string;
+    return m.mk_func_decl(symbol("str.from_sbv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_SBVTOS));
+}
+
 func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string, bool is_right) {
     ast_manager& m = *m_manager;
     sort_ref rng(m);
@@ -416,9 +427,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_STRING_FROM_CODE:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+
     case OP_STRING_UBVTOS:
         return mk_ubv2s(arity, domain);
 
+    case OP_STRING_SBVTOS:
+        return mk_sbv2s(arity, domain);
+
     case _OP_REGEXP_FULL_CHAR:
         m_has_re = true;
         if (!range) range = mk_reglan();
@@ -627,6 +642,7 @@ void seq_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("re.nostr",  _OP_REGEXP_EMPTY));
     op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT));
     op_names.push_back(builtin_name("str.from_ubv", OP_STRING_UBVTOS));
+    op_names.push_back(builtin_name("str.from_sbv", OP_STRING_SBVTOS));
 }
 
 void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/seq_decl_plugin.h

@@ -80,6 +80,7 @@ enum seq_op_kind {
     OP_STRING_ITOS,
     OP_STRING_STOI,
     OP_STRING_UBVTOS,
+    OP_STRING_SBVTOS,
     OP_STRING_LT,
     OP_STRING_LE,
     OP_STRING_IS_DIGIT,
@@ -150,7 +151,8 @@ class seq_decl_plugin : public decl_plugin {
     func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
     func_decl* mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
     func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq, bool is_right);
-    func_decl* mk_ubv2s(unsigned arity, sort* const* domain);
+    func_decl* mk_ubv2s(unsigned arity, sort* const* domain) const;
+    func_decl* mk_sbv2s(unsigned arity, sort* const* domain) const;
 
 
     void init();
@@ -297,6 +299,7 @@ public:
         app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
         app* mk_stoi(expr* s) const { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); }
         app* mk_ubv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_UBVTOS, 1, &b); }
+        app* mk_sbv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_SBVTOS, 1, &b); }
         app* mk_is_empty(expr* s) const;
         app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); }
         app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); }
@@ -336,6 +339,7 @@ public:
         bool is_itos(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
         bool is_stoi(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_STOI); }
         bool is_ubv2s(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_UBVTOS); }
+        bool is_sbv2s(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_SBVTOS); }
         bool is_in_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
         bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
         bool is_lt(expr const* n)       const { return is_app_of(n, m_fid, OP_STRING_LT); }
@@ -374,6 +378,7 @@ public:
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
         MATCH_UNARY(is_ubv2s);
+        MATCH_UNARY(is_sbv2s);
         MATCH_UNARY(is_is_digit);
         MATCH_UNARY(is_from_code);
         MATCH_UNARY(is_to_code);