From 4a5b645d88c68a7d446a7d7096c4fbaffb79681c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Dec 2015 05:37:24 -0800 Subject: [PATCH] automata Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 195 ++++++++++++++++++----------------------- src/smt/theory_seq.h | 33 ++++--- 2 files changed, 99 insertions(+), 129 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ee2b3070e..0b8e71f1c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -223,13 +223,24 @@ theory_seq::theory_seq(ast_manager& m): m_accepts_qhead(0), m_rejects_qhead(0), m_steps_qhead(0) { - m_prefix_sym = "seq.prefix.suffix"; - m_suffix_sym = "seq.suffix.prefix"; - m_left_sym = "seq.left"; - m_right_sym = "seq.right"; - m_contains_left_sym = "seq.contains.left"; - m_contains_right_sym = "seq.contains.right"; - m_accept_sym = "aut.accept"; + m_prefix = "seq.prefix.suffix"; + m_suffix = "seq.suffix.prefix"; + m_left = "seq.left"; + m_right = "seq.right"; + m_contains_left = "seq.contains.left"; + m_contains_right = "seq.contains.right"; + m_accept = "aut.accept"; + m_reject = "aut.reject"; + m_tail = "seq.tail"; + m_head_elem = "seq.head.elem"; + m_seq_first = "seq.first"; + m_seq_last = "seq.last"; + m_indexof_left = "seq.indexof.left"; + m_indexof_right = "seq.indexof.right"; + m_aut_step = "aut.step"; + m_extract_prefix = "seq.extract.prefix"; + m_at_left = "seq.at.left"; + m_at_right = "seq.at.right"; } theory_seq::~theory_seq() { @@ -252,9 +263,6 @@ final_check_status theory_seq::final_check_eh() { if (ctx.inconsistent()) { return FC_CONTINUE; } - if (propagate_automata()) { - return FC_CONTINUE; - } if (branch_variable()) { TRACE("seq", tout << "branch\n";); return FC_CONTINUE; @@ -274,6 +282,9 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << "check_length_coherence\n";); return FC_CONTINUE; } + if (propagate_automata()) { + return FC_CONTINUE; + } if (is_solved()) { TRACE("seq", tout << "is_solved\n";); return FC_DONE; @@ -440,8 +451,8 @@ bool theory_seq::check_length_coherence_tbd() { void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& tail) { sort* char_sort = 0; VERIFY(m_util.is_seq(m.get_sort(e), char_sort)); - tail = mk_skolem(symbol("seq.tail"), e); - expr_ref v(mk_skolem(symbol("seq.head.elem"), e, 0, 0, char_sort), m); + tail = mk_skolem(m_tail, e); + expr_ref v(mk_skolem(m_head_elem, e, 0, 0, char_sort), m); head = m_util.str.mk_unit(v); emp = m_util.str.mk_empty(m.get_sort(e)); } @@ -613,15 +624,15 @@ bool theory_seq::is_var(expr* a) { } bool theory_seq::is_left_select(expr* a, expr*& b) { - return is_skolem(m_left_sym, a) && (b = to_app(a)->get_arg(0), true); + return is_skolem(m_left, a) && (b = to_app(a)->get_arg(0), true); } bool theory_seq::is_right_select(expr* a, expr*& b) { - return is_skolem(m_right_sym, a) && (b = to_app(a)->get_arg(0), true); + return is_skolem(m_right, a) && (b = to_app(a)->get_arg(0), true); } bool theory_seq::is_head_elem(expr* e) const { - return is_skolem(symbol("seq.head.elem"), e); + return is_skolem(m_head_elem, e); } void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { @@ -633,13 +644,6 @@ void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { } } -bool theory_seq::simplify_eqs() { - return pre_process_eqs(true); -} - -bool theory_seq::solve_basic_eqs() { - return pre_process_eqs(false); -} bool theory_seq::pre_process_eqs(bool simplify_or_solve) { context& ctx = get_context(); @@ -782,12 +786,6 @@ bool theory_seq::simplify_and_solve_eqs() { return change; } -void theory_seq::internalize_eq_eh(app * atom, bool_var v) { -} - -bool theory_seq::internalize_atom(app* a, bool) { - return internalize_term(a); -} bool theory_seq::internalize_term(app* term) { TRACE("seq", tout << mk_pp(term, m) << "\n";); @@ -1123,8 +1121,8 @@ void theory_seq::deque_axiom(expr* n) { lit or s = "" or !prefix(s, x*s1) */ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) { - expr_ref s1 = mk_skolem(symbol("seq.first"), s); - expr_ref c = mk_skolem(symbol("seq.last"), s); + expr_ref s1 = mk_skolem(m_seq_first, s); + expr_ref c = mk_skolem(m_seq_last, s); expr_ref s1c(m_util.str.mk_concat(s1, c), m); expr_ref lc(m_util.str.mk_length(c), m); expr_ref one(m_autil.mk_int(1), m); @@ -1178,8 +1176,8 @@ void theory_seq::add_indexof_axiom(expr* i) { offset_ne_zero = ~mk_eq(offset, zero, false); } if (!is_num || r.is_zero()) { - expr_ref x = mk_skolem(m_contains_left_sym, t, s); - expr_ref y = mk_skolem(m_contains_right_sym, t, s); + expr_ref x = mk_skolem(m_contains_left, t, s); + expr_ref y = mk_skolem(m_contains_right, t, s); xsy = m_util.str.mk_concat(x,s,y); literal cnt = mk_literal(m_util.str.mk_contains(t, s)); literal eq_empty = mk_eq(s, emp, false); @@ -1200,8 +1198,8 @@ void theory_seq::add_indexof_axiom(expr* i) { // 0 <= offset & offset < len(t) => len(x) = offset // 0 <= offset & offset < len(t) & ~contains(s, y) => indexof(t, s, offset) = -1 // 0 <= offset & offset < len(t) & contains(s, y) => index(t, s, offset) = indexof(y, s, 0) + len(t) - expr_ref x = mk_skolem(symbol("seq.indexof.left"), t, s, offset); - expr_ref y = mk_skolem(symbol("seq.indexof.right"), t, s, offset); + expr_ref x = mk_skolem(m_indexof_left, t, s, offset); + expr_ref y = mk_skolem(m_indexof_right, t, s, offset); expr_ref indexof(m_util.str.mk_index(y, s, zero), m); // TBD: //literal offset_ge_0 = mk_literal(m_autil.mk_ge(offset, zero)); @@ -1221,8 +1219,8 @@ void theory_seq::add_indexof_axiom(expr* i) { void theory_seq::add_replace_axiom(expr* r) { expr* a, *s, *t; VERIFY(m_util.str.is_replace(r, a, s, t)); - expr_ref x = mk_skolem(m_contains_left_sym, a, s); - expr_ref y = mk_skolem(m_contains_right_sym, a, s); + expr_ref x = mk_skolem(m_contains_left, a, s); + expr_ref y = mk_skolem(m_contains_right, a, s); expr_ref xty(m_util.str.mk_concat(x, t, y), m); expr_ref xsy(m_util.str.mk_concat(x, s, y), m); literal cnt = mk_literal(m_util.str.mk_contains(a ,s)); @@ -1315,12 +1313,10 @@ void theory_seq::add_in_re_axiom(expr* n) { expr_ref emp(m_util.str.mk_empty(m.get_sort(e1)), m); for (unsigned i = 0; i < a->num_states(); ++i) { - expr_ref acc = mk_accept(emp, e2, m_autil.mk_int(i)); - expr_ref rej = mk_reject(emp, e2, m_autil.mk_int(i)); - literal alit = mk_literal(acc); - literal rlit = mk_literal(rej); - add_axiom(a->is_final_state(i)?alit:~alit); - add_axiom(a->is_final_state(i)?~rlit:rlit); + literal acc = mk_accept(emp, e2, i); + literal rej = mk_reject(emp, e2, i); + add_axiom(a->is_final_state(i)?acc:~acc); + add_axiom(a->is_final_state(i)?~rej:rej); } } @@ -1341,14 +1337,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { } for (unsigned i = 0; i < states.size(); ++i) { if (is_true) { - expr_ref acc = mk_accept(e1, e2, m_autil.mk_int(a->init())); - lits.push_back(mk_literal(acc)); + lits.push_back(mk_accept(e1, e2, states[i])); } else { - expr_ref rej = mk_reject(e1, e2, m_autil.mk_int(a->init())); - literal rlit = mk_literal(rej); literal nlit = ~lit; - propagate_lit(0, 1, &nlit, rlit); + propagate_lit(0, 1, &nlit, mk_reject(e1, e2, states[i])); } } if (is_true) { @@ -1393,7 +1386,7 @@ enode* theory_seq::ensure_enode(expr* e) { void theory_seq::add_extract_axiom(expr* e) { expr* s, *i, *l; VERIFY(m_util.str.is_extract(e, s, i, l)); - expr_ref x(mk_skolem(symbol("seq.extract.prefix"), s, e), m); + expr_ref x(mk_skolem(m_extract_prefix, s, e), m); expr_ref ls(m_util.str.mk_length(s), m); expr_ref lx(m_util.str.mk_length(x), m); expr_ref le(m_util.str.mk_length(e), m); @@ -1422,8 +1415,8 @@ void theory_seq::add_at_axiom(expr* e) { expr* s, *i; VERIFY(m_util.str.is_at(e, s, i)); expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m); - x = mk_skolem(symbol("seq.at.left"), s); - y = mk_skolem(symbol("seq.at.right"), s); + x = mk_skolem(m_at_left, s); + y = mk_skolem(m_at_right, s); xey = m_util.str.mk_concat(x, e, y); zero = m_autil.mk_int(0); one = m_autil.mk_int(1); @@ -1512,28 +1505,32 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { expr_ref f(m); if (is_true && m_util.str.is_prefix(e, e1, e2)) { - f = mk_skolem(m_prefix_sym, e1, e2); + f = mk_skolem(m_prefix, e1, e2); f = m_util.str.mk_concat(e1, f); propagate_eq(v, f, e2); } else if (is_true && m_util.str.is_suffix(e, e1, e2)) { - f = mk_skolem(m_suffix_sym, e1, e2); + f = mk_skolem(m_suffix, e1, e2); f = m_util.str.mk_concat(f, e1); propagate_eq(v, f, e2); } else if (is_true && m_util.str.is_contains(e, e1, e2)) { - expr_ref f1 = mk_skolem(m_contains_left_sym, e1, e2); - expr_ref f2 = mk_skolem(m_contains_right_sym, e1, e2); + expr_ref f1 = mk_skolem(m_contains_left, e1, e2); + expr_ref f2 = mk_skolem(m_contains_right, e1, e2); f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e2), f2); propagate_eq(v, f, e1); } else if (is_accept(e)) { - m_trail_stack.push(push_back_vector >(m_accepts)); - m_accepts.push_back(e); + if (is_true) { + m_trail_stack.push(push_back_vector >(m_accepts)); + m_accepts.push_back(e); + } } else if (is_reject(e)) { - m_trail_stack.push(push_back_vector >(m_rejects)); - m_rejects.push_back(e); + if (is_true) { + m_trail_stack.push(push_back_vector >(m_rejects)); + m_rejects.push_back(e); + } } else if (is_step(e)) { if (is_true) { @@ -1659,11 +1656,11 @@ eautomaton* theory_seq::get_automaton(expr* re) { return result; } -expr_ref theory_seq::mk_accept(expr* s, expr* re, expr* state) { - return expr_ref(mk_skolem(m_accept_sym, s, re, state, m.mk_bool_sort()), m); +literal theory_seq::mk_accept(expr* s, expr* re, expr* state) { + return mk_literal(mk_skolem(m_accept, s, re, state, m.mk_bool_sort())); } -expr_ref theory_seq::mk_reject(expr* s, expr* re, expr* state) { - return expr_ref(mk_skolem(m_reject_sym, s, re, state, m.mk_bool_sort()), m); +literal theory_seq::mk_reject(expr* s, expr* re, expr* state) { + return mk_literal(mk_skolem(m_reject, s, re, state, m.mk_bool_sort())); } bool theory_seq::is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& re, unsigned& i, eautomaton*& aut) { @@ -1683,7 +1680,7 @@ bool theory_seq::is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& re, unsi } bool theory_seq::is_step(expr* e) const { - return is_skolem(symbol("aut.step"), e); + return is_skolem(m_aut_step, e); } bool theory_seq::is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const { @@ -1709,7 +1706,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned args.push_back(m_autil.mk_int(i)); args.push_back(m_autil.mk_int(j)); args.push_back(t); - return expr_ref(m_util.mk_skolem(symbol("aut.step"), args.size(), args.c_ptr(), m.mk_bool_sort()), m); + return expr_ref(m_util.mk_skolem(m_aut_step, args.size(), args.c_ptr(), m.mk_bool_sort()), m); } @@ -1718,6 +1715,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned */ void theory_seq::add_accept2step(expr* acc) { context& ctx = get_context(); + SASSERT(ctx.get_assignment(acc) == l_true); expr* s, *re; unsigned src; eautomaton* aut = 0; @@ -1729,8 +1727,7 @@ void theory_seq::add_accept2step(expr* acc) { expr_ref head(m), tail(m), emp(m), step(m); mk_decompose(s, emp, head, tail); literal_vector lits; - literal acc_lit = mk_literal(acc); - lits.push_back(~acc_lit); + lits.push_back(~ctx.get_literal(acc)); lits.push_back(mk_eq(emp, s, false)); for (unsigned i = 0; i < mvs.size(); ++i) { eautomaton::move mv = mvs[i]; @@ -1747,11 +1744,13 @@ void theory_seq::add_accept2step(expr* acc) { */ void theory_seq::add_step2accept(expr* step) { + context& ctx = get_context(); + SASSERT(ctx.get_assignment(step) == l_true); expr* re, *t, *s, *tail, *i, *j; VERIFY(is_step(step, s, tail, re, i, j, t)); - expr_ref acc1 = mk_accept(s, re, i); - expr_ref acc2 = mk_accept(tail, re, j); - add_axiom(~mk_literal(acc1), ~mk_literal(step), mk_literal(acc2)); + literal acc1 = mk_accept(s, re, i); + literal acc2 = mk_accept(tail, re, j); + add_axiom(~acc1, ~ctx.get_literal(step), acc2); } @@ -1759,6 +1758,8 @@ void theory_seq::add_step2accept(expr* step) { rej(s, re, i) & s = t ++ tail => rej(tail, re, j) */ void theory_seq::add_reject2reject(expr* rej) { + context& ctx = get_context(); + SASSERT(ctx.get_assignment(rej) == l_true); expr* s, *re; unsigned src; eautomaton* aut = 0; @@ -1767,65 +1768,37 @@ void theory_seq::add_reject2reject(expr* rej) { if (m_util.str.is_empty(s)) return; eautomaton::moves mvs; aut->get_moves_to(src, mvs); - expr_ref head(m), tail(m), emp(m), rej2(m), conc(m); + expr_ref head(m), tail(m), emp(m), conc(m); mk_decompose(s, emp, head, tail); - literal rej1 = mk_literal(rej); + literal rej1 = ctx.get_literal(rej); for (unsigned i = 0; i < mvs.size(); ++i) { eautomaton::move const& mv = mvs[i]; conc = m_util.str.mk_concat(m_util.str.mk_unit(mv.t()), tail); - rej2 = mk_reject(tail, re, m_autil.mk_int(mv.dst())); - add_axiom(~rej1, ~mk_eq(s, conc, false), mk_literal(rej2)); + literal rej2 = mk_reject(tail, re, m_autil.mk_int(mv.dst())); + add_axiom(~rej1, ~mk_eq(s, conc, false), rej2); } } bool theory_seq::propagate_automata() { context& ctx = get_context(); - bool change = - (m_accepts_qhead < m_accepts.size()) || - (m_rejects_qhead < m_rejects.size()) || - (m_steps_qhead < m_steps.size()); + bool change = false; + if (m_accepts_qhead < m_accepts.size()) + m_trail_stack.push(value_trail(m_accepts_qhead)), change = true; + if (m_rejects_qhead < m_rejects.size()) + m_trail_stack.push(value_trail(m_rejects_qhead)), change = true; + if (m_steps_qhead < m_steps.size()) + m_trail_stack.push(value_trail(m_steps_qhead)), change = true; - if (change) { - m_trail_stack.push(value_trail(m_accepts_qhead)); - m_trail_stack.push(value_trail(m_rejects_qhead)); - m_trail_stack.push(value_trail(m_steps_qhead)); - } while (m_accepts_qhead < m_accepts.size() && !ctx.inconsistent()) { - expr* acc = m_accepts[m_accepts_qhead]; - lbool r = ctx.get_assignment(acc); - SASSERT(l_undef != r); - if (r == l_true) { - add_accept2step(acc); - } + add_accept2step(m_accepts[m_accepts_qhead]); ++m_accepts_qhead; } while (m_rejects_qhead < m_rejects.size() && !ctx.inconsistent()) { - expr* rej = m_rejects[m_rejects_qhead]; - lbool r = ctx.get_assignment(rej); - SASSERT(l_undef != r); - if (r == l_true) { - add_reject2reject(rej); - } + add_reject2reject(m_rejects[m_rejects_qhead]); ++m_rejects_qhead; } while (m_steps_qhead < m_steps.size() && !ctx.inconsistent()) { - expr* step = m_steps[m_steps_qhead]; - lbool r = ctx.get_assignment(step); - switch (r) { - case l_true: { - expr* re, *t, *s, *tail, *i, *j; - VERIFY(is_step(step, s, tail, re, i, j, t)); - expr_ref acc1 = mk_accept(s, re, i); - if (ctx.get_assignment(acc1) != l_false) { - add_step2accept(step); - } - break; - } - case l_false: - break; - default: - UNREACHABLE(); - } + add_step2accept(m_steps[m_steps_qhead]); ++m_steps_qhead; } return change || ctx.inconsistent(); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index ce5da5cae..f19599472 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -277,14 +277,9 @@ namespace smt { arith_util m_autil; th_trail_stack m_trail_stack; stats m_stats; - symbol m_prefix_sym; - symbol m_suffix_sym; - symbol m_contains_left_sym; - symbol m_contains_right_sym; - symbol m_left_sym; // split variable left part - symbol m_right_sym; // split variable right part - symbol m_accept_sym; - symbol m_reject_sym; + symbol m_prefix, m_suffix, m_contains_left, m_contains_right, m_left, m_right, m_accept, m_reject; + symbol m_tail, m_head_elem, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step; + symbol m_extract_prefix, m_at_left, m_at_right; // maintain automata with regular expressions. scoped_ptr_vector m_automata; @@ -293,9 +288,9 @@ namespace smt { unsigned m_accepts_qhead, m_rejects_qhead, m_steps_qhead; virtual final_check_status final_check_eh(); - virtual bool internalize_atom(app*, bool); + virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } virtual bool internalize_term(app*); - virtual void internalize_eq_eh(app * atom, bool_var v); + virtual void internalize_eq_eh(app * atom, bool_var v) {} virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); virtual void assign_eh(bool_var v, bool is_true); @@ -325,10 +320,10 @@ namespace smt { bool check_ineq_coherence(); bool pre_process_eqs(bool simplify_or_solve); - bool simplify_eqs(); + bool simplify_eqs() { return pre_process_eqs(true); } + bool solve_basic_eqs() { return pre_process_eqs(false); } bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep); bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep); - bool solve_basic_eqs(); bool solve_nqs(); bool solve_ne(unsigned i); @@ -385,15 +380,17 @@ namespace smt { // automata utilities void propagate_in_re(expr* n, bool is_true); eautomaton* get_automaton(expr* e); - expr_ref mk_accept(expr* s, expr* re, expr* state); - bool is_accept(expr* acc) const { return is_skolem(m_accept_sym, acc); } + literal mk_accept(expr* s, expr* re, expr* state); + literal mk_accept(expr* s, expr* re, unsigned i) { return mk_accept(s, re, m_autil.mk_int(i)); } + bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); } bool is_accept(expr* acc, expr*& s, expr*& re, unsigned& i, eautomaton*& aut) { - return is_acc_rej(m_accept_sym, acc, s, re, i, aut); + return is_acc_rej(m_accept, acc, s, re, i, aut); } - expr_ref mk_reject(expr* s, expr* re, expr* state); - bool is_reject(expr* rej) const { return is_skolem(m_reject_sym, rej); } + literal mk_reject(expr* s, expr* re, expr* state); + literal mk_reject(expr* s, expr* re, unsigned i) { return mk_reject(s, re, m_autil.mk_int(i)); } + bool is_reject(expr* rej) const { return is_skolem(m_reject, rej); } bool is_reject(expr* rej, expr*& s, expr*& re, unsigned& i, eautomaton*& aut) { - return is_acc_rej(m_reject_sym, rej, s, re, i, aut); + return is_acc_rej(m_reject, rej, s, re, i, aut); } bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& re, unsigned& i, eautomaton*& aut); expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);