From a8bfab32735449e8553cd39a14ee2db57b82aeca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 29 Aug 2019 12:08:09 -0300
Subject: [PATCH] add model.inline_def option to make #2517 happy

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp |  6 +++++-
 src/model/model.cpp             | 12 +++++++++++-
 src/model/model.h               |  3 ++-
 src/model/model_params.pyg      |  1 +
 4 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f4ddf3523..598c2a1f3 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/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;
     }
diff --git a/src/model/model.cpp b/src/model/model.cpp
index bd327d8b5..44338fbfa 100644
--- a/src/model/model.cpp
+++ b/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;
diff --git a/src/model/model.h b/src/model/model.h
index de31d08aa..81ec27765 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -36,6 +36,7 @@ protected:
     sort2universe                 m_usort2universe;
     model_evaluator               m_mev;
     bool                          m_cleaned;
+    bool                          m_inline;
     struct value_proc;
 
     struct deps_collector;    
@@ -84,7 +85,7 @@ public:
     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.
diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg
index 58337e863..c108d1f34 100644
--- a/src/model/model_params.pyg
+++ b/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'),
                           ))