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

/*++
Copyright (c) 2018 Arie Gurfinkel and Microsoft Corporation

Module Name:

    sym_mux.h

Abstract:

    A symbol multiplexer that helps with having multiple versions of
    each of a set of symbols.

Author:

    Arie Gurfinkel
    Krystof Hoder (t-khoder) 2011-9-8.

Revision History:

--*/

#pragma once

#include <optional>
#include <string>

#include "ast/ast.h"
#include "util/map.h"
#include "util/vector.h"

namespace spacer {
class sym_mux {
private:
    class sym_mux_entry {
    public:
        func_decl_ref m_main;
        func_decl_ref_vector m_variants;
        sym_mux_entry(ast_manager &m) : m_main(m), m_variants(m) {}
    };

    typedef obj_map<func_decl, sym_mux_entry*> decl2entry_map;
    typedef obj_map<func_decl, std::pair<sym_mux_entry*, unsigned> > mux2entry_map;

    ast_manager &m;
    mutable decl2entry_map m_entries;
    mutable mux2entry_map m_muxes;

    func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const;
    void ensure_capacity(sym_mux_entry &entry, unsigned sz) const;

public:
    sym_mux(ast_manager & m);
    ~sym_mux();
    ast_manager & get_manager() const { return m; }

    void register_decl(func_decl *fdecl);
    std::optional<unsigned> find_idx(func_decl * sym) const;
    bool has_index(func_decl * sym, unsigned idx) const
    {auto v = find_idx(sym); return v && *v == idx;}

    bool is_muxed(func_decl *fdecl) const {return m_muxes.contains(fdecl);}

    /**
       \brief Return symbol created from prefix, or 0 if the prefix
        was never used.
    */
    func_decl * find_by_decl(func_decl* fdecl, unsigned idx) const;

    /**
       \brief Return true if the only multiplexed symbols which e contains are
       of index idx.
    */
    bool is_homogenous_formula(expr * e, unsigned idx) const;


    /**
      \brief Convert symbol sym which has to be of src_idx variant
      into variant tgt_idx.
    */
    func_decl * shift_decl(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const;

    /**
      \brief Convert src_idx symbols in formula f variant into
      tgt_idx.  If homogenous is true, formula cannot contain symbols
      of other variants.
    */
    void shift_expr(expr * f, unsigned src_idx, unsigned tgt_idx,
                    expr_ref & res, bool homogenous = true) const;


};
}