mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

fix #4090 fix #4088 fix #4085

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-24 10:37:43 -07:00
parent 470e87afe9
commit c3b33aae8a
3 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/normal_forms/nnf.cpp
View file

@ -697,8 +697,7 @@ struct nnf::imp {
else {
r = arg;
if (proofs_enabled()) {
proof * p1 = m.mk_iff_oeq(m.mk_rewrite(t, t->get_arg(0)));
pr = m.mk_transitivity(p1, arg_pr);
pr = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(r));
}
}

2
src/smt/mam.cpp
View file

@ -1367,6 +1367,8 @@ namespace {
*/
bool is_semi_compatible(check * instr) const {
unsigned reg = instr->m_reg;
if (instr->m_enode && !instr->m_enode->has_lbl_hash())
instr->m_enode->set_lbl_hash(m_context);
return
m_registers[reg] != 0 &&
// if the register was already checked by another filter, then it doesn't make sense

13
src/smt/seq_eq_solver.cpp
View file

@ -988,6 +988,7 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
!is_ternary_eq2(e.rs(), e.ls(), xs, x, y1, ys, y2, flag1))
return false;
dependency* dep = e.dep();
rational lenX, lenY1, lenY2;
context& ctx = get_context();
if (!get_length(x, lenX)) {
@ -1001,7 +1002,7 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
}
SASSERT(!xs.empty() && !ys.empty());
unsigned_vector indexes = overlap2(xs, ys);
if (branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2))
if (branch_ternary_variable_base2(dep, indexes, xs, x, y1, ys, y2))
return true;
// xs ++ x = y1 ++ ys ++ y2 => xs ++ z = y1, x = z ++ ys ++ y2
@ -1015,7 +1016,6 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
TRACE("seq", tout << "one case\n";);
TRACE("seq", display_equation(tout, e););
literal_vector lits;
dependency* dep = e.dep();
propagate_eq(dep, lits, x, Zysy2, true);
propagate_eq(dep, lits, y1, xsZ, true);
}
@ -1029,11 +1029,11 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
break;
case l_true:
TRACE("seq", display_equation(tout << "true branch\n", e););
propagate_eq(e.dep(), ge, x, Zysy2, true);
propagate_eq(e.dep(), ge, y1, xsZ, true);
propagate_eq(dep, ge, x, Zysy2, true);
propagate_eq(dep, ge, y1, xsZ, true);
break;
default:
return branch_ternary_variable_base2(e.dep(), indexes, xs, x, y1, ys, y2);
return branch_ternary_variable_base2(dep, indexes, xs, x, y1, ys, y2);
}
}
@ -1055,6 +1055,7 @@ bool theory_seq::branch_quat_variable(eq const& e) {
expr_ref x1(m), x2(m), y1(m), y2(m);
if (!is_quat_eq(e.ls(), e.rs(), x1, xs, x2, y1, ys, y2))
return false;
dependency* dep = e.dep();
rational lenX1, lenX2, lenY1, lenY2;
context& ctx = get_context();
@ -1093,7 +1094,6 @@ bool theory_seq::branch_quat_variable(eq const& e) {
expr_ref Z1 = m_sk.mk_align(ysy2, xsx2, x1, y1);
expr_ref y1Z1 = mk_concat(y1, Z1);
expr_ref Z1xsx2 = mk_concat(Z1, xsx2);
dependency* dep = e.dep();
propagate_eq(dep, ~le, x1, y1Z1, true);
propagate_eq(dep, ~le, Z1xsx2, ysy2, true);
break;
@ -1105,7 +1105,6 @@ bool theory_seq::branch_quat_variable(eq const& e) {
expr_ref Z2 = m_sk.mk_align(xsx2, ysy2, y1, x1);
expr_ref x1Z2 = mk_concat(x1, Z2);
expr_ref Z2ysy2 = mk_concat(Z2, ysy2);
dependency* dep = e.dep();
propagate_eq(dep, le, x1Z2, y1, true);
propagate_eq(dep, le, xsx2, Z2ysy2, true);
break;