From 8a913981f6bce740ed10de969e97df336e9df37d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Jul 2023 17:03:04 -0700 Subject: [PATCH] fix #6813 - proofs terms are fragile with respect to simplificiation of not(not(e)). It would be better if proof terms didn't have to track this level of detail, but the legacy proof format assumes strictly checkable proofs. A patch is to fixup terms within the mk_transitivity constructor Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 41 +++++++++++++++++++++++------------- src/ast/euf/euf_etable.cpp | 7 ++++++ src/ast/normal_forms/nnf.cpp | 4 +++- src/sat/smt/pb_card.cpp | 14 ++++++------ 4 files changed, 43 insertions(+), 23 deletions(-) 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; }