dt updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/datatype_decl_plugin.h

@@ -341,8 +341,10 @@ namespace datatype {
         ast_manager & get_manager() const { return m; }
         // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); 
         bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
+        bool is_datatype(expr* e) const { return is_datatype(e->get_sort()); }
         bool is_enum_sort(sort* s);
         bool is_recursive(sort * ty);
+        bool is_recursive(expr* e) { return is_recursive(e->get_sort()); }
         bool is_recursive_nested(sort * ty);
         bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); }
         bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }

src/ast/sls/sls_context.cpp

@@ -69,6 +69,16 @@ namespace sls {
             verbose_stream() << "did not find plugin for " << fid << "\n";
     }
 
+    scoped_ptr<euf::egraph>& context::ensure_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();
+    }
+
     void context::ensure_plugin(expr* e) {
         auto fid = get_fid(e);
         ensure_plugin(fid);

src/ast/sls/sls_context.h

@@ -20,6 +20,7 @@ Author:
 #include "util/sat_sls.h"
 #include "util/statistics.h"
 #include "ast/ast.h"
+#include "ast/euf/euf_egraph.h"
 #include "model/model.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/obj_hashtable.h"
@@ -195,6 +196,7 @@ 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();
 
         void collect_statistics(statistics& st) const;
         void reset_statistics();

src/ast/sls/sls_datatype_plugin.cpp

@@ -33,13 +33,21 @@ Axioms:
    a := s = acc(t), a in Atoms  => (a => s < t) in P
 
    s << t if there is a path P with conditions L.
-   L => s != t
+   L => s != t   
 
    This disregards if acc is applied to non-matching constructor.
    In this case we rely on that the interpretation of acc can be
    forced.
    If this is incorrect, include is-c(t) assumptions in path axioms.
 
+   Is P sufficient? Should we just consider all possible paths of depth at most k to be safe?
+   Example: 
+      C(acc(t)) == C(s)
+   triggers equation acc(t) = s, but the equation is implicit, so acc(t) and s are not directly
+   connected.
+   Even, the axioms extracted from P don't consider transitivity of =.
+   So the can-be-equal alias approximation is currently too strong.
+
 --*/
 
 #include "ast/sls/sls_datatype_plugin.h"
@@ -48,7 +56,10 @@ namespace sls {
     
     datatype_plugin::datatype_plugin(context& c):
         plugin(c),
-        dt(m) {
+        g(c.ensure_euf()),
+        dt(m),
+        m_axioms(m),
+        m_values(m) {
         m_fid = dt.get_family_id();
     }
     
@@ -56,9 +67,14 @@ namespace sls {
 
     void datatype_plugin::collect_path_axioms() {
         expr* t = nullptr, *z = nullptr;
-        for (auto s : ctx.subterms()) 
+        for (auto s : ctx.subterms()) {
-            if (dt.is_accessor(s, t) && dt.is_recursive(t->get_sort()))
+            if (dt.is_accessor(s, t) && dt.is_recursive(t) && dt.is_recursive(s))
                 add_edge(s, t, sat::null_literal);
+            if (dt.is_constructor(s) && dt.is_recursive(s)) {
+                for (auto arg : *to_app(s))
+                    add_edge(arg, s, sat::null_literal);
+            }
+        }
         expr* x = nullptr, *y = nullptr;
         for (sat::bool_var v = 0; v < ctx.num_bool_vars(); ++v) {
             expr* e = ctx.atom(v);
@@ -66,8 +82,10 @@ namespace sls {
                 continue;
             if (!m.is_eq(e, x, y))
                 continue;
+            if (!dt.is_recursive(x))
+                continue;
             sat::literal lp(v, false), ln(v, true);
-            if (dt.is_accessor(x, z) && dt.is_recursive(z->get_sort())) {
+            if (dt.is_accessor(x, z) && dt.is_recursive(z)) {
                 if (ctx.is_unit(lp))
                     add_edge(y, z, sat::null_literal);
                 else if (ctx.is_unit(ln))
@@ -75,7 +93,7 @@ namespace sls {
                 else
                     add_edge(y, z, lp);                    
             }
-            if (dt.is_accessor(y, z) && dt.is_recursive(z->get_sort())) {
+            if (dt.is_accessor(y, z) && dt.is_recursive(z)) {
                 if (ctx.is_unit(lp))
                     add_edge(x, z, sat::null_literal);
                 else if (ctx.is_unit(ln))
@@ -107,7 +125,9 @@ namespace sls {
             if (lit != sat::null_literal)                    
                 lits.push_back(~lit);
             if (children.contains(parent)) {
-                ctx.add_clause(lits);
+                // only assert loop clauses for proper loops
+                if (parent == children[0])
+                    ctx.add_clause(lits);
                 if (lit != sat::null_literal)                    
                     lits.pop_back();
                 continue;
@@ -144,17 +164,17 @@ namespace sls {
             
             if (dt.is_constructor(t)) {
                 auto r = dt.get_constructor_recognizer(f);
-                axioms.push_back(m.mk_app(r, t));
+                m_axioms.push_back(m.mk_app(r, t));
                 auto& acc = *dt.get_constructor_accessors(f);
                 for (unsigned i = 0; i < ta->get_num_args(); ++i) {
                     auto ti = ta->get_arg(i);
-                    axioms.push_back(m.mk_eq(ti, m.mk_app(acc[i], t)));
+                    m_axioms.push_back(m.mk_eq(ti, m.mk_app(acc[i], t)));
                 }
                 auto& cns = *dt.get_datatype_constructors(s);
                 for (auto c : cns) {
                     if (c != f) {
                         auto r2 = dt.get_constructor_recognizer(c);
-                        axioms.push_back(m.mk_not(m.mk_app(r2, t)));
+                        m_axioms.push_back(m.mk_not(m.mk_app(r2, t)));
                     }
                 }
                 continue;
@@ -166,7 +186,7 @@ namespace sls {
                 expr_ref_vector args(m);
                 for (auto a : acc)
                     args.push_back(m.mk_app(a, u));
-                axioms.push_back(m.mk_implies(m.mk_app(r, u), m.mk_eq(u, m.mk_app(c, args))));                
+                m_axioms.push_back(m.mk_implies(m.mk_app(r, u), m.mk_eq(u, m.mk_app(c, args))));                
             }
 
             if (dt.is_datatype(s)) {
@@ -176,18 +196,18 @@ namespace sls {
                     auto r = dt.get_constructor_recognizer(c);
                     ors.push_back(m.mk_app(r, t));
                 }
-                axioms.push_back(m.mk_or(ors));
+                m_axioms.push_back(m.mk_or(ors));
                 for (unsigned i = 0; i < cns.size(); ++i) {
                     auto r1 = dt.get_constructor_recognizer(cns[i]);
                     for (unsigned j = i + 1; j < cns.size(); ++j) {
                         auto r2 = dt.get_constructor_recognizer(cns[j]);
-                        axioms.push_back(m.mk_or(m.mk_not(m.mk_app(r1, t)), m.mk_not(m.mk_app(r2, t))));
+                        m_axioms.push_back(m.mk_or(m.mk_not(m.mk_app(r1, t)), m.mk_not(m.mk_app(r2, t))));
                     }
                 }
                 for (auto c : cns) {
                     if (c->get_arity() == 0) {
                         auto r = dt.get_constructor_recognizer(c);
-                        axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_const(c))));
+                        m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_const(c))));
                     }
                 }
 
@@ -203,19 +223,104 @@ namespace sls {
         collect_path_axioms();
     }
 
-    expr_ref datatype_plugin::get_value(expr* e) { return expr_ref(m); }
+    void datatype_plugin::initialize() {
-    void datatype_plugin::initialize() {}
+        add_axioms();
-    void datatype_plugin::start_propagation() {}
+    }
+
+    expr_ref datatype_plugin::get_value(expr* e) {
+        if (!dt.is_datatype(e))
+            return expr_ref(m);
+        init_values();
+        return expr_ref(m_values.get(g->find(e)->get_root_id()), m);
+    }
+
+    void datatype_plugin::init_values() {
+        if (!m_values.empty())
+            return;
+        // retrieve e-graph from sls_euf_solver: add bridge in sls_context to share e-graph
+        SASSERT(g);
+        // build top_sort<euf::enode> similar to dt_solver.cpp
+        top_sort<euf::enode> deps;
+        for (auto* n : g->nodes())
+            if (n->is_root())
+                add_dep(n, deps);
+
+        deps.topological_sort();
+        expr_ref_vector args(m);
+        // walk topological sort in order of leaves to roots, attaching values to nodes.
+        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;
+            euf::enode* con = nullptr;
+            for (auto sib : euf::enode_class(n)) {
+                if (dt.is_constructor(sib->get_expr())) {
+                    con = sib;
+                    break;
+                }
+            }
+            if (con) {
+                auto f = con->get_decl();
+                args.reset();
+                for (auto arg : euf::enode_args(con)) {
+                    if (dt.is_datatype(arg->get_sort()))
+                        args.push_back(m_values.get(arg->get_root_id()));
+                    else
+                        args.push_back(ctx.get_value(arg->get_expr()));
+                }
+                m_values.setx(n->get_id(), m.mk_app(f, args));
+            }
+            else {
+                NOT_IMPLEMENTED_YET();
+            }                
+        }        
+    }
+    
+    void datatype_plugin::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
+        if (!dt.is_datatype(n->get_expr()))
+            return;
+        euf::enode* con = nullptr;
+        for (auto sib : euf::enode_class(n)) {
+            if (dt.is_constructor(sib->get_expr())) {
+                con = sib;
+                break;
+            }
+        }
+        TRACE("dt", display(tout) << g->bpp(n) << " con: " << g->bpp(con) << "\n";);
+        if (!con)
+            dep.insert(n, nullptr);
+        else if (con->num_args() == 0)
+            dep.insert(n, nullptr);
+        for (euf::enode* arg : euf::enode_args(con))
+            dep.add(n, arg->get_root());       
+    }
+
+    
+    void datatype_plugin::start_propagation() {
+        m_values.reset();
+    }
+    
     void datatype_plugin::propagate_literal(sat::literal lit) {}
     bool datatype_plugin::propagate() { return false; }       
     bool datatype_plugin::is_sat() { return true; }
     void datatype_plugin::register_term(expr* e) {}
     std::ostream& datatype_plugin::display(std::ostream& out) const {
+        for (auto a : m_axioms)
+            out << mk_bounded_pp(a, m, 3) << "\n";
         return out;
     }
-    void datatype_plugin::mk_model(model& mdl) {}
+    void datatype_plugin::mk_model(model& mdl) {
+    }
         
-    void datatype_plugin::collect_statistics(statistics& st) const {}
+    void datatype_plugin::collect_statistics(statistics& st) const {
+        st.update("sls-dt-axioms", m_axioms.size());
+    }
+    
     void datatype_plugin::reset_statistics() {}
     
 }

src/ast/sls/sls_datatype_plugin.h

@@ -18,6 +18,7 @@ Author:
 
 #include "ast/sls/sls_context.h"
 #include "ast/datatype_decl_plugin.h"
+#include "util/top_sort.h"
 
 namespace sls {
     
@@ -30,10 +31,12 @@ namespace sls {
             expr*        parent;
             sat::literal lit;
         };
+        scoped_ptr<euf::egraph>& g;
         obj_map<sort, ptr_vector<expr>> m_dts;
         obj_map<expr, svector<parent_t>> m_parents;
-
+        
         datatype_util dt;
+        expr_ref_vector m_axioms, m_values;
         stats m_stats;
 
         void collect_path_axioms();
@@ -41,6 +44,9 @@ namespace sls {
         void add_path_axioms();
         void add_path_axioms(ptr_vector<expr>& children, sat::literal_vector& lits, svector<parent_t> const& parents);
         void add_axioms();
+        
+        void init_values();
+        void add_dep(euf::enode* n, top_sort<euf::enode>& dep);
 
     public:
         datatype_plugin(context& c);

src/ast/sls/sls_euf_plugin.h

@@ -87,6 +87,8 @@ namespace sls {
 
         void collect_statistics(statistics& st) const override;
         void reset_statistics() override;
+
+        scoped_ptr<euf::egraph>& egraph() { return m_g; }
     };
     
 }