mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Fix mk_distict in term_graph

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-14 16:02:19 -07:00
parent 2a6b7e5482
commit 87715620d9
1 changed files with 26 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/qe/qe_term_graph.cpp
View file

@ -28,6 +28,13 @@ Notes:
namespace qe {
namespace {
struct sort_lt_proc {
bool operator()(const expr* a, const expr *b) const {
return get_sort(a)->get_id() < get_sort(b)->get_id();
}
};
}
namespace is_pure_ns {
struct found{};
struct proc {
@ -760,15 +767,29 @@ namespace qe {
val2rep.insert(val, rep);
}
}
// TBD: this ignores types, need one use of 'distinct' per sort.
// TBD: probably ignore distinct on values
// TBD: ignore distinct on Booleans
ptr_buffer<expr> reps;
for (auto &kv : val2rep) {
reps.push_back(kv.m_value);
std::cout << mk_pp(kv.m_value, m) << "\n";
expr *val = kv.m_value;
if (!m.is_unique_value(val))
reps.push_back(kv.m_value);
}
if (reps.size() <= 1) return;
// -- sort representatives, call mk_distinct on any range
// -- of the same sort longer than 1
std::sort(reps.c_ptr(), reps.c_ptr() + reps.size(), sort_lt_proc());
unsigned i = 0;
unsigned sz = res.size();
while (i < sz) {
sort* last_sort = get_sort(reps.get(i));
unsigned j = i + 1;
while (j < sz && last_sort == get_sort(reps.get(j))) {++j;}
if (j - i > 1)
res.push_back(m.mk_distinct(j - i, reps.c_ptr() + i));
i = j;
}
// res.push_back(m.mk_distinct(reps.size(), reps.c_ptr()));
}
public: