mirror of
https://github.com/Z3Prover/z3
synced 2025-08-11 13:40:52 +00:00
str.from_ubv step2
This commit is contained in:
Nikolaj Bjorner
parent
1bc10cebc5
commit
b6a3891ac4
10 changed files with 230 additions and 2 deletions
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<expr>& xs, ptr_vector<expr>& ys, expr_ref& y);
|
||||
bool reduce_binary_eq(eqr const& e, eq_ptr& r);
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue