From 7ddd2856c8f7bcac549d2472d0b733296a759dfe Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 5 Feb 2016 15:22:37 +0000
Subject: [PATCH] Added is_considered_uninterpreted() to decl_plugins.

---
 src/ast/arith_decl_plugin.h   | 19 +++++++++++++++++++
 src/ast/ast.h                 |  2 ++
 src/ast/bv_decl_plugin.h      | 32 ++++++++++++++++----------------
 src/model/model_evaluator.cpp |  2 +-
 4 files changed, 38 insertions(+), 17 deletions(-)

diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index dd48ef727..25356a667 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -211,6 +211,25 @@ public:
 
     virtual expr * get_some_value(sort * s);
 
+    virtual bool is_considered_uninterpreted(func_decl * f) {
+        if (f->get_family_id() != get_family_id())
+            return false;
+        switch (f->get_decl_kind())
+        {
+        case OP_0_PW_0_INT:
+        case OP_0_PW_0_REAL:
+        case OP_NEG_ROOT:
+        case OP_DIV_0:
+        case OP_IDIV_0:
+        case OP_MOD_0:
+        case OP_U_ASIN:
+        case OP_U_ACOS:
+            return true;
+        default:
+            return false;
+        }
+        return false;
+    }
 };
 
 /**
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 77dd68372..0dba6039c 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -992,6 +992,8 @@ public:
     // Event handlers for deleting/translating PARAM_EXTERNAL
     virtual void del(parameter const & p) {}
     virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; }
+
+    virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
 };
 
 // -----------------------------------
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index a4a0b1f57..563622338 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -266,6 +266,22 @@ public:
     virtual bool are_distinct(app* a, app* b) const;
 
     virtual expr * get_some_value(sort * s);
+
+    virtual bool is_considered_uninterpreted(func_decl * f) {
+        if (f->get_family_id() != get_family_id())
+            return false;
+        switch (f->get_decl_kind()) {
+        case OP_BSDIV0:
+        case OP_BUDIV0:
+        case OP_BSREM0:
+        case OP_BUREM0:
+        case OP_BSMOD0:
+            return true;
+        default:
+            return false;
+        }
+        return false;
+    }
 };
 
 class bv_recognizers {
@@ -353,22 +369,6 @@ public:
     rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
     bool has_sign_bit(rational const & n, unsigned bv_size) const;
     bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
-
-    bool is_considered_uninterpreted(func_decl * f) {
-        if (f->get_family_id() != get_family_id())
-            return false;
-        switch (f->get_decl_kind()) {
-        case OP_BSDIV0:
-        case OP_BUDIV0:
-        case OP_BSREM0:
-        case OP_BUREM0:
-        case OP_BSMOD0:
-            return true;
-        default:
-            return false;
-        }
-        return false;
-    }
 };
 
 class bv_util : public bv_recognizers {
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 366678cf8..1697b74ed 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -202,7 +202,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         if (m_model_completion &&
             (f->get_family_id() == null_family_id ||
-             m_bv_rw.get_util().is_considered_uninterpreted(f)))
+             m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
         {
             sort * s   = f->get_range();
             expr * val = m_model.get_some_value(s);