mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-11-15 20:32:45 -08:00
commit f47671931f
1 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/muz/transforms/dl_mk_slice.cpp
View file

@ -426,8 +426,8 @@ namespace datalog {
bool change = true; bool change = true;
while (change) { while (change) {
change = false; change = false;
for (unsigned i = 0; i < src.get_num_rules(); ++i) { for (rule* r : src) {
change = prune_rule(*src.get_rule(i)) || change; change = prune_rule(*r) || change;
} }
} }
} }
@ -457,18 +457,19 @@ namespace datalog {
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) { void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r); expr_ref_vector conjs = get_tail_conjs(r);
for (unsigned j = 0; j < conjs.size(); ++j) { for (expr * e : conjs) {
expr* e = conjs[j].get();
expr_ref r(m); expr_ref r(m);
unsigned v; unsigned v;
if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) { if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";); TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
add_var(v); add_var(v);
if (!m_solved_vars[v].get()) { if (!m_solved_vars[v].get()) {
TRACE("dl", tout << v << " is solved\n";);
add_free_vars(parameter_vars, r); add_free_vars(parameter_vars, r);
m_solved_vars[v] = r; m_solved_vars[v] = r;
} }
else { else {
TRACE("dl", tout << v << " is used\n";);
// variables can only be solved once. // variables can only be solved once.
add_free_vars(used_vars, e); add_free_vars(used_vars, e);
add_free_vars(used_vars, m_solved_vars[v].get()); add_free_vars(used_vars, m_solved_vars[v].get());
@ -508,10 +509,9 @@ namespace datalog {
// //
uint_set used_vars, parameter_vars; uint_set used_vars, parameter_vars;
solve_vars(r, used_vars, parameter_vars); solve_vars(r, used_vars, parameter_vars);
uint_set::iterator it = used_vars.begin(), end = used_vars.end(); for (unsigned uv : used_vars) {
for (; it != end; ++it) { if (uv < m_var_is_sliceable.size()) {
if (*it < m_var_is_sliceable.size()) { m_var_is_sliceable[uv] = false;
m_var_is_sliceable[*it] = false;
} }
} }
// //
@ -533,6 +533,9 @@ namespace datalog {
if (m_solved_vars[i].get()) { if (m_solved_vars[i].get()) {
m_var_is_sliceable[i] = false; m_var_is_sliceable[i] = false;
} }
if (parameter_vars.contains(i)) {
m_var_is_sliceable[i] = false;
}
} }
else if (is_output) { else if (is_output) {
if (parameter_vars.contains(i)) { if (parameter_vars.contains(i)) {
@ -687,11 +690,9 @@ namespace datalog {
} }
void mk_slice::display(std::ostream& out) { void mk_slice::display(std::ostream& out) {
obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(); for (auto const& kv : m_sliceable) {
obj_map<func_decl, bit_vector>::iterator end = m_sliceable.end(); out << kv.m_key->get_name() << " ";
for (; it != end; ++it) { bit_vector const& bv = kv.m_value;
out << it->m_key->get_name() << " ";
bit_vector const& bv = it->m_value;
for (unsigned i = 0; i < bv.size(); ++i) { for (unsigned i = 0; i < bv.size(); ++i) {
out << (bv.get(i)?"1":"0"); out << (bv.get(i)?"1":"0");
} }