sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure

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

src/ast/sls/sls_array_plugin.cpp

@@ -24,6 +24,7 @@ namespace sls {
         
     array_plugin::array_plugin(context& ctx):
         plugin(ctx),
+        euf(ctx.euf()),
         a(m)
     {
         m_fid = a.get_family_id();
@@ -36,36 +37,67 @@ namespace sls {
         m_kv = nullptr;
         init_egraph(*m_g);
         saturate(*m_g);
-#if 0
         if (m_g->inconsistent()) {
             resolve_conflict();
             return false;
         }         
-#endif
         return !m_g->inconsistent();
     }
 
 
     void array_plugin::resolve_conflict() {
+        ++m_stats.m_num_conflicts;
         auto& g = *m_g;
         SASSERT(g.inconsistent());
-        unsigned n = 0;
-        sat::literal_vector lits;
         ptr_vector<size_t> explain;
         g.begin_explain();
         g.explain<size_t>(explain, nullptr);
         g.end_explain();
 
-        verbose_stream() << "conflict\n";
+        IF_VERBOSE(3, verbose_stream() << "array conflict\n");
+        bool has_missing_axiom = false;
         for (auto p : explain) {
-            if (is_literal(p)) {
+            if (is_index(p)) {
-                sat::literal l = to_literal(p);
+                has_missing_axiom = true;
-                verbose_stream() << l << " " << mk_bounded_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n";
+                unsigned idx = to_index(p);
-            }
+                auto [t, sto, sel] = m_delayed_axioms[idx];
-            else {
+                switch (t) {
-                verbose_stream() << mk_bounded_pp(to_expr(p), m) << " == " << mk_bounded_pp(ctx.get_value(to_expr(p)), m) << "\n";
+                case store_axiom1:
+                    add_store_axiom1(sto->get_app());
+                    break;
+                case store_axiom2_down:
+                case store_axiom2_up:
+                    add_store_axiom2(sto->get_app(), sel->get_app());
+                    break;
+                case map_axiom:            
+                case const_axiom:
+                    add_eq_axiom(sto, sel);
+                    break;
+                default:
+                    UNREACHABLE();
+                    break;
+                }
             }
         }
+        if (has_missing_axiom)
+            return;
+
+        sat::literal_vector lits;
+        for (auto p : explain) {
+            if (is_enode(p)) {
+                auto n = to_enode(p);
+                auto v = ctx.get_value(n->get_expr());
+                lits.push_back(~ctx.mk_literal(m.mk_eq(n->get_expr(), v)));
+                if (a.is_store(n->get_expr()))
+                    add_store_axiom1(n->get_app());
+            }
+            else if (is_literal(p)) {
+                sat::literal l = to_literal(p);
+                lits.push_back(~l);
+            }          
+        }
+        IF_VERBOSE(3, verbose_stream() << "add conflict clause\n");
+        ctx.add_clause(lits);
     }
 
     // b ~ a[i -> v]
@@ -141,13 +173,12 @@ namespace sls {
         if (nmap->get_root() == nsel->get_root())
             return;
         if (!are_distinct(nsel, nmap)) {
-            g.merge(nmap, nsel, nullptr);
+            g.merge(nmap, nsel, to_ptr(map_axiom_index(nmap, nsel)));
             g.propagate();
             if (!g.inconsistent())
                 return;
         }
-        expr_ref eq(m.mk_eq(nmap->get_expr(), nsel->get_expr()), m);
+        add_eq_axiom(nmap, nsel);
-        ctx.add_theory_axiom(eq);
     }
 
     euf::enode* array_plugin::mk_select(euf::egraph& g, euf::enode* b, euf::enode* sel) {
@@ -175,10 +206,10 @@ namespace sls {
         auto nsel = mk_select(g, n, n);
         VERIFY(!g.inconsistent());
         if (!are_distinct(nsel, val)) {
-            g.merge(nsel, val, nullptr);
+            g.merge(nsel, val, to_ptr(store_axiom1_index(n)));
             g.propagate();
             if (!g.inconsistent())
-                return;
+                return;            
         }
         add_store_axiom1(n->get_app());
     }
@@ -195,7 +226,7 @@ namespace sls {
             return; 
         auto nsel = mk_select(g, sto->get_arg(0), sel);
         if (!are_distinct(nsel, sel)) {
-            g.merge(nsel, sel, nullptr);
+            g.merge(nsel, sel, to_ptr(store_axiom2_down_index(sto, sel)));
             g.propagate();
             if (!g.inconsistent())
                 return;
@@ -215,7 +246,7 @@ namespace sls {
             return;
         auto nsel = mk_select(g, sto, sel);
         if (!are_distinct(nsel, sel)) {
-            g.merge(nsel, sel, nullptr);
+            g.merge(nsel, sel, to_ptr(store_axiom2_up_index(sto, sel)));
             g.propagate();
             if (!g.inconsistent())
                 return;
@@ -234,13 +265,13 @@ namespace sls {
         auto val = cn->get_arg(0);
         auto nsel = mk_select(g, cn, sel);
         if (!are_distinct(nsel, sel)) {
-            g.merge(nsel, sel, nullptr);
+            g.merge(nsel, sel, to_ptr(const_axiom_index(val, nsel)));
             g.propagate();
             if (!g.inconsistent())
                 return;
         }
-        expr_ref eq(m.mk_eq(val->get_expr(), nsel->get_expr()), m);
+        ++m_stats.m_num_axioms;
-        ctx.add_theory_axiom(eq);
+        add_eq_axiom(val, nsel);
     }
 
     bool array_plugin::are_distinct(euf::enode* a, euf::enode* b) {
@@ -270,6 +301,7 @@ namespace sls {
         expr_ref sel(a.mk_select(args), m);
         expr_ref eq(m.mk_eq(sel, to_app(sto)->get_arg(sto->get_num_args() - 1)), m);
         IF_VERBOSE(3, verbose_stream() << "add store axiom 1 " << mk_bounded_pp(sto, m) << "\n");
+        ++m_stats.m_num_axioms;
         ctx.add_theory_axiom(eq);
     }
     
@@ -291,6 +323,7 @@ namespace sls {
         for (unsigned i = 1; i < sel->get_num_args() - 1; ++i) 
             ors.push_back(m.mk_eq(sel->get_arg(i), sto->get_arg(i)));     
         IF_VERBOSE(3, verbose_stream() << "add store axiom 2 " << mk_bounded_pp(sto, m) << " " << mk_bounded_pp(sel, m) << "\n");
+        ++m_stats.m_num_axioms;
         ctx.add_theory_axiom(m.mk_or(ors));
     }
 
@@ -307,11 +340,13 @@ namespace sls {
             n1 = n1 ? n1 : g.mk(t, 0, args.size(), args.data());
             if (a.is_array(t))
                 continue;
+            if (m.is_bool(t))
+                continue;
             auto v = ctx.get_value(t);
             IF_VERBOSE(3, verbose_stream() << "init " << mk_bounded_pp(t, m) << " := " << mk_bounded_pp(v, m) << " " << g.inconsistent() << "\n");
             n2 = g.find(v);
             n2 = n2 ? n2: g.mk(v, 0, 0, nullptr);
-            g.merge(n1, n2, to_ptr(t));            
+            g.merge(n1, n2, to_ptr(n1));            
         }
         for (auto lit : ctx.root_literals()) {
             if (!ctx.is_true(lit) || lit.sign())
@@ -319,9 +354,10 @@ namespace sls {
             auto e = ctx.atom(lit.var());
             expr* x = nullptr, * y = nullptr;
             if (e && m.is_eq(e, x, y))
-                g.merge(g.find(x), g.find(y), to_ptr(lit));
+                g.merge(g.find(x), g.find(y), nullptr);
 
         }
+        g.propagate();
 
         IF_VERBOSE(3, display(verbose_stream()));
         
@@ -388,4 +424,9 @@ namespace sls {
         }
         return out;
     }
+
+    void array_plugin::collect_statistics(statistics& st) const {
+        st.update("sls-array-conflicts", m_stats.m_num_conflicts);
+        st.update("sls-array-axioms", m_stats.m_num_axioms);
+    }
 }

src/ast/sls/sls_array_plugin.h

@@ -22,6 +22,8 @@ Author:
 
 namespace sls {
 
+    class euf_plugin;
+
     class array_plugin : public plugin {
         struct select_args {
             euf::enode* sel = nullptr;
@@ -29,15 +31,15 @@ namespace sls {
             select_args() {}
         };
         struct select_args_hash {
-            unsigned operator()(select_args const& a) const { 
+            unsigned operator()(select_args const& a) const {
                 unsigned h = 0;
                 for (unsigned i = 1; i < a.sel->num_args(); ++i)
-                    h ^= a.sel->get_arg(i)->get_root()->hash(); 
+                    h ^= a.sel->get_arg(i)->get_root()->hash();
                 return h;
             };
         };
         struct select_args_eq {
-            bool operator()(select_args const& a, select_args const& b) const { 
+            bool operator()(select_args const& a, select_args const& b) const {
                 SASSERT(a.sel->num_args() == b.sel->num_args());
                 for (unsigned i = 1; i < a.sel->num_args(); ++i)
                     if (a.sel->get_arg(i)->get_root() != b.sel->get_arg(i)->get_root())
@@ -47,12 +49,37 @@ namespace sls {
         };
         typedef map<select_args, euf::enode*, select_args_hash, select_args_eq> select2value;
         typedef obj_map<euf::enode, select2value> kv;
+        struct stats {
+            unsigned m_num_conflicts = 0;
+            unsigned m_num_axioms = 0;
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
 
+        euf_plugin&    euf;
         array_util     a;
         scoped_ptr<euf::egraph> m_g;
-        scoped_ptr<kv> m_kv;
+        scoped_ptr<kv>          m_kv;
-        bool m_add_conflicts = true;
+        bool  m_add_conflicts = true;
-        bool m_has_arrays = false;
+        bool  m_has_arrays = false;
+        stats m_stats;
+
+        enum axiom_t { store_axiom1, store_axiom2_down, store_axiom2_up, map_axiom, const_axiom };
+        struct axiom_instance {
+            axiom_t t;
+            euf::enode* sto; euf::enode* sel;
+        };
+        svector<axiom_instance> m_delayed_axioms;
+        unsigned store_axiom1_index(euf::enode* n) { m_delayed_axioms.push_back({ store_axiom1, n, nullptr }); return m_delayed_axioms.size() - 1; }
+        unsigned store_axiom2_down_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ store_axiom2_down, sto, sel }); return m_delayed_axioms.size() - 1; }
+        unsigned store_axiom2_up_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ store_axiom2_up, sto, sel }); return m_delayed_axioms.size() - 1; }
+        unsigned map_axiom_index(euf::enode* sto, euf::enode* sel) { m_delayed_axioms.push_back({ map_axiom, sto, sel }); return m_delayed_axioms.size() - 1; }
+        unsigned const_axiom_index(euf::enode* val, euf::enode* sel) { m_delayed_axioms.push_back({ const_axiom, val, sel }); return m_delayed_axioms.size() - 1; }
+
+        void add_eq_axiom(euf::enode* x, euf::enode* y) {
+            ++m_stats.m_num_axioms;
+            expr_ref eq(m.mk_eq(x->get_expr(), y->get_expr()), m);
+            ctx.add_theory_axiom(eq);
+        }
 
         void init_egraph(euf::egraph& g);
         void init_kv(euf::egraph& g, kv& kv);
@@ -73,10 +100,14 @@ namespace sls {
 
         void resolve_conflict();
         size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
-        size_t* to_ptr(expr* t) { return reinterpret_cast<size_t*>((reinterpret_cast<size_t>(t) << 4) + 1); }
+        size_t* to_ptr(euf::enode* t) { return reinterpret_cast<size_t*>((reinterpret_cast<size_t>(t) << 4) + 1); }
-        bool is_literal(size_t* p) { return (reinterpret_cast<size_t>(p) & 1) == 0; }
+        size_t* to_ptr(unsigned n) { return reinterpret_cast<size_t*>((size_t)(n << 4) + 3); }
+        bool is_literal(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 0; }
+        bool is_index(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 3; }
+        bool is_enode(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 1; }
         sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
-        expr* to_expr(size_t* p) { return reinterpret_cast<expr*>(reinterpret_cast<size_t>(p) >> 4); }
+        euf::enode* to_enode(size_t* p) { return reinterpret_cast<euf::enode*>(reinterpret_cast<size_t>(p) >> 4); }
+        unsigned to_index(size_t* p) { return static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4); }
         
     public:
         array_plugin(context& ctx);
@@ -95,8 +126,8 @@ namespace sls {
         void on_restart() override {}
         std::ostream& display(std::ostream& out) const override;
         bool set_value(expr* e, expr* v) override { return false; }
-        void collect_statistics(statistics& st) const override {}
+        void collect_statistics(statistics& st) const override;
-        void reset_statistics() override {}
+        void reset_statistics() override { m_stats.reset(); }
     };
 
 }

src/ast/sls/sls_context.cpp

@@ -315,11 +315,9 @@ namespace sls {
         auto p = m_plugins.get(fid, nullptr);
         if (p) 
             return p->get_value(e);  
-        if (m.is_bool(e)) {
+        if (m.is_bool(e)) 
-            sat::bool_var v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
+            return expr_ref(m.mk_bool_val(is_true(e)), m);
-            if (v != sat::null_bool_var)
+        
-                return expr_ref(m.mk_bool_val(is_true(v)), m);
-        }
         verbose_stream() << fid << " " << m.get_family_name(fid) << " " << mk_pp(e, m) << "\n";
         UNREACHABLE();
         return expr_ref(e, m);

src/ast/sls/sls_euf_plugin.cpp

@@ -90,7 +90,7 @@ namespace sls {
         g.explain<size_t>(explain, nullptr);
         g.end_explain();
         double reward = -1;
-        TRACE("enf",
+        TRACE("euf",
             for (auto p : explain) {
                 sat::literal l = to_literal(p);
                 tout << l << " " << mk_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n";