#pragma once
#include <cmath>
#include "util/var_queue.h"
#include "util/params.h"
#include "util/statistics.h"
#include "util/stopwatch.h"
#include "util/ema.h"
#include "util/trace.h"
#include "util/rlimit.h"
#include "util/scoped_ptr_vector.h"
#include "util/scoped_limit_trail.h"
#include "util/visit_helper.h"
#include "sat/sat_types.h"
#include "sat/sat_clause.h"
#include "sat/sat_watched.h"
#include "sat/sat_justification.h"
#include "sat/sat_extension.h"
#include "sat/sat_config.h"
#include "sat/sat_cleaner.h"
#include "sat/sat_simplifier.h"
#include "sat/sat_scc.h"
#include "sat/sat_asymm_branch.h"
#include "sat/sat_cut_simplifier.h"
#include "sat/sat_probing.h"
#include "sat/sat_mus.h"
#include "sat/sat_drat.h"
#include "sat/sat_parallel.h"
#include "sat/sat_local_search.h"
#include "sat/sat_solver_core.h"
namespace pb {
class solver;
};
namespace sat {
struct stats {
unsigned m_mk_var;
unsigned m_mk_bin_clause;
unsigned m_mk_ter_clause;
unsigned m_mk_clause;
unsigned m_conflict;
unsigned m_propagate;
unsigned m_bin_propagate;
unsigned m_ter_propagate;
unsigned m_decision;
unsigned m_restart;
unsigned m_gc_clause;
unsigned m_del_clause;
unsigned m_minimized_lits;
unsigned m_dyn_sub_res;
unsigned m_non_learned_generation;
unsigned m_blocked_corr_sets;
unsigned m_elim_var_res;
unsigned m_elim_var_bdd;
unsigned m_units;
unsigned m_backtracks;
unsigned m_backjumps;
stats() { reset(); }
void reset();
void collect_statistics(statistics & st) const;
};
struct no_drat_params : public params_ref {
no_drat_params() { set_bool("drat.disable", true); }
};
class solver : public solver_core {
public:
struct abort_solver : public std::exception {};
protected:
enum search_state { s_sat, s_unsat };
bool m_checkpoint_enabled;
config m_config;
stats m_stats;
scoped_ptr<extension> m_ext;
scoped_ptr<cut_simplifier> m_cut_simplifier;
parallel* m_par;
drat m_drat; clause_allocator m_cls_allocator[2];
bool m_cls_allocator_idx;
random_gen m_rand;
cleaner m_cleaner;
model m_model;
model_converter m_mc;
bool m_model_is_current;
simplifier m_simplifier;
scc m_scc;
asymm_branch m_asymm_branch;
probing m_probing;
bool m_is_probing { false };
mus m_mus; bool m_inconsistent;
bool m_searching;
justification m_conflict;
literal m_not_l;
clause_vector m_clauses;
clause_vector m_learned;
unsigned m_num_frozen;
unsigned_vector m_active_vars, m_free_vars, m_vars_to_free, m_vars_to_reinit;
vector<watch_list> m_watches;
svector<lbool> m_assignment;
svector<justification> m_justification;
bool_vector m_decision;
bool_vector m_mark;
bool_vector m_lit_mark;
bool_vector m_eliminated;
bool_vector m_external;
unsigned_vector m_var_scope;
unsigned_vector m_touched;
unsigned m_touch_index;
literal_vector m_replay_assign;
svector<unsigned> m_activity;
unsigned m_activity_inc;
svector<uint64_t> m_last_conflict;
svector<uint64_t> m_last_propagation;
svector<uint64_t> m_participated;
svector<uint64_t> m_canceled;
svector<uint64_t> m_reasoned;
int m_action;
double m_step_size;
bool_vector m_phase;
bool_vector m_best_phase;
bool_vector m_prev_phase;
bool m_new_best_phase = false;
svector<char> m_assigned_since_gc;
search_state m_search_state;
unsigned m_search_unsat_conflicts;
unsigned m_search_sat_conflicts;
unsigned m_search_next_toggle;
unsigned m_phase_counter;
unsigned m_best_phase_size;
backoff m_local_search_lim;
unsigned m_rephase_lim;
unsigned m_rephase_inc;
backoff m_rephase;
backoff m_reorder;
var_queue<unsigned_vector> m_case_split_queue;
unsigned m_qhead;
unsigned m_scope_lvl;
unsigned m_search_lvl;
ema m_fast_glue_avg;
ema m_slow_glue_avg;
ema m_fast_glue_backup;
ema m_slow_glue_backup;
ema m_trail_avg;
literal_vector m_trail;
clause_wrapper_vector m_clauses_to_reinit;
std::string m_reason_unknown;
bool m_trim = false;
bool m_solver_canceled = false;
visit_helper m_visited;
struct scope {
unsigned m_trail_lim;
unsigned m_clauses_to_reinit_lim;
bool m_inconsistent;
};
svector<scope> m_scopes;
scoped_limit_trail m_vars_lim;
stopwatch m_stopwatch;
params_ref m_params;
no_drat_params m_no_drat_params;
scoped_ptr<solver> m_clone; literal_vector m_assumptions; literal_set m_assumption_set; literal_set m_ext_assumption_set; literal_vector m_core;
unsigned m_par_id;
unsigned m_par_limit_in;
unsigned m_par_limit_out;
unsigned m_par_num_vars;
bool m_par_syncing_clauses;
class lookahead* m_cuber;
class i_local_search* m_local_search;
statistics m_aux_stats;
void del_clauses(clause_vector& clauses);
friend class integrity_checker;
friend class cleaner;
friend class asymm_branch;
friend class big;
friend class drat;
friend class elim_eqs;
friend class bcd;
friend class mus;
friend class probing;
friend class simplifier;
friend class scc;
friend class pb::solver;
friend class anf_simplifier;
friend class cut_simplifier;
friend class parallel;
friend class lookahead;
friend class local_search;
friend class ddfw_wrapper;
friend class prob;
friend class unit_walk;
friend struct mk_stat;
friend class elim_vars;
friend class scoped_detach;
friend class xor_finder;
friend class aig_finder;
friend class lut_finder;
friend class npn3_finder;
friend class proof_trim;
friend struct backoff;
public:
solver(params_ref const & p, reslimit& l);
~solver() override;
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void collect_statistics(statistics & st) const;
void reset_statistics();
void display_status(std::ostream & out) const;
void copy(solver const & src, bool copy_learned = false);
void add_clause(unsigned num_lits, literal * lits, sat::status st) override { mk_clause(num_lits, lits, st); }
void add_clause(literal l1, literal l2, status st) {
literal lits[2] = { l1, l2 };
add_clause(2, lits, st);
}
void add_clause(literal lit, status st) { literal lits[1] = { lit }; add_clause(1, lits, st); }
bool_var add_var(bool ext) override { return mk_var(ext, true); }
bool_var mk_var(bool ext = false, bool dvar = true);
clause* mk_clause(literal_vector const& lits, sat::status st = sat::status::asserted()) { return mk_clause(lits.size(), lits.data(), st); }
clause* mk_clause(unsigned num_lits, literal * lits, sat::status st = sat::status::asserted());
clause* mk_clause(literal l1, literal l2, sat::status st = sat::status::asserted());
clause* mk_clause(literal l1, literal l2, literal l3, sat::status st = sat::status::asserted());
random_gen& rand() { return m_rand; }
void set_trim() { m_trim = true; }
void set_canceled() { m_solver_canceled = true; }
protected:
void reset_var(bool_var v, bool ext, bool dvar);
inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; }
inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; }
inline clause * alloc_clause(unsigned num_lits, literal const * lits, bool learned) { return cls_allocator().mk_clause(num_lits, lits, learned); }
inline void dealloc_clause(clause* c) { cls_allocator().del_clause(c); }
struct cmp_activity;
void defrag_clauses();
bool should_defrag();
bool memory_pressure();
void del_clause(clause & c);
clause * mk_clause_core(unsigned num_lits, literal * lits, sat::status st);
clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.data()); }
clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, sat::status::asserted()); }
void mk_clause_core(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_clause_core(2, lits); }
void mk_bin_clause(literal l1, literal l2, sat::status st);
void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); }
bool propagate_bin_clause(literal l1, literal l2);
clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
bool has_variables_to_reinit(clause const& c) const;
bool has_variables_to_reinit(literal l1, literal l2) const;
bool attach_nary_clause(clause & c, bool is_asserting);
void attach_clause(clause & c, bool & reinit);
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
void set_learned(clause& c, bool learned);
void shrink(clause& c, unsigned old_sz, unsigned new_sz);
void set_learned(literal l1, literal l2, bool learned);
void set_learned1(literal l1, literal l2, bool learned);
void add_ate(clause& c) { m_mc.add_ate(c); }
void add_ate(literal l1, literal l2) { m_mc.add_ate(l1, l2); }
void add_ate(literal_vector const& lits) { m_mc.add_ate(lits); }
void drat_log_unit(literal lit, justification j);
void drat_log_clause(unsigned sz, literal const* lits, status st);
void drat_explain_conflict();
class scoped_disable_checkpoint {
solver& s;
public:
scoped_disable_checkpoint(solver& s): s(s) {
s.m_checkpoint_enabled = false;
}
~scoped_disable_checkpoint() {
s.m_checkpoint_enabled = true;
}
};
unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
unsigned select_learned_watch_lit(clause const & cls) const;
bool simplify_clause(unsigned & num_lits, literal * lits) const;
template<bool lvl0>
bool simplify_clause_core(unsigned & num_lits, literal * lits) const;
void detach_bin_clause(literal l1, literal l2, bool learned);
void detach_clause(clause & c);
void detach_nary_clause(clause & c);
void push_reinit_stack(clause & c);
void push_reinit_stack(literal l1, literal l2);
void init_visited(unsigned lim = 1) { m_visited.init_visited(2 * num_vars(), lim); }
bool is_visited(sat::bool_var v) const { return is_visited(literal(v, false)); }
bool is_visited(literal lit) const { return m_visited.is_visited(lit.index()); }
void mark_visited(literal lit) { m_visited.mark_visited(lit.index()); }
void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
bool all_distinct(literal_vector const& lits);
bool all_distinct(clause const& cl);
public:
bool inconsistent() const { return m_inconsistent; }
unsigned num_vars() const { return m_justification.size(); }
unsigned num_clauses() const;
void num_binary(unsigned& given, unsigned& learned) const;
unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const { return m_external[v]; }
bool is_external(literal l) const { return is_external(l.var()); }
void set_external(bool_var v) override;
void set_non_external(bool_var v);
bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
void set_eliminated(bool_var v, bool f) override;
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
void set_phase(literal l) override { if (l.var() < num_vars()) m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); }
bool get_phase(bool_var b) { return m_phase.get(b, false); }
bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); }
void set_has_new_best_phase(bool b) { m_new_best_phase = b; }
bool has_new_best_phase() const { return m_new_best_phase; }
void move_to_front(bool_var b);
unsigned scope_lvl() const { return m_scope_lvl; }
unsigned search_lvl() const { return m_search_lvl; }
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
bool at_base_lvl() const { return m_scope_lvl == 0; }
lbool value(literal l) const { return m_assignment[l.index()]; }
lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
justification get_justification(literal l) const { return m_justification[l.var()]; }
justification get_justification(bool_var v) const { return m_justification[v]; }
unsigned lvl(bool_var v) const { return m_justification[v].level(); }
unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
unsigned trail_size() const { return m_trail.size(); }
literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
void assign(literal l, justification j) {
TRACE(sat_assign, tout << l << " previous value: " << value(l) << " j: " << j << "\n";);
switch (value(l)) {
case l_false: set_conflict(j, ~l); break;
case l_undef: assign_core(l, j); break;
case l_true: update_assign(l, j); break;
}
}
void update_assign(literal l, justification j) {
if (j.level() == 0 && !m_trim && lvl(l) != 0)
m_justification[l.var()] = j;
}
void assign_unit(literal l) { assign(l, justification(0)); }
void assign_scoped(literal l) { assign(l, justification(scope_lvl())); }
void assign_core(literal l, justification jst);
void set_conflict(justification c, literal not_l);
void set_conflict(justification c) { set_conflict(c, null_literal); }
void set_conflict() { set_conflict(justification(0)); }
lbool status(clause const & c) const;
clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); }
bool limit_reached() {
if (!m_rlimit.inc()) {
m_model_is_current = false;
TRACE(sat, tout << "canceled\n";);
m_reason_unknown = "sat.canceled";
return true;
}
return false;
}
bool memory_exceeded() {
++m_num_checkpoints;
if (m_num_checkpoints < 10) return false;
m_num_checkpoints = 0;
return memory::get_allocation_size() > m_config.m_max_memory;
}
void checkpoint() {
if (!m_checkpoint_enabled)
return;
if (limit_reached())
throw solver_exception(Z3_CANCELED_MSG);
if (memory_exceeded())
throw solver_exception(Z3_MAX_MEMORY_MSG);
}
void set_par(parallel* p, unsigned id);
bool canceled() { return !m_rlimit.inc(); }
config const& get_config() const { return m_config; }
void set_drat(bool d) { m_config.m_drat = d; }
drat& get_drat() { return m_drat; }
drat* get_drat_ptr() { return &m_drat; }
void set_incremental(bool b) { m_config.m_incremental = b; }
bool is_incremental() const { return m_config.m_incremental; }
extension* get_extension() const override { return m_ext.get(); }
void set_extension(extension* e) override;
cut_simplifier* get_cut_simplifier() override { return m_cut_simplifier.get(); }
bool set_root(literal l, literal r);
void flush_roots();
typedef std::pair<literal, literal> bin_clause;
struct bin_clause_hash { unsigned operator()(bin_clause const& b) const { return b.first.hash() + 2*b.second.hash(); } };
watch_list const& get_wlist(literal l) const { return m_watches[l.index()]; }
watch_list& get_wlist(literal l) { return m_watches[l.index()]; }
protected:
watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; }
bool is_marked(bool_var v) const { return m_mark[v]; }
void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; }
void reset_mark(bool_var v) { SASSERT(is_marked(v)); m_mark[v] = false; }
bool is_marked_lit(literal l) const { return m_lit_mark[l.index()]; }
void mark_lit(literal l) { SASSERT(!is_marked_lit(l)); m_lit_mark[l.index()] = true; }
void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; }
bool check_inconsistent();
public:
bool propagate(bool update);
protected:
bool should_propagate() const;
bool propagate_core(bool update);
bool propagate_literal(literal l, bool update);
void propagate_clause(clause& c, bool update, unsigned assign_level, clause_offset cls_off);
void set_watch(clause& c, unsigned idx, clause_offset cls_off);
public:
lbool check(unsigned num_lits = 0, literal const* lits = nullptr);
lbool check(literal_vector const& lits) { return check(lits.size(), lits.data()); }
model const & get_model() const { return m_model; }
bool model_is_current() const { return m_model_is_current; }
literal_vector const& get_core() const { return m_core; }
model_converter const & get_model_converter() const { return m_mc; }
void flush(model_converter& mc) { mc.flush(m_mc); }
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
literal trail_literal(unsigned i) const { return m_trail[i]; }
clause_vector const& clauses() const { return m_clauses; }
void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const;
void set_model(model const& mdl, bool is_current);
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
bool check_clauses(model const& m) const;
bool is_assumption(bool_var v) const;
void set_activity(bool_var v, unsigned act);
lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
void display_lookahead_scores(std::ostream& out);
stats const& get_stats() const { return m_stats; }
protected:
unsigned m_conflicts_since_init { 0 };
unsigned m_restarts { 0 };
unsigned m_restart_next_out = 0;
unsigned m_conflicts_since_restart = 0;
bool m_force_conflict_analysis = false;
unsigned m_simplifications = 0;
unsigned m_restart_threshold = 0;
unsigned m_luby_idx = 0;
unsigned m_conflicts_since_gc = 0;
unsigned m_gc_threshold = 0;
unsigned m_defrag_threshold = 0;
unsigned m_num_checkpoints = 0;
double m_min_d_tk = 0.0 ;
unsigned m_next_simplify = 0;
double m_simplify_mult = 1.5;
bool m_simplify_enabled = true;
bool m_restart_enabled = true;
bool guess(bool_var next);
bool decide();
bool_var next_var();
lbool bounded_search();
lbool basic_search();
lbool search();
lbool final_check();
void init_search();
literal_vector m_min_core;
bool m_min_core_valid { false };
void init_reason_unknown() { m_reason_unknown = "no reason given"; }
void init_assumptions(unsigned num_lits, literal const* lits);
void reassert_min_core();
void update_min_core();
void resolve_weighted();
void reset_assumptions();
void add_assumption(literal lit);
void reinit_assumptions();
void init_ext_assumptions();
bool tracking_assumptions() const;
bool is_assumption(literal l) const;
bool should_simplify() const;
void do_simplify();
void mk_model();
bool check_model(model const & m) const;
void do_restart(bool to_base);
svector<size_t> m_last_positions;
unsigned m_last_position_log;
unsigned m_restart_logs;
unsigned restart_level(bool to_base);
void log_stats();
bool should_cancel();
bool should_restart() const;
void set_next_restart();
void update_activity(bool_var v, double p);
bool reached_max_conflicts();
void sort_watch_lits();
void exchange_par();
lbool check_par(unsigned num_lits, literal const* lits);
lbool do_local_search(unsigned num_lits, literal const* lits);
lbool do_ddfw_search(unsigned num_lits, literal const* lits);
lbool do_prob_search(unsigned num_lits, literal const* lits);
lbool invoke_local_search(unsigned num_lits, literal const* lits);
void bounded_local_search();
lbool do_unit_walk();
struct scoped_ls;
protected:
bool should_gc() const;
void do_gc();
void gc_glue();
void gc_psm();
void gc_glue_psm();
void gc_psm_glue();
void save_psm();
void gc_half(char const * st_name);
void gc_dyn_psm();
bool activate_frozen_clause(clause & c);
unsigned psm(clause const & c) const;
bool can_delete(clause const & c) const;
bool can_delete3(literal l1, literal l2, literal l3) const;
void gc_reinit_stack(unsigned num_scopes);
bool is_asserting(unsigned new_lvl, clause_wrapper const& cw) const;
clause& get_clause(watch_list::iterator it) const {
SASSERT(it->get_kind() == watched::CLAUSE);
return get_clause(it->get_clause_offset());
}
clause& get_clause(watched const& w) const {
SASSERT(w.get_kind() == watched::CLAUSE);
return get_clause(w.get_clause_offset());
}
clause& get_clause(justification const& j) const {
SASSERT(j.is_clause());
return get_clause(j.get_clause_offset());
}
clause& get_clause(clause_offset cls_off) const {
return *(cls_allocator().get_clause(cls_off));
}
protected:
unsigned m_conflict_lvl;
literal_vector m_lemma;
literal_vector m_ext_antecedents;
bool use_backjumping(unsigned num_scopes) const;
bool allow_backtracking() const;
bool resolve_conflict();
lbool resolve_conflict_core();
void learn_lemma_and_backjump();
inline unsigned update_max_level(literal lit, unsigned lvl2, bool& unique_max) {
unsigned lvl1 = lvl(lit);
if (lvl1 < lvl2) return lvl2;
unique_max = lvl1 > lvl2;
return lvl1;
}
unsigned get_max_lvl(literal consequent, justification js, bool& unique_max);
void process_antecedent(literal antecedent, unsigned & num_marks);
void resolve_conflict_for_unsat_core();
void process_antecedent_for_unsat_core(literal antecedent);
void process_consequent_for_unsat_core(literal consequent, justification const& js);
void fill_ext_antecedents(literal consequent, justification js, bool probing);
unsigned skip_literals_above_conflict_level();
void updt_phase_of_vars();
void updt_phase_counters();
void do_toggle_search_state();
bool should_toggle_search_state();
bool is_sat_phase() const;
bool is_two_phase() const;
bool should_rephase();
void do_rephase();
bool should_reorder();
void do_reorder();
svector<char> m_diff_levels;
unsigned num_diff_levels(unsigned num, literal const * lits);
bool num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue);
bool num_diff_false_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue);
typedef approx_set_tpl<unsigned, u2u, unsigned> level_approx_set;
bool_var_vector m_unmark;
level_approx_set m_lvl_set;
literal_vector m_lemma_min_stack;
bool process_antecedent_for_minimization(literal antecedent);
bool implied_by_marked(literal lit);
void reset_unmark(unsigned old_size);
void updt_lemma_lvl_set();
bool minimize_lemma();
bool minimize_lemma_binres();
void reset_lemma_var_marks();
bool dyn_sub_res();
void push();
void pop(unsigned num_scopes);
void pop_reinit(unsigned num_scopes);
void shrink_vars(unsigned v);
void pop_vars(unsigned num_scopes);
void unassign_vars(unsigned old_sz, unsigned new_lvl);
void reinit_clauses(unsigned old_sz);
literal_vector m_user_scope_literals;
vector<svector<bool_var>> m_free_var_freeze;
literal_vector m_aux_literals;
svector<bin_clause> m_user_bin_clauses;
void gc_vars(bool_var max_var);
public:
bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; }
bool is_probing() const { return m_is_probing; }
bool is_free(bool_var v) const { return m_free_vars.contains(v); }
public:
void user_push() override;
void user_pop(unsigned num_scopes) override;
void pop_to_base_level();
unsigned num_user_scopes() const override { return m_user_scope_literals.size(); }
unsigned num_scopes() const override { return m_scopes.size(); }
reslimit& rlimit() { return m_rlimit; }
params_ref const& params() { return m_params; }
public:
bool do_cleanup(bool force);
void simplify(bool learned = true);
void asymmetric_branching();
unsigned scc_bin();
public:
lbool find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes);
lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_vector>& conseq);
private:
typedef hashtable<unsigned, u_hash, u_eq> index_set;
u_map<index_set> m_antecedents;
literal_vector m_todo_antecedents;
bool extract_assumptions(literal lit, index_set& s);
bool check_domain(literal lit, literal lit2);
std::ostream& display_index_set(std::ostream& out, index_set const& s) const;
lbool get_consequences(literal_vector const& assms, literal_vector const& lits, vector<literal_vector>& conseq);
lbool get_bounded_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_vector>& conseq);
void delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
bool extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
void fixup_consequence_core();
public:
void inc_activity(bool_var v) {
unsigned & act = m_activity[v];
act += m_activity_inc;
m_case_split_queue.activity_increased_eh(v);
if (act > (1 << 24))
rescale_activity();
}
void decay_activity() {
m_activity_inc *= m_config.m_variable_decay;
m_activity_inc /= 100;
}
private:
void rescale_activity();
void update_chb_activity(bool is_sat, unsigned qhead);
void update_lrb_reasoned();
void update_lrb_reasoned(literal lit);
public:
clause * const * begin_clauses() const { return m_clauses.begin(); }
clause * const * end_clauses() const { return m_clauses.end(); }
clause * const * begin_learned() const { return m_learned.begin(); }
clause * const * end_learned() const { return m_learned.end(); }
clause_vector const& learned() const { return m_learned; }
public:
bool check_invariant() const;
void display(std::ostream & out) const;
void display_watches(std::ostream & out) const;
void display_watches(std::ostream & out, literal lit) const;
void display_dimacs(std::ostream & out) const;
std::ostream& display_model(std::ostream& out) const;
void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
void display_assignment(std::ostream & out) const;
std::ostream& display_justification(std::ostream & out, justification const& j) const;
std::ostream& display_watch_list(std::ostream& out, watch_list const& wl) const;
protected:
void display_binary(std::ostream & out) const;
void display_units(std::ostream & out) const;
bool is_unit(clause const & c) const;
bool is_empty(clause const & c) const;
bool check_missed_propagation(clause_vector const & cs) const;
bool check_missed_propagation() const;
bool check_marks() const;
};
struct mk_stat {
solver const & m_solver;
mk_stat(solver const & s):m_solver(s) {}
void display(std::ostream & out) const;
};
class scoped_detach {
solver& s;
clause& c;
bool m_deleted;
public:
scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
if (!c.frozen()) s.detach_clause(c);
}
~scoped_detach() {
if (!m_deleted && !c.frozen()) s.attach_clause(c);
}
void del_clause() {
if (!m_deleted) {
s.del_clause(c);
m_deleted = true;
}
}
};
std::ostream & operator<<(std::ostream & out, mk_stat const & stat);
};