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

fixes for #4688

Browse source 
https://github.com/Z3Prover/z3/issues/4866#issuecomment-778721073
This commit is contained in:
Nikolaj Bjorner 2021-04-11 17:42:12 -07:00
parent 2dcfe799bc
commit 804f065215
4 changed files with 59 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/ast/rewriter/th_rewriter.cpp
View file

@ -176,11 +176,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = args[0]->get_sort()->get_family_id();
if (s_fid == m_a_rw.get_fid()) {
if (s_fid == m_a_rw.get_fid())
st = m_a_rw.mk_eq_core(args[0], args[1], result);
if (st == BR_FAILED && is_app(args[0]) && to_app(args[0])->get_family_id() == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
}
else if (s_fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_dt_rw.get_fid())
@ -208,13 +205,30 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (st != BR_FAILED)
return st;
}
if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) {
if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
st = m_seq_rw.mk_bool_app(f, num, args, result);
if (st != BR_FAILED)
return st;
}
if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
return m_b_rw.mk_app_core(f, num, args, result);
}
if (fid == m_a_rw.get_fid() && OP_LE == f->get_decl_kind() && m_seq_rw.u().has_seq()) {
st = m_seq_rw.mk_le_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
if (fid == m_a_rw.get_fid() && OP_GE == f->get_decl_kind() && m_seq_rw.u().has_seq()) {
st = m_seq_rw.mk_le_core(args[1], args[0], result);
if (st != BR_FAILED)
return st;
}
if (fid == m_a_rw.get_fid())
return m_a_rw.mk_app_core(f, num, args, result);
if (fid == m_bv_rw.get_fid())