z3-src 503.2.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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138

/*++
Copyright (c) 2022 Microsoft Corporation

Module Name:

    euf_completion_tactic.cpp

Abstract:

    Tactic for simplifying with equations.

Author:

    Nikolaj Bjorner (nbjorner) 2022-10-30

--*/

#include "ast/rewriter/expr_safe_replace.h"
#include "tactic/tactic.h"
#include "tactic/portfolio/euf_completion_tactic.h"
#include "solver/solver.h"
#include "smt/smt_solver.h"

class euf_side_condition_solver : public euf::side_condition_solver {
    ast_manager& m;
    params_ref m_params;
    scoped_ptr<solver> m_solver;
    expr_ref_vector m_deps;
    obj_map<expr, std::pair<proof*, expr_dependency*>> m_e2d;
    expr_ref_vector m_fmls;
    obj_hashtable<expr> m_seen;
    trail_stack m_trail;

    void init_solver() {
        if (m_solver.get())
            return;
        m_params.set_uint("smt.max_conflicts", 100);
        scoped_ptr<solver_factory> f = mk_smt_solver_factory();
        m_solver = (*f)(m, m_params, false, false, true, symbol::null);
    }

public:

    euf_side_condition_solver(ast_manager& m, params_ref const& p) : 
        m(m), m_params(p), m_deps(m), m_fmls(m) {}

    void push() override {
        init_solver();
        m_solver->push();
        m_trail.pop_scope(1);
    }

    void pop(unsigned n) override {
        m_trail.push_scope();
        SASSERT(m_solver.get());
        m_solver->pop(n);
    }

    void add_constraint(expr* f, proof* pr, expr_dependency* d) override {
        if (m_seen.contains(f))
            return;
        m_seen.insert(f);
        m_trail.push(insert_obj_trail(m_seen, f));
        if (!is_ground(f))
            return;
        if (m.is_implies(f))
            return;
        init_solver();
        if (d) {
            expr* e_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
            m_deps.push_back(e_dep);
            m_e2d.insert(e_dep, { pr, d });
            m_trail.push(insert_obj_map(m_e2d, e_dep));
            m_solver->assert_expr(f, e_dep);
        }
        else
            m_solver->assert_expr(f);        
    }

    bool is_true(expr* f, proof_ref& pr, expr_dependency*& d) override {
        d = nullptr;
        init_solver();
        solver::scoped_push _sp(*m_solver);
        m_fmls.reset();
        m_fmls.push_back(m.mk_not(f));
        expr_ref nf(m.mk_not(f), m);
        lbool r = m_solver->check_sat(m_fmls);
        if (r == l_false) {
            expr_ref_vector core(m);
            m_solver->get_unsat_core(core);
            for (auto c : core) {
                if (c == nf)
                    continue;
                auto [pr, dep] = m_e2d[c];
                d = m.mk_join(d, dep);
            }
            if (m.proofs_enabled()) {
                pr = m_solver->get_proof();
                SASSERT(pr);
                expr_safe_replace rep(m);
                for (auto c : core) {
                    if (c == nf)
                        continue;
                    auto [p, dep] = m_e2d[c];
                    rep.insert(m.mk_asserted(c), p);
                }
                expr_ref ppr(pr, m);
                rep(ppr);
                pr = to_app(ppr.get());
            }
        }

        return r == l_false;
    }

    void solve_for(vector<solution>& sol) override {
        init_solver();
        vector<solver::solution> ss;
        for (auto [v, t, g] : sol)
            ss.push_back({ v, t, g });
        sol.reset();
        m_solver->solve_for(ss);
        for (auto [v, t, g] : ss)
            sol.push_back({ v, t, g });
    }
};

dependent_expr_simplifier* mk_euf_completion_simplifier(ast_manager& m, dependent_expr_state& s, params_ref const& p) {
    auto r = alloc(euf::completion, m, s);
    auto scs = alloc(euf_side_condition_solver, m, p);
    r->set_solver(scs);
    return r;
}

tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) {
    return alloc(dependent_expr_state_tactic, m, p,
                 [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return mk_euf_completion_simplifier(m, s, p); });
}