mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

experimenting with alternative prefix encodings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-24 08:55:22 -08:00
parent 8c68aed69e
commit 5679fb5d6b
2 changed files with 41 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
src/smt/theory_seq.cpp
View file

@ -2032,7 +2032,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
return result;
}
expr* e = m_rep.find(e0, deps);
expr* e1, *e2;
expr* e1, *e2, *e3;
if (m_util.str.is_concat(e, e1, e2)) {
result = mk_concat(expand(e1, deps), expand(e2, deps));
}
@ -2051,6 +2051,12 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
else if (m_util.str.is_unit(e, e1)) {
result = m_util.str.mk_unit(expand(e1, deps));
}
else if (m_util.str.is_index(e, e1, e2)) {
result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), m_autil.mk_int(0));
}
else if (m_util.str.is_index(e, e1, e2, e3)) {
result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3);
}
else {
result = e;
}
@ -2179,7 +2185,6 @@ void theory_seq::add_indexof_axiom(expr* i) {
expr_ref zero(m_autil.mk_int(0), m);
expr_ref xsy(m);
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
expr_ref x = mk_skolem(m_indexof_left, t, s);
expr_ref y = mk_skolem(m_indexof_right, t, s);
@ -2676,7 +2681,7 @@ literal theory_seq::mk_seq_eq(expr* a, expr* b) {
return mk_literal(mk_skolem(m_eq, a, b, 0, m.mk_bool_sort()));
}
literal theory_seq::mk_eq_empty(expr* _e) {
literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
context& ctx = get_context();
expr_ref e(_e, m);
SASSERT(m_util.is_seq(e));
@ -2698,8 +2703,9 @@ literal theory_seq::mk_eq_empty(expr* _e) {
emp = m_util.str.mk_empty(m.get_sort(e));
literal lit = mk_eq(e, emp, false);
ctx.force_phase(lit);
ctx.force_phase(phase?lit:~lit);
ctx.mark_as_relevant(lit);
TRACE("seq", tout << mk_pp(e, m) << " = empty\n";);
return lit;
}
@ -2797,7 +2803,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
}
else {
#if 0
propagate_not_prefix(e);
propagate_not_prefix2(e);
#else
propagate_non_empty(lit, e1);
if (add_prefix2prefix(e, change)) {
@ -3340,6 +3346,33 @@ void theory_seq::propagate_not_prefix(expr* e) {
add_axiom(lit, e2_is_emp, ~mk_eq(c, d, false), mk_seq_eq(e2, x));
}
/*
!prefix(e1,e2) => len(e1) > 0
!prefix(e1,e2) => len(e1) > len(e2) or e2 = pre(e2,len(e1))post(e2,len(e2)-len(e1)) & pre(e2, len(e1)) != e1
*/
void theory_seq::propagate_not_prefix2(expr* e) {
context& ctx = get_context();
//std::cout << mk_pp(e, m) << " " << ctx.get_scope_level() << "\n";
expr* e1, *e2;
VERIFY(m_util.str.is_prefix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);
if (canonizes(false, e)) {
return;
}
propagate_non_empty(~lit, e1);
expr_ref len_e1(m_util.str.mk_length(e1), m);
expr_ref len_e2(m_util.str.mk_length(e2), m);
expr_ref len_e2_e1(mk_sub(len_e2, len_e1), m);
expr_ref x = mk_skolem(m_pre, e2, len_e1);
expr_ref y = mk_skolem(m_post, e2, len_e2_e1);
literal e2_ge_e1 = mk_literal(m_autil.mk_ge(len_e2_e1, m_autil.mk_int(0)));
add_axiom(lit, ~e2_ge_e1, mk_seq_eq(e2, mk_concat(x, y)));
add_axiom(lit, ~e2_ge_e1, mk_eq(m_util.str.mk_length(x), len_e1, false));
add_axiom(lit, ~e2_ge_e1, ~mk_eq(e1, x, false));
}
/*
!suffix(e1,e2) => e1 != ""
!suffix(e1,e2) => e2 = "" or e1 = ycx & (e2 = zdx & c != d or x = e2)
@ -3403,7 +3436,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
conc = mk_concat(head2, tail2);
propagate_eq(~e2_is_emp, e2, conc, true);
literal e1_is_emp = mk_eq_empty(e1);
literal e1_is_emp = mk_eq_empty(e1, false);
switch (ctx.get_assignment(e1_is_emp)) {
case l_true:
TRACE("seq", tout << mk_pp(e, m) << ": " << mk_pp(e1, m) << " != empty\n";);

3
src/smt/theory_seq.h
View file

@ -441,7 +441,7 @@ namespace smt {
void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n);
literal mk_eq_empty(expr* n, bool phase = true);
literal mk_seq_eq(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
expr_ref mk_sub(expr* a, expr* b);
@ -489,6 +489,7 @@ namespace smt {
bool add_suffix2suffix(expr* e, bool& change);
bool add_contains2contains(expr* e, bool& change);
void propagate_not_prefix(expr* e);
void propagate_not_prefix2(expr* e);
void propagate_not_suffix(expr* e);
void ensure_nth(literal lit, expr* s, expr* idx);
bool canonizes(bool sign, expr* e);