From 9df2a183d6972cb408e88a3d3d245d0a2cfe45ce Mon Sep 17 00:00:00 2001
From: Mikolas Janota <mikolas.janota@gmail.com>
Date: Mon, 6 Jun 2016 18:06:45 +0100
Subject: [PATCH] Adding translation to ackr_model_converter.

---
 src/ackermannization/ackr_info.h              | 24 +++++++++++++++----
 src/ackermannization/ackr_model_converter.cpp | 11 ++++++++-
 2 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/src/ackermannization/ackr_info.h b/src/ackermannization/ackr_info.h
index 703f1f3d5..76be45e2b 100644
--- a/src/ackermannization/ackr_info.h
+++ b/src/ackermannization/ackr_info.h
@@ -20,6 +20,7 @@ Revision History:
 #include"ast.h"
 #include"ref.h"
 #include"expr_replacer.h"
+#include"ast_translation.h"
 
 /** \brief
    Information about how a formula is being converted into
@@ -35,7 +36,6 @@ class ackr_info {
     public:
         ackr_info(ast_manager& m)
         : m_m(m)
-        , m_consts(m)
         , m_er(mk_default_expr_replacer(m))
         , m_subst(m_m)
         , m_ref_count(0)
@@ -43,16 +43,20 @@ class ackr_info {
         {}
 
         virtual ~ackr_info() {
-            m_consts.reset();
+            for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) {
+                m_m.dec_ref(i->m_key);
+                m_m.dec_ref(i->m_value);
+            }
         }
 
         inline void set_abstr(app* term, app* c) {
             SASSERT(!m_sealed);
-            SASSERT(c);
+            SASSERT(c && term);
             m_t2c.insert(term,c);
             m_c2t.insert(c->get_decl(),term);
             m_subst.insert(term, c);
-            m_consts.push_back(c);
+            m_m.inc_ref(term);
+            m_m.inc_ref(c);
         }
 
         inline void abstract(expr * e, expr_ref& res) {
@@ -77,6 +81,17 @@ class ackr_info {
             m_er->set_substitution(&m_subst);
         }
 
+        virtual ackr_info * translate(ast_translation & translator) {
+            ackr_info * const retv = alloc(ackr_info, translator.to());
+            for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) {
+                app * const k = translator(i->m_key);
+                app * const v = translator(i->m_value);
+                retv->set_abstr(k, v);
+            }
+            if (m_sealed) retv->seal();
+            return retv;
+        }
+
         //
         // Reference counting
         //
@@ -94,7 +109,6 @@ class ackr_info {
 
         t2ct m_t2c; // terms to constants
         c2tt m_c2t; // constants to terms (inversion of m_t2c)
-        expr_ref_vector m_consts; // the constants introduced during abstraction
 
         // replacer and substitution used to compute abstractions
         scoped_ptr<expr_replacer> m_er;
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index eb24ee927..ea4f858ad 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -53,7 +53,16 @@ public:
 
     //void display(std::ostream & out);
 
-    virtual model_converter * translate(ast_translation & translator) {NOT_IMPLEMENTED_YET();}
+    virtual model_converter * translate(ast_translation & translator) {
+        ackr_info_ref retv_info = info->translate(translator);
+        if (fixed_model) {
+            model_ref retv_mod_ref = abstr_model->translate(translator);
+            return alloc(ackr_model_converter, translator.to(), retv_info, retv_mod_ref);
+        }
+        else {
+            return alloc(ackr_model_converter, translator.to(), retv_info);
+        }
+    }
 protected:
     ast_manager&              m;
     const ackr_info_ref       info;