z3-src 503.2.1

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

/*++
Copyright (c) 2026 Romain Soulat

    Theory clause weakening preserves obligations for removed literals.
--*/
#include "ast/reg_decl_plugins.h"
#include "sat/smt/euf_proof_checker.h"
#include "util/debug.h"

void tst_smt_proof_weakening() {
    ast_manager m;
    reg_decl_plugins(m);
    euf::theory_checker checker(m);
    expr_ref p(m.mk_const("p", m.mk_bool_sort()), m);
    expr_ref guard(m.mk_const("guard", m.mk_bool_sort()), m);
    expr_ref not_p(m.mk_not(p), m);
    // The EUF checker certifies the tautology !p or p from p and !p.
    expr* premises[] = {p, not_p};
    app_ref hint(m.mk_app(symbol("euf"), 2, premises, m.mk_proof_sort()), m);
    expr_ref_vector clause(m), units(m);
    auto check = [&](app* proof_hint) {
        return checker.check(proof_hint) &&
            checker.clause_follows(clause, checker.clause(proof_hint), units);
    };
    clause.push_back(p);
    clause.push_back(not_p);
    clause.push_back(guard);
    ENSURE(check(hint) && units.empty());
    clause.reset();
    clause.push_back(p);
    clause.push_back(guard);
    ENSURE(check(hint));
    ENSURE(units.size() == 1 && units[0] == p);
    clause.reset();
    clause.push_back(guard);
    ENSURE(check(hint) && units.size() == 2);
    ENSURE((units[0] == p && units[1] == not_p) ||
           (units[1] == p && units[0] == not_p));
    // Syntactic double negations do not create spurious unit obligations.
    clause.reset();
    clause.push_back(m.mk_not(m.mk_not(p)));
    clause.push_back(m.mk_not(m.mk_not(not_p)));
    clause.push_back(guard);
    ENSURE(check(hint) && units.empty());
    // Clause normalization must not turn a rejected hint into evidence.
    app_ref invalid(m.mk_const("unknown-rule", m.mk_proof_sort()), m);
    ENSURE(!check(invalid));
}