From de8b2041e6d09d86a243831db49c8b57bef7700d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jul 2021 00:03:32 +0200 Subject: [PATCH 01/17] make bpp work with nullptr --- src/ast/ast_ll_pp.cpp | 4 +++- src/sat/smt/euf_solver.cpp | 6 ++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index 62dbd74b5..f7ba8132f 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -303,7 +303,9 @@ public: } void display_bounded(ast * n, unsigned depth) { - if (is_app(n)) { + if (!n) + m_out << "null"; + else if (is_app(n)) { display(to_expr(n), depth); } else if (is_var(n)) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index e8c9bb54f..f66c4a331 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -286,11 +286,9 @@ namespace euf { void solver::asserted(literal l) { expr* e = m_bool_var2expr.get(l.var(), nullptr); - if (!e) { - TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << "\n";); + TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";); + if (!e) return; - } - TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";); euf::enode* n = m_egraph.find(e); if (!n) return; From 805bb5828953c65560856e056710a44a0fb8bcfc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jul 2021 12:35:24 +0200 Subject: [PATCH 02/17] fix #5404 --- src/smt/smt_setup.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 9f1103da2..ba601272d 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -735,10 +735,6 @@ namespace smt { else if (m_params.m_string_solver == "none") { // don't register any solver. } - else if (m_params.m_string_solver == "char") { - setup_QF_BV(); - setup_char(); - } else { throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'"); } From 1bc10cebc54d2a53ccf9ee5fb0b66530310780d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jul 2021 12:53:00 +0200 Subject: [PATCH 03/17] add ubv2s step 1 --- src/ast/rewriter/seq_rewriter.cpp | 14 ++++++++++++++ src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 18 +++++++++++++++--- src/ast/seq_decl_plugin.h | 4 ++++ 4 files changed, 34 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6e0d0f7b7..8745326b0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -714,6 +714,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 1); st = mk_str_stoi(args[0], result); break; + case OP_STRING_UBVTOS: + SASSERT(num_args == 1); + st = mk_str_ubv2s(args[0], result); + break; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: @@ -2204,6 +2208,11 @@ br_status seq_rewriter::mk_str_is_digit(expr* a, expr_ref& result) { } +br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) { + return BR_FAILED; +} + + br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; if (m_autil.is_numeral(a, r)) { @@ -2265,6 +2274,11 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one()); return BR_DONE; } + if (str().is_ubv2s(a, b)) { + bv_util bv(m()); + result = bv.mk_bv2int(b); + return BR_DONE; + } expr* c = nullptr, *t = nullptr, *e = nullptr; if (m().is_ite(a, c, t, e)) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 60e4cf031..7d102a5fb 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -228,6 +228,7 @@ class seq_rewriter { br_status mk_str_units(func_decl* f, expr_ref& result); 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_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 7c76b3f64..111b567da 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -350,6 +350,17 @@ 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) { + ast_manager& m = *m_manager; + if (arity != 1) + m.raise_exception("Invalid str.from_ubv expects one bit-vector argument"); + bv_util bv(m); + if (!bv.is_bv_sort(domain[0])) + m.raise_exception("Invalid str.from_ubv expects one bit-vector argument"); + sort* rng = m_string; + 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_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); @@ -400,14 +411,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_STRING_STOI: case OP_STRING_LT: case OP_STRING_LE: - 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_IS_DIGIT: case OP_STRING_TO_CODE: 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: + NOT_IMPLEMENTED_YET(); + case _OP_REGEXP_FULL_CHAR: m_has_re = true; if (!range) range = mk_reglan(); @@ -615,6 +626,7 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("int.to.str", OP_STRING_ITOS)); 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)); } 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 8ce0f7a4e..afb823284 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -79,6 +79,7 @@ enum seq_op_kind { OP_STRING_CONST, OP_STRING_ITOS, OP_STRING_STOI, + OP_STRING_UBVTOS, OP_STRING_LT, OP_STRING_LE, OP_STRING_IS_DIGIT, @@ -149,6 +150,7 @@ 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); void init(); @@ -332,6 +334,7 @@ public: bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); } 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_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); } @@ -369,6 +372,7 @@ public: MATCH_BINARY(is_le); MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); + MATCH_UNARY(is_ubv2s); MATCH_UNARY(is_is_digit); MATCH_UNARY(is_from_code); MATCH_UNARY(is_to_code); From b6a3891ac4320418b814d2d2cde165813d624ae5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jul 2021 15:00:36 +0200 Subject: [PATCH 04/17] str.from_ubv step2 --- src/ast/rewriter/seq_axioms.cpp | 37 ++++++++++ src/ast/rewriter/seq_axioms.h | 2 + src/ast/rewriter/seq_eq_solver.cpp | 108 ++++++++++++++++++++++++++++- src/ast/rewriter/seq_eq_solver.h | 6 ++ src/ast/rewriter/seq_skolem.cpp | 3 + src/ast/rewriter/seq_skolem.h | 2 + src/ast/seq_decl_plugin.h | 1 + src/smt/seq_axioms.h | 1 + src/smt/theory_seq.cpp | 64 +++++++++++++++++ src/smt/theory_seq.h | 8 +++ 10 files changed, 230 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 44389eb6c..3ef433138 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -769,6 +769,43 @@ namespace seq { } } + void axioms::ubv2s_axiom(expr* b, unsigned k) { + expr_ref ge10k(m), ge10k1(m), eq(m); + bv_util bv(m); + sort* bv_sort = b->get_sort(); + rational pow(1); + for (unsigned i = 0; i < k; ++i) + pow *= 10; + if (k == 0) { + ge10k = m.mk_true(); + } + else { + ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); + } + ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); + expr_ref_vector es(m); + expr_ref bb(b, m); + unsigned sz = bv.get_bv_size(b); + for (unsigned i = 0; i < k; ++i) { + es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, bv.mk_numeral(10, sz))))); + } + es.reverse(); + eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort())); + add_clause(~ge10k, ge10k1, eq); + ubv2ch_axiom(bv_sort); + + } + + void axioms::ubv2ch_axiom(sort* bv_sort) { + bv_util bv(m); + expr_ref eq(m); + unsigned sz = bv.get_bv_size(bv_sort); + for (unsigned i = 0; i < 10; ++i) { + eq = m.mk_eq(m_sk.mk_ubv2ch(bv.mk_numeral(i, sz)), seq.mk_char('0' + i)); + add_clause(eq); + } + } + /** Let s := itos(e) diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index d124dd39f..8c2af65e4 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -94,6 +94,8 @@ namespace seq { void stoi_axiom(expr* n); void stoi_axiom(expr* e, unsigned k); void itos_axiom(expr* s, unsigned k); + void ubv2s_axiom(expr* b, unsigned k); + void ubv2ch_axiom(sort* bv_sort); void lt_axiom(expr* n); void le_axiom(expr* n); void is_digit_axiom(expr* n); diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp index 2c595090e..e293743f8 100644 --- a/src/ast/rewriter/seq_eq_solver.cpp +++ b/src/ast/rewriter/seq_eq_solver.cpp @@ -16,6 +16,7 @@ Author: --*/ #include "ast/rewriter/seq_eq_solver.h" +#include "ast/bv_decl_plugin.h" namespace seq { @@ -37,6 +38,10 @@ namespace seq { return true; if (reduce_itos3(e, r)) return true; + if (reduce_ubv2s1(e, r)) + return true; + if (reduce_ubv2s2(e, r)) + return true; if (reduce_binary_eq(e, r)) return true; if (reduce_nth_solved(e, r)) @@ -184,8 +189,8 @@ namespace seq { expr_ref digit = m_ax.sk().mk_digit2int(u); add_consequence(m_ax.mk_ge(digit, 1)); } - expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m); - ctx.add_solution(e.ls[0], y); + expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m); + ctx.add_solution(seq.str.mk_itos(n), y); return true; } @@ -209,6 +214,105 @@ namespace seq { } + + /** + * from_ubv(s) == from_ubv(t) + * -------------------------- + * s = t + */ + + bool eq_solver::match_ubv2s1(eqr const& e, expr*& a, expr*& b) { + return + e.ls.size() == 1 && e.rs.size() == 1 && + seq.str.is_ubv2s(e.ls[0], a) && seq.str.is_ubv2s(e.rs[0], b); + return false; + } + + bool eq_solver::reduce_ubv2s1(eqr const& e, eq_ptr& r) { + expr* s = nullptr, * t = nullptr; + if (!match_ubv2s1(e, s, t)) + return false; + expr_ref eq = mk_eq(s, t); + add_consequence(eq); + return true; + } + + /** + * + * bv2s(n) = [d1]+[d2]+...+[dk] + * --------------------------------- + * n = 10^{k-1}*d1 + ... + dk + * + * k > 1 => d1 > 0 + */ + bool eq_solver::match_ubv2s2(eqr const& e, expr*& n, expr_ref_vector const*& es) { + if (e.ls.size() == 1 && seq.str.is_ubv2s(e.ls[0], n)) { + es = &e.rs; + return true; + } + if (e.rs.size() == 1 && seq.str.is_ubv2s(e.rs[0], n)) { + es = &e.ls; + return true; + } + return false; + } + + bool eq_solver::reduce_ubv2s2(eqr const& e, eq_ptr& r) { + expr* n = nullptr; + expr_ref_vector const* _es = nullptr; + if (!match_ubv2s2(e, n, _es)) + return false; + + expr_ref_vector const& es = *_es; + if (es.empty()) { + set_conflict(); + return true; + } + expr* u = nullptr; + for (expr* r : es) { + if (seq.str.is_unit(r, u)) { + expr_ref is_digit = m_ax.is_digit(u); + if (!m.is_true(ctx.expr2rep(is_digit))) + add_consequence(is_digit); + } + } + if (!all_units(es, 0, es.size())) + return false; + + expr_ref num(m); + bv_util bv(m); + sort* bv_sort = n->get_sort(); + unsigned sz = bv.get_bv_size(n); + if (es.size() > (sz + log2(10)-1)/log2(10)) { + set_conflict(); + return true; + } + + for (expr* r : es) { + VERIFY(seq.str.is_unit(r, u)); + expr_ref digit = m_ax.sk().mk_digit2bv(u, bv_sort); + if (!num) + num = digit; + else + num = bv.mk_bv_add(bv.mk_bv_mul(bv.mk_numeral(10, sz), num), digit); + } + + expr_ref eq(m.mk_eq(n, num), m); + m_ax.rewrite(eq); + add_consequence(eq); + if (es.size() > 1) { + VERIFY(seq.str.is_unit(es[0], u)); + expr_ref digit = m_ax.sk().mk_digit2bv(u, bv_sort); + expr_ref eq0(m.mk_eq(digit, bv.mk_numeral(0, sz)), m); + expr_ref neq0(m.mk_not(eq0), m); + add_consequence(neq0); + } + expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m); + ctx.add_solution(seq.str.mk_ubv2s(n), y); + return true; + } + + /** * Equation is of the form x ++ xs = ys ++ x * where |xs| = |ys| are units of same length diff --git a/src/ast/rewriter/seq_eq_solver.h b/src/ast/rewriter/seq_eq_solver.h index e014bb8e1..6be2531b2 100644 --- a/src/ast/rewriter/seq_eq_solver.h +++ b/src/ast/rewriter/seq_eq_solver.h @@ -64,6 +64,12 @@ namespace seq { bool reduce_itos3(eqr const& e, eq_ptr& r); bool match_itos3(eqr const& e, expr*& n, expr_ref_vector const* & es); + bool match_ubv2s1(eqr const& e, expr*& s, expr*& t); + bool reduce_ubv2s1(eqr const& e, eq_ptr& r); + + bool match_ubv2s2(eqr const& e, expr*& n, expr_ref_vector const*& es); + bool reduce_ubv2s2(eqr const& e, eq_ptr& r); + bool match_binary_eq(eqr const& e, expr_ref& x, ptr_vector& xs, ptr_vector& ys, expr_ref& y); bool reduce_binary_eq(eqr const& e, eq_ptr& r); diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index c76efda57..ecefe8374 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -201,3 +201,6 @@ expr_ref skolem::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, e return expr_ref(seq.mk_skolem(m_aut_step, args.size(), args.data(), m.mk_bool_sort()), m); } +expr_ref skolem::mk_digit2bv(expr* ch, sort* bv_sort) { + return mk(symbol("seq.digit2bv"), ch, nullptr, nullptr, nullptr, bv_sort); +} diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 56baf8def..a7d4be917 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -93,6 +93,8 @@ namespace seq { expr_ref mk_is_digit(expr* ch) { return mk(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()); } expr_ref mk_unit_inv(expr* n); expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); } + expr_ref mk_digit2bv(expr* ch, sort* bv_sort); + expr_ref mk_ubv2ch(expr* b) { return mk(symbol("seq.ubv2ch"), b, nullptr, nullptr, nullptr, seq.mk_char_sort()); } expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); } expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); } expr_ref mk_max_unfolding_depth(unsigned d); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index afb823284..61bbf7ba1 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -296,6 +296,7 @@ public: app* mk_char_bit(expr* e, unsigned i); 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_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); } diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index e1dd99b64..cd7f38064 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -79,6 +79,7 @@ namespace smt { void add_stoi_axiom(expr* n) { m_ax.stoi_axiom(n); } void add_stoi_axiom(expr* e, unsigned k) { m_ax.stoi_axiom(e, k); } 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_lt_axiom(expr* n) { m_ax.lt_axiom(n); } void add_le_axiom(expr* n) { m_ax.le_axiom(n); } void add_is_digit_axiom(expr* n) { m_ax.is_digit_axiom(n); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e4eec609f..7e4eda114 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -262,6 +262,7 @@ theory_seq::theory_seq(context& ctx): m_axioms(m), m_axioms_head(0), m_int_string(m), + m_ubv_string(m), m_length(m), m_length_limit(m), m_mg(nullptr), @@ -368,6 +369,11 @@ final_check_status theory_seq::final_check_eh() { TRACEFIN("int_string"); return FC_CONTINUE; } + if (check_ubv_string()) { + ++m_stats.m_ubv_string; + TRACEFIN("ubv_string"); + return FC_CONTINUE; + } if (reduce_length_eq()) { ++m_stats.m_branch_variable; TRACEFIN("reduce_length"); @@ -1525,6 +1531,60 @@ bool theory_seq::add_length_to_eqc(expr* e) { return change; } +void theory_seq::add_ubv_string(expr* e) { + m_ubv_string.push_back(e); + m_trail_stack.push(push_back_vector(m_ubv_string)); +} + +bool theory_seq::check_ubv_string() { + bool change = false; + for (expr* e : m_ubv_string) { + if (check_ubv_string(e)) + change = true; + } + return change; +} + +bool theory_seq::check_ubv_string(expr* e) { + expr* n = nullptr; + if (ctx.inconsistent()) + return true; + if (m_has_ubv_axiom.contains(e)) + return false; + expr* b = nullptr; + bv_util bv(m); + VERIFY(m_util.str.is_ubv2s(e, b)); + unsigned sz = bv.get_bv_size(b); + rational value(0); + bool all_bits_assigned = true; + for (unsigned i = 0; i < sz; ++i) { + expr_ref bit(bv.mk_bit2bool(b, i), m); + literal lit = mk_literal(bit); + switch (ctx.get_assignment(lit)) { + case l_undef: + ctx.mark_as_relevant(lit); + all_bits_assigned = false; + break; + case l_true: + value += rational::power_of_two(i); + break; + case l_false: + break; + } + } + if (!all_bits_assigned) + return true; + unsigned k = 0; + while (value >= 10) { + k++; + value = div(value, rational(10)); + } + m_has_ubv_axiom.insert(e); + m_trail_stack.push(insert_obj_trail(m_has_ubv_axiom, e)); + m_ax.add_ubv2s_axiom(b, k); + return true; +} + void theory_seq::add_int_string(expr* e) { m_int_string.push_back(e); m_trail_stack.push(push_back_vector(m_int_string)); @@ -1761,6 +1821,7 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq extensionality", m_stats.m_extensionality); st.update("seq fixed length", m_stats.m_fixed_length); st.update("seq int.to.str", m_stats.m_int_string); + st.update("seq str.from_ubv", m_stats.m_ubv_string); } void theory_seq::init_search_eh() { @@ -3099,6 +3160,9 @@ void theory_seq::relevant_eh(app* n) { add_int_string(n); } + if (m_util.str.is_ubv2s(n)) + add_ubv_string(n); + expr* arg = nullptr; if (m_sk.is_tail(n, arg)) { add_length_limit(arg, m_max_unfolding_depth, true); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index b7ea9517a..ad6ef0695 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -323,6 +323,7 @@ namespace smt { unsigned m_fixed_length; unsigned m_propagate_contains; unsigned m_int_string; + unsigned m_ubv_string; }; typedef hashtable rational_set; @@ -348,6 +349,8 @@ namespace smt { unsigned m_axioms_head; // index of first axiom to add. bool m_incomplete; // is the solver (clearly) incomplete for the fragment. expr_ref_vector m_int_string; + expr_ref_vector m_ubv_string; // list all occurrences of str.from_ubv that have been seen + obj_hashtable m_has_ubv_axiom; // keep track of ubv that have been axiomatized within scope. obj_hashtable m_has_length; // is length applied expr_ref_vector m_length; // length applications themselves obj_map m_length_limit_map; // sequences that have length limit predicates @@ -569,6 +572,11 @@ namespace smt { bool branch_itos(); bool branch_itos(expr* e); + // functions that convert ubv to string + void add_ubv_string(expr* e); + bool check_ubv_string(); + bool check_ubv_string(expr* e); + expr_ref add_elim_string_axiom(expr* n); void add_in_re_axiom(expr* n); literal mk_simplified_literal(expr* n); From f74adb1ebde0d5e5e8bdbebaa172c3befd22d049 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jul 2021 17:15:08 +0200 Subject: [PATCH 05/17] ubv2s step3 --- src/ast/rewriter/seq_axioms.cpp | 2 -- src/ast/rewriter/seq_rewriter.cpp | 6 ++++++ src/smt/seq_axioms.h | 1 + src/smt/theory_seq.cpp | 8 ++++++++ 4 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 3ef433138..2d48cfe4e 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -792,8 +792,6 @@ namespace seq { es.reverse(); eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort())); add_clause(~ge10k, ge10k1, eq); - ubv2ch_axiom(bv_sort); - } void axioms::ubv2ch_axiom(sort* bv_sort) { diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 8745326b0..0bd653232 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2209,6 +2209,12 @@ br_status seq_rewriter::mk_str_is_digit(expr* a, expr_ref& result) { br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) { + bv_util bv(m()); + rational val; + if (bv.is_numeral(a, val)) { + result = str().mk_string(zstring(val)); + return BR_DONE; + } return BR_FAILED; } diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index cd7f38064..16091fcf4 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -80,6 +80,7 @@ namespace smt { void add_stoi_axiom(expr* e, unsigned k) { m_ax.stoi_axiom(e, k); } 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_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); } void add_is_digit_axiom(expr* n) { m_ax.is_digit_axiom(n); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7e4eda114..599646b5b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1579,6 +1579,14 @@ bool theory_seq::check_ubv_string(expr* e) { k++; value = div(value, rational(10)); } + bool has_sort = false; + for (auto* e2 : m_has_ubv_axiom) { + expr* b2 = nullptr; + VERIFY(m_util.str.is_ubv2s(e2, b2)); + has_sort |= b2->get_sort() == b->get_sort(); + } + if (!has_sort) + m_ax.add_ubv2ch_axioms(b->get_sort()); m_has_ubv_axiom.insert(e); m_trail_stack.push(insert_obj_trail(m_has_ubv_axiom, e)); m_ax.add_ubv2s_axiom(b, k); From e5c5caea450a71abaaebb94c1145fd9d00f506d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 09:19:20 +0200 Subject: [PATCH 06/17] add call to function Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 111b567da..ea073f23f 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -417,7 +417,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, 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: - NOT_IMPLEMENTED_YET(); + return mk_ubv2s(arity, domain); case _OP_REGEXP_FULL_CHAR: m_has_re = true; From 34677e0e7c05a198707843fedfba318d4e69450a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 09:32:05 +0200 Subject: [PATCH 07/17] fix update of bb Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 2d48cfe4e..afd1c5239 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -783,11 +783,12 @@ namespace seq { ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); } ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); - expr_ref_vector es(m); - expr_ref bb(b, m); unsigned sz = bv.get_bv_size(b); + expr_ref_vector es(m); + expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m); for (unsigned i = 0; i < k; ++i) { - es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, bv.mk_numeral(10, sz))))); + es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten)))); + bb = bv.mk_bv_udiv(bb, ten); } es.reverse(); eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort())); From a49a5b3a0b23494e01881b3642956b2979d2f335 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 09:43:00 +0200 Subject: [PATCH 08/17] add release note for 4.8.12 prepare for addressing #5406 Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 89f839cae..dae1e81b8 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -11,6 +11,11 @@ Version 4.8.next turned off by default. +Version 4.8.12 +============== +Release provided to fix git tag discrepancy issues with 4.8.11 + + Version 4.8.11 ============== - self-contained character theory, direct support for UTF8, Unicode character sets. From 0752b1385c090a2aba82bc47392402943917a9be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 14:22:58 +0200 Subject: [PATCH 09/17] add length axioms Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 26 ++++++++++++++++++++++++-- src/ast/rewriter/seq_axioms.h | 1 + src/smt/seq_axioms.h | 1 + src/smt/theory_seq.cpp | 25 +++++++++++++++++-------- 4 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index afd1c5239..c255c7140 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -786,15 +786,37 @@ namespace seq { unsigned sz = bv.get_bv_size(b); expr_ref_vector es(m); expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m); - for (unsigned i = 0; i < k; ++i) { + pow = 1; + for (unsigned i = 0; i <= k; ++i) { + if (pow > 1) + bb = bv.mk_bv_udiv(b, bv.mk_numeral(pow, bv_sort)); es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten)))); - bb = bv.mk_bv_udiv(bb, ten); + pow *= 10; } es.reverse(); eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort())); add_clause(~ge10k, ge10k1, eq); } + /* + * len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k} k > 1 + * len(ubv2s(b)) = 1 => b < 10^{1} k = 1 + */ + void axioms::ubv2s_len_axiom(expr* b, unsigned k) { + expr_ref ge10k(m), ge10k1(m), eq(m); + bv_util bv(m); + sort* bv_sort = b->get_sort(); + rational pow(1); + for (unsigned i = 1; i < k; ++i) + pow *= 10; + ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); + ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); + eq = m.mk_eq(seq.str.mk_length(seq.str.mk_ubv2s(b)), a.mk_int(k)); + add_clause(~eq, ~ge10k1); + if (k > 1) + add_clause(~eq, ge10k); + } + void axioms::ubv2ch_axiom(sort* bv_sort) { bv_util bv(m); expr_ref eq(m); diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 8c2af65e4..c9cdbfc9a 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -95,6 +95,7 @@ namespace seq { void stoi_axiom(expr* e, unsigned k); void itos_axiom(expr* s, unsigned k); void ubv2s_axiom(expr* b, unsigned k); + void ubv2s_len_axiom(expr* b, unsigned k); void ubv2ch_axiom(sort* bv_sort); void lt_axiom(expr* n); void le_axiom(expr* n); diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 16091fcf4..c5aa68e0a 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -80,6 +80,7 @@ namespace smt { void add_stoi_axiom(expr* e, unsigned k) { m_ax.stoi_axiom(e, k); } 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_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 599646b5b..436752aa7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1532,8 +1532,19 @@ bool theory_seq::add_length_to_eqc(expr* e) { } void theory_seq::add_ubv_string(expr* e) { + bool has_sort = false; + expr* b = nullptr; + VERIFY(m_util.str.is_ubv2s(e, b)); + for (auto* e2 : m_ubv_string) { + expr* b2 = nullptr; + VERIFY(m_util.str.is_ubv2s(e2, b2)); + has_sort |= b2->get_sort() == b->get_sort(); + } + if (!has_sort) + m_ax.add_ubv2ch_axioms(b->get_sort()); m_ubv_string.push_back(e); m_trail_stack.push(push_back_vector(m_ubv_string)); + add_length_to_eqc(e); } bool theory_seq::check_ubv_string() { @@ -1554,6 +1565,11 @@ bool theory_seq::check_ubv_string(expr* e) { expr* b = nullptr; bv_util bv(m); VERIFY(m_util.str.is_ubv2s(e, b)); + rational len; + if (get_length(e, len) && len.is_unsigned()) + m_ax.add_ubv2s_len_axiom(b, len.get_unsigned()); + + unsigned sz = bv.get_bv_size(b); rational value(0); bool all_bits_assigned = true; @@ -1579,14 +1595,7 @@ bool theory_seq::check_ubv_string(expr* e) { k++; value = div(value, rational(10)); } - bool has_sort = false; - for (auto* e2 : m_has_ubv_axiom) { - expr* b2 = nullptr; - VERIFY(m_util.str.is_ubv2s(e2, b2)); - has_sort |= b2->get_sort() == b->get_sort(); - } - if (!has_sort) - m_ax.add_ubv2ch_axioms(b->get_sort()); + m_has_ubv_axiom.insert(e); m_trail_stack.push(insert_obj_trail(m_has_ubv_axiom, e)); m_ax.add_ubv2s_axiom(b, k); From 82e477ac02449f8d4aa3d7ceccdef1ae2441d912 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 14:40:32 +0200 Subject: [PATCH 10/17] bounds Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index c255c7140..cffef51a0 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -806,9 +806,12 @@ namespace seq { expr_ref ge10k(m), ge10k1(m), eq(m); bv_util bv(m); sort* bv_sort = b->get_sort(); + unsigned sz = bv.get_bv_size(bv_sort); rational pow(1); for (unsigned i = 1; i < k; ++i) pow *= 10; + if (pow * 10 >= rational::power_of_two(sz)) + return; // TODO: add conflict when k is too large or avoid overflow bounds and limits ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); eq = m.mk_eq(seq.str.mk_length(seq.str.mk_ubv2s(b)), a.mk_int(k)); From 75a5de99cae69f94bf12716342e0576b5f14b2c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 15:24:19 +0200 Subject: [PATCH 11/17] Update release.yml for Azure Pipelines --- scripts/release.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index cc5946a91..2e1029118 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -107,7 +107,6 @@ stages: inputs: artifactName: 'UbuntuDoc' targetPath: $(Build.ArtifactStagingDirectory) - - job: ManyLinuxBuild displayName: "ManyLinux build" From 3a402ca2c14c3891d24658318406f80ce59b719f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 15:25:23 +0200 Subject: [PATCH 12/17] Update release.yml for Azure Pipelines --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 2e1029118..901afc575 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.8.11' + ReleaseVersion: '4.8.12' stages: From 7ae78da850212441f0d5ab8c8e1df6d693044e15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 15:56:08 +0200 Subject: [PATCH 13/17] adding access to characters over API Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 1 + src/api/api_seq.cpp | 20 +++++++++++++ src/api/c++/z3++.h | 8 ++++- src/api/java/CMakeLists.txt | 1 + src/api/java/CharSort.java | 33 +++++++++++++++++++++ src/api/java/Context.java | 59 ++++++++++++++++++++++++------------- src/api/java/SeqSort.java | 1 + src/api/z3_api.h | 31 ++++++++++++++++--- 8 files changed, 128 insertions(+), 26 deletions(-) create mode 100644 src/api/java/CharSort.java diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index ef9d26889..648e3cd97 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1202,6 +1202,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_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 39e5b80cc..fc336da74 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -79,6 +79,16 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + Z3_sort Z3_API Z3_mk_char_sort(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_char_sort(c); + RESET_ERROR_CODE(); + sort* ty = mk_c(c)->sutil().mk_char_sort(); + mk_c(c)->save_ast_trail(ty); + RETURN_Z3(of_sort(ty)); + Z3_CATCH_RETURN(nullptr); + } + bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s) { Z3_TRY; LOG_Z3_is_seq_sort(c, s); @@ -121,6 +131,15 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_is_char_sort(c, s); + RESET_ERROR_CODE(); + return mk_c(c)->sutil().is_char(to_sort(s)); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) { Z3_TRY; LOG_Z3_is_string_sort(c, s); @@ -225,6 +244,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); 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 e0276c9e5..4403d1605 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1437,7 +1437,12 @@ namespace z3 { check_error(); return expr(ctx(), r); } - + expr ubvtos() const { + Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + friend expr range(expr const& lo, expr const& hi); /** \brief create a looping regular expression. @@ -3199,6 +3204,7 @@ namespace z3 { inline sort context::real_sort() { Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); } inline sort context::bv_sort(unsigned sz) { Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); } inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); } + inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); } inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); } inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); } inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); } diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index f886639f8..dd7115aaa 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -108,6 +108,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES BitVecSort.java BoolExpr.java BoolSort.java + CharSort.java ConstructorDecRefQueue.java Constructor.java ConstructorListDecRefQueue.java diff --git a/src/api/java/CharSort.java b/src/api/java/CharSort.java new file mode 100644 index 000000000..2d843c8ac --- /dev/null +++ b/src/api/java/CharSort.java @@ -0,0 +1,33 @@ +/** +Copyright (c) 2012-2014 Microsoft Corporation + +Module Name: + + CharSort.java + +Abstract: + +Author: + + @author Christoph Wintersteiger (cwinter) 2012-03-15 + +Notes: + +**/ + +package com.microsoft.z3; + +/** + * A Character sort + **/ +public class CharSort extends Sort +{ + CharSort(Context ctx, long obj) + { + super(ctx, obj); + } + + CharSort(Context ctx) { super(ctx, Native.mkCharSort(ctx.nCtx())); { }} + +} + diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 160dfa7db..a7d541242 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -120,7 +120,7 @@ public class Context implements AutoCloseable { private BoolSort m_boolSort = null; private IntSort m_intSort = null; private RealSort m_realSort = null; - private SeqSort m_stringSort = null; + private SeqSort m_stringSort = null; /** * Retrieves the Boolean sort of the context. @@ -164,9 +164,18 @@ public class Context implements AutoCloseable { } /** - * Retrieves the Integer sort of the context. + * Creates character sort object. **/ - public SeqSort getStringSort() + + public CharSort mkCharSort() + { + return new CharSort(this); + } + + /** + * Retrieves the String sort of the context. + **/ + public SeqSort getStringSort() { if (m_stringSort == null) { m_stringSort = mkStringSort(); @@ -239,7 +248,7 @@ public class Context implements AutoCloseable { /** * Create a new string sort **/ - public SeqSort mkStringSort() + public SeqSort mkStringSort() { return new SeqSort<>(this, Native.mkStringSort(nCtx())); } @@ -2006,23 +2015,31 @@ public class Context implements AutoCloseable { /** * Create a string constant. */ - public SeqExpr mkString(String s) + public SeqExpr mkString(String s) { - return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s)); + return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s)); } /** * Convert an integer expression to a string. */ - public SeqExpr intToString(Expr e) + public SeqExpr intToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject())); + } + + /** + * Convert an unsigned bitvector expression to a string. + */ + public SeqExpr ubvToString(Expr e) + { + return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); } /** * Convert an integer expression to a string. */ - public IntExpr stringToInt(Expr> e) + public IntExpr stringToInt(Expr> e) { return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject())); } @@ -2041,7 +2058,7 @@ public class Context implements AutoCloseable { /** * Retrieve the length of a given sequence. */ - public IntExpr mkLength(Expr> s) + public IntExpr mkLength(Expr> s) { checkContextMatch(s); return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject())); @@ -2050,7 +2067,7 @@ public class Context implements AutoCloseable { /** * Check for sequence prefix. */ - public BoolExpr mkPrefixOf(Expr> s1, Expr> s2) + public BoolExpr mkPrefixOf(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2059,7 +2076,7 @@ public class Context implements AutoCloseable { /** * Check for sequence suffix. */ - public BoolExpr mkSuffixOf(Expr> s1, Expr> s2) + public BoolExpr mkSuffixOf(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2068,7 +2085,7 @@ public class Context implements AutoCloseable { /** * Check for sequence containment of s2 in s1. */ - public BoolExpr mkContains(Expr> s1, Expr> s2) + public BoolExpr mkContains(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2077,7 +2094,7 @@ public class Context implements AutoCloseable { /** * Retrieve sequence of length one at index. */ - public SeqExpr mkAt(Expr> s, Expr index) + public SeqExpr mkAt(Expr> s, Expr index) { checkContextMatch(s, index); return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject())); @@ -2086,7 +2103,7 @@ public class Context implements AutoCloseable { /** * Retrieve element at index. */ - public Expr MkNth(Expr> s, Expr index) + public Expr MkNth(Expr> s, Expr index) { checkContextMatch(s, index); return (Expr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); @@ -2096,7 +2113,7 @@ public class Context implements AutoCloseable { /** * Extract subsequence. */ - public SeqExpr mkExtract(Expr> s, Expr offset, Expr length) + public SeqExpr mkExtract(Expr> s, Expr offset, Expr length) { checkContextMatch(s, offset, length); return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject())); @@ -2105,7 +2122,7 @@ public class Context implements AutoCloseable { /** * Extract index of sub-string starting at offset. */ - public IntExpr mkIndexOf(Expr> s, Expr> substr, Expr offset) + public IntExpr mkIndexOf(Expr> s, Expr> substr, Expr offset) { checkContextMatch(s, substr, offset); return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject())); @@ -2114,7 +2131,7 @@ public class Context implements AutoCloseable { /** * Replace the first occurrence of src by dst in s. */ - public SeqExpr mkReplace(Expr> s, Expr> src, Expr> dst) + public SeqExpr mkReplace(Expr> s, Expr> src, Expr> dst) { checkContextMatch(s, src, dst); return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject())); @@ -2123,7 +2140,7 @@ public class Context implements AutoCloseable { /** * Convert a regular expression that accepts sequence s. */ - public ReExpr mkToRe(Expr> s) + public ReExpr mkToRe(Expr> s) { checkContextMatch(s); return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject())); @@ -2133,7 +2150,7 @@ public class Context implements AutoCloseable { /** * Check for regular expression membership. */ - public BoolExpr mkInRe(Expr> s, Expr> re) + public BoolExpr mkInRe(Expr> s, Expr> re) { checkContextMatch(s, re); return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject())); @@ -2241,7 +2258,7 @@ public class Context implements AutoCloseable { /** * Create a range expression. */ - public ReExpr mkRange(Expr> lo, Expr> hi) + public ReExpr mkRange(Expr> lo, Expr> hi) { checkContextMatch(lo, hi); return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); diff --git a/src/api/java/SeqSort.java b/src/api/java/SeqSort.java index 28b865733..4650021b9 100644 --- a/src/api/java/SeqSort.java +++ b/src/api/java/SeqSort.java @@ -27,3 +27,4 @@ public class SeqSort extends Sort super(ctx, obj); } } + diff --git a/src/api/z3_api.h b/src/api/z3_api.h index cf650a5fa..f636e7caa 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1202,6 +1202,7 @@ typedef enum { // strings Z3_OP_STR_TO_INT, Z3_OP_INT_TO_STR, + Z3_OP_UBV_TO_STR, Z3_OP_STRING_LT, Z3_OP_STRING_LE, @@ -3437,15 +3438,22 @@ extern "C" { Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s); /** - \brief Create a sort for 8 bit strings. - - This function creates a sort for ASCII strings. - Each character is 8 bits. + \brief Create a sort for unicode strings. def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), )) */ Z3_sort Z3_API Z3_mk_string_sort(Z3_context c); + /** + \brief Create a sort for unicode characters. + + The sort for characters can be changed to ASCII by setting + the global parameter \c unicode to \c false. + + def_API('Z3_mk_char_sort', SORT ,(_in(CONTEXT), )) + */ + Z3_sort Z3_API Z3_mk_char_sort(Z3_context c); + /** \brief Check if \c s is a string sort. @@ -3453,6 +3461,13 @@ extern "C" { */ bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s); + /** + \brief Check if \c s is a character sort. + + def_API('Z3_is_char_sort', BOOL, (_in(CONTEXT), _in(SORT))) + */ + bool Z3_API Z3_is_char_sort(Z3_context c, Z3_sort s); + /** \brief Create a string constant out of the string that is passed in def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING))) @@ -3633,6 +3648,14 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s); + /** + \brief Unsigned bit-vector to string conversion. + + def_API('Z3_mk_ubv_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s); + + /** \brief Create a regular expression that accepts the sequence \c seq. From a3010c8875fb86db23891d517a0a8c542eb20473 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 17:14:47 +0200 Subject: [PATCH 14/17] version inc, bvsort->bitvecsort --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- src/api/java/Context.java | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d01004c36..46cb84ddc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.8.12.0 LANGUAGES CXX) +project(Z3 VERSION 4.8.13.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 4e7c0e97b..982ea194e 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 8, 12, 0) + set_version(4, 8, 13, 0) # Z3 Project definition def init_project_def(): diff --git a/src/api/java/Context.java b/src/api/java/Context.java index a7d541242..a6b867eb8 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2031,7 +2031,7 @@ public class Context implements AutoCloseable { /** * Convert an unsigned bitvector expression to a string. */ - public SeqExpr ubvToString(Expr e) + public SeqExpr ubvToString(Expr e) { return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); } From 1b648437b76c87114ceea317702cccd5ed8fc7a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 17:42:34 +0200 Subject: [PATCH 15/17] na Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4403d1605..792b038e9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -253,8 +253,13 @@ namespace z3 { \brief Return the Bit-vector sort of size \c sz. That is, the sort for bit-vectors of size \c sz. */ sort bv_sort(unsigned sz); + /** - \brief Return the sort for ASCII strings. + \brief Return the sort for Unicode characters. + */ + sort char_sort(); + /** + \brief Return the sort for Unicode strings. */ sort string_sort(); /** From 97a035fd6d8274b26001c9961c6e1976a2a8d9eb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 19:43:12 +0200 Subject: [PATCH 16/17] add char sort to .net Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/CMakeLists.txt | 1 + src/api/dotnet/CharSort.cs | 35 +++++++++++++++++++++++++++++++++++ src/api/dotnet/Context.cs | 26 +++++++++++++++++++++++--- 3 files changed, 59 insertions(+), 3 deletions(-) create mode 100644 src/api/dotnet/CharSort.cs diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index c7ae98762..98d4b9503 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -55,6 +55,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE BitVecSort.cs BoolExpr.cs BoolSort.cs + CharSort.cs Constructor.cs ConstructorList.cs Context.cs diff --git a/src/api/dotnet/CharSort.cs b/src/api/dotnet/CharSort.cs new file mode 100644 index 000000000..d5410e6c4 --- /dev/null +++ b/src/api/dotnet/CharSort.cs @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + CharSort.cs + +Abstract: + + Z3 Managed API: Character Sorts + +Author: + + Christoph Wintersteiger (cwinter) 2012-11-23 + +Notes: + +--*/ + +using System.Diagnostics; +using System; + +namespace Microsoft.Z3 +{ + /// + /// A Character sort + /// + public class CharSort : Sort + { + #region Internal + internal CharSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } + internal CharSort(Context ctx) : base(ctx, Native.Z3_mk_char_sort(ctx.nCtx)) { Debug.Assert(ctx != null); } + #endregion + } +} diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index b4afabe0e..e63f86ca0 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -89,7 +89,6 @@ namespace Microsoft.Z3 /// public IntSymbol MkSymbol(int i) { - return new IntSymbol(this, i); } @@ -98,7 +97,6 @@ namespace Microsoft.Z3 /// public StringSymbol MkSymbol(string name) { - return new StringSymbol(this, name); } @@ -107,7 +105,6 @@ namespace Microsoft.Z3 /// internal Symbol[] MkSymbols(string[] names) { - if (names == null) return null; Symbol[] result = new Symbol[names.Length]; for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]); @@ -120,6 +117,7 @@ namespace Microsoft.Z3 private IntSort m_intSort = null; private RealSort m_realSort = null; private SeqSort m_stringSort = null; + private CharSort m_charSort = null; /// /// Retrieves the Boolean sort of the context. @@ -155,6 +153,18 @@ namespace Microsoft.Z3 } } + /// + /// Retrieves the String sort of the context. + /// + public SeqSort CharSort + { + get + { + if (m_charSort == null) m_charSort = new CharSort(this, Native.Z3_mk_char_sort(nCtx)); return m_charSort; + } + } + + /// /// Retrieves the String sort of the context. /// @@ -2385,6 +2395,16 @@ namespace Microsoft.Z3 return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject)); } + /// + /// Convert a bit-vector expression, represented as an unsigned number, to a string. + /// + public SeqExpr UbvToString(Expr e) + { + Debug.Assert(e != null); + Debug.Assert(e is ArithExpr); + return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject)); + } + /// /// Convert an integer expression to a string. /// From 79c261736bf6a6b2018813f4e33519cab4256fb0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jul 2021 19:50:41 +0200 Subject: [PATCH 17/17] charsort Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 4 ++-- src/api/dotnet/SeqSort.cs | 5 ----- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index e63f86ca0..d40281a81 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -156,11 +156,11 @@ namespace Microsoft.Z3 /// /// Retrieves the String sort of the context. /// - public SeqSort CharSort + public CharSort CharSort { get { - if (m_charSort == null) m_charSort = new CharSort(this, Native.Z3_mk_char_sort(nCtx)); return m_charSort; + if (m_charSort == null) m_charSort = new CharSort(this); return m_charSort; } } diff --git a/src/api/dotnet/SeqSort.cs b/src/api/dotnet/SeqSort.cs index 2902b1e9e..ae57885ca 100644 --- a/src/api/dotnet/SeqSort.cs +++ b/src/api/dotnet/SeqSort.cs @@ -33,11 +33,6 @@ namespace Microsoft.Z3 { Debug.Assert(ctx != null); } - internal SeqSort(Context ctx) - : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx)) - { - Debug.Assert(ctx != null); - } #endregion } }