Skip to content

Commit 0e881e7

Browse files
NikolajBjornerNikolajBjorner
committed
fix #7584 
1 parent 7c226f4 commit 0e881e7

File tree

3 files changed

+40
-17
lines changed

3 files changed

+40
-17
lines changed

‎src/smt/smt_model_generator.cpp

+34-13
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ namespace smt {
3434
}
3535

3636
std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
37-
if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
37+
if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx() << "#" << src.get_value()->get_src()->get_id();
3838
else return out << "#" << src.get_enode()->get_owner_id();
3939
}
4040

@@ -115,8 +115,11 @@ namespace smt {
115115
SASSERT(proc);
116116
}
117117
else {
118-
TRACE("model", tout << "creating fresh value for #" << mk_pp(r->get_expr(), m) << "\n";);
119-
proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_sort()));
118+
TRACE("model", tout << "creating fresh value for #"
119+
<< r->get_expr_id() << " "
120+
<< mk_bounded_pp(r->get_expr(), m) << " "
121+
<< mk_pp(r->get_sort(), m) << "\n";);
122+
proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_expr(), r->get_sort()));
120123
}
121124
}
122125
else {
@@ -181,6 +184,11 @@ namespace smt {
181184
if (already_traversed.contains(s))
182185
return true;
183186
bool visited = true;
187+
TRACE("mg_top_sort", tout << "fresh value of sort " << mk_pp(s, m) << "\n";
188+
for (enode* r : roots)
189+
if (r->get_sort() == s)
190+
tout << mk_pp(r->get_expr(), m) << "\n";
191+
);
184192
for (enode * r : roots) {
185193
if (r->get_sort() != s)
186194
continue;
@@ -305,14 +313,21 @@ namespace smt {
305313
}
306314
else {
307315
enode * n = curr.get_enode();
316+
sort* s = n->get_sort();
308317
SASSERT(n->get_root() == n);
309-
tout << mk_pp(n->get_expr(), m) << "\n";
310-
sort * s = n->get_sort();
311318
tout << curr << " " << mk_pp(s, m);
312-
tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
319+
tout << mk_bounded_pp(n->get_expr(), m) << " ";
320+
tout << " is_fresh: " << root2proc[n]->is_fresh() << " - deps: ";
321+
dependencies.reset();
322+
model_value_proc* proc = root2proc[n];
323+
SASSERT(proc);
324+
proc->get_dependencies(dependencies);
325+
for (auto const& d : dependencies)
326+
tout << d << " ";
327+
tout << "\n";
313328
}
314329
}
315-
m_context->display(tout);
330+
// m_context->display(tout);
316331
);
317332

318333

@@ -340,10 +355,16 @@ namespace smt {
340355
proc->get_dependencies(dependencies);
341356
for (model_value_dependency const& d : dependencies) {
342357
if (d.is_fresh_value()) {
343-
CTRACE("mg_top_sort", !d.get_value()->get_value(),
344-
tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
345-
SASSERT(d.get_value()->get_value());
346-
dependency_values.push_back(d.get_value()->get_value());
358+
expr* val = d.get_value()->get_value();
359+
CTRACE("mg_top_sort", !val,
360+
tout << "#" << n->get_owner_id() << " " <<
361+
mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
362+
// there is a cyclic dependency for default(A), where A
363+
// is an array of a datatype with the datatype using A.
364+
if (!val)
365+
val = m_model->get_some_value(d.get_value()->get_sort());
366+
SASSERT(val);
367+
dependency_values.push_back(val);
347368
}
348369
else {
349370
enode * child = d.get_enode();
@@ -446,8 +467,8 @@ namespace smt {
446467
}
447468
}
448469

449-
extra_fresh_value * model_generator::mk_extra_fresh_value(sort * s) {
450-
extra_fresh_value * r = alloc(extra_fresh_value, s, m_fresh_idx);
470+
extra_fresh_value * model_generator::mk_extra_fresh_value(expr * src, sort* s) {
471+
extra_fresh_value * r = alloc(extra_fresh_value, src, s, m_fresh_idx);
451472
m_fresh_idx++;
452473
m_extra_fresh_values.push_back(r);
453474
return r;

‎src/smt/smt_model_generator.h

+5-3
Original file line numberDiff line numberDiff line change
@@ -76,12 +76,14 @@ namespace smt {
7676
\brief Stub for extra fresh value.
7777
*/
7878
struct extra_fresh_value {
79+
expr* m_src;
7980
sort * m_sort;
8081
unsigned m_idx;
81-
expr * m_value;
82+
expr * m_value = nullptr;
8283
public:
83-
extra_fresh_value(sort * s, unsigned idx):m_sort(s), m_idx(idx), m_value(nullptr) {}
84+
extra_fresh_value(expr * src, sort* s, unsigned idx):m_src(src), m_sort(s), m_idx(idx) {}
8485
sort * get_sort() const { return m_sort; }
86+
expr* get_src() const { return m_src; }
8587
unsigned get_idx() const { return m_idx; }
8688
void set_value(expr * n) { SASSERT(!m_value); m_value = n; }
8789
expr * get_value() const { return m_value; }
@@ -220,7 +222,7 @@ namespace smt {
220222
void set_context(context * c) { SASSERT(m_context == 0); m_context = c; }
221223

222224
void register_factory(value_factory * f);
223-
extra_fresh_value * mk_extra_fresh_value(sort * s);
225+
extra_fresh_value * mk_extra_fresh_value(expr * src, sort* s);
224226
model_value_proc * mk_model_value(enode* r);
225227
expr * get_some_value(sort * s);
226228
proto_model & get_model() { SASSERT(m_model); return *m_model; }

‎src/smt/theory_array_base.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -998,7 +998,7 @@ namespace smt {
998998

999999
TRACE("array", tout << pp(n, m) << " " << mk_pp(range, m) << " " << range->is_infinite() << "\n";);
10001000
if (range->is_infinite())
1001-
else_val = TAG(void*, mg.mk_extra_fresh_value(range), 1);
1001+
else_val = TAG(void*, mg.mk_extra_fresh_value(n->get_expr(), range), 1);
10021002
else
10031003
else_val = TAG(void*, mg.get_some_value(range), 0);
10041004
m_else_values[r] = else_val;

0 commit comments

Comments
 (0)