z3-src 501.0.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

/*++
Copyright (c) 2022 Microsoft Corporation

Module Name:

    rewriter_simplifier.h

Abstract:

    rewriter simplifier

Author:

    Nikolaj Bjorner (nbjorner) 2022-11-24

--*/

#pragma once

#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/th_rewriter.h"


class rewriter_simplifier : public dependent_expr_simplifier {

    unsigned               m_num_steps = 0;
    params_ref             m_params;
    th_rewriter            m_rewriter;

public:
    rewriter_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
        dependent_expr_simplifier(m, fmls),
        m_rewriter(m) {
        updt_params(p);
    }

    char const* name() const override { return "simplifier"; }
        
    void reduce() override {
        m_num_steps = 0;
        expr_ref   new_curr(m);
        proof_ref  new_pr(m);
        for (unsigned idx : indices()) {
            auto d = m_fmls[idx];
            m_rewriter(d.fml(), new_curr, new_pr);
            m_num_steps += m_rewriter.get_num_steps();
            m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep()));            
        }
    }
    bool supports_proofs() const override { return true; }
    void collect_statistics(statistics& st) const override { st.update("simplifier-steps", m_num_steps); }
    void reset_statistics() override { m_num_steps = 0; }
    void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(m_params); }
    void collect_param_descrs(param_descrs& r) override { th_rewriter::get_param_descrs(r); }
};

/*
  ADD_SIMPLIFIER("simplify", "apply simplification rules.", "alloc(rewriter_simplifier, m, p, s)")
 */