mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

tidy model generator

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-11 08:52:13 -07:00
parent 5e5f46f0f8
commit 9f2bafbf10
3 changed files with 39 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

71
src/smt/smt_model_generator.cpp
View file

@ -28,6 +28,15 @@ Revision History:
namespace smt { namespace smt {
void fresh_value_proc::get_dependencies(buffer<model_value_dependency>& result) {
result.push_back(model_value_dependency(m_value));
}
std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
else return out << "#" << src.get_enode()->get_owner_id();
}
model_generator::model_generator(ast_manager & m): model_generator::model_generator(ast_manager & m):
m_manager(m), m_manager(m),
m_context(nullptr), m_context(nullptr),
@ -161,20 +170,20 @@ namespace smt {
source2color & colors, source2color & colors,
obj_hashtable<sort> & already_traversed, obj_hashtable<sort> & already_traversed,
svector<source> & todo) { svector<source> & todo) {
if (src.is_fresh_value()) { if (src.is_fresh_value()) {
// there is an implicit dependency between a fresh value stub of sort S and the root enodes of sort S that are not associated with fresh values. // there is an implicit dependency between a fresh value stub of
// sort S and the root enodes of sort S that are not associated with fresh values.
//
sort * s = src.get_value()->get_sort(); sort * s = src.get_value()->get_sort();
if (already_traversed.contains(s)) if (already_traversed.contains(s))
return true; return true;
bool visited = true; bool visited = true;
unsigned sz = roots.size(); for (enode * r : roots) {
for (unsigned i = 0; i < sz; i++) {
enode * r = roots[i];
if (m_manager.get_sort(r->get_owner()) != s) if (m_manager.get_sort(r->get_owner()) != s)
continue; continue;
SASSERT(r == r->get_root()); SASSERT(r == r->get_root());
model_value_proc * proc = nullptr; model_value_proc * proc = root2proc[r];
root2proc.find(r, proc);
SASSERT(proc); SASSERT(proc);
if (proc->is_fresh()) if (proc->is_fresh())
continue; // r is associated with a fresh value... continue; // r is associated with a fresh value...
@ -192,17 +201,12 @@ namespace smt {
enode * n = src.get_enode(); enode * n = src.get_enode();
SASSERT(n == n->get_root()); SASSERT(n == n->get_root());
bool visited = true; bool visited = true;
model_value_proc * proc = nullptr; model_value_proc * proc = root2proc[n];
root2proc.find(n, proc);
SASSERT(proc);
buffer<model_value_dependency> dependencies; buffer<model_value_dependency> dependencies;
proc->get_dependencies(dependencies); proc->get_dependencies(dependencies);
for (model_value_dependency const& dep : dependencies) { for (model_value_dependency const& dep : dependencies) {
visit_child(dep, colors, todo, visited); visit_child(dep, colors, todo, visited);
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> "; TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";);
if (dep.is_fresh_value()) tout << "fresh!" << dep.get_value()->get_idx();
else tout << "#" << dep.get_enode()->get_owner_id();
tout << "\n";);
} }
return visited; return visited;
} }
@ -215,9 +219,7 @@ namespace smt {
svector<source> & todo, svector<source> & todo,
svector<source> & sorted_sources) { svector<source> & sorted_sources) {
TRACE("mg_top_sort", tout << "process source, is_fresh: " << src.is_fresh_value() << " "; TRACE("mg_top_sort", tout << "process source, is_fresh: " << src.is_fresh_value() << " ";
if (src.is_fresh_value()) tout << "fresh!" << src.get_value()->get_idx(); tout << src << ", todo.size(): " << todo.size() << "\n";);
else tout << "#" << src.get_enode()->get_owner_id();
tout << ", todo.size(): " << todo.size() << "\n";);
int color = get_color(colors, src); int color = get_color(colors, src);
SASSERT(color != Grey); SASSERT(color != Grey);
if (color == Black) if (color == Black)
@ -227,17 +229,16 @@ namespace smt {
while (!todo.empty()) { while (!todo.empty()) {
source curr = todo.back(); source curr = todo.back();
TRACE("mg_top_sort", tout << "current source, is_fresh: " << curr.is_fresh_value() << " "; TRACE("mg_top_sort", tout << "current source, is_fresh: " << curr.is_fresh_value() << " ";
if (curr.is_fresh_value()) tout << "fresh!" << curr.get_value()->get_idx(); tout << curr << ", todo.size(): " << todo.size() << "\n";);
else tout << "#" << curr.get_enode()->get_owner_id();
tout << ", todo.size(): " << todo.size() << "\n";);
switch (get_color(colors, curr)) { switch (get_color(colors, curr)) {
case White: case White:
set_color(colors, curr, Grey); set_color(colors, curr, Grey);
visit_children(curr, roots, root2proc, colors, already_traversed, todo); visit_children(curr, roots, root2proc, colors, already_traversed, todo);
break; break;
case Grey: case Grey:
SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo)); // SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
set_color(colors, curr, Black); set_color(colors, curr, Black);
TRACE("mg_top_sort", tout << "append " << curr << "\n";);
sorted_sources.push_back(curr); sorted_sources.push_back(curr);
break; break;
case Black: case Black:
@ -266,18 +267,15 @@ namespace smt {
// topological sort // topological sort
// traverse all extra fresh values... // traverse all extra fresh values...
unsigned sz = m_extra_fresh_values.size(); for (extra_fresh_value * f : m_extra_fresh_values) {
for (unsigned i = 0; i < sz; i++) {
extra_fresh_value * f = m_extra_fresh_values[i];
process_source(source(f), roots, root2proc, colors, already_traversed, todo, sorted_sources); process_source(source(f), roots, root2proc, colors, already_traversed, todo, sorted_sources);
} }
// traverse all enodes that are associated with fresh values... // traverse all enodes that are associated with fresh values...
sz = roots.size(); unsigned sz = roots.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
enode * r = roots[i]; enode * r = roots[i];
model_value_proc * proc = nullptr; model_value_proc * proc = root2proc[r];
root2proc.find(r, proc);
SASSERT(proc); SASSERT(proc);
if (!proc->is_fresh()) if (!proc->is_fresh())
continue; continue;
@ -303,43 +301,38 @@ namespace smt {
TRACE("sorted_sources", TRACE("sorted_sources",
for (source const& curr : sources) { for (source const& curr : sources) {
if (curr.is_fresh_value()) { if (curr.is_fresh_value()) {
tout << "fresh!" << curr.get_value()->get_idx() << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n"; tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
} }
else { else {
enode * n = curr.get_enode(); enode * n = curr.get_enode();
SASSERT(n->get_root() == n); SASSERT(n->get_root() == n);
sort * s = m_manager.get_sort(n->get_owner()); sort * s = m_manager.get_sort(n->get_owner());
tout << "#" << n->get_owner_id() << " " << mk_pp(s, m_manager); tout << curr << " " << mk_pp(s, m_manager);
model_value_proc * proc = 0; tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
root2proc.find(n, proc);
SASSERT(proc);
tout << " is_fresh: " << proc->is_fresh() << "\n";
} }
}); });
for (source const& curr : sources) { for (source const& curr : sources) {
if (curr.is_fresh_value()) { if (curr.is_fresh_value()) {
sort * s = curr.get_value()->get_sort(); sort * s = curr.get_value()->get_sort();
TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " : " << mk_pp(s, m_manager) << "\n";); TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m_manager) << "\n";);
expr * val = m_model->get_fresh_value(s); expr * val = m_model->get_fresh_value(s);
TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " := #" << (val == 0 ? UINT_MAX : val->get_id()) << "\n";); TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";);
m_asts.push_back(val); m_asts.push_back(val);
curr.get_value()->set_value(val); curr.get_value()->set_value(val);
} }
else { else {
enode * n = curr.get_enode(); enode * n = curr.get_enode();
SASSERT(n->get_root() == n); SASSERT(n->get_root() == n);
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << "\n";); TRACE("mg_top_sort", tout << curr << "\n";);
dependencies.reset(); dependencies.reset();
dependency_values.reset(); dependency_values.reset();
model_value_proc * proc = nullptr; model_value_proc * proc = root2proc[n];
VERIFY(root2proc.find(n, proc));
SASSERT(proc); SASSERT(proc);
proc->get_dependencies(dependencies); proc->get_dependencies(dependencies);
for (model_value_dependency const& d : dependencies) { for (model_value_dependency const& d : dependencies) {
if (d.is_fresh_value()) { if (d.is_fresh_value()) {
CTRACE("mg_top_sort", !d.get_value()->get_value(), CTRACE("mg_top_sort", !d.get_value()->get_value(),
tout << "#" << n->get_owner_id() << " -> "; tout << "#" << n->get_owner_id() << " -> " << d << "\n";);
tout << "fresh!" << d.get_value()->get_idx() << "\n";);
SASSERT(d.get_value()->get_value()); SASSERT(d.get_value()->get_value());
dependency_values.push_back(d.get_value()->get_value()); dependency_values.push_back(d.get_value()->get_value());
} }

10
src/smt/smt_model_generator.h
View file

@ -100,14 +100,16 @@ namespace smt {
extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value
}; };
public: public:
model_value_dependency():m_fresh(true), m_value(nullptr) {} model_value_dependency():m_fresh(true), m_value(nullptr) { }
model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {} explicit model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
model_value_dependency(extra_fresh_value * v):m_fresh(true), m_value(v) {} explicit model_value_dependency(extra_fresh_value * v) :m_fresh(true), m_value(v) { SASSERT(v); }
bool is_fresh_value() const { return m_fresh; } bool is_fresh_value() const { return m_fresh; }
enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; } enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; }
extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; } extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; }
}; };
std::ostream& operator<<(std::ostream& out, model_value_dependency const& d);
typedef model_value_dependency source; typedef model_value_dependency source;
struct source_hash_proc { struct source_hash_proc {
@ -166,7 +168,7 @@ namespace smt {
extra_fresh_value * m_value; extra_fresh_value * m_value;
public: public:
fresh_value_proc(extra_fresh_value * v):m_value(v) {} fresh_value_proc(extra_fresh_value * v):m_value(v) {}
void get_dependencies(buffer<model_value_dependency> & result) override { result.push_back(m_value); } void get_dependencies(buffer<model_value_dependency> & result) override;
app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); } app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); }
bool is_fresh() const override { return true; } bool is_fresh() const override { return true; }
}; };

1
src/smt/theory_datatype.cpp
View file

@ -636,6 +636,7 @@ namespace smt {
void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); } void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
~datatype_value_proc() override {} ~datatype_value_proc() override {}
void get_dependencies(buffer<model_value_dependency> & result) override { void get_dependencies(buffer<model_value_dependency> & result) override {
for (model_value_dependency& d : m_dependencies) { }
result.append(m_dependencies.size(), m_dependencies.c_ptr()); result.append(m_dependencies.size(), m_dependencies.c_ptr());
} }
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override { app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {