1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_context.h 7 8 Abstract: 9 10 Logical context 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-18. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "smt/smt_clause.h" 22 #include "smt/smt_setup.h" 23 #include "smt/smt_enode.h" 24 #include "smt/smt_cg_table.h" 25 #include "smt/smt_b_justification.h" 26 #include "smt/smt_eq_justification.h" 27 #include "smt/smt_justification.h" 28 #include "smt/smt_bool_var_data.h" 29 #include "smt/smt_clause_proof.h" 30 #include "smt/smt_theory.h" 31 #include "smt/smt_quantifier.h" 32 #include "smt/smt_quantifier_stat.h" 33 #include "smt/smt_statistics.h" 34 #include "smt/smt_conflict_resolution.h" 35 #include "smt/smt_relevancy.h" 36 #include "smt/smt_induction.h" 37 #include "smt/smt_case_split_queue.h" 38 #include "smt/smt_almost_cg_table.h" 39 #include "smt/smt_failure.h" 40 #include "smt/asserted_formulas.h" 41 #include "smt/smt_types.h" 42 #include "smt/dyn_ack.h" 43 #include "ast/ast_smt_pp.h" 44 #include "smt/watch_list.h" 45 #include "util/trail.h" 46 #include "util/ref.h" 47 #include "util/timer.h" 48 #include "util/statistics.h" 49 #include "smt/fingerprints.h" 50 #include "smt/proto_model/proto_model.h" 51 #include "smt/user_propagator.h" 52 #include "model/model.h" 53 #include "solver/progress_callback.h" 54 #include <tuple> 55 56 // there is a significant space overhead with allocating 1000+ contexts in 57 // the case that each context only references a few expressions. 58 // Using a map instead of a vector for the literals can compress space 59 // consumption. 60 #define USE_BOOL_VAR_VECTOR 1 61 62 namespace smt { 63 64 class model_generator; 65 66 class context { 67 friend class model_generator; 68 friend class lookahead; 69 friend class parallel; 70 public: 71 statistics m_stats; 72 73 std::ostream& display_last_failure(std::ostream& out) const; 74 std::string last_failure_as_string() const; set_reason_unknown(char const * msg)75 void set_reason_unknown(char const* msg) { m_unknown = msg; } 76 void set_progress_callback(progress_callback *callback); 77 78 79 protected: 80 ast_manager & m; 81 smt_params & m_fparams; 82 params_ref m_params; 83 ::statistics m_aux_stats; 84 setup m_setup; 85 unsigned m_relevancy_lvl; 86 timer m_timer; 87 asserted_formulas m_asserted_formulas; 88 th_rewriter m_rewriter; 89 scoped_ptr<quantifier_manager> m_qmanager; 90 scoped_ptr<model_generator> m_model_generator; 91 scoped_ptr<relevancy_propagator> m_relevancy_propagator; 92 user_propagator* m_user_propagator; 93 random_gen m_random; 94 bool m_flushing; // (debug support) true when flushing 95 mutable unsigned m_lemma_id; 96 progress_callback * m_progress_callback; 97 unsigned m_next_progress_sample; 98 clause_proof m_clause_proof; 99 region m_region; 100 fingerprint_set m_fingerprints; 101 102 expr_ref_vector m_b_internalized_stack; // stack of the boolean expressions already internalized. 103 // Remark: boolean expressions can also be internalized as 104 // enodes. Examples: boolean expression nested in an 105 // uninterpreted function. 106 expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes. 107 quantifier_ref_vector m_l_internalized_stack; 108 109 ptr_vector<justification> m_justifications; 110 111 unsigned m_final_check_idx; // circular counter used for implementing fairness 112 113 bool m_is_auxiliary; // used to prevent unwanted information from being logged. 114 class parallel* m_par; 115 unsigned m_par_index; 116 117 // ----------------------------------- 118 // 119 // Equality & Uninterpreted functions 120 // 121 // ----------------------------------- 122 enode * m_true_enode; 123 enode * m_false_enode; 124 app2enode_t m_app2enode; // app -> enode 125 ptr_vector<enode> m_enodes; 126 plugin_manager<theory> m_theories; // mapping from theory_id -> theory 127 ptr_vector<theory> m_theory_set; // set of theories for fast traversal 128 vector<enode_vector> m_decl2enodes; // decl -> enode (for decls with arity > 0) 129 enode_vector m_empty_vector; 130 cg_table m_cg_table; 131 struct new_eq { 132 enode * m_lhs; 133 enode * m_rhs; 134 eq_justification m_justification; new_eqnew_eq135 new_eq() {} new_eqnew_eq136 new_eq(enode * lhs, enode * rhs, eq_justification const & js): 137 m_lhs(lhs), m_rhs(rhs), m_justification(js) {} 138 }; 139 svector<new_eq> m_eq_propagation_queue; 140 struct new_th_eq { 141 theory_id m_th_id; 142 theory_var m_lhs; 143 theory_var m_rhs; new_th_eqnew_th_eq144 new_th_eq():m_th_id(null_theory_id), m_lhs(null_theory_var), m_rhs(null_theory_var) {} new_th_eqnew_th_eq145 new_th_eq(theory_id id, theory_var l, theory_var r):m_th_id(id), m_lhs(l), m_rhs(r) {} 146 }; 147 svector<new_th_eq> m_th_eq_propagation_queue; 148 svector<new_th_eq> m_th_diseq_propagation_queue; 149 #ifdef Z3DEBUG 150 svector<new_th_eq> m_propagated_th_eqs; 151 svector<new_th_eq> m_propagated_th_diseqs; 152 svector<enode_pair> m_diseq_vector; 153 #endif 154 enode * m_is_diseq_tmp; // auxiliary enode used to find congruent equality atoms. 155 156 tmp_enode m_tmp_enode; 157 ptr_vector<almost_cg_table> m_almost_cg_tables; // temporary field for is_ext_diseq 158 159 // ----------------------------------- 160 // 161 // Boolean engine 162 // 163 // ----------------------------------- 164 #if USE_BOOL_VAR_VECTOR 165 svector<bool_var> m_expr2bool_var; // expr id -> bool_var 166 #else 167 u_map<bool_var> m_expr2bool_var; 168 #endif 169 ptr_vector<expr> m_bool_var2expr; // bool_var -> expr 170 signed_char_vector m_assignment; //!< mapping literal id -> assignment lbool 171 vector<watch_list> m_watches; //!< per literal 172 unsigned_vector m_lit_occs; //!< occurrence count of literals 173 svector<bool_var_data> m_bdata; //!< mapping bool_var -> data 174 svector<double> m_activity; 175 clause_vector m_aux_clauses; 176 clause_vector m_lemmas; 177 vector<clause_vector> m_clauses_to_reinit; 178 expr_ref_vector m_units_to_reassert; 179 svector<char> m_units_to_reassert_sign; 180 literal_vector m_assigned_literals; 181 typedef std::pair<clause*, literal_vector> tmp_clause; 182 vector<tmp_clause> m_tmp_clauses; 183 unsigned m_qhead; 184 unsigned m_simp_qhead; 185 int m_simp_counter; //!< can become negative 186 scoped_ptr<case_split_queue> m_case_split_queue; 187 scoped_ptr<induction> m_induction; 188 double m_bvar_inc; 189 bool m_phase_cache_on; 190 unsigned m_phase_counter; //!< auxiliary variable used to decide when to turn on/off phase caching 191 bool m_phase_default; //!< default phase when using phase caching 192 193 // A conflict is usually a single justification. That is, a justification 194 // for false. If m_not_l is not null_literal, then m_conflict is a 195 // justification for l, and the conflict is union of m_not_l and m_conflict; 196 // m_empty_clause is set to ensure that an empty clause generated in deep scope 197 // levels survives to the base level. 198 b_justification m_conflict; 199 literal m_not_l; 200 scoped_ptr<conflict_resolution> m_conflict_resolution; 201 proof_ref m_unsat_proof; 202 203 204 literal_vector m_atom_propagation_queue; 205 206 obj_map<expr, unsigned> m_cached_generation; 207 obj_hashtable<expr> m_cache_generation_visited; 208 dyn_ack_manager m_dyn_ack_manager; 209 210 // ----------------------------------- 211 // 212 // Model generation 213 // 214 // ----------------------------------- 215 proto_model_ref m_proto_model; 216 model_ref m_model; 217 std::string m_unknown; 218 void mk_proto_model(); reset_model()219 void reset_model() { m_model = nullptr; m_proto_model = nullptr; } 220 221 // ----------------------------------- 222 // 223 // Unsat core extraction 224 // 225 // ----------------------------------- 226 typedef u_map<expr *> literal2assumption; 227 literal_vector m_assumptions; 228 literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption 229 expr_ref_vector m_unsat_core; 230 231 unsigned m_last_position_log { 0 }; 232 svector<size_t> m_last_positions; 233 234 // ----------------------------------- 235 // 236 // Theory case split 237 // 238 // ----------------------------------- 239 uint_set m_all_th_case_split_literals; 240 vector<literal_vector> m_th_case_split_sets; 241 u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in 242 243 // ----------------------------------- 244 // 245 // Accessors 246 // 247 // ----------------------------------- 248 public: get_manager()249 ast_manager & get_manager() const { 250 return m; 251 } 252 get_rewriter()253 th_rewriter & get_rewriter() { 254 return m_rewriter; 255 } 256 get_fparams()257 smt_params & get_fparams() { 258 return m_fparams; 259 } 260 get_params()261 params_ref const & get_params() { 262 return m_params; 263 } 264 265 void updt_params(params_ref const& p); 266 267 bool get_cancel_flag(); 268 get_region()269 region & get_region() { 270 return m_region; 271 } 272 relevancy()273 bool relevancy() const { 274 return relevancy_lvl() > 0; 275 } 276 277 unsigned relevancy_lvl() const; 278 get_enode(expr const * n)279 enode * get_enode(expr const * n) const { 280 SASSERT(e_internalized(n)); 281 return m_app2enode[n->get_id()]; 282 } 283 284 /** 285 \brief Similar to get_enode, but returns 0 if n is to e_internalized. 286 */ find_enode(expr const * n)287 enode * find_enode(expr const * n) const { 288 return m_app2enode.get(n->get_id(), 0); 289 } 290 reset_bool_vars()291 void reset_bool_vars() { 292 m_expr2bool_var.reset(); 293 } 294 get_bool_var(expr const * n)295 bool_var get_bool_var(expr const * n) const { 296 return m_expr2bool_var[n->get_id()]; 297 } 298 get_bool_var(enode const * n)299 bool_var get_bool_var(enode const * n) const { 300 return get_bool_var(n->get_owner()); 301 } 302 get_bool_var_of_id(unsigned id)303 bool_var get_bool_var_of_id(unsigned id) const { 304 return m_expr2bool_var[id]; 305 } 306 get_bool_var_of_id_option(unsigned id)307 bool_var get_bool_var_of_id_option(unsigned id) const { 308 return m_expr2bool_var.get(id, null_bool_var); 309 } 310 311 #if USE_BOOL_VAR_VECTOR 312 set_bool_var(unsigned id,bool_var v)313 void set_bool_var(unsigned id, bool_var v) { 314 m_expr2bool_var.setx(id, v, null_bool_var); 315 } 316 #else 317 set_bool_var(unsigned id,bool_var v)318 void set_bool_var(unsigned id, bool_var v) { 319 if (v == null_bool_var) { 320 m_expr2bool_var.erase(id); 321 } 322 else { 323 m_expr2bool_var.insert(id, v); 324 } 325 } 326 #endif 327 get_lemmas()328 clause_vector const& get_lemmas() const { return m_lemmas; } 329 330 literal get_literal(expr * n) const; 331 has_enode(bool_var v)332 bool has_enode(bool_var v) const { 333 return m_bdata[v].is_enode(); 334 } 335 bool_var2enode(bool_var v)336 enode * bool_var2enode(bool_var v) const { 337 SASSERT(m_bdata[v].is_enode()); 338 return m_app2enode[m_bool_var2expr[v]->get_id()]; 339 } 340 enode2bool_var(enode const * n)341 bool_var enode2bool_var(enode const * n) const { 342 SASSERT(n->is_bool()); 343 SASSERT(n != m_false_enode); 344 return get_bool_var_of_id(n->get_owner_id()); 345 } 346 enode2literal(enode const * n)347 literal enode2literal(enode const * n) const { 348 SASSERT(n->is_bool()); 349 return n == m_false_enode ? false_literal : literal(enode2bool_var(n)); 350 } 351 get_num_bool_vars()352 unsigned get_num_bool_vars() const { 353 return m_b_internalized_stack.size(); 354 } 355 get_bdata(bool_var v)356 bool_var_data & get_bdata(bool_var v) { 357 return m_bdata[v]; 358 } 359 get_bdata(bool_var v)360 bool_var_data const & get_bdata(bool_var v) const { 361 return m_bdata[v]; 362 } 363 get_lit_assignment(unsigned lit_idx)364 lbool get_lit_assignment(unsigned lit_idx) const { 365 return static_cast<lbool>(m_assignment[lit_idx]); 366 } 367 get_assignment(literal l)368 lbool get_assignment(literal l) const { 369 return get_lit_assignment(l.index()); 370 } 371 get_assignment(bool_var v)372 lbool get_assignment(bool_var v) const { 373 return get_assignment(literal(v)); 374 } 375 assigned_literals()376 literal_vector const & assigned_literals() const { 377 return m_assigned_literals; 378 } 379 get_watch(literal l)380 watch_list const& get_watch(literal l) const { 381 return m_watches[l.index()]; 382 } 383 384 lbool get_assignment(expr * n) const; 385 386 // Similar to get_assignment, but returns l_undef if n is not internalized. 387 lbool find_assignment(expr * n) const; 388 389 lbool get_assignment(enode * n) const; 390 391 void get_assignments(expr_ref_vector& assignments); 392 get_justification(bool_var v)393 b_justification get_justification(bool_var v) const { 394 return get_bdata(v).justification(); 395 } 396 397 void set_justification(bool_var v, bool_var_data& d, b_justification const& j); 398 has_th_justification(bool_var v,theory_id th_id)399 bool has_th_justification(bool_var v, theory_id th_id) const { 400 b_justification js = get_justification(v); 401 return js.get_kind() == b_justification::JUSTIFICATION && js.get_justification()->get_from_theory() == th_id; 402 } 403 set_random_seed(unsigned s)404 void set_random_seed(unsigned s) { m_random.set_seed(s); } 405 get_random_value()406 int get_random_value() { return m_random(); } 407 is_searching()408 bool is_searching() const { return m_searching; } 409 get_activity_vector()410 svector<double> const & get_activity_vector() const { return m_activity; } 411 get_activity(bool_var v)412 double get_activity(bool_var v) const { return m_activity[v]; } 413 set_activity(bool_var v,double act)414 void set_activity(bool_var v, double act) { m_activity[v] = act; } 415 activity_changed(bool_var v,bool increased)416 void activity_changed(bool_var v, bool increased) { 417 if (increased) { 418 m_case_split_queue->activity_increased_eh(v); 419 } 420 else { 421 m_case_split_queue->activity_decreased_eh(v); 422 } 423 } 424 is_assumption(bool_var v)425 bool is_assumption(bool_var v) const { 426 return get_bdata(v).m_assumption; 427 } 428 is_assumption(literal l)429 bool is_assumption(literal l) const { 430 return is_assumption(l.var()); 431 } 432 is_marked(bool_var v)433 bool is_marked(bool_var v) const { 434 return get_bdata(v).m_mark; 435 } 436 set_mark(bool_var v)437 void set_mark(bool_var v) { 438 SASSERT(!is_marked(v)); 439 get_bdata(v).m_mark = true; 440 } 441 unset_mark(bool_var v)442 void unset_mark(bool_var v) { 443 SASSERT(is_marked(v)); 444 get_bdata(v).m_mark = false; 445 } 446 447 /** 448 \brief Return the scope level when v was assigned. 449 */ get_assign_level(bool_var v)450 unsigned get_assign_level(bool_var v) const { 451 return get_bdata(v).m_scope_lvl; 452 } 453 get_assign_level(literal l)454 unsigned get_assign_level(literal l) const { 455 return get_assign_level(l.var()); 456 } 457 458 /** 459 \brief Return the scope level when v was internalized. 460 */ get_intern_level(bool_var v)461 unsigned get_intern_level(bool_var v) const { 462 return get_bdata(v).get_intern_level(); 463 } 464 get_theory(theory_id th_id)465 theory * get_theory(theory_id th_id) const { 466 return m_theories.get_plugin(th_id); 467 } 468 theories()469 ptr_vector<theory> const& theories() const { return m_theories.plugins(); } 470 begin_theories()471 ptr_vector<theory>::const_iterator begin_theories() const { 472 return m_theories.begin(); 473 } 474 end_theories()475 ptr_vector<theory>::const_iterator end_theories() const { 476 return m_theories.end(); 477 } 478 get_scope_level()479 unsigned get_scope_level() const { 480 return m_scope_lvl; 481 } 482 get_base_level()483 unsigned get_base_level() const { 484 return m_base_lvl; 485 } 486 at_base_level()487 bool at_base_level() const { 488 return m_scope_lvl == m_base_lvl; 489 } 490 get_search_level()491 unsigned get_search_level() const { 492 return m_search_lvl; 493 } 494 at_search_level()495 bool at_search_level() const { 496 return m_scope_lvl == m_search_lvl; 497 } 498 tracking_assumptions()499 bool tracking_assumptions() const { 500 return !m_assumptions.empty() && m_search_lvl > m_base_lvl; 501 } 502 bool_var2expr(bool_var v)503 expr * bool_var2expr(bool_var v) const { 504 return m_bool_var2expr[v]; 505 } 506 literal2expr(literal l,expr_ref & result)507 void literal2expr(literal l, expr_ref & result) const { 508 if (l == true_literal) 509 result = m.mk_true(); 510 else if (l == false_literal) 511 result = m.mk_false(); 512 else if (l.sign()) 513 result = m.mk_not(bool_var2expr(l.var())); 514 else 515 result = bool_var2expr(l.var()); 516 } 517 literal2expr(literal l)518 expr_ref literal2expr(literal l) const { 519 expr_ref result(m); 520 literal2expr(l, result); 521 return result; 522 } 523 is_true(enode const * n)524 bool is_true(enode const * n) const { 525 return n == m_true_enode; 526 } 527 is_false(enode const * n)528 bool is_false(enode const * n) const { 529 return n == m_false_enode; 530 } 531 get_num_enodes_of(func_decl const * decl)532 unsigned get_num_enodes_of(func_decl const * decl) const { 533 unsigned id = decl->get_decl_id(); 534 return id < m_decl2enodes.size() ? m_decl2enodes[id].size() : 0; 535 } 536 enodes_of(func_decl const * d)537 enode_vector const& enodes_of(func_decl const * d) const { 538 unsigned id = d->get_decl_id(); 539 return id < m_decl2enodes.size() ? m_decl2enodes[id] : m_empty_vector; 540 } 541 begin_enodes_of(func_decl const * decl)542 enode_vector::const_iterator begin_enodes_of(func_decl const * decl) const { 543 unsigned id = decl->get_decl_id(); 544 return id < m_decl2enodes.size() ? m_decl2enodes[id].begin() : nullptr; 545 } 546 end_enodes_of(func_decl const * decl)547 enode_vector::const_iterator end_enodes_of(func_decl const * decl) const { 548 unsigned id = decl->get_decl_id(); 549 return id < m_decl2enodes.size() ? m_decl2enodes[id].end() : nullptr; 550 } 551 enodes()552 ptr_vector<enode> const& enodes() const { return m_enodes; } 553 begin_enodes()554 ptr_vector<enode>::const_iterator begin_enodes() const { 555 return m_enodes.begin(); 556 } 557 end_enodes()558 ptr_vector<enode>::const_iterator end_enodes() const { 559 return m_enodes.end(); 560 } 561 get_generation(quantifier * q)562 unsigned get_generation(quantifier * q) const { 563 return m_qmanager->get_generation(q); 564 } 565 566 /** 567 \brief Return true if the logical context internalized universal quantifiers. 568 */ internalized_quantifiers()569 bool internalized_quantifiers() const { 570 return !m_qmanager->empty(); 571 } 572 573 /** 574 \brief Return true if the logical context internalized or will internalize universal quantifiers. 575 */ has_quantifiers()576 bool has_quantifiers() const { 577 return m_asserted_formulas.has_quantifiers(); 578 } 579 580 fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) { 581 return m_fingerprints.insert(data, data_hash, num_args, args, def); 582 } 583 get_var_theory(bool_var v)584 theory_id get_var_theory(bool_var v) const { 585 return get_bdata(v).get_theory(); 586 } 587 588 /** 589 * flag to toggle quantifier tracing. 590 */ 591 bool m_coming_from_quant { false }; 592 593 594 friend class set_var_theory_trail; 595 void set_var_theory(bool_var v, theory_id tid); 596 597 // ----------------------------------- 598 // 599 // Backtracking support 600 // 601 // ----------------------------------- 602 protected: 603 typedef ptr_vector<trail<context> > trail_stack; 604 trail_stack m_trail_stack; 605 #ifdef Z3DEBUG 606 bool m_trail_enabled; 607 #endif 608 609 public: 610 template<typename TrailObject> push_trail(const TrailObject & obj)611 void push_trail(const TrailObject & obj) { 612 SASSERT(m_trail_enabled); 613 m_trail_stack.push_back(new (m_region) TrailObject(obj)); 614 } 615 push_trail_ptr(trail<context> * ptr)616 void push_trail_ptr(trail<context> * ptr) { 617 m_trail_stack.push_back(ptr); 618 } 619 620 protected: 621 622 unsigned m_scope_lvl; 623 unsigned m_base_lvl; 624 unsigned m_search_lvl; // It is greater than m_base_lvl when assumptions are used. Otherwise, it is equals to m_base_lvl 625 struct scope { 626 unsigned m_assigned_literals_lim; 627 unsigned m_trail_stack_lim; 628 unsigned m_aux_clauses_lim; 629 unsigned m_justifications_lim; 630 unsigned m_units_to_reassert_lim; 631 }; 632 struct base_scope { 633 unsigned m_lemmas_lim; 634 unsigned m_simp_qhead_lim; 635 unsigned m_inconsistent; 636 }; 637 638 svector<scope> m_scopes; 639 svector<base_scope> m_base_scopes; 640 641 void push_scope(); 642 643 unsigned pop_scope_core(unsigned num_scopes); 644 645 void pop_scope(unsigned num_scopes); 646 647 void undo_trail_stack(unsigned old_size); 648 649 void unassign_vars(unsigned old_lim); 650 651 void remove_watch_literal(clause * cls, unsigned idx); 652 653 void remove_cls_occs(clause * cls); 654 655 void del_clause(bool log, clause * cls); 656 657 void del_clauses(clause_vector & v, unsigned old_size); 658 659 void del_justifications(ptr_vector<justification> & justifications, unsigned old_lim); 660 661 bool is_unit_clause(clause const * c) const; 662 663 bool is_empty_clause(clause const * c) const; 664 665 void cache_generation(unsigned new_scope_lvl); 666 667 void cache_generation(clause const * cls, unsigned new_scope_lvl); 668 669 void cache_generation(unsigned num_lits, literal const * lits, unsigned new_scope_lvl); 670 671 void cache_generation(expr * n, unsigned new_scope_lvl); 672 673 void reset_cache_generation(); 674 675 void reinit_clauses(unsigned num_scopes, unsigned num_bool_vars); 676 677 void reassert_units(unsigned units_to_reassert_lim); 678 679 public: 680 // \brief exposed for PB solver to participate in GC 681 682 void remove_watch(bool_var v); 683 684 // ----------------------------------- 685 // 686 // Internalization 687 // 688 // ----------------------------------- 689 public: b_internalized(expr const * n)690 bool b_internalized(expr const * n) const { 691 return get_bool_var_of_id_option(n->get_id()) != null_bool_var; 692 } 693 lit_internalized(expr const * n)694 bool lit_internalized(expr const * n) const { 695 return m.is_false(n) || (m.is_not(n) ? b_internalized(to_app(n)->get_arg(0)) : b_internalized(n)); 696 } 697 e_internalized(expr const * n)698 bool e_internalized(expr const * n) const { 699 return m_app2enode.get(n->get_id(), 0) != 0; 700 } 701 get_num_b_internalized()702 unsigned get_num_b_internalized() const { 703 return m_b_internalized_stack.size(); 704 } 705 get_b_internalized(unsigned idx)706 expr * get_b_internalized(unsigned idx) const { 707 return m_b_internalized_stack.get(idx); 708 } 709 get_num_e_internalized()710 unsigned get_num_e_internalized() const { 711 return m_e_internalized_stack.size(); 712 } 713 get_e_internalized(unsigned idx)714 expr * get_e_internalized(unsigned idx) const { 715 return m_e_internalized_stack.get(idx); 716 } 717 718 /** 719 \brief Return the position (in the assignment stack) of the decision literal at the given scope level. 720 */ get_decision_literal_pos(unsigned scope_lvl)721 unsigned get_decision_literal_pos(unsigned scope_lvl) const { 722 SASSERT(scope_lvl > m_base_lvl); 723 return m_scopes[scope_lvl - 1].m_assigned_literals_lim; 724 } 725 726 protected: 727 unsigned m_generation; //!< temporary variable used during internalization 728 729 public: binary_clause_opt_enabled()730 bool binary_clause_opt_enabled() const { 731 return !m.proofs_enabled() && m_fparams.m_binary_clause_opt; 732 } 733 protected: get_bdata(expr const * n)734 bool_var_data & get_bdata(expr const * n) { 735 return get_bdata(get_bool_var(n)); 736 } 737 get_bdata(expr const * n)738 bool_var_data const & get_bdata(expr const * n) const { 739 return get_bdata(get_bool_var(n)); 740 } 741 742 typedef std::pair<expr *, bool> expr_bool_pair; 743 744 void ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited); 745 746 bool ts_visit_children(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo); 747 748 svector<expr_bool_pair> ts_todo; 749 char_vector tcolors; 750 char_vector fcolors; 751 752 bool should_internalize_rec(expr* e) const; 753 754 void top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & sorted_exprs); 755 756 void internalize_rec(expr * n, bool gate_ctx); 757 758 void internalize_deep(expr * n); 759 void internalize_deep(expr* const* n, unsigned num_exprs); 760 761 void assert_default(expr * n, proof * pr); 762 763 void assert_distinct(app * n, proof * pr); 764 765 void internalize_formula(expr * n, bool gate_ctx); 766 767 void internalize_eq(app * n, bool gate_ctx); 768 769 void internalize_distinct(app * n, bool gate_ctx); 770 771 bool internalize_theory_atom(app * n, bool gate_ctx); 772 773 void internalize_quantifier(quantifier * q, bool gate_ctx); 774 775 void internalize_lambda(quantifier * q); 776 777 void internalize_formula_core(app * n, bool gate_ctx); 778 779 void set_merge_tf(enode * n, bool_var v, bool is_new_var); 780 781 friend class set_enode_flag_trail; 782 783 public: 784 void set_enode_flag(bool_var v, bool is_new_var); 785 786 protected: 787 void internalize_term(app * n); 788 789 void internalize_ite_term(app * n); 790 791 bool internalize_theory_term(app * n); 792 793 void internalize_uninterpreted(app * n); 794 795 friend class mk_bool_var_trail; 796 class mk_bool_var_trail : public trail<context> { 797 public: undo(context & ctx)798 void undo(context & ctx) override { ctx.undo_mk_bool_var(); } 799 }; 800 mk_bool_var_trail m_mk_bool_var_trail; 801 void undo_mk_bool_var(); 802 803 friend class mk_enode_trail; 804 class mk_enode_trail : public trail<context> { 805 public: undo(context & ctx)806 void undo(context & ctx) override { ctx.undo_mk_enode(); } 807 }; 808 mk_enode_trail m_mk_enode_trail; 809 void undo_mk_enode(); 810 811 friend class mk_lambda_trail; 812 class mk_lambda_trail : public trail<context> { 813 public: undo(context & ctx)814 void undo(context & ctx) override { ctx.undo_mk_lambda(); } 815 }; 816 mk_lambda_trail m_mk_lambda_trail; 817 void undo_mk_lambda(); 818 819 820 void apply_sort_cnstr(app * term, enode * e); 821 822 bool simplify_aux_clause_literals(unsigned & num_lits, literal * lits, literal_buffer & simp_lits); 823 824 bool simplify_aux_lemma_literals(unsigned & num_lits, literal * lits); 825 826 void mark_for_reinit(clause * cls, unsigned scope_lvl, bool reinternalize_atoms); 827 828 unsigned get_max_iscope_lvl(unsigned num_lits, literal const * lits) const; 829 830 bool use_binary_clause_opt(literal l1, literal l2, bool lemma) const; 831 832 int select_learned_watch_lit(clause const * cls) const; 833 834 int select_watch_lit(clause const * cls, int starting_at) const; 835 836 void add_watch_literal(clause * cls, unsigned idx); 837 838 proof * mk_clause_def_axiom(unsigned num_lits, literal * lits, expr * root_gate); 839 840 public: 841 void mk_gate_clause(unsigned num_lits, literal * lits); 842 843 void mk_gate_clause(literal l1, literal l2); 844 845 void mk_gate_clause(literal l1, literal l2, literal l3); 846 847 void mk_gate_clause(literal l1, literal l2, literal l3, literal l4); 848 849 protected: 850 void mk_root_clause(unsigned num_lits, literal * lits, proof * pr); 851 852 void mk_root_clause(literal l1, literal l2, proof * pr); 853 854 void mk_root_clause(literal l1, literal l2, literal l3, proof * pr); 855 856 void add_and_rel_watches(app * n); 857 858 void add_or_rel_watches(app * n); 859 860 void add_ite_rel_watches(app * n); 861 862 void mk_not_cnstr(app * n); 863 864 void mk_and_cnstr(app * n); 865 866 void mk_or_cnstr(app * n); 867 868 void mk_iff_cnstr(app * n, bool sign); 869 870 void mk_ite_cnstr(app * n); 871 track_occs()872 bool track_occs() const { return m_fparams.m_phase_selection == PS_OCCURRENCE; } 873 874 void dec_ref(literal l); 875 876 void inc_ref(literal l); 877 878 void remove_lit_occs(clause const& cls, unsigned num_bool_vars); 879 880 void add_lit_occs(clause const& cls); 881 public: 882 883 void ensure_internalized(expr* e); 884 885 void internalize(expr * n, bool gate_ctx); 886 void internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx); 887 888 void internalize(expr * n, bool gate_ctx, unsigned generation); 889 890 clause * mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k = CLS_AUX, clause_del_eh * del_eh = nullptr); 891 892 void mk_clause(literal l1, literal l2, justification * j); 893 894 void mk_clause(literal l1, literal l2, literal l3, justification * j); 895 896 void mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k); 897 898 void mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) { 899 mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_AXIOM); 900 } 901 902 void mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params = 0, parameter * params = nullptr); 903 904 void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr); 905 906 void mk_th_axiom(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) { 907 mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params); 908 } 909 910 void mk_th_lemma(theory_id tid, literal l1, literal l2, unsigned num_params = 0, parameter * params = nullptr) { 911 literal ls[2] = { l1, l2 }; 912 mk_th_lemma(tid, 2, ls, num_params, params); 913 } 914 915 void mk_th_lemma(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr) { 916 literal ls[3] = { l1, l2, l3 }; 917 mk_th_lemma(tid, 3, ls, num_params, params); 918 } 919 920 void mk_th_lemma(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) { 921 mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA); 922 } 923 924 void mk_th_lemma(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) { 925 mk_th_lemma(tid, ls.size(), ls.c_ptr(), num_params, params); 926 } 927 928 /* 929 * Provide a hint to the core solver that the specified literals form a "theory case split". 930 * The core solver will enforce the condition that exactly one of these literals can be 931 * assigned 'true' at any time. 932 * We assume that the theory solver has already asserted the disjunction of these literals 933 * or some other axiom that means at least one of them must be assigned 'true'. 934 */ 935 void mk_th_case_split(unsigned num_lits, literal * lits); 936 937 938 /* 939 * Provide a hint to the branching heuristic about the priority of a "theory-aware literal". 940 * Literals marked in this way will always be branched on before unmarked literals, 941 * starting with the literal having the highest priority. 942 */ 943 void add_theory_aware_branching_info(bool_var v, double priority, lbool phase); 944 945 public: 946 947 // helper function for trail 948 void undo_th_case_split(literal l); 949 950 bool propagate_th_case_split(unsigned qhead); 951 952 bool_var mk_bool_var(expr * n); 953 954 enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled); 955 956 void attach_th_var(enode * n, theory * th, theory_var v); 957 958 template<typename Justification> mk_justification(Justification const & j)959 justification * mk_justification(Justification const & j) { 960 justification * js = new (m_region) Justification(j); 961 SASSERT(js->in_region()); 962 if (js->has_del_eh()) 963 m_justifications.push_back(js); 964 return js; 965 } 966 967 // ----------------------------------- 968 // 969 // Engine 970 // 971 // ----------------------------------- 972 protected: 973 lbool m_last_search_result; 974 failure m_last_search_failure; 975 ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model 976 bool m_searching; 977 unsigned m_num_conflicts; 978 unsigned m_num_conflicts_since_restart; 979 unsigned m_num_conflicts_since_lemma_gc; 980 unsigned m_num_restarts; 981 unsigned m_num_simplifications; 982 unsigned m_restart_threshold; 983 unsigned m_restart_outer_threshold; 984 unsigned m_luby_idx; 985 double m_agility; 986 unsigned m_lemma_gc_threshold; 987 988 void assign_core(literal l, b_justification j, bool decision = false); 989 void trace_assign(literal l, b_justification j, bool decision) const; 990 991 public: 992 void assign(literal l, const b_justification & j, bool decision = false) { 993 SASSERT(l != false_literal); 994 SASSERT(l != null_literal); 995 switch (get_assignment(l)) { 996 case l_false: 997 set_conflict(j, ~l); 998 break; 999 case l_undef: 1000 assign_core(l, j, decision); 1001 break; 1002 case l_true: 1003 return; 1004 } 1005 } 1006 1007 void assign(literal l, justification * j, bool decision = false) { 1008 assign(l, j ? b_justification(j) : b_justification::mk_axiom(), decision); 1009 } 1010 1011 friend class set_true_first_trail; 1012 void set_true_first_flag(bool_var v); 1013 try_true_first(bool_var v)1014 bool try_true_first(bool_var v) const { return get_bdata(v).try_true_first(); } 1015 1016 bool assume_eq(enode * lhs, enode * rhs); 1017 1018 bool is_shared(enode * n) const; 1019 assign_eq(enode * lhs,enode * rhs,eq_justification const & js)1020 void assign_eq(enode * lhs, enode * rhs, eq_justification const & js) { 1021 push_eq(lhs, rhs, js); 1022 } 1023 1024 /** 1025 \brief Force the given phase next time we case split v. 1026 This method has no effect if phase caching is disabled. 1027 */ force_phase(bool_var v,bool phase)1028 void force_phase(bool_var v, bool phase) { 1029 bool_var_data & d = get_bdata(v); 1030 d.m_phase_available = true; 1031 d.m_phase = phase; 1032 } 1033 force_phase(literal l)1034 void force_phase(literal l) { 1035 force_phase(l.var(), !l.sign()); 1036 } 1037 1038 bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings); 1039 1040 bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation, 1041 unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/); 1042 set_global_generation(unsigned generation)1043 void set_global_generation(unsigned generation) { m_generation = generation; } 1044 1045 #ifdef Z3DEBUG slow_contains_instance(quantifier const * q,unsigned num_bindings,enode * const * bindings)1046 bool slow_contains_instance(quantifier const * q, unsigned num_bindings, enode * const * bindings) const { 1047 return m_fingerprints.slow_contains(q, q->get_id(), num_bindings, bindings); 1048 } 1049 #endif 1050 1051 void add_eq(enode * n1, enode * n2, eq_justification js); 1052 1053 protected: 1054 void push_new_th_eq(theory_id th, theory_var lhs, theory_var rhs); 1055 1056 void push_new_th_diseq(theory_id th, theory_var lhs, theory_var rhs); 1057 1058 friend class add_eq_trail; 1059 1060 1061 void remove_parents_from_cg_table(enode * r1); 1062 1063 void reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js); 1064 1065 void invert_trans(enode * n); 1066 1067 theory_var get_closest_var(enode * n, theory_id th_id); 1068 1069 void merge_theory_vars(enode * r2, enode * r1, eq_justification js); 1070 1071 void propagate_bool_enode_assignment(enode * r1, enode * r2, enode * n1, enode * n2); 1072 1073 void propagate_bool_enode_assignment_core(enode * source, enode * target); 1074 1075 void undo_add_eq(enode * r1, enode * n1, unsigned r2_num_parents); 1076 1077 void restore_theory_vars(enode * r2, enode * r1); 1078 push_eq(enode * lhs,enode * rhs,eq_justification const & js)1079 void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { 1080 if (lhs->get_root() != rhs->get_root()) { 1081 SASSERT(m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner())); 1082 m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); 1083 } 1084 } 1085 push_new_congruence(enode * n1,enode * n2,bool used_commutativity)1086 void push_new_congruence(enode * n1, enode * n2, bool used_commutativity) { 1087 SASSERT(n1->m_cg == n2); 1088 // if (is_relevant(n1)) mark_as_relevant(n2); 1089 push_eq(n1, n2, eq_justification::mk_cg(used_commutativity)); 1090 } 1091 1092 bool add_diseq(enode * n1, enode * n2); 1093 1094 void assign_quantifier(quantifier * q); 1095 1096 void set_conflict(const b_justification & js, literal not_l); 1097 set_conflict(const b_justification & js)1098 void set_conflict(const b_justification & js) { 1099 set_conflict(js, null_literal); 1100 } 1101 1102 public: set_conflict(justification * js)1103 void set_conflict(justification * js) { 1104 SASSERT(js); 1105 set_conflict(b_justification(js)); 1106 } 1107 inconsistent()1108 bool inconsistent() const { 1109 return m_conflict != null_b_justification || 1110 m_asserted_formulas.inconsistent(); 1111 } 1112 1113 bool has_case_splits(); 1114 get_num_conflicts()1115 unsigned get_num_conflicts() const { 1116 return m_num_conflicts; 1117 } 1118 is_eq(enode const * n1,enode const * n2)1119 static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); } 1120 1121 bool is_diseq(enode * n1, enode * n2) const; 1122 1123 bool is_diseq_slow(enode * n1, enode * n2) const; 1124 1125 bool is_ext_diseq(enode * n1, enode * n2, unsigned depth); 1126 1127 enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args); 1128 1129 protected: 1130 bool decide(); 1131 1132 void update_phase_cache_counter(); 1133 1134 #define ACTIVITY_LIMIT 1e100 1135 #define INV_ACTIVITY_LIMIT 1e-100 1136 1137 void rescale_bool_var_activity(); 1138 1139 public: inc_bvar_activity(bool_var v)1140 void inc_bvar_activity(bool_var v) { 1141 double & act = m_activity[v]; 1142 act += m_bvar_inc; 1143 if (act > ACTIVITY_LIMIT) 1144 rescale_bool_var_activity(); 1145 m_case_split_queue->activity_increased_eh(v); 1146 TRACE("case_split", tout << "v" << v << " " << m_bvar_inc << " -> " << act << "\n";); 1147 } 1148 1149 protected: 1150 decay_bvar_activity()1151 void decay_bvar_activity() { 1152 m_bvar_inc *= m_fparams.m_inv_decay; 1153 } 1154 1155 bool simplify_clause(clause& cls); 1156 1157 unsigned simplify_clauses(clause_vector & clauses, unsigned starting_at); 1158 1159 void simplify_clauses(); 1160 1161 /** 1162 \brief Return true if the give clause is justifying some literal. 1163 */ is_justifying(clause * cls)1164 bool is_justifying(clause * cls) const { 1165 for (unsigned i = 0; i < 2; i++) { 1166 b_justification js; 1167 js = get_justification((*cls)[i].var()); 1168 if (js.get_kind() == b_justification::CLAUSE && js.get_clause() == cls) 1169 return true; 1170 } 1171 return false; 1172 } 1173 can_delete(clause * cls)1174 bool can_delete(clause * cls) const { 1175 if (cls->in_reinit_stack()) 1176 return false; 1177 return !is_justifying(cls); 1178 } 1179 1180 void del_inactive_lemmas(); 1181 1182 void del_inactive_lemmas1(); 1183 1184 void del_inactive_lemmas2(); 1185 1186 bool more_than_k_unassigned_literals(clause * cls, unsigned k); 1187 1188 void internalize_assertions(); 1189 1190 void asserted_inconsistent(); 1191 1192 bool validate_assumptions(expr_ref_vector const& asms); 1193 1194 void init_assumptions(expr_ref_vector const& asms); 1195 1196 void init_clause(expr_ref_vector const& clause); 1197 1198 lbool decide_clause(); 1199 1200 void reset_tmp_clauses(); 1201 1202 void reset_assumptions(); 1203 1204 void add_theory_assumptions(expr_ref_vector & theory_assumptions); 1205 1206 lbool mk_unsat_core(lbool result); 1207 1208 bool should_research(lbool result); 1209 1210 void validate_unsat_core(); 1211 1212 void init_search(); 1213 1214 void end_search(); 1215 1216 lbool search(); 1217 1218 void inc_limits(); 1219 1220 bool restart(lbool& status, unsigned curr_lvl); 1221 1222 void tick(unsigned & counter) const; 1223 1224 lbool bounded_search(); 1225 1226 final_check_status final_check(); 1227 1228 void check_proof(proof * pr); 1229 1230 void forget_phase_of_vars_in_current_level(); 1231 1232 virtual bool resolve_conflict(); 1233 1234 1235 // ----------------------------------- 1236 // 1237 // Propagation 1238 // 1239 // ----------------------------------- 1240 protected: 1241 bool bcp(); 1242 1243 bool propagate_eqs(); 1244 1245 bool propagate_atoms(); 1246 1247 void push_new_th_diseqs(enode * r, theory_var v, theory * th); 1248 1249 void propagate_bool_var_enode(bool_var v); 1250 is_relevant_core(expr * n)1251 bool is_relevant_core(expr * n) const { return m_relevancy_propagator->is_relevant(n); } 1252 1253 bool_vector m_relevant_conflict_literals; 1254 void record_relevancy(unsigned n, literal const* lits); 1255 void restore_relevancy(unsigned n, literal const* lits); 1256 1257 public: 1258 // event handler for relevancy_propagator class 1259 void relevant_eh(expr * n); 1260 is_relevant(expr * n)1261 bool is_relevant(expr * n) const { 1262 return !relevancy() || is_relevant_core(n); 1263 } 1264 is_relevant(enode * n)1265 bool is_relevant(enode * n) const { 1266 return is_relevant(n->get_owner()); 1267 } 1268 is_relevant(bool_var v)1269 bool is_relevant(bool_var v) const { 1270 return is_relevant(bool_var2expr(v)); 1271 } 1272 is_relevant(literal l)1273 bool is_relevant(literal l) const { 1274 SASSERT(l != true_literal && l != false_literal); 1275 return is_relevant(l.var()); 1276 } 1277 is_relevant_core(literal l)1278 bool is_relevant_core(literal l) const { 1279 return is_relevant_core(bool_var2expr(l.var())); 1280 } 1281 mark_as_relevant(expr * n)1282 void mark_as_relevant(expr * n) { m_relevancy_propagator->mark_as_relevant(n); m_relevancy_propagator->propagate(); } 1283 mark_as_relevant(enode * n)1284 void mark_as_relevant(enode * n) { mark_as_relevant(n->get_owner()); } 1285 mark_as_relevant(bool_var v)1286 void mark_as_relevant(bool_var v) { mark_as_relevant(bool_var2expr(v)); } 1287 mark_as_relevant(literal l)1288 void mark_as_relevant(literal l) { mark_as_relevant(l.var()); } 1289 1290 template<typename Eh> mk_relevancy_eh(Eh const & eh)1291 relevancy_eh * mk_relevancy_eh(Eh const & eh) { 1292 return m_relevancy_propagator->mk_relevancy_eh(eh); 1293 } 1294 add_relevancy_eh(expr * source,relevancy_eh * eh)1295 void add_relevancy_eh(expr * source, relevancy_eh * eh) { m_relevancy_propagator->add_handler(source, eh); } add_relevancy_dependency(expr * source,expr * target)1296 void add_relevancy_dependency(expr * source, expr * target) { m_relevancy_propagator->add_dependency(source, target); } add_rel_watch(literal l,relevancy_eh * eh)1297 void add_rel_watch(literal l, relevancy_eh * eh) { m_relevancy_propagator->add_watch(bool_var2expr(l.var()), !l.sign(), eh); } add_rel_watch(literal l,expr * n)1298 void add_rel_watch(literal l, expr * n) { m_relevancy_propagator->add_watch(bool_var2expr(l.var()), !l.sign(), n); } 1299 1300 protected: 1301 lbool get_assignment_core(expr * n) const; 1302 1303 void propagate_relevancy(unsigned qhead); 1304 1305 bool propagate_theories(); 1306 1307 void propagate_th_eqs(); 1308 1309 void propagate_th_diseqs(); 1310 1311 bool can_theories_propagate() const; 1312 1313 bool propagate(); 1314 1315 void add_rec_funs_to_model(); 1316 1317 public: 1318 bool can_propagate() const; 1319 1320 induction& get_induction(); 1321 1322 // Retrieve arithmetic values. 1323 bool get_arith_lo(expr* e, rational& lo, bool& strict); 1324 bool get_arith_up(expr* e, rational& up, bool& strict); 1325 bool get_arith_value(expr* e, rational& value); 1326 1327 // ----------------------------------- 1328 // 1329 // Model checking... (must be improved) 1330 // 1331 // ----------------------------------- 1332 public: 1333 bool get_value(enode * n, expr_ref & value); 1334 1335 // ----------------------------------- 1336 // 1337 // Pretty Printing 1338 // 1339 // ----------------------------------- 1340 protected: 1341 ast_mark m_pp_visited; 1342 get_pp_visited()1343 ast_mark & get_pp_visited() const { return const_cast<ast_mark&>(m_pp_visited); } 1344 1345 public: 1346 void display_enode_defs(std::ostream & out) const; 1347 1348 void display_bool_var_defs(std::ostream & out) const; 1349 1350 void display_asserted_formulas(std::ostream & out) const; 1351 1352 std::ostream& display_literal(std::ostream & out, literal l) const; 1353 display_detailed_literal(std::ostream & out,literal l)1354 std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m, m_bool_var2expr.c_ptr()); return out; } 1355 1356 void display_literal_info(std::ostream & out, literal l) const; 1357 1358 std::ostream& display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const; 1359 display_literals(std::ostream & out,literal_vector const & lits)1360 std::ostream& display_literals(std::ostream & out, literal_vector const& lits) const { 1361 return display_literals(out, lits.size(), lits.c_ptr()); 1362 } 1363 1364 std::ostream& display_literal_smt2(std::ostream& out, literal lit) const; 1365 display_literals_smt2(std::ostream & out,literal l1,literal l2)1366 std::ostream& display_literals_smt2(std::ostream& out, literal l1, literal l2) const { literal ls[2] = { l1, l2 }; return display_literals_smt2(out, 2, ls); } 1367 1368 std::ostream& display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const; 1369 display_literals_smt2(std::ostream & out,literal_vector const & ls)1370 std::ostream& display_literals_smt2(std::ostream& out, literal_vector const& ls) const { return display_literals_smt2(out, ls.size(), ls.c_ptr()); } 1371 1372 std::ostream& display_literal_verbose(std::ostream & out, literal lit) const; 1373 1374 std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const; 1375 display_literals_verbose(std::ostream & out,literal_vector const & lits)1376 std::ostream& display_literals_verbose(std::ostream & out, literal_vector const& lits) const { 1377 return display_literals_verbose(out, lits.size(), lits.c_ptr()); 1378 } 1379 1380 void display_watch_list(std::ostream & out, literal l) const; 1381 1382 void display_watch_lists(std::ostream & out) const; 1383 1384 std::ostream& display_clause_detail(std::ostream & out, clause const * cls) const; 1385 1386 std::ostream& display_clause(std::ostream & out, clause const * cls) const; 1387 1388 std::ostream& display_clause_smt2(std::ostream & out, clause const& cls) const; 1389 1390 std::ostream& display_clauses(std::ostream & out, ptr_vector<clause> const & v) const; 1391 1392 std::ostream& display_binary_clauses(std::ostream & out) const; 1393 1394 void display_assignment(std::ostream & out) const; 1395 1396 void display_eqc(std::ostream & out) const; 1397 1398 void display_app_enode_map(std::ostream & out) const; 1399 1400 void display_expr_bool_var_map(std::ostream & out) const; 1401 1402 void display_relevant_exprs(std::ostream & out) const; 1403 1404 void display_theories(std::ostream & out) const; 1405 1406 void display_eq_detail(std::ostream & out, enode * n) const; 1407 1408 void display_parent_eqs(std::ostream & out, enode * n) const; 1409 1410 void display_hot_bool_vars(std::ostream & out) const; 1411 1412 void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const; 1413 1414 unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const; 1415 void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, 1416 unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs, 1417 literal consequent = false_literal, symbol const& logic = symbol::null) const; 1418 1419 unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, 1420 unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs, 1421 literal consequent = false_literal, symbol const& logic = symbol::null) const; 1422 1423 std::string mk_lemma_name() const; 1424 1425 void display_assignment_as_smtlib2(std::ostream& out, symbol const& logic = symbol::null) const; 1426 1427 void display_normalized_enodes(std::ostream & out) const; 1428 1429 void display_enodes_lbls(std::ostream & out) const; 1430 1431 void display_decl2enodes(std::ostream & out) const; 1432 1433 void display_subexprs_info(std::ostream & out, expr * n) const; 1434 1435 void display_var_occs_histogram(std::ostream & out) const; 1436 1437 void display_num_min_occs(std::ostream & out) const; 1438 1439 void display_profile_res_sub(std::ostream & out) const; 1440 1441 void display_profile(std::ostream & out) const; 1442 1443 std::ostream& display(std::ostream& out, b_justification j) const; 1444 1445 std::ostream& display_compact_j(std::ostream& out, b_justification j) const; 1446 1447 // ----------------------------------- 1448 // 1449 // Debugging support 1450 // 1451 // ----------------------------------- 1452 protected: 1453 #ifdef Z3DEBUG 1454 bool is_watching_clause(literal l, clause const * cls) const; 1455 1456 bool check_clause(clause const * cls) const; 1457 1458 bool check_clauses(clause_vector const & v) const; 1459 1460 bool check_watch_list(literal l) const; 1461 1462 bool check_watch_list(unsigned l_idx) const; 1463 1464 bool check_bin_watch_lists() const; 1465 1466 bool check_enode(enode * n) const; 1467 1468 bool check_enodes() const; 1469 1470 bool check_invariant() const; 1471 1472 bool check_eqc_bool_assignment() const; 1473 1474 bool check_missing_clause_propagation(clause_vector const & v) const; 1475 1476 bool check_missing_bin_clause_propagation() const; 1477 1478 bool check_missing_eq_propagation() const; 1479 1480 bool check_missing_congruence() const; 1481 1482 bool check_missing_bool_enode_propagation() const; 1483 1484 bool check_missing_propagation() const; 1485 1486 bool check_relevancy(expr_ref_vector const & v) const; 1487 1488 bool check_relevancy() const; 1489 1490 bool check_bool_var_vector_sizes() const; 1491 1492 bool check_th_diseq_propagation() const; 1493 1494 bool check_missing_diseq_conflict() const; 1495 1496 #endif 1497 // ----------------------------------- 1498 // 1499 // Introspection 1500 // 1501 // ----------------------------------- 1502 unsigned get_lemma_avg_activity() const; 1503 void display_literal_num_occs(std::ostream & out) const; 1504 void display_num_assigned_literals_per_lvl(std::ostream & out) const; 1505 1506 // ----------------------------------- 1507 // 1508 // Auxiliary 1509 // 1510 // ----------------------------------- 1511 void init(); 1512 void flush(); 1513 config_mode get_config_mode(bool use_static_features) const; 1514 virtual void setup_context(bool use_static_features); 1515 void setup_components(); 1516 void pop_to_base_lvl(); 1517 void pop_to_search_lvl(); 1518 #ifdef Z3DEBUG 1519 bool already_internalized_theory(theory * th) const; 1520 bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const; 1521 #endif 1522 bool check_preamble(bool reset_cancel); 1523 lbool check_finalize(lbool r); 1524 1525 // ----------------------------------- 1526 // 1527 // API 1528 // 1529 // ----------------------------------- 1530 void assert_expr_core(expr * e, proof * pr); 1531 1532 // copy plugins into a fresh context. 1533 void copy_plugins(context& src, context& dst); 1534 1535 /* 1536 \brief Utilities for consequence finding. 1537 */ 1538 typedef hashtable<unsigned, u_hash, u_eq> index_set; 1539 //typedef uint_set index_set; 1540 u_map<index_set> m_antecedents; 1541 obj_map<expr, expr*> m_var2orig; 1542 u_map<expr*> m_assumption2orig; 1543 obj_map<expr, expr*> m_var2val; 1544 void extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq); 1545 void extract_fixed_consequences(unsigned& idx, index_set const& assumptions, expr_ref_vector& conseq); 1546 1547 void display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq); 1548 1549 unsigned delete_unfixed(expr_ref_vector& unfixed); 1550 1551 unsigned extract_fixed_eqs(expr_ref_vector& conseq); 1552 1553 expr_ref antecedent2fml(index_set const& ante); 1554 1555 1556 literal mk_diseq(expr* v, expr* val); 1557 1558 void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 1559 expr_ref_vector const& conseq, expr_ref_vector const& unfixed); 1560 1561 bool validate_justification(bool_var v, bool_var_data const& d, b_justification const& j); 1562 1563 void justify(literal lit, index_set& s); 1564 1565 void extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size); 1566 1567 void preferred_sat(literal_vector& literals); 1568 1569 void display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size); 1570 1571 void log_stats(); 1572 1573 void copy_user_propagator(context& src); 1574 1575 public: 1576 context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); 1577 1578 1579 virtual ~context(); 1580 1581 /** 1582 \brief Return a new context containing the same theories and simplifier plugins, but with an empty 1583 set of assertions. 1584 1585 If l == 0, then the logic of this context is used in the new context. 1586 If p == 0, then this->m_params is used 1587 */ 1588 context * mk_fresh(symbol const * l = nullptr, smt_params * smtp = nullptr, params_ref const & p = params_ref()); 1589 1590 static void copy(context& src, context& dst, bool override_base = false); 1591 1592 /** 1593 \brief Translate context to use new manager m. 1594 */ 1595 1596 app * mk_eq_atom(expr * lhs, expr * rhs); 1597 set_logic(symbol const & logic)1598 bool set_logic(symbol const& logic) { return m_setup.set_logic(logic); } 1599 1600 void register_plugin(theory * th); 1601 1602 void assert_expr(expr * e); 1603 1604 void assert_expr(expr * e, proof * pr); 1605 1606 void push(); 1607 1608 void pop(unsigned num_scopes); 1609 1610 lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true); 1611 1612 lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses); 1613 1614 lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); 1615 1616 lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes); 1617 1618 lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores); 1619 1620 lbool setup_and_check(bool reset_cancel = true); 1621 1622 void reduce_assertions(); 1623 1624 bool resource_limits_exceeded(); 1625 1626 failure get_last_search_failure() const; 1627 1628 proof * get_proof(); 1629 get_cr()1630 conflict_resolution& get_cr() { return *m_conflict_resolution.get(); } 1631 1632 void get_relevant_labels(expr* cnstr, buffer<symbol> & result); 1633 1634 void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result); 1635 1636 void get_relevant_literals(expr_ref_vector & result); 1637 1638 void get_guessed_literals(expr_ref_vector & result); 1639 1640 void internalize_assertion(expr * n, proof * pr, unsigned generation); 1641 1642 void internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy); 1643 internalize_instance(expr * body,proof * pr,unsigned generation)1644 void internalize_instance(expr * body, proof * pr, unsigned generation) { 1645 internalize_assertion(body, pr, generation); 1646 if (relevancy()) 1647 m_case_split_queue->internalize_instance_eh(body, generation); 1648 } 1649 get_unsat_core_size()1650 unsigned get_unsat_core_size() const { 1651 return m_unsat_core.size(); 1652 } 1653 get_unsat_core_expr(unsigned idx)1654 expr * get_unsat_core_expr(unsigned idx) const { 1655 return m_unsat_core.get(idx); 1656 } 1657 unsat_core()1658 expr_ref_vector const& unsat_core() const { return m_unsat_core; } 1659 1660 void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth); 1661 1662 expr_ref_vector get_trail(); 1663 1664 void get_model(model_ref & m); 1665 set_model(model * m)1666 void set_model(model* m) { m_model = m; } 1667 1668 bool update_model(bool refinalize); 1669 1670 bool validate_model(); 1671 get_num_asserted_formulas()1672 unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); } 1673 get_asserted_formulas_last_level()1674 unsigned get_asserted_formulas_last_level() const { return m_asserted_formulas.get_formulas_last_level(); } 1675 get_asserted_formula(unsigned idx)1676 expr * get_asserted_formula(unsigned idx) const { return m_asserted_formulas.get_formula(idx); } 1677 get_asserted_formula_proof(unsigned idx)1678 proof * get_asserted_formula_proof(unsigned idx) const { return m_asserted_formulas.get_formula_proof(idx); } 1679 get_asserted_formulas(ptr_vector<expr> & r)1680 void get_asserted_formulas(ptr_vector<expr>& r) const { m_asserted_formulas.get_assertions(r); } 1681 1682 //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); } 1683 get_assertions(ptr_vector<expr> & result)1684 void get_assertions(ptr_vector<expr> & result) { m_asserted_formulas.get_assertions(result); } 1685 1686 /* 1687 * user-propagator 1688 */ 1689 void user_propagate_init( 1690 void* ctx, 1691 solver::push_eh_t& push_eh, 1692 solver::pop_eh_t& pop_eh, 1693 solver::fresh_eh_t& fresh_eh); 1694 user_propagate_register_final(solver::final_eh_t & final_eh)1695 void user_propagate_register_final(solver::final_eh_t& final_eh) { 1696 if (!m_user_propagator) 1697 throw default_exception("user propagator must be initialized"); 1698 m_user_propagator->register_final(final_eh); 1699 } 1700 user_propagate_register_fixed(solver::fixed_eh_t & fixed_eh)1701 void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) { 1702 if (!m_user_propagator) 1703 throw default_exception("user propagator must be initialized"); 1704 m_user_propagator->register_fixed(fixed_eh); 1705 } 1706 user_propagate_register_eq(solver::eq_eh_t & eq_eh)1707 void user_propagate_register_eq(solver::eq_eh_t& eq_eh) { 1708 if (!m_user_propagator) 1709 throw default_exception("user propagator must be initialized"); 1710 m_user_propagator->register_eq(eq_eh); 1711 } 1712 user_propagate_register_diseq(solver::eq_eh_t & diseq_eh)1713 void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) { 1714 if (!m_user_propagator) 1715 throw default_exception("user propagator must be initialized"); 1716 m_user_propagator->register_diseq(diseq_eh); 1717 } 1718 user_propagate_register(expr * e)1719 unsigned user_propagate_register(expr* e) { 1720 if (!m_user_propagator) 1721 throw default_exception("user propagator must be initialized"); 1722 return m_user_propagator->add_expr(e); 1723 } 1724 1725 bool watches_fixed(enode* n) const; 1726 1727 void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain); 1728 assign_fixed(enode * n,expr * val,literal_vector const & explain)1729 void assign_fixed(enode* n, expr* val, literal_vector const& explain) { 1730 assign_fixed(n, val, explain.size(), explain.c_ptr()); 1731 } 1732 assign_fixed(enode * n,expr * val,literal explain)1733 void assign_fixed(enode* n, expr* val, literal explain) { 1734 assign_fixed(n, val, 1, &explain); 1735 } 1736 1737 void display(std::ostream & out) const; 1738 1739 void display_unsat_core(std::ostream & out) const; 1740 1741 void collect_statistics(::statistics & st) const; 1742 1743 void display_statistics(std::ostream & out) const; 1744 void display_istatistics(std::ostream & out) const; 1745 1746 // ----------------------------------- 1747 // 1748 // Macros 1749 // 1750 // ----------------------------------- 1751 public: get_num_macros()1752 unsigned get_num_macros() const { return m_asserted_formulas.get_num_macros(); } get_first_macro_last_level()1753 unsigned get_first_macro_last_level() const { return m_asserted_formulas.get_first_macro_last_level(); } get_macro_func_decl(unsigned i)1754 func_decl * get_macro_func_decl(unsigned i) const { return m_asserted_formulas.get_macro_func_decl(i); } get_macro_interpretation(unsigned i,expr_ref & interp)1755 func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); } get_macro_quantifier(func_decl * f)1756 quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); } insert_macro(func_decl * f,quantifier * m,proof * pr,expr_dependency * dep)1757 void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); } 1758 }; 1759 1760 struct pp_lit { 1761 context & ctx; 1762 literal lit; pp_litpp_lit1763 pp_lit(context & ctx, literal lit) : ctx(ctx), lit(lit) {} 1764 }; 1765 1766 inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) { 1767 return pp.ctx.display_detailed_literal(out, pp.lit); 1768 } 1769 1770 struct pp_lits { 1771 context & ctx; 1772 literal const *lits; 1773 unsigned len; pp_litspp_lits1774 pp_lits(context & ctx, unsigned len, literal const *lits) : ctx(ctx), lits(lits), len(len) {} pp_litspp_lits1775 pp_lits(context & ctx, literal_vector const& ls) : ctx(ctx), lits(ls.c_ptr()), len(ls.size()) {} 1776 }; 1777 1778 inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) { 1779 out << "{"; 1780 bool first = true; 1781 for (unsigned i = 0; i < pp.len; ++i) { 1782 if (first) { first = false; } else { out << " or\n"; } 1783 pp.ctx.display_detailed_literal(out, pp.lits[i]); 1784 } 1785 return out << "}"; 1786 1787 } 1788 struct enode_eq_pp { 1789 context const& ctx; 1790 enode_pair const& p; enode_eq_ppenode_eq_pp1791 enode_eq_pp(enode_pair const& p, context const& ctx): ctx(ctx), p(p) {} 1792 }; 1793 1794 std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p); 1795 1796 struct enode_pp { 1797 context const& ctx; 1798 enode* n; enode_ppenode_pp1799 enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {} 1800 }; 1801 1802 std::ostream& operator<<(std::ostream& out, enode_pp const& p); 1803 1804 }; 1805 1806 1807