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

/*++
Copyright (c) 2022 Microsoft Corporation

Module Name:

    demodulator_simplifier.h

Author:

    Nikolaj Bjorner (nbjorner) 2022-12-4

--*/

#pragma once

#include "ast/substitution/demodulator_rewriter.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "util/uint_set.h"

class demodulator_index {
    ast_manager& m;
    obj_map<func_decl, uint_set*> m_fwd_index, m_bwd_index; 
    void add(func_decl* f, unsigned i, obj_map<func_decl, uint_set*>& map);
    void del(func_decl* f, unsigned i, obj_map<func_decl, uint_set*>& map);
 public:
    demodulator_index(ast_manager& m): m(m) {}
    ~demodulator_index();
    void reset();
    void insert_fwd(func_decl* f, unsigned i) { add(f, i, m_fwd_index); }
    void remove_fwd(func_decl* f, unsigned i) { del(f, i, m_fwd_index); }
    void insert_bwd(expr* e, unsigned i);
    void remove_bwd(expr* e, unsigned i);
    bool find_fwd(func_decl* f, uint_set*& s) { return m_fwd_index.find(f, s); }
    bool find_bwd(func_decl* f, uint_set*& s) { return m_bwd_index.find(f, s); }
    bool empty() const { return m_fwd_index.empty(); }
    std::ostream& display(std::ostream& out) const;
};

class demodulator_simplifier : public dependent_expr_simplifier {
    typedef std::pair<app*, expr*> app_expr_pair;
    demodulator_index         m_index;
    demodulator_util          m_util;
    demodulator_match_subst   m_match_subst;
    demodulator_rewriter_util m_rewriter;
    u_map<app_expr_pair>      m_rewrites;
    uint_set                  m_processed, m_dependencies;
    unsigned_vector           m_todo;
    expr_ref_vector           m_pinned;
    proof_ref_vector          m_proof_pinned;

    void rewrite(unsigned i);
    bool rewrite1(func_decl* f, expr_ref_vector const& args, expr_ref& np, proof_ref& pr);
    proof* mk_instance_proof(unsigned i, func_decl* f, expr_ref_vector const& args, expr* np);
    expr* fml(unsigned i) { return m_fmls[i].fml(); }
    proof* pr(unsigned i) { return m_fmls[i].pr(); }
    expr_dependency* dep(unsigned i) { return m_fmls[i].dep(); }
    void reschedule_processed(func_decl* f);
    void reschedule_demodulators(func_decl* f, expr* lhs);
    void reset();

 public:
     demodulator_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st);

     void reduce() override;    

     char const* name() const override { return "demodulator"; }
     bool supports_proofs() const override { return true; }
};