mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fixed slicing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-26 15:44:54 -08:00
parent 8b8fb74fd6
commit c513f7e9c2
2 changed files with 28 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

68
src/muz_qe/dl_mk_slice.cpp
View file

@ -429,6 +429,29 @@ namespace datalog {
}
}
void mk_slice::filter_unique_vars(rule& r) {
//
// Variables that occur in multiple uinterpreted predicates are not sliceable.
//
uint_set used_vars;
for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
app* p = r.get_tail(j);
for (unsigned i = 0; i < p->get_num_args(); ++i) {
expr* v = p->get_arg(i);
if (is_var(v)) {
unsigned vi = to_var(v)->get_idx();
add_var(vi);
if (used_vars.contains(vi)) {
m_var_is_sliceable[vi] = false;
}
else {
used_vars.insert(vi);
}
}
}
}
}
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r);
for (unsigned j = 0; j < conjs.size(); ++j) {
@ -475,6 +498,7 @@ namespace datalog {
}
}
}
filter_unique_vars(r);
//
// Collect the set of variables that are solved.
// Collect the occurrence count of the variables per conjunct.
@ -750,51 +774,11 @@ namespace datalog {
m_solved_vars.reset();
#if 0
uint_set used_vars;
expr_ref b(m);
TBD: buggy code:
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
if (is_eq(e, v, b)) {
if (v >= m_solved_vars.size()) {
m_solved_vars.resize(v+1);
}
if (v < sorts.size() && sorts[v]) {
TRACE("dl", tout << "already bound " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
}
else if (m_solved_vars[v].get()) {
TRACE("dl", tout << "already solved " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
add_free_vars(used_vars, m_solved_vars[v].get());
used_vars.insert(v);
}
else {
TRACE("dl", tout << "new solution " << mk_pp(e, m) << "\n";);
m_solved_vars[v] = b;
}
}
else {
TRACE("dl", tout << "not solved " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
}
tail.push_back(to_app(e));
}
#endif
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
#if 0
if (false && is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) {
TRACE("dl", tout << "removing conjunct: " << mk_pp(e, m) << "\n";);
// skip conjunct
}
#endif
tail.push_back(to_app(e));
}
new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);
rm.fix_unbound_vars(new_rule, false);

2
src/muz_qe/dl_mk_slice.h
View file

@ -89,6 +89,8 @@ namespace datalog {
void update_predicate(app* p, app_ref& q);
void filter_unique_vars(rule& r);
void solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars);
public: