mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-16 22:01:44 +00:00
Code Activity

Add test for initializer_list overloads

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:48:21 +00:00
parent 9efb0e0794
commit d239e7a19d
1 changed files with 42 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/test/proof_checker.cpp
View file

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