add undo trail

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<atom> -> vector<atom>.
+- 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<disjunct> 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<std::tuple<expr_ref, expr_ref, u_dependency*>> const& memberships) {
@@ -493,10 +498,8 @@ void seq_monadic::minimize_core(vector<std::tuple<expr_ref, expr_ref, u_dependen
 
 lbool seq_monadic::check() {
     m_core.reset();
-    vector<std::tuple<expr_ref, expr_ref, u_dependency*>> 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;
 }

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 <utility>
 #include <tuple>
 
@@ -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<std::tuple<expr_ref, expr_ref, u_dependency*>> 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();

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<expr, expr*> 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<expr, expr*> 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<std::pair<expr*, expr*>> 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<unsigned> 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";

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<expr, expr*> var_re;
     obj_map<expr, expr*> term_re;