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

fixing #2378

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-12 14:21:22 +01:00
parent be72accaf5
commit 84990ffa27
5 changed files with 79 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -1119,6 +1119,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
}
std::ostringstream buffer;
buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
INVOKE_DEBUGGER();
throw ast_exception(buffer.str());
}

93
src/ast/rewriter/array_rewriter.cpp
View file

@ -539,53 +539,75 @@ void array_rewriter::mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls)
}
}
bool array_rewriter::has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices) {
bool array_rewriter::has_index_set(expr* e, expr_ref& else_case, vector<expr_ref_vector>& stores) {
expr_ref_vector args(m());
expr_ref a(m()), v(m());
a = e;
while (m_util.is_store_ext(e, a, args, v)) {
indices.push_back(args);
args.push_back(v);
stores.push_back(args);
e = a;
}
e0 = e;
if (is_lambda(e0)) {
quantifier* q = to_quantifier(e0);
if (m_util.is_const(e, e)) {
else_case = e;
return true;
}
if (is_lambda(e)) {
quantifier* q = to_quantifier(e);
e = q->get_expr();
unsigned num_idxs = q->get_num_decls();
expr* e1, *e2, *e3;
ptr_vector<expr> eqs;
while (!is_ground(e) && m().is_ite(e, e1, e2, e3) && is_ground(e2)) {
args.reset();
args.resize(num_idxs, nullptr);
eqs.reset();
eqs.push_back(e1);
for (unsigned i = 0; i < eqs.size(); ++i) {
expr* e = eqs[i];
if (m().is_and(e)) {
eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else if (m().is_eq(e, e1, e2)) {
if (is_var(e2)) {
std::swap(e1, e2);
}
if (is_var(e1) && is_ground(e2)) {
unsigned idx = to_var(e1)->get_idx();
args[num_idxs - idx - 1] = e2;
}
else {
return false;
}
}
expr* e1, *e3, *store_val;
if (!is_ground(e) && m().is_or(e)) {
for (expr* arg : *to_app(e)) {
if (!add_store(args, num_idxs, arg, m().mk_true(), stores)) {
return false;
}
}
for (unsigned i = 0; i < num_idxs; ++i) {
if (!args.get(i)) return false;
}
indices.push_back(args);
else_case = m().mk_false();
return true;
}
while (!is_ground(e) && m().is_ite(e, e1, store_val, e3) && is_ground(store_val)) {
if (!add_store(args, num_idxs, e1, store_val, stores)) {
return false;
}
e = e3;
}
e0 = e;
else_case = e;
return is_ground(e);
}
return false;
}
bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e, expr* store_val, vector<expr_ref_vector>& stores) {
expr* e1, *e2;
ptr_vector<expr> eqs;
args.reset();
args.resize(num_idxs + 1, nullptr);
eqs.push_back(e);
for (unsigned i = 0; i < eqs.size(); ++i) {
e = eqs[i];
if (m().is_and(e)) {
eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else if (m().is_eq(e, e1, e2)) {
if (is_var(e2)) {
std::swap(e1, e2);
}
if (is_var(e1) && is_ground(e2)) {
unsigned idx = to_var(e1)->get_idx();
args[num_idxs - idx - 1] = e2;
}
else {
return false;
}
}
}
for (unsigned i = 0; i < num_idxs; ++i) {
if (!args.get(i)) return false;
}
args[num_idxs] = store_val;
stores.push_back(args);
return true;
}
@ -616,7 +638,8 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
for (auto const& idxs : indices) {
args.reset();
args.push_back(lhs);
args.append(idxs);
idxs.pop_back();
args.append(idxs);
mk_select(args.size(), args.c_ptr(), tmp1);
args[0] = rhs;
mk_select(args.size(), args.c_ptr(), tmp2);

6
src/ast/rewriter/array_rewriter.h
View file

@ -35,11 +35,12 @@ class array_rewriter {
bool m_expand_select_ite;
template<bool CHECK_DISEQ>
lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
bool has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices);
void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls);
sort_ref get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args);
bool add_store(expr_ref_vector& args, unsigned num_idxs, expr* e, expr* store_val, vector<expr_ref_vector>& stores);
public:
array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {
@ -65,6 +66,9 @@ public:
void mk_select(unsigned num_args, expr * const * args, expr_ref & result);
void mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
bool has_index_set(expr* e, expr_ref& e0, vector<expr_ref_vector>& indices);
// The following methods never return BR_FAILED
br_status mk_set_union(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_set_intersect(unsigned num_args, expr * const * args, expr_ref & result);

14
src/model/model_evaluator.cpp
View file

@ -184,6 +184,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_ar_rw.get_fid())
st = mk_array_eq(args[0], args[1], result);
else if (m.are_equal(args[0], args[1])) {
result = m.mk_true();
st = BR_DONE;
}
else if (m.are_distinct(args[0], args[1])) {
result = m.mk_false();
st = BR_DONE;
}
TRACE("model_evaluator",
tout << st << " " << mk_pp(s, m) << " " << s_fid << " " << m_ar_rw.get_fid() << " "
<< mk_pp(args[0], m) << " " << mk_pp(args[1], m) << " " << result << "\n";);
@ -508,6 +516,12 @@ struct evaluator_cfg : public default_rewriter_cfg {
return true;
}
if (m_ar_rw.has_index_set(a, else_case, stores)) {
for (auto const& store : stores) {
are_values &= args_are_values(store, are_unique);
}
return true;
}
if (!m_ar.is_as_array(a)) {
TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";);
TRACE("model_evaluator", tout << m_model << "\n";);

2
src/qe/qe_arrays.cpp
View file

@ -389,7 +389,7 @@ namespace qe {
if (!m_has_stores_v.is_marked (lhs)) {
std::swap (lhs, rhs);
}
if (m_has_stores_v.is_marked (lhs)) {
if (m_has_stores_v.is_marked (lhs) && m_arr_u.is_store(lhs)) {
/** project using the equivalence:
*
* (store(arr0,idx,x) ==I arr1) <->