z3-src 503.2.1

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
135
136
137

/*++
Copyright (c) 2023 Microsoft Corporation

Module Name:

    polymorphism_util.h

Abstract:

    Utilities for supporting polymorphic type signatures.

Author:

    Nikolaj Bjorner (nbjorner) 2023-7-8

--*/
#pragma once

#include "ast/ast.h"
#include "util/hashtable.h"

namespace polymorphism {

    class substitution {
        ast_manager& m;
        obj_map<sort, sort*> m_sub;
        sort_ref_vector m_trail;
    public:
        substitution(ast_manager& m): m(m), m_trail(m) {}
    
        sort_ref_vector operator()(sort_ref_vector const& s);
        
        sort_ref operator()(sort* s);

        expr_ref operator()(expr* e);
        
        bool unify(sort* s1, sort* s2);       

        bool match(sort* s1, sort* s_ground);

        obj_map<sort, sort*>::iterator begin() const { return m_sub.begin(); }
        obj_map<sort, sort*>::iterator end() const { return m_sub.end(); }

        void insert(sort* v, sort* t) { m_trail.push_back(v).push_back(t); m_sub.insert(v, t); }

        bool find(sort* v, sort*& t) const { return m_sub.find(v, t); }

        unsigned size() const { return m_sub.size(); }

        /**
        * weak equality: strong equality considers applying substitutions recursively in range
        * because substitutions may be in triangular form.
        */
        struct eq {
            bool operator()(substitution const* s1, substitution const* s2) const {
                if (s1->size() != s2->size())
                    return false;
                sort* v2;
                for (auto const& [k, v] : *s1) {
                    if (!s2->find(k, v2))
                        return false;
                    if (v != v2)
                        return false;
                }
                return true;
            }
        };

        struct hash {
            unsigned operator()(substitution const* s) const {
                unsigned hash = 0xfabc1234 + s->size();
                for (auto const& [k, v] : *s) 
                    hash ^= k->hash() + 2 * v->hash();                
                return hash;
            }
        };
    };

    typedef hashtable<substitution*, substitution::hash, substitution::eq> substitutions;

    /**
     * Polymorphic signature for operators
     */
    struct psig {
        symbol          m_name;
        unsigned        m_num_params;
        sort_ref_vector m_dom;
        sort_ref        m_range;
        psig(ast_manager& m, char const* name, unsigned n, unsigned dsz, sort* const* dom, sort* rng):
            m_name(name),
            m_num_params(n),
            m_dom(m),
            m_range(rng, m)
        {
            m_dom.append(dsz, dom);
        }
    };
    
    class util {
        ast_manager&         m;
        sort_ref_vector      m_trail;
        obj_map<sort, sort*> m_fresh;
        unsigned             m_counter = 0;

        sort_ref fresh(sort* s);

        sort_ref_vector fresh(unsigned n, sort* const* s);
        
    public:
        util(ast_manager& m): m(m), m_trail(m) {}
        
        bool unify(sort* s1, sort* s2, substitution& sub);
        
        bool unify(func_decl* f1, func_decl* f2, substitution& sub);
        
        bool unify(substitution const& s1, substitution const& s2,
                   substitution& sub);

        bool match(substitution& sub, sort* s1, sort* s_ground);

        /**
         * Match a polymorphic signature against concrete argument sorts.
         * Raises exception if arity mismatch or type mismatch.
         * Returns the instantiated range sort via range_out.
         */
        void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& range_out);
                        
        // collect instantiations of polymorphic functions
        void collect_poly_instances(expr* e, ptr_vector<func_decl>& instances);
        
        // test if expression contains polymorphic variable.
        bool has_type_vars(expr* e);

        void collect_type_vars(expr* e, ptr_vector<sort>& tvs);
        
    };
}