mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 03:33:35 +00:00
9fc4015c46
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
885 lines
35 KiB
C++
885 lines
35 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_solver.h
|
|
|
|
Abstract:
|
|
|
|
SAT solver main class.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2011-05-21.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#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 "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_binspr.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 {
|
|
|
|
/**
|
|
\brief Main statistic counters.
|
|
*/
|
|
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 {};
|
|
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; // DRAT for generating proofs
|
|
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; // MUS for minimal core extraction
|
|
binspr m_binspr;
|
|
bool m_inconsistent;
|
|
bool m_searching;
|
|
// A conflict is usually a single justification. That is, a justification
|
|
// for false. If m_not_l is not null_literal, then m_conflict is a
|
|
// justification for l, and the conflict is union of m_no_l and m_conflict;
|
|
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;
|
|
// branch variable selection:
|
|
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;
|
|
// phase
|
|
bool_vector m_phase;
|
|
bool_vector m_best_phase;
|
|
bool_vector m_prev_phase;
|
|
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;
|
|
unsigned m_rephase_lim;
|
|
unsigned m_rephase_inc;
|
|
unsigned m_reorder_lim;
|
|
unsigned m_reorder_inc;
|
|
var_queue 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;
|
|
|
|
svector<unsigned> m_visited;
|
|
unsigned m_visited_ts;
|
|
|
|
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; // for debugging purposes
|
|
literal_vector m_assumptions; // additional assumptions during check
|
|
literal_set m_assumption_set; // set of enabled assumptions
|
|
literal_set m_ext_assumption_set; // set of enabled assumptions
|
|
literal_vector m_core; // unsat 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 binspr;
|
|
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;
|
|
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;
|
|
public:
|
|
solver(params_ref const & p, reslimit& l);
|
|
~solver() override;
|
|
|
|
// -----------------------
|
|
//
|
|
// Misc
|
|
//
|
|
// -----------------------
|
|
void updt_params(params_ref const & p);
|
|
static void collect_param_descrs(param_descrs & d);
|
|
|
|
// collect statistics from sat solver
|
|
void collect_statistics(statistics & st) const;
|
|
void reset_statistics();
|
|
void display_status(std::ostream & out) const;
|
|
|
|
/**
|
|
\brief Copy (non learned) clauses from src to this solver.
|
|
Create missing variables if needed.
|
|
|
|
\pre the model converter of src and this must be empty
|
|
*/
|
|
void copy(solver const & src, bool copy_learned = false);
|
|
|
|
// -----------------------
|
|
//
|
|
// Variable & Clause creation
|
|
//
|
|
// -----------------------
|
|
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; }
|
|
|
|
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_ts(unsigned n, svector<unsigned>& v, unsigned& ts);
|
|
void init_visited();
|
|
void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
|
|
void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
|
|
bool is_visited(bool_var v) const { return is_visited(literal(v, false)); }
|
|
bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; }
|
|
bool all_distinct(literal_vector const& lits);
|
|
bool all_distinct(clause const& cl);
|
|
|
|
// -----------------------
|
|
//
|
|
// Basic
|
|
//
|
|
// -----------------------
|
|
public:
|
|
// is the state inconsistent?
|
|
bool inconsistent() const { return m_inconsistent; }
|
|
|
|
// number of variables and clauses
|
|
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); }
|
|
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)
|
|
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();
|
|
|
|
// -----------------------
|
|
//
|
|
// Propagation
|
|
//
|
|
// -----------------------
|
|
public:
|
|
// if update == true, then glue of learned clauses is updated.
|
|
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);
|
|
|
|
// -----------------------
|
|
//
|
|
// Search
|
|
//
|
|
// -----------------------
|
|
public:
|
|
lbool check(unsigned num_lits = 0, literal const* lits = nullptr);
|
|
|
|
// retrieve model if solver return sat
|
|
model const & get_model() const { return m_model; }
|
|
bool model_is_current() const { return m_model_is_current; }
|
|
|
|
// retrieve core from assumptions
|
|
literal_vector const& get_core() const { return m_core; }
|
|
|
|
model_converter const & get_model_converter() const { return m_mc; }
|
|
|
|
// The following methods are used when converting the state from the SAT solver back
|
|
// to a set of assertions.
|
|
|
|
// retrieve model converter that handles variable elimination and other transformations
|
|
void flush(model_converter& mc) { mc.flush(m_mc); }
|
|
|
|
// size of initial trail containing unit clauses
|
|
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
|
|
|
|
// literal at trail index i
|
|
literal trail_literal(unsigned i) const { return m_trail[i]; }
|
|
|
|
// collect n-ary clauses
|
|
clause_vector const& clauses() const { return m_clauses; }
|
|
|
|
// collect binary 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);
|
|
lbool do_unit_walk();
|
|
|
|
// -----------------------
|
|
//
|
|
// GC
|
|
//
|
|
// -----------------------
|
|
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;
|
|
|
|
// gc for lemmas in the reinit-stack
|
|
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));
|
|
}
|
|
|
|
// -----------------------
|
|
//
|
|
// Conflict resolution
|
|
//
|
|
// -----------------------
|
|
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);
|
|
|
|
// lemma minimization
|
|
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();
|
|
|
|
// -----------------------
|
|
//
|
|
// Backtracking
|
|
//
|
|
// -----------------------
|
|
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);
|
|
|
|
// -----------------------
|
|
//
|
|
// External
|
|
//
|
|
// -----------------------
|
|
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; }
|
|
// -----------------------
|
|
//
|
|
// Simplification
|
|
//
|
|
// -----------------------
|
|
public:
|
|
bool do_cleanup(bool force);
|
|
void simplify(bool learned = true);
|
|
void asymmetric_branching();
|
|
unsigned scc_bin();
|
|
|
|
// -----------------------
|
|
//
|
|
// Auxiliary methods.
|
|
//
|
|
// -----------------------
|
|
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);
|
|
|
|
// initialize and retrieve local search.
|
|
// local_search& init_local_search();
|
|
|
|
private:
|
|
|
|
typedef hashtable<unsigned, u_hash, u_eq> index_set;
|
|
|
|
u_map<index_set> m_antecedents;
|
|
literal_vector m_todo_antecedents;
|
|
// vector<literal_vector> m_binary_clause_graph;
|
|
|
|
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();
|
|
|
|
// -----------------------
|
|
//
|
|
// Activity related stuff
|
|
//
|
|
// -----------------------
|
|
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);
|
|
|
|
// -----------------------
|
|
//
|
|
// Iterators
|
|
//
|
|
// -----------------------
|
|
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; }
|
|
|
|
|
|
// -----------------------
|
|
//
|
|
// Debugging
|
|
//
|
|
// -----------------------
|
|
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);
|
|
};
|