diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 2dc028e97f..c934b38c68 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -19,7 +19,6 @@ Abstract: yields the concrete element used to build a witness sequence. TODOs: -- track unsat cores and expose them as explain functionality - if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead) - create a validation harness: expose certificates for correctness that can be checked. - extend with lower and upper bound constraints @@ -419,12 +418,12 @@ lbool seq_monadic::decide_dnf(vector const& dnf) { return any_undef ? l_undef : l_false; } -void seq_monadic::add(expr* term, expr* regex, u_dependency* d) { +void seq_monadic::add(expr* term, expr* regex, void* d) { m_memberships.push_back({ expr_ref(term, m), expr_ref(regex, m), d }); m_undo_trail.push(push_back_vector(m_memberships)); } -void seq_monadic::add_lo(expr* term, unsigned lo, u_dependency* d) { +void seq_monadic::add_lo(expr* term, unsigned lo, void* d) { if (lo == 0) return; sort* re_sort = re().mk_re(term->get_sort()); @@ -435,21 +434,21 @@ void seq_monadic::add_lo(expr* term, unsigned lo, u_dependency* d) { add(term, regex, d); } -void seq_monadic::add_hi(expr* term, unsigned hi, u_dependency* d) { +void seq_monadic::add_hi(expr* term, unsigned hi, void* d) { sort* re_sort = re().mk_re(term->get_sort()); expr_ref all_char(re().mk_full_char(re_sort), m); expr_ref regex(re().mk_loop_proper(all_char, 0, hi), m); add(term, regex, d); } -void seq_monadic::add_len(expr* term, unsigned len, u_dependency* d) { +void seq_monadic::add_len(expr* term, unsigned len, void* d) { sort* re_sort = re().mk_re(term->get_sort()); expr_ref all_char(re().mk_full_char(re_sort), m); expr_ref regex(re().mk_loop_proper(all_char, len, len), m); add(term, regex, d); } -lbool seq_monadic::decide(vector> const& memberships) { +lbool seq_monadic::decide(membership_vec const& memberships) { m_model.reset(); if (memberships.empty()) return l_true; // empty conjunction is vacuously true @@ -487,7 +486,7 @@ lbool seq_monadic::decide(vector> return decide_dnf(combined); } -void seq_monadic::minimize_core(vector> const& memberships) { +void seq_monadic::minimize_core(membership_vec const& memberships) { m_core.reset(); if (!m_min_core) { // No minimization: the core is simply every asserted membership's dependency. @@ -499,13 +498,10 @@ void seq_monadic::minimize_core(vector> keep(memberships); - unsigned i = 0; - while (i < keep.size()) { - vector> trial; - for (unsigned j = 0; j < keep.size(); ++j) - if (j != i) - trial.push_back(keep[j]); + membership_vec keep(memberships); + for (unsigned i = 0; i < keep.size(); ) { + membership_vec trial(keep); + trial.erase(trial.begin() + i); if (decide(trial) == l_false) keep.swap(trial); // membership i is not needed for unsat else diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 4b0855de2a..2f56c6a9e1 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -85,8 +85,9 @@ private: bool m_min_core = true; // whether check() minimizes the unsat core (else: all deps) obj_map m_model; // last extracted model (var -> witness); see get_model() obj_map m_cofactor_cache; // memoizes derivative_cofactors per regex - vector> m_memberships; // asserted (term in regex, dep) for check() - ptr_vector m_core; // dependencies of an unsat subset, filled by check() on l_false + using membership_vec = vector>; + membership_vec m_memberships; // asserted (term in regex, dep) for check() + ptr_vector m_core; // dependencies of an unsat subset, filled by check() on l_false seq_util& u() const { return m_rw.u(); } seq_util::rex& re() const { return m_rw.u().re; } @@ -155,11 +156,11 @@ private: // Decide a CONJUNCTION of memberships jointly (the core algorithm behind check()): // multiplies the per-membership DNFs and decides emptiness. Does not touch // m_memberships or m_core; fills m_model on l_true when model generation is enabled. - lbool decide(vector> const& memberships); + lbool decide(membership_vec const& memberships); // Given an unsatisfiable membership set, extract a minimal unsatisfiable subset by // deletion and collect the (non-null) dependencies of its members into m_core. - void minimize_core(vector> const& memberships); + void minimize_core(membership_vec const& memberships); public: seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, @@ -193,16 +194,16 @@ public: // Assert a membership (term in regex) to be decided jointly by the next check(). // `d` carries the dependency used for unsat-core tracking and may be nullptr. // Memberships remain asserted until the constructor-provided trail is popped. - void add(expr* term, expr* regex, u_dependency* d); + void add(expr* term, expr* regex, void* d); // Assert that `term` has at least `lo` elements. A zero lower bound is a no-op. - void add_lo(expr* term, unsigned lo, u_dependency* d); + void add_lo(expr* term, unsigned lo, void* d); // Assert that `term` has at most `hi` elements. - void add_hi(expr* term, unsigned hi, u_dependency* d); + void add_hi(expr* term, unsigned hi, void* d); // Assert that `term` has exactly `len` elements. - void add_len(expr* term, unsigned len, u_dependency* d); + void add_len(expr* term, unsigned len, void* d); // Decide the CONJUNCTION of all memberships asserted via add() jointly: a variable // shared across memberships is constrained consistently (the DNFs are multiplied and @@ -217,5 +218,5 @@ public: // Dependencies of a minimal unsatisfiable subset from the last check() that returned // l_false (nullptr dependencies are omitted). Empty otherwise. - ptr_vector const& core() const { return m_core; } + ptr_vector const& core() const { return m_core; } }; diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 9753e42072..5f65fa6ce2 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -141,6 +141,7 @@ def_module_params(module_name='smt', ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'), ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'), ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'), + ('seq.regex_monadic', BOOL, False, 'use the monadic regular-expression end-game solver'), ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'), ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), diff --git a/src/params/theory_seq_params.cpp b/src/params/theory_seq_params.cpp index 54bf691620..789b0c00ed 100644 --- a/src/params/theory_seq_params.cpp +++ b/src/params/theory_seq_params.cpp @@ -21,6 +21,7 @@ void theory_seq_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); m_split_w_len = p.seq_split_w_len(); m_seq_validate = p.seq_validate(); + m_seq_regex_monadic = p.seq_regex_monadic(); m_seq_max_unfolding = p.seq_max_unfolding(); m_seq_min_unfolding = p.seq_min_unfolding(); } diff --git a/src/params/theory_seq_params.h b/src/params/theory_seq_params.h index f964088eb8..287cccfacf 100644 --- a/src/params/theory_seq_params.h +++ b/src/params/theory_seq_params.h @@ -24,6 +24,7 @@ struct theory_seq_params { */ bool m_split_w_len = false; bool m_seq_validate = false; + bool m_seq_regex_monadic = false; unsigned m_seq_max_unfolding = UINT_MAX/4; unsigned m_seq_min_unfolding = 1; @@ -33,4 +34,3 @@ struct theory_seq_params { void updt_params(params_ref const & p); }; - diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 8d3913cde2..0109279443 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -30,6 +30,7 @@ namespace smt { th(th), ctx(th.get_context()), m(th.get_manager()), + m_monadic(seq_rw(), ctx.get_trail_stack()), m_state_to_expr(m), m_state_graph(state_graph::state_pp(this, pp_state)) { } @@ -41,6 +42,104 @@ namespace smt { arith_util& seq_regex::a() { return th.m_autil; } void seq_regex::rewrite(expr_ref& e) { th.m_rewrite(e); } + void seq_regex::add_monadic_membership(literal lit, expr* s, expr* r) { + for (auto const& membership : m_monadic_memberships) + if (membership.m_lit == lit) + return; + m_monadic_memberships.push_back(monadic_membership(m, lit, s, r)); + ctx.push_trail(push_back_vector(m_monadic_memberships)); + theory_seq::dependency* dep = th.m_dm.mk_leaf(theory_seq::assumption(lit)); + m_monadic.add(s, r, dep); + ctx.push_trail(value_trail(m_monadic_generation)); + ++m_monadic_generation; + TRACE(seq_regex, tout << "monadic add " << lit << ": " + << mk_pp(s, m) << " in " << mk_pp(r, m) << "\n";); + } + + void seq_regex::propagate_accept_legacy(literal lit, expr* s, expr* r) { + expr_ref regex(r, m); + if (!m.is_value(s)) { + expr_ref s_approx = get_overapprox_regex(s); + if (!re().is_full_seq(s_approx)) { + regex = re().mk_inter(regex, s_approx); + TRACE(seq_regex, tout + << "get_overapprox_regex(" << mk_pp(s, m) + << ") = " << mk_pp(s_approx, m) << std::endl;); + STRACE(seq_regex_brief, tout + << "overapprox=" << state_str(regex) << " ";); + } + } + + expr_ref zero(a().mk_int(0), m); + expr_ref acc(sk().mk_accept(s, zero, regex), m); + literal acc_lit = th.mk_literal(acc); + + TRACE(seq, tout << "propagate " << acc << "\n";); + th.add_axiom(~lit, acc_lit); + } + + void seq_regex::enable_legacy_fallback() { + if (m_monadic_fallback_generation == m_monadic_generation) + return; + for (auto const& membership : m_monadic_memberships) + propagate_accept_legacy(membership.m_lit, membership.m_s, membership.m_re); + ctx.push_trail(value_trail(m_monadic_fallback_generation)); + m_monadic_fallback_generation = m_monadic_generation; + ++th.m_stats.m_regex_monadic_fallbacks; + } + + final_check_status seq_regex::final_check() { + if (!th.use_monadic_regex() || m_monadic_memberships.empty()) + return FC_DONE; + if (m_monadic_fallback_generation == m_monadic_generation) + return FC_DONE; + + if (m_monadic_assumption_generation == m_monadic_generation) { + for (auto const& assumption : m_monadic_assumptions) { + if (assumption.m_generation != m_monadic_generation) + continue; + if (assumption.m_var->get_root() != assumption.m_witness->get_root()) { + enable_legacy_fallback(); + return FC_CONTINUE; + } + } + return FC_DONE; + } + + ++th.m_stats.m_regex_monadic_checks; + lbool result = m_monadic.check(); + if (result == l_false) { + ++th.m_stats.m_regex_monadic_unsat; + theory_seq::dependency* dep = nullptr; + for (void* core_dep : m_monadic.core()) + dep = th.m_dm.mk_join(dep, static_cast(core_dep)); + th.set_conflict(dep); + return FC_CONTINUE; + } + if (result == l_undef) { + ++th.m_stats.m_regex_monadic_undef; + enable_legacy_fallback(); + return FC_CONTINUE; + } + + ++th.m_stats.m_regex_monadic_sat; + ctx.push_trail(value_trail(m_monadic_assumption_generation)); + m_monadic_assumption_generation = m_monadic_generation; + for (auto const& [var, witness] : m_monadic.get_model()) { + enode* var_node = th.ensure_enode(var); + enode* witness_node = th.ensure_enode(witness); + if (var_node->get_root() == witness_node->get_root()) + continue; + ctx.assume_eq(var_node, witness_node); + m_monadic_assumptions.push_back({ m_monadic_generation, var_node, witness_node }); + ctx.push_trail(push_back_vector(m_monadic_assumptions)); + ++th.m_stats.m_regex_monadic_assumptions; + TRACE(seq_regex, tout << "monadic assume " + << mk_pp(var, m) << " = " << mk_pp(witness, m) << "\n";); + } + return FC_CONTINUE; + } + /** * is_string_equality holds of str.in_re s R, * @@ -128,34 +227,10 @@ namespace smt { return; } - // Convert a non-ground sequence into an additional regex and - // strengthen the original regex constraint into an intersection - // for example: - // (x ++ "a" ++ y) in b* - // is coverted to - // (x ++ "a" ++ y) in intersect((.* ++ "a" ++ .*), b*) - expr_ref _r_temp_owner(m); - if (!m.is_value(s)) { - expr_ref s_approx = get_overapprox_regex(s); - if (!re().is_full_seq(s_approx)) { - r = re().mk_inter(r, s_approx); - _r_temp_owner = r; - TRACE(seq_regex, tout - << "get_overapprox_regex(" << mk_pp(s, m) - << ") = " << mk_pp(s_approx, m) << std::endl;); - STRACE(seq_regex_brief, tout - << "overapprox=" << state_str(r) << " ";); - } - } - - expr_ref zero(a().mk_int(0), m); - expr_ref acc(sk().mk_accept(s, zero, r), m); - literal acc_lit = th.mk_literal(acc); - - TRACE(seq, tout << "propagate " << acc << "\n";); - - //th.propagate_lit(nullptr, 1, &lit, acc_lit); - th.add_axiom(~lit, acc_lit); + if (th.use_monadic_regex()) + add_monadic_membership(lit, s, r); + else + propagate_accept_legacy(lit, s, r); } /** diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index bba4d30eaa..8c4f3617f2 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -19,6 +19,7 @@ Author: #include "util/scoped_vector.h" #include "util/state_graph.h" #include "ast/seq_decl_plugin.h" +#include "ast/rewriter/seq_monadic.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_skolem.h" #include "smt/smt_context.h" @@ -108,6 +109,28 @@ namespace smt { ast_manager& m; vector m_s_in_re; + struct monadic_membership { + literal m_lit; + expr_ref m_s; + expr_ref m_re; + + monadic_membership(ast_manager& m, literal lit, expr* s, expr* re) : + m_lit(lit), m_s(s, m), m_re(re, m) {} + }; + + struct monadic_assumption { + unsigned m_generation; + enode* m_var; + enode* m_witness; + }; + + seq_monadic m_monadic; + vector m_monadic_memberships; + svector m_monadic_assumptions; + unsigned m_monadic_generation = 0; + unsigned m_monadic_assumption_generation = UINT_MAX; + unsigned m_monadic_fallback_generation = UINT_MAX; + /* state_graph for dead state detection, and associated methods */ @@ -188,6 +211,9 @@ namespace smt { } bool block_if_empty(expr* r, literal lit); + void add_monadic_membership(literal lit, expr* s, expr* r); + void propagate_accept_legacy(literal lit, expr* s, expr* r); + void enable_legacy_fallback(); public: @@ -197,6 +223,7 @@ namespace smt { void pop_scope(unsigned num_scopes) {} bool can_propagate() const { return false; } bool propagate() const { return false; } + final_check_status final_check(); void propagate_in_re(literal lit); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 27b43a6f16..559a8fb2b9 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -428,6 +428,16 @@ final_check_status theory_seq::final_check_eh(unsigned level) { TRACEFIN("solve_recfun"); return FC_CONTINUE; } + switch (m_regex.final_check()) { + case FC_CONTINUE: + TRACEFIN("regex monadic"); + return FC_CONTINUE; + case FC_GIVEUP: + TRACEFIN("regex monadic giveup"); + return FC_GIVEUP; + case FC_DONE: + break; + } if (m_unhandled_expr) { TRACEFIN("give_up"); TRACE(seq, tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";); @@ -1956,6 +1966,12 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq fixed length", m_stats.m_fixed_length); st.update("seq int.to.str", m_stats.m_int_string); st.update("seq str.from_ubv", m_stats.m_ubv_string); + st.update("seq regex monadic checks", m_stats.m_regex_monadic_checks); + st.update("seq regex monadic sat", m_stats.m_regex_monadic_sat); + st.update("seq regex monadic unsat", m_stats.m_regex_monadic_unsat); + st.update("seq regex monadic undef", m_stats.m_regex_monadic_undef); + st.update("seq regex monadic assumptions", m_stats.m_regex_monadic_assumptions); + st.update("seq regex monadic fallbacks", m_stats.m_regex_monadic_fallbacks); } void theory_seq::init_search_eh() { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 50a267d653..d9bede8741 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -319,6 +319,12 @@ namespace smt { unsigned m_propagate_contains; unsigned m_int_string; unsigned m_ubv_string; + unsigned m_regex_monadic_checks; + unsigned m_regex_monadic_sat; + unsigned m_regex_monadic_unsat; + unsigned m_regex_monadic_undef; + unsigned m_regex_monadic_assumptions; + unsigned m_regex_monadic_fallbacks; }; typedef hashtable rational_set; @@ -632,6 +638,7 @@ namespace smt { app* mk_value(expr* a); trail_stack& get_trail_stack() { return m_trail_stack; } + bool use_monadic_regex() const { return get_fparams().m_seq_regex_monadic; } void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {} void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { } void unmerge_eh(theory_var v1, theory_var v2) {} @@ -644,4 +651,3 @@ namespace smt { }; } - diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 36457cb023..bd8caca1ac 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -24,6 +24,8 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/seq_monadic.h" #include "ast/rewriter/expr_safe_replace.h" +#include "params/smt_params.h" +#include "smt/smt_kernel.h" #include #include @@ -220,8 +222,10 @@ class seq_monadic_test { // collect the core ids after a check() into `ids`. void core_ids(std::set& ids) { ids.clear(); - for (u_dependency* d : m_mon.core()) + for (void* dep : m_mon.core()) { + u_dependency* d = static_cast(dep); ids.insert(d->leaf_value()); + } } // Assert each membership with a distinct leaf dependency (id = its index) and expect @@ -265,6 +269,24 @@ class seq_monadic_test { std::cout << "} full=" << (ok0 ? "yes" : "no") << "\n"; } + lbool smt_check(expr_ref_vector const& assertions, bool enable_monadic = true) { + smt_params params; + params.m_seq_regex_monadic = enable_monadic; + smt::kernel solver(m, params); + for (expr* assertion : assertions) + solver.assert_expr(assertion); + return solver.check(); + } + + void check_smt(char const* name, expr_ref_vector const& assertions, lbool expected, + bool enable_monadic = true) { + lbool got = smt_check(assertions, enable_monadic); + 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(seq_monadic::transition_mode mode) : m_reg(m), m_rw(m), m_mon(m_rw, m_trail, mode), u(m), m_str(m), m_re(m), m_mode(mode) { @@ -489,6 +511,70 @@ public: std::cout << (zero_lo_ok ? " OK " : " FAIL ") << "|x| >= 0 is a no-op\n"; + std::cout << "=== seq_monadic: SMT regex end-game ===\n"; + { + expr_ref_vector assertions(m); + assertions.push_back(re().mk_in_re(x, star(alt(a, b)))); + check_smt("enabled SAT membership", assertions, l_true); + check_smt("disabled legacy membership", assertions, l_true, false); + } + { + expr_ref_vector assertions(m); + expr_ref a_star(star(a), m); + assertions.push_back(re().mk_in_re(x, a_star)); + assertions.push_back(re().mk_in_re(x, comp(a_star))); + check_smt("enabled joint UNSAT memberships", assertions, l_false); + } + { + expr_ref_vector assertions(m); + assertions.push_back(m.mk_not(re().mk_in_re(x, star(a)))); + assertions.push_back(re().mk_in_re(x, star(a))); + check_smt("enabled negative membership", assertions, l_false); + } + { + expr_ref_vector assertions(m); + assertions.push_back(m.mk_eq(x, sword("aa"))); + assertions.push_back(re().mk_in_re(x, expr_ref(re().mk_plus(a), m))); + check_smt("rejected witness uses legacy fallback", assertions, l_true); + } + { + expr_ref_vector assertions(m); + assertions.push_back(m.mk_eq(x, y)); + assertions.push_back(re().mk_in_re(x, star(a))); + assertions.push_back(re().mk_in_re(y, expr_ref(re().mk_plus(b), m))); + check_smt("aliased variables use legacy fallback", assertions, l_false); + } + { + arith_util ar2(m); + sort_ref int_sort(ar2.mk_int(), m); + sort_ref seq_sort(u.str.mk_seq(int_sort), m); + sort_ref regex_sort(re().mk_re(seq_sort), m); + expr_ref seq_var(m.mk_const("seq_var", seq_sort), m); + expr_ref elem_var(m.mk_const("elem_var", int_sort), m); + expr_ref symbolic_unit(u.str.mk_unit(elem_var), m); + expr_ref term(u.str.mk_concat(seq_var, symbolic_unit), m); + expr_ref_vector assertions(m); + assertions.push_back(re().mk_in_re(term, re().mk_full_seq(regex_sort))); + check_smt("unsupported symbolic unit uses fallback", assertions, l_true); + } + { + smt_params params; + params.m_seq_regex_monadic = true; + smt::kernel solver(m, params); + expr_ref a_star(star(a), m); + solver.assert_expr(re().mk_in_re(x, a_star)); + lbool before_push = solver.check(); + solver.push(); + solver.assert_expr(re().mk_in_re(x, comp(a_star))); + lbool in_push = solver.check(); + solver.pop(1); + lbool after_pop = solver.check(); + bool ok = before_push == l_true && in_push == l_false && after_pop == l_true; + if (!ok) ++m_fail; + std::cout << (ok ? " OK " : " FAIL ") + << "SMT membership trail push/pop\n"; + } + // ---- unsat cores: the extracted core must contain only constraints that // ---- participate in the contradiction, not independent ones. std::cout << "=== seq_monadic: unsat cores ===\n";