updated dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 1, 2020 · 79162b9 · 79162b9
1 parent c76a452
commit 79162b9
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 7 deletions.
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
@@ -49,7 +49,7 @@ def init_project_def():
     add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core')
     add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
 
-    add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster'], 'sat/smt')
+    add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
     add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
     add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')

diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 
 #include "sat/smt/fpa_solver.h"
+#include "ast/fpa/bv2fpa_converter.h"
 
 namespace fpa {
 
@@ -36,10 +37,8 @@ namespace fpa {
     }
 
     solver::~solver() {
-        dec_ref_map_key_values(m, m_conversions);
-        dec_ref_collection_values(m, m_is_added_to_model);                
-        SASSERT(m_conversions.empty());
-        SASSERT(m_is_added_to_model.empty());
+        dec_ref_map_key_values(m, m_conversions);            
+        SASSERT(m_conversions.empty());        
     }
 
 
@@ -66,7 +65,7 @@ namespace fpa {
             m.inc_ref(e);
             m.inc_ref(res);
 
-            // ctx.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
+            ctx.push(fpa2bv_conversion_trail_elem<euf::solver>(m, m_conversions, e));
         }
         return res;
     }
@@ -476,4 +475,29 @@ namespace fpa {
         return out;
     }
 
+
+    void solver::finalize_model(model& mdl) {
+        model new_model(m);
+
+        bv2fpa_converter bv2fp(m, m_converter);
+
+        obj_hashtable<func_decl> seen;
+        bv2fp.convert_min_max_specials(&mdl, &new_model, seen);
+        bv2fp.convert_uf2bvuf(&mdl, &new_model, seen);
+
+        for (func_decl* f : seen)
+            mdl.unregister_decl(f);
+
+        for (unsigned i = 0; i < new_model.get_num_constants(); i++) {
+            func_decl* f = new_model.get_constant(i);
+            mdl.register_decl(f, new_model.get_const_interp(f));
+        }
+
+        for (unsigned i = 0; i < new_model.get_num_functions(); i++) {
+            func_decl* f = new_model.get_function(i);
+            func_interp* fi = new_model.get_func_interp(f)->copy();
+            mdl.register_decl(f, fi);
+        }
+    }
+
 };
diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h
@@ -36,7 +36,6 @@ namespace fpa {
         bv_util                 & m_bv_util;
         arith_util              & m_arith_util;
         obj_map<expr, expr*>      m_conversions;
-        obj_hashtable<func_decl>  m_is_added_to_model;
 
         bool visit(expr* e) override;
         bool visited(expr* e) override;
@@ -50,6 +49,8 @@ namespace fpa {
         expr* bv2rm_value(expr* b);
         expr* bvs2fpa_value(sort* s, expr* a, expr* b, expr* c);
 
+        void finalize_model(model& mdl);
+
 
     public:
         solver(euf::solver& ctx);