mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #2879. relax benign restriction on eq propagation justification

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-23 14:00:14 -06:00
parent 794aafa6f8
commit f9917edf6c
3 changed files with 2 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_justification.cpp
View file

@ -182,7 +182,7 @@ namespace smt {
}
void eq_propagation_justification::get_antecedents(conflict_resolution & cr) {
cr.mark_eq(m_node1, m_node2);
if (m_node1 != m_node2) cr.mark_eq(m_node1, m_node2);
}
proof * eq_propagation_justification::mk_proof(conflict_resolution & cr) {

1
src/smt/smt_justification.h
View file

@ -181,7 +181,6 @@ namespace smt {
enode * m_node2;
public:
eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) {
SASSERT(n1 != n2);
}
void get_antecedents(conflict_resolution & cr) override;

22
src/smt/theory_seq.cpp
View file

@ -5830,27 +5830,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
}
else if (m_util.str.is_contains(e, e1, e2)) {
expr_ref_vector disj(m);
// disabled pending regression on issue 1196
if (false && m_seq_rewrite.reduce_contains(e1, e2, disj)) {
literal_vector lits;
literal lit = mk_literal(e);
lits.push_back(~lit);
for (expr* d : disj) {
lits.push_back(mk_literal(d));
}
++m_stats.m_add_axiom;
{
std::function<expr*(void)> fn = [&]() { return m.mk_implies(e, m.mk_or(disj.size(), disj.c_ptr())); };
scoped_trace_stream _sts(*this, fn);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
for (expr* d : disj) {
add_axiom(lit, ~mk_literal(d));
}
}
else if (is_true) {
if (is_true) {
expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
f = mk_concat(f1, e2, f2);