1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_enode.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-19. 15 16 Revision History: 17 18 --*/ 19 #include "ast/ast_pp.h" 20 #include "smt/smt_context.h" 21 #include "smt/smt_enode.h" 22 23 namespace smt { 24 25 /** 26 \brief Initialize an enode in the given memory position. 27 */ init(ast_manager & m,void * mem,app2enode_t const & app2enode,app * owner,unsigned generation,bool suppress_args,bool merge_tf,unsigned iscope_lvl,bool cgc_enabled,bool update_children_parent)28 enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 29 unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, 30 bool cgc_enabled, bool update_children_parent) { 31 SASSERT(m.is_bool(owner) || !merge_tf); 32 enode * n = new (mem) enode(); 33 n->m_owner = owner; 34 n->m_root = n; 35 n->m_next = n; 36 n->m_cg = nullptr; 37 n->m_class_size = 1; 38 n->m_generation = generation; 39 n->m_func_decl_id = UINT_MAX; 40 n->m_mark = false; 41 n->m_mark2 = false; 42 n->m_interpreted = false; 43 n->m_suppress_args = suppress_args; 44 n->m_eq = m.is_eq(owner); 45 n->m_commutative = n->get_num_args() == 2 && owner->get_decl()->is_commutative(); 46 n->m_bool = m.is_bool(owner); 47 n->m_merge_tf = merge_tf; 48 n->m_cgc_enabled = cgc_enabled; 49 n->m_iscope_lvl = iscope_lvl; 50 n->m_lbl_hash = -1; 51 n->m_proof_is_logged = false; 52 unsigned num_args = n->get_num_args(); 53 for (unsigned i = 0; i < num_args; i++) { 54 enode * arg = app2enode[owner->get_arg(i)->get_id()]; 55 n->m_args[i] = arg; 56 SASSERT(n->get_arg(i) == arg); 57 if (update_children_parent) 58 arg->get_root()->m_parents.push_back(n); 59 } 60 TRACE("mk_enode_detail", tout << "new enode suppress_args: " << n->m_suppress_args << "\n";); 61 SASSERT(n->m_suppress_args == suppress_args); 62 return n; 63 } 64 mk(ast_manager & m,region & r,app2enode_t const & app2enode,app * owner,unsigned generation,bool suppress_args,bool merge_tf,unsigned iscope_lvl,bool cgc_enabled,bool update_children_parent)65 enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 66 unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, 67 bool cgc_enabled, bool update_children_parent) { 68 SASSERT(m.is_bool(owner) || !merge_tf); 69 unsigned sz = get_enode_size(suppress_args ? 0 : owner->get_num_args()); 70 void * mem = r.allocate(sz); 71 return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent); 72 } 73 mk_dummy(ast_manager & m,app2enode_t const & app2enode,app * owner)74 enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) { 75 unsigned sz = get_enode_size(owner->get_num_args()); 76 void * mem = alloc_svect(char, sz); 77 return init(m, mem, app2enode, owner, 0, false, false, 0, true, false); 78 } 79 del_eh(ast_manager & m,bool update_children_parent)80 void enode::del_eh(ast_manager & m, bool update_children_parent) { 81 SASSERT(m_class_size == 1); 82 SASSERT(m_root == this); 83 SASSERT(m_next == this); 84 unsigned num_args = get_num_args(); 85 for (unsigned i = 0; i < num_args; i++) { 86 enode * arg = get_arg(i); 87 if (update_children_parent) { 88 SASSERT(arg->get_root()->m_parents.back() == this); 89 arg->get_root()->m_parents.pop_back(); 90 } 91 } 92 this->~enode(); 93 } 94 get_num_th_vars() const95 unsigned enode::get_num_th_vars() const { 96 return m_th_var_list.size(); 97 } 98 99 /** 100 \brief Return the theory var (in theory th_id) associated with 101 the enode. 102 Return null_theory_var if the enode is not associated 103 with a variable of theory th_id 104 */ get_th_var(theory_id th_id) const105 theory_var enode::get_th_var(theory_id th_id) const { 106 return m_th_var_list.find(th_id); 107 } 108 109 /** 110 \brief Add the entry (v, id) to the list of theory variables. 111 */ add_th_var(theory_var v,theory_id id,region & r)112 void enode::add_th_var(theory_var v, theory_id id, region & r) { 113 m_th_var_list.add_var(v, id, r); 114 } 115 116 /** 117 \brief Replace the entry (v', id) with the entry (v, id). 118 The enode must have an entry (v', id) 119 */ replace_th_var(theory_var v,theory_id id)120 void enode::replace_th_var(theory_var v, theory_id id) { 121 m_th_var_list.replace(v, id); 122 } 123 124 /** 125 \brief Delete theory variable. It assumes the 126 enode is associated with a variable of the given theory. 127 */ del_th_var(theory_id id)128 void enode::del_th_var(theory_id id) { 129 m_th_var_list.del_var(id); 130 } 131 132 133 /** 134 \brief Push old value of generation on the context trail stack 135 and update the generation. 136 */ set_generation(context & ctx,unsigned generation)137 void enode::set_generation(context & ctx, unsigned generation) { 138 if (m_generation == generation) 139 return; 140 ctx.push_trail(value_trail<context, unsigned>(m_generation)); 141 m_generation = generation; 142 } 143 144 set_lbl_hash(context & ctx)145 void enode::set_lbl_hash(context & ctx) { 146 SASSERT(m_lbl_hash == -1); 147 // m_lbl_hash should be different from -1, if and only if, 148 // there is a pattern that contains the enode. So, 149 // I use a trail to restore the value of m_lbl_hash to -1. 150 ctx.push_trail(value_trail<context, signed char>(m_lbl_hash)); 151 unsigned h = hash_u(get_owner_id()); 152 m_lbl_hash = h & (APPROX_SET_CAPACITY - 1); 153 // propagate modification to the root m_lbls set. 154 approx_set & r_lbls = m_root->m_lbls; 155 if (!r_lbls.may_contain(m_lbl_hash)) { 156 ctx.push_trail(value_trail<context, approx_set>(r_lbls)); 157 r_lbls.insert(m_lbl_hash); 158 } 159 } 160 get_eq_enode_with_min_gen()161 enode * enode::get_eq_enode_with_min_gen() { 162 if (m_generation == 0) 163 return this; 164 enode * r = this; 165 enode * curr = this; 166 do { 167 if (curr->m_generation < r->m_generation) { 168 r = curr; 169 if (r->m_generation == 0) 170 return r; 171 } 172 curr = curr->m_next; 173 } 174 while (curr != this); 175 return r; 176 } 177 178 #ifdef Z3DEBUG check_invariant() const179 bool enode::check_invariant() const { 180 unsigned class_size = 0; 181 bool found_root = false; 182 bool found_this = false; 183 bool has_interpreted = false; 184 185 // "Equivalence" class structure. 186 enode const * curr = this; 187 do { 188 SASSERT(curr->m_root == m_root); 189 class_size++; 190 if (curr == m_root) 191 found_root = true; 192 if (curr == this) 193 found_this = true; 194 if (curr->is_interpreted()) 195 has_interpreted = true; 196 curr = curr->m_next; 197 } 198 while (curr != this); 199 200 SASSERT(found_root); 201 SASSERT(found_this); 202 SASSERT(this != m_root || class_size == m_class_size); 203 SASSERT(!has_interpreted || m_root->is_interpreted()); 204 205 // Parent use-list 206 if (this == m_root) { 207 for (enode* parent : m_parents) { 208 unsigned i = 0; 209 unsigned num_args = parent->get_num_args(); 210 SASSERT(num_args > 0); 211 for (; i < num_args; i++) { 212 enode * arg = parent->get_arg(i); 213 if (arg->get_root() == m_root) 214 break; 215 } 216 SASSERT(i < num_args); 217 } 218 } 219 220 // Proof tree 221 // m_root is reachable from "this" by following the transitivity proof 222 SASSERT(trans_reaches(m_root)); 223 SASSERT(check_parent_invariant()); 224 return true; 225 } 226 227 /** 228 \brief Return true if the node is n or n is reached following the 229 m_proof.m_target pointers 230 */ trans_reaches(enode * n) const231 bool enode::trans_reaches(enode * n) const { 232 const enode * curr = this; 233 while (curr != 0) { 234 if (curr == n) { 235 return true; 236 } 237 curr = curr->m_trans.m_target; 238 } 239 return false; 240 } 241 check_parent_invariant() const242 bool enode::check_parent_invariant() const { 243 if (this != m_root) 244 return true; 245 enode const * curr = m_root; 246 do { 247 if (curr != m_root) { 248 for (enode * p : curr->m_parents) { 249 if (!p->is_true_eq() && !m_root->contains_parent_congruent_to(p)) { 250 UNREACHABLE(); 251 } 252 } 253 } 254 curr = curr->m_next; 255 } 256 while (curr != m_root); 257 return true; 258 } 259 contains_parent_congruent_to(enode * p) const260 bool enode::contains_parent_congruent_to(enode * p) const { 261 for (enode* curr : m_parents) { 262 if (congruent(curr, p)) 263 return true; 264 } 265 return false; 266 } 267 268 #endif 269 display_lbls(std::ostream & out) const270 void enode::display_lbls(std::ostream & out) const { 271 out << "#" << get_owner_id() << " -> #" << get_root()->get_owner_id() << ", lbls: " << get_lbls() << ", plbls: " << get_plbls() 272 << ", root->lbls: " << get_root()->get_lbls() << ", root->plbls: " << get_root()->get_plbls(); 273 if (has_lbl_hash()) 274 out << ", lbl-hash: " << static_cast<int>(get_lbl_hash()); 275 out << "\n"; 276 } 277 congruent(enode * n1,enode * n2,bool & comm)278 bool congruent(enode * n1, enode * n2, bool & comm) { 279 comm = false; 280 if (n1->get_owner()->get_decl() != n2->get_owner()->get_decl()) 281 return false; 282 unsigned num_args = n1->get_num_args(); 283 if (num_args != n2->get_num_args()) 284 return false; 285 if (n1->is_commutative()) { 286 enode * c1_1 = n1->get_arg(0)->get_root(); 287 enode * c1_2 = n1->get_arg(1)->get_root(); 288 enode * c2_1 = n2->get_arg(0)->get_root(); 289 enode * c2_2 = n2->get_arg(1)->get_root(); 290 if (c1_1 == c2_1 && c1_2 == c2_2) { 291 return true; 292 } 293 if (c1_1 == c2_2 && c1_2 == c2_1) { 294 comm = true; 295 return true; 296 } 297 return false; 298 } 299 else { 300 for (unsigned i = 0; i < num_args; i++) 301 if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) 302 return false; 303 return true; 304 } 305 } 306 get_max_generation(unsigned num_enodes,enode * const * enodes)307 unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) { 308 unsigned max = 0; 309 for (unsigned i = 0; i < num_enodes; i++) { 310 unsigned curr = enodes[i]->get_generation(); 311 if (curr > max) 312 max = curr; 313 } 314 return max; 315 } 316 unmark_enodes(unsigned num_enodes,enode * const * enodes)317 void unmark_enodes(unsigned num_enodes, enode * const * enodes) { 318 for (unsigned i = 0; i < num_enodes; i++) 319 enodes[i]->unset_mark(); 320 } 321 unmark_enodes2(unsigned num_enodes,enode * const * enodes)322 void unmark_enodes2(unsigned num_enodes, enode * const * enodes) { 323 for (unsigned i = 0; i < num_enodes; i++) 324 enodes[i]->unset_mark2(); 325 } 326 tmp_enode()327 tmp_enode::tmp_enode(): 328 m_app(0), 329 m_capacity(0), 330 m_enode_data(nullptr) { 331 SASSERT(m_app.get_app()->get_decl() == 0); 332 set_capacity(5); 333 } 334 ~tmp_enode()335 tmp_enode::~tmp_enode() { 336 dealloc_svect(m_enode_data); 337 } 338 set_capacity(unsigned new_capacity)339 void tmp_enode::set_capacity(unsigned new_capacity) { 340 SASSERT(new_capacity > m_capacity); 341 if (m_enode_data) 342 dealloc_svect(m_enode_data); 343 m_capacity = new_capacity; 344 unsigned sz = sizeof(enode) + m_capacity * sizeof(enode*); 345 m_enode_data = alloc_svect(char, sz); 346 memset(m_enode_data, 0, sz); 347 enode * n = get_enode(); 348 n->m_owner = m_app.get_app(); 349 n->m_root = n; 350 n->m_next = n; 351 n->m_class_size = 1; 352 n->m_cgc_enabled = true; 353 n->m_func_decl_id = UINT_MAX; 354 } 355 set(func_decl * f,unsigned num_args,enode * const * args)356 enode * tmp_enode::set(func_decl * f, unsigned num_args, enode * const * args) { 357 if (num_args > m_capacity) 358 set_capacity(num_args * 2); 359 enode * r = get_enode(); 360 if (m_app.get_app()->get_decl() != f) { 361 r->m_func_decl_id = UINT_MAX; 362 } 363 m_app.set_decl(f); 364 m_app.set_num_args(num_args); 365 r->m_commutative = num_args == 2 && f->is_commutative(); 366 memcpy(get_enode()->m_args, args, sizeof(enode*)*num_args); 367 return r; 368 } 369 reset()370 void tmp_enode::reset() { 371 get_enode()->m_func_decl_id = UINT_MAX; 372 } 373 374 }; 375 376