z3-src 503.2.2

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

/*++
Copyright (c) 2022 Microsoft Corporation

Module Name:

    bv_bounds_simplifier.h

Author:

    Nikolaj Bjorner (nbjorner) 2023-01-27

--*/

#include "ast/simplifiers/bv_bounds_simplifier.h"
#include "ast/simplifiers/dominator_simplifier.h"
#include "ast/rewriter/bv_bounds_base.h"
#include "ast/rewriter/dom_simplifier.h"
#include "ast/rewriter/th_rewriter.h"


class dom_bv_bounds_simplifier : public dom_simplifier, public bv::bv_bounds_base {
    params_ref         m_params;
    th_rewriter        m_rewriter;
    
public:
    dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) :
        bv_bounds_base(m), m_rewriter(m) {
        updt_params(p);
    }
    
    void updt_params(params_ref const & p) override {
        m_params.append(p);
        m_propagate_eq = p.get_bool("propagate_eq", false);
        m_rewriter.updt_params(m_params);
    }
    
    void collect_param_descrs(param_descrs& r) override {
        th_rewriter::get_param_descrs(r);
        r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false");
    }
    
    bool assert_expr(expr * t, bool sign) override {
        return assert_expr_core(t, sign);
    }
    
    void operator()(expr_ref& r) override {
        expr_ref result(m);
        if (simplify_core(r, result)) {
            m_rewriter(result);
            r = result;
        }
    }       
    
    void pop(unsigned num_scopes) override {
        pop_core(num_scopes);
    }
    
    dom_simplifier * translate(ast_manager & m) override {
        return alloc(dom_bv_bounds_simplifier, m, m_params);
    }
    
    unsigned scope_level() const override {
        return m_scopes.size();
    }
};

dependent_expr_simplifier* mk_bv_bounds_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) {
    return alloc(dominator_simplifier, m, s, alloc(dom_bv_bounds_simplifier, m, p), p); 
}