mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fixes to #1500 and #1457

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-25 13:11:20 +09:00
parent 9279cbfbac
commit 7b68be75c9
2 changed files with 81 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

144
src/smt/theory_seq.cpp
View file

@ -2346,28 +2346,31 @@ bool theory_seq::check_int_string() {
bool change = false;
for (unsigned i = 0; i < m_int_string.size(); ++i) {
expr* e = m_int_string[i].get(), *n;
if (m_util.str.is_itos(e) && add_itos_axiom(e)) {
if (m_util.str.is_itos(e) && add_itos_val_axiom(e)) {
change = true;
}
else if (m_util.str.is_stoi(e, n) && add_stoi_axiom(e)) {
else if (m_util.str.is_stoi(e, n) && add_stoi_val_axiom(e)) {
change = true;
}
}
return change;
}
bool theory_seq::add_stoi_axiom(expr* e) {
void theory_seq::add_stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
SASSERT(m_util.str.is_stoi(e));
literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
add_axiom(l);
}
bool theory_seq::add_stoi_val_axiom(expr* e) {
context& ctx = get_context();
expr* n = nullptr;
rational val;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
if (!get_num_value(e, val)) {
literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
add_axiom(l);
TRACE("seq", tout << l << " " << ctx.get_assignment(l) << "\n";
ctx.display(tout););
return true;
return false;
}
if (!m_stoi_axioms.contains(val)) {
m_stoi_axioms.insert(val);
@ -2445,54 +2448,61 @@ expr_ref theory_seq::digit2int(expr* ch) {
return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, nullptr, nullptr, m_autil.mk_int()), m);
}
bool theory_seq::add_itos_axiom(expr* e) {
void theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
if (get_num_value(n, val)) {
if (!m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
expr_ref n1(arith_util(m).mk_numeral(val, true), m);
// itos(n) = "25" <=> n = 25
literal eq1 = mk_eq(n1, n , false);
literal eq2 = mk_eq(e, e1, false);
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
ctx.force_phase(eq1);
ctx.force_phase(eq2);
// itos(n) = "" <=> n < 0
app_ref e1(m_util.str.mk_empty(m.get_sort(e)), m);
expr_ref zero(arith_util(m).mk_int(0), m);
literal eq1 = mk_eq(e1, e, false);
literal ge0 = mk_literal(m_autil.mk_ge(n, zero));
// n >= 0 => itos(n) != ""
// itos(n) = "" or n >= 0
add_axiom(~eq1, ~ge0);
add_axiom(eq1, ge0);
// n >= 0 => stoi(itos(n)) = n
app_ref stoi(m_util.str.mk_stoi(e), m);
add_axiom(~ge0, mk_eq(stoi, n, false));
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
// n >= 0 => itos(n) in (0-9)+
expr_ref num_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
add_axiom(~ge0, mk_literal(in_re));
}
bool theory_seq::add_itos_val_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
bool change = false;
if (get_num_value(n, val) && !val.is_neg() && !m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
expr_ref n1(arith_util(m).mk_numeral(val, true), m);
// itos(n) = "25" <=> n = 25
literal eq1 = mk_eq(n1, n , false);
literal eq2 = mk_eq(e, e1, false);
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
ctx.force_phase(eq1);
ctx.force_phase(eq2);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
change = true;
}
else {
// stoi(itos(n)) = n
app_ref e2(m_util.str.mk_stoi(e), m);
if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) {
return false;
}
add_axiom(mk_eq(e2, n, false));
#if 1
expr_ref num_re(m), opt_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
opt_re = m_util.re.mk_opt(m_util.re.mk_to_re(m_util.str.mk_string(symbol("-"))));
num_re = m_util.re.mk_concat(opt_re, num_re);
app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
internalize_term(in_re);
propagate_in_re(in_re, true);
#endif
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
return false;
return change;
}
void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
@ -3048,8 +3058,11 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
enode* n2 = ctx.get_enode(e1);
res = m_util.str.mk_string(symbol(val.to_string().c_str()));
#if 1
if (val.is_neg()) {
result = e;
}
// TBD remove this: using roots is unsound for propagation.
if (n1->get_root() == n2->get_root()) {
else if (n1->get_root() == n2->get_root()) {
result = res;
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
}
@ -3147,6 +3160,9 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_itos(n)) {
add_itos_axiom(n);
}
else if (m_util.str.is_stoi(n)) {
add_stoi_axiom(n);
}
}
@ -3366,9 +3382,9 @@ void theory_seq::add_itos_length_axiom(expr* len) {
rational len1, len2;
rational ten(10);
if (get_num_value(n, len1)) {
bool neg = len1.is_neg();
if (neg) len1.neg();
num_char1 = neg?2:1;
if (len1.is_neg()) {
return;
}
// 0 <= x < 10
// 10 <= x < 100
// 100 <= x < 1000
@ -3387,13 +3403,12 @@ void theory_seq::add_itos_length_axiom(expr* len) {
literal len_le(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char))));
literal len_ge(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char))));
literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
add_axiom(~n_ge_0, mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));
if (num_char == 1) {
add_axiom(len_ge);
literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
literal n_ge_10(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(10))));
add_axiom(~n_ge_0, n_ge_10, len_le);
add_axiom(~len_le, n_ge_0);
add_axiom(~len_le, ~n_ge_10);
return;
}
@ -3401,22 +3416,13 @@ void theory_seq::add_itos_length_axiom(expr* len) {
for (unsigned i = 2; i < num_char; ++i) {
hi *= ten;
}
// n <= -hi or n >= hi*10 <=> len >= num_chars
// -10*hi < n < 100*hi <=> len <= num_chars
literal n_le_hi = mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-hi, true)));
// n >= hi*10 <=> len >= num_chars
// n < 100*hi <=> len <= num_chars
literal n_ge_10hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*hi, true)));
literal n_le_m10hi = mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-ten*hi, true)));
literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
add_axiom(~n_le_hi, len_ge);
add_axiom(~n_ge_10hi, len_ge);
add_axiom(n_le_hi, n_ge_10hi, ~len_ge);
add_axiom(n_le_m10hi, n_ge_100hi, len_le);
add_axiom(~n_le_m10hi, ~len_le);
add_axiom(~n_ge_100hi, ~len_le);
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));
}
@ -3729,6 +3735,7 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
/*
0 <= l <= len(s) => s = ey & l = len(e)
len(s) < l => s = e
*/
void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";);
@ -3743,6 +3750,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false));
add_axiom(l_le_s, mk_eq(e, s, false));
}
/*
@ -4214,7 +4222,9 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_extract(n) ||
m_util.str.is_at(n) ||
m_util.str.is_empty(n) ||
m_util.str.is_string(n)) {
m_util.str.is_string(n) ||
m_util.str.is_itos(n) ||
m_util.str.is_stoi(n)) {
enque_axiom(n);
}

6
src/smt/theory_seq.h
View file

@ -507,8 +507,10 @@ namespace smt {
void add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n);
bool add_stoi_axiom(expr* n);
bool add_itos_axiom(expr* n);
void add_itos_axiom(expr* n);
void add_stoi_axiom(expr* n);
bool add_stoi_val_axiom(expr* n);
bool add_itos_val_axiom(expr* n);
literal is_digit(expr* ch);
expr_ref digit2int(expr* ch);
void add_itos_length_axiom(expr* n);