add model.inline_def option to make #2517 happy

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

src/cmd_context/cmd_context.cpp

@@ -1790,7 +1790,9 @@ struct contains_underspecified_op_proc {
     \brief Complete the model if necessary.
 */
 void cmd_context::complete_model(model_ref& md) const {
-    if (gparams::get_value("model.completion") != "true" || !md.get())
+    if (!md.get()) 
+        return;
+    if (gparams::get_value("model.completion") != "true")
         return;
 
     params_ref p;
@@ -2045,6 +2047,8 @@ bool cmd_context::is_model_available(model_ref& md) const {
         has_manager() &&
         (cs_state() == css_sat || cs_state() == css_unknown)) {
         get_check_sat_result()->get_model(md);
+        params_ref p;
+        if (md.get()) md->updt_params(p);
         complete_model(md);
         return md.get() != nullptr;
     }

src/model/model.cpp

@@ -27,12 +27,14 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "ast/for_each_ast.h"
 #include "model/model.h"
+#include "model/model_params.hpp"
 #include "model/model_evaluator.h"
 
 model::model(ast_manager & m):
     model_core(m),
     m_mev(*this),
-    m_cleaned(false) {
+    m_cleaned(false),
+    m_inline(false) {
 }
 
 model::~model() {
@@ -43,6 +45,13 @@ model::~model() {
     }
 }
 
+void model::updt_params(params_ref const & p) {
+    model_params mp(p);
+    m_inline = mp.inline_def();
+    m_mev.updt_params(p); 
+}
+
+
 void model::copy_const_interps(model const & source) {
     for (auto const& kv : source.m_interp) 
         register_decl(kv.m_key, kv.m_value);
@@ -353,6 +362,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) {
     func_interp* fi = get_func_interp(f);
     if (!fi) return false;
     if (fi->get_else() == nullptr) return false;
+    if (m_inline) return true;
     expr* e = fi->get_else();
     obj_hashtable<expr> subs;
     ptr_buffer<expr> todo;

src/model/model.h

@@ -36,6 +36,7 @@ class model : public model_core {
     sort2universe                 m_usort2universe;
     model_evaluator               m_mev;
     bool                          m_cleaned;
+    bool                          m_inline;
     struct value_proc;
 
     struct deps_collector;    
@@ -84,7 +85,7 @@ class model : public model_core {
     void compress();
 
     void set_model_completion(bool f) { m_mev.set_model_completion(f); }
-    void updt_params(params_ref const & p) { m_mev.updt_params(p); }
+    void updt_params(params_ref const & p);
 
     /**
      * evaluation using the model evaluator. Caches results.

src/model/model_params.pyg

@@ -4,6 +4,7 @@ def_module_params('model',
                           ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
                           ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
                           ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
+                          ('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'),
                           ('completion', BOOL, False, 'enable/disable model completion'),
                           ))