z3-src 415.4.4

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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202

/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    array_factory.cpp

Abstract:

    <abstract>

Author:

    Leonardo de Moura (leonardo) 2008-10-28.

Revision History:

--*/

#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include "model/func_interp.h"
#include "model/model_core.h"
#include "model/array_factory.h"

func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
    ptr_buffer<sort> domain;
    sort * range = get_array_range(s);
    unsigned arity = get_array_arity(s);
    for (unsigned i = 0; i < arity; i++) {
        domain.push_back(get_array_domain(s, i));
    }
    return m.mk_fresh_func_decl(symbol::null, symbol::null, arity, domain.data(), range);
}

array_factory::array_factory(ast_manager & m, model_core & md):
    struct_factory(m, m.mk_family_id("array"), md) {
}

/**
   \brief Return as-array[f] where f is a fresh function symbol with the right domain and range for the array sort s.
   Store in fi the function interpretation for f.
*/
expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) {
    func_decl * f    = mk_aux_decl_for_array_sort(m_manager, s);
    fi = alloc(func_interp, m_manager, get_array_arity(s));
    m_model.register_decl(f, fi);
    parameter p(f);
    expr * val = m_manager.mk_app(get_family_id(), OP_AS_ARRAY, 1, &p);
    register_value(val);
    return val;
}

void array_factory::get_some_args_for(sort * s, ptr_buffer<expr> & args) {
    unsigned arity = get_array_arity(s);
    for (unsigned i = 0; i < arity; i++) {
        sort * d = get_array_domain(s, i);
        expr * a = m_model.get_some_value(d);
        args.push_back(a);
    }
}

expr * array_factory::get_some_value(sort * s) {
    TRACE(array_factory, tout << mk_pp(s, m_manager) << "\n";);
    value_set * set = nullptr;
    if (m_sort2value_set.find(s, set) && !set->empty())
        return *(set->begin());
    func_interp * fi;
    expr * val = mk_array_interp(s, fi);
    fi->set_else(m_model.get_some_value(get_array_range(s)));
    return val;
}

bool array_factory::mk_two_diff_values_for(sort * s) {
    TRACE(array_factory, tout << mk_pp(s, m_manager) << "\n";);
    DEBUG_CODE({
        value_set * set = 0;
        SASSERT(!m_sort2value_set.find(s, set) || set->size() <= 1);
    });
    expr_ref r1(m_manager);
    expr_ref r2(m_manager);
    sort * range = get_array_range(s);
    if (!m_model.get_some_values(range, r1, r2))
        return false; // failed... the range is probably unit.
    ptr_buffer<expr> args;
    get_some_args_for(s, args);
    func_interp * fi1;
    func_interp * fi2;
    mk_array_interp(s, fi1);    
    mk_array_interp(s, fi2);
    fi1->insert_entry(args.data(), r1);
    fi2->insert_entry(args.data(), r2);
    DEBUG_CODE({
        value_set * set = 0;
        SASSERT(m_sort2value_set.find(s, set) && set->size() >= 2);
    });
    return true;
}

bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
    value_set * set = nullptr;
    if (!m_sort2value_set.find(s, set) || set->size() < 2) {
        if (!mk_two_diff_values_for(s)) {
            TRACE(array_factory_bug, tout << "could not create diff values: " << mk_pp(s, m_manager) << "\n";);
            return false;
        }
    }
    m_sort2value_set.find(s, set);
    SASSERT(set != 0);
    SASSERT(set->size() >= 2);
    
    value_set::iterator it = set->begin();
    v1 = *it;
    ++it;
    v2 = *it;
    TRACE(array_factory, tout << v1 << " " << v2 << "\n";);
    return true;    
}

//
// TODO: I have to check if the following procedure is really correct.
// I'm supporting partial arrays where the "else" can be set later by the model_finder or model classes.
// Projection functions may be also used.
//
// If projections are not used, then the following code should work if the "else" of a partial array
// is set with the result of some entry.
//
expr * array_factory::get_fresh_value(sort * s) {
    value_set * set = get_value_set(s);
    if (set->empty()) {
        // easy case 
        return get_some_value(s);
    }
    sort * range    = get_array_range(s);
    expr* range_val = nullptr;
    
    if (!m_ranges.contains(range)) {
        ptr_vector<sort>::scoped_stack _s(m_ranges);
        m_ranges.push_back(range);
        range_val = m_model.get_fresh_value(range);
        if (range_val != nullptr) {
            // easy case
            func_interp* fi;
            expr* val = mk_array_interp(s, fi);
            fi->set_else(range_val);
            return val;
        }
    }

    TRACE(array_factory_bug, tout << "array fresh value: using fresh index, range: " << mk_pp(range, m_manager) << "\n";);
    expr_ref v1(m_manager), v2(m_manager), w1(m_manager), w2(m_manager);
    if (m_model.get_some_values(range, v1, v2)) {
        // Claim: A is fresh if A[i1] = v1 and A[i2] = v2 where i1 and i2 are fresh values,
        // and v1 and v2 are distinct.
        //
        // Proof: let assume there is an Array A' such that A' = A.
        // Then A[i1] == A'[i1] and A[i2] == A'[i2]. Since, i1 and i2 are fresh,
        // A' does not have an entry for i1 or i2, So A'[i1] == A'[i2] == A'.m_else.
        // Thus, A[i1] == A[i2] which is a contradiction since v1 != v2 and A[i1] = v1 and A[i2] = v2. 
        TRACE(array_factory_bug, tout << "v1: " << mk_pp(v1, m_manager) << " v2: " << mk_pp(v2, m_manager) << "\n";);
        ptr_buffer<expr> args1;
        ptr_buffer<expr> args2;
        bool found = false;
        unsigned arity = get_array_arity(s);
        for (unsigned i = 0; i < arity; i++) {
            sort * d    = get_array_domain(s, i);
            if (!found) {
                expr * arg1 = m_model.get_fresh_value(d);
                expr * arg2 = m_model.get_fresh_value(d);
                if (arg1 != nullptr && arg2 != nullptr) {
                    found = true;
                    args1.push_back(arg1);
                    args2.push_back(arg2);
                    continue;
                }
            }
            expr * arg = m_model.get_some_value(d);
            args1.push_back(arg);
            args2.push_back(arg);
        }
        if (found) {
            func_interp * fi;
            expr * val = mk_array_interp(s, fi);
            fi->insert_entry(args1.data(), v1);
            fi->insert_entry(args2.data(), v2);
            return val;
        }
    }
    
    // TODO: use more expensive procedures to create a fresh array value.
    // Example: track the values used in the domain.
    
    // Remark: in the current implementation, this function
    // will never fail, since if a type is finite, then
    // type_pred will be applied and get_fresh_value will not
    // need to be used.
    
    // failed to create a fresh array value
    TRACE(array_factory_bug, tout << "failed to build fresh array value\n";);
    return nullptr;
}