diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index df06cedfe3..b96a2ba33e 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -43,6 +43,7 @@ z3_add_component(rewriter seq_subset.cpp seq_split.cpp seq_derive.cpp + seq_monadic.cpp seq_range_collapse.cpp seq_range_predicate.cpp seq_rewriter.cpp diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp new file mode 100644 index 0000000000..8fbb553441 --- /dev/null +++ b/src/ast/rewriter/seq_monadic.cpp @@ -0,0 +1,609 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.cpp + +Abstract: + + Whole-language monadic decomposition for regex membership. See seq_monadic.h. + Automaton-based (product-reachability); reach(q) is never materialized as a regex. + + Generic in the element sort. The decomposition, liveness and product-reachability + are element-agnostic; only the *guard algebra* over the derivative cofactor guards + depends on the element sort. For the character sort it is the exact, compact + seq::range_predicate; for any other element sort it is a candidate-basis over the + element values mentioned by the guards (sound and complete for the + {true,false,=,<=,and,or,not} grammar the derivatives emit). The same guard algebra + yields the concrete element used to build a witness sequence. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ + +#include "ast/rewriter/seq_monadic.h" +#include "ast/rewriter/seq_range_collapse.h" +#include "ast/arith_decl_plugin.h" +#include "ast/bv_decl_plugin.h" +#include +#include +#include +#include +#include +#include + +namespace { + +// A conjunction of derivative cofactor guards over the element variable v0 = (:var 0), +// interpreted as the set of element values satisfying it. Two representations by +// element sort: +// * character sort: the exact, compact seq::range_predicate. +// * any other sort: the guard predicate kept symbolically and decided by a candidate +// basis -- the element values mentioned in the guards, plus one fresh value. This +// is sound and complete for the {true,false,=,<=,and,or,not} grammar the derivatives +// emit (over a general element sort only equalities appear). +class guard_set { + ast_manager& m; + seq_util& u; + sort* m_sort; + expr* m_v0; + bool m_is_char; + bool m_ok = true; // false: an unsupported guard was conjoined + seq::range_predicate m_rp; // char representation + expr_ref m_guard; // generic representation (conjunction over v0) + + // ---- generic path: candidate basis ---- + + // element values compared to v0 by the equalities in `g`. + void collect_consts(expr* g, ptr_vector& out) const { + expr* a = nullptr, * b = nullptr; + if (m.is_and(g) || m.is_or(g)) { + for (expr* arg : *to_app(g)) collect_consts(arg, out); + return; + } + if (m.is_not(g, a)) { collect_consts(a, out); return; } + if (m.is_eq(g, a, b)) { + if (a == m_v0 && b != m_v0) out.push_back(b); + else if (b == m_v0 && a != m_v0) out.push_back(a); + } + } + + // evaluate `g` at v0 := cand ; l_undef on a construct outside the grammar. + lbool eval_at(expr* g, expr* cand) const { + expr* a = nullptr, * b = nullptr; + if (m.is_true(g)) return l_true; + if (m.is_false(g)) return l_false; + if (m.is_not(g, a)) { + lbool r = eval_at(a, cand); + return r == l_undef ? l_undef : (r == l_true ? l_false : l_true); + } + if (m.is_and(g)) { + lbool r = l_true; + for (expr* arg : *to_app(g)) { + lbool e = eval_at(arg, cand); + if (e == l_false) return l_false; + if (e == l_undef) r = l_undef; + } + return r; + } + if (m.is_or(g)) { + lbool r = l_false; + for (expr* arg : *to_app(g)) { + lbool e = eval_at(arg, cand); + if (e == l_true) return l_true; + if (e == l_undef) r = l_undef; + } + return r; + } + if (m.is_eq(g, a, b)) { + expr* other = (a == m_v0) ? b : (b == m_v0 ? a : nullptr); + if (!other) return l_undef; + if (other == m_v0) return l_true; + return (cand == other) ? l_true : l_false; // canonical values: identity == equality + } + return l_undef; + } + + // a value of m_sort distinct from every element of `consts`, if one can be built. + bool mk_fresh(ptr_vector const& consts, expr_ref& out) const { + if (m.is_bool(m_sort)) { + bool hasT = false, hasF = false; + for (expr* c : consts) { if (m.is_true(c)) hasT = true; else if (m.is_false(c)) hasF = true; } + if (!hasT) { out = m.mk_true(); return true; } + if (!hasF) { out = m.mk_false(); return true; } + return false; + } + arith_util a(m); + if (a.is_int_real(m_sort)) { + rational mx(0); bool any = false; + for (expr* c : consts) { + rational v; + if (a.is_numeral(c, v)) { if (!any || v > mx) mx = v; any = true; } + } + out = a.mk_numeral(any ? mx + rational(1) : rational(0), a.is_int(m_sort)); + return true; + } + bv_util bv(m); + if (bv.is_bv_sort(m_sort)) { + unsigned sz = bv.get_bv_size(m_sort); + for (unsigned k = 0; k <= consts.size(); ++k) { + rational kv(k); + bool clash = false; + for (expr* c : consts) { + rational v; unsigned bsz = 0; + if (bv.is_numeral(c, v, bsz) && v == kv) { clash = true; break; } + } + if (!clash) { out = bv.mk_numeral(kv, sz); return true; } + } + return false; + } + return false; + } + + lbool generic_eval(expr_ref* witness) const { + ptr_vector consts; + collect_consts(m_guard, consts); + bool saw_undef = false; + for (expr* c : consts) { + lbool r = eval_at(m_guard, c); + if (r == l_true) { if (witness) *witness = expr_ref(c, m); return l_true; } + if (r == l_undef) saw_undef = true; + } + expr_ref fresh(m); + if (mk_fresh(consts, fresh)) { + lbool r = eval_at(m_guard, fresh); + if (r == l_true) { if (witness) *witness = fresh; return l_true; } + if (r == l_undef) saw_undef = true; + } + else + saw_undef = true; // the "distinct from all mentioned values" region is untested + return saw_undef ? l_undef : l_false; + } + +public: + guard_set(ast_manager& _m, seq_util& _u, sort* elem_sort, expr* v0) + : m(_m), u(_u), m_sort(elem_sort), m_v0(v0), + m_is_char(_u.is_char(elem_sort)), + m_rp(_u.max_char()), m_guard(_m) { + if (m_is_char) m_rp = seq::range_predicate::top(u.max_char()); + else m_guard = m.mk_true(); + } + + bool ok() const { return m_ok; } + + // AND in a cofactor guard g (a Boolean over v0). + void conjoin(expr* g) { + if (!m_ok) return; + if (m_is_char) { + seq::range_predicate s(u.max_char()); + if (!seq::guard_to_range_predicate(u, m_v0, g, s)) { m_ok = false; return; } + m_rp = m_rp & s; + } + else + m_guard = m.mk_and(m_guard, g); + } + + // l_false = empty, l_true = non-empty (sets *witness if non-null to a concrete + // element of the set), l_undef = unknown / unsupported guard. + lbool eval(expr_ref* witness) const { + if (!m_ok) return l_undef; + if (m_is_char) { + if (m_rp.is_empty()) return l_false; + if (witness) *witness = expr_ref(u.mk_char(m_rp[0].first), m); + return l_true; + } + return generic_eval(witness); + } +}; + +} + +expr_ref seq_monadic::der_elem(expr* r, expr* elem) { + expr_ref d = m_rw.mk_derivative(elem, r); // mk_derivative(element, regex) + // Normalize: for a general element sort the derivative by a non-matching constant can + // leave a ground guard (e.g. (= 1 2)) unfolded; simplifying collapses such dead + // branches to re.empty so nullability/emptiness stay decidable. + expr_ref d2(m); + m_thrw(d, d2); + return d2; +} + +void seq_monadic::live_states(expr* R, ptr_vector& out, bool& ok) { + ok = true; + obj_map id; + expr_ref_vector states(m); + vector> succ; + bool_vector maybe_null; + auto intern = [&](expr* s) -> unsigned { + unsigned k; + if (id.find(s, k)) return k; + k = states.size(); + id.insert(s, k); + states.push_back(s); + succ.push_back(svector()); + expr_ref nb = m_rw.is_nullable(s); + maybe_null.push_back(!m.is_false(nb)); // unknown nullability => keep (conservative) + return k; + }; + intern(R); + const unsigned STATE_CAP = 1u << 12; + for (unsigned i = 0; i < states.size(); ++i) { + if (states.size() > STATE_CAP || !m.inc()) { ok = false; return; } + expr_ref_pair_vector cof(m); + m_rw.brz_derivative_cofactors(states.get(i), cof); + for (auto const& [g, t] : cof) { + if (re().is_empty(t)) continue; + unsigned k = intern(t); // MUST precede succ[i] indexing: intern may + succ[i].push_back(k); // grow (realloc) succ, invalidating succ[i]& + } + } + unsigned n = states.size(); + bool_vector live; + live.resize(n, false); + for (unsigned i = 0; i < n; ++i) + live[i] = maybe_null[i]; + for (bool ch = true; ch; ) { + ch = false; + for (unsigned i = 0; i < n; ++i) + if (!live[i]) + for (unsigned j : succ[i]) + if (live[j]) { live[i] = true; ch = true; break; } + } + for (unsigned i = 0; i < n; ++i) + if (live[i]) { out.push_back(states.get(i)); m_pin.push_back(states.get(i)); } +} + +lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* witness_word) { + unsigned n = comps.size(); + if (n == 0) { + if (witness_word) + *witness_word = expr_ref(u().str.mk_empty(m_seq_sort), m); + return l_true; + } + expr_ref var0(m.mk_var(0, m_elem_sort), m); // the element variable the guards range over + + svector start; + for (auto const& c : comps) + start.push_back(c.state); + + auto id_key = [&](svector const& st) { + std::vector k; + k.reserve(st.size()); + for (expr* e : st) k.push_back(e->get_id()); + return k; + }; + typedef std::vector key; + + bool undecided = false; + auto is_accept = [&](svector const& st) -> bool { + for (unsigned i = 0; i < n; ++i) { + if (comps[i].target) { + if (st[i] != comps[i].target) return false; + } + else { + expr_ref nb = m_rw.is_nullable(st[i]); + if (m.is_true(nb)) continue; + if (m.is_false(nb)) return false; + undecided = true; return false; + } + } + return true; + }; + + std::set visited; + std::vector> work; + // tree of first-discovery edges for witness reconstruction (only built when a + // witness is requested): child-key -> (parent-key, element read on the edge). + std::map> parent; + key start_key = id_key(start); + + auto reconstruct = [&](key end_key) -> expr_ref { + ptr_vector elems; // collected in accept..start order + key k = end_key; + while (k != start_key) { + auto it = parent.find(k); + if (it == parent.end()) break; // safety (should not happen) + elems.push_back(it->second.second); + k = it->second.first; + } + expr_ref_vector es(m); // start..accept order + for (unsigned idx = elems.size(); idx-- > 0; ) + es.push_back(u().str.mk_unit(elems[idx])); + if (es.empty()) + return expr_ref(u().str.mk_empty(m_seq_sort), m); + return expr_ref(u().str.mk_concat(es.size(), es.data(), m_seq_sort), m); + }; + + work.push_back(start); + visited.insert(start_key); + + while (!work.empty()) { + if (m_budget == 0) { m_giveup = true; return l_undef; } + --m_budget; + if (!m.inc()) + return l_undef; + svector st = work.back(); + work.pop_back(); + if (is_accept(st)) { + if (witness_word) + *witness_word = reconstruct(id_key(st)); + return l_true; + } + if (undecided) + return l_undef; + + // per-component cofactor branches (target, guard); pin both, they outlive `cof`. + std::vector>> branches(n); + for (unsigned i = 0; i < n; ++i) { + expr_ref_pair_vector cof(m); + m_rw.brz_derivative_cofactors(st[i], cof); + for (auto const& [g, t] : cof) { + if (re().is_empty(t)) continue; + m_pin.push_back(t); + m_pin.push_back(g); + branches[i].push_back(std::make_pair((expr*) t, (expr*) g)); + } + } + + // joint transitions = cartesian product of the branches with the guards + // conjoined; prune as soon as the accumulated guard is empty, bail on unknown. + svector cur; + cur.resize(n); + key st_key = id_key(st); + bool bail = false; + std::function rec = + [&](unsigned i, guard_set const& acc) { + if (bail) return; + if (i == n) { + key ck = id_key(cur); + if (visited.find(ck) == visited.end()) { + visited.insert(ck); + if (witness_word) { + expr_ref e(m); + if (acc.eval(&e) == l_true) { + m_pin.push_back(e); + parent[ck] = std::make_pair(st_key, e.get()); + } + } + work.push_back(cur); + } + return; + } + for (auto const& pr : branches[i]) { + guard_set nacc = acc; + nacc.conjoin(pr.second); + lbool ne = nacc.eval(nullptr); + if (ne == l_undef) { bail = true; return; } // non-range / unknown guard + if (ne == l_false) continue; // empty joint guard: prune + cur[i] = pr.first; + rec(i + 1, nacc); + if (bail) return; + } + }; + guard_set top(m, u(), m_elem_sort, var0); + rec(0, top); + if (bail) + return l_undef; + } + return l_false; +} + +bool seq_monadic::parse_term(expr* t, svector& atoms, expr*& the_var) { + if (u().str.is_concat(t)) { + app* a = to_app(t); + for (unsigned i = 0; i < a->get_num_args(); ++i) + if (!parse_term(a->get_arg(i), atoms, the_var)) + return false; + return true; + } + if (u().str.is_empty(t)) + return true; // epsilon: contributes nothing + zstring s; + if (u().str.is_string(t, s)) { + for (unsigned i = 0; i < s.length(); ++i) + atoms.push_back(atom{ false, nullptr, u().str.mk_char(s, i) }); + return true; + } + if (u().str.is_unit(t)) { // seq.unit of a constant element + expr* elem = to_app(t)->get_arg(0); + if (m.is_value(elem)) { + atoms.push_back(atom{ false, nullptr, elem }); + return true; + } + return false; // symbolic (non-constant) unit: unsupported + } + // uninterpreted 0-ary constant of sequence sort => a sequence variable + if (is_app(t) && to_app(t)->get_num_args() == 0 && + to_app(t)->get_family_id() == null_family_id) { + the_var = t; // mark that at least one variable occurs + atoms.push_back(atom{ true, t, nullptr }); + return true; + } + return false; +} + +void seq_monadic::decompose(svector const& atoms, unsigned i, expr* R, + vector& out, bool& ok) { + if (!ok) + return; + if (m_giveup) { ok = false; return; } + m_pin.push_back(R); + if (i == atoms.size()) { + expr_ref nb = m_rw.is_nullable(R); + if (m.is_true(nb)) + out.push_back(disjunct()); // empty conjunction = true + else if (!m.is_false(nb)) + ok = false; // undecidable nullability => bail + return; + } + atom const& a = atoms[i]; + if (!a.is_var) { + expr_ref d = der_elem(R, a.elem); + decompose(atoms, i + 1, d, out, ok); + return; + } + if (i + 1 == atoms.size()) { // last atom: membership component a.var in R + disjunct D; + D.push_back(component{ a.var, R, nullptr }); + out.push_back(D); + return; + } + // a variable with a non-empty rest: split over the live states q of R (midpoints) + ptr_vector Q; + live_states(R, Q, ok); + if (!ok) + return; + const unsigned DISJUNCT_CAP = 1u << 13; + for (expr* q : Q) { + vector sub; + decompose(atoms, i + 1, q, sub, ok); + if (!ok) + return; + for (disjunct const& sd : sub) { + if (out.size() > DISJUNCT_CAP || m_budget == 0) { m_giveup = true; ok = false; return; } + --m_budget; + disjunct D(sd); + D.push_back(component{ a.var, R, q }); // reach component: a.var drives R -> q + out.push_back(D); + } + } + simplify_dnf(out); +} + +void seq_monadic::simplify_dnf(vector& dnf) { + std::set>> seen; + vector result; + for (disjunct const& D : dnf) { + bool dead = false; + for (auto const& c : D) + if (re().is_empty(c.state)) { dead = true; break; } + if (dead) + continue; + std::vector> sig; + sig.reserve(D.size()); + for (auto const& c : D) + sig.push_back(std::make_tuple(c.var->get_id(), c.state->get_id(), + c.target ? c.target->get_id() : UINT_MAX)); + std::sort(sig.begin(), sig.end()); + if (seen.insert(sig).second) + result.push_back(D); + } + dnf.swap(result); +} + +lbool seq_monadic::solve(expr* term, expr* R) { + obj_map none; + return solve(term, R, none, nullptr); +} + +lbool seq_monadic::solve(expr* term, expr* R, obj_map const& var_extra) { + return solve(term, R, var_extra, nullptr); +} + +bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector& dnf) { + if (!u().is_re(R, m_seq_sort)) + return false; + if (!u().is_seq(m_seq_sort, m_elem_sort)) + return false; + svector atoms; + expr* the_var = nullptr; + if (!parse_term(term, atoms, the_var)) + return false; + if (!the_var) + return false; // no variable: ground membership, not our case + m_pin.push_back(R); + bool ok = true; + decompose(atoms, 0, R, dnf, ok); + return ok; +} + +lbool seq_monadic::decide_dnf(vector const& dnf, obj_map const& var_extra, + obj_map* model) { + bool any_undef = false; + for (disjunct const& D : dnf) { + // group components by variable, add the extra per-variable constraints + obj_map idx; + vector> groups; + ptr_vector group_var; + auto bucket = [&](expr* v) -> unsigned { + unsigned gi; + if (idx.find(v, gi)) return gi; + gi = groups.size(); idx.insert(v, gi); + groups.push_back(svector()); + group_var.push_back(v); + return gi; + }; + for (auto const& c : D) + groups[bucket(c.var)].push_back(c); + for (auto const& kv : var_extra) + groups[bucket(kv.m_key)].push_back(component{ kv.m_key, kv.m_value, nullptr }); + + bool has_empty = false, has_undef = false; + obj_map local; // var -> witness for this disjunct + for (unsigned gi = 0; gi < groups.size(); ++gi) { + expr_ref w(m); + lbool ne = product_nonempty(groups[gi], model ? &w : nullptr); + if (ne == l_false) { has_empty = true; break; } // this variable has no value + if (ne == l_undef) { has_undef = true; continue; } + if (model) { m_pin.push_back(w); local.insert(group_var[gi], w.get()); } + } + if (has_empty) continue; + if (has_undef) { any_undef = true; continue; } + if (model) + for (auto const& kv : local) + model->insert(kv.m_key, kv.m_value); + return l_true; // all variables satisfiable => sat + } + return any_undef ? l_undef : l_false; +} + +lbool seq_monadic::solve(expr* term, expr* R, obj_map const& var_extra, + obj_map* model) { + m_pin.reset(); + m_budget = 200000; // global work budget: bail fast on DNF explosion + m_giveup = false; + vector dnf; + if (!build_membership_dnf(term, R, dnf)) + return l_undef; + return decide_dnf(dnf, var_extra, model); +} + +lbool seq_monadic::solve_and(vector> const& mems, + obj_map const& var_extra, obj_map* model) { + if (mems.empty()) + return l_undef; + m_pin.reset(); + m_budget = 200000; + m_giveup = false; + // Multiply the per-membership DNFs: combined = { d ++ e : d in combined, e in dnf_i }. + // A variable shared by several memberships thus gets several components in the same + // disjunct, which decide_dnf/product_nonempty intersect -- enforcing one consistent + // value across all memberships (the joint solve the harness could not do per-term). + vector combined; + combined.push_back(disjunct()); // { true } + const unsigned DNF_CAP = 1u << 14; + for (auto const& tr : mems) { + vector dnf_i; + if (!build_membership_dnf(tr.first, tr.second, dnf_i)) + return l_undef; + vector next; + for (disjunct const& d : combined) { + for (disjunct const& e : dnf_i) { + if (next.size() > DNF_CAP || m_budget == 0) { m_giveup = true; return l_undef; } + --m_budget; + disjunct D(d); + for (auto const& c : e) + D.push_back(c); + next.push_back(D); + } + } + combined.swap(next); + simplify_dnf(combined); + if (combined.empty()) + return l_false; // no viable disjunct left => unsat + } + return decide_dnf(combined, var_extra, model); +} diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h new file mode 100644 index 0000000000..d979134e47 --- /dev/null +++ b/src/ast/rewriter/seq_monadic.h @@ -0,0 +1,148 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.h + +Abstract: + + Whole-language monadic decomposition for regex membership of a term that is a + concatenation of sequence variables and constant elements, e.g. x.a.x in R. + Generic in the element sort: characters are one instance, but the procedure works + for any sequence element sort (the guard algebra falls back from the exact character + range_predicate to a candidate-basis over the element values mentioned by the + derivatives). + + Self-contained decision procedure: NO Nielsen splitting (seq_split), NO minterms, + and NO materialization of reach(q) as a regex. It relies only on the symbolic + Brzozowski derivative (brz_derivative_cofactors as a transition regex) and on + automaton product-reachability for emptiness. + + Method. For a term x.u in R and the whole-language split, x drives the derivative + automaton of R from R to some live state q, and the rest u must be accepted from q: + + x.u in R <=> OR_{q live} ( x reaches q in A_R /\ u in q ). + + Decomposing u recursively (a leading constant is consumed by a derivative, a leading + variable splits again, the last variable is a plain membership) yields a DNF whose + disjuncts are conjunctions of per-variable *components*: + + - reach component : the variable's value drives the + derivative automaton from state0 to q + - membership component : the variable's value is in L(state0) + + reach(q) is therefore NEVER built as a regex (which state-elimination would blow up + super-polynomially for lattice-shaped automata). Instead the constraints on a + variable are decided directly by a lazy product-reachability search over tuples of + component states: a product state accepts iff every reach component is at its target + and every membership component is nullable; transitions are the product of the + components' cofactor branches with pairwise-conjoined range guards (minterm-free). + This stays in the product-of-state-counts regime, never the path-enumeration (k!) + regime of regex state-elimination. + + Supports single / multiple / repeated variables, and per-variable extra constraints + (base membership + length-regex) via `var_extra`. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ +#pragma once + +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_range_predicate.h" +#include "ast/rewriter/th_rewriter.h" +#include "util/lbool.h" +#include "util/obj_hashtable.h" +#include + +class seq_monadic { + ast_manager& m; + seq_rewriter& m_rw; + th_rewriter m_thrw; // normalizes constant-element derivatives (folds + // ground guards so dead states become re.empty) + sort* m_seq_sort = nullptr; // sequence sort of the regex under analysis + sort* m_elem_sort = nullptr; // element sort of that sequence sort + expr_ref_vector m_pin; // pins derivative states / witnesses referenced later + unsigned m_budget = 0; // global work budget (decompose disjuncts + product pops) + bool m_giveup = false; // set when the budget is exhausted + + seq_util& u() const { return m_rw.u(); } + seq_util::rex& re() const { return m_rw.u().re; } + + // A term atom: a sequence variable or a constant element (a value of the element sort). + struct atom { bool is_var; expr* var; expr* elem; }; + + // A component of one variable's constraint. As the variable's value w is read, + // the current state is derived from `state`; the component accepts when + // target ? (current == target) -- reach component (w drives A from state to target) + // : nullable(current) -- membership component (w in L(state)) + struct component { expr* var; expr* state; expr* target; }; + + typedef svector disjunct; // a conjunction of components (a DNF disjunct) + + // Brzozowski derivative of regex `r` by the concrete element `elem`. + expr_ref der_elem(expr* r, expr* elem); + + // Live reachable derivative states of R (BFS over cofactor targets + liveness + // least-fixpoint). These are the split states q. Sets `ok` false on a cap overrun. + void live_states(expr* R, ptr_vector& out, bool& ok); + + // Product-reachability emptiness of a conjunction of components (all on one + // variable). l_false = empty (unsat), l_true = non-empty (sat), l_undef = gave up + // (cap overrun, non-range guard, or undecidable nullability). + // On l_true, if `witness_word` is non-null it is set to a concrete sequence term + // (over the element sort) whose value drives every component to acceptance + // simultaneously -- i.e. a witness value for the variable the components constrain. + lbool product_nonempty(svector const& comps, expr_ref* witness_word = nullptr); + + // Flatten a str.++ term into atoms; false on an unsupported shape (non-constant unit). + bool parse_term(expr* term, svector& atoms, expr*& the_var); + + // Monadic decomposition: append to `out` the DNF disjuncts for atoms[i..] in R, + // threading the current derivative state R. `ok` false on give-up. + void decompose(svector const& atoms, unsigned i, expr* R, + vector& out, bool& ok); + + // Drop disjuncts with a syntactically-empty component and dedup identical disjuncts. + void simplify_dnf(vector& dnf); + + // Build the DNF over primitive per-variable components for one membership term in R. + // Sets m_seq_sort/m_elem_sort; false on an unsupported shape or give-up. + bool build_membership_dnf(expr* term, expr* R, vector& dnf); + + // Decide a DNF (over primitive components): sat iff some disjunct has every variable + // group non-empty. On l_true, fills `model` (var -> witness) if non-null. + lbool decide_dnf(vector const& dnf, obj_map const& var_extra, + obj_map* model); + +public: + seq_monadic(seq_rewriter& rw) : m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_pin(rw.m()) {} + + // Decide (str.in_re term R) for a term that is a concatenation of string variables + // (possibly repeated / several distinct) and constant characters. + // l_true = sat, l_false = unsat, l_undef = unsupported shape / gave up. + lbool solve(expr* term, expr* R); + + // As above, with extra per-variable constraints (e.g. a base membership intersected + // with a length-regex): `var_extra` maps a variable to a regex it must also satisfy. + lbool solve(expr* term, expr* R, obj_map const& var_extra); + + // As above; on l_true, if `model` is non-null it is populated with var -> witness, + // where each witness is a concrete sequence term (over the element sort) giving one + // satisfying assignment. Witness terms are pinned by the solver and remain valid + // until the next call to solve(). + lbool solve(expr* term, expr* R, obj_map const& var_extra, + obj_map* model); + + // Decide a CONJUNCTION of memberships AND_i (term_i in R_i) jointly: a variable + // shared across memberships is constrained consistently (the DNFs are multiplied and + // each variable's constraints intersected). This is the natural extension of single- + // membership solving to a Boolean combination of memberships (a disjunction is the + // union of DNFs; a negated membership ~(t in R) is just t in complement(R)). + // var_extra / model as above. l_true = sat, l_false = unsat, l_undef = gave up. + lbool solve_and(vector> const& mems, + obj_map const& var_extra, obj_map* model = nullptr); +}; diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index 8206ef5c1f..4ddcf1048b 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -21,66 +21,66 @@ Authors: namespace seq { - // Cofactor path condition `pred` (a Boolean over x = (:var 0)) -> the canonical - // range_predicate (union of ranges) of the characters satisfying it. Returns - // false on a construct outside {true,false,and,or,not,=,char.<=} over x. - static bool pred_to_rp(ast_manager &m, seq_util &sq, expr *x, expr *pred, - seq::range_predicate &out) { - unsigned maxc = sq.max_char(); - expr *a = nullptr, *b = nullptr; + // Cofactor guard `guard` (a Boolean over the character variable v0 = (:var 0)) -> + // the canonical range_predicate (union of ranges) of the characters satisfying it. + // Returns false on a construct outside {true,false,and,or,not,=,char.<=} over v0. + bool guard_to_range_predicate(seq_util& u, expr* v0, expr* guard, range_predicate& out) { + ast_manager& m = u.get_manager(); + unsigned maxc = u.max_char(); + expr* a = nullptr, * b = nullptr; unsigned c = 0; - if (m.is_true(pred)) { - out = seq::range_predicate::top(maxc); + if (m.is_true(guard)) { + out = range_predicate::top(maxc); return true; } - if (m.is_false(pred)) { - out = seq::range_predicate::empty(maxc); + if (m.is_false(guard)) { + out = range_predicate::empty(maxc); return true; } - if (m.is_eq(pred, a, b)) { - if (a == x && sq.is_const_char(b, c)) { - out = seq::range_predicate::singleton(c, maxc); + if (m.is_eq(guard, a, b)) { + if (a == v0 && u.is_const_char(b, c)) { + out = range_predicate::singleton(c, maxc); return true; } - if (b == x && sq.is_const_char(a, c)) { - out = seq::range_predicate::singleton(c, maxc); + if (b == v0 && u.is_const_char(a, c)) { + out = range_predicate::singleton(c, maxc); return true; } return false; } - if (sq.is_char_le(pred, a, b)) { - if (b == x && sq.is_const_char(a, c)) { - out = seq::range_predicate::range(c, maxc, maxc); + if (u.is_char_le(guard, a, b)) { + if (b == v0 && u.is_const_char(a, c)) { + out = range_predicate::range(c, maxc, maxc); return true; } - if (a == x && sq.is_const_char(b, c)) { - out = seq::range_predicate::range(0, c, maxc); + if (a == v0 && u.is_const_char(b, c)) { + out = range_predicate::range(0, c, maxc); return true; } return false; } - if (m.is_not(pred, a)) { - seq::range_predicate s(maxc); - if (!pred_to_rp(m, sq, x, a, s)) + if (m.is_not(guard, a)) { + range_predicate s(maxc); + if (!guard_to_range_predicate(u, v0, a, s)) return false; out = ~s; return true; } - if (m.is_and(pred)) { - out = seq::range_predicate::top(maxc); - for (expr *arg : *to_app(pred)) { - seq::range_predicate s(maxc); - if (!pred_to_rp(m, sq, x, arg, s)) + if (m.is_and(guard)) { + out = range_predicate::top(maxc); + for (expr *arg : *to_app(guard)) { + range_predicate s(maxc); + if (!guard_to_range_predicate(u, v0, arg, s)) return false; out = out & s; } return true; } - if (m.is_or(pred)) { - out = seq::range_predicate::empty(maxc); - for (expr *arg : *to_app(pred)) { - seq::range_predicate s(maxc); - if (!pred_to_rp(m, sq, x, arg, s)) + if (m.is_or(guard)) { + out = range_predicate::empty(maxc); + for (expr *arg : *to_app(guard)) { + range_predicate s(maxc); + if (!guard_to_range_predicate(u, v0, arg, s)) return false; out = out | s; } @@ -183,7 +183,7 @@ namespace seq { auto body = q->get_expr(); sort *char_sort = q->get_decl_sort(0); expr_ref var(m.mk_var(0, char_sort), m); - if (u.get_char_plugin().get_family_id() == char_sort->get_family_id() && pred_to_rp(m, u, var, body, out)) + if (u.get_char_plugin().get_family_id() == char_sort->get_family_id() && guard_to_range_predicate(u, var, body, out)) return true; } diff --git a/src/ast/rewriter/seq_range_collapse.h b/src/ast/rewriter/seq_range_collapse.h index f6effc8ee4..6255ac2294 100644 --- a/src/ast/rewriter/seq_range_collapse.h +++ b/src/ast/rewriter/seq_range_collapse.h @@ -31,6 +31,14 @@ Authors: namespace seq { + /** + * Convert a Boolean guard over the single character variable v0 = (:var 0) -- a + * derivative cofactor path condition -- into the range_predicate of the characters + * satisfying it. Recognizes {true, false, =, char.<=, and, or, not} over v0 and + * concrete characters; returns false (out untouched) on anything else. + */ + bool guard_to_range_predicate(seq_util& u, expr* v0, expr* guard, range_predicate& out); + /** * If r is a boolean combination of character-class regex primitives * over the unsigned character domain [0, max_char], compute the diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 61b13aa7c9..3175b2d4bc 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -24,7 +24,6 @@ add_executable(test-z3 api_datalog.cpp parametric_datatype.cpp arith_rewriter.cpp - seq_rewriter.cpp arith_simplifier_plugin.cpp ast.cpp bdd.cpp @@ -132,6 +131,8 @@ add_executable(test-z3 sat_user_scope.cpp scoped_timer.cpp scoped_vector.cpp + seq_rewriter.cpp + seq_monadic.cpp simple_parser.cpp scanner_io.cpp simplex.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 4899f656ff..89b1f09e51 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -116,6 +116,7 @@ X(range_predicate) \ X(regex_range_collapse) \ X(seq_rewriter) \ + X(seq_monadic) \ X(check_assumptions) \ X(smt_context) \ X(theory_dl) \ diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp new file mode 100644 index 0000000000..5377aac1a3 --- /dev/null +++ b/src/test/seq_monadic.cpp @@ -0,0 +1,314 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + seq_monadic.cpp + +Abstract: + + Unit tests for the whole-language monadic-decomposition membership solver in + ast/rewriter/seq_monadic.cpp. Mirrors the validated Python prototype + (files/solve_proto.py): single-variable repeated-membership shapes x.a.x in R. + +Author: + + Nikolaj Bjorner / Margus Veanes 2026 + +--*/ + +#include "ast/ast.h" +#include "ast/reg_decl_plugins.h" +#include "ast/seq_decl_plugin.h" +#include "ast/arith_decl_plugin.h" +#include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_monadic.h" +#include "ast/rewriter/expr_safe_replace.h" +#include + +namespace { + +struct plugin_registrar { + plugin_registrar(ast_manager& m) { reg_decl_plugins(m); } +}; + +class seq_monadic_test { + ast_manager m; + plugin_registrar m_reg; + seq_rewriter m_rw; + seq_monadic m_mon; + seq_util u; + sort_ref m_str; // String sort + sort_ref m_re; // RegEx sort over m_str + unsigned m_fail = 0; + + seq_util::rex& re() { return u.re; } + + // regex builders + expr_ref word(char const* s) { return expr_ref(re().mk_to_re(u.str.mk_string(zstring(s))), m); } + expr_ref cat(expr* a, expr* b) { return expr_ref(re().mk_concat(a, b), m); } + expr_ref alt(expr* a, expr* b) { return expr_ref(re().mk_union(a, b), m); } + expr_ref star(expr* a) { return expr_ref(re().mk_star(a), m); } + expr_ref inter(expr* a, expr* b) { return expr_ref(re().mk_inter(a, b), m); } + expr_ref comp(expr* a) { return expr_ref(re().mk_complement(a), m); } + expr_ref dotstar() { return expr_ref(re().mk_full_seq(m_re), m); } + expr_ref rng(char lo, char hi) { + char sl[2] = { lo, 0 }, sh[2] = { hi, 0 }; + return expr_ref(re().mk_range(u.str.mk_string(zstring(sl)), u.str.mk_string(zstring(sh))), m); + } + expr_ref loop(expr* r, unsigned lo, unsigned hi) { return expr_ref(re().mk_loop(r, lo, hi), m); } + + // string-term builders + expr_ref var(char const* nm) { return expr_ref(m.mk_const(nm, m_str), m); } + expr_ref sword(char const* s) { return expr_ref(u.str.mk_string(zstring(s)), m); } + expr_ref sconcat(expr* a, expr* b) { return expr_ref(u.str.mk_concat(a, b), m); } + // term x . w . x (w a constant word) + expr_ref xwx(expr* x, char const* w) { return sconcat(x, sconcat(sword(w), x)); } + // term x . a . y (two distinct variables) + expr_ref xay(expr* x, expr* y) { return sconcat(x, sconcat(sword("a"), y)); } + // term x . y . x + expr_ref xyx(expr* x, expr* y) { return sconcat(x, sconcat(y, x)); } + + static char const* s(lbool l) { return l == l_true ? "sat" : l == l_false ? "unsat" : "undef"; } + + void check(char const* name, expr* term, expr* R, lbool expected) { + lbool got = m_mon.solve(term, R); + bool ok = (got == expected); + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + } + + void check_extra(char const* name, expr* term, expr* R, + obj_map const& ve, lbool expected) { + lbool got = m_mon.solve(term, R, ve); + bool ok = (got == expected); + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + } + + // flatten a ground sequence term into its element values. + void flatten_seq(expr* seqv, ptr_vector& elems) { + zstring zs; + if (u.str.is_concat(seqv)) { + for (expr* arg : *to_app(seqv)) flatten_seq(arg, elems); + return; + } + if (u.str.is_empty(seqv)) + return; + if (u.str.is_string(seqv, zs)) { + for (unsigned i = 0; i < zs.length(); ++i) elems.push_back(u.str.mk_char(zs, i)); + return; + } + if (u.str.is_unit(seqv)) + elems.push_back(to_app(seqv)->get_arg(0)); + } + + // decide membership of a concrete word (list of element values) in R by folding + // derivatives and testing nullability of the residual. + bool word_in_re(ptr_vector const& elems, expr* R) { + expr_ref cur(R, m); + for (expr* e : elems) cur = m_rw.mk_derivative(e, cur); + return m.is_true(m_rw.is_nullable(cur)); + } + + // solve for a model, then check the returned witness assignment actually makes + // term a member of R (substitute var -> witness and re-decide by derivatives). + void check_witness(char const* name, expr* term, expr* R, + obj_map const& ve) { + obj_map model; + lbool got = m_mon.solve(term, R, ve, &model); + bool ok = (got == l_true) && !model.empty(); + if (ok) { + expr_safe_replace rep(m); + for (auto const& kv : model) rep.insert(kv.m_key, kv.m_value); + expr_ref g(m); + rep(term, g); + ptr_vector elems; + flatten_seq(g, elems); + ok = word_in_re(elems, R); + } + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " solve=" << s(got) << " witness-verified=" << (ok ? "yes" : "no") << "\n"; + } + + // decide a conjunction of memberships jointly (shared variables constrained together). + void check_and(char const* name, vector> const& mems, lbool expected) { + obj_map nove; + lbool got = m_mon.solve_and(mems, nove, nullptr); + bool ok = (got == expected); + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") << name + << " got=" << s(got) << " expected=" << s(expected) << "\n"; + } + +public: + seq_monadic_test() : m_reg(m), m_rw(m), m_mon(m_rw), u(m), m_str(m), m_re(m) { + m_str = u.str.mk_string_sort(); + m_re = re().mk_re(m_str); + } + + void run() { + expr_ref x = var("x"); + expr_ref a = word("a"); + expr_ref b = word("b"); + expr_ref ab = cat(a, b); + expr_ref sig = dotstar(); // Sigma* + expr_ref saas = cat(sig, cat(cat(a, a), sig)); // Sigma* a a Sigma* + expr_ref sbbs = cat(sig, cat(cat(b, b), sig)); // Sigma* b b Sigma* + + std::cout << "=== seq_monadic: single-variable membership (x.a.x in R) ===\n"; + + // sanity + check("(a|b)* x.a.x", xwx(x, "a"), star(alt(a, b)), l_true); + check("b* x.a.x", xwx(x, "a"), star(b), l_false); + check("Sig*aaSig* x.a.x", xwx(x, "a"), saas, l_true); + check("x in (a|b)* ", x, star(alt(a, b)), l_true); + check("x in b* (x=aa) ", xwx(x, "a"), star(b), l_false); + + // ALT = (a|b)* & ~(Sig*aaSig*) & ~(Sig*bbSig*) (strictly alternating) + expr_ref altre = inter(star(alt(a, b)), inter(comp(saas), comp(sbbs))); + check("ALT x.a.x", xwx(x, "a"), altre, l_true); + + // R*.S complement family + check("~(a*.b) x.a.x", xwx(x, "a"), comp(cat(star(a), b)), l_true); + + // L3-02 ~((ab)*.~((ab)*)) -> unsat (odd length) + check("L3-02 x.a.x", xwx(x, "a"), + comp(cat(star(ab), comp(star(ab)))), l_false); + + // L3-03 ~(a*.~(b*.~((ab)*))) -> sat + check("L3-03 x.a.x", xwx(x, "a"), + comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))), l_true); + + std::cout << "=== seq_monadic: multi-variable ===\n"; + expr_ref y = var("y"); + check("(a|b)* x.a.y", xay(x, y), star(alt(a, b)), l_true); + check("b* x.a.y", xay(x, y), star(b), l_false); + check("L3-02 x.a.y", xay(x, y), comp(cat(star(ab), comp(star(ab)))), l_true); + check("L3-03 x.a.y", xay(x, y), + comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))), l_true); + check("empty ~Sig* x.y.x", xyx(x, y), comp(dotstar()), l_false); + check("Sig* x.y.x", xyx(x, y), dotstar(), l_true); + check("(a|b)* x.y.x", xyx(x, y), star(alt(a, b)), l_true); + + std::cout << "=== seq_monadic: per-variable constraints ===\n"; + expr_ref digitp = cat(rng('0', '9'), star(rng('0', '9'))); // [0-9]+ + obj_map ve; + ve.insert(y, digitp); + // y must be in the (a|b)* tail AND in [0-9]+ -> empty -> unsat + check_extra("(a|b)* & y in[0-9]+ x.a.y", xay(x, y), star(alt(a, b)), ve, l_false); + // y any digits, x/'a' anything -> sat + check_extra("Sig* & y in[0-9]+ x.a.y", xay(x, y), dotstar(), ve, l_true); + + // Bounded loop (re.loop) with repeated variable -- exercises live_states on a + // counted automaton (t04-exact benchmark family). Regression for a + // reference-invalidation bug in live_states (succ[i].push_back(intern(t))). + std::cout << "=== seq_monadic: bounded loop (t04-exact family) ===\n"; + expr_ref clsr = rng('0', '9'); // [0-9] + expr_ref digitS = star(clsr); // [0-9]* + expr_ref loop22 = loop(clsr, 2, 2); // [0-9]{2} + check("[0-9]{2} x ", x, loop22, l_true); // x = "00" + check("[0-9]{2} x.a.x", xwx(x, "a"), loop22, l_false); // 'a' not a digit + obj_map ve2; ve2.insert(x, digitp); ve2.insert(y, digitS); + // x.y.x in [0-9]{2}, x in [0-9]+, y in [0-9]* -> sat (x="0", y="") + check_extra("[0-9]{2} & x[0-9]+ y[0-9]* x.y.x", xyx(x, y), loop22, ve2, l_true); + obj_map ve3; ve3.insert(x, digitp); + check_extra("[0-9]{2} & x[0-9]+ x.y.x", xyx(x, y), loop22, ve3, l_true); + obj_map ve4; ve4.insert(x, digitp); + // x.y.x in [0-9]{3}, x in [0-9]+ -> sat (x=1 digit, y=1 digit) + check_extra("[0-9]{3} & x[0-9]+ x.y.x", xyx(x, y), loop(clsr, 3, 3), ve4, l_true); + + // ---- witness extraction: a produced witness must be a concrete SEQUENCE of + // ---- elements that actually satisfies the membership (not a predicate). + std::cout << "=== seq_monadic: witness extraction (char) ===\n"; + obj_map nove; + check_witness("(a|b)* x.a.x", xwx(x, "a"), star(alt(a, b)), nove); + check_witness("Sig*aaSig* x.a.x", xwx(x, "a"), saas, nove); // forces nonempty x + check_witness("~(a*.b) x.a.x", xwx(x, "a"), comp(cat(star(a), b)), nove); + check_witness("L3-03 x.a.x", xwx(x, "a"), + comp(cat(star(a), comp(cat(star(b), comp(star(ab)))))), nove); + check_witness("(a|b)* x.a.y", xay(x, y), star(alt(a, b)), nove); + check_witness("Sig* x.y.x", xyx(x, y), dotstar(), nove); + check_witness("Sig* & y[0-9]+ x.a.y", xay(x, y), dotstar(), ve); // ve: y in [0-9]+ + check_witness("[0-9]{2}&x[0-9]+ y[0-9]* x.y.x", xyx(x, y), loop22, ve2); + + // ---- generic element sort: sequences of Int exercise the non-character guard + // ---- algebra (candidate-basis emptiness + witness), not seq::range_predicate. + std::cout << "=== seq_monadic: generic element sort (Seq Int) ===\n"; + arith_util ar(m); + sort_ref intS(ar.mk_int(), m); + sort_ref seqI(u.str.mk_seq(intS), m); + sort_ref reI(u.re.mk_re(seqI), m); + expr_ref i1(ar.mk_numeral(rational(1), true), m); + expr_ref i2(ar.mk_numeral(rational(2), true), m); + expr_ref one_seq(u.str.mk_unit(i1), m); // [1] : (Seq Int) + expr_ref re1(re().mk_to_re(u.str.mk_unit(i1)), m); // matches [1] + expr_ref re2(re().mk_to_re(u.str.mk_unit(i2)), m); // matches [2] + expr_ref re12s(star(alt(re1, re2)), m); // ([1]|[2])* + expr_ref re2s(star(re2), m); // [2]* + expr_ref xi(m.mk_const("xi", seqI), m); + expr_ref yi(m.mk_const("yi", seqI), m); + expr_ref xi1xi(sconcat(xi, sconcat(one_seq, xi)), m); // xi.[1].xi + expr_ref xiyi(sconcat(xi, sconcat(one_seq, yi)), m); // xi.[1].yi + obj_map nove2; + check("([1]|[2])* xi.[1].xi", xi1xi, re12s, l_true); + check("[2]* xi.[1].xi", xi1xi, re2s, l_false); // the middle [1] is not in [2]* + check("([1]|[2])* xi ", xi, re12s, l_true); + check("([1]|[2])* xi.[1].yi", xiyi, re12s, l_true); + check_witness("([1]|[2])* xi.[1].xi", xi1xi, re12s, nove2); + check_witness("([1]|[2])* xi ", xi, re12s, nove2); + check_witness("([1]|[2])* xi.[1].yi", xiyi, re12s, nove2); + // per-variable extra constraint over (Seq Int): yi must also be in [2]* + obj_map veI; veI.insert(yi, re2s.get()); + check_extra("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI, l_true); + check_witness("([1]|[2])* & yi[2]* xi.[1].yi", xiyi, re12s, veI); + + // ---- conjunction of memberships (solve_and): a variable shared across memberships + // ---- is constrained jointly. These are cases that are individually SAT but + // ---- jointly UNSAT -- exactly what independent per-membership solving gets wrong. + std::cout << "=== seq_monadic: conjunction of memberships (solve_and) ===\n"; + expr_ref aaS(star(cat(a, a)), m); // (aa)* : even number of a's + expr_ref a_aaS(cat(a, star(cat(a, a))), m); // a(aa)* : odd number of a's + expr_ref abS(star(ab), m); // (ab)* + expr_ref sig2(dotstar(), m); // Sigma* + // x in (aa)* /\ x in a(aa)* : even-and-odd length of a's -> unsat (each alone sat) + vector> mUnsat1; + mUnsat1.push_back(std::make_pair((expr*)x.get(), (expr*)aaS.get())); + mUnsat1.push_back(std::make_pair((expr*)x.get(), (expr*)a_aaS.get())); + check_and("x in (aa)* & x in a(aa)*", mUnsat1, l_false); + // compound terms sharing x: x.a in (aa)* (x odd) /\ x.aa in (aa)* (x even) -> unsat + expr_ref tXa(sconcat(x, sword("a")), m); + expr_ref tXaa(sconcat(x, sword("aa")), m); + vector> mUnsat2; + mUnsat2.push_back(std::make_pair((expr*)tXa.get(), (expr*)aaS.get())); + mUnsat2.push_back(std::make_pair((expr*)tXaa.get(), (expr*)aaS.get())); + check_and("x.a in (aa)* & x.aa in (aa)*", mUnsat2, l_false); + // consistent conjunction: x in (ab)* /\ x in Sigma* -> sat (x=eps or ab) + vector> mSat; + mSat.push_back(std::make_pair((expr*)x.get(), (expr*)abS.get())); + mSat.push_back(std::make_pair((expr*)x.get(), (expr*)sig2.get())); + check_and("x in (ab)* & x in Sigma*", mSat, l_true); + // two variables, two memberships: x.a.y in (a|b)* /\ y.b.x in (a|b)* -> sat + expr_ref tXaY(xay(x, y), m); + expr_ref tYbX(sconcat(y, sconcat(sword("b"), x)), m); + expr_ref abStar(star(alt(a, b)), m); + vector> mSat2; + mSat2.push_back(std::make_pair((expr*)tXaY.get(), (expr*)abStar.get())); + mSat2.push_back(std::make_pair((expr*)tYbX.get(), (expr*)abStar.get())); + check_and("x.a.y & y.b.x in (a|b)*", mSat2, l_true); + + std::cout << "=== seq_monadic: " << (m_fail == 0 ? "ALL PASS" : "FAILURES") << " (" + << m_fail << " fail) ===\n"; + ENSURE(m_fail == 0); + } +}; + +} + +void tst_seq_monadic() { + seq_monadic_test t; + t.run(); +}