Remove sgraph dependency from seq_plugin, let sgraph register nodes via on_make callback

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/euf/euf_seq_plugin.cpp

@@ -21,16 +21,14 @@ Author:
 --*/
 
 #include "ast/euf/euf_seq_plugin.h"
-#include "ast/euf/euf_sgraph.h"
 #include "ast/euf/euf_egraph.h"
 #include "ast/ast_pp.h"
 
 namespace euf {
 
-    seq_plugin::seq_plugin(egraph& g, sgraph& sg):
+    seq_plugin::seq_plugin(egraph& g):
         plugin(g),
-        m_seq(g.get_manager()),
+        m_seq(g.get_manager()) {
-        m_sg(sg) {
     }
 
     void seq_plugin::register_node(enode* n) {
@@ -71,9 +69,6 @@ namespace euf {
 
         TRACE(seq, tout << "seq register " << g.bpp(n) << "\n");
 
-        // register in sgraph
-        m_sg.mk(n->get_expr());
-
         if (is_concat(n)) {
             m_concats.push_back(n);
             propagate_assoc(n);
@@ -178,13 +173,34 @@ namespace euf {
         }
     }
 
-    bool seq_plugin::is_nullable(enode* n) {
+    bool seq_plugin::is_nullable(expr* e) {
-        snode* s = m_sg.find(n->get_expr());
+        // compute nullable from expression structure without sgraph dependency
-        if (s)
+        if (m_seq.str.is_empty(e))
-            return s->is_nullable();
-        // empty string is nullable
-        if (is_empty(n))
             return true;
+        if (m_seq.re.is_full_seq(e))
+            return true;
+        if (m_seq.re.is_star(e))
+            return true;
+        if (m_seq.str.is_concat(e)) {
+            SASSERT(to_app(e)->get_num_args() == 2);
+            return is_nullable(to_app(e)->get_arg(0)) && is_nullable(to_app(e)->get_arg(1));
+        }
+        if (m_seq.re.is_union(e)) {
+            SASSERT(to_app(e)->get_num_args() == 2);
+            return is_nullable(to_app(e)->get_arg(0)) || is_nullable(to_app(e)->get_arg(1));
+        }
+        if (m_seq.re.is_intersection(e)) {
+            SASSERT(to_app(e)->get_num_args() == 2);
+            return is_nullable(to_app(e)->get_arg(0)) && is_nullable(to_app(e)->get_arg(1));
+        }
+        if (m_seq.re.is_complement(e)) {
+            SASSERT(to_app(e)->get_num_args() == 1);
+            return !is_nullable(to_app(e)->get_arg(0));
+        }
+        if (m_seq.re.is_to_re(e)) {
+            SASSERT(to_app(e)->get_num_args() == 1);
+            return is_nullable(to_app(e)->get_arg(0));
+        }
         return false;
     }
 
@@ -237,8 +253,6 @@ namespace euf {
     }
 
     std::ostream& seq_plugin::display(std::ostream& out) const {
-        // sgraph contents are displayed by sgraph::display, not here,
-        // since sgraph owns the seq_plugin (not the other way around)
         out << "seq-plugin\n";
         return out;
     }

src/ast/euf/euf_seq_plugin.h

@@ -26,8 +26,9 @@ Abstract:
     -- Nullable absorption: a nullable token adjacent to .*
        is absorbed, u.*.v.w = u.*.w when v is nullable.
 
-    The plugin integrates with euf_egraph for congruence closure
+    The plugin integrates with euf_egraph for congruence closure.
-    and with sgraph for snode-based string representation.
+    Node registration in sgraph is handled by sgraph itself via
+    the egraph's on_make callback, not by the plugin.
 
 Author:
 
@@ -44,7 +45,6 @@ Author:
 namespace euf {
 
     class egraph;
-    class sgraph;
 
     class seq_plugin : public plugin {
 
@@ -53,7 +53,6 @@ namespace euf {
         };
 
         seq_util         m_seq;
-        sgraph&          m_sg;
         svector<undo_kind> m_undo;
 
         // queue of merges and registrations to process
@@ -90,8 +89,9 @@ namespace euf {
         // merging Kleene stars, merging loops, absorbing nullables
         void propagate_simplify(enode* n);
 
-        // check if snode is nullable via sgraph metadata
+        // check if expression is nullable, computed from expression structure
-        bool is_nullable(enode* n);
+        bool is_nullable(expr* e);
+        bool is_nullable(enode* n) { return is_nullable(n->get_expr()); }
 
         // check if two enodes have congruent star bodies
         bool same_star_body(enode* a, enode* b);
@@ -100,7 +100,7 @@ namespace euf {
         bool same_loop_body(enode* a, enode* b, unsigned& lo1, unsigned& hi1, unsigned& lo2, unsigned& hi2);
 
     public:
-        seq_plugin(egraph& g, sgraph& sg);
+        seq_plugin(egraph& g);
 
         theory_id get_id() const override { return m_seq.get_family_id(); }
 
@@ -117,8 +117,5 @@ namespace euf {
         std::ostream& display(std::ostream& out) const override;
 
         void collect_statistics(statistics& st) const override;
-
-        sgraph& get_sgraph() { return m_sg; }
-        sgraph const& get_sgraph() const { return m_sg; }
     };
 }

src/ast/euf/euf_sgraph.cpp

@@ -70,8 +70,14 @@ namespace euf {
         m_egraph(m),
         m_exprs(m) {
         // create seq_plugin and register it with the egraph
-        // the seq_plugin gets a reference back to this sgraph
+        m_egraph.add_plugin(alloc(seq_plugin, m_egraph));
-        m_egraph.add_plugin(alloc(seq_plugin, m_egraph, *this));
+        // register on_make callback so sgraph creates snodes for new enodes
+        std::function<void(enode*)> on_make = [this](enode* n) {
+            expr* e = n->get_expr();
+            if (m_seq.is_seq(e) || m_seq.is_re(e))
+                mk(e);
+        };
+        m_egraph.set_on_make(on_make);
     }
 
     sgraph::~sgraph() {