z3-src 503.3.0

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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

/*++
Copyright (c) 2026 Romain Soulat

    Incremental SAT/SMT proof clauses must bind user-scope guard literals.
--*/
#include "ast/reg_decl_plugins.h"
#include "ast/arith_decl_plugin.h"
#include "solver/solver.h"
#include "model/model.h"
#include "tactic/user_propagator_base.h"
#include "util/debug.h"

void tst_sat_smt_proof_scope() {
    for (auto [early_scope, proof_logging] : {std::pair{false, false}, {false, true},
                                             {true, false}, {true, true}}) {
        ast_manager m;
        reg_decl_plugins(m);
        arith_util a(m);
        params_ref p;
        p.set_bool("smt", true);
        p.set_bool("euf", true);
        p.set_bool("smt.proof.check", proof_logging);
        scoped_ptr<solver> s = mk_smt2_solver(m, p);
        if (early_scope) {
            s->push();
            s->push();
        }
        unsigned clauses = 0;
        auto pop = [&](unsigned n) { s->pop(n); };
        user_propagator::on_clause_eh_t callback = [&](void*, expr*, unsigned, unsigned const*,
                                                       unsigned n, expr* const* literals) {
            // Includes deletion notifications during pop, before variable IDs
            // can be recycled for a different scope's atoms.
            for (unsigned i = 0; i < n; ++i)
                ENSURE(literals[i] && m.is_bool(literals[i]));
            ++clauses;
        };
        if (proof_logging)
            s->register_on_clause(nullptr, callback);
        expr_ref x(m.mk_const("scope_x", a.mk_int()), m);
        s->assert_expr(a.mk_ge(x, a.mk_int(0)));
        s->assert_expr(a.mk_le(x, a.mk_int(3)));
        ENSURE(s->check_sat() == l_true);
        for (unsigned i = 0; i < 8; ++i) {
            s->push();
            expr_ref value(m.mk_eq(x, a.mk_int(i % 4)), m);
            s->assert_expr(value);
            ENSURE(s->check_sat() == l_true);
            model_ref model;
            s->get_model(model);
            expr_ref evaluated(m);
            ENSURE(model->eval_expr(value, evaluated, true) && m.is_true(evaluated));
            // The scope's proof atom is internal and must not pollute models.
            for (unsigned j = 0; j < model->get_num_constants(); ++j)
                ENSURE(model->get_constant(j)->get_name().str().find("sat.scope") != 0);
            s->push();
            s->assert_expr(m.mk_not(value));
            ENSURE(s->check_sat() == l_false);
            pop(1);
            ENSURE(s->check_sat() == l_true);
            pop(1);
            ENSURE(s->check_sat() == l_true);
            expr_ref out_of_range(m.mk_eq(x, a.mk_int(4)), m);
            expr* assumptions[] = {out_of_range};
            ENSURE(s->check_sat(1, assumptions) == l_false);
            ENSURE(s->check_sat() == l_true);
        }
        if (early_scope) {
            pop(2);
            ENSURE(s->check_sat() == l_true);
            s->push();
            s->assert_expr(m.mk_eq(x, a.mk_int(7)));
            ENSURE(s->check_sat() == l_true);
            pop(1);
        }
        ENSURE(!proof_logging || clauses > 0);
    }
}