1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_solver.h 7 8 Abstract: 9 10 SAT solver main class. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2011-05-21. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include <cmath> 22 #include "util/var_queue.h" 23 #include "util/params.h" 24 #include "util/statistics.h" 25 #include "util/stopwatch.h" 26 #include "util/ema.h" 27 #include "util/trace.h" 28 #include "util/rlimit.h" 29 #include "util/scoped_ptr_vector.h" 30 #include "util/scoped_limit_trail.h" 31 #include "sat/sat_types.h" 32 #include "sat/sat_clause.h" 33 #include "sat/sat_watched.h" 34 #include "sat/sat_justification.h" 35 #include "sat/sat_extension.h" 36 #include "sat/sat_config.h" 37 #include "sat/sat_cleaner.h" 38 #include "sat/sat_simplifier.h" 39 #include "sat/sat_scc.h" 40 #include "sat/sat_asymm_branch.h" 41 #include "sat/sat_cut_simplifier.h" 42 #include "sat/sat_probing.h" 43 #include "sat/sat_mus.h" 44 #include "sat/sat_binspr.h" 45 #include "sat/sat_drat.h" 46 #include "sat/sat_parallel.h" 47 #include "sat/sat_local_search.h" 48 #include "sat/sat_solver_core.h" 49 50 namespace pb { 51 class solver; 52 }; 53 54 namespace sat { 55 56 /** 57 \brief Main statistic counters. 58 */ 59 struct stats { 60 unsigned m_mk_var; 61 unsigned m_mk_bin_clause; 62 unsigned m_mk_ter_clause; 63 unsigned m_mk_clause; 64 unsigned m_conflict; 65 unsigned m_propagate; 66 unsigned m_bin_propagate; 67 unsigned m_ter_propagate; 68 unsigned m_decision; 69 unsigned m_restart; 70 unsigned m_gc_clause; 71 unsigned m_del_clause; 72 unsigned m_minimized_lits; 73 unsigned m_dyn_sub_res; 74 unsigned m_non_learned_generation; 75 unsigned m_blocked_corr_sets; 76 unsigned m_elim_var_res; 77 unsigned m_elim_var_bdd; 78 unsigned m_units; 79 unsigned m_backtracks; 80 unsigned m_backjumps; statsstats81 stats() { reset(); } 82 void reset(); 83 void collect_statistics(statistics & st) const; 84 }; 85 86 struct no_drat_params : public params_ref { no_drat_paramsno_drat_params87 no_drat_params() { set_sym("drat.file", symbol()); } 88 }; 89 90 class solver : public solver_core { 91 public: 92 struct abort_solver {}; 93 protected: 94 enum search_state { s_sat, s_unsat }; 95 96 bool m_checkpoint_enabled; 97 config m_config; 98 stats m_stats; 99 scoped_ptr<extension> m_ext; 100 scoped_ptr<cut_simplifier> m_cut_simplifier; 101 parallel* m_par; 102 drat m_drat; // DRAT for generating proofs 103 clause_allocator m_cls_allocator[2]; 104 bool m_cls_allocator_idx; 105 random_gen m_rand; 106 cleaner m_cleaner; 107 model m_model; 108 model_converter m_mc; 109 bool m_model_is_current; 110 simplifier m_simplifier; 111 scc m_scc; 112 asymm_branch m_asymm_branch; 113 probing m_probing; 114 bool m_is_probing { false }; 115 mus m_mus; // MUS for minimal core extraction 116 binspr m_binspr; 117 bool m_inconsistent; 118 bool m_searching; 119 // A conflict is usually a single justification. That is, a justification 120 // for false. If m_not_l is not null_literal, then m_conflict is a 121 // justification for l, and the conflict is union of m_no_l and m_conflict; 122 justification m_conflict; 123 literal m_not_l; 124 clause_vector m_clauses; 125 clause_vector m_learned; 126 unsigned m_num_frozen; 127 unsigned_vector m_active_vars, m_free_vars, m_vars_to_reinit; 128 vector<watch_list> m_watches; 129 svector<lbool> m_assignment; 130 svector<justification> m_justification; 131 bool_vector m_decision; 132 bool_vector m_mark; 133 bool_vector m_lit_mark; 134 bool_vector m_eliminated; 135 bool_vector m_external; 136 unsigned_vector m_var_scope; 137 unsigned_vector m_touched; 138 unsigned m_touch_index; 139 literal_vector m_replay_assign; 140 // branch variable selection: 141 svector<unsigned> m_activity; 142 unsigned m_activity_inc; 143 svector<uint64_t> m_last_conflict; 144 svector<uint64_t> m_last_propagation; 145 svector<uint64_t> m_participated; 146 svector<uint64_t> m_canceled; 147 svector<uint64_t> m_reasoned; 148 int m_action; 149 double m_step_size; 150 // phase 151 bool_vector m_phase; 152 bool_vector m_best_phase; 153 bool_vector m_prev_phase; 154 svector<char> m_assigned_since_gc; 155 search_state m_search_state; 156 unsigned m_search_unsat_conflicts; 157 unsigned m_search_sat_conflicts; 158 unsigned m_search_next_toggle; 159 unsigned m_phase_counter; 160 unsigned m_best_phase_size; 161 unsigned m_rephase_lim; 162 unsigned m_rephase_inc; 163 unsigned m_reorder_lim; 164 unsigned m_reorder_inc; 165 var_queue m_case_split_queue; 166 unsigned m_qhead; 167 unsigned m_scope_lvl; 168 unsigned m_search_lvl; 169 ema m_fast_glue_avg; 170 ema m_slow_glue_avg; 171 ema m_fast_glue_backup; 172 ema m_slow_glue_backup; 173 ema m_trail_avg; 174 literal_vector m_trail; 175 clause_wrapper_vector m_clauses_to_reinit; 176 std::string m_reason_unknown; 177 178 svector<unsigned> m_visited; 179 unsigned m_visited_ts; 180 181 struct scope { 182 unsigned m_trail_lim; 183 unsigned m_clauses_to_reinit_lim; 184 bool m_inconsistent; 185 }; 186 svector<scope> m_scopes; 187 scoped_limit_trail m_vars_lim; 188 stopwatch m_stopwatch; 189 params_ref m_params; 190 no_drat_params m_no_drat_params; 191 scoped_ptr<solver> m_clone; // for debugging purposes 192 literal_vector m_assumptions; // additional assumptions during check 193 literal_set m_assumption_set; // set of enabled assumptions 194 literal_set m_ext_assumption_set; // set of enabled assumptions 195 literal_vector m_core; // unsat core 196 197 unsigned m_par_id; 198 unsigned m_par_limit_in; 199 unsigned m_par_limit_out; 200 unsigned m_par_num_vars; 201 bool m_par_syncing_clauses; 202 203 class lookahead* m_cuber; 204 class i_local_search* m_local_search; 205 206 statistics m_aux_stats; 207 208 void del_clauses(clause_vector& clauses); 209 210 friend class integrity_checker; 211 friend class cleaner; 212 friend class asymm_branch; 213 friend class big; 214 friend class binspr; 215 friend class drat; 216 friend class elim_eqs; 217 friend class bcd; 218 friend class mus; 219 friend class probing; 220 friend class simplifier; 221 friend class scc; 222 friend class pb::solver; 223 friend class anf_simplifier; 224 friend class cut_simplifier; 225 friend class parallel; 226 friend class lookahead; 227 friend class local_search; 228 friend class ddfw; 229 friend class prob; 230 friend class unit_walk; 231 friend struct mk_stat; 232 friend class elim_vars; 233 friend class scoped_detach; 234 friend class xor_finder; 235 friend class aig_finder; 236 friend class lut_finder; 237 friend class npn3_finder; 238 public: 239 solver(params_ref const & p, reslimit& l); 240 ~solver() override; 241 242 // ----------------------- 243 // 244 // Misc 245 // 246 // ----------------------- 247 void updt_params(params_ref const & p); 248 static void collect_param_descrs(param_descrs & d); 249 250 // collect statistics from sat solver 251 void collect_statistics(statistics & st) const; 252 void reset_statistics(); 253 void display_status(std::ostream & out) const; 254 255 /** 256 \brief Copy (non learned) clauses from src to this solver. 257 Create missing variables if needed. 258 259 \pre the model converter of src and this must be empty 260 */ 261 void copy(solver const & src, bool copy_learned = false); 262 263 // ----------------------- 264 // 265 // Variable & Clause creation 266 // 267 // ----------------------- add_clause(unsigned num_lits,literal * lits,sat::status st)268 void add_clause(unsigned num_lits, literal * lits, sat::status st) override { mk_clause(num_lits, lits, st); } add_var(bool ext)269 bool_var add_var(bool ext) override { return mk_var(ext, true); } 270 271 bool_var mk_var(bool ext = false, bool dvar = true); 272 273 clause* mk_clause(literal_vector const& lits, sat::status st = sat::status::asserted()) { return mk_clause(lits.size(), lits.data(), st); } 274 clause* mk_clause(unsigned num_lits, literal * lits, sat::status st = sat::status::asserted()); 275 clause* mk_clause(literal l1, literal l2, sat::status st = sat::status::asserted()); 276 clause* mk_clause(literal l1, literal l2, literal l3, sat::status st = sat::status::asserted()); 277 rand()278 random_gen& rand() { return m_rand; } 279 280 protected: 281 void reset_var(bool_var v, bool ext, bool dvar); 282 cls_allocator()283 inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; } cls_allocator()284 inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; } alloc_clause(unsigned num_lits,literal const * lits,bool learned)285 inline clause * alloc_clause(unsigned num_lits, literal const * lits, bool learned) { return cls_allocator().mk_clause(num_lits, lits, learned); } dealloc_clause(clause * c)286 inline void dealloc_clause(clause* c) { cls_allocator().del_clause(c); } 287 struct cmp_activity; 288 void defrag_clauses(); 289 bool should_defrag(); 290 bool memory_pressure(); 291 void del_clause(clause & c); 292 clause * mk_clause_core(unsigned num_lits, literal * lits, sat::status st); mk_clause_core(literal_vector const & lits)293 clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.data()); } mk_clause_core(unsigned num_lits,literal * lits)294 clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, sat::status::asserted()); } mk_clause_core(literal l1,literal l2)295 void mk_clause_core(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_clause_core(2, lits); } 296 void mk_bin_clause(literal l1, literal l2, sat::status st); mk_bin_clause(literal l1,literal l2,bool learned)297 void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); } 298 bool propagate_bin_clause(literal l1, literal l2); 299 clause * mk_ter_clause(literal * lits, status st); 300 bool attach_ter_clause(clause & c, status st); 301 bool propagate_ter_clause(clause& c); 302 clause * mk_nary_clause(unsigned num_lits, literal * lits, status st); 303 bool has_variables_to_reinit(clause const& c) const; 304 bool has_variables_to_reinit(literal l1, literal l2) const; 305 bool attach_nary_clause(clause & c, bool is_asserting); 306 void attach_clause(clause & c, bool & reinit); attach_clause(clause & c)307 void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); } 308 void set_learned(clause& c, bool learned); 309 void shrink(clause& c, unsigned old_sz, unsigned new_sz); 310 void set_learned(literal l1, literal l2, bool learned); 311 void set_learned1(literal l1, literal l2, bool learned); add_ate(clause & c)312 void add_ate(clause& c) { m_mc.add_ate(c); } add_ate(literal l1,literal l2)313 void add_ate(literal l1, literal l2) { m_mc.add_ate(l1, l2); } add_ate(literal_vector const & lits)314 void add_ate(literal_vector const& lits) { m_mc.add_ate(lits); } 315 void drat_log_unit(literal lit, justification j); 316 void drat_log_clause(unsigned sz, literal const* lits, status st); 317 void drat_explain_conflict(); 318 319 class scoped_disable_checkpoint { 320 solver& s; 321 public: scoped_disable_checkpoint(solver & s)322 scoped_disable_checkpoint(solver& s): s(s) { 323 s.m_checkpoint_enabled = false; 324 } ~scoped_disable_checkpoint()325 ~scoped_disable_checkpoint() { 326 s.m_checkpoint_enabled = true; 327 } 328 }; 329 unsigned select_watch_lit(clause const & cls, unsigned starting_at) const; 330 unsigned select_learned_watch_lit(clause const & cls) const; 331 bool simplify_clause(unsigned & num_lits, literal * lits) const; 332 template<bool lvl0> 333 bool simplify_clause_core(unsigned & num_lits, literal * lits) const; 334 void detach_bin_clause(literal l1, literal l2, bool learned); 335 void detach_clause(clause & c); 336 void detach_nary_clause(clause & c); 337 void detach_ter_clause(clause & c); 338 void push_reinit_stack(clause & c); 339 void push_reinit_stack(literal l1, literal l2); 340 341 void init_visited(); mark_visited(literal l)342 void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; } mark_visited(bool_var v)343 void mark_visited(bool_var v) { mark_visited(literal(v, false)); } is_visited(bool_var v)344 bool is_visited(bool_var v) const { return is_visited(literal(v, false)); } is_visited(literal l)345 bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; } 346 bool all_distinct(literal_vector const& lits); 347 bool all_distinct(clause const& cl); 348 349 // ----------------------- 350 // 351 // Basic 352 // 353 // ----------------------- 354 public: 355 // is the state inconsistent? inconsistent()356 bool inconsistent() const { return m_inconsistent; } 357 358 // number of variables and clauses num_vars()359 unsigned num_vars() const { return m_justification.size(); } 360 unsigned num_clauses() const; 361 362 void num_binary(unsigned& given, unsigned& learned) const; num_restarts()363 unsigned num_restarts() const { return m_restarts; } is_external(bool_var v)364 bool is_external(bool_var v) const { return m_external[v]; } is_external(literal l)365 bool is_external(literal l) const { return is_external(l.var()); } 366 void set_external(bool_var v) override; 367 void set_non_external(bool_var v); was_eliminated(bool_var v)368 bool was_eliminated(bool_var v) const { return m_eliminated[v]; } 369 void set_eliminated(bool_var v, bool f) override; was_eliminated(literal l)370 bool was_eliminated(literal l) const { return was_eliminated(l.var()); } set_phase(literal l)371 void set_phase(literal l) override { if (l.var() < num_vars()) m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); } get_phase(bool_var b)372 bool_var get_phase(bool_var b) { return m_phase.get(b, false); } 373 void move_to_front(bool_var b); scope_lvl()374 unsigned scope_lvl() const { return m_scope_lvl; } search_lvl()375 unsigned search_lvl() const { return m_search_lvl; } at_search_lvl()376 bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } at_base_lvl()377 bool at_base_lvl() const { return m_scope_lvl == 0; } value(literal l)378 lbool value(literal l) const { return m_assignment[l.index()]; } value(bool_var v)379 lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; } get_justification(literal l)380 justification get_justification(literal l) const { return m_justification[l.var()]; } get_justification(bool_var v)381 justification get_justification(bool_var v) const { return m_justification[v]; } lvl(bool_var v)382 unsigned lvl(bool_var v) const { return m_justification[v].level(); } lvl(literal l)383 unsigned lvl(literal l) const { return m_justification[l.var()].level(); } trail_size()384 unsigned trail_size() const { return m_trail.size(); } scope_literal(unsigned n)385 literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; } assign(literal l,justification j)386 void assign(literal l, justification j) { 387 TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";); 388 switch (value(l)) { 389 case l_false: set_conflict(j, ~l); break; 390 case l_undef: assign_core(l, j); break; 391 case l_true: update_assign(l, j); break; 392 } 393 } update_assign(literal l,justification j)394 void update_assign(literal l, justification j) { 395 if (j.level() == 0) 396 m_justification[l.var()] = j; 397 } assign_unit(literal l)398 void assign_unit(literal l) { assign(l, justification(0)); } assign_scoped(literal l)399 void assign_scoped(literal l) { assign(l, justification(scope_lvl())); } 400 void assign_core(literal l, justification jst); 401 void set_conflict(justification c, literal not_l); set_conflict(justification c)402 void set_conflict(justification c) { set_conflict(c, null_literal); } set_conflict()403 void set_conflict() { set_conflict(justification(0)); } 404 lbool status(clause const & c) const; get_offset(clause const & c)405 clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); } 406 limit_reached()407 bool limit_reached() { 408 if (!m_rlimit.inc()) { 409 m_model_is_current = false; 410 TRACE("sat", tout << "canceled\n";); 411 m_reason_unknown = "sat.canceled"; 412 return true; 413 } 414 return false; 415 } 416 memory_exceeded()417 bool memory_exceeded() { 418 ++m_num_checkpoints; 419 if (m_num_checkpoints < 10) return false; 420 m_num_checkpoints = 0; 421 return memory::get_allocation_size() > m_config.m_max_memory; 422 } 423 checkpoint()424 void checkpoint() { 425 if (!m_checkpoint_enabled) return; 426 if (limit_reached()) { 427 throw solver_exception(Z3_CANCELED_MSG); 428 } 429 if (memory_exceeded()) { 430 throw solver_exception(Z3_MAX_MEMORY_MSG); 431 } 432 } 433 void set_par(parallel* p, unsigned id); canceled()434 bool canceled() { return !m_rlimit.inc(); } get_config()435 config const& get_config() const { return m_config; } get_drat()436 drat& get_drat() { return m_drat; } get_drat_ptr()437 drat* get_drat_ptr() { return &m_drat; } set_incremental(bool b)438 void set_incremental(bool b) { m_config.m_incremental = b; } is_incremental()439 bool is_incremental() const { return m_config.m_incremental; } get_extension()440 extension* get_extension() const override { return m_ext.get(); } 441 void set_extension(extension* e) override; get_cut_simplifier()442 cut_simplifier* get_cut_simplifier() override { return m_cut_simplifier.get(); } 443 bool set_root(literal l, literal r); 444 void flush_roots(); 445 typedef std::pair<literal, literal> bin_clause; operatorbin_clause_hash446 struct bin_clause_hash { unsigned operator()(bin_clause const& b) const { return b.first.hash() + 2*b.second.hash(); } }; 447 protected: get_wlist(literal l)448 watch_list & get_wlist(literal l) { return m_watches[l.index()]; } get_wlist(literal l)449 watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; } get_wlist(unsigned l_idx)450 watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; } is_marked(bool_var v)451 bool is_marked(bool_var v) const { return m_mark[v]; } mark(bool_var v)452 void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; } reset_mark(bool_var v)453 void reset_mark(bool_var v) { SASSERT(is_marked(v)); m_mark[v] = false; } is_marked_lit(literal l)454 bool is_marked_lit(literal l) const { return m_lit_mark[l.index()]; } mark_lit(literal l)455 void mark_lit(literal l) { SASSERT(!is_marked_lit(l)); m_lit_mark[l.index()] = true; } unmark_lit(literal l)456 void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; } 457 bool check_inconsistent(); 458 459 // ----------------------- 460 // 461 // Propagation 462 // 463 // ----------------------- 464 public: 465 // if update == true, then glue of learned clauses is updated. 466 bool propagate(bool update); 467 468 protected: 469 bool should_propagate() const; 470 bool propagate_core(bool update); 471 bool propagate_literal(literal l, bool update); 472 473 // ----------------------- 474 // 475 // Search 476 // 477 // ----------------------- 478 public: 479 lbool check(unsigned num_lits = 0, literal const* lits = nullptr); 480 481 // retrieve model if solver return sat get_model()482 model const & get_model() const { return m_model; } model_is_current()483 bool model_is_current() const { return m_model_is_current; } 484 485 // retrieve core from assumptions get_core()486 literal_vector const& get_core() const { return m_core; } 487 get_model_converter()488 model_converter const & get_model_converter() const { return m_mc; } 489 490 // The following methods are used when converting the state from the SAT solver back 491 // to a set of assertions. 492 493 // retrieve model converter that handles variable elimination and other transformations flush(model_converter & mc)494 void flush(model_converter& mc) { mc.flush(m_mc); } 495 496 // size of initial trail containing unit clauses init_trail_size()497 unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } 498 499 // literal at trail index i trail_literal(unsigned i)500 literal trail_literal(unsigned i) const { return m_trail[i]; } 501 502 // collect n-ary clauses clauses()503 clause_vector const& clauses() const { return m_clauses; } 504 505 // collect binary clauses 506 void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const; 507 508 void set_model(model const& mdl, bool is_current); get_reason_unknown()509 char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } 510 bool check_clauses(model const& m) const; 511 bool is_assumption(bool_var v) const; 512 void set_activity(bool_var v, unsigned act); 513 514 lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level); 515 516 void display_lookahead_scores(std::ostream& out); 517 get_stats()518 stats const& get_stats() const { return m_stats; } 519 520 protected: 521 522 unsigned m_conflicts_since_init { 0 }; 523 unsigned m_restarts { 0 }; 524 unsigned m_restart_next_out { 0 }; 525 unsigned m_conflicts_since_restart { 0 }; 526 bool m_force_conflict_analysis { false }; 527 unsigned m_simplifications { 0 }; 528 unsigned m_restart_threshold { 0 }; 529 unsigned m_luby_idx { 0 }; 530 unsigned m_conflicts_since_gc { 0 }; 531 unsigned m_gc_threshold { 0 }; 532 unsigned m_defrag_threshold { 0 }; 533 unsigned m_num_checkpoints { 0 }; 534 double m_min_d_tk { 0 } ; 535 unsigned m_next_simplify { 0 }; 536 bool m_simplify_enabled { true }; 537 bool m_restart_enabled { true }; 538 bool decide(); 539 bool_var next_var(); 540 lbool bounded_search(); 541 lbool basic_search(); 542 lbool search(); 543 lbool final_check(); 544 void init_search(); 545 546 literal_vector m_min_core; 547 bool m_min_core_valid { false }; init_reason_unknown()548 void init_reason_unknown() { m_reason_unknown = "no reason given"; } 549 void init_assumptions(unsigned num_lits, literal const* lits); 550 void reassert_min_core(); 551 void update_min_core(); 552 void resolve_weighted(); 553 void reset_assumptions(); 554 void add_assumption(literal lit); 555 void reinit_assumptions(); 556 void init_ext_assumptions(); 557 bool tracking_assumptions() const; 558 bool is_assumption(literal l) const; 559 bool should_simplify() const; 560 void do_simplify(); 561 void mk_model(); 562 bool check_model(model const & m) const; 563 void do_restart(bool to_base); 564 svector<size_t> m_last_positions; 565 unsigned m_last_position_log; 566 unsigned m_restart_logs; 567 unsigned restart_level(bool to_base); 568 void log_stats(); 569 bool should_cancel(); 570 bool should_restart() const; 571 void set_next_restart(); 572 void update_activity(bool_var v, double p); 573 bool reached_max_conflicts(); 574 void sort_watch_lits(); 575 void exchange_par(); 576 lbool check_par(unsigned num_lits, literal const* lits); 577 lbool do_local_search(unsigned num_lits, literal const* lits); 578 lbool do_ddfw_search(unsigned num_lits, literal const* lits); 579 lbool do_prob_search(unsigned num_lits, literal const* lits); 580 lbool invoke_local_search(unsigned num_lits, literal const* lits); 581 lbool do_unit_walk(); 582 583 // ----------------------- 584 // 585 // GC 586 // 587 // ----------------------- 588 protected: 589 bool should_gc() const; 590 void do_gc(); 591 void gc_glue(); 592 void gc_psm(); 593 void gc_glue_psm(); 594 void gc_psm_glue(); 595 void save_psm(); 596 void gc_half(char const * st_name); 597 void gc_dyn_psm(); 598 bool activate_frozen_clause(clause & c); 599 unsigned psm(clause const & c) const; 600 bool can_delete(clause const & c) const; 601 bool can_delete3(literal l1, literal l2, literal l3) const; 602 603 // gc for lemmas in the reinit-stack 604 void gc_reinit_stack(unsigned num_scopes); 605 bool is_asserting(unsigned new_lvl, clause_wrapper const& cw) const; 606 get_clause(watch_list::iterator it)607 clause& get_clause(watch_list::iterator it) const { 608 SASSERT(it->get_kind() == watched::CLAUSE); 609 return get_clause(it->get_clause_offset()); 610 } 611 get_clause(watched const & w)612 clause& get_clause(watched const& w) const { 613 SASSERT(w.get_kind() == watched::CLAUSE); 614 return get_clause(w.get_clause_offset()); 615 } 616 get_clause(justification const & j)617 clause& get_clause(justification const& j) const { 618 SASSERT(j.is_clause()); 619 return get_clause(j.get_clause_offset()); 620 } 621 get_clause(clause_offset cls_off)622 clause& get_clause(clause_offset cls_off) const { 623 return *(cls_allocator().get_clause(cls_off)); 624 } 625 626 // ----------------------- 627 // 628 // Conflict resolution 629 // 630 // ----------------------- 631 protected: 632 unsigned m_conflict_lvl; 633 literal_vector m_lemma; 634 literal_vector m_ext_antecedents; 635 bool use_backjumping(unsigned num_scopes) const; 636 bool allow_backtracking() const; 637 bool resolve_conflict(); 638 lbool resolve_conflict_core(); 639 void learn_lemma_and_backjump(); update_max_level(literal lit,unsigned lvl2,bool & unique_max)640 inline unsigned update_max_level(literal lit, unsigned lvl2, bool& unique_max) { 641 unsigned lvl1 = lvl(lit); 642 if (lvl1 < lvl2) return lvl2; 643 unique_max = lvl1 > lvl2; 644 return lvl1; 645 } 646 unsigned get_max_lvl(literal consequent, justification js, bool& unique_max); 647 void process_antecedent(literal antecedent, unsigned & num_marks); 648 void resolve_conflict_for_unsat_core(); 649 void process_antecedent_for_unsat_core(literal antecedent); 650 void process_consequent_for_unsat_core(literal consequent, justification const& js); 651 void fill_ext_antecedents(literal consequent, justification js, bool probing); 652 unsigned skip_literals_above_conflict_level(); 653 void updt_phase_of_vars(); 654 void updt_phase_counters(); 655 void do_toggle_search_state(); 656 bool should_toggle_search_state(); 657 bool is_sat_phase() const; 658 bool is_two_phase() const; 659 bool should_rephase(); 660 void do_rephase(); 661 bool should_reorder(); 662 void do_reorder(); 663 svector<char> m_diff_levels; 664 unsigned num_diff_levels(unsigned num, literal const * lits); 665 bool num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue); 666 bool num_diff_false_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue); 667 668 // lemma minimization 669 typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set; 670 bool_var_vector m_unmark; 671 level_approx_set m_lvl_set; 672 literal_vector m_lemma_min_stack; 673 bool process_antecedent_for_minimization(literal antecedent); 674 bool implied_by_marked(literal lit); 675 void reset_unmark(unsigned old_size); 676 void updt_lemma_lvl_set(); 677 bool minimize_lemma(); 678 bool minimize_lemma_binres(); 679 void reset_lemma_var_marks(); 680 bool dyn_sub_res(); 681 682 // ----------------------- 683 // 684 // Backtracking 685 // 686 // ----------------------- 687 void push(); 688 void pop(unsigned num_scopes); 689 void pop_reinit(unsigned num_scopes); 690 void shrink_vars(unsigned v); 691 void pop_vars(unsigned num_scopes); 692 693 void unassign_vars(unsigned old_sz, unsigned new_lvl); 694 void reinit_clauses(unsigned old_sz); 695 696 literal_vector m_user_scope_literals; 697 vector<svector<bool_var>> m_free_var_freeze; 698 literal_vector m_aux_literals; 699 svector<bin_clause> m_user_bin_clauses; 700 701 void gc_vars(bool_var max_var); 702 703 // ----------------------- 704 // 705 // External 706 // 707 // ----------------------- 708 public: set_should_simplify()709 void set_should_simplify() { m_next_simplify = m_conflicts_since_init; } get_vars_to_reinit()710 bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; } is_probing()711 bool is_probing() const { return m_is_probing; } is_free(bool_var v)712 bool is_free(bool_var v) const { return m_free_vars.contains(v); } 713 714 public: 715 void user_push() override; 716 void user_pop(unsigned num_scopes) override; 717 void pop_to_base_level(); num_user_scopes()718 unsigned num_user_scopes() const override { return m_user_scope_literals.size(); } num_scopes()719 unsigned num_scopes() const override { return m_scopes.size(); } rlimit()720 reslimit& rlimit() { return m_rlimit; } params()721 params_ref const& params() { return m_params; } 722 // ----------------------- 723 // 724 // Simplification 725 // 726 // ----------------------- 727 public: 728 bool do_cleanup(bool force); 729 void simplify(bool learned = true); 730 void asymmetric_branching(); 731 unsigned scc_bin(); 732 733 // ----------------------- 734 // 735 // Auxiliary methods. 736 // 737 // ----------------------- 738 public: 739 lbool find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes); 740 741 lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_vector>& conseq); 742 743 // initialize and retrieve local search. 744 // local_search& init_local_search(); 745 746 private: 747 748 typedef hashtable<unsigned, u_hash, u_eq> index_set; 749 750 u_map<index_set> m_antecedents; 751 literal_vector m_todo_antecedents; 752 vector<literal_vector> m_binary_clause_graph; 753 754 bool extract_assumptions(literal lit, index_set& s); 755 756 bool check_domain(literal lit, literal lit2); 757 758 std::ostream& display_index_set(std::ostream& out, index_set const& s) const; 759 760 lbool get_consequences(literal_vector const& assms, literal_vector const& lits, vector<literal_vector>& conseq); 761 762 lbool get_bounded_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_vector>& conseq); 763 764 void delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars); 765 766 void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq); 767 768 void extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq); 769 770 void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq); 771 772 bool extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq); 773 774 void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars); 775 776 void fixup_consequence_core(); 777 778 // ----------------------- 779 // 780 // Activity related stuff 781 // 782 // ----------------------- 783 public: inc_activity(bool_var v)784 void inc_activity(bool_var v) { 785 unsigned & act = m_activity[v]; 786 act += m_activity_inc; 787 m_case_split_queue.activity_increased_eh(v); 788 if (act > (1 << 24)) 789 rescale_activity(); 790 } 791 decay_activity()792 void decay_activity() { 793 m_activity_inc *= m_config.m_variable_decay; 794 m_activity_inc /= 100; 795 } 796 797 private: 798 void rescale_activity(); 799 800 void update_chb_activity(bool is_sat, unsigned qhead); 801 802 void update_lrb_reasoned(); 803 804 void update_lrb_reasoned(literal lit); 805 806 // ----------------------- 807 // 808 // Iterators 809 // 810 // ----------------------- 811 public: begin_clauses()812 clause * const * begin_clauses() const { return m_clauses.begin(); } end_clauses()813 clause * const * end_clauses() const { return m_clauses.end(); } begin_learned()814 clause * const * begin_learned() const { return m_learned.begin(); } end_learned()815 clause * const * end_learned() const { return m_learned.end(); } learned()816 clause_vector const& learned() const { return m_learned; } 817 818 819 // ----------------------- 820 // 821 // Debugging 822 // 823 // ----------------------- 824 public: 825 bool check_invariant() const; 826 void display(std::ostream & out) const; 827 void display_watches(std::ostream & out) const; 828 void display_watches(std::ostream & out, literal lit) const; 829 void display_dimacs(std::ostream & out) const; 830 std::ostream& display_model(std::ostream& out) const; 831 void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; 832 void display_assignment(std::ostream & out) const; 833 std::ostream& display_justification(std::ostream & out, justification const& j) const; 834 std::ostream& display_watch_list(std::ostream& out, watch_list const& wl) const; 835 836 protected: 837 void display_binary(std::ostream & out) const; 838 void display_units(std::ostream & out) const; 839 bool is_unit(clause const & c) const; 840 bool is_empty(clause const & c) const; 841 bool check_missed_propagation(clause_vector const & cs) const; 842 bool check_missed_propagation() const; 843 bool check_marks() const; 844 }; 845 846 struct mk_stat { 847 solver const & m_solver; mk_statmk_stat848 mk_stat(solver const & s):m_solver(s) {} 849 void display(std::ostream & out) const; 850 }; 851 852 class scoped_detach { 853 solver& s; 854 clause& c; 855 bool m_deleted; 856 public: scoped_detach(solver & s,clause & c)857 scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) { 858 if (!c.frozen()) s.detach_clause(c); 859 } ~scoped_detach()860 ~scoped_detach() { 861 if (!m_deleted && !c.frozen()) s.attach_clause(c); 862 } 863 del_clause()864 void del_clause() { 865 if (!m_deleted) { 866 s.del_clause(c); 867 m_deleted = true; 868 } 869 } 870 }; 871 872 873 std::ostream & operator<<(std::ostream & out, mk_stat const & stat); 874 }; 875