diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 6e966e4618..95fd2e5f19 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -24,6 +24,10 @@ TODOs: - create a validation harness: expose certificates for correctness that can be checked. - extend with lower and upper bound constraints - consider using expr_ref as alternative to pinned expressions + - change type of atom to use expr_ref and avoid pin. svector -> vector. +- revisit parse_term and "the_var" condition. A sequence of units should be allowed. +- support units of non-values (element variables). + Model construction would assign values to the elements. - encapsulate within general interface: create: undo_trail x dependency_manager x ast_manager -> regex_membership add_constraint : expr* x expr* x dependency* -> void @@ -422,6 +426,7 @@ lbool seq_monadic::decide_dnf(vector const& dnf) { void seq_monadic::add(expr* term, expr* regex, u_dependency* d) { m_memberships.push_back({ expr_ref(term, m), expr_ref(regex, m), d }); + m_undo_trail.push(push_back_vector(m_memberships)); } lbool seq_monadic::decide(vector> const& memberships) { @@ -493,10 +498,8 @@ void seq_monadic::minimize_core(vector> memberships; - memberships.swap(m_memberships); // consume the asserted memberships - lbool r = decide(memberships); + lbool r = decide(m_memberships); if (r == l_false) - minimize_core(memberships); + minimize_core(m_memberships); return r; } diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index 8410554993..610c6687c3 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -58,6 +58,7 @@ Author: #include "util/lbool.h" #include "util/obj_hashtable.h" #include "util/dependency.h" +#include "util/trail.h" #include #include @@ -73,6 +74,7 @@ private: seq_rewriter& m_rw; th_rewriter m_thrw; // normalizes constant-element derivatives (folds // ground guards so dead states become re.empty) + trail_stack& m_undo_trail; transition_mode m_mode; sort* m_seq_sort = nullptr; // sequence sort of the regex under analysis sort* m_elem_sort = nullptr; // element sort of that sequence sort @@ -153,8 +155,10 @@ private: void minimize_core(vector> const& memberships); public: - seq_monadic(seq_rewriter& rw, transition_mode mode = transition_mode::light_antimirov) : - m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_mode(mode), m_pin(rw.m()) {} + seq_monadic(seq_rewriter& rw, trail_stack& undo_trail, + transition_mode mode = transition_mode::light_antimirov) : + m(rw.m()), m_rw(rw), m_thrw(rw.m()), m_undo_trail(undo_trail), + m_mode(mode), m_pin(rw.m()) {} ~seq_monadic() { reset_cofactor_cache(); } @@ -181,7 +185,7 @@ 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 accumulate until check() consumes them. + // Memberships remain asserted until the constructor-provided trail is popped. void add(expr* term, expr* regex, u_dependency* d); // Decide the CONJUNCTION of all memberships asserted via add() jointly: a variable @@ -190,7 +194,7 @@ public: // 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 as extra memberships (v in R'). - // Consumes the asserted memberships. l_true = sat (empty conjunction is sat), + // Leaves the asserted memberships unchanged. l_true = sat (empty conjunction is sat), // l_false = unsat, l_undef = gave up. On l_false, core() holds the dependencies // of a minimal unsatisfiable subset. lbool check(); diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index bf970499d5..612a95dc7e 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -37,6 +37,7 @@ class seq_monadic_test { ast_manager m; plugin_registrar m_reg; seq_rewriter m_rw; + trail_stack m_trail; seq_monadic m_mon; seq_util u; sort_ref m_str; // String sort @@ -141,9 +142,11 @@ class seq_monadic_test { void check_extra(char const* name, expr* term, expr* R, obj_map const& ve, lbool expected) { + m_trail.push_scope(); add_extra(term, R, ve); m_mon.set_gen_model(false); // this check does not use the model lbool got = m_mon.check(); + m_trail.pop_scope(1); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -179,6 +182,7 @@ 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) { + m_trail.push_scope(); add_extra(term, R, ve); m_mon.set_gen_model(true); // this check verifies the extracted model lbool got = m_mon.check(); @@ -193,6 +197,7 @@ class seq_monadic_test { flatten_seq(g, elems); ok = word_in_re(elems, R); } + m_trail.pop_scope(1); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name << " solve=" << s(got) << " witness-verified=" << (ok ? "yes" : "no") << "\n"; @@ -200,10 +205,12 @@ 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) { + m_trail.push_scope(); for (auto const& [t, r] : mems) m_mon.add(t, r, nullptr); m_mon.set_gen_model(false); // this check does not use the model lbool got = m_mon.check(); + m_trail.pop_scope(1); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -230,20 +237,24 @@ class seq_monadic_test { // minimization disabled: the core is every asserted membership's dependency. m_mon.set_min_core(false); + m_trail.push_scope(); for (unsigned i = 0; i < mems.size(); ++i) m_mon.add(mems[i].first, mems[i].second, m_dm.mk_leaf(i)); lbool got0 = m_mon.check(); core_ids(got_ids); bool ok0 = (got0 == l_false) && (got_ids == all_ids); + m_trail.pop_scope(1); // minimization enabled: the core drops constraints irrelevant to the conflict. m_mon.set_min_core(true); + m_trail.push_scope(); for (unsigned i = 0; i < mems.size(); ++i) m_mon.add(mems[i].first, mems[i].second, m_dm.mk_leaf(i)); lbool got1 = m_mon.check(); std::set min_ids; core_ids(min_ids); bool ok1 = (got1 == l_false) && (min_ids == expected_core); + m_trail.pop_scope(1); m_mon.set_min_core(false); // restore the harness default bool ok = ok0 && ok1; @@ -256,7 +267,7 @@ class seq_monadic_test { public: seq_monadic_test(seq_monadic::transition_mode mode) : - m_reg(m), m_rw(m), m_mon(m_rw, mode), u(m), m_str(m), m_re(m), m_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) { m_str = u.str.mk_string_sort(); m_re = re().mk_re(m_str); m_mon.set_min_core(false); // tests use unminimized cores by default @@ -415,6 +426,25 @@ public: 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: assertion trail ===\n"; + m_mon.set_gen_model(false); + m_trail.push_scope(); + m_mon.add(x, aaS, nullptr); + lbool before = m_mon.check(); + m_trail.push_scope(); + m_mon.add(x, a_aaS, nullptr); + lbool with_conflict = m_mon.check(); + lbool repeated = m_mon.check(); + m_trail.pop_scope(1); + lbool after_pop = m_mon.check(); + m_trail.pop_scope(1); + lbool empty = m_mon.check(); + bool trail_ok = before == l_true && with_conflict == l_false && + repeated == l_false && after_pop == l_true && empty == l_true; + if (!trail_ok) ++m_fail; + std::cout << (trail_ok ? " OK " : " FAIL ") + << "check preserves assertions and pop removes them\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"; diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp index 3481f2935b..804ce15d1b 100644 --- a/src/test/seq_monadic_bench.cpp +++ b/src/test/seq_monadic_bench.cpp @@ -90,7 +90,8 @@ lbool run_file( ast_manager& m = ctx.m(); seq_util u(m); seq_rewriter rw(m); - seq_monadic mon(rw, mode); + trail_stack undo_trail; + seq_monadic mon(rw, undo_trail, mode); obj_map var_re; obj_map term_re;