From bd9b5b57353dd518f7353b76deeedd5294c1d9bb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Dec 2015 10:13:19 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 + src/math/automata/automaton.h | 26 ++---- src/smt/smt_model_generator.cpp | 1 + src/smt/theory_seq.cpp | 139 +++++++++++++++++++++++------- src/smt/theory_seq.h | 17 ++-- 5 files changed, 133 insertions(+), 54 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index aa27489ad..a5c3fb403 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -39,7 +39,10 @@ re2automaton::re2automaton(ast_manager& m): m(m), u(m) {} eautomaton* re2automaton::operator()(expr* e) { eautomaton* r = re2aut(e); if (r) { + //display_expr1 disp(m); + //r->display(std::cout, disp); r->compress(); + //r->display(std::cout, disp); } return r; } @@ -61,6 +64,7 @@ eautomaton* re2automaton::re2aut(expr* e) { else if (u.re.is_star(e, e1) && (a = re2aut(e1))) { a->add_final_to_init_moves(); a->add_init_to_final_states(); + return a.detach(); } else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) { diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index df1d37919..54cd02832 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -209,24 +209,16 @@ public: moves mvs; unsigned_vector final; unsigned init = 0; - if (a.has_single_final_sink() && b.initial_state_is_source() && b.init() == 0) { - unsigned offset2 = a.num_states(); - init = a.init(); - append_moves(0, a, mvs); - append_moves(offset2, b, mvs); - append_final(offset2, b, final); - } - else { - unsigned offset1 = 1; - unsigned offset2 = a.num_states() + offset1; - mvs.push_back(move(m, 0, a.init() + offset1)); - append_moves(offset1, a, mvs); - for (unsigned i = 0; i < a.m_final_states.size(); ++i) { - mvs.push_back(move(m, a.m_final_states[i], b.init() + offset2)); - } - append_moves(offset2, b, mvs); - append_final(offset2, b, final); + unsigned offset1 = 1; + unsigned offset2 = a.num_states() + offset1; + mvs.push_back(move(m, 0, a.init() + offset1)); + append_moves(offset1, a, mvs); + for (unsigned i = 0; i < a.m_final_states.size(); ++i) { + mvs.push_back(move(m, a.m_final_states[i] + offset1, b.init() + offset2)); } + append_moves(offset2, b, mvs); + append_final(offset2, b, final); + return alloc(automaton, m, init, final, mvs); } diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 16cf18d2e..88e9761b4 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -361,6 +361,7 @@ namespace smt { } else { enode * child = d.get_enode(); + TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";); child = child->get_root(); app * val = 0; m_root2value.find(child, val); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d4ae23203..63bdedd1e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -77,6 +77,14 @@ expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { return result; } +expr* theory_seq::solution_map::find(expr* e) { + std::pair value; + while (m_map.find(e, value)) { + e = value.first; + } + return e; +} + void theory_seq::solution_map::pop_scope(unsigned num_scopes) { if (num_scopes == 0) return; m_cache.reset(); @@ -185,26 +193,32 @@ final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); TRACE("seq", display(tout);); if (!check_ineqs()) { + ++m_stats.m_check_ineqs; TRACE("seq", tout << ">>check_ineqs\n";); return FC_CONTINUE; } if (simplify_and_solve_eqs()) { + ++m_stats.m_solve_eqs; TRACE("seq", tout << ">>solve_eqs\n";); return FC_CONTINUE; } if (solve_nqs()) { + ++m_stats.m_solve_nqs; TRACE("seq", tout << ">>solve_nqs\n";); return FC_CONTINUE; } if (branch_variable()) { + ++m_stats.m_branch_variable; TRACE("seq", tout << ">>branch_variable\n";); return FC_CONTINUE; } if (!check_length_coherence()) { + ++m_stats.m_check_length_coherence; TRACE("seq", tout << ">>check_length_coherence\n";); return FC_CONTINUE; } if (propagate_automata()) { + ++m_stats.m_propagate_automata; TRACE("seq", tout << ">>propagate_automata\n";); return FC_CONTINUE; } @@ -312,23 +326,27 @@ bool theory_seq::assume_equality(expr* l, expr* r) { } bool theory_seq::propagate_length_coherence(expr* e) { - expr_ref head(m), tail(m), emp(m); + expr_ref head(m), tail(m); rational lo, hi; + + if (!is_var(e) || !m_rep.is_root(e)) { + return false; + } + if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) { + return false; + } TRACE("seq", tout << "Unsolved " << mk_pp(e, m); if (!lower_bound(e, lo)) lo = -rational::one(); if (!upper_bound(e, hi)) hi = -rational::one(); tout << " lo: " << lo << " hi: " << hi << "\n"; ); - if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) { - return false; - } literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true)))); expr_ref seq(e, m); expr_ref_vector elems(m); unsigned _lo = lo.get_unsigned(); for (unsigned j = 0; j < _lo; ++j) { - mk_decompose(seq, emp, head, tail); + mk_decompose(seq, head, tail); elems.push_back(head); seq = tail; } @@ -342,6 +360,10 @@ bool theory_seq::propagate_length_coherence(expr* e) { expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m); add_axiom(~mk_literal(high1), mk_literal(high2)); } + + //m_replay_length_coherence.push_back(e); + //m_replay_length_coherence_qhead = m_replay_length_coherence.size(); + return true; } @@ -357,14 +379,12 @@ bool theory_seq::check_length_coherence() { expr_ref head(m), tail(m); if (propagate_length_coherence(e)) { - //m_replay_length_coherence.push_back(e); - //m_replay_length_coherence_qhead = m_replay_length_coherence.size(); } else if (!assume_equality(e, emp)) { - mk_decompose(e, emp, head, tail); + mk_decompose(e, head, tail); // e = emp \/ e = unit(head.elem(e))*tail(e) expr_ref conc(m_util.str.mk_concat(head, tail), m); - add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false)); + add_axiom(mk_eq_empty(e), mk_eq(e, conc, false)); assume_equality(tail, emp); } return false; @@ -379,10 +399,9 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) { return mk_skolem(m_nth, s, idx, 0, char_sort); } -void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& tail) { +void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { expr* e1, *e2; zstring s; - emp = m_util.str.mk_empty(m.get_sort(e)); if (m_util.str.is_empty(e)) { head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0))); tail = e; @@ -393,7 +412,7 @@ void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& } else if (m_util.str.is_unit(e)) { head = e; - tail = emp; + tail = m_util.str.mk_empty(m.get_sort(e)); } else if (m_util.str.is_concat(e, e1, e2) && m_util.str.is_unit(e1)) { head = e1; @@ -585,7 +604,7 @@ bool theory_seq::is_var(expr* a) { } -bool theory_seq::is_head_elem(expr* e) const { +bool theory_seq::is_nth(expr* e) const { return is_skolem(m_nth, e); } @@ -884,6 +903,13 @@ void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) con void theory_seq::collect_statistics(::statistics & st) const { st.update("seq num splits", m_stats.m_num_splits); st.update("seq num reductions", m_stats.m_num_reductions); + st.update("e", m_stats.m_propagate_automata); + st.update("seq length coherence", m_stats.m_check_length_coherence); + st.update("seq branch", m_stats.m_branch_variable); + st.update("seq solve !=", m_stats.m_solve_nqs); + st.update("seq solve =", m_stats.m_solve_eqs); + st.update("seq check negations", m_stats.m_check_ineqs); + } void theory_seq::init_model(model_generator & mg) { @@ -910,7 +936,6 @@ public: if (values.empty()) { return th.mk_value(n); } - SASSERT(values.size() == n->get_num_args()); return th.mk_value(mg.get_manager().mk_app(n->get_decl(), values.size(), values.c_ptr())); } }; @@ -918,13 +943,35 @@ public: model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { context& ctx = get_context(); - enode_pair_dependency* dep = 0; - expr* e = m_rep.find(n->get_owner(), dep); - expr* e1, *e2; + expr_ref e(m); + expr* e1; + ptr_vector concats; + get_concat(n->get_owner(), concats); + switch (concats.size()) { + case 0: + e = m_util.str.mk_empty(m.get_sort(n->get_owner())); + break; + case 1: + e = concats[0]; + SASSERT(!m_util.str.is_concat(e)); + break; + default: + e = m_rep.find(n->get_owner()); + SASSERT(m_util.str.is_concat(e)); + break; + } seq_value_proc* sv = alloc(seq_value_proc, *this, to_app(e)); - if (m_util.str.is_concat(e, e1, e2)) { - sv->add_dependency(ctx.get_enode(e1)); - sv->add_dependency(ctx.get_enode(e2)); + TRACE("seq", tout << mk_pp(n->get_owner(), m) << " "; + for (unsigned i = 0; i < concats.size(); ++i) { + tout << mk_pp(concats[i], m) << " "; + } + tout << "\n"; + ); + + if (concats.size() > 1) { + for (unsigned i = 0; i < concats.size(); ++i) { + sv->add_dependency(ctx.get_enode(concats[i])); + } } else if (m_util.str.is_unit(e, e1)) { sv->add_dependency(ctx.get_enode(e1)); @@ -932,6 +979,22 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { return sv; } +void theory_seq::get_concat(expr* e, ptr_vector& concats) { + expr* e1, *e2; + while (true) { + e = m_rep.find(e); + if (m_util.str.is_concat(e, e1, e2)) { + get_concat(e1, concats); + e = e2; + continue; + } + if (!m_util.str.is_empty(e)) { + concats.push_back(e); + } + return; + } +} + app* theory_seq::mk_value(app* e) { expr* e1; expr_ref result(e, m); @@ -964,7 +1027,7 @@ app* theory_seq::mk_value(app* e) { result = e; } } - else if (is_head_elem(e)) { + else if (is_nth(e)) { enode* n = get_context().get_enode(e)->get_root(); enode* n0 = n; bool found_value = false; @@ -1088,6 +1151,9 @@ void theory_seq::deque_axiom(expr* n) { if (m_util.str.is_length(n)) { add_length_axiom(n); } + else if (m_util.str.is_empty(n) && !has_length(n)) { + enforce_length(get_context().get_enode(n)); + } else if (m_util.str.is_index(n)) { add_indexof_axiom(n); } @@ -1120,8 +1186,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) { 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); - expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m); - literal s_eq_emp = mk_eq(s, emp, false); + literal s_eq_emp = mk_eq_empty(s); add_axiom(lit1, lit2, s_eq_emp, mk_eq(s, s1c, false)); add_axiom(lit1, lit2, s_eq_emp, mk_eq(lc, one, false)); add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1)))); @@ -1160,7 +1225,6 @@ void theory_seq::add_indexof_axiom(expr* i) { expr_ref emp(m), minus_one(m), zero(m), xsy(m); minus_one = m_autil.mk_int(-1); zero = m_autil.mk_int(0); - emp = m_util.str.mk_empty(m.get_sort(s)); literal offset_ne_zero = null_literal; bool is_num = m_autil.is_numeral(offset, r); if (is_num && r.is_zero()) { @@ -1174,7 +1238,7 @@ void theory_seq::add_indexof_axiom(expr* i) { 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); + literal eq_empty = mk_eq_empty(s); add_axiom(offset_ne_zero, cnt, mk_eq(i, minus_one, false)); add_axiom(offset_ne_zero, ~eq_empty, mk_eq(i, zero, false)); add_axiom(offset_ne_zero, ~cnt, eq_empty, mk_eq(t, xsy, false)); @@ -1263,12 +1327,12 @@ void theory_seq::add_length_axiom(expr* n) { } else { expr_ref zero(m_autil.mk_int(0), m); - expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m); - literal eq1(mk_eq(zero, n, false)); - literal eq2(mk_eq(x, emp, false)); add_axiom(mk_literal(m_autil.mk_ge(n, zero))); - add_axiom(~eq1, eq2); - add_axiom(~eq2, eq1); + + //expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m); + //literal eq1(mk_eq(zero, n, false)); + //literal eq2(mk_eq(x, emp, false)); + //add_axiom(~eq1, eq2); } } @@ -1510,6 +1574,17 @@ literal theory_seq::mk_literal(expr* _e) { return ctx.get_literal(e); } +literal theory_seq::mk_eq_empty(expr* _e) { + expr_ref e(_e, m); + context& ctx = get_context(); + SASSERT(m_util.is_seq(e)); + expr_ref emp(m); + emp = m_util.str.mk_empty(m.get_sort(e)); + literal lit = mk_eq(e, emp, false); + ctx.force_phase(lit); + return lit; +} + void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { context& ctx = get_context(); literal_vector lits; @@ -1681,8 +1756,8 @@ void theory_seq::relevant_eh(app* n) { m_util.str.is_replace(n) || m_util.str.is_extract(n) || m_util.str.is_at(n) || - m_util.str.is_string(n) || - is_step(n)) { + m_util.str.is_empty(n) || + m_util.str.is_string(n)) { enque_axiom(n); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 024a5b8da..5760fb437 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -72,6 +72,7 @@ namespace smt { void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); } bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); } expr* find(expr* e, enode_pair_dependency*& d); + expr* find(expr* e); bool is_root(expr* e) const; void cache(expr* e, expr* r, enode_pair_dependency* d); void reset_cache() { m_cache.reset(); } @@ -246,6 +247,12 @@ namespace smt { void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; unsigned m_num_reductions; + unsigned m_propagate_automata; + unsigned m_check_length_coherence; + unsigned m_branch_variable; + unsigned m_solve_nqs; + unsigned m_solve_eqs; + unsigned m_check_ineqs; }; ast_manager& m; enode_pair_dependency_manager m_dm; @@ -335,13 +342,13 @@ namespace smt { bool occurs(expr* a, expr* b); bool is_var(expr* b); bool add_solution(expr* l, expr* r, enode_pair_dependency* dep); - bool is_left_select(expr* a, expr*& b); - bool is_right_select(expr* a, expr*& b); - bool is_head_elem(expr* a) const; + bool is_nth(expr* a) const; + expr_ref mk_nth(expr* s, expr* idx); expr_ref canonize(expr* e, enode_pair_dependency*& eqs); expr_ref expand(expr* e, enode_pair_dependency*& eqs); void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); + void get_concat(expr* e, ptr_vector& concats); // terms whose meaning are encoded using axioms. void enque_axiom(expr* e); @@ -360,6 +367,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); void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal); expr_ref mk_sub(expr* a, expr* b); enode* ensure_enode(expr* a); @@ -369,9 +377,8 @@ namespace smt { bool upper_bound(expr* s, rational& hi); bool get_length(expr* s, rational& val); - void mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& tail); + void mk_decompose(expr* e, expr_ref& head, expr_ref& tail); expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0); - expr_ref mk_nth(expr* s, expr* idx); bool is_skolem(symbol const& s, expr* e) const; void set_incomplete(app* term);