mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

updated dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-01 08:11:55 -07:00
parent c76a45276b
commit 79162b96f3
3 changed files with 32 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_project.py
View file

@ -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')

34
src/sat/smt/fpa_solver.cpp
View file

@ -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);
}
}
};

3
src/sat/smt/fpa_solver.h
View file

@ -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);