From 659a7ede84454e3da91675e376bd8b2442f9c061 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Dec 2015 04:25:23 -0800 Subject: [PATCH] automata Signed-off-by: Nikolaj Bjorner --- src/math/automata/automaton.h | 20 +- src/smt/theory_seq.cpp | 391 ++++++++++++++++++++++++++-------- src/smt/theory_seq.h | 26 ++- 3 files changed, 338 insertions(+), 99 deletions(-) diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index 606991f6a..684082170 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -384,15 +384,23 @@ public: return out; } private: + mutable unsigned_vector m_states1, m_states2; + void get_moves(unsigned state, vector const& delta, moves& mvs) const { - unsigned_vector states; - get_epsilon_closure(state, delta, states); - for (unsigned i = 0; i < states.size(); ++i) { - state = states[i]; + m_states1.reset(); + m_states2.reset(); + get_epsilon_closure(state, delta, m_states1); + for (unsigned i = 0; i < m_states1.size(); ++i) { + state = m_states1[i]; moves const& mv1 = delta[state]; for (unsigned j = 0; j < mv1.size(); ++j) { - if (!mv1[j].is_epsilon()) { - mvs.push_back(mv1[j]); + move const& mv = mv1[j]; + if (!mv.is_epsilon()) { + m_states2.reset(); + get_epsilon_closure(mv.dst(), delta, m_states2); + for (unsigned k = 0; k < m_states2.size(); ++k) { + mvs.push_back(move(m, mv.src(), m_states2[k], mv.t())); + } } } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a379d9eed..ee2b3070e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -219,7 +219,10 @@ theory_seq::theory_seq(ast_manager& m): m_rewrite(m), m_util(m), m_autil(m), - m_trail_stack(*this) { + m_trail_stack(*this), + 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"; @@ -249,6 +252,9 @@ 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; @@ -416,19 +422,14 @@ bool theory_seq::check_length_coherence_tbd() { if (is_var(f) && f == e) { expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";); -#if 1 if (!assume_equality(e, emp)) { + expr_ref head(m), tail(m); + mk_decompose(e, emp, head, tail); // e = emp \/ e = unit(head.elem(e))*tail(e) - sort* char_sort = 0; - VERIFY(m_util.is_seq(m.get_sort(e), char_sort)); - expr_ref tail(mk_skolem(symbol("seq.tail"), e), m); - expr_ref v(mk_skolem(symbol("seq.head.elem"), e, 0, 0, char_sort), m); - expr_ref head(m_util.str.mk_unit(v), m); expr_ref conc(m_util.str.mk_concat(head, tail), m); add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false)); assume_equality(tail, emp); } -#endif m_branch_variable_head = j + 1; return false; } @@ -436,6 +437,15 @@ bool theory_seq::check_length_coherence_tbd() { return coherent; } +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); + head = m_util.str.mk_unit(v); + emp = m_util.str.mk_empty(m.get_sort(e)); +} + bool theory_seq::check_ineq_coherence() { bool all_false = true; for (unsigned i = 0; all_false && i < m_ineqs.size(); ++i) { @@ -473,7 +483,7 @@ bool theory_seq::is_solved() { } -void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) { +void theory_seq::propagate_lit(enode_pair_dependency* dep, unsigned n, literal const* lits, literal lit) { context& ctx = get_context(); ctx.mark_as_relevant(lit); vector _eqs; @@ -483,7 +493,7 @@ void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) { justification* js = ctx.mk_justification( ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit)); + get_id(), ctx.get_region(), n, lits, _eqs.size(), _eqs.c_ptr(), lit)); ctx.assign(lit, js); } @@ -1293,11 +1303,12 @@ void theory_seq::add_length_axiom(expr* n) { } } +// // the empty sequence is accepted only in the final states. // membership holds iff the initial state holds. +// void theory_seq::add_in_re_axiom(expr* n) { expr* e1, *e2; - context& ctx = get_context(); VERIFY(m_util.str.is_in_re(n, e1, e2)); eautomaton* a = get_automaton(e2); if (!a) return; @@ -1305,64 +1316,52 @@ 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)); - literal lit = mk_literal(acc); - add_axiom(a->is_final_state(i)?lit:~lit); + 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); } +} + + +void theory_seq::propagate_in_re(expr* n, bool is_true) { + expr* e1, *e2; + VERIFY(m_util.str.is_in_re(n, e1, e2)); + eautomaton* a = get_automaton(e2); + if (!a) return; + if (m_util.str.is_empty(e1)) return; + context& ctx = get_context(); unsigned_vector states; a->get_epsilon_closure(a->init(), states); literal_vector lits; - literal lit = mk_literal(n); - ctx.mark_as_relevant(lit); - lits.push_back(~lit); + literal lit = ctx.get_literal(n); + if (is_true) { + lits.push_back(~lit); + } for (unsigned i = 0; i < states.size(); ++i) { - expr_ref acc = mk_accept(e1, e2, m_autil.mk_int(a->init())); - literal lit2 = mk_literal(acc); - lits.push_back(lit2); - add_axiom(~lit2, lit); + if (is_true) { + expr_ref acc = mk_accept(e1, e2, m_autil.mk_int(a->init())); + lits.push_back(mk_literal(acc)); + } + 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); + } } - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); -} - -eautomaton* theory_seq::get_automaton(expr* re) { - eautomaton* result = 0; - if (m_re2aut.find(re, result)) { - return result; - } - result = re2automaton(m)(re); - if (result) { - display_expr disp(m); - TRACE("seq", result->display(tout, disp);); - } - if (result) { - m_automata.push_back(result); - m_trail_stack.push(push_back_vector >(m_automata)); - } - m_re2aut.insert(re, result); - m_trail_stack.push(insert_obj_map(m_re2aut, 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); -} - - -bool theory_seq::is_accept(expr* acc, expr*& s, expr*& re, unsigned& i, eautomaton*& aut) { - if (is_accept(acc)) { - rational r; - s = to_app(acc)->get_arg(0); - re = to_app(acc)->get_arg(1); - VERIFY(m_autil.is_numeral(to_app(acc)->get_arg(2), r)); - SASSERT(r.is_unsigned()); - i = r.get_unsigned(); - aut = m_re2aut[re]; - return true; - } - else { - return false; + if (is_true) { + if (lits.size() == 2) { + propagate_lit(0, 1, &lit, lits[1]); + } + else { + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + } } } + expr_ref theory_seq::mk_sub(expr* a, expr* b) { expr_ref result(m_autil.mk_sub(a, b), m); m_rewrite(result); @@ -1439,6 +1438,16 @@ void theory_seq::add_at_axiom(expr* e) { add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false)); } +/** + step(s, tail, re, i, j, t) -> s = t ++ tail +*/ +void theory_seq::propagate_step(bool_var v, expr* step) { + expr* re, *t, *s, *tail, *i, *j; + VERIFY(is_step(step, s, tail, re, i, j, t)); + expr_ref conc(m_util.str.mk_concat(m_util.str.mk_unit(t), tail), m); + propagate_eq(v, s, conc); +} + literal theory_seq::mk_literal(expr* _e) { expr_ref e(_e, m); @@ -1499,40 +1508,45 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { void theory_seq::assign_eh(bool_var v, bool is_true) { context & ctx = get_context(); expr* e = ctx.bool_var2expr(v); - if (is_accept(e)) { - // TBD + expr* e1, *e2; + expr_ref f(m); + + if (is_true && m_util.str.is_prefix(e, e1, e2)) { + f = mk_skolem(m_prefix_sym, e1, e2); + f = m_util.str.mk_concat(e1, f); + propagate_eq(v, f, e2); } - else if (is_true) { - expr* e1, *e2; - expr_ref f(m); - if (m_util.str.is_prefix(e, e1, e2)) { - f = mk_skolem(m_prefix_sym, e1, e2); - f = m_util.str.mk_concat(e1, f); - propagate_eq(v, f, e2); - } - else if (m_util.str.is_suffix(e, e1, e2)) { - f = mk_skolem(m_suffix_sym, e1, e2); - f = m_util.str.mk_concat(f, e1); - propagate_eq(v, f, e2); - } - else if (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); - f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e2), f2); - propagate_eq(v, f, e1); - } - else if (m_util.str.is_in_re(e, e1, e2)) { - - // Predicate: accept(e1, e2, state) - // seq.in.re(e1,e2) <-> accept(e1, e2, init) - // accept("", e2, state) <-> state is final in a - // e = head.elem(e)*tail(e) -> accept(e, e2, state) <-> \/ accept(tail(e), e2, state') & label(t) = head.elem(e) for t : state->state' in a - } - else { - UNREACHABLE(); + else if (is_true && m_util.str.is_suffix(e, e1, e2)) { + f = mk_skolem(m_suffix_sym, 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); + 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); + } + else if (is_reject(e)) { + m_trail_stack.push(push_back_vector >(m_rejects)); + m_rejects.push_back(e); + } + else if (is_step(e)) { + if (is_true) { + propagate_step(v, e); + m_trail_stack.push(push_back_vector >(m_steps)); + m_steps.push_back(e); } } + else if (m_util.str.is_in_re(e)) { + propagate_in_re(e, is_true); + } else { + SASSERT(!is_true); //if (m_util.str.is_prefix(e, e1, e2)) { // could add negative prefix axioms: // len(e1) <= len(e2) => e2 = seq.prefix.left(e2)*seq.prefix.right(e2) @@ -1599,9 +1613,11 @@ void theory_seq::relevant_eh(app* n) { m_util.str.is_empty(n) || m_util.str.is_unit(n) || m_util.str.is_string(n) || - m_util.str.is_in_re(n)) { + m_util.str.is_in_re(n) || + is_step(n)) { enque_axiom(n); } +#if 0 if (m_util.str.is_in_re(n) || m_util.str.is_contains(n) || m_util.str.is_suffix(n) || @@ -1620,4 +1636,197 @@ void theory_seq::relevant_eh(app* n) { break; } } +#endif +} + + +eautomaton* theory_seq::get_automaton(expr* re) { + eautomaton* result = 0; + if (m_re2aut.find(re, result)) { + return result; + } + result = re2automaton(m)(re); + if (result) { + display_expr disp(m); + TRACE("seq", result->display(tout, disp);); + } + if (result) { + m_automata.push_back(result); + m_trail_stack.push(push_back_vector >(m_automata)); + } + m_re2aut.insert(re, result); + m_trail_stack.push(insert_obj_map(m_re2aut, 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); +} +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); +} + +bool theory_seq::is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& re, unsigned& i, eautomaton*& aut) { + if (is_skolem(ar, e)) { + rational r; + s = to_app(e)->get_arg(0); + re = to_app(e)->get_arg(1); + VERIFY(m_autil.is_numeral(to_app(e)->get_arg(2), r)); + SASSERT(r.is_unsigned()); + i = r.get_unsigned(); + aut = m_re2aut[re]; + return true; + } + else { + return false; + } +} + +bool theory_seq::is_step(expr* e) const { + return is_skolem(symbol("aut.step"), e); +} + +bool theory_seq::is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const { + if (is_step(e)) { + s = to_app(e)->get_arg(0); + tail = to_app(e)->get_arg(1); + re = to_app(e)->get_arg(2); + i = to_app(e)->get_arg(3); + j = to_app(e)->get_arg(4); + t = to_app(e)->get_arg(5); + return true; + } + else { + return false; + } +} + +expr_ref theory_seq::mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t) { + expr_ref_vector args(m); + args.push_back(s); + args.push_back(tail); + args.push_back(re); + 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); +} + + +/** + acc & s != emp -> \/ step_i_t_j +*/ +void theory_seq::add_accept2step(expr* acc) { + context& ctx = get_context(); + expr* s, *re; + unsigned src; + eautomaton* aut = 0; + VERIFY(is_accept(acc, s, re, src, aut)); + if (!aut) return; + 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), 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(mk_eq(emp, s, false)); + for (unsigned i = 0; i < mvs.size(); ++i) { + eautomaton::move mv = mvs[i]; + step = mk_step(s, tail, re, src, mv.dst(), mv.t()); + lits.push_back(mk_literal(step)); + } + TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); +} + + +/** + acc(s, re, i) & step(head, tail, re, i, j, t) => acc(tail, re, j) +*/ + +void theory_seq::add_step2accept(expr* step) { + 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)); +} + + +/* + rej(s, re, i) & s = t ++ tail => rej(tail, re, j) +*/ +void theory_seq::add_reject2reject(expr* rej) { + expr* s, *re; + unsigned src; + eautomaton* aut = 0; + VERIFY(is_reject(rej, s, re, src, aut)); + if (!aut) return; + 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); + mk_decompose(s, emp, head, tail); + literal rej1 = mk_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)); + } +} + +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()); + + 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); + } + ++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); + } + ++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(); + } + ++m_steps_qhead; + } + return change || ctx.inconsistent(); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index ab0038933..ce5da5cae 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -284,10 +284,13 @@ namespace smt { symbol m_left_sym; // split variable left part symbol m_right_sym; // split variable right part symbol m_accept_sym; + symbol m_reject_sym; // maintain automata with regular expressions. scoped_ptr_vector m_automata; obj_map m_re2aut; + ptr_vector m_accepts, m_rejects, m_steps; + unsigned m_accepts_qhead, m_rejects_qhead, m_steps_qhead; virtual final_check_status final_check_eh(); virtual bool internalize_atom(app*, bool); @@ -332,7 +335,8 @@ namespace smt { bool unchanged(expr* e, expr_ref_vector& es) const { return es.size() == 1 && es[0] == e; } // asserting consequences - void propagate_lit(enode_pair_dependency* dep, literal lit); + void propagate_lit(enode_pair_dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); } + void propagate_lit(enode_pair_dependency* dep, unsigned n, literal const* lits, literal lit); void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2); void propagate_eq(bool_var v, expr* e1, expr* e2); void set_conflict(enode_pair_dependency* dep, literal_vector const& lits = literal_vector()); @@ -372,16 +376,34 @@ namespace smt { expr_ref mk_sub(expr* a, expr* b); enode* ensure_enode(expr* a); + void mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& tail); expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0); bool is_skolem(symbol const& s, expr* e) const; void set_incomplete(app* term); // 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); } - bool is_accept(expr* acc, expr*& s, expr*& re, unsigned& i, eautomaton*& aut); + 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); + } + expr_ref mk_reject(expr* s, expr* re, expr* state); + bool is_reject(expr* rej) const { return is_skolem(m_reject_sym, 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); + } + 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); + bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const; + bool is_step(expr* e) const; + void propagate_step(bool_var v, expr* n); + void add_reject2reject(expr* rej); + void add_accept2step(expr* acc); + void add_step2accept(expr* step); + bool propagate_automata(); // diagnostics void display_equations(std::ostream& out) const;