From ccc170a06e9f5b8dfae559d8640e908155b23fc1 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 2 Mar 2019 16:42:18 +0000
Subject: [PATCH] model evaluator: cleanup cache when model_eval param changes

---
 src/api/api_model.cpp                |  1 -
 src/model/model_evaluator.cpp        | 27 +++++++++++++++------------
 src/model/model_evaluator_params.pyg |  1 -
 3 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 0937e668e..8fba5e9f6 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -15,7 +15,6 @@ Author:
 Revision History:
 
 --*/
-#include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 968aca51f..eb8f718fb 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -36,7 +36,7 @@ Revision History:
 #include "model/model_smt2_pp.h"
 #include "ast/rewriter/var_subst.h"
 
-
+namespace {
 struct evaluator_cfg : public default_rewriter_cfg {
     ast_manager &                   m;
     model_core &                    m_model;
@@ -53,7 +53,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
     unsigned long long              m_max_memory;
     unsigned                        m_max_steps;
     bool                            m_model_completion;
-    bool                            m_cache;
     bool                            m_array_equalities;
     bool                            m_array_as_stores;
     obj_map<func_decl, expr*>       m_def_cache;
@@ -91,7 +90,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
         model_evaluator_params p(_p);
         m_max_memory       = megabytes_to_bytes(p.max_memory());
         m_max_steps        = p.max_steps();
-        m_cache            = p.cache();
         m_model_completion = p.completion();
         m_array_equalities = p.array_equalities();
         m_array_as_stores  = p.array_as_stores();
@@ -328,8 +326,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return num_steps > m_max_steps;
     }
 
-    bool cache_results() const { return m_cache; }
-
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
         TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";);
         if (a == b) {
@@ -544,8 +540,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return true;
     }
 };
-
-template class rewriter_tpl<evaluator_cfg>;
+}
 
 struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
     evaluator_cfg m_cfg;
@@ -557,6 +552,11 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
         set_cancel_check(false);
     }
     void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
+    void reset() {
+        rewriter_tpl<evaluator_cfg>::reset();
+        m_cfg.reset();
+        m_cfg.m_def_cache.reset();
+    }
 };
 
 model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
@@ -580,7 +580,10 @@ void model_evaluator::get_param_descrs(param_descrs & r) {
 }
 
 void model_evaluator::set_model_completion(bool f) {
-    m_imp->cfg().m_model_completion = f;
+    if (m_imp->cfg().m_model_completion != f) {
+        reset();
+        m_imp->cfg().m_model_completion = f;
+    }
 }
 
 bool model_evaluator::get_model_completion() const {
@@ -597,8 +600,8 @@ unsigned model_evaluator::get_num_steps() const {
 
 void model_evaluator::cleanup(params_ref const & p) {
     model_core & md = m_imp->cfg().m_model;
-    dealloc(m_imp);
-    m_imp = alloc(imp, md, p);
+    m_imp->~imp();
+    new (m_imp) imp(md, p);
 }
 
 void model_evaluator::reset(params_ref const & p) {
@@ -607,8 +610,8 @@ void model_evaluator::reset(params_ref const & p) {
 }
 
 void model_evaluator::reset(model_core &model, params_ref const& p) {
-    dealloc(m_imp);
-    m_imp = alloc(imp, model, p);
+    m_imp->~imp();
+    new (m_imp) imp(model, p);
 }
 
 
diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg
index 509b3e7c7..890e19cfe 100644
--- a/src/model/model_evaluator_params.pyg
+++ b/src/model/model_evaluator_params.pyg
@@ -3,7 +3,6 @@ def_module_params('model_evaluator',
                   params=(max_memory_param(),
                           max_steps_param(),
                           ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
-                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
                           ('array_equalities', BOOL, True, 'evaluate array equalities'),
                           ('array_as_stores', BOOL, True, 'return array as a set of stores'),
                           ))