From e1fa04b365ee068026b168cb363193b722c43c46 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Apr 2020 16:53:20 -0700 Subject: [PATCH] disable breaking change to model generation Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 36 +++++++++++++++++++++---------- src/ast/rewriter/seq_rewriter.h | 1 + src/smt/theory_seq.cpp | 32 ++++++++++++++++++--------- 3 files changed, 48 insertions(+), 21 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index eef418048..b1a70e2c4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -257,6 +257,19 @@ eautomaton* re2automaton::operator()(expr* e) { return r; } +bool re2automaton::is_unit_char(expr* e, expr_ref& ch) { + zstring s; + expr* c = nullptr; + if (u.str.is_string(e, s) && s.length() == 1) { + ch = u.mk_char(s[0]); + return true; + } + if (u.str.is_unit(e, c)) { + ch = c; + return true; + } + return false; +} eautomaton* re2automaton::re2aut(expr* e) { SASSERT(u.is_re(e)); @@ -287,15 +300,12 @@ eautomaton* re2automaton::re2aut(expr* e) { return a.detach(); } else if (u.re.is_range(e, e1, e2)) { - if (u.str.is_string(e1, s1) && u.str.is_string(e2, s2) && - s1.length() == 1 && s2.length() == 1) { - unsigned start = s1[0]; - unsigned stop = s2[0]; - expr_ref _start(u.mk_char(start), m); - expr_ref _stop(u.mk_char(stop), m); - TRACE("seq", tout << "Range: " << start << " " << stop << "\n";); + expr_ref _start(m), _stop(m); + if (is_unit_char(e1, _start) && + is_unit_char(e2, _stop)) { + TRACE("seq", tout << "Range: " << _start << " " << _stop << "\n";); a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop)); - return a.detach(); + return a.detach(); } else { TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";); @@ -569,7 +579,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case _OP_STRING_STRIDOF: UNREACHABLE(); } + if (st != BR_FAILED && m().get_sort(result) != f->get_range()) { + std::cout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n"; + } CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";); + SASSERT(st == BR_FAILED || m().get_sort(result) == f->get_range()); return st; } @@ -1804,9 +1818,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { TRACE("seq", tout << result << "\n";); return BR_REWRITE_FULL; } + br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { return BR_FAILED; } + br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { if (m_util.re.is_full_seq(a) && m_util.re.is_full_seq(b)) { result = a; @@ -1965,9 +1981,7 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { expr* ac = nullptr, *bc = nullptr; if ((m_util.re.is_complement(a, ac) && ac == b) || (m_util.re.is_complement(b, bc) && bc == a)) { - sort* seq_sort = nullptr; - VERIFY(m_util.is_re(a, seq_sort)); - result = m_util.re.mk_empty(seq_sort); + result = m_util.re.mk_empty(m().get_sort(a)); return BR_DONE; } return BR_FAILED; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 6a6125095..0154a93d5 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -89,6 +89,7 @@ class re2automaton { scoped_ptr m_ba; scoped_ptr m_sa; + bool is_unit_char(expr* e, expr_ref& ch); eautomaton* re2aut(expr* e); eautomaton* seq2aut(expr* e); public: diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5d02d005c..207b2d643 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2388,7 +2388,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { // Shortcut for well-founded values to avoid some quadratic overhead expr* x = nullptr, *y = nullptr, *z = nullptr; - if (m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) && + if (false && m_util.str.is_concat(e, x, y) && m_util.str.is_unit(x, z) && ctx.e_internalized(z) && ctx.e_internalized(y)) { sort* srt = m.get_sort(e); seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt); @@ -3466,15 +3466,23 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { new_eq_eh(deps, n1, n2); } -lbool theory_seq::regex_are_equal(expr* r1, expr* r2) { - if (r1 == r2) { +lbool theory_seq::regex_are_equal(expr* _r1, expr* _r2) { + if (_r1 == _r2) { return l_true; } + expr_ref r1(_r1, m); + expr_ref r2(_r2, m); + m_rewrite(r1); + m_rewrite(r2); + if (r1 == r2) + return l_true; expr* d1 = m_util.re.mk_inter(r1, m_util.re.mk_complement(r2)); expr* d2 = m_util.re.mk_inter(r2, m_util.re.mk_complement(r1)); expr_ref diff(m_util.re.mk_union(d1, d2), m); + m_rewrite(diff); eautomaton* aut = get_automaton(diff); if (!aut) { + std::cout << diff << "\n"; return l_undef; } else if (aut->is_empty()) { @@ -3487,26 +3495,28 @@ lbool theory_seq::regex_are_equal(expr* r1, expr* r2) { void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { - TRACE("seq", tout << mk_bounded_pp(n1->get_owner(), m) << " = " << mk_bounded_pp(n2->get_owner(), m) << "\n";); - if (n1 != n2 && m_util.is_seq(n1->get_owner())) { + expr* e1 = n1->get_owner(); + expr* e2 = n2->get_owner(); + TRACE("seq", tout << mk_bounded_pp(e1, m) << " = " << mk_bounded_pp(e2, m) << "\n";); + if (n1 != n2 && m_util.is_seq(e1)) { theory_var v1 = n1->get_th_var(get_id()); theory_var v2 = n2->get_th_var(get_id()); if (m_find.find(v1) == m_find.find(v2)) { return; } m_find.merge(v1, v2); - expr_ref o1(n1->get_owner(), m); - expr_ref o2(n2->get_owner(), m); + expr_ref o1(e1, m); + expr_ref o2(e2, m); TRACE("seq", tout << mk_bounded_pp(o1, m) << " = " << mk_bounded_pp(o2, m) << "\n";); m_eqs.push_back(mk_eqdep(o1, o2, deps)); solve_eqs(m_eqs.size()-1); enforce_length_coherence(n1, n2); } - else if (n1 != n2 && m_util.is_re(n1->get_owner())) { + else if (n1 != n2 && m_util.is_re(e1)) { // create an expression for the symmetric difference and imply it is empty. enode_pair_vector eqs; literal_vector lits; - switch (regex_are_equal(n1->get_owner(), n2->get_owner())) { + switch (regex_are_equal(e1, e2)) { case l_true: break; case l_false: @@ -3515,7 +3525,9 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { set_conflict(eqs, lits); break; default: - throw default_exception("convert regular expressions into automata"); + std::stringstream strm; + strm << "could not decide equality over: " << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n"; + throw default_exception(strm.str()); } } }