1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_enode.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-18. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "util/id_var_list.h" 22 #include "util/approx_set.h" 23 #include "ast/ast.h" 24 #include "smt/smt_types.h" 25 #include "smt/smt_eq_justification.h" 26 27 28 namespace smt { 29 30 class context; 31 32 /** 33 \brief Justification for the transitivity rule. 34 */ 35 struct trans_justification { 36 enode * m_target; 37 eq_justification m_justification; trans_justificationtrans_justification38 trans_justification(): 39 m_target(nullptr), 40 m_justification(null_eq_justification) { 41 } 42 }; 43 44 /** \ brief Use sparse maps in SMT solver. 45 46 Define this to use hash maps rather than vectors over ast 47 nodes. This is useful in the case there are many solvers, each 48 referencing few nodes from a large ast manager. There is some 49 unknown performance penalty for this. */ 50 51 typedef ptr_vector<enode> app2enode_t; // app -> enode 52 typedef id_var_list<null_family_id, null_theory_var> theory_var_list; 53 54 class tmp_enode; 55 56 /** 57 \brief Additional data-structure for implementing congruence closure, 58 equality propagation, and the theory central bus of equalities. 59 */ 60 class enode { 61 app * m_owner; //!< The application that 'owns' this enode. 62 enode * m_root; //!< Representative of the equivalence class 63 enode * m_next; //!< Next element in the equivalence class. 64 enode * m_cg; 65 unsigned m_class_size; //!< Size of the equivalence class if the enode is the root. 66 unsigned m_generation; //!< Tracks how many quantifier instantiation rounds were needed to generate this enode. 67 68 unsigned m_func_decl_id; //!< Id generated by the congruence table for fast indexing. 69 70 unsigned m_mark:1; //!< Multi-purpose auxiliary mark. 71 unsigned m_mark2:1; //!< Multi-purpose auxiliary mark. 72 unsigned m_interpreted:1; //!< True if the node is an interpreted constant. 73 unsigned m_suppress_args:1; //!< True if the arguments of m_owner should not be accessed by this enode. 74 unsigned m_eq:1; //!< True if it is an equality 75 unsigned m_commutative:1; //!< True if commutative app 76 unsigned m_bool:1; //!< True if it is a boolean enode 77 unsigned m_merge_tf:1; //!< True if the enode should be merged with true/false when the associated boolean variable is assigned. 78 unsigned m_cgc_enabled:1; //!< True if congruence closure is enabled for this enode. 79 unsigned m_iscope_lvl; //!< When the enode was internalized 80 /* 81 The following property is valid for m_parents 82 83 If this = m_root, then for every term f(a) such that a->get_root() == m_root, 84 there is a f(b) in m_parents such that b->get_root() == m_root, and f(a) and f(b) are 85 congruent. 86 Remark: f(a) and f(b) may have other arguments. 87 88 Exception: If f(a) and f(b) are terms of the form (= a c) and (= b d), then 89 m_parents will not contains (= b d) if b->get_root() == d->get_root(). 90 91 Remark regarding relevancy propagation: relevancy is propagated to all 92 elements of an equivalence class. So, if there is a f(a) that is relevant, 93 then the congruent f(b) in m_parents will also be relevant. 94 */ 95 enode_vector m_parents; //!< Parent enodes of the equivalence class. 96 id_var_list<> m_th_var_list; //!< List of theories that 'care' about this enode. 97 trans_justification m_trans; //!< A justification for the enode being equal to its root. 98 bool m_proof_is_logged; //!< Indicates that the proof for the enode being equal to its root is in the log. 99 signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern 100 approx_set m_lbls; 101 approx_set m_plbls; 102 enode * m_args[0]; //!< Cached args 103 104 friend class context; 105 friend class conflict_resolution; 106 friend class quantifier_manager; 107 108 get_th_var_list()109 theory_var_list * get_th_var_list() { 110 return m_th_var_list.get_var() == null_theory_var ? nullptr : &m_th_var_list; 111 } 112 113 friend class set_merge_tf_trail; 114 /** 115 \brief Return true if the enode should be merged with the true (false) enodes when 116 the associated boolean variable is assigned to true (false). 117 */ merge_tf()118 bool merge_tf() const { 119 return m_merge_tf; 120 } 121 122 friend class add_th_var_trail; 123 friend class replace_th_var_trail; 124 125 void add_th_var(theory_var v, theory_id id, region & r); 126 127 void replace_th_var(theory_var v, theory_id id); 128 129 void del_th_var(theory_id id); 130 131 friend class tmp_enode; 132 133 static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 134 unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, 135 bool cgc_enabled, bool update_children_parent); 136 public: 137 get_enode_size(unsigned num_args)138 static unsigned get_enode_size(unsigned num_args) { 139 return sizeof(enode) + num_args * sizeof(enode*); 140 } 141 142 static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 143 unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl, 144 bool cgc_enabled, bool update_children_parent); 145 146 static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner); 147 del_dummy(enode * n)148 static void del_dummy(enode * n) { dealloc_svect(reinterpret_cast<char*>(n)); } 149 get_func_decl_id()150 unsigned get_func_decl_id() const { 151 return m_func_decl_id; 152 } 153 set_func_decl_id(unsigned id)154 void set_func_decl_id(unsigned id) { 155 m_func_decl_id = id; 156 } 157 mark_as_interpreted()158 void mark_as_interpreted() { 159 SASSERT(!m_interpreted); 160 SASSERT(m_owner->get_num_args() == 0); 161 SASSERT(m_class_size == 1); 162 m_interpreted = true; 163 } 164 165 166 void del_eh(ast_manager & m, bool update_children_parent = true); 167 get_owner()168 app * get_owner() const { return m_owner; } get_expr()169 app * get_expr() const { return m_owner; } 170 get_owner_id()171 unsigned get_owner_id() const { return m_owner->get_id(); } get_expr_id()172 unsigned get_expr_id() const { return m_owner->get_id(); } 173 get_decl()174 func_decl * get_decl() const { 175 return m_owner->get_decl(); 176 } 177 get_decl_id()178 unsigned get_decl_id() const { 179 return m_owner->get_decl()->get_decl_id(); 180 } 181 hash()182 unsigned hash() const { 183 return m_owner->hash(); 184 } 185 186 get_root()187 enode * get_root() const { 188 return m_root; 189 } 190 is_root()191 bool is_root() const { 192 return m_root == this; 193 } 194 set_root(enode * r)195 void set_root(enode* r) { 196 m_root = r; 197 } 198 get_next()199 enode * get_next() const { 200 return m_next; 201 } 202 get_num_args()203 unsigned get_num_args() const { 204 return m_suppress_args ? 0 : m_owner->get_num_args(); 205 } 206 get_arg(unsigned idx)207 enode * get_arg(unsigned idx) const { 208 SASSERT(idx < get_num_args()); 209 return m_args[idx]; 210 } 211 get_args()212 enode * const * get_args() const { 213 return m_args; 214 } 215 216 class const_args { 217 enode const& n; 218 public: const_args(enode const & n)219 const_args(enode const& n):n(n) {} const_args(enode const * n)220 const_args(enode const* n):n(*n) {} begin()221 enode_vector::const_iterator begin() const { return n.m_args; } end()222 enode_vector::const_iterator end() const { return n.m_args + n.get_num_args(); } 223 }; 224 225 class args { 226 enode & n; 227 public: args(enode & n)228 args(enode & n):n(n) {} args(enode * n)229 args(enode * n):n(*n) {} begin()230 enode_vector::iterator begin() const { return n.m_args; } end()231 enode_vector::iterator end() const { return n.m_args + n.get_num_args(); } 232 }; 233 get_const_args()234 const_args get_const_args() const { return const_args(this); } 235 get_class_size()236 unsigned get_class_size() const { 237 return m_class_size; 238 } 239 is_bool()240 bool is_bool() const { 241 return m_bool; 242 } 243 is_eq()244 bool is_eq() const { 245 return m_eq; 246 } 247 is_true_eq()248 bool is_true_eq() const { 249 return m_eq && get_arg(0)->get_root() == get_arg(1)->get_root(); 250 } 251 is_marked()252 bool is_marked() const { 253 return m_mark; 254 } 255 set_mark()256 void set_mark() { 257 SASSERT(!m_mark); m_mark = true; 258 } 259 unset_mark()260 void unset_mark() { 261 SASSERT(m_mark); m_mark = false; 262 } 263 is_marked2()264 bool is_marked2() const { 265 return m_mark2; 266 } 267 set_mark2()268 void set_mark2() { 269 SASSERT(!m_mark2); m_mark2 = true; 270 } 271 unset_mark2()272 void unset_mark2() { 273 SASSERT(m_mark2); m_mark2 = false; 274 } 275 is_interpreted()276 bool is_interpreted() const { 277 return m_interpreted; 278 } 279 280 /** 281 \brief Return true if node is not a constant and it is the root of its congruence class. 282 283 \remark if get_num_args() == 0, then is_cgr() = false. 284 */ is_cgr()285 bool is_cgr() const { 286 return m_cg == this; 287 } 288 get_cg()289 enode * get_cg() const { 290 return m_cg; 291 } 292 is_cgc_enabled()293 bool is_cgc_enabled() const { 294 return m_cgc_enabled; 295 } 296 is_commutative()297 bool is_commutative() const { 298 return m_commutative; 299 } 300 301 class const_parents { 302 enode const& n; 303 public: const_parents(enode const & _n)304 const_parents(enode const& _n):n(_n) {} const_parents(enode const * _n)305 const_parents(enode const* _n):n(*_n) {} begin()306 enode_vector::const_iterator begin() const { return n.begin_parents(); } end()307 enode_vector::const_iterator end() const { return n.end_parents(); } 308 }; 309 310 class parents { 311 enode& n; 312 public: parents(enode & _n)313 parents(enode & _n):n(_n) {} parents(enode * _n)314 parents(enode * _n):n(*_n) {} begin()315 enode_vector::iterator begin() const { return n.begin_parents(); } end()316 enode_vector::iterator end() const { return n.end_parents(); } 317 }; 318 get_parents()319 parents get_parents() { return parents(this); } 320 get_const_parents()321 const_parents get_const_parents() const { return const_parents(this); } 322 get_num_parents()323 unsigned get_num_parents() const { 324 return m_parents.size(); 325 } 326 begin_parents()327 enode_vector::iterator begin_parents() { 328 return m_parents.begin(); 329 } 330 end_parents()331 enode_vector::iterator end_parents() { 332 return m_parents.end(); 333 } 334 begin_parents()335 enode_vector::const_iterator begin_parents() const { 336 return m_parents.begin(); 337 } 338 end_parents()339 enode_vector::const_iterator end_parents() const { 340 return m_parents.end(); 341 } 342 343 class iterator { 344 enode* m_first; 345 enode* m_last; 346 public: iterator(enode * n,enode * m)347 iterator(enode* n, enode* m): m_first(n), m_last(m) {} 348 enode* operator*() { return m_first; } 349 iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->m_next; return *this; } 350 iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; } 351 bool operator==(iterator const& other) const { return m_last == other.m_last && m_first == other.m_first; } 352 bool operator!=(iterator const& other) const { return !(*this == other); } 353 }; 354 begin()355 iterator begin() { return iterator(this, nullptr); } end()356 iterator end() { return iterator(this, this); } 357 get_th_var_list()358 theory_var_list const * get_th_var_list() const { 359 return m_th_var_list.get_var() == null_theory_var ? nullptr : &m_th_var_list; 360 } 361 has_th_vars()362 bool has_th_vars() const { 363 return m_th_var_list.get_var() != null_theory_var; 364 } 365 366 unsigned get_num_th_vars() const; 367 368 theory_var get_th_var(theory_id th_id) const; 369 get_trans_justification()370 trans_justification get_trans_justification() { 371 return m_trans; 372 } 373 get_generation()374 unsigned get_generation() const { 375 return m_generation; 376 } 377 378 void set_generation(context & ctx, unsigned generation); 379 380 /** 381 \brief Return the enode n that is in the eqc of *this, and has the minimal generation. 382 That is, there is no other enode with smaller generation. 383 */ 384 enode * get_eq_enode_with_min_gen(); 385 get_iscope_lvl()386 unsigned get_iscope_lvl() const { 387 return m_iscope_lvl; 388 } 389 390 void set_lbl_hash(context & ctx); 391 has_lbl_hash()392 bool has_lbl_hash() const { 393 return m_lbl_hash >= 0; 394 } 395 get_lbl_hash()396 unsigned char get_lbl_hash() const { 397 SASSERT(m_lbl_hash >= 0 && static_cast<unsigned>(m_lbl_hash) < approx_set_traits<unsigned long long>::capacity); 398 return static_cast<unsigned char>(m_lbl_hash); 399 } 400 get_lbls()401 approx_set & get_lbls() { 402 return m_lbls; 403 } 404 get_plbls()405 approx_set & get_plbls() { 406 return m_plbls; 407 } 408 get_lbls()409 const approx_set & get_lbls() const { 410 return m_lbls; 411 } 412 get_plbls()413 const approx_set & get_plbls() const { 414 return m_plbls; 415 } 416 417 void display_lbls(std::ostream & out) const; 418 419 #ifdef Z3DEBUG 420 bool check_invariant() const; 421 bool trans_reaches(enode * n) const; 422 bool check_parent_invariant() const; 423 bool contains_parent_congruent_to(enode * p) const; 424 #endif 425 }; 426 same_eqc(enode const * n1,enode const * n2)427 inline bool same_eqc(enode const * n1 , enode const * n2) { return n1->get_root() == n2->get_root(); } 428 429 /** 430 \brief Return true, if n1 and n2 are congruent. 431 Set comm to true, if the nodes are congruent modulo commutativity. 432 */ 433 bool congruent(enode * n1, enode * n2, bool & comm); 434 congruent(enode * n1,enode * n2)435 inline bool congruent(enode * n1, enode * n2) { 436 bool aux; 437 return congruent(n1, n2, aux); 438 } 439 440 unsigned get_max_generation(unsigned num_enodes, enode * const * enodes); 441 442 void unmark_enodes(unsigned num_enodes, enode * const * enodes); 443 444 void unmark_enodes2(unsigned num_enodes, enode * const * enodes); 445 446 class tmp_enode { 447 tmp_app m_app; 448 unsigned m_capacity; 449 char * m_enode_data; get_enode()450 enode * get_enode() { return reinterpret_cast<enode*>(m_enode_data); } 451 void set_capacity(unsigned new_capacity); 452 public: 453 tmp_enode(); 454 ~tmp_enode(); 455 enode * set(func_decl * f, unsigned num_args, enode * const * args); 456 void reset(); 457 }; 458 459 }; 460 461 462