z3-src 415.4.3

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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    simplify_tactic.cpp

Abstract:

    Apply simplification and rewriting rules.

Author:

    Leonardo (leonardo) 2011-11-20

Notes:

--*/
#include "tactic/core/simplify_tactic.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/ast_pp.h"

struct simplify_tactic::imp {
    ast_manager &   m_manager;
    th_rewriter     m_r;
    unsigned        m_num_steps;

    imp(ast_manager & m, params_ref const & p):
        m_manager(m),
        m_r(m, p),
        m_num_steps(0) {
    }

    ast_manager & m() const { return m_manager; }


    void reset() {
        m_r.reset();
        m_num_steps = 0;
    }

    void collect_statistics(statistics& st) {
        st.update("rewriter.steps", m_num_steps);
    }

    void operator()(goal & g) {
        tactic_report report("simplifier", g);
        m_num_steps = 0;
        if (g.inconsistent())
            return;
        expr_ref   new_curr(m());
        proof_ref  new_pr(m());
        unsigned size = g.size();
        for (unsigned idx = 0; idx < size; ++idx) {
            if (g.inconsistent())
                break;
            expr * curr = g.form(idx);
            m_r(curr, new_curr, new_pr);
            m_num_steps += m_r.get_num_steps();
            if (g.proofs_enabled()) {
                proof * pr = g.pr(idx);
                new_pr     = m().mk_modus_ponens(pr, new_pr);
            }
            g.update(idx, new_curr, new_pr, g.dep(idx));
        }
        TRACE(simplifier, g.display(tout););
        g.elim_redundancies();
        TRACE(after_simplifier_detail, g.display_with_dependencies(tout););
    }

    unsigned get_num_steps() const { return m_num_steps; }
};

simplify_tactic::simplify_tactic(ast_manager & m, params_ref const & p):
    m_params(p) {
    m_imp = alloc(imp, m, p);
}

simplify_tactic::~simplify_tactic() {
    dealloc(m_imp);
}

void simplify_tactic::updt_params(params_ref const & p) {
    m_params.append(p);
    m_imp->m_r.updt_params(m_params);
}

void simplify_tactic::get_param_descrs(param_descrs & r) {
    th_rewriter::get_param_descrs(r);
}

void simplify_tactic::operator()(goal_ref const & in, 
                                 goal_ref_buffer & result) {
    try {
        (*m_imp)(*(in.get()));
        in->inc_depth();
        result.push_back(in.get());
        m_clean = false;
    }
    catch (rewriter_exception & ex) {
        throw tactic_exception(ex.what());
    }
}


void simplify_tactic::cleanup() {
    if (m_clean)
        return;
    ast_manager & m = m_imp->m();
    params_ref p = std::move(m_params);
    m_imp->~imp();
    new (m_imp) imp(m, p);
    m_clean = true;
}

void simplify_tactic::collect_statistics(statistics& st) const {
    if (m_imp)
        m_imp->collect_statistics(st);
}

unsigned simplify_tactic::get_num_steps() const {
    return m_imp->get_num_steps();
}

tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p) {
    return clean(alloc(simplify_tactic, m, p));
}

tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p) {
    params_ref xp = p;
    xp.set_bool("elim_and", true);
    return using_params(mk_simplify_tactic(m, xp), xp);
}