1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     value_factory.h
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2008-10-28.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "util/obj_hashtable.h"
23 
24 /**
25    \brief Auxiliary object used during model construction.
26 */
27 class value_factory {
28 protected:
29     ast_manager & m_manager;
30     family_id     m_fid;
31 public:
32     value_factory(ast_manager & m, family_id fid);
33 
34     virtual ~value_factory();
35 
36     /**
37        \brief Return some value of the given sort. The result is always different from zero.
38     */
39     virtual expr * get_some_value(sort * s) = 0;
40 
41     /**
42        \brief Return two distinct values of the given sort. The results are stored in v1 and v2.
43        Return false if the intended interpretation of the given sort has only one element.
44     */
45     virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
46 
47     /**
48        \brief Return a fresh value of the given sort.
49        Return 0 if it is not possible to do that (e.g., the sort is finite).
50     */
51     virtual expr * get_fresh_value(sort * s) = 0;
52 
53     /**
54        \brief Used to register that the given value was used in model construction.
55        So, get_fresh_value cannot return this value anymore.
56     */
57     virtual void register_value(expr * n) = 0;
58 
get_family_id()59     family_id get_family_id() const { return m_fid; }
60 };
61 
62 class basic_factory : public value_factory {
63 public:
64     basic_factory(ast_manager & m);
65 
66     expr * get_some_value(sort * s) override;
67 
68     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override;
69 
70     expr * get_fresh_value(sort * s) override;
71 
register_value(expr * n)72     void register_value(expr * n) override { }
73 };
74 
75 /**
76    \brief Template for value factories for numeric (and enumeration-like) sorts
77 */
78 template<typename Number>
79 class simple_factory : public value_factory {
80 protected:
81     struct value_set {
82         obj_hashtable<expr> m_values;
83         Number              m_next;
value_setvalue_set84         value_set():
85             m_next(0) {
86         }
87     };
88 
89     typedef obj_map<sort, value_set *> sort2value_set;
90 
91     sort2value_set         m_sort2value_set;
92     expr_ref_vector        m_values;
93     sort_ref_vector        m_sorts;
94     ptr_vector<value_set>  m_sets;
95 
get_value_set(sort * s)96     value_set * get_value_set(sort * s) {
97         value_set * set = nullptr;
98         if (!m_sort2value_set.find(s, set)) {
99             set = alloc(value_set);
100             m_sort2value_set.insert(s, set);
101             m_sorts.push_back(s);
102             m_sets.push_back(set);
103         }
104         SASSERT(set != 0);
105         DEBUG_CODE({
106             value_set * set2 = 0;
107             SASSERT(m_sort2value_set.find(s, set2));
108             SASSERT(set == set2);
109         });
110         return set;
111     }
112 
113     virtual app * mk_value_core(Number const & val, sort * s) = 0;
114 
mk_value(Number const & val,sort * s,bool & is_new)115     app * mk_value(Number const & val, sort * s, bool & is_new) {
116         value_set * set = get_value_set(s);
117         app * new_val   = mk_value_core(val, s);
118         is_new          = false;
119         if (!set->m_values.contains(new_val)) {
120             m_values.push_back(new_val);
121             set->m_values.insert(new_val);
122             is_new = true;
123         }
124         SASSERT(set->m_values.contains(new_val));
125         return new_val;
126     }
127 
128 public:
simple_factory(ast_manager & m,family_id fid)129     simple_factory(ast_manager & m, family_id fid):
130         value_factory(m, fid),
131         m_values(m),
132         m_sorts(m) {
133     }
134 
~simple_factory()135     ~simple_factory() override {
136         std::for_each(m_sets.begin(), m_sets.end(), delete_proc<value_set>());
137     }
138 
get_some_value(sort * s)139     expr * get_some_value(sort * s) override {
140         value_set * set = nullptr;
141         expr * result = nullptr;
142         if (m_sort2value_set.find(s, set) && !set->m_values.empty())
143             result = *(set->m_values.begin());
144         else
145             result = mk_value(Number(0), s);
146         return result;
147     }
148 
get_some_values(sort * s,expr_ref & v1,expr_ref & v2)149     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
150         value_set * set = nullptr;
151         if (m_sort2value_set.find(s, set)) {
152             switch (set->m_values.size()) {
153             case 0:
154                 v1 = mk_value(Number(0), s);
155                 v2 = mk_value(Number(1), s);
156                 break;
157             case 1:
158                 v1 = *(set->m_values.begin());
159                 v2 = mk_value(Number(0), s);
160                 if (v1 == v2)
161                     v2 = mk_value(Number(1), s);
162                 break;
163             default:
164                 obj_hashtable<expr>::iterator it = set->m_values.begin();
165                 v1 = *it;
166                 ++it;
167                 v2 = *it;
168                 break;
169             }
170             SASSERT(v1 != v2);
171             return true;
172         }
173         v1 = mk_value(Number(0), s);
174         v2 = mk_value(Number(1), s);
175         return true;
176     }
177 
get_fresh_value(sort * s)178     expr * get_fresh_value(sort * s) override {
179         value_set * set  = get_value_set(s);
180         bool is_new      = false;
181         expr * result    = nullptr;
182         sort_info* s_info = s->get_info();
183         sort_size const* sz = s_info?&s_info->get_num_elements():nullptr;
184         bool has_max = false;
185         Number max_size(0);
186         if (sz && sz->is_finite() && sz->size() < UINT_MAX) {
187             unsigned usz = static_cast<unsigned>(sz->size());
188             max_size = Number(usz);
189             has_max = true;
190         }
191         Number start = set->m_next;
192         Number & next    = set->m_next;
193         while (!is_new) {
194             result = mk_value(next, s, is_new);
195             next++;
196             if (has_max && next > max_size + start) {
197                 return nullptr;
198             }
199         }
200         SASSERT(result != 0);
201         return result;
202     }
203 
register_value(expr * n)204     void register_value(expr * n) override {
205         sort * s = n->get_sort();
206         value_set * set  = get_value_set(s);
207         if (!set->m_values.contains(n)) {
208             m_values.push_back(n);
209             set->m_values.insert(n);
210         }
211     }
212 
mk_value(Number const & val,sort * s)213     virtual app * mk_value(Number const & val, sort * s) {
214         bool is_new;
215         return mk_value(val, s, is_new);
216     }
217 
get_num_sorts()218     unsigned get_num_sorts() const { return m_sorts.size(); }
219 
get_sort(unsigned idx)220     sort * get_sort(unsigned idx) const { return m_sorts.get(idx); }
221 };
222 
223 /**
224    \brief Factory for creating values for uninterpreted sorts and user
225    declared (uninterpreted) sorts.
226 */
227 class user_sort_factory : public simple_factory<unsigned> {
228     obj_hashtable<sort>  m_finite;   //!< set of sorts that are marked as finite.
229     obj_hashtable<expr>  m_empty_universe;
230     app * mk_value_core(unsigned const & val, sort * s) override;
231 public:
232     user_sort_factory(ast_manager & m);
~user_sort_factory()233     ~user_sort_factory() override {}
234 
235     /**
236        \brief Make the universe of \c s finite, by preventing new
237        elements to be added to its universe.
238     */
239     void freeze_universe(sort * s);
240 
241     /**
242        \brief Return true if the universe of \c s is frozen and finite.
243     */
is_finite(sort * s)244     bool is_finite(sort * s) const {
245         return m_finite.contains(s);
246     }
247 
248     /**
249        \brief Return the "known" universe of \c s. It doesn't matter whether
250        s is finite or not. If \c s is finite, then it is the whole universe.
251     */
252     obj_hashtable<expr> const & get_known_universe(sort * s) const;
253 
254     /**
255        \brief Return sorts with finite interpretations.
256     */
get_finite_sorts()257     obj_hashtable<sort> const & get_finite_sorts() const { return m_finite; }
258 
259     expr * get_some_value(sort * s) override;
260 
261     bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override;
262 
263     expr * get_fresh_value(sort * s) override;
264 
265     void register_value(expr * n) override;
266 };
267 
268 
269