mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 13:56:08 +00:00
Code Activity

Add initializer_list overloads and update all call sites

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 01:27:08 +00:00
parent e57e0df29c
commit 9efb0e0794
5 changed files with 20 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

4
src/smt/smt_conflict_resolution.cpp
View file

@ -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) {

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