From e57e0df29c0a5156b2c2b3d075524e24d5844432 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Feb 2026 01:24:01 +0000 Subject: [PATCH 1/5] Initial plan From 9efb0e079456414a60cc40d0f9f7f10589e97ad1 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Feb 2026 01:27:08 +0000 Subject: [PATCH 2/5] Add initializer_list overloads and update all call sites Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/ast.h | 12 ++++++++++++ src/smt/dyn_ack.cpp | 6 ++---- src/smt/smt_conflict_resolution.cpp | 4 +--- src/smt/smt_internalizer.cpp | 3 +-- src/tactic/goal.cpp | 12 ++++-------- 5 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 6e5ce8c78..0f3bcc022 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2361,6 +2361,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 const& proofs) { + return mk_transitivity(proofs.size(), proofs.begin()); + } + proof * mk_transitivity(std::initializer_list 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); @@ -2391,6 +2397,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 const& proofs) { + return mk_unit_resolution(proofs.size(), proofs.begin()); + } + proof * mk_unit_resolution(std::initializer_list 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); diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 3779911cd..a2a96e8a4 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -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); diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index a578b553d..88f6ceedc 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1333,9 +1333,7 @@ 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); + pr = m.mk_unit_resolution({ m_lit2proof[not_l], pr }); } expr_ref_buffer lits(m); for (literal lit : m_lemma) { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index dce34a366..8889409c2 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -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))); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 63d5e2ddc..a15298ac8 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -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)); From d239e7a19d8d6895ecc93badabd954b76907a471 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Feb 2026 01:48:21 +0000 Subject: [PATCH 3/5] Add test for initializer_list overloads Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/test/proof_checker.cpp | 44 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 42 insertions(+), 2 deletions(-) diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index bc3dd39ad..d600c60f5 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -29,6 +29,46 @@ 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 + expr_ref c(m), eq_ab(m), eq_bc(m); + c = m.mk_const(symbol("c"), m.mk_bool_sort()); + eq_ab = m.mk_eq(a.get(), b.get()); + eq_bc = m.mk_eq(b.get(), c.get()); + + proof_ref pr1(m.mk_reflexivity(eq_ab.get()), m); + proof_ref pr2(m.mk_reflexivity(eq_bc.get()), m); + + // Test the new initializer_list overload for transitivity + proof_ref p5(m.mk_transitivity({ pr1.get(), pr2.get() }), m); + VERIFY(p5.get() != nullptr); + + std::cout << "Initializer list overloads test passed!" << std::endl; +} + +void tst_proof_checker() { + tst_checker1(); + tst_initializer_list_overloads(); } From e627e60fe711743b91c1e57044cff871a47146f5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Feb 2026 01:50:51 +0000 Subject: [PATCH 4/5] Restore defensive SASSERT in smt_conflict_resolution Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/smt_conflict_resolution.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 88f6ceedc..0d81e8d9e 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1333,6 +1333,7 @@ namespace smt { } else { pr = get_proof(consequent, conflict); + SASSERT(m_lit2proof[not_l] && pr); pr = m.mk_unit_resolution({ m_lit2proof[not_l], pr }); } expr_ref_buffer lits(m); From f3c4c57c58a3d1ce2761095f44defa0eb797bf19 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Feb 2026 01:52:20 +0000 Subject: [PATCH 5/5] Improve test validation for mk_transitivity Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/test/proof_checker.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index d600c60f5..ec5fc9edc 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -53,17 +53,23 @@ void tst_initializer_list_overloads() { VERIFY(m.get_fact(p4.get()) == b.get()); // Test mk_transitivity with initializer_list - expr_ref c(m), eq_ab(m), eq_bc(m); + // 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()); - eq_ab = m.mk_eq(a.get(), b.get()); - eq_bc = m.mk_eq(b.get(), c.get()); - proof_ref pr1(m.mk_reflexivity(eq_ab.get()), m); - proof_ref pr2(m.mk_reflexivity(eq_bc.get()), m); + // 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 - proof_ref p5(m.mk_transitivity({ pr1.get(), pr2.get() }), m); + // 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; }