diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 1bd5297878..18661651e1 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -80,7 +80,7 @@ void seq_monadic::reset_cofactor_cache() { m_cofactor_cache.reset(); } -bool seq_monadic::live_states(expr* R, ptr_vector& out) { +bool seq_monadic::live_states(expr* R, expr_ref_vector& out) { obj_map id; expr_ref_vector states(m); vector> succ; @@ -133,11 +133,11 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w } expr_ref var0(m.mk_var(0, m_elem_sort), m); // the element variable the guards range over - svector start; + ptr_vector start; for (auto const& c : comps) start.push_back(c.state); - auto id_key = [&](svector const& st) { + auto id_key = [&](ptr_vector const& st) { std::vector k; k.reserve(st.size()); for (expr* e : st) k.push_back(e->get_id()); @@ -146,7 +146,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w typedef std::vector key; bool undecided = false; - auto is_accept = [&](svector const& st) -> bool { + auto is_accept = [&](ptr_vector const& st) -> bool { for (unsigned i = 0; i < n; ++i) { if (comps[i].target) { if (st[i] != comps[i].target) return false; @@ -162,7 +162,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w }; std::set visited; - std::vector> work; + 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; @@ -193,7 +193,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w --m_budget; if (!m.inc()) return l_undef; - svector st = work.back(); + ptr_vector st = work.back(); work.pop_back(); if (is_accept(st)) { if (witness_word) @@ -217,7 +217,7 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w // 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; + ptr_vector cur; cur.resize(n); key st_key = id_key(st); bool bail = false; @@ -259,13 +259,8 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w } 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_concat(t)) + return all_of(*to_app(t), [&](expr* arg) { return parse_term(arg, atoms, the_var); }); if (u().str.is_empty(t)) return true; // epsilon: contributes nothing zstring s; @@ -320,7 +315,7 @@ bool seq_monadic::decompose(svector const& atoms, unsigned i, expr* R, return true; } // a variable with a non-empty rest: split over the live states q of R (midpoints) - ptr_vector Q; + expr_ref_vector Q(m); if (!live_states(R, Q)) return false; const unsigned DISJUNCT_CAP = 1u << 13; @@ -362,7 +357,14 @@ void seq_monadic::simplify_dnf(vector& dnf) { } lbool seq_monadic::solve(expr* term, expr* R) { - return solve(term, R, nullptr); + m_pin.reset(); + reset_cofactor_cache(); + 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); } bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector& dnf) { @@ -380,7 +382,8 @@ bool seq_monadic::build_membership_dnf(expr* term, expr* R, vector& dn return decompose(atoms, 0, R, dnf); } -lbool seq_monadic::decide_dnf(vector const& dnf, obj_map* model) { +lbool seq_monadic::decide_dnf(vector const& dnf) { + m_model.reset(); bool any_undef = false; for (disjunct const& D : dnf) { // group components by variable @@ -402,34 +405,22 @@ lbool seq_monadic::decide_dnf(vector const& dnf, obj_map* 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); + lbool ne = product_nonempty(groups[gi], m_gen_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 (m_gen_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) + if (m_gen_model) for (auto const& [k, v] : local) - model->insert(k, v); + m_model.insert(k, v); return l_true; // all variables satisfiable => sat } return any_undef ? l_undef : l_false; } -lbool seq_monadic::solve(expr* term, expr* R, obj_map* model) { - m_pin.reset(); - reset_cofactor_cache(); - 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, model); -} - -lbool seq_monadic::solve_and(vector> const& mems, - obj_map* model) { +lbool seq_monadic::solve_and(vector> const& mems) { if (mems.empty()) return l_undef; m_pin.reset(); @@ -463,5 +454,5 @@ lbool seq_monadic::solve_and(vector> const& mems, if (combined.empty()) return l_false; // no viable disjunct left => unsat } - return decide_dnf(combined, model); + return decide_dnf(combined); } diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index cbe8848ce5..29231f2024 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -77,6 +77,8 @@ private: 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 + bool m_gen_model = true; // whether solve()/solve_and() extract a feasible model + obj_map m_model; // last extracted model (var -> witness); see get_model() obj_map m_cofactor_cache; // memoizes derivative_cofactors per regex seq_util& u() const { return m_rw.u(); } @@ -106,7 +108,7 @@ private: // Live reachable derivative states of R (BFS over cofactor targets + liveness // least-fixpoint). These are the split states q. Returns false on a cap overrun. - bool live_states(expr* R, ptr_vector& out); + bool live_states(expr* R, expr_ref_vector& out); // 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 @@ -132,8 +134,9 @@ private: 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* model); + // group non-empty. On l_true, when model generation is enabled, fills m_model + // (var -> witness). + lbool decide_dnf(vector const& dnf); public: seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : @@ -143,24 +146,27 @@ public: transition_mode mode() const { return m_mode; } + // Enable/disable model generation (default: enabled). When enabled, a successful + // solve()/solve_and() extracts a feasible model retrievable via get_model(). + void set_gen_model(bool b) { m_gen_model = b; } + + // The model extracted by the last successful solve()/solve_and(): 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 solve()/solve_and(). Only valid when model generation is enabled. + obj_map const& get_model() const { return m_model; } + // 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; 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* 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)). // Per-variable extra constraints are expressed here as extra memberships (v in R'). - // model as above. l_true = sat, l_false = unsat, l_undef = gave up. - lbool solve_and(vector> const& mems, - obj_map* model = nullptr); + // l_true = sat, l_false = unsat, l_undef = gave up. + lbool solve_and(vector> const& mems); }; diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 621c40b73d..7bf05bbf98 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -121,6 +121,7 @@ class seq_monadic_test { } void check(char const* name, expr* term, expr* R, lbool expected) { + m_mon.set_gen_model(false); // this check does not use the model lbool got = m_mon.solve(term, R); bool ok = (got == expected); if (!ok) ++m_fail; @@ -141,7 +142,8 @@ class seq_monadic_test { obj_map const& ve, lbool expected) { vector> mems; add_extra(mems, term, R, ve); - lbool got = m_mon.solve_and(mems, nullptr); + m_mon.set_gen_model(false); // this check does not use the model + lbool got = m_mon.solve_and(mems); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -177,10 +179,11 @@ class seq_monadic_test { // 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; vector> mems; add_extra(mems, term, R, ve); - lbool got = m_mon.solve_and(mems, &model); + m_mon.set_gen_model(true); // this check verifies the extracted model + lbool got = m_mon.solve_and(mems); + obj_map const& model = m_mon.get_model(); bool ok = (got == l_true) && !model.empty(); if (ok) { expr_safe_replace rep(m); @@ -198,7 +201,8 @@ class seq_monadic_test { // decide a conjunction of memberships jointly (shared variables constrained together). void check_and(char const* name, vector> const& mems, lbool expected) { - lbool got = m_mon.solve_and(mems, nullptr); + m_mon.set_gen_model(false); // this check does not use the model + lbool got = m_mon.solve_and(mems); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index 071cc5f536..bc343f2557 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -138,9 +138,10 @@ lbool run_file( memberships.push_back(std::make_pair(entry.m_key, entry.m_value)); auto start = std::chrono::high_resolution_clock::now(); + mon.set_gen_model(false); // benchmark only needs the verdict lbool verdict = memberships.empty() ? l_undef - : mon.solve_and(memberships, nullptr); + : mon.solve_and(memberships); solve_ms = std::chrono::duration( std::chrono::high_resolution_clock::now() - start).count(); return verdict;