From 2165c09defb5a989ba703e9ca05eaf8aa0a1e203 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 13 Sep 2017 19:50:51 +0100
Subject: [PATCH] Improved FPA models of partial theory functions

---
 src/ast/fpa/bv2fpa_converter.cpp | 52 +++++++++++++++++---------------
 1 file changed, 27 insertions(+), 25 deletions(-)

diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index 59f24779e..d3eedbf54 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/src/ast/fpa/bv2fpa_converter.cpp
@@ -120,9 +120,9 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
     res = m_fpa_util.mk_value(fp_val);
 
     TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) <<
-        " " << mk_ismt2_pp(exp, m) <<
-        " " << mk_ismt2_pp(sig, m) << "] == " <<
-        mk_ismt2_pp(res, m) << std::endl;);
+                            " " << mk_ismt2_pp(exp, m) <<
+                            " " << mk_ismt2_pp(sig, m) << "] == " <<
+                            mk_ismt2_pp(res, m) << std::endl;);
     m_fpa_util.fm().del(fp_val);
 
     return res;
@@ -263,7 +263,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
     unsigned arity = bv_f->get_arity();
     func_interp * bv_fi = mc->get_func_interp(bv_f);
 
-    if (bv_fi != 0) {
+    if (bv_fi) {
         fpa_rewriter rw(m);
         expr_ref ai(m);
         result = alloc(func_interp, m, arity);
@@ -384,7 +384,7 @@ void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_mo
         expr * bvval = to_app(val)->get_arg(0);
         expr_ref fv(m);
         fv = convert_bv2rm(mc, to_app(bvval));
-        TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
+        TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;);
         target_model->register_decl(var, fv);
         seen.insert(to_app(bvval)->get_decl());
     }
@@ -455,11 +455,14 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
 
                 // Upon request, add this 'recursive' definition?
                 func_interp * fmv = convert_func_interp(mc, f, it->m_value);
-                unsigned n = fmv->get_arity();
-                expr_ref_vector args(m);
-                for (unsigned i = 0; i < n; i++)
-                    args.push_back(m.mk_var(i, f->get_domain()[i]));
-                fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
+                if (fmv) {
+                    unsigned n = fmv->get_arity();
+                    expr_ref_vector args(m);
+                    for (unsigned i = 0; i < n; i++)
+                        args.push_back(m.mk_var(i, f->get_domain()[i]));
+                    fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr()));
+                    target_model->register_decl(f, fmv);
+                }
             }
             else {
                 func_interp * fmv = convert_func_interp(mc, f, it->m_value);
@@ -554,21 +557,20 @@ bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) {
 
 void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) {
     TRACE("bv2fpa", tout << "BV Model: " << std::endl;
-    for (unsigned i = 0; i < mc->get_num_constants(); i++)
-        tout << mc->get_constant(i)->get_name() << " --> " <<
-        mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
-    for (unsigned i = 0; i < mc->get_num_functions(); i++) {
-        func_decl * f = mc->get_function(i);
-        tout << f->get_name() << "(...) := " << std::endl;
-        func_interp * fi = mc->get_func_interp(f);
-        for (unsigned j = 0; j < fi->num_entries(); j++) {
-            func_entry const * fe = fi->get_entry(j);
-            for (unsigned k = 0; k < f->get_arity(); k++) {
-                tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
+        for (unsigned i = 0; i < mc->get_num_constants(); i++)
+            tout << mc->get_constant(i)->get_name() << " --> " <<
+                    mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl;
+        for (unsigned i = 0; i < mc->get_num_functions(); i++) {
+            func_decl * f = mc->get_function(i);
+            tout << f->get_name() << "(...) := " << std::endl;
+            func_interp * fi = mc->get_func_interp(f);
+            for (unsigned j = 0; j < fi->num_entries(); j++) {
+                func_entry const * fe = fi->get_entry(j);
+                for (unsigned k = 0; k < f->get_arity(); k++)
+                    tout << mk_ismt2_pp(fe->get_arg(k), m) << " ";
+                tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
             }
-            tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl;
-        }
-        tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
-    });
+            tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl;
+        });
 
 }