q

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

src/sat/smt/CMakeLists.txt

@@ -23,6 +23,8 @@ z3_add_component(sat_smt
     euf_proof.cpp
     euf_relevancy.cpp
     euf_solver.cpp
+    q_mbi.cpp
+    q_solver.cpp
     sat_dual_solver.cpp
     sat_th.cpp
     user_solver.cpp

src/sat/smt/array_axioms.cpp

@@ -89,15 +89,12 @@ namespace array {
         app* select = r.select->get_app();
         SASSERT(a.is_select(select));
         SASSERT(can_beta_reduce(r.n));
-        //std::cout << mk_bounded_pp(child, m) << " " << ctx.is_relevant(child) << " " << mk_bounded_pp(select, m) << "\n";
         if (!ctx.is_relevant(child))
             return false;
         for (unsigned i = 1; i < select->get_num_args(); ++i)
             if (!ctx.is_relevant(select->get_arg(i)))
                 return false;
         TRACE("array", tout << "select-axiom: " << mk_bounded_pp(select, m, 2) << " " << mk_bounded_pp(child, m, 2) << "\n";);
-//        if (r.select->get_arg(0)->get_root() != r.n->get_root())
-//            std::cout << "delayed: " << r.m_delayed << "\n";
         if (get_config().m_array_delay_exp_axiom && r.select->get_arg(0)->get_root() != r.n->get_root() && !r.m_delayed) {
             IF_VERBOSE(11, verbose_stream() << "delay: " << mk_bounded_pp(child, m) << " " << mk_bounded_pp(select, m) << "\n");
             ctx.push(set_delay_bit(*this, idx));

src/sat/smt/array_model.cpp

@@ -88,7 +88,6 @@ namespace array {
 
         for (euf::enode* p : euf::enode_parents(n)) {
             if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) {
-//                std::cout << "parent " << mk_bounded_pp(p->get_expr(), m) << "\n";
                 expr* value = values.get(p->get_root_id());
                 if (!value || value == fi->get_else())
                     continue;

src/sat/smt/array_solver.cpp

@@ -61,6 +61,11 @@ also currently, as a base-line it is eager:
     -------------------------------
     A = B => forall i . M[i] = B[i]
 
+A hypothetical refinement could use some limited HO pattern unification steps.
+For example
+    lambda x y z . Y z y x = lambda x y z . X x z y
+-> Y = lambda x y z . X ....
+
 --*/
 
 #include "ast/ast_ll_pp.h"
@@ -191,17 +196,12 @@ namespace array {
             push_axiom(congruence_axiom(n1, n2));
     }
 
-    void solver::tracked_push(euf::enode_vector& v, euf::enode* n) {
-        v.push_back(n);
-        ctx.push(push_back_trail<euf::solver, euf::enode*, false>(v));
-    }
-
     void solver::add_parent_select(theory_var v_child, euf::enode* select) {
         SASSERT(a.is_select(select->get_expr()));
         SASSERT(m.get_sort(select->get_arg(0)->get_expr()) == m.get_sort(var2expr(v_child)));
 
         v_child = find(v_child);
-        tracked_push(get_var_data(v_child).m_parent_selects, select);
+        ctx.push_vec(get_var_data(v_child).m_parent_selects, select);
         euf::enode* child = var2enode(v_child);
         if (can_beta_reduce(child) && child != select->get_arg(0))
             push_axiom(select_axiom(select, child));
@@ -212,7 +212,7 @@ namespace array {
         auto& d = get_var_data(find(v));
         if (should_set_prop_upward(d))
             set_prop_upward(d);
-        tracked_push(d.m_lambdas, lambda);
+        ctx.push_vec(d.m_lambdas, lambda);
         if (should_set_prop_upward(d)) {
             set_prop_upward(lambda);
             propagate_select_axioms(d, lambda);
@@ -222,7 +222,7 @@ namespace array {
     void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) {
         SASSERT(can_beta_reduce(lambda));
         auto& d = get_var_data(find(v_child));
-        tracked_push(d.m_parent_lambdas, lambda);
+        ctx.push_vec(d.m_parent_lambdas, lambda);
         if (should_set_prop_upward(d))
             propagate_select_axioms(d, lambda);
     }

src/sat/smt/array_solver.h

@@ -211,8 +211,6 @@ namespace array {
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override;
 
-        void tracked_push(euf::enode_vector& v, euf::enode* n);
-
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2) {}

src/sat/smt/euf_solver.h

@@ -215,6 +215,16 @@ namespace euf {
         egraph& get_egraph() { return m_egraph; }
         template <typename C>
         void push(C const& c) { m_trail.push(c); }
+        template <typename V>
+        void push_vec(ptr_vector<V>& vec, V* val) {
+            vec.push_back(val);
+            push(push_back_trail<solver, V*, false>(vec));
+        }
+        template <typename V>
+        void push_vec(svector<V>& vec, V val) {
+            vec.push_back(val);
+            push(push_back_trail<solver, V, false>(vec));
+        }
         euf_trail_stack& get_trail_stack() { return m_trail; }
 
         void updt_params(params_ref const& p);

src/sat/smt/q_mbi.cpp

@@ -0,0 +1,200 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_mbi.cpp
+
+Abstract:
+
+    Model-based quantifier instantiation plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-29
+
+--*/
+#pragma once
+
+#include "ast/ast_trail.h"
+#include "ast/rewriter/var_subst.h"
+#include "sat/smt/sat_th.h"
+#include "sat/smt/q_mbi.h"
+#include "sat/smt/q_solver.h"
+#include "sat/smt/euf_solver.h"
+
+
+namespace q {
+
+    mbqi::mbqi(euf::solver& ctx, solver& s): 
+        ctx(ctx), qs(s), m(s.get_manager())  {}
+
+
+    void mbqi::restrict_to_universe(expr * sk, ptr_vector<expr> const & universe) {
+        SASSERT(!universe.empty());
+        expr_ref_vector eqs(m);
+        for (expr * e : universe) {
+            eqs.push_back(m.mk_eq(sk, e));
+        }
+        expr_ref fml(m.mk_or(eqs), m);
+        m_solver->assert_expr(fml);
+    }
+
+    void mbqi::register_value(expr* e) {
+        sort* s = m.get_sort(e);
+        obj_hashtable<expr>* values = nullptr;
+        if (!m_fresh.find(s, values)) {
+            values = alloc(obj_hashtable<expr>);
+            m_fresh.insert(s, values);
+            m_values.push_back(values);
+        }
+        if (!values->contains(e)) {
+            NOT_IMPLEMENTED_YET();
+#if 0
+            for (expr* b : *values) {
+                m_context.add(m.mk_not(m.mk_eq(e, b)), __FUNCTION__);
+            }
+#endif
+            values->insert(e);
+#if 0
+            m_fresh_trail.push_back(e);
+#endif
+        }
+    }
+
+    // sort -> [ value -> expr ]
+    // for fixed value return expr
+    // new fixed value is distinct from other expr
+    expr_ref mbqi::replace_model_value(expr* e) {
+        if (m.is_model_value(e)) { 
+            register_value(e);
+            expr_ref r(e, m);
+            return r;
+        }
+        if (is_app(e) && to_app(e)->get_num_args() > 0) {
+            expr_ref_vector args(m);
+            for (expr* arg : *to_app(e)) {
+                args.push_back(replace_model_value(arg));
+            }
+            return expr_ref(m.mk_app(to_app(e)->get_decl(), args.size(), args.c_ptr()), m);
+        }
+        return expr_ref(e, m);
+    }
+    
+    lbool mbqi::check_forall(quantifier* q) {
+        expr_ref_vector vars(m);
+        expr_ref body = specialize(q, vars);        
+        init_solver();
+        ::solver::scoped_push _sp(*m_solver);
+        m_solver->assert_expr(body);
+        lbool r = m_solver->check_sat(0, nullptr);
+        if (r == l_undef)
+            return r;
+        if (r == l_false)
+            return l_true;
+        model_ref mdl;        
+        m_solver->get_model(mdl);
+        expr_ref proj = project(*mdl, q, vars);
+        if (!proj)
+            return l_undef;
+        if (is_forall(q))
+            qs.add_clause(~ctx.expr2literal(q), ctx.b_internalize(proj));
+        else
+            qs.add_clause(ctx.expr2literal(q), ~ctx.b_internalize(proj));
+        return l_true;
+    }
+
+    expr_ref mbqi::specialize(quantifier* q, expr_ref_vector& vars) {
+        expr_ref tmp(m);
+        unsigned sz = q->get_num_decls();
+        if (!m_model->eval_expr(q->get_expr(), tmp, true))
+            return expr_ref(m);
+        vars.resize(sz, nullptr);
+        for (unsigned i = 0; i < sz; ++i) {
+            sort* s = q->get_decl_sort(i);
+            vars[i] = m.mk_fresh_const(q->get_decl_name(i), s, false);    
+            if (m_model->has_uninterpreted_sort(s)) 
+                restrict_to_universe(vars.get(i), m_model->get_universe(s));            
+        }
+        var_subst subst(m);
+        expr_ref body = subst(tmp, vars.size(), vars.c_ptr());        
+        if (is_forall(q)) 
+            body = m.mk_not(body);        
+        return body;
+    }
+
+    expr_ref mbqi::project(model& mdl, quantifier* q, expr_ref_vector& vars) {
+        return basic_project(mdl, q, vars);
+    }
+
+    /**
+    * A most rudimentary projection operator that only tries to find proxy terms from the set of existing terms.
+    * Refinements:
+    * - grammar based from MBQI paper 
+    * - quantifier elimination based on projection operators defined in qe.
+    */
+    expr_ref mbqi::basic_project(model& mdl, quantifier* q, expr_ref_vector& vars) {
+        unsigned sz = q->get_num_decls();
+        expr_ref_vector vals(m);
+        vals.resize(sz, nullptr);
+        for (unsigned i = 0; i < sz; ++i) {
+            app* v = to_app(vars.get(i));
+            func_decl* f = v->get_decl();
+            expr_ref val(mdl.get_some_const_interp(f), m);
+            if (!val)
+                return expr_ref(m);
+            expr* t = nullptr;
+            NOT_IMPLEMENTED_YET();
+#if 0
+            if (m_val2term.find(val, m.get_sort(v), t)) {
+                val = t;
+            }
+            else {
+                val = replace_model_value(val);
+            }
+            vals[i] = val;
+#endif
+        }
+        var_subst subst(m);
+        expr_ref body = subst(q->get_expr(), vals.size(), vals.c_ptr());
+        return body;        
+    }
+
+
+    lbool mbqi::operator()() {
+        lbool result = l_true;
+        m_model = nullptr;
+        for (sat::literal lit : qs.m_universal) {
+            quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
+            if (!ctx.is_relevant(q))
+                continue;
+            init_model();
+            switch (check_forall(q)) {
+            case l_false:
+                result = l_false;
+                break;
+            case l_undef:
+                if (result == l_true)
+                    result = l_undef;
+                break;
+            default:
+                break;
+            }
+        }
+        return result;
+    }
+
+    void mbqi::init_model() {
+        if (m_model)
+            return;
+        m_model = alloc(model, m);
+        ctx.update_model(m_model);
+    }
+
+    void mbqi::init_solver() {
+        if (m_solver)
+            return;
+        NOT_IMPLEMENTED_YET();
+    }
+
+}

src/sat/smt/q_mbi.h

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_mbi.h
+
+Abstract:
+
+    Model-based quantifier instantiation plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-29
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "solver/solver.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace q {
+
+    class solver;
+
+    class mbqi {
+        euf::solver&                           ctx;
+        solver&                                qs;
+        ast_manager&                           m;
+        model_ref                              m_model;
+        ref<::solver>                          m_solver;
+        obj_map<sort, obj_hashtable<expr>*>    m_fresh;
+        scoped_ptr_vector<obj_hashtable<expr>> m_values;
+
+        void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe);
+        void register_value(expr* e);
+        expr_ref replace_model_value(expr* e);
+        lbool check_forall(quantifier* q);
+        expr_ref specialize(quantifier* q, expr_ref_vector& vars);
+        expr_ref project(model& mdl, quantifier* q, expr_ref_vector& vars);
+        expr_ref basic_project(model& mdl, quantifier* q, expr_ref_vector& vars);
+        void init_model();
+        void init_solver();
+
+    public:
+
+        mbqi(euf::solver& ctx, solver& s);
+            
+        lbool operator()();
+    };
+
+}

src/sat/smt/q_solver.cpp

@@ -0,0 +1,110 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    a_solver.cpp
+
+Abstract:
+
+    Quantifier solver plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-29
+
+--*/
+#pragma once
+
+#include "ast/rewriter/var_subst.h"
+#include "sat/smt/q_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/sat_th.h"
+
+
+namespace q {
+    
+    solver::solver(euf::solver& ctx):
+        th_euf_solver(ctx, ctx.get_manager().get_family_id("quant")),
+        m_mbqi(ctx, *this)
+    {}
+
+    void solver::asserted(sat::literal l) {
+        expr* e = bool_var2expr(l.var());
+        SASSERT(is_forall(e) || is_exists(e));
+        if (l.sign() == is_forall(e)) {
+            // existential force
+            add_clause(~l, skolemize(to_quantifier(e)));
+        }
+        else {
+            // universal force
+            add_clause(~l, uskolemize(to_quantifier(e)));
+            ctx.push_vec(m_universal, l);
+        }
+    }
+
+    sat::check_result solver::check() {
+        switch (m_mbqi()) {
+        case l_true: return sat::check_result::CR_DONE;
+        case l_false: return sat::check_result::CR_CONTINUE;
+        case l_undef: return sat::check_result::CR_GIVEUP;            
+        }
+        return sat::check_result::CR_GIVEUP;
+    }
+
+    std::ostream& solver::display(std::ostream& out) const {
+        return out;
+    }
+
+    void solver::collect_statistics(statistics& st) const {
+        st.update("quantifier inst", m_stats.m_num_inst);
+    }
+
+    euf::th_solver* solver::clone(sat::solver* s, euf::solver& ctx) {
+        return alloc(solver, ctx);
+    }
+
+    bool solver::unit_propagate() {
+        return false;
+    }
+
+    euf::theory_var solver::mk_var(euf::enode* n) {
+        SASSERT(is_forall(n->get_expr()) || is_exists(n->get_expr()));
+        auto v = euf::th_euf_solver::mk_var(n);
+        ctx.attach_th_var(n, this, v);        
+        return v;
+    }
+
+    sat::literal solver::skolemize(quantifier* q) {
+        sat::literal sk;
+        if (m_skolems.find(q, sk))
+            return sk;        
+        expr_ref tmp(m);
+        expr_ref_vector vars(m);
+        unsigned sz = q->get_num_decls();
+        vars.resize(sz, nullptr);
+        for (unsigned i = 0; i < sz; ++i) {
+            vars[i] = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));    
+        }
+        var_subst subst(m);
+        expr_ref body = subst(q->get_expr(), vars.size(), vars.c_ptr());
+        ctx.get_rewriter()(body);
+        sk = b_internalize(body);
+        if (is_forall(q))
+            sk.neg();
+        m_skolems.insert(q, sk);
+        // TODO find a different way than rely on backtrack stack, e,g., save body/q in ref-counted stack
+        ctx.push(insert_map<euf::solver, skolem_table, quantifier*>(m_skolems, q));
+        return sk;
+    }
+
+    /*
+    * Find initial values to instantiate quantifier with so to make it as hard as possible for solver
+    * to find values to free variables. 
+    */
+    sat::literal solver::uskolemize(quantifier* q) {
+        NOT_IMPLEMENTED_YET();
+        return sat::null_literal;
+    }
+    
+}

src/sat/smt/q_solver.h

@@ -0,0 +1,71 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    a_solver.h
+
+Abstract:
+
+    Quantifier solver plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-29
+
+--*/
+#pragma once
+
+#include "util/obj_hashtable.h"
+#include "ast/ast_trail.h"
+#include "sat/smt/sat_th.h"
+#include "sat/smt/q_mbi.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace q {
+
+    class solver : public euf::th_euf_solver {
+
+        typedef obj_map<quantifier, sat::literal> skolem_table;
+        friend class mbqi;
+
+        struct stats {
+            unsigned m_num_inst;
+            void reset() { memset(this, 0, sizeof(*this)); }
+            stats() { reset(); }
+        };
+
+        stats                  m_stats;
+        mbqi                   m_mbqi;
+
+        skolem_table           m_skolems;
+        sat::literal_vector    m_universal;
+
+        sat::literal skolemize(quantifier* q);
+        sat::literal uskolemize(quantifier* q);
+
+    public:
+
+        solver(euf::solver& ctx);
+        ~solver() override {}
+        bool is_external(sat::bool_var v) override { return false; }
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {}
+        void asserted(sat::literal l) override;
+        sat::check_result check() override;
+
+        std::ostream& display(std::ostream& out) const override;
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }
+        void collect_statistics(statistics& st) const override;
+        euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override;
+        bool unit_propagate() override;
+        sat::literal internalize(expr* e, bool sign, bool root, bool learned) override { UNREACHABLE(); return sat::null_literal; }
+        void internalize(expr* e, bool redundant) override { UNREACHABLE(); }
+        euf::theory_var mk_var(euf::enode* n) override;
+
+        ast_manager& get_manager() { return m; }
+    };
+}