mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 06:11:44 +00:00
Code Activity

Merge pull request #8637 from Z3Prover/copilot/refactor-proof-functions-initializer-list

Browse source 
Modernize mk_unit_resolution and mk_transitivity with std::initializer_list overloads
This commit is contained in:
Nikolaj Bjorner 2026-02-15 21:33:08 -08:00 • committed by GitHub
commit 249b59f42c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 69 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/ast.h
View file

@ -2368,6 +2368,12 @@ public:
proof * mk_transitivity(proof * p1, proof * p2, proof * p3, proof * p4);
proof * mk_transitivity(unsigned num_proofs, proof * const * proofs);
proof * mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2);
proof * mk_transitivity(std::initializer_list<proof*> const& proofs) {
return mk_transitivity(proofs.size(), proofs.begin());
}
proof * mk_transitivity(std::initializer_list<proof*> const& proofs, expr * n1, expr * n2) {
return mk_transitivity(proofs.size(), proofs.begin(), n1, n2);
}
proof * mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs);
proof * mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs);
proof * mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs);
@ -2398,6 +2404,12 @@ public:
proof * mk_def_axiom(expr * ax);
proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs);
proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact);
proof * mk_unit_resolution(std::initializer_list<proof*> const& proofs) {
return mk_unit_resolution(proofs.size(), proofs.begin());
}
proof * mk_unit_resolution(std::initializer_list<proof*> const& proofs, expr * new_fact) {
return mk_unit_resolution(proofs.size(), proofs.begin(), new_fact);
}
proof * mk_hypothesis(expr * h);
proof * mk_lemma(proof * p, expr * lemma);

6
src/smt/dyn_ack.cpp
View file

@ -89,8 +89,7 @@ namespace smt {
app_ref eq(m.mk_eq(m_app1, m_app2), m);
proof_ref a1(m.mk_congruence(m_app1, m_app2, prs.size(), prs.data()), m);
proof_ref a2(mk_hypothesis(m, eq, true, m_app1, m_app2), m);
proof * antecedents[2] = { a1.get(), a2.get() };
proof_ref false_pr(m.mk_unit_resolution(2, antecedents), m);
proof_ref false_pr(m.mk_unit_resolution({ a1.get(), a2.get() }), m);
lits.push_back(eq);
SASSERT(lits.size() >= 2);
app_ref lemma(m.mk_or(lits), m);
@ -152,8 +151,7 @@ namespace smt {
if (m.get_fact(p3) != m_eq3) p3 = m.mk_symmetry(p3);
SASSERT(m.get_fact(p3) == m_eq3);
p4 = m.mk_hypothesis(m.mk_not(m_eq3));
proof* ps[2] = { p3, p4 };
p5 = m.mk_unit_resolution(2, ps);
p5 = m.mk_unit_resolution({ p3, p4 });
SASSERT(m.get_fact(p5) == m.mk_false());
expr_ref conclusion(m.mk_or(m.mk_not(m_eq1), m.mk_not(m_eq2), m_eq3), m);
p6 = m.mk_lemma(p5, conclusion);

5
src/smt/smt_conflict_resolution.cpp
View file

@ -1333,9 +1333,8 @@ namespace smt {
}
else {
pr = get_proof(consequent, conflict);
proof * prs[2] = { m_lit2proof[not_l], pr};
SASSERT(prs[0] && prs[1]);
pr = m.mk_unit_resolution(2, prs);
SASSERT(m_lit2proof[not_l] && pr);
pr = m.mk_unit_resolution({ m_lit2proof[not_l], pr });
}
expr_ref_buffer lits(m);
for (literal lit : m_lemma) {

3
src/smt/smt_internalizer.cpp
View file

@ -1656,8 +1656,7 @@ namespace smt {
proof * def = mk_clause_def_axiom(num_lits, lits, m.get_fact(pr));
TRACE(gate_clause, tout << mk_ll_pp(def, m) << "\n";
tout << mk_ll_pp(pr, m););
proof * prs[2] = { def, pr };
pr = m.mk_unit_resolution(2, prs);
pr = m.mk_unit_resolution({ def, pr });
}
mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
}

12
src/tactic/goal.cpp
View file

@ -549,10 +549,8 @@ void goal::elim_redundancies() {
continue;
if (pos_lits.is_marked(atom)) {
proof * p = nullptr;
if (proofs_enabled()) {
proof * prs[2] = { pr(get_idx(atom)), pr(i) };
p = m().mk_unit_resolution(2, prs);
}
if (proofs_enabled())
p = m().mk_unit_resolution({ pr(get_idx(atom)), pr(i) });
expr_dependency_ref d(m());
if (unsat_core_enabled())
d = m().mk_join(dep(get_idx(atom)), dep(i));
@ -566,10 +564,8 @@ void goal::elim_redundancies() {
continue;
if (neg_lits.is_marked(f)) {
proof * p = nullptr;
if (proofs_enabled()) {
proof * prs[2] = { pr(get_not_idx(f)), pr(i) };
p = m().mk_unit_resolution(2, prs);
}
if (proofs_enabled())
p = m().mk_unit_resolution({ pr(get_not_idx(f)), pr(i) });
expr_dependency_ref d(m());
if (unsat_core_enabled())
d = m().mk_join(dep(get_not_idx(f)), dep(i));

50
src/test/proof_checker.cpp
View file

@ -29,6 +29,52 @@ void tst_checker1() {
VERIFY(checker.check(p4.get(), side_conditions));
}
void tst_proof_checker() {
tst_checker1();
void tst_initializer_list_overloads() {
ast_manager m(PGM_ENABLED);
expr_ref a(m), b(m);
proof_ref p1(m), p2(m), p3(m), p4(m);
expr_ref_vector side_conditions(m);
// Test mk_unit_resolution with initializer_list
a = m.mk_const(symbol("a"), m.mk_bool_sort());
b = m.mk_const(symbol("b"), m.mk_bool_sort());
p1 = m.mk_hypothesis(a.get());
p2 = m.mk_hypothesis(m.mk_not(a.get()));
// Test the new initializer_list overload - should produce false
p3 = m.mk_unit_resolution({ p1.get(), p2.get() });
VERIFY(m.get_fact(p3.get()) == m.mk_false());
// Test mk_unit_resolution with new_fact parameter
expr_ref fact(m.mk_or(a.get(), b.get()), m);
proof_ref pa_or_b(m.mk_hypothesis(fact.get()), m);
proof_ref pnot_a(m.mk_hypothesis(m.mk_not(a.get())), m);
p4 = m.mk_unit_resolution({ pa_or_b.get(), pnot_a.get() }, b.get());
VERIFY(m.get_fact(p4.get()) == b.get());
// Test mk_transitivity with initializer_list
// Create a simple transitivity chain: a = b, b = c => a = c
expr_ref c(m);
c = m.mk_const(symbol("c"), m.mk_bool_sort());
// Create rewrite proofs for a = b and b = c
proof_ref pr_ab(m.mk_rewrite(a.get(), b.get()), m);
proof_ref pr_bc(m.mk_rewrite(b.get(), c.get()), m);
// Test the new initializer_list overload for transitivity
// This should create a proof of a = c
proof_ref p5(m.mk_transitivity({ pr_ab.get(), pr_bc.get() }), m);
VERIFY(p5.get() != nullptr);
// Verify the result is a proof with the expected fact (a = c)
expr* trans_fact = m.get_fact(p5.get());
VERIFY(m.is_eq(trans_fact));
VERIFY(to_app(trans_fact)->get_arg(0) == a.get());
VERIFY(to_app(trans_fact)->get_arg(1) == c.get());
std::cout << "Initializer list overloads test passed!" << std::endl;
}
void tst_proof_checker() {
tst_checker1();
tst_initializer_list_overloads();
}