Refactor context management, improve datatype handling, and enhance logging in sls plugins.

src/ast/sls/sls_context.cpp

@@ -72,14 +72,18 @@ namespace sls {
             verbose_stream() << "did not find plugin for " << fid << "\n";
     }
 
-    scoped_ptr<euf::egraph>& context::ensure_euf() {
+    scoped_ptr<euf::egraph>& context::egraph() {
+        return euf().egraph();
+    }
+
+    euf_plugin& context::euf() {
         auto fid = user_sort_family_id;
         auto p = m_plugins.get(fid, nullptr);
         if (!p) {
             p = alloc(euf_plugin, *this);
             register_plugin(p);
         }
-        return dynamic_cast<euf_plugin*>(p)->egraph();
+        return *dynamic_cast<euf_plugin*>(p);
     }
 
     void context::ensure_plugin(expr* e) {

src/ast/sls/sls_context.h

@@ -29,6 +29,7 @@ Author:
 namespace sls {
 
     class context;
+    class euf_plugin;
     
     class plugin {
     protected:
@@ -196,7 +197,8 @@ namespace sls {
         ast_manager& get_manager() { return m; }
         std::ostream& display(std::ostream& out) const;
         std::ostream& display_all(std::ostream& out) const { return s.display(out); }
-        scoped_ptr<euf::egraph>& ensure_euf();
+        scoped_ptr<euf::egraph>& egraph();
+        euf_plugin& euf();
 
         void collect_statistics(statistics& st) const;
         void reset_statistics();

src/ast/sls/sls_datatype_plugin.cpp

@@ -62,19 +62,26 @@ Model-repair based:
    violated x != y: x <- fresh, y <- fresh
    violated x != t: x <- fresh, subterm y of t: y <- fresh
 
+   acc(x) = t: eval(x) = c(u, v) acc(c(u,v)) = u -> repair(u = t)
+   acc(x) = t: eval(x) does not match acc        -> acc(x) 
+   has a fixed interpretation, so repair over t instead, or update interpretation of x
+
+   uses:
     model::get_fresh_value(s)
     model::get_some_value(s)
 
 --*/
 
 #include "ast/sls/sls_datatype_plugin.h"
+#include "ast/sls/sls_euf_plugin.h"
 #include "ast/ast_pp.h"
 
 namespace sls {
     
     datatype_plugin::datatype_plugin(context& c):
         plugin(c),
-        g(c.ensure_euf()),
+        euf(c.euf()),
+        g(c.egraph()),
         dt(m),
         m_axioms(m),
         m_values(m) {
@@ -206,6 +213,10 @@ namespace sls {
                 m_axioms.push_back(m.mk_iff(t, m.mk_app(dt.get_constructor_is(c), u)));
             }
             
+            if (dt.is_update_field(t)) {
+                NOT_IMPLEMENTED_YET();
+            }
+
             if (dt.is_datatype(s)) {
                 auto& cns = *dt.get_datatype_constructors(s);
                 expr_ref_vector ors(m);
@@ -309,13 +320,12 @@ namespace sls {
         // assign fresh values to uninterpeted nodes
         for (euf::enode* n : deps.top_sorted()) {
             SASSERT(n->is_root());
+            expr* e = n->get_expr();
+            if (!dt.is_datatype(e))
+                continue;
             unsigned id = n->get_id();
             if (m_values.get(id, nullptr))
                 continue;
-            expr* e = n->get_expr();
-            m_values.reserve(id + 1);
-            if (!dt.is_datatype(e))
-                continue;
             auto con = get_constructor(n);
             if (con)
                 continue;
@@ -327,13 +337,10 @@ namespace sls {
         for (euf::enode* n : deps.top_sorted()) {
             SASSERT(n->is_root());
             unsigned id = n->get_id();
-            if (m_values.get(id, nullptr))
-                continue;
             expr* e = n->get_expr();
-            m_values.reserve(id + 1);
             if (!dt.is_datatype(e))
                 continue;
-            if (m_values.get(id, nullptr))
+            if (m_values.get(id))
                 continue;
             euf::enode* con = get_constructor(n);
             if (!con)
@@ -432,9 +439,10 @@ namespace sls {
                                 break;
                             }
                         }
+                        IF_VERBOSE(1,
                             verbose_stream() << "cycle\n";
                             for (auto e : diseqs)
-                            verbose_stream() << mk_pp(e, m) << "\n";
+                                verbose_stream() << mk_pp(e, m) << "\n";);
                         ctx.add_constraint(m.mk_or(diseqs));
                         return true;                       
                     }
@@ -463,7 +471,9 @@ namespace sls {
         return out;
     }
     
-    void datatype_plugin::propagate_literal(sat::literal lit) {}
+    void datatype_plugin::propagate_literal(sat::literal lit) {
+        euf.propagate_literal(lit);
+    }
    
     bool datatype_plugin::is_sat() { return true; }
     void datatype_plugin::register_term(expr* e) {}

src/ast/sls/sls_datatype_plugin.h

@@ -22,6 +22,8 @@ Author:
 
 namespace sls {
 
+    class euf_plugin;
+    
     class datatype_plugin : public plugin {
         struct stats {
             unsigned m_num_axioms = 0;
@@ -31,6 +33,7 @@ namespace sls {
             expr*        parent;
             sat::literal lit;
         };
+        euf_plugin& euf;
         scoped_ptr<euf::egraph>& g;
         obj_map<sort, ptr_vector<expr>> m_dts;
         obj_map<expr, svector<parent_t>> m_parents;

src/ast/sls/sls_euf_plugin.cpp

@@ -216,6 +216,7 @@ namespace sls {
             return;
 
         auto block = [&](euf::enode* a, euf::enode* b) {
+            TRACE("euf", tout << "block " << m_g->bpp(a) << " != " << m_g->bpp(b) << "\n");
             if (a->get_root() != b->get_root())
                 return;
             ptr_vector<size_t> explain;
@@ -281,6 +282,7 @@ namespace sls {
         // merge all equalities
         // check for conflict with disequalities during propagation
         if (merge_eqs) {
+            TRACE("euf", tout << "root literals " << ctx.root_literals() << "\n");
             for (auto lit : ctx.root_literals()) {
                 if (!ctx.is_true(lit))
                     lit.neg();