diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 648e3cd97..50a02d262 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1202,7 +1202,8 @@ 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_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;
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index fc336da74..9ce3ded09 100644
--- a/src/api/api_seq.cpp
+++ b/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) {
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 792b038e9..28e8aa052 100644
--- a/src/api/c++/z3++.h
+++ b/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);
/**
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index d40281a81..7279fe847 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -556,18 +556,18 @@ namespace Microsoft.Z3
///
/// Bind a definition to a recursive function declaration.
- /// The function must have previously been created using
- /// MkRecFuncDecl. The body may contain recursive uses of the function or
- /// other mutually recursive functions.
+ /// The function must have previously been created using
+ /// MkRecFuncDecl. The body may contain recursive uses of the function or
+ /// other mutually recursive functions.
///
- public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
- {
- CheckContextMatch(f);
- CheckContextMatch(args);
- CheckContextMatch(body);
+ public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
+ {
+ CheckContextMatch(f);
+ CheckContextMatch(args);
+ CheckContextMatch(body);
IntPtr[] argsNative = AST.ArrayToNative(args);
- Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
- }
+ Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
+ }
///
/// Creates a new function declaration.
@@ -2405,6 +2405,15 @@ namespace Microsoft.Z3
return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
}
+ ///
+ /// Convert a bit-vector expression, represented as an signed number, to a string.
+ ///
+ 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));
+ }
+
///
/// Convert an integer expression to a string.
///
@@ -2474,7 +2483,7 @@ namespace Microsoft.Z3
///
/// Check if the string s1 is lexicographically strictly less than s2.
///
- public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
+ public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2)
{
Debug.Assert(s1 != null);
Debug.Assert(s2 != null);
@@ -2485,7 +2494,7 @@ namespace Microsoft.Z3
///
/// Check if the string s1 is lexicographically strictly less than s2.
///
- public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
+ public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2)
{
Debug.Assert(s1 != null);
Debug.Assert(s2 != null);
@@ -2655,7 +2664,7 @@ namespace Microsoft.Z3
///
/// Create the empty regular expression.
- /// The sort s should be a regular expression.
+ /// The sort s should be a regular expression.
///
public ReExpr MkEmptyRe(Sort s)
{
@@ -2665,7 +2674,7 @@ namespace Microsoft.Z3
///
/// Create the full regular expression.
- /// The sort s should be a regular expression.
+ /// The sort s should be a regular expression.
///
public ReExpr MkFullRe(Sort s)
{
@@ -3399,7 +3408,7 @@ namespace Microsoft.Z3
{
Debug.Assert(t1 != null);
Debug.Assert(t2 != null);
- // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+ // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
return AndThen(t1, t2, ts);
}
@@ -4696,7 +4705,7 @@ namespace Microsoft.Z3
{
foreach (Z3Object a in arr)
{
- Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
+ Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
CheckContextMatch(a);
}
}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index a6b867eb8..1e581c482 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2035,7 +2035,15 @@ public class Context implements AutoCloseable {
{
return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
}
-
+
+ /**
+ * Convert an signed bitvector expression to a string.
+ */
+ public SeqExpr sbvToString(Expr e)
+ {
+ return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
+ }
+
/**
* Convert an integer expression to a string.
*/
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index f636e7caa..79f7ca25d 100644
--- a/src/api/z3_api.h
+++ b/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.
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index e780ad7a7..25c68819a 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/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);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index dcea166cd..312bab3bb 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/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;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 7d102a5fb..c779a5f73 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/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);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index ea073f23f..6695d9497 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/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);
@@ -376,7 +387,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
}
-func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
init();
m_has_seq = true;
@@ -416,8 +427,12 @@ 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);
+ return mk_ubv2s(arity, domain);
+
+ case OP_STRING_SBVTOS:
+ return mk_sbv2s(arity, domain);
case _OP_REGEXP_FULL_CHAR:
m_has_re = true;
@@ -627,6 +642,7 @@ void seq_decl_plugin::get_op_names(svector & 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 & sort_names, symbol const & logic) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 61bbf7ba1..3c0f28ca6 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/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);