diff --git a/src/ast/rewriter/seq_membership_length_constraints.cpp b/src/ast/rewriter/seq_membership_length_constraints.cpp index b95cbc5dd1..6faf5523cb 100644 --- a/src/ast/rewriter/seq_membership_length_constraints.cpp +++ b/src/ast/rewriter/seq_membership_length_constraints.cpp @@ -16,17 +16,113 @@ Abstract: namespace seq { +bool membership_length_constraints::is_var(expr* term) const { + return m_is_var ? m_is_var(term) : is_uninterp(term); +} + +bool membership_length_constraints::length_interval(expr* regex, unsigned& lo, unsigned& hi) const { + auto& re = m_rw.u().re; + expr* body = nullptr, *head = nullptr, *tail = nullptr; + unsigned lower = 0, upper = 0; + if (re.is_full_char(regex)) { + lo = hi = 1; + return true; + } + if (re.is_epsilon(regex)) { + lo = hi = 0; + return true; + } + if (re.is_loop(regex, body, lower, upper) && re.is_full_char(body)) { + lo = lower; + hi = upper; + return true; + } + if (!re.is_concat(regex, head, tail) || !re.is_full_seq(tail)) + return false; + if (re.is_full_char(head)) { + lo = 1; + hi = UINT_MAX; + return true; + } + if (re.is_loop(head, body, lower, upper) && re.is_full_char(body) && lower == upper) { + lo = lower; + hi = UINT_MAX; + return true; + } + return false; +} + lbool membership_length_constraints::check(constraint_vector const& constraints) { m_core.reset(); + obj_map lo_bounds; + obj_map lo_dependencies; + for (auto const& [term, regex, dependency] : constraints) { + unsigned lo = 0, hi = 0, current = 0; + if (length_interval(regex, lo, hi) && lo > 0 && + (!lo_bounds.find(term.get(), current) || lo > current)) { + lo_bounds.insert(term.get(), lo); + lo_dependencies.insert(term.get(), dependency); + } + } + + auto add_dependency = [&](void* dependency) { + if (!dependency) + return; + for (void* existing : m_core) + if (existing == dependency) + return; + m_core.push_back(dependency); + }; + + std::function min_length = [&](expr* term, unsigned& result) { + auto& str = m_rw.u().str; + if (str.is_concat(term)) { + result = 0; + for (expr* arg : *to_app(term)) { + unsigned arg_length = 0; + if (!min_length(arg, arg_length)) + return false; + result = add_truncate(result, arg_length); + } + return true; + } + if (str.is_empty(term)) { + result = 0; + return true; + } + zstring value; + if (str.is_string(term, value)) { + result = value.length(); + return true; + } + expr* element = nullptr; + if (str.is_unit(term, element) && m_rw.m().is_value(element)) { + result = 1; + return true; + } + if (!is_var(term)) + return false; + result = 0; + if (lo_bounds.find(term, result) && result > 0) { + void* dependency = nullptr; + if (lo_dependencies.find(term, dependency)) + add_dependency(dependency); + } + return true; + }; + for (auto const& [term, regex, dependency] : constraints) { - unsigned min_length = m_rw.u().str.min_length(term); unsigned max_length = m_rw.u().re.max_length(regex); - if (min_length <= max_length) + if (max_length == UINT_MAX) continue; - if (dependency) - m_core.push_back(dependency); + m_core.reset(); + unsigned lower = 0; + if (!min_length(term, lower) || lower <= max_length) + continue; + add_dependency(dependency); return l_false; } + m_core.reset(); return l_true; } diff --git a/src/ast/rewriter/seq_membership_length_constraints.h b/src/ast/rewriter/seq_membership_length_constraints.h index 5e29a20c26..622ad45c7f 100644 --- a/src/ast/rewriter/seq_membership_length_constraints.h +++ b/src/ast/rewriter/seq_membership_length_constraints.h @@ -15,6 +15,7 @@ Abstract: #include "ast/ast.h" #include "util/lbool.h" #include "util/vector.h" +#include #include class seq_rewriter; @@ -29,10 +30,16 @@ public: private: seq_rewriter& m_rw; ptr_vector m_core; + std::function m_is_var; + + bool is_var(expr* term) const; + bool length_interval(expr* regex, unsigned& lo, unsigned& hi) const; public: explicit membership_length_constraints(seq_rewriter& rw) : m_rw(rw) {} + void set_is_var(std::function const& is_var) { m_is_var = is_var; } + // Return l_false when the constraints are inconsistent and populate core(). // Return l_true when no contradiction was found. lbool check(constraint_vector const& constraints); diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index fb2395fc15..9a3765d954 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -288,6 +288,7 @@ public: void set_is_var(std::function const &is_var) { m_is_var = is_var; + m_length_constraints.set_is_var(is_var); } // Assert a membership (term in regex) to be decided jointly by the next check(). diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index daca2d3627..553def34ba 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -783,19 +783,20 @@ public: ms.push_back(std::make_pair((expr*)x.get(), (expr*)aP.get())); // 2: x in a+ check_core("z in a* (& x in b* & x in a+)", ms, std::set{1, 2}); } - // The term's syntactic minimum length exceeds the regex's finite maximum. + // Lower bounds on repeated variables refine the compound term's minimum length. { m_trail.push_scope(); - m_mon.add(sword("aa"), word("a"), m_dm.mk_leaf(0)); - m_mon.add(y, dotstar(), m_dm.mk_leaf(1)); + m_mon.add_lo(x, 3, m_dm.mk_leaf(0)); + m_mon.add_hi(t_xax, 5, m_dm.mk_leaf(1)); + m_mon.add(y, dotstar(), m_dm.mk_leaf(2)); lbool got = m_mon.check(); std::set ids; core_ids(ids); m_trail.pop_scope(1); - bool ok = got == l_false && ids == std::set{0}; + bool ok = got == l_false && ids == std::set{0, 1}; if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") - << "minimum sequence length exceeds maximum regex length\n"; + << "refined minimum sequence length exceeds maximum regex length\n"; } std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " ("