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