working on mam

src/sat/smt/CMakeLists.txt

@@ -29,6 +29,8 @@ z3_add_component(sat_smt
     euf_relevancy.cpp
     euf_solver.cpp
     fpa_solver.cpp
+    q_ematch.cpp
+    q_mam.cpp
     q_mbi.cpp
     q_model_fixer.cpp
     q_solver.cpp

src/sat/smt/q_ematch.cpp

@@ -0,0 +1,445 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_ematch.cpp
+
+Abstract:
+
+    E-matching quantifier instantiation plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-01-24
+
+Todo:
+
+- clausify
+- propagate without instantiations, produce explanations for eval
+- generations
+- insert instantiations into priority queue 
+- cache instantiations and substitutions
+- nested quantifiers
+- non-cnf quantifiers
+
+--*/
+
+#include "ast/rewriter/var_subst.h"
+#include "solver/solver.h"
+#include "sat/smt/sat_th.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/q_solver.h"
+#include "sat/smt/q_mam.h"
+#include "sat/smt/q_ematch.h"
+
+
+namespace q {
+
+    ematch::ematch(euf::solver& ctx, solver& s):
+        ctx(ctx),
+        m_qs(s),
+        m(ctx.get_manager())
+    {
+        std::function<void(euf::enode*, euf::enode*)> _on_merge = 
+            [&](euf::enode* root, euf::enode* other) { 
+            on_merge(root, other); 
+        };
+        ctx.get_egraph().set_on_merge(_on_merge);
+        m_mam = mam::mk(ctx, *this);
+    }
+
+    void ematch::ensure_ground_enodes(expr* e) {
+        mam::ground_subterms(e, m_ground);
+        for (expr* g : m_ground) 
+            m_qs.e_internalize(g);
+    }
+
+    void ematch::ensure_ground_enodes(clause const& c) {
+        quantifier* q = c.m_q;
+        unsigned num_patterns = q->get_num_patterns();
+        for (unsigned i = 0; i < num_patterns; i++) 
+            ensure_ground_enodes(q->get_pattern(i));
+        for (auto lit : c.m_lits) {
+            ensure_ground_enodes(lit.lhs);
+            ensure_ground_enodes(lit.rhs);
+        }
+    }
+
+    struct restore_watch : public trail<euf::solver> {
+        vector<unsigned_vector>& v;
+        unsigned idx, offset;
+        restore_watch(vector<unsigned_vector>& v, unsigned idx):
+            v(v), idx(idx), offset(v[idx].size()) {}
+        void undo(euf::solver& ctx) override {
+            v[idx].shrink(offset);
+        }
+    };
+
+    void ematch::on_merge(euf::enode* root, euf::enode* other) {
+        SASSERT(root->get_root() == other->get_root());
+        unsigned root_id = root->get_expr_id();
+        unsigned other_id = other->get_expr_id();
+        m_watch.reserve(std::max(root_id, other_id) + 1);
+
+        insert_to_propagate(root_id);
+        insert_to_propagate(other_id);
+
+        if (!m_watch[other_id].empty()) {        
+            ctx.push(restore_watch(m_watch, root_id));
+            m_watch[root_id].append(m_watch[other_id]);
+        }
+   
+        m_mam->on_merge(root, other);
+        if (m_lazy_mam)
+            m_lazy_mam->on_merge(root, other);
+    }
+
+    // watch only nodes introduced in bindings or ground arguments of functions
+    // or functions that have been inserted.
+
+    void ematch::add_watch(euf::enode* n, unsigned idx) {
+        unsigned root_id = n->get_root_id();
+        m_watch.reserve(root_id + 1);
+        ctx.push(restore_watch(m_watch, root_id));
+        m_watch[root_id].push_back(idx);
+    }
+
+    void ematch::init_watch(expr* e, unsigned clause_idx) {
+        ptr_buffer<expr> todo;
+        m_mark.reset();
+        todo.push_back(e);
+        while (!todo.empty()) {
+            expr* t = todo.back();
+            if (m_mark.is_marked(t))
+                continue;
+            todo.pop_back();
+            m_mark.mark(t);
+            if (is_ground(t)) {
+                add_watch(ctx.get_egraph().find(t), clause_idx);
+                continue;
+            }
+            if (!is_app(t))
+                continue;
+            for (expr* arg : *to_app(t))
+                todo.push_back(arg);
+        }
+    }
+
+    void ematch::init_watch(clause& c, unsigned idx) {
+        for (auto lit : c.m_lits) {
+            if (!is_ground(lit.lhs))
+                init_watch(lit.lhs, idx);
+            if (!is_ground(lit.rhs))
+                init_watch(lit.rhs, idx);
+        }
+    }
+
+    ematch::binding* ematch::alloc_binding(unsigned n) {
+        unsigned sz = sizeof(binding) + sizeof(euf::enode* const*)*n;
+        void* mem = ctx.get_region().allocate(sz);
+        return new (mem) binding();
+    }
+
+    void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding) {
+        clause& c = *m_clauses[m_q2clauses[q]];
+        if (propagate(_binding, c))
+            return;
+        unsigned n = q->get_num_decls();
+        binding* b = alloc_binding(n);
+        b->m_propagated = false;
+        for (unsigned i = 0; i < n; ++i)
+            b->m_nodes[i] = _binding[i];
+        c.m_bindings.push_back(b);
+        ctx.push(push_back_vector<euf::solver, ptr_vector<binding>>(c.m_bindings));
+    }
+
+    bool ematch::propagate(euf::enode* const* binding, clause& c) {
+        unsigned clause_idx = m_q2clauses[c.m_q];
+        struct scoped_reset {
+            ematch& e;
+            scoped_reset(ematch& e): e(e) { e.m_mark.reset(); }
+            ~scoped_reset() { e.m_mark.reset(); }
+        };
+        scoped_reset _sr(*this);
+
+        unsigned idx = UINT_MAX;
+        for (unsigned i = c.m_lits.size(); i-- > 0; ) {
+            lit l = c.m_lits[i];
+            m_indirect_nodes.reset();
+            lbool cmp = compare(binding, l.lhs, l.rhs);
+            switch (cmp) {
+            case l_false:
+                if (l.sign) {
+                    if (i > 0)
+                        std::swap(c.m_lits[0], c.m_lits[i]);
+                    return true;
+                }
+                break;
+            case l_true:
+                if (!l.sign) {
+                    if (i > 0)
+                        std::swap(c.m_lits[0], c.m_lits[i]);
+                    return true;
+                }
+                break;
+            case l_undef:
+                if (idx == 0) {
+                    // attach bindings and indirect nodes
+                    // to watch
+                    for (euf::enode* n : m_indirect_nodes)
+                        add_watch(n, clause_idx);
+                    for (unsigned j = c.m_q->get_num_decls(); j-- > 0; )
+                        add_watch(binding[j], clause_idx);
+                    if (i > 1) 
+                        std::swap(c.m_lits[1], c.m_lits[i]);
+                    return false;
+                }
+                else if (i > 0) {
+                    std::swap(c.m_lits[0], c.m_lits[i]);
+                    idx = 0;
+                }
+                break;
+            }
+        }
+        if (idx == UINT_MAX) {
+            std::cout << "clause is false\n";
+        }
+        else {
+            std::cout << "unit propagate\n";
+        }
+        instantiate(binding, c);
+        return true;
+    }
+
+    // vanilla instantiation method.
+    void ematch::instantiate(euf::enode* const* binding, clause& c) {
+        expr_ref_vector _binding(m);
+        quantifier* q = c.m_q;
+        for (unsigned i = 0; i < q->get_num_decls(); ++i)
+            _binding.push_back(binding[i]->get_expr());
+        var_subst subst(m);
+        expr_ref result = subst(q->get_expr(), _binding);
+        if (is_forall(q)) 
+            m_qs.add_clause(~ctx.mk_literal(q), ctx.mk_literal(result));
+        else
+            m_qs.add_clause(ctx.mk_literal(q), ~ctx.mk_literal(result));
+    }
+
+    lbool ematch::compare(euf::enode* const* binding, expr* s, expr* t) {
+        euf::enode* sn = eval(binding, s);
+        euf::enode* tn = eval(binding, t);
+        lbool c;
+        if (sn && sn == tn)
+            return l_true;
+        if (sn && tn && ctx.get_egraph().are_diseq(sn, tn))
+            return l_false;
+        if (sn && tn)
+            return l_undef;
+        if (!sn && !tn) 
+            return compare_rec(binding, s, t);
+        if (!sn && tn) 
+            for (euf::enode* t1 : euf::enode_class(tn)) 
+                if (c = compare_rec(binding, s, t1->get_expr()), c != l_undef)
+                    return c;
+        if (sn && !tn) 
+            for (euf::enode* s1 : euf::enode_class(sn)) 
+                if (c = compare_rec(binding, t, s1->get_expr()), c != l_undef)
+                    return c;
+        return l_undef;
+    }
+
+    // f(p1) = f(p2)  if p1 = p2
+    // f(p1) != f(p2) if p1 != p2 and f is injective
+    lbool ematch::compare_rec(euf::enode* const* binding, expr* s, expr* t) {
+        if (m.are_equal(s, t))
+            return l_true;
+        if (m.are_distinct(s, t))
+            return l_false;
+        if (!is_app(s) || !is_app(t))
+            return l_undef;
+        if (to_app(s)->get_decl() != to_app(t)->get_decl())
+            return l_undef;
+        if (to_app(s)->get_num_args() != to_app(t)->get_num_args())
+            return l_undef;
+        bool is_injective = to_app(s)->get_decl()->is_injective();
+        bool has_undef = false;
+        for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) {
+            switch (compare(binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i))) {
+            case l_true:
+                break;
+            case l_false:
+                if (is_injective)
+                    return l_false;
+                return l_undef;
+            case l_undef:
+                if (!is_injective)
+                    return l_undef;
+                has_undef = true;
+                break;
+            }
+        }
+        return has_undef ? l_undef : l_true;
+    }
+
+    euf::enode* ematch::eval(euf::enode* const* binding, expr* e) {
+        if (is_ground(e))
+            ctx.get_egraph().find(e)->get_root();
+        if (m_mark.is_marked(e))
+            return m_eval[e->get_id()];
+        ptr_buffer<expr> todo;
+        ptr_buffer<euf::enode> args;
+        todo.push_back(e);
+        while (!todo.empty()) {
+            expr* t = todo.back();
+            SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
+            if (is_ground(t)) {
+                m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
+                SASSERT(m_eval[t->get_id()]);
+                todo.pop_back();
+                continue;
+            }
+            if (m_mark.is_marked(t)) {
+                todo.pop_back();
+                continue;
+            }
+            if (is_var(t)) {
+                m_mark.mark(t);
+                m_eval.setx(t->get_id(), binding[to_var(t)->get_idx()], nullptr);
+                todo.pop_back();
+                continue;
+            }
+            if (!is_app(t))
+                return nullptr;
+            args.reset();
+            for (expr* arg : *to_app(t)) {
+                if (m_mark.is_marked(arg))
+                    args.push_back(m_eval[t->get_id()]);
+                else
+                    todo.push_back(arg);
+            }
+            if (args.size() == to_app(t)->get_num_args()) {
+                euf::enode* n = ctx.get_egraph().find(t, args.size(), args.c_ptr());
+                if (!n)
+                    return nullptr;
+                m_indirect_nodes.push_back(n);
+                m_eval.setx(t->get_id(), n->get_root(), nullptr);
+                m_mark.mark(t);
+                todo.pop_back();
+            }
+        }
+        return m_eval[e->get_id()]->get_root();
+    }
+
+    void ematch::insert_to_propagate(unsigned node_id) {
+        if (m_node_in_queue.contains(node_id))
+            return;
+        m_node_in_queue.insert(node_id);
+        for (unsigned idx : m_watch[node_id]) {
+            if (!m_clause_in_queue.contains(idx)) {
+                m_clause_in_queue.insert(idx);
+                m_queue.push_back(idx);
+            }
+        }
+    }
+
+    bool ematch::propagate() {
+        m_mam->propagate();
+        if (m_qhead >= m_queue.size())
+            return false;
+        bool propagated = false;
+        ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
+        for (; m_qhead < m_queue.size(); ++m_qhead) {
+            unsigned idx = m_queue[m_qhead];
+            clause& c = *m_clauses[idx];
+            for (auto& b : c.bindings()) {
+                if (!b->propagated() && propagate(b->m_nodes, c)) {
+                    ctx.push(value_trail<euf::solver, bool>(b->m_propagated));
+                    b->set_propagated(true);
+                    propagated = true;
+                }
+            }
+        }
+        m_clause_in_queue.reset();
+        m_node_in_queue.reset();
+        return propagated;
+    }
+
+    ematch::clause* ematch::clausify(quantifier* q) {
+        NOT_IMPLEMENTED_YET();
+        return nullptr;
+    }
+
+    /**
+     * Attach ground subterms of patterns so they appear shared.
+     */
+    void ematch::attach_ground_pattern_terms(expr* pat) {
+        mam::ground_subterms(pat, m_ground);
+        for (expr* g : m_ground) { 
+            euf::enode* n = ctx.get_egraph().find(g);
+            if (!n->is_attached_to(m_qs.get_id())) {
+                euf::theory_var v = m_qs.mk_var(n);
+                ctx.get_egraph().add_th_var(n, v, m_qs.get_id());
+            }
+        }
+    }
+
+    struct ematch::pop_clause : public trail<euf::solver> {
+        ematch& em;
+        pop_clause(ematch& em): em(em) {}
+        void undo(euf::solver& ctx) override {
+            em.m_q2clauses.remove(em.m_clauses.back()->m_q);
+            em.m_clauses.pop_back();
+        }
+    };
+
+    void ematch::add(quantifier* q) {
+        clause* c = clausify(q);
+        ensure_ground_enodes(*c);
+        unsigned idx = m_clauses.size();
+        m_clauses.push_back(c);
+        m_q2clauses.insert(q, idx);
+        ctx.push(pop_clause(*this));
+        init_watch(*c, idx);
+        
+        bool has_unary_pattern = false;
+        unsigned num_patterns = q->get_num_patterns();
+        for (unsigned i = 0; i < num_patterns && !has_unary_pattern; i++) 
+            has_unary_pattern = (1 == to_app(q->get_pattern(i))->get_num_args());
+        unsigned num_eager_multi_patterns = ctx.get_config().m_qi_max_eager_multipatterns;
+        if (!has_unary_pattern)
+            num_eager_multi_patterns++;
+        for (unsigned i = 0, j = 0; i < num_patterns; i++) {
+            app * mp = to_app(q->get_pattern(i));
+            SASSERT(m.is_pattern(mp));
+            bool unary = (mp->get_num_args() == 1);
+            TRACE("quantifier", tout << "adding:\n" << expr_ref(mp, m) << "\n";);
+            if (!unary && j >= num_eager_multi_patterns) {
+                TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";);
+                if (!m_lazy_mam)
+                    m_lazy_mam = mam::mk(ctx, *this);
+                m_lazy_mam->add_pattern(q, mp);
+            }
+            else 
+                m_mam->add_pattern(q, mp);
+
+            attach_ground_pattern_terms(mp);
+
+            if (!unary)
+                j++;
+        }
+    }
+
+    bool ematch::operator()() {
+        if (m_lazy_mam)
+            m_lazy_mam->propagate();
+        if (propagate())
+            return true;
+        // 
+        // TODO: loop over pending bindings and instantiate them
+        // 
+        NOT_IMPLEMENTED_YET();
+        return false;
+    }
+
+}

src/sat/smt/q_ematch.h

@@ -0,0 +1,138 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_ematch.h
+
+Abstract:
+
+    E-matching quantifier instantiation plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-01-24
+
+--*/
+#pragma once
+
+#include "util/nat_set.h"
+#include "solver/solver.h"
+#include "sat/smt/sat_th.h"
+#include "sat/smt/q_mam.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace q {
+
+    class solver;
+
+    class ematch {
+        struct stats {
+            unsigned m_num_instantiations;
+            
+            stats() { reset(); }
+
+            void reset() {
+                memset(this, 0, sizeof(*this));
+            }
+        };
+
+
+        struct lit {
+            expr_ref lhs;
+            expr_ref rhs;
+            bool     sign;
+            lit(expr_ref& lhs, expr_ref& rhs, bool sign):
+                lhs(lhs), rhs(rhs), sign(sign) {}
+            
+        };
+
+        struct binding {
+            bool               m_propagated { false };
+            euf::enode*        m_nodes[0];
+
+            binding() {}
+
+            bool propagated() const { return m_propagated; }
+            void set_propagated(bool b) { m_propagated = b; }
+            euf::enode* const* nodes() { return m_nodes; }
+        };
+
+        binding* alloc_binding(unsigned n);
+        
+        struct clause {
+            vector<lit>         m_lits;
+            quantifier*         m_q;
+            ptr_vector<binding> m_bindings;
+
+            ptr_vector<binding> const& bindings() { return m_bindings; }
+        };
+
+        struct pop_clause;
+        
+        euf::solver&                           ctx;
+        solver&                                m_qs;
+        ast_manager&                           m;
+        scoped_ptr<q::mam>                     m_mam, m_lazy_mam;
+        ptr_vector<clause>                     m_clauses;
+        obj_map<quantifier, unsigned>          m_q2clauses;
+        vector<unsigned_vector>                m_watch;     // expr_id -> clause-index*
+        stats                                  m_stats;
+        expr_fast_mark1                        m_mark;
+
+        nat_set         m_node_in_queue;
+        nat_set         m_clause_in_queue;
+        unsigned        m_qhead { 0 };
+        unsigned_vector m_queue;
+
+        ptr_vector<app> m_ground;
+        void ensure_ground_enodes(expr* e);
+        void ensure_ground_enodes(clause const& c);
+
+        // compare s, t modulo sign under binding
+        lbool compare(euf::enode* const* binding, expr* s, expr* t);
+        lbool compare_rec(euf::enode* const* binding, expr* s, expr* t);
+        euf::enode_vector m_eval, m_indirect_nodes;
+        euf::enode* eval(euf::enode* const* binding, expr* e);
+
+        bool propagate(euf::enode* const* binding, clause& c);
+        void instantiate(euf::enode* const* binding, clause& c);
+
+        // register as callback into egraph.
+        void on_merge(euf::enode* root, euf::enode* other);          
+        void insert_to_propagate(unsigned node_id);
+
+        void add_watch(euf::enode* root, unsigned clause_idx);
+        void init_watch(expr* e, unsigned clause_idx);
+        void init_watch(clause& c, unsigned idx);
+
+        // extract explanation
+        void get_antecedents(euf::enode* const* binding, unsigned clause_idx, bool probing);
+
+        void attach_ground_pattern_terms(expr* pat);
+        clause* clausify(quantifier* q);
+
+
+    public:
+        
+        ematch(euf::solver& ctx, solver& s);
+            
+        bool operator()();
+
+        bool propagate();
+
+        void init_search();
+
+        void add(quantifier* q);
+
+        void collect_statistics(statistics& st) const;
+
+        // callback from mam
+        void on_binding(quantifier* q, app* pat, euf::enode* const* binding);
+
+    };
+
+}

src/sat/smt/q_mam.h

@@ -0,0 +1,71 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    euf_mam.h
+
+Abstract:
+
+    Matching Abstract Machine
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-02-13.
+    Nikolaj Bjorner (nbjorner) 2021-01-22.
+
+--*/
+#pragma once
+
+#include "ast/ast.h"
+#include "ast/euf/euf_egraph.h"
+#include <functional>
+
+namespace euf {
+    class solver;
+};
+
+namespace q {
+
+    typedef euf::enode enode;
+    typedef euf::egraph egraph;
+    typedef euf::enode_vector enode_vector;
+
+    class ematch;
+
+    /**
+       \brief Matching Abstract Machine (MAM)
+    */
+    class mam {
+        friend class mam_impl;
+
+        mam() {}
+
+    public:
+
+        static mam * mk(euf::solver& ctx, ematch& em);
+        
+        virtual ~mam() {}
+        
+        virtual void add_pattern(quantifier * q, app * mp) = 0;
+
+        virtual void propagate() = 0;
+
+        virtual bool can_propagate() const = 0;
+        
+        virtual void rematch(bool use_irrelevant = false) = 0;
+        
+        virtual void on_merge(enode * root, enode * other) = 0;
+
+        virtual void reset() = 0;
+
+        virtual std::ostream& display(std::ostream& out) = 0;
+                
+        virtual bool check_missing_instances() = 0;
+
+        virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation) = 0;
+
+        static void ground_subterms(expr* e, ptr_vector<app>& ground);
+    };
+};
+

src/sat/smt/q_solver.h

@@ -55,6 +55,8 @@ namespace q {
         
         expr_ref_vector const& expand(quantifier* q);
 
+        friend class ematch;
+
     public:
 
         solver(euf::solver& ctx, family_id fid);
@@ -75,6 +77,7 @@ namespace q {
         euf::theory_var mk_var(euf::enode* n) override;
         void init_search() override;
         void finalize_model(model& mdl) override;
+        bool is_shared(euf::theory_var v) const override { return true; }
 
         ast_manager& get_manager() { return m; }
         sat::literal_vector const& universal() const { return m_universal; }

src/sat/smt/sat_th.h

@@ -152,7 +152,6 @@ namespace euf {
         sat::literal eq_internalize(expr* a, expr* b);
         sat::literal eq_internalize(enode* a, enode* b) { return eq_internalize(a->get_expr(), b->get_expr()); }
 
-        euf::enode* e_internalize(expr* e); 
         euf::enode* mk_enode(expr* e, bool suppress_args = false);
         expr_ref mk_eq(expr* e1, expr* e2);
         expr_ref mk_var_eq(theory_var v1, theory_var v2) { return mk_eq(var2expr(v1), var2expr(v2)); }
@@ -173,6 +172,7 @@ namespace euf {
         virtual ~th_euf_solver() {}
         virtual theory_var mk_var(enode* n);
         unsigned get_num_vars() const { return m_var2enode.size(); }
+        euf::enode* e_internalize(expr* e); 
         enode* expr2enode(expr* e) const;
         enode* var2enode(theory_var v) const { return m_var2enode[v]; }
         expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); }