From bfeab9cc154dc93547d67aee36e6210f2fa6638c Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 9 Jun 2016 17:49:45 +0100
Subject: [PATCH] Added facilities for hiding UFs in smt::model_generator

---
 src/smt/smt_model_generator.cpp | 7 +++++--
 src/smt/smt_model_generator.h   | 3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 21a310a42..b9c1ac453 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include"smt_context.h"
 #include"smt_model_generator.h"
 #include"proto_model.h"
+#include"ref_util.h"
 #include"for_each_expr.h"
 #include"ast_ll_pp.h"
 #include"ast_pp.h"
@@ -36,6 +37,7 @@ namespace smt {
     }
 
     model_generator::~model_generator() {
+        dec_ref_collection_values(m_manager, m_hidden_ufs);
     }
 
     void model_generator::reset() {
@@ -386,6 +388,7 @@ namespace smt {
             enode * n = *it3;
             if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
                 func_decl * d = n->get_owner()->get_decl();
+                if (m_hidden_ufs.contains(d)) continue;
                 expr * val    = get_value(n);
                 m_model->register_decl(d, val);
             }
@@ -404,9 +407,9 @@ namespace smt {
     */
     bool model_generator::include_func_interp(func_decl * f) const {
         family_id fid = f->get_family_id();
-        if (fid == null_family_id) return true;
+        if (fid == null_family_id) return !m_hidden_ufs.contains(f); 
         if (fid == m_manager.get_basic_family_id()) return false;
-        theory * th   = m_context->get_theory(fid);
+        theory * th = m_context->get_theory(fid);
         if (!th) return true;
         return th->include_func_interp(f);
     }
diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h
index 6017176e5..07f508e69 100644
--- a/src/smt/smt_model_generator.h
+++ b/src/smt/smt_model_generator.h
@@ -182,6 +182,7 @@ namespace smt {
         obj_map<enode, app *>         m_root2value;
         ast_ref_vector                m_asts;
         proto_model *                 m_model;
+        obj_hashtable<func_decl>      m_hidden_ufs;
 
         void init_model();
         void mk_bool_model();
@@ -220,6 +221,8 @@ namespace smt {
 
         obj_map<enode, app *> const & get_root2value() const { return m_root2value; }
         app * get_value(enode * n) const;
+
+        void hide(func_decl * f) { m_hidden_ufs.insert_if_not_there(f); m_manager.inc_ref(f); }
     };
 };