mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-15 17:03:04 -07:00
parent 3849f665d6
commit 8a913981f6
4 changed files with 43 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/ast/ast.cpp
View file

@ -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)));
}

7
src/ast/euf/euf_etable.cpp
View file

@ -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<table_kind>(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<table_kind>(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 {

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

@ -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 <array>
/**
@ -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<app*>(n2.get()), 1, prs);
}

14
src/sat/smt/pb_card.cpp
View file

@ -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;
}