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

fix #7584

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-15 13:33:08 -07:00
parent 7c226f40df
commit 0e881e7abb
3 changed files with 40 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/smt/smt_model_generator.cpp
View file

@ -34,7 +34,7 @@ namespace smt {
}
std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx() << "#" << src.get_value()->get_src()->get_id();
else return out << "#" << src.get_enode()->get_owner_id();
}
@ -115,8 +115,11 @@ namespace smt {
SASSERT(proc);
}
else {
TRACE("model", tout << "creating fresh value for #" << mk_pp(r->get_expr(), m) << "\n";);
proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_sort()));
TRACE("model", tout << "creating fresh value for #"
<< r->get_expr_id() << " "
<< mk_bounded_pp(r->get_expr(), m) << " "
<< mk_pp(r->get_sort(), m) << "\n";);
proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_expr(), r->get_sort()));
}
}
else {
@ -181,6 +184,11 @@ namespace smt {
if (already_traversed.contains(s))
return true;
bool visited = true;
TRACE("mg_top_sort", tout << "fresh value of sort " << mk_pp(s, m) << "\n";
for (enode* r : roots)
if (r->get_sort() == s)
tout << mk_pp(r->get_expr(), m) << "\n";
);
for (enode * r : roots) {
if (r->get_sort() != s)
continue;
@ -305,14 +313,21 @@ namespace smt {
}
else {
enode * n = curr.get_enode();
sort* s = n->get_sort();
SASSERT(n->get_root() == n);
tout << mk_pp(n->get_expr(), m) << "\n";
sort * s = n->get_sort();
tout << curr << " " << mk_pp(s, m);
tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
tout << mk_bounded_pp(n->get_expr(), m) << " ";
tout << " is_fresh: " << root2proc[n]->is_fresh() << " - deps: ";
dependencies.reset();
model_value_proc* proc = root2proc[n];
SASSERT(proc);
proc->get_dependencies(dependencies);
for (auto const& d : dependencies)
tout << d << " ";
tout << "\n";
}
}
m_context->display(tout);
// m_context->display(tout);
);
@ -340,10 +355,16 @@ namespace smt {
proc->get_dependencies(dependencies);
for (model_value_dependency const& d : dependencies) {
if (d.is_fresh_value()) {
CTRACE("mg_top_sort", !d.get_value()->get_value(),
tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
SASSERT(d.get_value()->get_value());
dependency_values.push_back(d.get_value()->get_value());
expr* val = d.get_value()->get_value();
CTRACE("mg_top_sort", !val,
tout << "#" << n->get_owner_id() << " " <<
mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
// there is a cyclic dependency for default(A), where A
// is an array of a datatype with the datatype using A.
if (!val)
val = m_model->get_some_value(d.get_value()->get_sort());
SASSERT(val);
dependency_values.push_back(val);
}
else {
enode * child = d.get_enode();
@ -446,8 +467,8 @@ namespace smt {
}
}
extra_fresh_value * model_generator::mk_extra_fresh_value(sort * s) {
extra_fresh_value * r = alloc(extra_fresh_value, s, m_fresh_idx);
extra_fresh_value * model_generator::mk_extra_fresh_value(expr * src, sort* s) {
extra_fresh_value * r = alloc(extra_fresh_value, src, s, m_fresh_idx);
m_fresh_idx++;
m_extra_fresh_values.push_back(r);
return r;

8
src/smt/smt_model_generator.h
View file

@ -76,12 +76,14 @@ namespace smt {
\brief Stub for extra fresh value.
*/
struct extra_fresh_value {
expr* m_src;
sort * m_sort;
unsigned m_idx;
expr * m_value;
expr * m_value = nullptr;
public:
extra_fresh_value(sort * s, unsigned idx):m_sort(s), m_idx(idx), m_value(nullptr) {}
extra_fresh_value(expr * src, sort* s, unsigned idx):m_src(src), m_sort(s), m_idx(idx) {}
sort * get_sort() const { return m_sort; }
expr* get_src() const { return m_src; }
unsigned get_idx() const { return m_idx; }
void set_value(expr * n) { SASSERT(!m_value); m_value = n; }
expr * get_value() const { return m_value; }
@ -220,7 +222,7 @@ namespace smt {
void set_context(context * c) { SASSERT(m_context == 0); m_context = c; }
void register_factory(value_factory * f);
extra_fresh_value * mk_extra_fresh_value(sort * s);
extra_fresh_value * mk_extra_fresh_value(expr * src, sort* s);
model_value_proc * mk_model_value(enode* r);
expr * get_some_value(sort * s);
proto_model & get_model() { SASSERT(m_model); return *m_model; }

2
src/smt/theory_array_base.cpp
View file

@ -998,7 +998,7 @@ namespace smt {
TRACE("array", tout << pp(n, m) << " " << mk_pp(range, m) << " " << range->is_infinite() << "\n";);
if (range->is_infinite())
else_val = TAG(void*, mg.mk_extra_fresh_value(range), 1);
else_val = TAG(void*, mg.mk_extra_fresh_value(n->get_expr(), range), 1);
else
else_val = TAG(void*, mg.get_some_value(range), 0);
m_else_values[r] = else_val;