From 956d7742996d7c33f494bc4bb1ab01091c847c90 Mon Sep 17 00:00:00 2001
From: mikolas <mikolas.janota@gmail.com>
Date: Wed, 27 Jan 2016 16:22:28 +0000
Subject: [PATCH] Detecting OP_BSDIV0, etc. as uninterpreted functions in
 ackermannization.

---
 src/tactic/ackr/ackr_model_converter.cpp    |  7 ++++++-
 src/tactic/ackr/lackr.cpp                   |  2 +-
 src/tactic/ackr/lackr.h                     | 19 +++++++++++++++++++
 src/tactic/ackr/lackr_model_constructor.cpp |  6 ++++++
 4 files changed, 32 insertions(+), 2 deletions(-)

diff --git a/src/tactic/ackr/ackr_model_converter.cpp b/src/tactic/ackr/ackr_model_converter.cpp
index c21a6240c..7967cdb63 100644
--- a/src/tactic/ackr/ackr_model_converter.cpp
+++ b/src/tactic/ackr/ackr_model_converter.cpp
@@ -68,7 +68,12 @@ protected:
 };
 
 void ackr_model_converter::convert(model * source, model * destination) {
-    SASSERT(source->get_num_functions() == 0);
+    //SASSERT(source->get_num_functions() == 0);
+    for (unsigned i = 0; i < source->get_num_functions(); i++) {
+        func_decl * const fd = source->get_function(i);
+        func_interp * const fi = source->get_func_interp(fd);
+        destination->register_decl(fd, fi);
+    }
     convert_constants(source,destination);
     convert_sorts(source,destination);
 }
diff --git a/src/tactic/ackr/lackr.cpp b/src/tactic/ackr/lackr.cpp
index fc36d4e1d..e363b96a2 100644
--- a/src/tactic/ackr/lackr.cpp
+++ b/src/tactic/ackr/lackr.cpp
@@ -177,8 +177,8 @@ void lackr::abstract() {
 
 void lackr::add_term(app* a) {
     if (a->get_num_args() == 0) return;
+    if (!should_ackermannize(a)) return;
     func_decl* const fd = a->get_decl();
-    if (!is_uninterp(a)) return;
     SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a));
     app_set* ts = 0;
     if (!m_fun2terms.find(fd, ts)) {
diff --git a/src/tactic/ackr/lackr.h b/src/tactic/ackr/lackr.h
index b108653ac..3258b9d6c 100644
--- a/src/tactic/ackr/lackr.h
+++ b/src/tactic/ackr/lackr.h
@@ -122,5 +122,24 @@ class lackr {
         // Collect all uninterpreted terms, skipping 0-arity.
         //
         void collect_terms();
+
+        inline bool should_ackermannize(app const * a) const;
 };
+
+inline bool lackr::should_ackermannize(app const * a) const {
+    if (a->get_family_id() == m_bvutil.get_family_id()) {
+        switch (a->get_decl_kind()) {
+        case OP_BSDIV0:
+        case OP_BUDIV0:
+        case OP_BSREM0:
+        case OP_BUREM0:
+        case OP_BSMOD0:
+            return true;
+        default:
+            return is_uninterp(a);
+        }
+    }
+    return (is_uninterp(a));
+}
+
 #endif /* LACKR_H_15079 */
diff --git a/src/tactic/ackr/lackr_model_constructor.cpp b/src/tactic/ackr/lackr_model_constructor.cpp
index ad64fc679..22eb4b40b 100644
--- a/src/tactic/ackr/lackr_model_constructor.cpp
+++ b/src/tactic/ackr/lackr_model_constructor.cpp
@@ -78,6 +78,12 @@ struct lackr_model_constructor::imp {
                     destination->register_usort(s, u.size(), u.c_ptr());
                 }
             }
+            for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) {
+                func_decl * const fd = m_abstr_model->get_function(i);
+                func_interp * const fi = m_abstr_model->get_func_interp(fd);
+                destination->register_decl(fd, fi);
+            }
+
             {
                 const app2val_t::iterator e = m_app2val.end();
                 app2val_t::iterator i = m_app2val.end();