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
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt_model_generator.h
Abstract:
The model generator builds a (partial) model for the ground
formulas in the logical context.
The model finder (smt_model_finder.h) tries to extend the
partial model to satisfy the quantifiers. Main invariant:
the new model still satisfies the ground formulas.
The model checker (smt_model_checker.h) checks whether the (new)
model satisfies the quantifiers. If it doesn't, new instances are
added.
Author:
Leonardo de Moura (leonardo) 2008-10-29.
Revision History:
--*/
#pragma once
#include "ast/ast.h"
#include "smt/smt_types.h"
#include "util/obj_hashtable.h"
#include "util/map.h"
#include "util/ref.h"
class value_factory;
class proto_model;
namespace smt {
// -----------------------------
//
// This module builds an interpretation for each relevant expression in the logical context.
//
// 1) The interpretation of boolean constants is their truth value in the logical context.
//
// 2) The interpretation of expressions associated with enodes is built using functors (model_value_proc).
// Theories as arrays and datatypes many need the interpretation of some expressions to be built before the interpretation of others.
// We say this is a dependency. Moreover, some values must be fresh. That is, they should be different
// from all other values associated with enodes of a given sort. For example, the array theory
// uses fresh values to make sure that some array constants are different from each other.
//
// So a dependency for building the interpretation of an enode N can be:
// a) a fresh value (stub) of sort S: it must be built after the interpretation of all enodes of sort S were assigned.
//
// b) an enode N': the interpretation of N' must be built before the interpretation of N.
//
// We say a 'source' is an fresh value or an enode. Note that every dependency is a source,
// but not every source is a dependency.
//
// We use these dependencies to sort (using a topological sort) the sources. The sorted 'sources' specify the
// order the interpretations will be built.
//
// Assumptions regarding dependencies:
//
// - They are acyclic.
//
// - All dependencies are marked as relevant.
//
// - A fresh value stub of sort S depends (implicitly) on all enodes of sort S (that are not associated with fresh values).
// So an enode of sort S may not have a dependency of sort S.
//
// ------------------------------
/**
\brief Stub for extra fresh value.
*/
struct extra_fresh_value {
expr* m_src;
sort * m_sort;
unsigned m_idx;
expr * m_value = nullptr;
public:
extra_fresh_value(expr * src, sort* s, unsigned idx):m_src(src), m_sort(s), m_idx(idx) {}
sort * get_sort() const { return m_sort; }
expr* get_src() const { return m_src; }
unsigned get_idx() const { return m_idx; }
void set_value(expr * n) { SASSERT(!m_value); m_value = n; }
expr * get_value() const { return m_value; }
};
/**
\brief Theories such as arrays and datatypes may need some values to be already available when
building a value. We say this a dependency. Object of this class are used to track such dependencies.
Example: to build the value (cons 10 nil), the values 10 and nil should be already available.
*/
class model_value_dependency {
bool m_fresh; //!< True if the dependency is a new fresh value;
union {
enode * m_enode; //!< When m_fresh == false, contains an enode dependency.
extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value
};
public:
model_value_dependency():m_fresh(true), m_value(nullptr) { }
explicit model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
explicit model_value_dependency(extra_fresh_value * v) :m_fresh(true), m_value(v) { SASSERT(v); }
bool is_fresh_value() const { return m_fresh; }
enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; }
extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; }
};
std::ostream& operator<<(std::ostream& out, model_value_dependency const& d);
typedef model_value_dependency source;
struct source_hash_proc {
unsigned operator()(source const & s) const { return s.is_fresh_value() ? hash_u_u(17, s.get_value()->get_idx()) : hash_u_u(13, s.get_enode()->get_owner_id()); }
};
struct source_eq_proc {
bool operator()(source const & s1, source const & s2) const {
if (s1.is_fresh_value() != s2.is_fresh_value())
return false;
if (s1.is_fresh_value())
return s1.get_value()->get_idx() == s2.get_value()->get_idx();
else
return s1.get_enode() == s2.get_enode();
}
};
typedef map<source, int, source_hash_proc, source_eq_proc> source2color;
/**
\brief Model value builder. This functor is used to specify the dependencies
needed to build a value, and to build the actual value.
*/
class model_value_proc {
public:
virtual ~model_value_proc() = default;
/**
\brief Fill result with the dependencies of this functor.
That is, to invoke mk_value, the dependencies in result must be constructed.
*/
virtual void get_dependencies(buffer<model_value_dependency> & result) {}
/**
\brief The array values has size equal to the size of the argument \c result in get_dependencies.
It contain the values built for the dependencies.
*/
virtual app * mk_value(model_generator & m, expr_ref_vector const & values) = 0;
/**
\brief Return true if it is associated with a fresh value.
*/
virtual bool is_fresh() const { return false; }
};
/**
\brief Simple model_value_proc. It has no dependencies, and
just returns a given expression.
*/
class expr_wrapper_proc : public model_value_proc {
app * m_value;
public:
expr_wrapper_proc(app * v):m_value(v) {}
app * mk_value(model_generator & m, expr_ref_vector const & values) override { return m_value; }
};
class fresh_value_proc : public model_value_proc {
extra_fresh_value * m_value;
public:
fresh_value_proc(extra_fresh_value * v):m_value(v) {}
void get_dependencies(buffer<model_value_dependency> & result) override;
app * mk_value(model_generator & m, expr_ref_vector const & values) override { return to_app(values[0]); }
bool is_fresh() const override { return true; }
};
/**
\brief Auxiliary class used during model generation.
*/
class model_generator {
ast_manager & m;
context * m_context;
ptr_vector<extra_fresh_value> m_extra_fresh_values;
unsigned m_fresh_idx;
obj_map<enode, app *> m_root2value;
ast_ref_vector m_asts;
ref<proto_model> m_model;
obj_hashtable<func_decl> m_hidden_ufs;
void init_model();
void mk_bool_model();
void mk_value_procs(obj_map<enode, model_value_proc *> & root2proc, ptr_vector<enode> & roots, ptr_vector<model_value_proc> & procs);
void mk_values();
bool include_func_interp(func_decl * f) const;
void mk_func_interps();
void finalize_theory_models();
void display(std::ostream & out);
void register_existing_model_values();
void register_macros();
bool visit_children(source const & src, ptr_vector<enode> const & roots, obj_map<enode, model_value_proc *> const & root2proc,
source2color & colors, obj_hashtable<sort> & already_traversed, svector<source> & todo);
void process_source(source const & src, ptr_vector<enode> const & roots, obj_map<enode, model_value_proc *> const & root2proc,
source2color & colors, obj_hashtable<sort> & already_traversed, svector<source> & todo, svector<source> & sorted_sources);
void top_sort_sources(ptr_vector<enode> const & roots, obj_map<enode, model_value_proc *> const & root2proc, svector<source> & sorted_sources);
struct scoped_reset {
model_generator& mg;
ptr_vector<model_value_proc>& procs;
scoped_reset(model_generator& mg, ptr_vector<model_value_proc>& procs);
~scoped_reset();
};
public:
model_generator(ast_manager & m);
~model_generator();
void reset();
void set_context(context * c) { SASSERT(m_context == 0); m_context = c; }
void register_factory(value_factory * f);
extra_fresh_value * mk_extra_fresh_value(expr * src, sort* s);
model_value_proc * mk_model_value(enode* r);
expr * get_some_value(sort * s);
proto_model & get_model() { SASSERT(m_model); return *m_model; }
void register_value(expr * val);
ast_manager & get_manager() { return m; }
proto_model* mk_model();
obj_map<enode, app *> const & get_root2value() const { return m_root2value; }
app * get_value(enode * n) const;
void hide(func_decl * f) {
if (!m_hidden_ufs.contains(f)) {
m_hidden_ufs.insert(f);
m.inc_ref(f);
}
}
};
}