diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 3bb435ed8..f1db92a57 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2901,29 +2901,40 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { SASSERT(has_fact(p2)); SASSERT(is_app(get_fact(p1))); SASSERT(is_app(get_fact(p2))); - SASSERT(to_app(get_fact(p1))->get_num_args() == 2); - SASSERT(to_app(get_fact(p2))->get_num_args() == 2); - CTRACE("mk_transitivity", to_app(get_fact(p1))->get_decl() != to_app(get_fact(p2))->get_decl(), - tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n"; - tout << mk_pp(to_app(get_fact(p1))->get_decl(), *this) << "\n"; - tout << mk_pp(to_app(get_fact(p2))->get_decl(), *this) << "\n";); - SASSERT(to_app(get_fact(p1))->get_decl() == to_app(get_fact(p2))->get_decl() || - ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) && - (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))); - CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0), - tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n"; + app* fact1 = to_app(get_fact(p1)); + app* fact2 = to_app(get_fact(p2)); + SASSERT(fact1->get_num_args() == 2); + SASSERT(fact2->get_num_args() == 2); + CTRACE("mk_transitivity", fact1->get_decl() != fact2->get_decl(), + tout << mk_pp(fact1, *this) << "\n\n" << mk_pp(fact2, *this) << "\n"; + tout << mk_pp(fact1->get_decl(), *this) << "\n"; + tout << mk_pp(fact2->get_decl(), *this) << "\n";); + SASSERT(fact1->get_decl() == fact2->get_decl() || + ( (is_eq(fact1) || is_oeq(fact1)) && + (is_eq(fact2) || is_oeq(fact2)))); + CTRACE("mk_transitivity", fact1->get_arg(1) != fact2->get_arg(0), + tout << mk_pp(fact1, *this) << "\n\n" << mk_pp(fact2, *this) << "\n"; tout << p1->get_id() << ": " << mk_bounded_pp(p1, *this, 5) << "\n\n"; tout << p2->get_id() << ": " << mk_bounded_pp(p2, *this, 5) << "\n\n"; ); - SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)); if (is_reflexivity(p1)) return p2; if (is_reflexivity(p2)) return p1; + // local fixup to admit inline simplifications of not(not(e)) to e + expr* e; + if (is_not(fact1->get_arg(1), e) && is_not(e, e) && e == fact2->get_arg(0)) + p1 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0))); + else if (is_not(fact2->get_arg(0), e) && is_not(e, e) && e == fact1->get_arg(1)) + p2 = mk_transitivity(p1, mk_rewrite(fact1->get_arg(1), fact2->get_arg(0))); + else { + SASSERT(fact1->get_arg(1) == fact2->get_arg(0)); + } // OEQ is compatible with EQ for transitivity. - func_decl* f = to_app(get_fact(p1))->get_decl(); - if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl(); - return mk_app(basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); + func_decl* f = fact1->get_decl(); + if (is_oeq(fact2)) + f = fact2->get_decl(); + return mk_app(basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, fact1->get_arg(0), fact2->get_arg(1))); } diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index e007297ef..6aed46f64 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -203,6 +203,7 @@ namespace euf { SASSERT(n->num_args() > 0); enode * n_prime; void * t = get_table(n); + verbose_stream() << "insert " << n << "\n"; switch (static_cast(GET_TAG(t))) { case UNARY: n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); @@ -223,6 +224,11 @@ namespace euf { void etable::erase(enode * n) { SASSERT(n->num_args() > 0); void * t = get_table(n); + static unsigned count = 0; + verbose_stream() << "erase " << (++count) << " " << n << "\n"; + if (count == 10398) { + verbose_stream() << "here\n"; + } switch (static_cast(GET_TAG(t))) { case UNARY: UNTAG(unary_table*, t)->erase(n); @@ -237,6 +243,7 @@ namespace euf { UNTAG(table*, t)->erase(n); break; } + SASSERT(!contains_ptr(n)); } bool etable::contains(enode* n) const { diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index a35956454..a894f882e 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -28,6 +28,7 @@ Notes: #include "ast/rewriter/var_subst.h" #include "ast/normal_forms/name_exprs.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" #include /** @@ -149,7 +150,7 @@ class skolemizer { p = nullptr; if (m_proofs_enabled) { if (q->get_kind() == forall_k) - p = m.mk_skolemization(mk_not(m, q), mk_not(m, r)); + p = m.mk_skolemization(mk_not(m, q), m.mk_not(r)); else p = m.mk_skolemization(q, r); } @@ -644,6 +645,7 @@ struct nnf::imp { m_result_stack.push_back(n2); if (proofs_enabled()) { if (!fr.m_pol) { + verbose_stream() << mk_pp(t, m) << "\n"; proof * prs[1] = { pr2 }; pr2 = m.mk_oeq_congruence(m.mk_not(t), static_cast(n2.get()), 1, prs); } diff --git a/src/sat/smt/pb_card.cpp b/src/sat/smt/pb_card.cpp index 7356c3e84..30120cb73 100644 --- a/src/sat/smt/pb_card.cpp +++ b/src/sat/smt/pb_card.cpp @@ -176,17 +176,17 @@ namespace pb { return false; } else if (j == bound) { - for (unsigned i = 0; i < bound; ++i) { - s.assign(c, c[i]); - } + for (unsigned i = 0; i < bound; ++i) + s.assign(c, c[i]); return false; } else { - if (c.is_watched()) return true; + if (c.is_watched()) + return true; clear_watch(s); - for (unsigned i = 0; i <= bound; ++i) { - c.watch_literal(s, c[i]); - } + for (unsigned i = 0; i <= bound; ++i) + if (!c.is_watched(s, c[i])) + c.watch_literal(s, c[i]); c.set_watch(); return true; }