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