stubs for model finder

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

src/model/model.cpp

@@ -502,6 +502,17 @@ void model::remove_decls(ptr_vector<func_decl> & decls, func_decl_set const & s)
     decls.shrink(j);
 }
 
+expr_ref model::unfold_as_array(expr* e) {
+    func_decl* f = nullptr;
+    array_util autil(m);
+    if (!autil.is_as_array(e, f))
+        return expr_ref(e, m);
+    auto* fi = get_func_interp(f);
+    if (!fi)
+        return expr_ref(e, m);
+    return fi->get_array_interp(f);
+}
+
 
 expr_ref model::get_inlined_const_interp(func_decl* f) {
     expr* v = get_const_interp(f);

src/model/model.h

@@ -78,6 +78,7 @@ public:
     bool has_uninterpreted_sort(sort * s) const;
 
     expr_ref get_inlined_const_interp(func_decl* f);
+    expr_ref unfold_as_array(expr* e);
 
     //
     // Primitives for building models

src/sat/smt/CMakeLists.txt

@@ -24,6 +24,7 @@ z3_add_component(sat_smt
     euf_relevancy.cpp
     euf_solver.cpp
     q_mbi.cpp
+    q_model_finder.cpp
     q_solver.cpp
     sat_dual_solver.cpp
     sat_th.cpp

src/sat/smt/q_mbi.cpp

@@ -25,8 +25,8 @@ Author:
 
 namespace q {
 
-    mbqi::mbqi(euf::solver& ctx, solver& s):
-        ctx(ctx), qs(s), m(s.get_manager()), m_fresh_trail(m)  {}
+    mbqi::mbqi(euf::solver& ctx, solver& s): 
+        ctx(ctx), qs(s), m(s.get_manager()), m_model_finder(ctx), m_fresh_trail(m)  {}
 
 
     void mbqi::restrict_to_universe(expr * sk, ptr_vector<expr> const & universe) {
@@ -86,10 +86,10 @@ namespace q {
     }
     
     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);
+        expr_ref_vector vars(m);
+        expr_ref body = specialize(q, vars);        
         m_solver->assert_expr(body);
         lbool r = m_solver->check_sat(0, nullptr);
         if (r == l_undef)
@@ -99,8 +99,8 @@ namespace q {
         model_ref mdl0, mdl1;        
         m_solver->get_model(mdl0);       
         expr_ref proj(m);
-        auto add_projection = [&](model& mdl) {
-            proj = project(*mdl1, q, vars);
+        auto add_projection = [&](model& mdl, bool inv) {
+            proj = project(mdl, q, vars, inv);
             if (!proj)
                 return;
             if (is_forall(q))
@@ -110,10 +110,10 @@ namespace q {
         };
         bool added = false;
 #if 0
-        restrict_vars_to_instantiation_sets(mdl0, q, vars);
+        m_model_finder.restrict_instantiations(*m_solver, *mdl0, q, vars);
         for (unsigned i = 0; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) {
             m_solver->get_model(mdl1);
-            add_projection(*mdl1);
+            add_projection(*mdl1, true);
             if (!proj)
                 break;
             added = true;
@@ -121,7 +121,7 @@ namespace q {
         }
 #endif
         if (!added) {
-            add_projection(*mdl0);
+            add_projection(*mdl0, false);
             added = proj;
         }
         return added ? l_false : l_undef;
@@ -146,18 +146,18 @@ namespace q {
         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.
+    * 
+    * - eliminate as-array terms, use lambda
+    * - have mode with inv-term from model-finder
     */
-    expr_ref mbqi::basic_project(model& mdl, quantifier* q, expr_ref_vector& vars) {
+    expr_ref mbqi::project(model& mdl, quantifier* q, expr_ref_vector& vars, bool inv) {
         unsigned sz = q->get_num_decls();
+        unsigned max_generation = 0;
         expr_ref_vector vals(m);
         vals.resize(sz, nullptr);
         auto const& v2r = ctx.values2root();
@@ -167,9 +167,13 @@ namespace q {
             expr_ref val(mdl.get_some_const_interp(f), m);
             if (!val)
                 return expr_ref(m);
-            expr* t = nullptr;
+            val = mdl.unfold_as_array(val);
+            if (!val)
+                return expr_ref(m);
+            if (inv)
+                vals[i] = m_model_finder.inv_term(mdl, q, i, val, max_generation);            
             euf::enode* r = nullptr;
-            if (v2r.find(val, r))
+            if (!vals.get(i) && v2r.find(val, r))
                 vals[i] = choose_term(r);
             if (!vals.get(i))
                 vals[i] = replace_model_value(val);

src/sat/smt/q_mbi.h

@@ -16,8 +16,10 @@ Author:
 --*/
 #pragma once
 
-#include "sat/smt/sat_th.h"
 #include "solver/solver.h"
+#include "sat/smt/sat_th.h"
+#include "sat/smt/q_model_finder.h"
+
 
 namespace euf {
     class solver;
@@ -31,6 +33,7 @@ namespace q {
         euf::solver&                           ctx;
         solver&                                qs;
         ast_manager&                           m;
+        model_finder                           m_model_finder;
         model_ref                              m_model;
         ref<::solver>                          m_solver;
         obj_map<sort, obj_hashtable<expr>*>    m_fresh;
@@ -44,8 +47,7 @@ namespace q {
         expr_ref choose_term(euf::enode* r);
         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);
+        expr_ref project(model& mdl, quantifier* q, expr_ref_vector& vars, bool inv);
         void init_model();
         void init_solver();
 

src/sat/smt/q_model_finder.cpp

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_model_finder.cpp
+
+Abstract:
+
+    Model-based quantifier instantiation model-finder plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-29
+
+Notes:
+   
+    Derives from smt/smt_model_finder.cpp
+
+--*/
+
+#include "sat/smt/q_model_finder.h"
+#include "sat/smt/euf_solver.h"
+
+
+namespace q {
+
+    model_finder::model_finder(euf::solver&):
+        ctx(ctx), m(ctx.get_manager()) {}
+
+    expr_ref model_finder::inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation) {
+        return expr_ref(value, m);
+    }
+
+    void model_finder::restrict_instantiations(::solver& s, model& mdl, quantifier* q, expr_ref_vector const& vars) {
+        
+    }
+
+}

src/sat/smt/q_model_finder.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    q_model_finder.h
+
+Abstract:
+
+    Model-based quantifier instantiation model-finder plugin
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-29
+
+Notes:
+   
+    Derives from smt/smt_model_finder.cpp
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "solver/solver.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace q {
+
+    class model_finder {
+        euf::solver&                           ctx;        
+        ast_manager&                           m;
+
+    public:
+
+        model_finder(euf::solver& ctx);
+
+        expr_ref inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation);
+
+        void restrict_instantiations(::solver& s, model& mdl, quantifier* q, expr_ref_vector const& vars);
+        
+    };
+
+}