1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 subpaving_t.h 7 8 Abstract: 9 10 Subpaving template for non-linear arithmetic. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2012-07-31. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include<iostream> 22 #include "util/tptr.h" 23 #include "util/small_object_allocator.h" 24 #include "util/chashtable.h" 25 #include "util/parray.h" 26 #include "math/interval/interval.h" 27 #include "util/scoped_numeral_vector.h" 28 #include "math/subpaving/subpaving_types.h" 29 #include "util/params.h" 30 #include "util/statistics.h" 31 #include "util/lbool.h" 32 #include "util/id_gen.h" 33 #include "util/rlimit.h" 34 #ifdef _MSC_VER 35 #pragma warning(disable : 4200) 36 #pragma warning(disable : 4355) 37 #endif 38 39 namespace subpaving { 40 41 template<typename C> 42 class context_t { 43 public: 44 typedef typename C::numeral_manager numeral_manager; 45 typedef typename numeral_manager::numeral numeral; 46 47 /** 48 \brief Inequalities used to encode a problem. 49 */ 50 class ineq { 51 friend class context_t; 52 var m_x; 53 numeral m_val; 54 unsigned m_ref_count:30; 55 unsigned m_lower:1; 56 unsigned m_open:1; 57 public: x()58 var x() const { return m_x; } value()59 numeral const & value() const { return m_val; } is_lower()60 bool is_lower() const { return m_lower; } is_open()61 bool is_open() const { return m_open; } 62 void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc()); operatorlt_var_proc63 struct lt_var_proc { bool operator()(ineq const * a, ineq const * b) const { return a->m_x < b->m_x; } }; 64 }; 65 66 class node; 67 68 class constraint { 69 public: 70 enum kind { 71 CLAUSE, MONOMIAL, POLYNOMIAL 72 // TODO: add SIN, COS, TAN, ... 73 }; 74 protected: 75 kind m_kind; 76 uint64_t m_timestamp; 77 public: constraint(kind k)78 constraint(kind k):m_kind(k), m_timestamp(0) {} 79 get_kind()80 kind get_kind() const { return m_kind; } 81 82 // Return the timestamp of the last propagation visit timestamp()83 uint64_t timestamp() const { return m_timestamp; } 84 // Reset propagation visit time set_visited(uint64_t ts)85 void set_visited(uint64_t ts) { m_timestamp = ts; } 86 }; 87 88 /** 89 \brief Clauses in the problem description and lemmas learned during paving. 90 */ 91 class clause : public constraint { 92 friend class context_t; 93 unsigned m_size; //!< Number of atoms in the clause. 94 unsigned m_lemma:1; //!< True if it is a learned clause. 95 unsigned m_watched:1; //!< True if it we are watching this clause. All non-lemmas are watched. 96 unsigned m_num_jst:30; //!< Number of times it is used to justify some bound. 97 ineq * m_atoms[0]; get_obj_size(unsigned sz)98 static unsigned get_obj_size(unsigned sz) { return sizeof(clause) + sz*sizeof(ineq*); } 99 public: clause()100 clause():constraint(constraint::CLAUSE) {} size()101 unsigned size() const { return m_size; } watched()102 bool watched() const { return m_watched; } 103 ineq * operator[](unsigned i) const { SASSERT(i < size()); return m_atoms[i]; } 104 void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc()); 105 }; 106 107 class justification { 108 void * m_data; 109 public: 110 enum kind { 111 AXIOM = 0, 112 ASSUMPTION, 113 CLAUSE, 114 VAR_DEF 115 }; 116 117 justification(bool axiom = true) { 118 m_data = axiom ? reinterpret_cast<void*>(static_cast<size_t>(AXIOM)) : reinterpret_cast<void*>(static_cast<size_t>(ASSUMPTION)); 119 } justification(justification const & source)120 justification(justification const & source) { m_data = source.m_data; } justification(clause * c)121 explicit justification(clause * c) { m_data = TAG(void*, c, CLAUSE); } justification(var x)122 explicit justification(var x) { m_data = BOXTAGINT(void*, x, VAR_DEF); } 123 get_kind()124 kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); } is_clause()125 bool is_clause() const { return get_kind() == CLAUSE; } is_axiom()126 bool is_axiom() const { return get_kind() == AXIOM; } is_assumption()127 bool is_assumption() const { return get_kind() == ASSUMPTION; } is_var_def()128 bool is_var_def() const { return get_kind() == VAR_DEF; } 129 get_clause()130 clause * get_clause() const { 131 SASSERT(is_clause()); 132 return UNTAG(clause*, m_data); 133 } 134 get_var()135 var get_var() const { 136 SASSERT(is_var_def()); 137 return UNBOXINT(m_data); 138 } 139 140 bool operator==(justification const & other) const { return m_data == other.m_data; } 141 bool operator!=(justification const & other) const { return !operator==(other); } 142 }; 143 144 class bound { 145 friend class context_t; 146 numeral m_val; 147 unsigned m_x:29; 148 unsigned m_lower:1; 149 unsigned m_open:1; 150 unsigned m_mark:1; 151 uint64_t m_timestamp; 152 bound * m_prev; 153 justification m_jst; set_timestamp(uint64_t ts)154 void set_timestamp(uint64_t ts) { m_timestamp = ts; } 155 public: x()156 var x() const { return static_cast<var>(m_x); } value()157 numeral const & value() const { return m_val; } value()158 numeral & value() { return m_val; } is_lower()159 bool is_lower() const { return m_lower; } is_open()160 bool is_open() const { return m_open; } timestamp()161 uint64_t timestamp() const { return m_timestamp; } prev()162 bound * prev() const { return m_prev; } jst()163 justification jst() const { return m_jst; } 164 void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc()); 165 }; 166 167 struct bound_array_config { 168 typedef context_t value_manager; 169 typedef small_object_allocator allocator; 170 typedef bound * value; 171 static const bool ref_count = false; 172 static const bool preserve_roots = true; 173 static const unsigned max_trail_sz = 16; 174 static const unsigned factor = 2; 175 }; 176 177 // auxiliary declarations for parray_manager dec_ref(bound *)178 void dec_ref(bound *) {} inc_ref(bound *)179 void inc_ref(bound *) {} 180 181 typedef parray_manager<bound_array_config> bound_array_manager; 182 typedef typename bound_array_manager::ref bound_array; 183 184 /** 185 \brief Node in the context_t. 186 */ 187 class node { 188 bound_array_manager & m_bm; 189 bound_array m_lowers; 190 bound_array m_uppers; 191 var m_conflict; 192 unsigned m_id; 193 unsigned m_depth; 194 bound * m_trail; 195 node * m_parent; //!< parent node 196 node * m_first_child; 197 node * m_next_sibling; 198 // Doubly linked list of leaves to be processed 199 node * m_prev; 200 node * m_next; 201 public: 202 node(context_t & s, unsigned id); 203 node(node * parent, unsigned id); 204 // return unique identifier. id()205 unsigned id() const { return m_id; } bm()206 bound_array_manager & bm() const { return m_bm; } lowers()207 bound_array & lowers() { return m_lowers; } uppers()208 bound_array & uppers() { return m_uppers; } inconsistent()209 bool inconsistent() const { return m_conflict != null_var; } set_conflict(var x)210 void set_conflict(var x) { SASSERT(!inconsistent()); m_conflict = x; } trail_stack()211 bound * trail_stack() const { return m_trail; } parent_trail_stack()212 bound * parent_trail_stack() const { return m_parent == nullptr ? nullptr : m_parent->m_trail; } lower(var x)213 bound * lower(var x) const { return bm().get(m_lowers, x); } upper(var x)214 bound * upper(var x) const { return bm().get(m_uppers, x); } parent()215 node * parent() const { return m_parent; } first_child()216 node * first_child() const { return m_first_child; } next_sibling()217 node * next_sibling() const { return m_next_sibling; } prev()218 node * prev() const { return m_prev; } next()219 node * next() const { return m_next; } 220 /** 221 \brief Return true if x is unbounded in this node 222 */ is_unbounded(var x)223 bool is_unbounded(var x) const { return lower(x) == nullptr && upper(x) == nullptr; } 224 void push(bound * b); 225 set_first_child(node * n)226 void set_first_child(node * n) { m_first_child = n; } set_next_sibling(node * n)227 void set_next_sibling(node * n) { m_next_sibling = n; } set_next(node * n)228 void set_next(node * n) { m_next = n; } set_prev(node * n)229 void set_prev(node * n) { m_prev = n; } 230 depth()231 unsigned depth() const { return m_depth; } 232 }; 233 234 /** 235 \brief Intervals are just temporary place holders. 236 The pavers maintain bounds. 237 */ 238 struct interval { 239 bool m_constant; // Flag: constant intervals are pairs <node*, var> 240 // constant intervals 241 node * m_node; 242 var m_x; 243 // mutable intervals 244 numeral m_l_val; 245 bool m_l_inf; 246 bool m_l_open; 247 numeral m_u_val; 248 bool m_u_inf; 249 bool m_u_open; 250 intervalinterval251 interval():m_constant(false) {} set_constantinterval252 void set_constant(node * n, var x) { 253 m_constant = true; 254 m_node = n; 255 m_x = x; 256 } set_mutableinterval257 void set_mutable() { m_constant = false; } 258 }; 259 260 class interval_config { 261 public: 262 typedef typename C::numeral_manager numeral_manager; 263 typedef typename numeral_manager::numeral numeral; 264 typedef typename context_t::interval interval; 265 private: 266 numeral_manager & m_manager; 267 public: interval_config(numeral_manager & m)268 interval_config(numeral_manager & m):m_manager(m) {} 269 m()270 numeral_manager & m() const { return m_manager; } round_to_minus_inf()271 void round_to_minus_inf() { C::round_to_minus_inf(m()); } round_to_plus_inf()272 void round_to_plus_inf() { C::round_to_plus_inf(m()); } set_rounding(bool to_plus_inf)273 void set_rounding(bool to_plus_inf) { C::set_rounding(m(), to_plus_inf); } lower(interval const & a)274 numeral const & lower(interval const & a) const { 275 if (a.m_constant) { 276 bound * b = a.m_node->lower(a.m_x); 277 return b == nullptr ? a.m_l_val /* don't care */ : b->value(); 278 } 279 return a.m_l_val; 280 } upper(interval const & a)281 numeral const & upper(interval const & a) const { 282 if (a.m_constant) { 283 bound * b = a.m_node->upper(a.m_x); 284 return b == nullptr ? a.m_u_val /* don't care */ : b->value(); 285 } 286 return a.m_u_val; 287 } lower(interval & a)288 numeral & lower(interval & a) { SASSERT(!a.m_constant); return a.m_l_val; } upper(interval & a)289 numeral & upper(interval & a) { SASSERT(!a.m_constant); return a.m_u_val; } lower_is_inf(interval const & a)290 bool lower_is_inf(interval const & a) const { return a.m_constant ? a.m_node->lower(a.m_x) == nullptr : a.m_l_inf; } upper_is_inf(interval const & a)291 bool upper_is_inf(interval const & a) const { return a.m_constant ? a.m_node->upper(a.m_x) == nullptr : a.m_u_inf; } lower_is_open(interval const & a)292 bool lower_is_open(interval const & a) const { 293 if (a.m_constant) { 294 bound * b = a.m_node->lower(a.m_x); 295 return b == nullptr || b->is_open(); 296 } 297 return a.m_l_open; 298 } upper_is_open(interval const & a)299 bool upper_is_open(interval const & a) const { 300 if (a.m_constant) { 301 bound * b = a.m_node->upper(a.m_x); 302 return b == nullptr || b->is_open(); 303 } 304 return a.m_u_open; 305 } 306 // Setters set_lower(interval & a,numeral const & n)307 void set_lower(interval & a, numeral const & n) { SASSERT(!a.m_constant); m().set(a.m_l_val, n); } set_upper(interval & a,numeral const & n)308 void set_upper(interval & a, numeral const & n) { SASSERT(!a.m_constant); m().set(a.m_u_val, n); } set_lower_is_open(interval & a,bool v)309 void set_lower_is_open(interval & a, bool v) { SASSERT(!a.m_constant); a.m_l_open = v; } set_upper_is_open(interval & a,bool v)310 void set_upper_is_open(interval & a, bool v) { SASSERT(!a.m_constant); a.m_u_open = v; } set_lower_is_inf(interval & a,bool v)311 void set_lower_is_inf(interval & a, bool v) { SASSERT(!a.m_constant); a.m_l_inf = v; } set_upper_is_inf(interval & a,bool v)312 void set_upper_is_inf(interval & a, bool v) { SASSERT(!a.m_constant); a.m_u_inf = v; } 313 }; 314 315 typedef ::interval_manager<interval_config> interval_manager; 316 317 class definition : public constraint { 318 public: definition(typename constraint::kind k)319 definition(typename constraint::kind k):constraint(k) {} 320 }; 321 322 class monomial : public definition { 323 friend class context_t; 324 unsigned m_size; 325 power m_powers[0]; 326 monomial(unsigned sz, power const * pws); get_obj_size(unsigned sz)327 static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz*sizeof(power); } 328 public: size()329 unsigned size() const { return m_size; } get_power(unsigned idx)330 power const & get_power(unsigned idx) const { SASSERT(idx < size()); return m_powers[idx]; } get_powers()331 power const * get_powers() const { return m_powers; } x(unsigned idx)332 var x(unsigned idx) const { return get_power(idx).x(); } degree(unsigned idx)333 unsigned degree(unsigned idx) const { return get_power(idx).degree(); } 334 void display(std::ostream & out, display_var_proc const & proc = display_var_proc(), bool use_star = false) const; 335 }; 336 337 class polynomial : public definition { 338 friend class context_t; 339 unsigned m_size; 340 numeral m_c; 341 numeral * m_as; 342 var * m_xs; get_obj_size(unsigned sz)343 static unsigned get_obj_size(unsigned sz) { return sizeof(polynomial) + sz*sizeof(numeral) + sz*sizeof(var); } 344 public: polynomial()345 polynomial():definition(constraint::POLYNOMIAL) {} size()346 unsigned size() const { return m_size; } a(unsigned i)347 numeral const & a(unsigned i) const { return m_as[i]; } x(unsigned i)348 var x(unsigned i) const { return m_xs[i]; } xs()349 var const * xs() const { return m_xs; } as()350 numeral const * as() const { return m_as; } c()351 numeral const & c() const { return m_c; } 352 void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc = display_var_proc(), bool use_star = false) const; 353 }; 354 355 /** 356 \brief Watched element (aka occurrence) can be: 357 358 - A clause 359 - A definition (i.e., a variable) 360 361 Remark: we cannot use the two watched literal approach since we process multiple nodes. 362 */ 363 class watched { 364 public: 365 enum kind { CLAUSE=0, DEFINITION }; 366 private: 367 void * m_data; 368 public: watched()369 watched():m_data(nullptr) {} watched(var x)370 explicit watched(var x) { m_data = BOXTAGINT(void*, x, DEFINITION); } watched(clause * c)371 explicit watched(clause * c) { m_data = TAG(void*, c, CLAUSE); } get_kind()372 kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); } is_clause()373 bool is_clause() const { return get_kind() != DEFINITION; } is_definition()374 bool is_definition() const { return get_kind() == DEFINITION; } get_clause()375 clause * get_clause() const { SASSERT(is_clause()); return UNTAG(clause*, m_data); } get_var()376 var get_var() const { SASSERT(is_definition()); return UNBOXINT(m_data); } 377 bool operator==(watched const & other) const { return m_data == other.m_data; } 378 bool operator!=(watched const & other) const { return !operator==(other); } 379 }; 380 381 /** 382 \brief Abstract functor for selecting the next leaf node to be explored. 383 */ 384 class node_selector { 385 context_t * m_ctx; 386 public: node_selector(context_t * ctx)387 node_selector(context_t * ctx):m_ctx(ctx) {} ~node_selector()388 virtual ~node_selector() {} 389 ctx()390 context_t * ctx() const { return m_ctx; } 391 392 // Return the next leaf node to be processed. 393 // Front and back are the first and last nodes in the doubly linked list of 394 // leaf nodes. 395 // Remark: new nodes are always inserted in the front of the list. 396 virtual node * operator()(node * front, node * back) = 0; 397 }; 398 399 /** 400 \brief Abstract functor for selecting the next variable to branch. 401 */ 402 class var_selector { 403 context_t * m_ctx; 404 public: var_selector(context_t * ctx)405 var_selector(context_t * ctx):m_ctx(ctx) {} ~var_selector()406 virtual ~var_selector() {} 407 ctx()408 context_t * ctx() const { return m_ctx; } 409 410 // Return the next variable to branch. 411 virtual var operator()(node * n) = 0; 412 413 // ----------------------------------- 414 // 415 // Event handlers 416 // 417 // ----------------------------------- 418 419 // Invoked when a new variable is created. new_var_eh(var x)420 virtual void new_var_eh(var x) {} 421 // Invoked when node n is created new_node_eh(node * n)422 virtual void new_node_eh(node * n) {} 423 // Invoked before deleting node n. del_node_eh(node * n)424 virtual void del_node_eh(node * n) {} 425 // Invoked when variable x is used during conflict resolution. used_var_eh(node * n,var x)426 virtual void used_var_eh(node * n, var x) {} 427 }; 428 429 class node_splitter; 430 friend class node_splitter; 431 432 /** 433 \brief Abstract functor for creating children for node n by branching on a given variable. 434 */ 435 class node_splitter { 436 context_t * m_ctx; 437 public: node_splitter(context_t * ctx)438 node_splitter(context_t * ctx):m_ctx(ctx) {} ~node_splitter()439 virtual ~node_splitter() {} 440 ctx()441 context_t * ctx() const { return m_ctx; } mk_node(node * p)442 node * mk_node(node * p) { return ctx()->mk_node(p); } mk_decided_bound(var x,numeral const & val,bool lower,bool open,node * n)443 bound * mk_decided_bound(var x, numeral const & val, bool lower, bool open, node * n) { 444 return ctx()->mk_bound(x, val, lower, open, n, justification()); 445 } 446 447 /** 448 \brief Create children nodes for n by splitting on x. 449 450 \pre n is a leaf. The interval for x in n has more than one element. 451 */ 452 virtual void operator()(node * n, var x) = 0; 453 }; 454 455 /** 456 \brief Return most recent splitting var for node n. 457 */ 458 var splitting_var(node * n) const; 459 460 /** 461 \brief Return true if x is a definition. 462 */ is_definition(var x)463 bool is_definition(var x) const { return m_defs[x] != 0; } 464 465 typedef svector<watched> watch_list; 466 typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector; 467 468 private: 469 reslimit& m_limit; 470 C m_c; 471 bool m_arith_failed; //!< True if the arithmetic module produced an exception. 472 bool m_own_allocator; 473 small_object_allocator * m_allocator; 474 bound_array_manager m_bm; 475 interval_manager m_im; 476 scoped_numeral_vector m_num_buffer; 477 478 bool_vector m_is_int; 479 ptr_vector<definition> m_defs; 480 vector<watch_list> m_wlist; 481 482 ptr_vector<ineq> m_unit_clauses; 483 ptr_vector<clause> m_clauses; 484 ptr_vector<clause> m_lemmas; 485 486 id_gen m_node_id_gen; 487 488 uint64_t m_timestamp; 489 node * m_root; 490 // m_leaf_head is the head of a doubly linked list of leaf nodes to be processed. 491 node * m_leaf_head; 492 node * m_leaf_tail; 493 494 var m_conflict; 495 ptr_vector<bound> m_queue; 496 unsigned m_qhead; 497 498 display_var_proc m_default_display_proc; 499 display_var_proc * m_display_proc; 500 501 scoped_ptr<node_selector> m_node_selector; 502 scoped_ptr<var_selector> m_var_selector; 503 scoped_ptr<node_splitter> m_node_splitter; 504 505 svector<power> m_pws; 506 507 // Configuration 508 numeral m_epsilon; //!< If upper - lower < epsilon, then new bound is not propagated. 509 bool m_zero_epsilon; 510 numeral m_max_bound; //!< Bounds > m_max and < -m_max are not propagated 511 numeral m_minus_max_bound; //!< -m_max_bound 512 numeral m_nth_root_prec; //!< precision for computing the nth root 513 unsigned m_max_depth; //!< Maximum depth 514 unsigned m_max_nodes; //!< Maximum number of nodes in the tree 515 unsigned long long m_max_memory; // in bytes 516 517 // Counters 518 unsigned m_num_nodes; 519 520 // Statistics 521 unsigned m_num_conflicts; 522 unsigned m_num_mk_bounds; 523 unsigned m_num_splits; 524 unsigned m_num_visited; 525 526 // Temporary 527 numeral m_tmp1, m_tmp2, m_tmp3; 528 interval m_i_tmp1, m_i_tmp2, m_i_tmp3; 529 530 531 friend class node; 532 set_arith_failed()533 void set_arith_failed() { m_arith_failed = true; } 534 535 void checkpoint(); 536 bm()537 bound_array_manager & bm() { return m_bm; } im()538 interval_manager & im() { return m_im; } allocator()539 small_object_allocator & allocator() const { return *m_allocator; } 540 541 bound * mk_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst); 542 void del_bound(bound * b); 543 // Create a new bound and add it to the propagation queue. 544 void propagate_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst); 545 546 bool is_int(monomial const * m) const; 547 bool is_int(polynomial const * p) const; 548 is_monomial(var x)549 bool is_monomial(var x) const { return m_defs[x] != 0 && m_defs[x]->get_kind() == constraint::MONOMIAL; } get_monomial(var x)550 monomial * get_monomial(var x) const { SASSERT(is_monomial(x)); return static_cast<monomial*>(m_defs[x]); } is_polynomial(var x)551 bool is_polynomial(var x) const { return m_defs[x] != 0 && m_defs[x]->get_kind() == constraint::POLYNOMIAL; } get_polynomial(var x)552 polynomial * get_polynomial(var x) const { SASSERT(is_polynomial(x)); return static_cast<polynomial*>(m_defs[x]); } 553 static void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc, var x, numeral & k, bool lower, bool open); 554 void display(std::ostream & out, var x) const; 555 void display_definition(std::ostream & out, definition const * d, bool use_star = false) const; 556 void display(std::ostream & out, constraint * a, bool use_star = false) const; 557 void display(std::ostream & out, bound * b) const; 558 void display(std::ostream & out, ineq * a) const; 559 void display_params(std::ostream & out) const; 560 void add_unit_clause(ineq * a, bool axiom); 561 // Remark: Not all lemmas need to be watched. Some of them can be used to justify clauses only. 562 void add_clause_core(unsigned sz, ineq * const * atoms, bool lemma, bool watched); 563 void del_clause(clause * cls); 564 565 node * mk_node(node * parent = nullptr); 566 void del_node(node * n); 567 void del_nodes(); 568 569 void del(interval & a); 570 void del_clauses(ptr_vector<clause> & cs); 571 void del_unit_clauses(); 572 void del_clauses(); 573 void del_monomial(monomial * m); 574 void del_sum(polynomial * p); 575 void del_definitions(); 576 577 /** 578 \brief Insert n in the beginning of the doubly linked list of leaves. 579 580 \pre n is a leaf, and it is not already in the list. 581 */ 582 void push_front(node * n); 583 584 /** 585 \brief Insert n in the end of the doubly linked list of leaves. 586 587 \pre n is a leaf, and it is not already in the list. 588 */ 589 void push_back(node * n); 590 591 /** 592 \brief Remove n from the doubly linked list of leaves. 593 594 \pre n is a leaf, and it is in the list. 595 */ 596 void remove_from_leaf_dlist(node * n); 597 598 /** 599 \brief Remove all nodes from the leaf dlist. 600 */ 601 void reset_leaf_dlist(); 602 603 /** 604 \brief Add all leaves back to the leaf dlist. 605 */ 606 void rebuild_leaf_dlist(node * n); 607 608 // ----------------------------------- 609 // 610 // Propagation 611 // 612 // ----------------------------------- 613 614 /** 615 \brief Return true if the given node is in an inconsistent state. 616 */ inconsistent(node * n)617 bool inconsistent(node * n) const { return n->inconsistent(); } 618 619 /** 620 \brief Set a conflict produced by the bounds of x at the given node. 621 */ 622 void set_conflict(var x, node * n); 623 624 /** 625 \brief Return true if bound b may propagate a new bound using constraint c at node n. 626 */ 627 bool may_propagate(bound * b, constraint * c, node * n); 628 629 /** 630 \brief Normalize bound if x is integer. 631 632 Examples: 633 x < 2 --> x <= 1 634 x <= 2.3 --> x <= 2 635 */ 636 void normalize_bound(var x, numeral & val, bool lower, bool & open); 637 638 /** 639 \brief Return true if (x, k, lower, open) is a relevant new bound at node n. 640 That is, it improves the current bound, and satisfies m_epsilon and m_max_bound. 641 */ 642 bool relevant_new_bound(var x, numeral const & k, bool lower, bool open, node * n); 643 644 /** 645 \brief Return true if the lower and upper bounds of x are 0 at node n. 646 */ 647 bool is_zero(var x, node * n) const; 648 649 /** 650 \brief Return true if upper bound of x is 0 at node n. 651 */ 652 bool is_upper_zero(var x, node * n) const; 653 654 /** 655 \brief Return true if lower and upper bounds of x are conflicting at node n. That is, upper(x) < lower(x) 656 */ 657 bool conflicting_bounds(var x, node * n) const; 658 659 /** 660 \brief Return true if x is unbounded at node n. 661 */ is_unbounded(var x,node * n)662 bool is_unbounded(var x, node * n) const { return n->is_unbounded(x); } 663 664 /** 665 \brief Return true if b is the most recent lower/upper bound for variable b->x() at node n. 666 */ 667 bool most_recent(bound * b, node * n) const; 668 669 /** 670 \brief Add most recent bounds of node n into the propagation queue. 671 That is, all bounds b s.t. b is in the trail of n, but not in the tail of parent(n), and most_recent(b, n). 672 */ 673 void add_recent_bounds(node * n); 674 675 /** 676 \brief Propagate new bounds at node n using get_monomial(x) 677 \pre is_monomial(x) 678 */ 679 void propagate_monomial(var x, node * n); 680 void propagate_monomial_upward(var x, node * n); 681 void propagate_monomial_downward(var x, node * n, unsigned i); 682 683 /** 684 \brief Propagate new bounds at node n using get_polynomial(x) 685 \pre is_polynomial(x) 686 */ 687 void propagate_polynomial(var x, node * n); 688 // Propagate a new bound for y using the polynomial associated with x. x may be equal to y. 689 void propagate_polynomial(var x, node * n, var y); 690 691 /** 692 \brief Propagate new bounds at node n using clause c. 693 */ 694 void propagate_clause(clause * c, node * n); 695 696 /** 697 \brief Return the truth value of inequaliy t at node n. 698 */ 699 lbool value(ineq * t, node * n); 700 701 /** 702 \brief Propagate new bounds at node n using the definition of variable x. 703 \pre is_definition(x) 704 */ 705 void propagate_def(var x, node * n); 706 707 /** 708 \brief Propagate constraints in b->x()'s watch list. 709 */ 710 void propagate(node * n, bound * b); 711 712 /** 713 \brief Perform bound propagation at node n. 714 */ 715 void propagate(node * n); 716 717 /** 718 \brief Try to propagate at node n using all definitions. 719 */ 720 void propagate_all_definitions(node * n); 721 722 // ----------------------------------- 723 // 724 // Main 725 // 726 // ----------------------------------- 727 void init(); 728 729 /** 730 \brief Assert unit clauses in the node n. 731 */ 732 void assert_units(node * n); 733 734 // ----------------------------------- 735 // 736 // Debugging support 737 // 738 // ----------------------------------- 739 740 /** 741 \brief Return true if b is a bound for node n. 742 */ 743 bool is_bound_of(bound * b, node * n) const; 744 745 /** 746 \brief Check the consistency of the doubly linked list of leaves. 747 */ 748 bool check_leaf_dlist() const; 749 750 /** 751 \brief Check paving tree structure. 752 */ 753 bool check_tree() const; 754 755 /** 756 \brief Check main invariants. 757 */ 758 bool check_invariant() const; 759 760 public: 761 context_t(reslimit& lim, C const & c, params_ref const & p, small_object_allocator * a); 762 ~context_t(); 763 764 /** 765 \brief Return true if the arithmetic module failed. 766 */ arith_failed()767 bool arith_failed() const { return m_arith_failed; } 768 nm()769 numeral_manager & nm() const { return m_c.m(); } 770 num_vars()771 unsigned num_vars() const { return m_is_int.size(); } 772 is_int(var x)773 bool is_int(var x) const { SASSERT(x < num_vars()); return m_is_int[x]; } 774 775 /** 776 \brief Create a new variable. 777 */ 778 var mk_var(bool is_int); 779 780 /** 781 \brief Create the monomial xs[0]^ks[0] * ... * xs[sz-1]^ks[sz-1]. 782 The result is a variable y s.t. y = xs[0]^ks[0] * ... * xs[sz-1]^ks[sz-1]. 783 784 \pre for all i \in [0, sz-1] : ks[i] > 0 785 \pre sz > 0 786 */ 787 var mk_monomial(unsigned sz, power const * pws); 788 789 /** 790 \brief Create the sum c + as[0]*xs[0] + ... + as[sz-1]*xs[sz-1]. 791 The result is a variable y s.t. y = c + as[0]*xs[0] + ... + as[sz-1]*xs[sz-1]. 792 793 \pre sz > 0 794 \pre for all i \in [0, sz-1] : as[i] != 0 795 */ 796 var mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs); 797 798 /** 799 \brief Create an inequality. 800 */ 801 ineq * mk_ineq(var x, numeral const & k, bool lower, bool open); 802 void inc_ref(ineq * a); 803 void dec_ref(ineq * a); 804 805 /** 806 \brief Assert the clause atoms[0] \/ ... \/ atoms[sz-1] 807 \pre sz > 1 808 */ add_clause(unsigned sz,ineq * const * atoms)809 void add_clause(unsigned sz, ineq * const * atoms) { add_clause_core(sz, atoms, false, true); } 810 811 /** 812 \brief Assert a constraint of one of the forms: x < k, x > k, x <= k, x >= k. 813 814 If axiom == true, then the constraint is not tracked in proofs. 815 */ 816 void add_ineq(var x, numeral const & k, bool lower, bool open, bool axiom); 817 818 /** 819 \brief Store in the given vector all leaves of the paving tree. 820 */ 821 void collect_leaves(ptr_vector<node> & leaves) const; 822 823 /** 824 \brief Display constraints asserted in the subpaving. 825 */ 826 void display_constraints(std::ostream & out, bool use_star = false) const; 827 828 /** 829 \brief Display bounds for each leaf of the tree. 830 */ 831 void display_bounds(std::ostream & out) const; 832 833 void display_bounds(std::ostream & out, node * n) const; 834 set_display_proc(display_var_proc * p)835 void set_display_proc(display_var_proc * p) { m_display_proc = p; } 836 837 void updt_params(params_ref const & p); 838 839 static void collect_param_descrs(param_descrs & d); 840 841 void reset_statistics(); 842 843 void collect_statistics(statistics & st) const; 844 845 void operator()(); 846 }; 847 848 }; 849 850