mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00
Code Activity

fix #4899

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-17 23:03:01 -08:00
parent 11477f1ed1
commit 727095c563
5 changed files with 38 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/model/model.cpp
View file

@ -63,7 +63,7 @@ void model::updt_params(params_ref const & p) {
void model::copy_const_interps(model const & source) {
for (auto const& kv : source.m_interp)
register_decl(kv.m_key, kv.m_value);
register_decl(kv.m_key, kv.m_value.second);
}
void model::copy_func_interps(model const & source) {
@ -168,12 +168,14 @@ model * model::translate(ast_translation & translator) const {
// Translate const interps
for (auto const& kv : m_interp) {
res->register_decl(translator(kv.m_key), translator(kv.m_value));
func_decl_ref d(translator(kv.m_key), translator.to());
expr_ref v(translator(kv.m_value.second), translator.to());
res->register_decl(d, v);
}
// Translate func interps
for (auto const& kv : m_finterp) {
func_interp * fi = kv.m_value;
res->register_decl(translator(kv.m_key), fi->translate(translator));
func_interp* fi = kv.m_value->translate(translator);
res->register_decl(translator(kv.m_key), fi);
}
// Translate usort interps
@ -265,7 +267,7 @@ void model::collect_deps(top_sort& ts) {
ts.insert(kv.m_key, collect_deps(ts, kv.m_value));
}
for (auto const& kv : m_interp) {
ts.insert(kv.m_key, collect_deps(ts, kv.m_value));
ts.insert(kv.m_key, collect_deps(ts, kv.m_value.second));
}
}

24
src/model/model_core.cpp
View file

@ -22,7 +22,7 @@ Revision History:
model_core::~model_core() {
for (auto & kv : m_interp) {
m.dec_ref(kv.m_key);
m.dec_ref(kv.m_value);
m.dec_ref(kv.m_value.second);
}
for (auto & kv : m_finterp) {
@ -56,20 +56,22 @@ void model_core::register_decl(func_decl * d, expr * v) {
TRACE("model", tout << "register " << d->get_name() << "\n";
if (v) tout << mk_pp(v, m) << "\n";
);
auto& value = m_interp.insert_if_not_there(d, nullptr);
if (value == nullptr) {
i_expr v0(0, nullptr);
auto& value = m_interp.insert_if_not_there(d, v0);
if (value == v0) {
// new entry
m_decls.push_back(d);
m_const_decls.push_back(d);
m.inc_ref(d);
m.inc_ref(v);
value = v;
value.second = v;
value.first = m_const_decls.size();
m_decls.push_back(d);
m_const_decls.push_back(d);
}
else {
// replacing entry
m.inc_ref(v);
m.dec_ref(value);
value = v;
m.dec_ref(value.second);
value.second = v;
}
}
@ -104,10 +106,12 @@ void model_core::unregister_decl(func_decl * d) {
if (ec) {
auto k = ec->get_data().m_key;
auto v = ec->get_data().m_value;
m_const_decls[v.first] = m_const_decls.back();
m_interp[m_const_decls.back()].first = v.first;
m_const_decls.pop_back();
m_interp.remove(d);
m_const_decls.erase(d);
m.dec_ref(k);
m.dec_ref(v);
m.dec_ref(v.second);
return;
}

6
src/model/model_core.h
View file

@ -24,7 +24,9 @@ Revision History:
class model_core {
protected:
typedef obj_map<func_decl, expr *> decl2expr;
typedef std::pair<unsigned, expr*> i_expr;
typedef std::pair<unsigned, func_interp*> i_interp;
typedef obj_map<func_decl, i_expr> decl2expr;
typedef obj_map<func_decl, func_interp*> decl2finterp;
ast_manager & m;
unsigned m_ref_count;
@ -43,7 +45,7 @@ public:
unsigned get_num_decls() const { return m_decls.size(); }
func_decl * get_decl(unsigned i) const { return m_decls[i]; }
bool has_interpretation(func_decl * d) const { return m_interp.contains(d) || m_finterp.contains(d); }
expr * get_const_interp(func_decl * d) const { expr * v; return m_interp.find(d, v) ? v : nullptr; }
expr * get_const_interp(func_decl * d) const { i_expr v; return m_interp.find(d, v) ? v.second : nullptr; }
func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : nullptr; }
bool eval(func_decl * f, expr_ref & r) const;

4
src/smt/proto_model/proto_model.cpp
View file

@ -220,7 +220,7 @@ void proto_model::cleanup() {
}
for (unsigned i = 0; i < m_const_decls.size(); ++i) {
func_decl* d = m_const_decls[i];
expr* e = m_interp[d];
expr* e = m_interp[d].second;
expr* r = cleanup_expr(trail, e, found_aux_fs);
if (e != r) {
register_decl(d, r);
@ -385,7 +385,7 @@ model * proto_model::mk_model() {
model * mdl = alloc(model, m);
for (auto const& kv : m_interp) {
mdl->register_decl(kv.m_key, kv.m_value);
mdl->register_decl(kv.m_key, kv.m_value.second);
}
for (auto const& kv : m_finterp) {

12
src/tactic/generic_model_converter.cpp
View file

@ -108,7 +108,17 @@ model_converter * generic_model_converter::translate(ast_translation & translato
ast_manager& to = translator.to();
generic_model_converter * res = alloc(generic_model_converter, to, m_orig.c_str());
for (entry const& e : m_entries) {
res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
func_decl_ref d(translator(e.m_f.get()), to);
switch (e.m_instruction) {
case instruction::HIDE:
res->hide(d);
break;
case instruction::ADD: {
expr_ref def(translator(e.m_def.get()), to);
res->add(d, def);
break;
}
}
}
return res;
}