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

fix bug in array simplification. Codeplex issue 173

Browse source 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
This commit is contained in:
nikolajbjorner 2015-02-19 07:01:55 -08:00
parent 6537390171
commit 7735a40752
1 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -327,18 +327,22 @@ void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr
}
lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) {
bool all_diseq = m_manager.is_unique_value(def) && num_st > 0;
bool all_eq = true;
for (unsigned i = 0; i < num_st; ++i) {
if (st[i][arity] == def) {
continue;
}
if (m_manager.is_unique_value(st[i][arity]) && m_manager.is_unique_value(def)) {
return l_false;
}
return l_undef;
all_eq &= (st[i][arity] == def);
all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def);
}
return l_true;
if (all_eq) {
return l_true;
}
if (all_diseq) {
return l_false;
}
return l_undef;
}
bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
for (unsigned i = 0; i < num_st; ++i ) {
for (unsigned j = 0; j < arity; ++j) {