Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_solver.cpp
Abstract:
SAT solver main class.
Author:
Leonardo de Moura (leonardo) 2011-05-21.
Revision History:
--*/
#include <cmath>
#ifndef SINGLE_THREAD
#include <thread>
#endif
#include "util/luby.h"
#include "util/trace.h"
#include "util/max_cliques.h"
#include "util/gparams.h"
#include "sat/sat_solver.h"
#include "sat/sat_integrity_checker.h"
#include "sat/sat_lookahead.h"
#include "sat/sat_ddfw.h"
#include "sat/sat_prob.h"
#include "sat/sat_anf_simplifier.h"
#include "sat/sat_cut_simplifier.h"
#if defined(_MSC_VER) && !defined(_M_ARM) && !defined(_M_ARM64)
# include <xmmintrin.h>
#endif
#define ENABLE_TERNARY true
namespace sat {
solver::solver(params_ref const & p, reslimit& l):
solver_core(l),
m_checkpoint_enabled(true),
m_config(p),
m_par(nullptr),
m_drat(*this),
m_cls_allocator_idx(false),
m_cleaner(*this),
m_simplifier(*this, p),
m_scc(*this, p),
m_asymm_branch(*this, p),
m_probing(*this, p),
m_mus(*this),
m_binspr(*this),
m_inconsistent(false),
m_searching(false),
m_conflict(justification(0)),
m_num_frozen(0),
m_activity_inc(128),
m_case_split_queue(m_activity),
m_qhead(0),
m_scope_lvl(0),
m_search_lvl(0),
m_fast_glue_avg(),
m_slow_glue_avg(),
m_fast_glue_backup(),
m_slow_glue_backup(),
m_trail_avg(),
m_params(p),
m_par_id(0),
m_par_syncing_clauses(false) {
init_reason_unknown();
updt_params(p);
m_best_phase_size = 0;
m_conflicts_since_gc = 0;
m_conflicts_since_init = 0;
m_next_simplify = 0;
m_num_checkpoints = 0;
m_simplifications = 0;
m_touch_index = 0;
m_ext = nullptr;
m_cuber = nullptr;
m_local_search = nullptr;
m_mc.set_solver(this);
mk_var(false, false);
}
solver::~solver() {
m_ext = nullptr;
SASSERT(m_config.m_num_threads > 1 || check_invariant());
CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
del_clauses(m_clauses);
CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
del_clauses(m_learned);
dealloc(m_cuber);
m_cuber = nullptr;
}
void solver::del_clauses(clause_vector& clauses) {
for (clause * cp : clauses)
dealloc_clause(cp);
clauses.reset();
++m_stats.m_non_learned_generation;
}
void solver::set_extension(extension* ext) {
m_ext = ext;
if (ext) {
ext->set_solver(this);
for (unsigned i = num_user_scopes(); i-- > 0;)
ext->user_push();
for (unsigned i = num_scopes(); i-- > 0;)
ext->push();
}
}
void solver::copy(solver const & src, bool copy_learned) {
pop_to_base_level();
del_clauses(m_clauses);
del_clauses(m_learned);
m_watches.reset();
m_assignment.reset();
m_justification.reset();
m_decision.reset();
m_eliminated.reset();
m_external.reset();
m_var_scope.reset();
m_activity.reset();
m_mark.reset();
m_lit_mark.reset();
m_best_phase.reset();
m_phase.reset();
m_prev_phase.reset();
m_assigned_since_gc.reset();
m_last_conflict.reset();
m_last_propagation.reset();
m_participated.reset();
m_canceled.reset();
m_reasoned.reset();
m_case_split_queue.reset();
m_simplifier.reset_todos();
m_qhead = 0;
m_trail.reset();
m_scopes.reset();
mk_var(false, false);
if (src.inconsistent()) {
set_conflict();
return;
}
for (bool_var v = num_vars(); v < src.num_vars(); v++) {
bool ext = src.m_external[v];
bool dvar = src.m_decision[v];
VERIFY(v == mk_var(ext, dvar));
if (src.was_eliminated(v)) {
set_eliminated(v, true);
}
m_phase[v] = src.m_phase[v];
m_best_phase[v] = src.m_best_phase[v];
m_prev_phase[v] = src.m_prev_phase[v];
m_activity[v] = src.m_activity[v];
m_case_split_queue.activity_changed_eh(v, false);
}
if (src.get_extension()) {
m_ext = src.get_extension()->copy(this);
}
unsigned trail_sz = src.init_trail_size();
for (unsigned i = 0; i < trail_sz; ++i) {
assign_unit(src.m_trail[i]);
}
{
unsigned sz = src.m_watches.size();
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
literal l = ~to_literal(l_idx);
if (src.was_eliminated(l.var())) continue;
watch_list const & wlist = src.m_watches[l_idx];
for (auto & wi : wlist) {
if (!wi.is_binary_clause())
continue;
literal l2 = wi.get_literal();
if (l.index() > l2.index() ||
src.was_eliminated(l2.var()))
continue;
watched w1(l2, wi.is_learned());
watched w2(l, wi.is_learned());
m_watches[(~l).index()].push_back(w1);
m_watches[(~l2).index()].push_back(w2);
}
}
}
{
literal_vector buffer;
for (clause* c : src.m_clauses) {
buffer.reset();
for (literal l : *c) buffer.push_back(l);
mk_clause_core(buffer);
}
unsigned num_learned = 0;
for (clause* c : src.m_learned) {
if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8) || copy_learned) {
buffer.reset();
for (literal l : *c) buffer.push_back(l);
clause* c1 = mk_clause_core(buffer.size(), buffer.data(), sat::status::redundant());
if (c1) {
++num_learned;
c1->set_glue(c->glue());
c1->set_psm(c->psm());
}
}
}
IF_VERBOSE(2, verbose_stream() << "(sat.copy :learned " << num_learned << ")\n";);
}
m_best_phase_size = src.m_best_phase_size;
if (m_best_phase_size > 0) {
for (bool_var v = 0; v < num_vars(); ++v) {
m_best_phase[v] = src.m_best_phase[v];
}
}
m_user_scope_literals.reset();
m_user_scope_literals.append(src.m_user_scope_literals);
m_mc = src.m_mc;
m_stats.m_units = init_trail_size();
}
void solver::reset_var(bool_var v, bool ext, bool dvar) {
m_watches[2*v].reset();
m_watches[2*v+1].reset();
m_assignment[2*v] = l_undef;
m_assignment[2*v+1] = l_undef;
m_justification[v] = justification(UINT_MAX);
m_decision[v] = dvar;
m_eliminated[v] = false;
m_external[v] = ext;
m_var_scope[v] = scope_lvl();
m_touched[v] = 0;
m_activity[v] = 0;
m_mark[v] = false;
m_lit_mark[2*v] = false;
m_lit_mark[2*v+1] = false;
m_phase[v] = false;
m_best_phase[v] = false;
m_prev_phase[v] = false;
m_assigned_since_gc[v] = false;
m_last_conflict[v] = 0;
m_last_propagation[v] = 0;
m_participated[v] = 0;
m_canceled[v] = 0;
m_reasoned[v] = 0;
m_case_split_queue.mk_var_eh(v);
m_simplifier.insert_elim_todo(v);
}
bool_var solver::mk_var(bool ext, bool dvar) {
m_model_is_current = false;
m_stats.m_mk_var++;
bool_var v = m_justification.size();
if (!m_free_vars.empty()) {
v = m_free_vars.back();
m_free_vars.pop_back();
m_active_vars.push_back(v);
reset_var(v, ext, dvar);
return v;
}
m_active_vars.push_back(v);
m_watches.push_back(watch_list());
m_watches.push_back(watch_list());
m_assignment.push_back(l_undef);
m_assignment.push_back(l_undef);
m_justification.push_back(justification(UINT_MAX));
m_decision.push_back(dvar);
m_eliminated.push_back(false);
m_external.push_back(ext);
m_var_scope.push_back(scope_lvl());
m_touched.push_back(0);
m_activity.push_back(0);
m_mark.push_back(false);
m_lit_mark.push_back(false);
m_lit_mark.push_back(false);
m_phase.push_back(false);
m_best_phase.push_back(false);
m_prev_phase.push_back(false);
m_assigned_since_gc.push_back(false);
m_last_conflict.push_back(0);
m_last_propagation.push_back(0);
m_participated.push_back(0);
m_canceled.push_back(0);
m_reasoned.push_back(0);
m_case_split_queue.mk_var_eh(v);
m_simplifier.insert_elim_todo(v);
SASSERT(!was_eliminated(v));
return v;
}
void solver::set_non_external(bool_var v) {
m_external[v] = false;
}
void solver::set_external(bool_var v) {
m_external[v] = true;
}
void solver::set_eliminated(bool_var v, bool f) {
if (m_eliminated[v] == f)
return;
if (!f)
reset_var(v, m_external[v], m_decision[v]);
else if (f && m_ext)
m_ext->set_eliminated(v);
m_eliminated[v] = f;
}
clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
m_model_is_current = false;
for (unsigned i = 0; i < num_lits; i++)
VERIFY(!was_eliminated(lits[i]));
DEBUG_CODE({
for (unsigned i = 0; i < num_lits; i++) {
CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";);
SASSERT(!was_eliminated(lits[i]));
}
});
if (m_user_scope_literals.empty()) {
return mk_clause_core(num_lits, lits, st);
}
else {
m_aux_literals.reset();
m_aux_literals.append(num_lits, lits);
m_aux_literals.append(m_user_scope_literals);
return mk_clause_core(m_aux_literals.size(), m_aux_literals.data(), st);
}
}
clause* solver::mk_clause(literal l1, literal l2, sat::status st) {
literal ls[2] = { l1, l2 };
return mk_clause(2, ls, st);
}
clause* solver::mk_clause(literal l1, literal l2, literal l3, sat::status st) {
literal ls[3] = { l1, l2, l3 };
return mk_clause(3, ls, st);
}
void solver::del_clause(clause& c) {
if (!c.is_learned()) {
m_stats.m_non_learned_generation++;
}
if (c.frozen()) {
--m_num_frozen;
}
if (!c.was_removed() && m_config.m_drat && !m_drat.is_cleaned(c)) {
m_drat.del(c);
}
dealloc_clause(&c);
if (m_searching)
m_stats.m_del_clause++;
}
void solver::drat_explain_conflict() {
if (m_config.m_drat && m_ext) {
extension::scoped_drating _sd(*m_ext);
bool unique_max;
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);
resolve_conflict_for_unsat_core();
}
}
void solver::drat_log_unit(literal lit, justification j) {
if (!m_ext)
return;
extension::scoped_drating _sd(*m_ext.get());
if (j.get_kind() == justification::EXT_JUSTIFICATION)
fill_ext_antecedents(lit, j, false);
m_drat.add(lit, m_searching);
}
void solver::drat_log_clause(unsigned num_lits, literal const* lits, sat::status st) {
m_drat.add(num_lits, lits, st);
}
clause * solver::mk_clause_core(unsigned num_lits, literal * lits, sat::status st) {
bool redundant = st.is_redundant();
TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << (redundant?" learned":" aux") << "\n";);
if (!redundant || !st.is_sat()) {
unsigned old_sz = num_lits;
bool keep = simplify_clause(num_lits, lits);
TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";);
if (!keep) {
return nullptr;
}
if (m_config.m_drat && old_sz > num_lits)
drat_log_clause(num_lits, lits, st);
++m_stats.m_non_learned_generation;
if (!m_searching) {
m_mc.add_clause(num_lits, lits);
}
}
switch (num_lits) {
case 0:
set_conflict();
return nullptr;
case 1:
if (m_config.m_drat && (!st.is_sat() || st.is_input()))
drat_log_clause(num_lits, lits, st);
assign_unit(lits[0]);
return nullptr;
case 2:
mk_bin_clause(lits[0], lits[1], st);
if (redundant && m_par)
m_par->share_clause(*this, lits[0], lits[1]);
return nullptr;
case 3:
if (ENABLE_TERNARY)
return mk_ter_clause(lits, st);
Z3_fallthrough;
default:
return mk_nary_clause(num_lits, lits, st);
}
}
void solver::mk_bin_clause(literal l1, literal l2, sat::status st) {
bool redundant = st.is_redundant();
m_touched[l1.var()] = m_touch_index;
m_touched[l2.var()] = m_touch_index;
if (redundant && find_binary_watch(get_wlist(~l1), ~l2) && value(l1) == l_undef) {
assign_unit(l1);
return;
}
if (redundant && find_binary_watch(get_wlist(~l2), ~l1) && value(l2) == l_undef) {
assign_unit(l2);
return;
}
watched* w0 = redundant ? find_binary_watch(get_wlist(~l1), l2) : nullptr;
if (w0) {
TRACE("sat", tout << "found binary " << l1 << " " << l2 << "\n";);
if (w0->is_learned() && !redundant) {
w0->set_learned(false);
w0 = find_binary_watch(get_wlist(~l2), l1);
VERIFY(w0);
w0->set_learned(false);
}
if (propagate_bin_clause(l1, l2) && !at_base_lvl() && !redundant)
push_reinit_stack(l1, l2);
else if (has_variables_to_reinit(l1, l2))
push_reinit_stack(l1, l2);
return;
}
if (m_config.m_drat)
m_drat.add(l1, l2, st);
if (propagate_bin_clause(l1, l2)) {
if (at_base_lvl())
return;
push_reinit_stack(l1, l2);
}
else if (has_variables_to_reinit(l1, l2))
push_reinit_stack(l1, l2);
m_stats.m_mk_bin_clause++;
get_wlist(~l1).push_back(watched(l2, redundant));
get_wlist(~l2).push_back(watched(l1, redundant));
}
bool solver::has_variables_to_reinit(clause const& c) const {
for (auto lit : c)
if (m_var_scope[lit.var()] > 0)
return true;
return false;
}
bool solver::has_variables_to_reinit(literal l1, literal l2) const {
if (at_base_lvl())
return false;
if (m_var_scope[l1.var()] > 0)
return true;
if (m_var_scope[l2.var()] > 0)
return true;
return false;
}
bool solver::propagate_bin_clause(literal l1, literal l2) {
if (value(l2) == l_false) {
m_stats.m_bin_propagate++;
assign(l1, justification(lvl(l2), l2));
return true;
}
if (value(l1) == l_false) {
m_stats.m_bin_propagate++;
assign(l2, justification(lvl(l1), l1));
return true;
}
return false;
}
void solver::push_reinit_stack(clause & c) {
SASSERT(!at_base_lvl());
TRACE("sat_reinit", tout << "adding to reinit stack: " << c << "\n";);
m_clauses_to_reinit.push_back(clause_wrapper(c));
c.set_reinit_stack(true);
}
void solver::push_reinit_stack(literal l1, literal l2) {
TRACE("sat_reinit", tout << "adding to reinit stack: " << l1 << " " << l2 << "\n";);
m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
}
clause * solver::mk_ter_clause(literal * lits, sat::status st) {
VERIFY(ENABLE_TERNARY);
m_stats.m_mk_ter_clause++;
clause * r = alloc_clause(3, lits, st.is_redundant());
bool reinit = attach_ter_clause(*r, st);
if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
if (st.is_redundant())
m_learned.push_back(r);
else
m_clauses.push_back(r);
for (literal l : *r) {
m_touched[l.var()] = m_touch_index;
}
return r;
}
bool solver::attach_ter_clause(clause & c, sat::status st) {
VERIFY(ENABLE_TERNARY);
bool reinit = false;
if (m_config.m_drat) m_drat.add(c, st);
TRACE("sat_verbose", tout << c << "\n";);
SASSERT(!c.was_removed());
m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
if (!at_base_lvl())
reinit = propagate_ter_clause(c);
return reinit;
}
bool solver::propagate_ter_clause(clause& c) {
bool reinit = false;
if (value(c[1]) == l_false && value(c[2]) == l_false) {
m_stats.m_ter_propagate++;
assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2]));
reinit = !c.is_learned();
}
else if (value(c[0]) == l_false && value(c[2]) == l_false) {
m_stats.m_ter_propagate++;
assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2]));
reinit = !c.is_learned();
}
else if (value(c[0]) == l_false && value(c[1]) == l_false) {
m_stats.m_ter_propagate++;
assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1]));
reinit = !c.is_learned();
}
return reinit;
}
clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) {
m_stats.m_mk_clause++;
clause * r = alloc_clause(num_lits, lits, st.is_redundant());
SASSERT(!st.is_redundant() || r->is_learned());
bool reinit = attach_nary_clause(*r, st.is_sat() && st.is_redundant());
if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
if (st.is_redundant()) {
m_learned.push_back(r);
}
else {
m_clauses.push_back(r);
}
if (m_config.m_drat) {
m_drat.add(*r, st);
}
for (literal l : *r) {
m_touched[l.var()] = m_touch_index;
}
return r;
}
bool solver::attach_nary_clause(clause & c, bool is_asserting) {
bool reinit = false;
clause_offset cls_off = cls_allocator().get_offset(&c);
if (!at_base_lvl()) {
if (is_asserting) {
unsigned w2_idx = select_learned_watch_lit(c);
std::swap(c[1], c[w2_idx]);
}
else {
unsigned w1_idx = select_watch_lit(c, 0);
std::swap(c[0], c[w1_idx]);
unsigned w2_idx = select_watch_lit(c, 1);
std::swap(c[1], c[w2_idx]);
}
if (value(c[0]) == l_false) {
m_stats.m_propagate++;
unsigned level = lvl(c[0]);
for (unsigned i = c.size(); i-- > 2; ) {
level = std::max(level, lvl(c[i]));
}
assign(c[1], justification(level, cls_off));
reinit |= !c.is_learned();
}
else if (value(c[1]) == l_false) {
m_stats.m_propagate++;
unsigned level = lvl(c[1]);
for (unsigned i = c.size(); i-- > 2; ) {
level = std::max(level, lvl(c[i]));
}
assign(c[0], justification(level, cls_off));
reinit |= !c.is_learned();
}
}
unsigned some_idx = c.size() >> 1;
literal block_lit = c[some_idx];
VERIFY(!c.frozen());
DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
SASSERT(c[0] != c[1]);
m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
return reinit;
}
void solver::attach_clause(clause & c, bool & reinit) {
SASSERT(c.size() > 2);
reinit = false;
if (ENABLE_TERNARY && c.size() == 3)
reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
else
reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
}
void solver::set_learned(clause& c, bool redundant) {
if (c.is_learned() != redundant)
c.set_learned(redundant);
}
void solver::set_learned1(literal l1, literal l2, bool redundant) {
for (watched& w : get_wlist(~l1)) {
if (w.is_binary_clause() && l2 == w.get_literal() && !w.is_learned()) {
w.set_learned(redundant);
break;
}
}
}
void solver::shrink(clause& c, unsigned old_sz, unsigned new_sz) {
SASSERT(new_sz > 2);
SASSERT(old_sz >= new_sz);
if (old_sz != new_sz) {
c.shrink(new_sz);
for (literal l : c) {
m_touched[l.var()] = m_touch_index;
}
if (m_config.m_drat) {
m_drat.add(c, status::redundant());
c.restore(old_sz);
m_drat.del(c);
c.shrink(new_sz);
}
}
}
bool solver::memory_pressure() {
return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size();
}
struct solver::cmp_activity {
solver& s;
cmp_activity(solver& s):s(s) {}
bool operator()(bool_var v1, bool_var v2) const {
return s.m_activity[v1] > s.m_activity[v2];
}
};
bool solver::should_defrag() {
if (m_defrag_threshold > 0) --m_defrag_threshold;
return m_defrag_threshold == 0 && m_config.m_gc_defrag;
}
void solver::defrag_clauses() {
m_defrag_threshold = 2;
if (memory_pressure()) return;
pop(scope_lvl());
IF_VERBOSE(2, verbose_stream() << "(sat-defrag)\n");
clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx];
ptr_vector<clause> new_clauses, new_learned;
for (clause* c : m_clauses) c->unmark_used();
for (clause* c : m_learned) c->unmark_used();
svector<bool_var> vars;
for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i);
std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this));
literal_vector lits;
for (bool_var v : vars) lits.push_back(literal(v, false)), lits.push_back(literal(v, true));
for (literal lit : lits) {
watch_list& wlist = m_watches[lit.index()];
for (watched& w : wlist) {
if (w.is_clause()) {
clause& c1 = get_clause(w);
clause_offset offset;
if (c1.was_used()) {
offset = c1.get_new_offset();
}
else {
clause* c2 = alloc.copy_clause(c1);
c1.mark_used();
if (c1.is_learned()) {
new_learned.push_back(c2);
}
else {
new_clauses.push_back(c2);
}
offset = get_offset(*c2);
c1.set_new_offset(offset);
}
w = watched(w.get_blocked_literal(), offset);
}
}
}
for (clause* c : m_clauses) {
if (!c->was_used()) {
SASSERT(c->size() == 3);
new_clauses.push_back(alloc.copy_clause(*c));
}
dealloc_clause(c);
}
for (clause* c : m_learned) {
if (!c->was_used()) {
SASSERT(c->size() == 3);
new_learned.push_back(alloc.copy_clause(*c));
}
dealloc_clause(c);
}
m_clauses.swap(new_clauses);
m_learned.swap(new_learned);
cls_allocator().finalize();
m_cls_allocator_idx = !m_cls_allocator_idx;
reinit_assumptions();
}
void solver::set_learned(literal l1, literal l2, bool redundant) {
set_learned1(l1, l2, redundant);
set_learned1(l2, l1, redundant);
}
\brief Select a watch literal starting the search at the given position.
This method is only used for clauses created during the search.
I use the following rules to select a watch literal.
1- select a literal l in idx >= starting_at such that value(l) = l_true,
and for all l' in idx' >= starting_at . value(l') = l_true implies lvl(l) <= lvl(l')
The purpose of this rule is to make the clause inactive for as long as possible. A clause
is inactive when it contains a literal assigned to true.
2- if there isn't a literal assigned to true, then select an unassigned literal l in idx >= starting_at
3- if there isn't a literal l in idx >= starting_at such that value(l) = l_true or
value(l) = l_undef (that is, all literals at positions >= starting_at are assigned
to false), then peek the literal l such that for all l' starting at starting_at
lvl(l) >= lvl(l')
Without rule 3, boolean propagation is incomplete, that is, it may miss possible propagations.
\remark The method select_lemma_watch_lit is used to select the watch literal for regular learned clauses.
*/
unsigned solver::select_watch_lit(clause const & cls, unsigned starting_at) const {
SASSERT(cls.size() >= 2);
unsigned min_true_idx = UINT_MAX;
unsigned max_false_idx = UINT_MAX;
unsigned unknown_idx = UINT_MAX;
unsigned n = cls.size();
for (unsigned i = starting_at; i < n; i++) {
literal l = cls[i];
switch(value(l)) {
case l_false:
if (max_false_idx == UINT_MAX || lvl(l) > lvl(cls[max_false_idx]))
max_false_idx = i;
break;
case l_undef:
unknown_idx = i;
break;
case l_true:
if (min_true_idx == UINT_MAX || lvl(l) < lvl(cls[min_true_idx]))
min_true_idx = i;
break;
}
}
if (min_true_idx != UINT_MAX)
return min_true_idx;
if (unknown_idx != UINT_MAX)
return unknown_idx;
SASSERT(max_false_idx != UINT_MAX);
return max_false_idx;
}
\brief The learned clauses (lemmas) produced by the SAT solver
have the property that the first literal will be implied by it
after backtracking. All other literals are assigned to (or
implied to be) false when the learned clause is created. The
first watch literal will always be the first literal. The
second watch literal is computed by this method. It should be
the literal with the highest decision level.
// TODO: do we really need this? strength the conflict resolution
*/
unsigned solver::select_learned_watch_lit(clause const & cls) const {
SASSERT(cls.size() >= 2);
unsigned max_false_idx = UINT_MAX;
unsigned num_lits = cls.size();
for (unsigned i = 1; i < num_lits; i++) {
literal l = cls[i];
CTRACE("sat", value(l) != l_false, tout << l << ":=" << value(l););
SASSERT(value(l) == l_false);
if (max_false_idx == UINT_MAX || lvl(l) > lvl(cls[max_false_idx]))
max_false_idx = i;
}
return max_false_idx;
}
template<bool lvl0>
bool solver::simplify_clause_core(unsigned & num_lits, literal * lits) const {
std::sort(lits, lits+num_lits);
literal prev = null_literal;
unsigned i = 0;
unsigned j = 0;
for (; i < num_lits; i++) {
literal curr = lits[i];
lbool val = value(curr);
if (!lvl0 && lvl(curr) > 0)
val = l_undef;
switch (val) {
case l_false:
break;
case l_undef:
if (curr == ~prev)
return false;
if (curr != prev) {
prev = curr;
if (i != j)
std::swap(lits[j], lits[i]);
j++;
}
break;
case l_true:
return false;
}
}
num_lits = j;
return true;
}
bool solver::simplify_clause(unsigned & num_lits, literal * lits) const {
if (at_base_lvl())
return simplify_clause_core<true>(num_lits, lits);
else
return simplify_clause_core<false>(num_lits, lits);
}
void solver::detach_bin_clause(literal l1, literal l2, bool redundant) {
get_wlist(~l1).erase(watched(l2, redundant));
get_wlist(~l2).erase(watched(l1, redundant));
if (m_config.m_drat) m_drat.del(l1, l2);
}
void solver::detach_clause(clause & c) {
if (ENABLE_TERNARY && c.size() == 3)
detach_ter_clause(c);
else
detach_nary_clause(c);
}
void solver::detach_nary_clause(clause & c) {
clause_offset cls_off = get_offset(c);
erase_clause_watch(get_wlist(~c[0]), cls_off);
erase_clause_watch(get_wlist(~c[1]), cls_off);
}
void solver::detach_ter_clause(clause & c) {
erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
}
void solver::set_conflict(justification c, literal not_l) {
if (m_inconsistent)
return;
m_inconsistent = true;
m_conflict = c;
m_not_l = not_l;
}
void solver::assign_core(literal l, justification j) {
SASSERT(value(l) == l_undef);
TRACE("sat_assign_core", tout << l << " " << j << "\n";);
if (j.level() == 0) {
if (m_config.m_drat)
drat_log_unit(l, j);
j = justification(0);
}
else {
VERIFY(!at_base_lvl());
}
m_assignment[l.index()] = l_true;
m_assignment[(~l).index()] = l_false;
bool_var v = l.var();
m_justification[v] = j;
m_phase[v] = !l.sign();
m_assigned_since_gc[v] = true;
m_trail.push_back(l);
switch (m_config.m_branching_heuristic) {
case BH_VSIDS:
break;
case BH_CHB:
m_last_propagation[v] = m_stats.m_conflict;
break;
}
if (m_config.m_anti_exploration) {
uint64_t age = m_stats.m_conflict - m_canceled[v];
if (age > 0) {
double decay = pow(0.95, static_cast<double>(age));
set_activity(v, static_cast<unsigned>(m_activity[v] * decay));
m_canceled[v] = m_stats.m_conflict;
}
}
if (m_config.m_propagate_prefetch) {
#if defined(__GNUC__) || defined(__clang__)
__builtin_prefetch((const char*)((m_watches[l.index()].data())));
#else
#if !defined(_M_ARM) && !defined(_M_ARM64)
_mm_prefetch((const char*)((m_watches[l.index()].data())), _MM_HINT_T1);
#endif
#endif
}
SASSERT(!l.sign() || !m_phase[v]);
SASSERT(l.sign() || m_phase[v]);
SASSERT(!l.sign() || value(v) == l_false);
SASSERT(l.sign() || value(v) == l_true);
SASSERT(value(l) == l_true);
SASSERT(value(~l) == l_false);
}
lbool solver::status(clause const & c) const {
bool found_undef = false;
for (literal lit : c) {
switch (value(lit)) {
case l_true:
return l_true;
case l_undef:
found_undef = true;
break;
default:
break;
}
}
return found_undef ? l_undef : l_false;
}
bool solver::propagate_core(bool update) {
while (m_qhead < m_trail.size() && !m_inconsistent) {
do {
checkpoint();
m_cleaner.dec();
literal l = m_trail[m_qhead];
m_qhead++;
if (!propagate_literal(l, update))
return false;
} while (m_qhead < m_trail.size());
if (m_ext && (!is_probing() || at_base_lvl()))
m_ext->unit_propagate();
}
if (m_inconsistent)
return false;
SASSERT(m_qhead == m_trail.size());
SASSERT(!m_inconsistent);
return true;
}
bool solver::propagate(bool update) {
unsigned qhead = m_qhead;
bool r = propagate_core(update);
if (m_config.m_branching_heuristic == BH_CHB) {
update_chb_activity(r, qhead);
}
CASSERT("sat_propagate", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
return r;
}
bool solver::propagate_literal(literal l, bool update) {
literal l1, l2;
lbool val1, val2;
bool keep;
unsigned curr_level = lvl(l);
TRACE("sat_propagate", tout << "propagating: " << l << "@" << curr_level << " " << m_justification[l.var()] << "\n"; );
literal not_l = ~l;
SASSERT(value(l) == l_true);
SASSERT(value(not_l) == l_false);
watch_list& wlist = m_watches[l.index()];
m_asymm_branch.dec(wlist.size());
m_probing.dec(wlist.size());
watch_list::iterator it = wlist.begin();
watch_list::iterator it2 = it;
watch_list::iterator end = wlist.end();
#define CONFLICT_CLEANUP() { \
for (; it != end; ++it, ++it2) \
*it2 = *it; \
wlist.set_end(it2); \
}
for (; it != end; ++it) {
switch (it->get_kind()) {
case watched::BINARY:
l1 = it->get_literal();
switch (value(l1)) {
case l_false:
CONFLICT_CLEANUP();
set_conflict(justification(curr_level, not_l), ~l1);
return false;
case l_undef:
m_stats.m_bin_propagate++;
assign_core(l1, justification(curr_level, not_l));
break;
case l_true:
break;
}
*it2 = *it;
it2++;
break;
case watched::TERNARY:
l1 = it->get_literal1();
l2 = it->get_literal2();
val1 = value(l1);
val2 = value(l2);
if (val1 == l_false && val2 == l_undef) {
m_stats.m_ter_propagate++;
assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l));
}
else if (val1 == l_undef && val2 == l_false) {
m_stats.m_ter_propagate++;
assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l));
}
else if (val1 == l_false && val2 == l_false) {
CONFLICT_CLEANUP();
set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2);
return false;
}
*it2 = *it;
it2++;
break;
case watched::CLAUSE: {
if (value(it->get_blocked_literal()) == l_true) {
TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
tout << get_clause(it) << "\n";);
*it2 = *it;
it2++;
break;
}
clause_offset cls_off = it->get_clause_offset();
clause& c = get_clause(cls_off);
TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";);
if (c[0] == not_l)
std::swap(c[0], c[1]);
CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";);
if (c.was_removed() || c.size() == 1 || c[1] != not_l) {
*it2 = *it;
it2++;
break;
}
if (value(c[0]) == l_true) {
it2->set_clause(c[0], cls_off);
it2++;
break;
}
VERIFY(c[1] == not_l);
literal* l_it = c.begin() + 2;
literal* l_end = c.end();
unsigned assign_level = curr_level;
unsigned max_index = 1;
for (; l_it != l_end; ++l_it) {
if (value(*l_it) != l_false) {
c[1] = *l_it;
*l_it = not_l;
DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
goto end_clause_case;
}
}
SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef);
if (assign_level != scope_lvl()) {
for (unsigned i = 2; i < c.size(); ++i) {
unsigned level = lvl(c[i]);
if (level > assign_level) {
assign_level = level;
max_index = i;
}
}
IF_VERBOSE(20, verbose_stream() << "lower assignment level " << assign_level << " scope: " << scope_lvl() << "\n");
}
if (value(c[0]) == l_false) {
assign_level = std::max(assign_level, lvl(c[0]));
c.mark_used();
CONFLICT_CLEANUP();
set_conflict(justification(assign_level, cls_off));
return false;
}
else {
if (max_index != 1) {
IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n");
std::swap(c[1], c[max_index]);
m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
}
else {
*it2 = *it;
it2++;
}
m_stats.m_propagate++;
c.mark_used();
assign_core(c[0], justification(assign_level, cls_off));
if (update && c.is_learned() && c.glue() > 2) {
unsigned glue;
if (num_diff_levels_below(c.size(), c.begin(), c.glue() - 1, glue)) {
c.set_glue(glue);
}
}
}
end_clause_case:
break;
}
case watched::EXT_CONSTRAINT:
SASSERT(m_ext);
keep = m_ext->propagated(l, it->get_ext_constraint_idx());
if (m_inconsistent) {
if (!keep) {
++it;
}
CONFLICT_CLEANUP();
return false;
}
if (keep) {
*it2 = *it;
it2++;
}
break;
default:
UNREACHABLE();
break;
}
}
wlist.set_end(it2);
if (m_ext && m_external[l.var()] && (!is_probing() || at_base_lvl()))
m_ext->asserted(l);
return true;
}
void solver::display_lookahead_scores(std::ostream& out) {
lookahead lh(*this);
lh.display_lookahead_scores(out);
}
lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
bool is_first = !m_cuber;
if (is_first) {
m_cuber = alloc(lookahead, *this);
}
lbool result = m_cuber->cube(vars, lits, backtrack_level);
m_cuber->update_cube_statistics(m_aux_stats);
switch (result) {
case l_false:
dealloc(m_cuber);
m_cuber = nullptr;
if (is_first) {
pop_to_base_level();
set_conflict();
}
break;
case l_true: {
lits.reset();
pop_to_base_level();
model const& mdl = m_cuber->get_model();
for (bool_var v = 0; v < mdl.size(); ++v) {
if (value(v) != l_undef) {
continue;
}
literal l(v, false);
if (mdl[v] != l_true) l.neg();
if (inconsistent())
return l_undef;
push();
assign_core(l, justification(scope_lvl()));
propagate(false);
}
mk_model();
break;
}
default:
break;
}
return result;
}
lbool solver::check(unsigned num_lits, literal const* lits) {
init_reason_unknown();
pop_to_base_level();
m_stats.m_units = init_trail_size();
IF_VERBOSE(2, verbose_stream() << "(sat.solver)\n";);
SASSERT(at_base_lvl());
if (m_config.m_ddfw_search) {
m_cleaner(true);
return do_ddfw_search(num_lits, lits);
}
if (m_config.m_prob_search) {
m_cleaner(true);
return do_prob_search(num_lits, lits);
}
if (m_config.m_local_search) {
m_cleaner(true);
return do_local_search(num_lits, lits);
}
if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 ||
m_config.m_ddfw_threads > 0) && !m_par && !m_ext) {
SASSERT(scope_lvl() == 0);
return check_par(num_lits, lits);
}
flet<bool> _searching(m_searching, true);
m_clone = nullptr;
if (m_mc.empty() && gparams::get_ref().get_bool("model_validate", false)) {
m_clone = alloc(solver, m_params, m_rlimit);
m_clone->copy(*this);
m_clone->set_extension(nullptr);
}
try {
init_search();
if (check_inconsistent()) return l_false;
propagate(false);
if (check_inconsistent()) return l_false;
init_assumptions(num_lits, lits);
propagate(false);
if (check_inconsistent()) return l_false;
if (m_config.m_force_cleanup) do_cleanup(true);
TRACE("sat", display(tout););
if (m_config.m_gc_burst) {
m_conflicts_since_gc = m_gc_threshold + 1;
do_gc();
}
if (m_config.m_enable_pre_simplify) {
do_simplify();
if (check_inconsistent()) return l_false;
}
if (m_config.m_max_conflicts == 0) {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";);
TRACE("sat", display(tout); m_mc.display(tout););
return l_undef;
}
log_stats();
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
m_restart_threshold = m_config.m_burst_search;
lbool r = bounded_search();
log_stats();
if (r != l_undef)
return r;
pop_reinit(scope_lvl());
m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial;
}
lbool is_sat = search();
log_stats();
return is_sat;
}
catch (const abort_solver &) {
m_reason_unknown = "sat.giveup";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort giveup\")\n";);
return l_undef;
}
}
bool solver::should_cancel() {
if (limit_reached() || memory_exceeded()) {
return true;
}
if (m_config.m_restart_max <= m_restarts) {
m_reason_unknown = "sat.max.restarts";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
return true;
}
if (m_config.m_inprocess_max <= m_simplifications) {
m_reason_unknown = "sat.max.inprocess";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-inprocess\")\n";);
return true;
}
if (reached_max_conflicts()) {
return true;
}
return false;
}
enum par_exception_kind {
DEFAULT_EX,
ERROR_EX
};
lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) {
literal_vector _lits(num_lits, lits);
for (literal lit : m_user_scope_literals) _lits.push_back(~lit);
struct scoped_ls {
solver& s;
scoped_ls(solver& s): s(s) {}
~scoped_ls() {
dealloc(s.m_local_search);
s.m_local_search = nullptr;
}
};
scoped_ls _ls(*this);
if (inconsistent())
return l_false;
scoped_limits scoped_rl(rlimit());
SASSERT(m_local_search);
m_local_search->add(*this);
m_local_search->updt_params(m_params);
scoped_rl.push_child(&(m_local_search->rlimit()));
lbool r = m_local_search->check(_lits.size(), _lits.data(), nullptr);
if (r == l_true) {
m_model = m_local_search->get_model();
m_model_is_current = true;
}
return r;
}
lbool solver::do_local_search(unsigned num_lits, literal const* lits) {
SASSERT(!m_local_search);
m_local_search = alloc(local_search);
return invoke_local_search(num_lits, lits);
}
lbool solver::do_ddfw_search(unsigned num_lits, literal const* lits) {
if (m_ext) return l_undef;
SASSERT(!m_local_search);
m_local_search = alloc(ddfw);
return invoke_local_search(num_lits, lits);
}
lbool solver::do_prob_search(unsigned num_lits, literal const* lits) {
if (m_ext) return l_undef;
if (num_lits > 0 || !m_user_scope_literals.empty()) return l_undef;
SASSERT(!m_local_search);
m_local_search = alloc(prob);
return invoke_local_search(num_lits, lits);
}
#ifdef SINGLE_THREAD
lbool solver::check_par(unsigned num_lits, literal const* lits) {
return l_undef;
}
#else
lbool solver::check_par(unsigned num_lits, literal const* lits) {
if (!rlimit().inc()) {
return l_undef;
}
if (m_ext)
return l_undef;
scoped_ptr_vector<i_local_search> ls;
scoped_ptr_vector<solver> uw;
int num_extra_solvers = m_config.m_num_threads - 1;
int num_local_search = static_cast<int>(m_config.m_local_search_threads);
int num_ddfw = m_ext ? 0 : static_cast<int>(m_config.m_ddfw_threads);
int num_threads = num_extra_solvers + 1 + num_local_search + num_ddfw;
for (int i = 0; i < num_local_search; ++i) {
local_search* l = alloc(local_search);
l->updt_params(m_params);
l->add(*this);
l->set_seed(m_config.m_random_seed + i);
ls.push_back(l);
}
vector<reslimit> lims(num_ddfw);
for (int i = 0; i < num_ddfw; ++i) {
ddfw* d = alloc(ddfw);
d->updt_params(m_params);
d->set_seed(m_config.m_random_seed + i);
d->add(*this);
ls.push_back(d);
}
int local_search_offset = num_extra_solvers;
int main_solver_offset = num_extra_solvers + num_local_search + num_ddfw;
#define IS_AUX_SOLVER(i) (0 <= i && i < num_extra_solvers)
#define IS_LOCAL_SEARCH(i) (local_search_offset <= i && i < main_solver_offset)
#define IS_MAIN_SOLVER(i) (i == main_solver_offset)
sat::parallel par(*this);
par.reserve(num_threads, 1 << 12);
par.init_solvers(*this, num_extra_solvers);
for (unsigned i = 0; i < ls.size(); ++i) {
par.push_child(ls[i]->rlimit());
}
for (reslimit& rl : lims) {
par.push_child(rl);
}
for (unsigned i = 0; i < uw.size(); ++i) {
uw[i]->set_par(&par, 0);
}
int finished_id = -1;
std::string ex_msg;
par_exception_kind ex_kind = DEFAULT_EX;
unsigned error_code = 0;
lbool result = l_undef;
bool canceled = false;
std::mutex mux;
auto worker_thread = [&](int i) {
try {
lbool r = l_undef;
if (IS_AUX_SOLVER(i)) {
r = par.get_solver(i).check(num_lits, lits);
}
else if (IS_LOCAL_SEARCH(i)) {
r = ls[i-local_search_offset]->check(num_lits, lits, &par);
}
else {
r = check(num_lits, lits);
}
bool first = false;
{
std::lock_guard<std::mutex> lock(mux);
if (finished_id == -1) {
finished_id = i;
first = true;
result = r;
}
}
if (first) {
for (unsigned j = 0; j < ls.size(); ++j) {
ls[j]->rlimit().cancel();
}
for (auto& rl : lims) {
rl.cancel();
}
for (int j = 0; j < num_extra_solvers; ++j) {
if (i != j) {
par.cancel_solver(j);
}
}
if (!IS_MAIN_SOLVER(i)) {
canceled = !rlimit().inc();
if (!canceled) {
rlimit().cancel();
}
}
}
}
catch (z3_error & err) {
error_code = err.error_code();
ex_kind = ERROR_EX;
}
catch (z3_exception & ex) {
ex_msg = ex.msg();
ex_kind = DEFAULT_EX;
}
};
if (!rlimit().inc()) {
set_par(nullptr, 0);
return l_undef;
}
vector<std::thread> threads(num_threads);
for (int i = 0; i < num_threads; ++i) {
threads[i] = std::thread([&, i]() { worker_thread(i); });
}
for (auto & th : threads) {
th.join();
}
if (IS_AUX_SOLVER(finished_id)) {
m_stats = par.get_solver(finished_id).m_stats;
}
if (result == l_true && IS_AUX_SOLVER(finished_id)) {
set_model(par.get_solver(finished_id).get_model(), true);
}
else if (result == l_false && IS_AUX_SOLVER(finished_id)) {
m_core.reset();
m_core.append(par.get_solver(finished_id).get_core());
}
if (result == l_true && IS_LOCAL_SEARCH(finished_id)) {
set_model(ls[finished_id - local_search_offset]->get_model(), true);
}
if (!canceled) {
rlimit().reset_cancel();
}
set_par(nullptr, 0);
ls.reset();
uw.reset();
if (finished_id == -1) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
default: throw default_exception(std::move(ex_msg));
}
}
return result;
}
#endif
\brief import lemmas/units from parallel sat solvers.
*/
void solver::exchange_par() {
if (m_par && at_base_lvl() && m_config.m_num_threads > 1) m_par->get_clauses(*this);
if (m_par && at_base_lvl() && m_config.m_num_threads > 1) {
unsigned sz = init_trail_size();
unsigned num_in = 0, num_out = 0;
literal_vector in, out;
for (unsigned i = m_par_limit_out; i < sz; ++i) {
literal lit = m_trail[i];
if (lit.var() < m_par_num_vars) {
++num_out;
out.push_back(lit);
}
}
m_par_limit_out = sz;
m_par->exchange(*this, out, m_par_limit_in, in);
for (unsigned i = 0; !inconsistent() && i < in.size(); ++i) {
literal lit = in[i];
SASSERT(lit.var() < m_par_num_vars);
if (lvl(lit.var()) != 0 || value(lit) != l_true) {
++num_in;
assign_unit(lit);
}
}
if (num_in > 0 || num_out > 0) {
IF_VERBOSE(2, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";);
}
}
}
void solver::set_par(parallel* p, unsigned id) {
m_par = p;
m_par_num_vars = num_vars();
m_par_limit_in = 0;
m_par_limit_out = 0;
m_par_id = id;
m_par_syncing_clauses = false;
}
bool_var solver::next_var() {
bool_var next;
if (m_rand() < static_cast<int>(m_config.m_random_freq * random_gen::max_value())) {
if (num_vars() == 0)
return null_bool_var;
next = m_rand() % num_vars();
TRACE("random_split", tout << "next: " << next << " value(next): " << value(next) << "\n";);
if (value(next) == l_undef && !was_eliminated(next))
return next;
}
while (!m_case_split_queue.empty()) {
if (m_config.m_anti_exploration) {
next = m_case_split_queue.min_var();
auto age = m_stats.m_conflict - m_canceled[next];
while (age > 0) {
set_activity(next, static_cast<unsigned>(m_activity[next] * pow(0.95, static_cast<double>(age))));
m_canceled[next] = m_stats.m_conflict;
next = m_case_split_queue.min_var();
age = m_stats.m_conflict - m_canceled[next];
}
}
next = m_case_split_queue.next_var();
if (value(next) == l_undef && !was_eliminated(next))
return next;
}
return null_bool_var;
}
bool solver::decide() {
bool_var next = next_var();
if (next == null_bool_var)
return false;
push();
m_stats.m_decision++;
lbool lphase = m_ext ? m_ext->get_phase(next) : l_undef;
bool phase = lphase == l_true;
if (lphase == l_undef) {
switch (m_config.m_phase) {
case PS_ALWAYS_TRUE:
phase = true;
break;
case PS_ALWAYS_FALSE:
phase = false;
break;
case PS_BASIC_CACHING:
phase = m_phase[next];
break;
case PS_FROZEN:
phase = m_best_phase[next];
break;
case PS_SAT_CACHING:
if (m_search_state == s_unsat) {
phase = m_phase[next];
}
else {
phase = m_best_phase[next];
}
break;
case PS_RANDOM:
phase = (m_rand() % 2) == 0;
break;
default:
UNREACHABLE();
phase = false;
break;
}
}
literal next_lit(next, !phase);
TRACE("sat_decide", tout << scope_lvl() << ": next-case-split: " << next_lit << "\n";);
assign_scoped(next_lit);
return true;
}
lbool solver::bounded_search() {
flet<bool> _disable_simplify(m_simplify_enabled, false);
flet<bool> _restart_enabled(m_restart_enabled, false);
return search();
}
lbool solver::basic_search() {
lbool is_sat = l_undef;
while (is_sat == l_undef && !should_cancel()) {
if (inconsistent()) is_sat = resolve_conflict_core();
else if (should_propagate()) propagate(true);
else if (do_cleanup(false)) continue;
else if (should_gc()) do_gc();
else if (should_rephase()) do_rephase();
else if (should_restart()) { if (!m_restart_enabled) return l_undef; do_restart(!m_config.m_restart_fast); }
else if (should_simplify()) do_simplify();
else if (!decide()) is_sat = final_check();
}
return is_sat;
}
lbool solver::search() {
if (!m_ext || !m_ext->tracking_assumptions())
return basic_search();
while (true) {
pop_to_base_level();
reinit_assumptions();
lbool r = basic_search();
if (r != l_false)
return r;
if (!m_ext->should_research(m_core))
return r;
}
}
bool solver::should_propagate() const {
return !inconsistent() && m_qhead < m_trail.size();
}
lbool solver::final_check() {
if (m_ext) {
switch (m_ext->check()) {
case check_result::CR_DONE:
mk_model();
return l_true;
case check_result::CR_CONTINUE:
break;
case check_result::CR_GIVEUP:
throw abort_solver();
}
return l_undef;
}
else {
mk_model();
return l_true;
}
}
bool solver::check_inconsistent() {
if (inconsistent()) {
if (tracking_assumptions() && at_search_lvl())
resolve_conflict();
else if (m_config.m_drat && at_base_lvl())
resolve_conflict();
return true;
}
else {
return false;
}
}
void solver::init_assumptions(unsigned num_lits, literal const* lits) {
if (num_lits == 0 && m_user_scope_literals.empty()) {
return;
}
SASSERT(at_base_lvl());
reset_assumptions();
push();
propagate(false);
if (inconsistent()) {
return;
}
TRACE("sat",
tout << literal_vector(num_lits, lits) << "\n";
if (!m_user_scope_literals.empty()) {
tout << "user literals: " << m_user_scope_literals << "\n";
}
m_mc.display(tout);
);
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
literal nlit = ~m_user_scope_literals[i];
assign_scoped(nlit);
}
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
set_external(lit.var());
SASSERT(is_external(lit.var()));
add_assumption(lit);
assign_scoped(lit);
}
m_search_lvl = scope_lvl();
SASSERT(m_search_lvl == 1);
}
void solver::update_min_core() {
if (!m_min_core_valid || m_core.size() < m_min_core.size()) {
m_min_core.reset();
m_min_core.append(m_core);
m_min_core_valid = true;
}
}
void solver::reset_assumptions() {
m_assumptions.reset();
m_assumption_set.reset();
m_ext_assumption_set.reset();
}
void solver::add_assumption(literal lit) {
m_assumption_set.insert(lit);
m_assumptions.push_back(lit);
set_external(lit.var());
}
void solver::reassert_min_core() {
SASSERT(m_min_core_valid);
pop_to_base_level();
push();
reset_assumptions();
TRACE("sat", tout << "reassert: " << m_min_core << "\n";);
for (literal lit : m_min_core) {
SASSERT(is_external(lit.var()));
add_assumption(lit);
assign_scoped(lit);
}
propagate(false);
SASSERT(inconsistent());
}
void solver::reinit_assumptions() {
if (tracking_assumptions() && at_base_lvl() && !inconsistent()) {
TRACE("sat", tout << "assumptions: " << m_assumptions << " user scopes: " << m_user_scope_literals << "\n";);
if (!propagate(false)) return;
push();
for (literal lit : m_user_scope_literals) {
if (inconsistent()) break;
assign_scoped(~lit);
}
for (literal lit : m_assumptions) {
if (inconsistent()) break;
assign_scoped(lit);
}
init_ext_assumptions();
if (!inconsistent())
propagate(false);
TRACE("sat",
tout << "consistent: " << !inconsistent() << "\n";
for (literal a : m_assumptions) {
index_set s;
if (m_antecedents.find(a.var(), s)) {
tout << a << ": "; display_index_set(tout, s) << "\n";
}
}
for (literal lit : m_user_scope_literals) {
tout << "user " << lit << "\n";
}
);
}
}
void solver::init_ext_assumptions() {
if (m_ext && m_ext->tracking_assumptions()) {
m_ext_assumption_set.reset();
unsigned trail_size = m_trail.size();
if (!inconsistent())
m_ext->add_assumptions();
for (unsigned i = trail_size; i < m_trail.size(); ++i)
m_ext_assumption_set.insert(m_trail[i]);
}
}
bool solver::tracking_assumptions() const {
return !m_assumptions.empty() || !m_user_scope_literals.empty() || (m_ext && m_ext->tracking_assumptions());
}
bool solver::is_assumption(literal l) const {
return tracking_assumptions() && (m_assumption_set.contains(l) || m_ext_assumption_set.contains(l));
}
void solver::set_activity(bool_var v, unsigned new_act) {
unsigned old_act = m_activity[v];
m_activity[v] = new_act;
if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) {
m_case_split_queue.activity_changed_eh(v, new_act > old_act);
}
}
bool solver::is_assumption(bool_var v) const {
return is_assumption(literal(v, false)) || is_assumption(literal(v, true));
}
void solver::init_search() {
m_model_is_current = false;
m_phase_counter = 0;
m_search_state = s_unsat;
m_search_unsat_conflicts = m_config.m_search_unsat_conflicts;
m_search_sat_conflicts = m_config.m_search_sat_conflicts;
m_search_next_toggle = m_search_unsat_conflicts;
m_best_phase_size = 0;
m_rephase_lim = 0;
m_rephase_inc = 0;
m_reorder_lim = m_config.m_reorder_base;
m_reorder_inc = 0;
m_conflicts_since_restart = 0;
m_force_conflict_analysis = false;
m_restart_threshold = m_config.m_restart_initial;
m_luby_idx = 1;
m_gc_threshold = m_config.m_gc_initial;
m_defrag_threshold = 2;
m_restarts = 0;
m_last_position_log = 0;
m_restart_logs = 0;
m_simplifications = 0;
m_conflicts_since_init = 0;
m_next_simplify = m_config.m_simplify_delay;
m_min_d_tk = 1.0;
m_search_lvl = 0;
if (m_learned.size() <= 2*m_clauses.size())
m_conflicts_since_gc = 0;
m_restart_next_out = 0;
m_asymm_branch.init_search();
m_stopwatch.reset();
m_stopwatch.start();
m_core.reset();
m_min_core_valid = false;
m_min_core.reset();
m_simplifier.init_search();
m_mc.init_search(*this);
if (m_ext)
m_ext->init_search();
TRACE("sat", display(tout););
}
bool solver::should_simplify() const {
return m_conflicts_since_init >= m_next_simplify && m_simplify_enabled;
}
\brief Apply all simplifications.
*/
void solver::do_simplify() {
if (!should_simplify()) {
return;
}
log_stats();
m_simplifications++;
TRACE("sat", tout << "simplify\n";);
pop(scope_lvl());
struct report {
solver& s;
stopwatch m_watch;
report(solver& s):s(s) {
m_watch.start();
s.log_stats();
IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << s.m_simplifications << ")\n";);
}
~report() {
m_watch.stop();
s.log_stats();
}
};
report _rprt(*this);
SASSERT(at_base_lvl());
m_cleaner(m_config.m_force_cleanup);
CASSERT("sat_simplify_bug", check_invariant());
m_scc();
CASSERT("sat_simplify_bug", check_invariant());
if (m_ext) {
m_ext->pre_simplify();
}
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
if (!m_learned.empty()) {
m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
}
sort_watch_lits();
CASSERT("sat_simplify_bug", check_invariant());
m_probing();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
m_asymm_branch(false);
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
if (m_ext) {
m_ext->clauses_modifed();
m_ext->simplify();
}
if (m_config.m_lookahead_simplify && !m_ext) {
lookahead lh(*this);
lh.simplify(true);
lh.collect_statistics(m_aux_stats);
}
reinit_assumptions();
if (inconsistent()) return;
if (m_next_simplify == 0) {
m_next_simplify = m_config.m_next_simplify1;
}
else {
m_next_simplify = static_cast<unsigned>(m_conflicts_since_init * m_config.m_simplify_mult2);
if (m_next_simplify > m_conflicts_since_init + m_config.m_simplify_max)
m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max;
}
if (m_par) {
m_par->from_solver(*this);
if (m_par->to_solver(*this)) {
m_activity_inc = 128;
}
}
if (m_config.m_binspr && !inconsistent()) {
m_binspr();
}
if (m_config.m_anf_simplify && m_simplifications > m_config.m_anf_delay && !inconsistent()) {
anf_simplifier anf(*this);
anf_simplifier::config cfg;
cfg.m_enable_exlin = m_config.m_anf_exlin;
anf();
anf.collect_statistics(m_aux_stats);
}
if (m_cut_simplifier && m_simplifications > m_config.m_cut_delay && !inconsistent()) {
(*m_cut_simplifier)();
}
if (m_config.m_inprocess_out.is_non_empty_string()) {
std::ofstream fout(m_config.m_inprocess_out.str());
if (fout) {
display_dimacs(fout);
}
throw solver_exception("output generated");
}
}
bool solver::set_root(literal l, literal r) {
return !m_ext || m_ext->set_root(l, r);
}
void solver::flush_roots() {
if (m_ext) m_ext->flush_roots();
}
void solver::sort_watch_lits() {
for (watch_list & wlist : m_watches) {
std::stable_sort(wlist.begin(), wlist.end(), watched_lt());
}
}
void solver::set_model(model const& mdl, bool is_current) {
m_model.reset();
m_model.append(mdl);
m_model_is_current = is_current;
}
void solver::mk_model() {
m_model.reset();
m_model_is_current = true;
unsigned num = num_vars();
m_model.resize(num, l_undef);
for (bool_var v = 0; v < num; v++) {
if (!was_eliminated(v)) {
m_model[v] = value(v);
m_phase[v] = value(v) == l_true;
m_best_phase[v] = value(v) == l_true;
}
}
TRACE("sat_mc_bug", m_mc.display(tout););
#if 0
IF_VERBOSE(2, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";);
for (auto p : big::s_del_bin) {
if (value(p.first) != l_true && value(p.second) != l_true) {
IF_VERBOSE(2, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n");
}
}
#endif
if (m_clone) {
IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
if (!check_clauses(m_model)) {
throw solver_exception("check model failed");
}
}
if (m_config.m_drat) {
m_drat.check_model(m_model);
}
m_mc(m_model);
if (m_clone && !check_clauses(m_model)) {
IF_VERBOSE(1, verbose_stream() << "failure checking clauses on transformed model\n";);
IF_VERBOSE(10, m_mc.display(verbose_stream()));
IF_VERBOSE(1, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";);
throw solver_exception("check model failed");
}
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
if (m_clone) {
IF_VERBOSE(1, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
if (!m_clone->check_model(m_model)) {
IF_VERBOSE(1, m_mc.display(verbose_stream()));
IF_VERBOSE(1, display_units(verbose_stream()));
throw solver_exception("check model failed (for cloned solver)");
}
}
}
bool solver::check_clauses(model const& m) const {
bool ok = true;
for (clause const* cp : m_clauses) {
clause const & c = *cp;
if (!c.satisfied_by(m)) {
IF_VERBOSE(1, verbose_stream() << "failed clause " << c.id() << ": " << c << "\n";);
TRACE("sat", tout << "failed: " << c << "\n";
tout << "assumptions: " << m_assumptions << "\n";
tout << "trail: " << m_trail << "\n";
tout << "model: " << m << "\n";
m_mc.display(tout);
);
for (literal l : c) {
if (was_eliminated(l.var())) IF_VERBOSE(1, verbose_stream() << "eliminated: " << l << "\n";);
}
ok = false;
}
}
unsigned l_idx = 0;
for (watch_list const& wlist : m_watches) {
literal l = ~to_literal(l_idx);
if (value_at(l, m) != l_true) {
for (watched const& w : wlist) {
if (!w.is_binary_non_learned_clause())
continue;
literal l2 = w.get_literal();
if (l.index() > l2.index())
continue;
if (value_at(l2, m) != l_true) {
IF_VERBOSE(1, verbose_stream() << "failed binary: " << l << " := " << value_at(l, m) << " " << l2 << " := " << value_at(l2, m) << "\n");
IF_VERBOSE(1, verbose_stream() << "elim l1: " << was_eliminated(l.var()) << " elim l2: " << was_eliminated(l2) << "\n");
TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n"););
ok = false;
}
}
}
++l_idx;
}
for (literal l : m_assumptions) {
if (value_at(l, m) != l_true) {
VERIFY(is_external(l.var()));
IF_VERBOSE(1, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";);
TRACE("sat",
tout << l << " does not model check\n";
tout << "trail: " << m_trail << "\n";
tout << "model: " << m << "\n";
m_mc.display(tout);
);
ok = false;
}
}
if (m_ext && !m_ext->check_model(m)) {
ok = false;
}
return ok;
}
bool solver::check_model(model const & m) const {
bool ok = check_clauses(m);
if (ok && !m_mc.check_model(m)) {
ok = false;
TRACE("sat", tout << "model: " << m << "\n"; m_mc.display(tout););
IF_VERBOSE(0, verbose_stream() << "model check failed\n");
}
return ok;
}
bool solver::should_restart() const {
if (m_conflicts_since_restart <= m_restart_threshold) return false;
if (scope_lvl() < 2 + search_lvl()) return false;
if (m_config.m_restart != RS_EMA) return true;
return
m_fast_glue_avg + search_lvl() <= scope_lvl() &&
m_config.m_restart_margin * m_slow_glue_avg <= m_fast_glue_avg;
}
void solver::log_stats() {
m_restart_logs++;
std::stringstream strm;
strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " "
<< std::setw(6) << m_stats.m_decision << " "
<< std::setw(4) << m_stats.m_restart
<< mk_stat(*this)
<< " " << std::setw(6) << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";
std::string str(strm.str());
svector<size_t> nums;
for (size_t i = 0; i < str.size(); ++i) {
while (i < str.size() && str[i] != ' ') ++i;
while (i < str.size() && str[i] == ' ') ++i;
if (i < str.size()) {
nums.push_back(i);
}
}
bool same = m_last_positions.size() == nums.size();
size_t diff = 0;
for (unsigned i = 0; i < nums.size() && same; ++i) {
if (m_last_positions[i] > nums[i]) diff += m_last_positions[i] - nums[i];
if (m_last_positions[i] < nums[i]) diff += nums[i] - m_last_positions[i];
}
if (m_last_positions.empty() ||
m_restart_logs >= 20 + m_last_position_log ||
(m_restart_logs >= 6 + m_last_position_log && (!same || diff > 3))) {
m_last_position_log = m_restart_logs;
int adjust[9] = { -3, -3, -3, -1, -3, -2, -1, -2, -1 };
char const* tag[9] = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" };
std::stringstream l1, l2;
l1 << "(sat.stats ";
l2 << "(sat.stats ";
size_t p1 = 11, p2 = 11;
SASSERT(nums.size() == 9);
for (unsigned i = 0; i < 9 && i < nums.size(); ++i) {
size_t p = nums[i];
if (i & 0x1) {
for (; p2 < p + adjust[i]; ++p2) l2 << " ";
p2 += strlen(tag[i]);
l2 << tag[i];
}
else {
for (; p1 < p + adjust[i]; ++p1) l1 << " ";
p1 += strlen(tag[i]);
l1 << tag[i];
}
}
for (; p1 + 2 < str.size(); ++p1) l1 << " ";
for (; p2 + 2 < str.size(); ++p2) l2 << " ";
l1 << ")\n";
l2 << ")\n";
IF_VERBOSE(1, verbose_stream() << l1.str() << l2.str());
m_last_positions.reset();
m_last_positions.append(nums);
}
IF_VERBOSE(1, verbose_stream() << str);
}
void solver::do_restart(bool to_base) {
m_stats.m_restart++;
m_restarts++;
if (m_conflicts_since_init >= m_restart_next_out && get_verbosity_level() >= 1) {
if (0 == m_restart_next_out) {
m_restart_next_out = 1;
}
else {
m_restart_next_out = std::min(m_conflicts_since_init + 50000, (3*m_restart_next_out)/2 + 1);
}
log_stats();
}
TRACE("sat", tout << "restart " << restart_level(to_base) << "\n";);
IF_VERBOSE(30, display_status(verbose_stream()););
TRACE("sat", tout << "restart " << restart_level(to_base) << "\n";);
pop_reinit(restart_level(to_base));
set_next_restart();
}
unsigned solver::restart_level(bool to_base) {
if (to_base || scope_lvl() == search_lvl()) {
return scope_lvl() - search_lvl();
}
else {
bool_var next = m_case_split_queue.min_var();
#if 0
unsigned n = 0;
do {
bool_var prev = scope_literal(scope_lvl() - n - 1).var();
if (m_case_split_queue.more_active(prev, next)) break;
++n;
}
while (n < scope_lvl() - search_lvl());
return n;
#endif
unsigned n = search_lvl();
for (; n < scope_lvl() && m_case_split_queue.more_active(scope_literal(n).var(), next); ++n) {
}
return n - search_lvl();
}
}
void solver::update_activity(bool_var v, double p) {
unsigned new_act = (unsigned) (num_vars() * m_config.m_activity_scale * p);
set_activity(v, new_act);
}
void solver::set_next_restart() {
m_conflicts_since_restart = 0;
switch (m_config.m_restart) {
case RS_GEOMETRIC:
m_restart_threshold = static_cast<unsigned>(m_restart_threshold * m_config.m_restart_factor);
break;
case RS_LUBY:
m_luby_idx++;
m_restart_threshold = m_config.m_restart_initial * get_luby(m_luby_idx);
break;
case RS_EMA:
m_restart_threshold = m_config.m_restart_initial;
break;
case RS_STATIC:
break;
default:
UNREACHABLE();
break;
}
CASSERT("sat_restart", check_invariant());
}
bool solver::resolve_conflict() {
while (true) {
lbool r = resolve_conflict_core();
CASSERT("sat_check_marks", check_marks());
if (r == l_false)
return false;
if (!inconsistent())
return true;
}
}
lbool solver::resolve_conflict_core() {
m_conflicts_since_init++;
m_conflicts_since_restart++;
m_conflicts_since_gc++;
m_stats.m_conflict++;
if (m_step_size > m_config.m_step_size_min) {
m_step_size -= m_config.m_step_size_dec;
}
bool unique_max;
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);
justification js = m_conflict;
if (m_conflict_lvl <= 1 && tracking_assumptions()) {
TRACE("sat", tout << "unsat core\n";);
resolve_conflict_for_unsat_core();
return l_false;
}
if (m_conflict_lvl == 0) {
drat_explain_conflict();
if (m_config.m_drat)
drat_log_clause(0, nullptr, sat::status::redundant());
TRACE("sat", tout << "conflict level is 0\n";);
return l_false;
}
if (allow_backtracking() && unique_max && !m_force_conflict_analysis) {
TRACE("sat", tout << "unique max " << js << " " << m_not_l << "\n";);
pop_reinit(m_scope_lvl - m_conflict_lvl + 1);
m_force_conflict_analysis = true;
++m_stats.m_backtracks;
return l_undef;
}
m_force_conflict_analysis = false;
updt_phase_of_vars();
if (m_ext) {
switch (m_ext->resolve_conflict()) {
case l_true:
learn_lemma_and_backjump();
return l_undef;
case l_undef:
break;
case l_false:
return l_undef;
}
}
m_lemma.reset();
unsigned idx = skip_literals_above_conflict_level();
m_lemma.push_back(null_literal);
TRACE("sat_conflict_detail",
tout << "resolve: " << m_not_l << " "
<< " js: " << js
<< " idx: " << idx
<< " trail: " << m_trail.size()
<< " @" << m_conflict_lvl << "\n";);
unsigned num_marks = 0;
literal consequent = null_literal;
if (m_not_l != null_literal) {
TRACE("sat_conflict_detail", tout << "not_l: " << m_not_l << "\n";);
process_antecedent(m_not_l, num_marks);
consequent = ~m_not_l;
}
do {
TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << " @" << (consequent==null_literal?m_conflict_lvl:lvl(consequent)) << "\n";
tout << "num_marks: " << num_marks << "\n";
display_justification(tout, js) << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
process_antecedent(~(js.get_literal()), num_marks);
break;
case justification::TERNARY:
process_antecedent(~(js.get_literal1()), num_marks);
process_antecedent(~(js.get_literal2()), num_marks);
break;
case justification::CLAUSE: {
clause & c = get_clause(js);
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
if (c[0] == consequent) {
i = 1;
}
else {
process_antecedent(~c[0], num_marks);
i = 2;
}
}
unsigned sz = c.size();
for (; i < sz; i++)
process_antecedent(~c[i], num_marks);
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js, false);
TRACE("sat", tout << "ext antecedents: " << m_ext_antecedents << "\n";);
for (literal l : m_ext_antecedents)
process_antecedent(l, num_marks);
#if 0
if (m_ext_antecedents.size() <= 1) {
for (literal& l : m_ext_antecedents)
l.neg();
m_ext_antecedents.push_back(consequent);
mk_clause(m_ext_antecedents.size(), m_ext_antecedents.c_ptr(), sat::status::redundant());
}
#endif
break;
}
default:
UNREACHABLE();
break;
}
bool_var c_var;
while (true) {
consequent = m_trail[idx];
c_var = consequent.var();
if (is_marked(c_var)) {
if (lvl(c_var) == m_conflict_lvl) {
break;
}
SASSERT(lvl(c_var) < m_conflict_lvl);
}
CTRACE("sat", idx == 0,
for (literal lit : m_trail)
if (is_marked(lit.var()))
tout << "missed " << lit << "@" << lvl(lit) << "\n";);
CTRACE("sat", idx == 0, display(tout););
if (idx == 0)
IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflict << "\n");
VERIFY(idx > 0);
idx--;
}
SASSERT(lvl(consequent) == m_conflict_lvl);
js = m_justification[c_var];
idx--;
num_marks--;
reset_mark(c_var);
TRACE("sat", display_justification(tout << consequent << " ", js) << "\n";);
}
while (num_marks > 0);
m_lemma[0] = ~consequent;
learn_lemma_and_backjump();
return l_undef;
}
void solver::learn_lemma_and_backjump() {
TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
if (m_lemma.empty()) {
pop_reinit(m_scope_lvl);
mk_clause_core(0, nullptr, sat::status::redundant());
return;
}
if (m_config.m_minimize_lemmas) {
minimize_lemma();
reset_lemma_var_marks();
if (m_config.m_dyn_sub_res)
dyn_sub_res();
TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
}
else {
reset_lemma_var_marks();
}
unsigned backtrack_lvl = lvl(m_lemma[0]);
unsigned backjump_lvl = 0;
for (unsigned i = m_lemma.size(); i-- > 1;) {
unsigned level = lvl(m_lemma[i]);
backjump_lvl = std::max(level, backjump_lvl);
}
if (backtrack_lvl < backjump_lvl) {
backtrack_lvl = backjump_lvl;
for (unsigned i = m_lemma.size(); i-- > 1;) {
if (lvl(m_lemma[i]) == backjump_lvl) {
TRACE("sat", tout << "swap " << m_lemma[0] << "@" << lvl(m_lemma[0]) << m_lemma[1] << "@" << backjump_lvl << "\n";);
std::swap(m_lemma[i], m_lemma[0]);
break;
}
}
}
unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.data());
m_fast_glue_avg.update(glue);
m_slow_glue_avg.update(glue);
unsigned num_scopes = m_scope_lvl - backjump_lvl;
if (use_backjumping(num_scopes)) {
++m_stats.m_backjumps;
pop_reinit(num_scopes);
}
else {
TRACE("sat", tout << "backtrack " << (m_scope_lvl - backtrack_lvl + 1) << " scopes\n";);
++m_stats.m_backtracks;
pop_reinit(m_scope_lvl - backtrack_lvl + 1);
}
clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.data(), sat::status::redundant());
if (lemma) {
lemma->set_glue(glue);
}
if (m_par && lemma) {
m_par->share_clause(*this, *lemma);
}
m_lemma.reset();
TRACE("sat_conflict_detail", tout << "consistent " << (!m_inconsistent) << " scopes: " << scope_lvl() << " backtrack: " << backtrack_lvl << " backjump: " << backjump_lvl << "\n";);
decay_activity();
updt_phase_counters();
}
bool solver::use_backjumping(unsigned num_scopes) const {
return
num_scopes > 0 &&
(num_scopes <= m_config.m_backtrack_scopes || !allow_backtracking());
}
bool solver::allow_backtracking() const {
return m_conflicts_since_init > m_config.m_backtrack_init_conflicts;
}
void solver::process_antecedent_for_unsat_core(literal antecedent) {
bool_var var = antecedent.var();
SASSERT(var < num_vars());
TRACE("sat", tout << antecedent << " " << (is_marked(var)?"+":"-") << "\n";);
if (!is_marked(var)) {
mark(var);
m_unmark.push_back(var);
if (is_assumption(antecedent)) {
m_core.push_back(antecedent);
}
}
}
void solver::process_consequent_for_unsat_core(literal consequent, justification const& js) {
TRACE("sat", tout << "processing consequent: ";
if (consequent == null_literal) tout << "null\n";
else tout << consequent << "\n";
display_justification(tout << "js kind: ", js) << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
SASSERT(consequent != null_literal);
process_antecedent_for_unsat_core(~(js.get_literal()));
break;
case justification::TERNARY:
SASSERT(consequent != null_literal);
process_antecedent_for_unsat_core(~(js.get_literal1()));
process_antecedent_for_unsat_core(~(js.get_literal2()));
break;
case justification::CLAUSE: {
clause & c = get_clause(js);
unsigned i = 0;
if (consequent != null_literal) {
SASSERT(c[0] == consequent || c[1] == consequent);
if (c[0] == consequent) {
i = 1;
}
else {
process_antecedent_for_unsat_core(~c[0]);
i = 2;
}
}
unsigned sz = c.size();
for (; i < sz; i++)
process_antecedent_for_unsat_core(~c[i]);
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js, false);
for (literal l : m_ext_antecedents) {
process_antecedent_for_unsat_core(l);
}
break;
}
default:
UNREACHABLE();
break;
}
}
void solver::resolve_conflict_for_unsat_core() {
TRACE("sat_verbose", display(tout);
unsigned level = 0;
for (literal l : m_trail) {
if (level != lvl(l)) {
level = lvl(l);
tout << level << ": ";
}
tout << l;
if (m_mark[l.var()]) {
tout << "*";
}
tout << " ";
}
tout << "\n";
tout << "conflict level: " << m_conflict_lvl << "\n";
);
m_core.reset();
if (!m_config.m_drat && m_conflict_lvl == 0) {
return;
}
SASSERT(m_unmark.empty());
DEBUG_CODE({
for (literal lit : m_trail) {
SASSERT(!is_marked(lit.var()));
}});
unsigned old_size = m_unmark.size();
int idx = skip_literals_above_conflict_level();
literal consequent = m_not_l;
if (m_not_l != null_literal) {
justification js = m_justification[m_not_l.var()];
TRACE("sat", tout << "not_l: " << m_not_l << "\n";
display_justification(tout, js) << "\n";);
process_antecedent_for_unsat_core(m_not_l);
if (is_assumption(~m_not_l)) {
m_core.push_back(~m_not_l);
}
else {
process_consequent_for_unsat_core(m_not_l, js);
}
consequent = ~m_not_l;
}
justification js = m_conflict;
int init_sz = init_trail_size();
while (true) {
process_consequent_for_unsat_core(consequent, js);
while (idx >= init_sz) {
consequent = m_trail[idx];
if (is_marked(consequent.var()) && lvl(consequent) == m_conflict_lvl)
break;
idx--;
}
if (idx < init_sz) {
break;
}
SASSERT(lvl(consequent) == m_conflict_lvl);
js = m_justification[consequent.var()];
idx--;
}
reset_unmark(old_size);
if (m_core.size() > 1) {
unsigned j = 0;
for (unsigned i = 0; i < m_core.size(); ++i) {
if (lvl(m_core[i]) > 0) m_core[j++] = m_core[i];
}
m_core.shrink(j);
}
if (m_config.m_core_minimize) {
if (m_min_core_valid && m_min_core.size() < m_core.size()) {
IF_VERBOSE(2, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";);
m_core.reset();
m_core.append(m_min_core);
}
m_mus();
set_model(m_mus.get_model(), !m_mus.get_model().empty());
IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
}
}
unsigned solver::get_max_lvl(literal not_l, justification js, bool& unique_max) {
unique_max = true;
unsigned level = 0;
if (not_l != null_literal) {
level = lvl(not_l);
}
switch (js.get_kind()) {
case justification::NONE:
level = std::max(level, js.level());
return level;
case justification::BINARY:
level = update_max_level(js.get_literal(), level, unique_max);
return level;
case justification::TERNARY:
level = update_max_level(js.get_literal1(), level, unique_max);
level = update_max_level(js.get_literal2(), level, unique_max);
return level;
case justification::CLAUSE:
for (literal l : get_clause(js))
level = update_max_level(l, level, unique_max);
return level;
case justification::EXT_JUSTIFICATION:
if (not_l != null_literal)
not_l.neg();
fill_ext_antecedents(not_l, js, true);
for (literal l : m_ext_antecedents)
level = update_max_level(l, level, unique_max);
return level;
default:
UNREACHABLE();
return 0;
}
}
\brief Skip literals from levels above m_conflict_lvl.
It returns an index idx such that lvl(m_trail[idx]) <= m_conflict_lvl, and
for all idx' > idx, lvl(m_trail[idx']) > m_conflict_lvl
*/
unsigned solver::skip_literals_above_conflict_level() {
unsigned idx = m_trail.size();
if (idx == 0) {
return idx;
}
idx--;
while (lvl(m_trail[idx]) > m_conflict_lvl) {
SASSERT(idx > 0);
idx--;
}
return idx;
}
void solver::process_antecedent(literal antecedent, unsigned & num_marks) {
bool_var var = antecedent.var();
unsigned var_lvl = lvl(var);
SASSERT(var < num_vars());
TRACE("sat_verbose", tout << "process " << var << "@" << var_lvl << " marked " << is_marked(var) << " conflict " << m_conflict_lvl << "\n";);
if (!is_marked(var) && var_lvl > 0) {
mark(var);
switch (m_config.m_branching_heuristic) {
case BH_VSIDS:
inc_activity(var);
break;
case BH_CHB:
m_last_conflict[var] = m_stats.m_conflict;
break;
default:
break;
}
if (var_lvl == m_conflict_lvl)
num_marks++;
else
m_lemma.push_back(~antecedent);
}
}
\brief js is an external justification. Collect its antecedents and store at m_ext_antecedents.
*/
void solver::fill_ext_antecedents(literal consequent, justification js, bool probing) {
SASSERT(js.is_ext_justification());
SASSERT(m_ext);
auto idx = js.get_ext_justification_idx();
m_ext_antecedents.reset();
m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing);
}
bool solver::is_two_phase() const {
return m_config.m_phase == PS_SAT_CACHING;
}
bool solver::is_sat_phase() const {
return is_two_phase() && m_search_state == s_sat;
}
void solver::updt_phase_of_vars() {
if (m_config.m_phase == PS_FROZEN)
return;
unsigned from_lvl = m_conflict_lvl;
unsigned head = from_lvl == 0 ? 0 : m_scopes[from_lvl - 1].m_trail_lim;
unsigned sz = m_trail.size();
for (unsigned i = head; i < sz; i++) {
bool_var v = m_trail[i].var();
TRACE("forget_phase", tout << "forgetting phase of v" << v << "\n";);
m_phase[v] = m_rand() % 2 == 0;
}
if (is_sat_phase() && head >= m_best_phase_size) {
m_best_phase_size = head;
IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n");
for (unsigned i = 0; i < head; ++i) {
bool_var v = m_trail[i].var();
m_best_phase[v] = m_phase[v];
}
}
}
bool solver::should_toggle_search_state() {
if (m_search_state == s_unsat) {
m_trail_avg.update(m_trail.size());
}
return
(m_phase_counter >= m_search_next_toggle) &&
(m_search_state == s_sat || m_trail.size() > 0.50*m_trail_avg);
}
void solver::do_toggle_search_state() {
if (is_two_phase()) {
m_best_phase_size = 0;
std::swap(m_fast_glue_backup, m_fast_glue_avg);
std::swap(m_slow_glue_backup, m_slow_glue_avg);
if (m_search_state == s_sat) {
m_search_unsat_conflicts += m_config.m_search_unsat_conflicts;
}
else {
m_search_sat_conflicts += m_config.m_search_sat_conflicts;
}
}
if (m_search_state == s_unsat) {
m_search_state = s_sat;
m_search_next_toggle = m_search_sat_conflicts;
}
else {
m_search_state = s_unsat;
m_search_next_toggle = m_search_unsat_conflicts;
}
m_phase_counter = 0;
}
bool solver::should_rephase() {
return m_conflicts_since_init > m_rephase_lim;
}
void solver::do_rephase() {
switch (m_config.m_phase) {
case PS_ALWAYS_TRUE:
for (auto& p : m_phase) p = true;
break;
case PS_ALWAYS_FALSE:
for (auto& p : m_phase) p = false;
break;
case PS_FROZEN:
break;
case PS_BASIC_CACHING:
switch (m_rephase_lim % 4) {
case 0:
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
break;
case 1:
for (auto& p : m_phase) p = false;
break;
case 2:
for (auto& p : m_phase) p = !p;
break;
default:
break;
}
break;
case PS_SAT_CACHING:
if (m_search_state == s_sat) {
for (unsigned i = 0; i < m_phase.size(); ++i) {
m_phase[i] = m_best_phase[i];
}
}
break;
case PS_RANDOM:
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
break;
default:
UNREACHABLE();
break;
}
m_rephase_inc += m_config.m_rephase_base;
m_rephase_lim += m_rephase_inc;
}
bool solver::should_reorder() {
return m_conflicts_since_init > m_reorder_lim;
}
void solver::do_reorder() {
IF_VERBOSE(1, verbose_stream() << "(reorder)\n");
m_activity_inc = 128;
svector<bool_var> vars;
for (bool_var v = num_vars(); v-- > 0; ) {
if (!was_eliminated(v) && value(v) == l_undef) {
vars.push_back(v);
}
}
#if 1
svector<double> logits(vars.size(), 0.0);
double itau = m_config.m_reorder_itau;
double lse = 0;
double mid = m_rand.max_value()/2;
double max = 0;
for (double& f : logits) {
f = itau * (m_rand() - mid)/mid;
if (f > max) max = f;
}
for (double f : logits) {
lse += log(f - max);
}
lse = max + exp(lse);
for (unsigned i = 0; i < vars.size(); ++i) {
update_activity(vars[i], exp(logits[i] - lse));
}
#else
shuffle(vars.size(), vars.c_ptr(), m_rand);
for (bool_var v : vars) {
update_activity(v, m_rand(10)/10.0);
}
#endif
m_reorder_inc += m_config.m_reorder_base;
m_reorder_lim += m_reorder_inc;
}
void solver::updt_phase_counters() {
m_phase_counter++;
if (should_toggle_search_state()) {
do_toggle_search_state();
}
}
\brief Return the number of different levels in lits.
All literals in lits must be assigned.
*/
unsigned solver::num_diff_levels(unsigned num, literal const * lits) {
m_diff_levels.reserve(scope_lvl() + 1, false);
unsigned r = 0;
for (unsigned i = 0; i < num; i++) {
SASSERT(value(lits[i]) != l_undef);
unsigned lit_lvl = lvl(lits[i]);
if (!m_diff_levels[lit_lvl]) {
m_diff_levels[lit_lvl] = true;
r++;
}
}
for (unsigned i = 0; i < num; i++)
m_diff_levels[lvl(lits[i])] = false;
return r;
}
bool solver::num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue) {
m_diff_levels.reserve(scope_lvl() + 1, false);
glue = 0;
unsigned i = 0;
for (; i < num && glue < max_glue; i++) {
SASSERT(value(lits[i]) != l_undef);
unsigned lit_lvl = lvl(lits[i]);
if (!m_diff_levels[lit_lvl]) {
m_diff_levels[lit_lvl] = true;
glue++;
}
}
for (; i-- > 0; )
m_diff_levels[lvl(lits[i])] = false;
return glue < max_glue;
}
bool solver::num_diff_false_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue) {
m_diff_levels.reserve(scope_lvl() + 1, false);
glue = 0;
unsigned i = 0;
for (; i < num && glue < max_glue; i++) {
if (value(lits[i]) == l_false) {
unsigned lit_lvl = lvl(lits[i]);
if (!m_diff_levels[lit_lvl]) {
m_diff_levels[lit_lvl] = true;
glue++;
}
}
}
for (; i-- > 0;) {
literal lit = lits[i];
if (value(lit) == l_false) {
VERIFY(lvl(lit) < m_diff_levels.size());
m_diff_levels[lvl(lit)] = false;
}
}
return glue < max_glue;
}
\brief Process an antecedent for lemma minimization.
*/
bool solver::process_antecedent_for_minimization(literal antecedent) {
bool_var var = antecedent.var();
unsigned var_lvl = lvl(var);
if (!is_marked(var) && var_lvl > 0) {
if (m_lvl_set.may_contain(var_lvl)) {
mark(var);
m_unmark.push_back(var);
m_lemma_min_stack.push_back(antecedent);
}
else {
return false;
}
}
return true;
}
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
The idea is to stop the recursive search with a failure
as soon as we find a literal assigned in a level that is not in lvl_set.
*/
bool solver::implied_by_marked(literal lit) {
m_lemma_min_stack.reset();
m_lemma_min_stack.push_back(lit);
unsigned old_size = m_unmark.size();
while (!m_lemma_min_stack.empty()) {
lit = m_lemma_min_stack.back();
bool_var var = lit.var();
m_lemma_min_stack.pop_back();
justification const& js = m_justification[var];
switch(js.get_kind()) {
case justification::NONE:
if (lvl(var) > 0) {
reset_unmark(old_size);
return false;
}
break;
case justification::BINARY:
if (!process_antecedent_for_minimization(~(js.get_literal()))) {
reset_unmark(old_size);
return false;
}
break;
case justification::TERNARY:
if (!process_antecedent_for_minimization(~(js.get_literal1())) ||
!process_antecedent_for_minimization(~(js.get_literal2()))) {
reset_unmark(old_size);
return false;
}
break;
case justification::CLAUSE: {
clause & c = get_clause(js);
unsigned i = 0;
if (c[0].var() == var) {
i = 1;
}
else {
SASSERT(c[1].var() == var);
if (!process_antecedent_for_minimization(~c[0])) {
reset_unmark(old_size);
return false;
}
i = 2;
}
unsigned sz = c.size();
for (; i < sz; i++) {
if (!process_antecedent_for_minimization(~c[i])) {
reset_unmark(old_size);
return false;
}
}
break;
}
case justification::EXT_JUSTIFICATION: {
literal consequent(var, value(var) == l_false);
fill_ext_antecedents(consequent, js, false);
for (literal l : m_ext_antecedents) {
if (!process_antecedent_for_minimization(l)) {
reset_unmark(old_size);
return false;
}
}
break;
}
default:
UNREACHABLE();
break;
}
TRACE("sat_conflict",
display_justification(tout << var << " ",js) << "\n";);
}
return true;
}
\brief Restore the size of m_unmark to old_size, and
unmark variables at positions [old_size, m_unmark.size()).
*/
void solver::reset_unmark(unsigned old_size) {
unsigned curr_size = m_unmark.size();
for(unsigned i = old_size; i < curr_size; i++)
reset_mark(m_unmark[i]);
m_unmark.shrink(old_size);
}
\brief Store the levels of the literals at m_lemma in the
approximated set m_lvl_set.
*/
void solver::updt_lemma_lvl_set() {
m_lvl_set.reset();
for (literal l : m_lemma)
m_lvl_set.insert(lvl(l));
}
\brief Minimize lemma using binary resolution
*/
bool solver::minimize_lemma_binres() {
SASSERT(!m_lemma.empty());
SASSERT(m_unmark.empty());
unsigned sz = m_lemma.size();
unsigned num_reduced = 0;
for (unsigned i = 1; i < sz; ++i) {
mark_lit(m_lemma[i]);
}
watch_list const& wlist = get_wlist(m_lemma[0]);
for (watched const& w : wlist) {
if (w.is_binary_clause() && is_marked_lit(w.get_literal())) {
unmark_lit(~w.get_literal());
num_reduced++;
}
}
if (num_reduced > 0) {
unsigned j = 1;
for (unsigned i = 1; i < sz; ++i) {
if (is_marked_lit(m_lemma[i])) {
m_lemma[j++] = m_lemma[i];
unmark_lit(m_lemma[i]);
}
}
m_lemma.shrink(j);
}
return num_reduced > 0;
}
\brief Minimize the number of literals in m_lemma. The main idea is to remove
literals that are implied by other literals in m_lemma and/or literals
assigned at level 0.
*/
bool solver::minimize_lemma() {
SASSERT(!m_lemma.empty());
SASSERT(m_unmark.empty());
updt_lemma_lvl_set();
unsigned sz = m_lemma.size();
unsigned i = 1;
unsigned j = 1;
for (; i < sz; i++) {
literal l = m_lemma[i];
if (implied_by_marked(l)) {
m_unmark.push_back(l.var());
}
else {
m_lemma[j++] = m_lemma[i];
}
}
reset_unmark(0);
m_lemma.shrink(j);
m_stats.m_minimized_lits += sz - j;
return j < sz;
}
\brief Reset the mark of the variables in the current lemma.
*/
void solver::reset_lemma_var_marks() {
if (m_config.m_branching_heuristic == BH_VSIDS) {
update_lrb_reasoned();
}
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
SASSERT(!is_marked((*it).var()));
++it;
for(; it != end; ++it) {
bool_var var = (*it).var();
reset_mark(var);
}
}
void solver::update_lrb_reasoned() {
unsigned sz = m_lemma.size();
SASSERT(!is_marked(m_lemma[0].var()));
mark(m_lemma[0].var());
for (unsigned i = m_lemma.size(); i-- > 0; ) {
justification js = m_justification[m_lemma[i].var()];
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
update_lrb_reasoned(js.get_literal());
break;
case justification::TERNARY:
update_lrb_reasoned(js.get_literal1());
update_lrb_reasoned(js.get_literal2());
break;
case justification::CLAUSE: {
clause & c = get_clause(js);
for (literal l : c) {
update_lrb_reasoned(l);
}
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(~m_lemma[i], js, true);
for (literal l : m_ext_antecedents) {
update_lrb_reasoned(l);
}
break;
}
}
}
reset_mark(m_lemma[0].var());
for (unsigned i = m_lemma.size(); i-- > sz; ) {
reset_mark(m_lemma[i].var());
}
m_lemma.shrink(sz);
}
void solver::update_lrb_reasoned(literal lit) {
bool_var v = lit.var();
if (!is_marked(v)) {
mark(v);
m_reasoned[v]++;
inc_activity(v);
m_lemma.push_back(lit);
}
}
\brief Apply dynamic subsumption resolution to new lemma.
Only binary and ternary clauses are used.
*/
bool solver::dyn_sub_res() {
unsigned sz = m_lemma.size();
for (unsigned i = 0; i < sz; i++) {
mark_lit(m_lemma[i]);
}
literal l0 = m_lemma[0];
for (unsigned i = 0; i < sz; i++) {
literal l = m_lemma[i];
if (!is_marked_lit(l))
continue;
watch_list const & wlist = get_wlist(~l);
for (watched const& w : wlist) {
if (w.is_binary_clause()) {
literal l2 = w.get_literal();
if (is_marked_lit(~l2) && l0 != ~l2) {
unmark_lit(~l2);
}
}
else if (w.is_ternary_clause()) {
literal l2 = w.get_literal1();
literal l3 = w.get_literal2();
if (is_marked_lit(l2) && is_marked_lit(~l3) && l0 != ~l3) {
unmark_lit(~l3);
}
else if (is_marked_lit(~l2) && is_marked_lit(l3) && l0 != ~l2) {
unmark_lit(~l2);
}
}
else {
break;
}
}
literal_vector * implied_lits = m_probing.cached_implied_lits(~l);
if (implied_lits) {
for (literal l2 : *implied_lits) {
if (is_marked_lit(~l2) && l0 != ~l2) {
unmark_lit(~l2);
}
}
}
}
SASSERT(is_marked_lit(m_lemma[0]));
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
literal l = m_lemma[i];
if (is_marked_lit(l)) {
unmark_lit(l);
m_lemma[j] = l;
j++;
}
}
m_stats.m_dyn_sub_res += sz - j;
SASSERT(j >= 1);
m_lemma.shrink(j);
return j < sz;
}
void solver::push() {
SASSERT(!inconsistent());
TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";);
SASSERT(m_qhead == m_trail.size());
m_scopes.push_back(scope());
scope & s = m_scopes.back();
m_scope_lvl++;
s.m_trail_lim = m_trail.size();
s.m_clauses_to_reinit_lim = m_clauses_to_reinit.size();
s.m_inconsistent = m_inconsistent;
if (m_ext) {
m_vars_lim.push(m_active_vars.size());
m_ext->push();
}
}
void solver::pop_reinit(unsigned num_scopes) {
pop(num_scopes);
exchange_par();
reinit_assumptions();
m_stats.m_units = init_trail_size();
}
void solver::pop_vars(unsigned num_scopes) {
m_vars_to_reinit.reset();
unsigned old_num_vars = m_vars_lim.pop(num_scopes);
if (old_num_vars == m_active_vars.size())
return;
unsigned free_vars_head = m_free_vars.size();
unsigned sz = m_active_vars.size(), j = old_num_vars;
unsigned new_lvl = m_scopes.size() - num_scopes;
gc_reinit_stack(num_scopes);
init_visited();
unsigned old_sz = m_scopes[new_lvl].m_clauses_to_reinit_lim;
for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) {
clause_wrapper const& cw = m_clauses_to_reinit[i];
for (unsigned j = cw.size(); j-- > 0; )
mark_visited(cw[j].var());
}
for (literal lit : m_lemma)
mark_visited(lit.var());
auto is_active = [&](bool_var v) {
return value(v) != l_undef && lvl(v) <= new_lvl;
};
for (unsigned i = old_num_vars; i < sz; ++i) {
bool_var v = m_active_vars[i];
if (is_visited(v) || is_active(v)) {
m_vars_to_reinit.push_back(v);
m_active_vars[j++] = v;
m_var_scope[v] = new_lvl;
}
else {
set_eliminated(v, true);
if (!is_external(v) || true) {
m_free_vars.push_back(v);
}
}
}
m_active_vars.shrink(j);
auto cleanup_watch = [&](literal lit) {
for (auto const& w : get_wlist(lit)) {
IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
}
};
for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) {
bool_var v = m_free_vars[i];
cleanup_watch(literal(v, false));
cleanup_watch(literal(v, true));
}
TRACE("sat",
tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n";
tout << "new level: " << new_lvl << "\n";
tout << "vars to reinit: " << m_vars_to_reinit << "\n";
tout << "free vars: " << bool_var_vector(m_free_vars.size() - free_vars_head, m_free_vars.data() + free_vars_head) << "\n";
for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; )
tout << "reinit: " << m_clauses_to_reinit[i] << "\n";
display(tout););
}
void solver::shrink_vars(unsigned v) {
unsigned j = 0;
for (bool_var w : m_free_vars)
if (w < v)
m_free_vars[j++] = w;
m_free_vars.shrink(j);
for (bool_var w = m_justification.size(); w-- > v;) {
m_case_split_queue.del_var_eh(w);
m_probing.reset_cache(literal(w, true));
m_probing.reset_cache(literal(w, false));
}
m_watches.shrink(2*v);
m_assignment.shrink(2*v);
m_justification.shrink(v);
m_decision.shrink(v);
m_eliminated.shrink(v);
m_external.shrink(v);
m_var_scope.shrink(v);
m_touched.shrink(v);
m_activity.shrink(v);
m_mark.shrink(v);
m_lit_mark.shrink(2*v);
m_phase.shrink(v);
m_best_phase.shrink(v);
m_prev_phase.shrink(v);
m_assigned_since_gc.shrink(v);
m_simplifier.reset_todos();
}
void solver::pop(unsigned num_scopes) {
if (num_scopes == 0)
return;
unsigned free_vars_head = m_free_vars.size();
if (m_ext) {
pop_vars(num_scopes);
m_ext->pop(num_scopes);
}
SASSERT(num_scopes <= scope_lvl());
unsigned new_lvl = scope_lvl() - num_scopes;
scope & s = m_scopes[new_lvl];
m_inconsistent = false;
unassign_vars(s.m_trail_lim, new_lvl);
for (unsigned i = m_free_vars.size(); i-- > free_vars_head; )
m_case_split_queue.del_var_eh(m_free_vars[i]);
m_scope_lvl -= num_scopes;
reinit_clauses(s.m_clauses_to_reinit_lim);
m_scopes.shrink(new_lvl);
if (m_ext)
m_ext->pop_reinit();
}
void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) {
SASSERT(old_sz <= m_trail.size());
SASSERT(m_replay_assign.empty());
for (unsigned i = m_trail.size(); i-- > old_sz; ) {
literal l = m_trail[i];
bool_var v = l.var();
if (lvl(v) <= new_lvl) {
m_replay_assign.push_back(l);
continue;
}
m_assignment[l.index()] = l_undef;
m_assignment[(~l).index()] = l_undef;
SASSERT(value(v) == l_undef);
m_case_split_queue.unassign_var_eh(v);
if (m_config.m_anti_exploration) {
m_canceled[v] = m_stats.m_conflict;
}
}
m_trail.shrink(old_sz);
m_qhead = m_trail.size();
if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
CTRACE("sat", !m_replay_assign.empty(), tout << "replay-assign: " << m_replay_assign << "\n";);
for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
literal lit = m_replay_assign[i];
m_trail.push_back(lit);
}
m_replay_assign.reset();
}
void solver::reinit_clauses(unsigned old_sz) {
unsigned sz = m_clauses_to_reinit.size();
SASSERT(old_sz <= sz);
unsigned j = old_sz;
for (unsigned i = old_sz; i < sz; i++) {
clause_wrapper cw = m_clauses_to_reinit[i];
bool reinit = false;
if (cw.is_binary()) {
if (propagate_bin_clause(cw[0], cw[1]) && !at_base_lvl())
m_clauses_to_reinit[j++] = cw;
else if (has_variables_to_reinit(cw[0], cw[1]))
m_clauses_to_reinit[j++] = cw;
}
else {
clause & c = *(cw.get_clause());
if (ENABLE_TERNARY && c.size() == 3) {
if (!at_base_lvl() && propagate_ter_clause(c))
m_clauses_to_reinit[j++] = cw;
else if (has_variables_to_reinit(c))
m_clauses_to_reinit[j++] = cw;
else
c.set_reinit_stack(false);
continue;
}
detach_clause(c);
attach_clause(c, reinit);
if (!at_base_lvl() && reinit)
m_clauses_to_reinit[j++] = cw;
else if (has_variables_to_reinit(c))
m_clauses_to_reinit[j++] = cw;
else
c.set_reinit_stack(false);
}
}
m_clauses_to_reinit.shrink(j);
}
void solver::user_push() {
pop_to_base_level();
m_free_var_freeze.push_back(m_free_vars);
m_free_vars.reset();
bool_var new_v = mk_var(true, false);
literal lit = literal(new_v, false);
m_user_scope_literals.push_back(lit);
m_cut_simplifier = nullptr;
if (m_ext)
m_ext->user_push();
TRACE("sat", tout << "user_push: " << lit << "\n";);
}
void solver::user_pop(unsigned num_scopes) {
unsigned old_sz = m_user_scope_literals.size() - num_scopes;
bool_var max_var = m_user_scope_literals[old_sz].var();
m_user_scope_literals.shrink(old_sz);
pop_to_base_level();
if (m_ext)
m_ext->user_pop(num_scopes);
gc_vars(max_var);
TRACE("sat", display(tout););
m_qhead = 0;
unsigned j = 0;
for (bool_var v : m_free_vars)
if (v < max_var)
m_free_vars[j++] = v;
m_free_vars.shrink(j);
m_free_vars.append(m_free_var_freeze[old_sz]);
m_free_var_freeze.shrink(old_sz);
scoped_suspend_rlimit _sp(m_rlimit);
propagate(false);
}
void solver::pop_to_base_level() {
reset_assumptions();
pop(scope_lvl());
}
void solver::updt_params(params_ref const & p) {
m_params.append(p);
m_config.updt_params(p);
m_simplifier.updt_params(p);
m_asymm_branch.updt_params(p);
m_probing.updt_params(p);
m_scc.updt_params(p);
m_rand.set_seed(m_config.m_random_seed);
m_step_size = m_config.m_step_size_init;
m_drat.updt_config();
m_fast_glue_avg.set_alpha(m_config.m_fast_glue_avg);
m_slow_glue_avg.set_alpha(m_config.m_slow_glue_avg);
m_fast_glue_backup.set_alpha(m_config.m_fast_glue_avg);
m_slow_glue_backup.set_alpha(m_config.m_slow_glue_avg);
m_trail_avg.set_alpha(m_config.m_slow_glue_avg);
if (m_config.m_cut_simplify && !m_cut_simplifier && m_user_scope_literals.empty()) {
m_cut_simplifier = alloc(cut_simplifier, *this);
}
}
void solver::collect_param_descrs(param_descrs & d) {
config::collect_param_descrs(d);
simplifier::collect_param_descrs(d);
asymm_branch::collect_param_descrs(d);
probing::collect_param_descrs(d);
scc::collect_param_descrs(d);
}
void solver::collect_statistics(statistics & st) const {
m_stats.collect_statistics(st);
m_cleaner.collect_statistics(st);
m_simplifier.collect_statistics(st);
m_scc.collect_statistics(st);
m_asymm_branch.collect_statistics(st);
m_probing.collect_statistics(st);
if (m_ext) m_ext->collect_statistics(st);
if (m_local_search) m_local_search->collect_statistics(st);
if (m_cut_simplifier) m_cut_simplifier->collect_statistics(st);
st.copy(m_aux_stats);
}
void solver::reset_statistics() {
m_stats.reset();
m_cleaner.reset_statistics();
m_simplifier.reset_statistics();
m_asymm_branch.reset_statistics();
m_probing.reset_statistics();
m_aux_stats.reset();
}
void solver::rescale_activity() {
SASSERT(m_config.m_branching_heuristic == BH_VSIDS);
for (unsigned& act : m_activity) {
act >>= 14;
}
m_activity_inc >>= 14;
}
void solver::update_chb_activity(bool is_sat, unsigned qhead) {
SASSERT(m_config.m_branching_heuristic == BH_CHB);
double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0);
for (unsigned i = qhead; i < m_trail.size(); ++i) {
auto v = m_trail[i].var();
auto d = m_stats.m_conflict - m_last_conflict[v] + 1;
if (d == 0) d = 1;
auto reward = multiplier / d;
auto activity = m_activity[v];
set_activity(v, static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity)));
}
}
void solver::move_to_front(bool_var b) {
if (b >= num_vars())
return;
bool_var next = m_case_split_queue.min_var();
auto next_act = m_activity[next];
set_activity(b, next_act + 1);
}
void solver::collect_bin_clauses(svector<bin_clause> & r, bool redundant, bool learned_only) const {
SASSERT(redundant || !learned_only);
unsigned sz = m_watches.size();
for (unsigned l_idx = 0; l_idx < sz; l_idx++) {
literal l = to_literal(l_idx);
l.neg();
for (watched const& w : m_watches[l_idx]) {
if (!w.is_binary_clause())
continue;
if (!redundant && w.is_learned())
continue;
else if (redundant && learned_only && !w.is_learned())
continue;
literal l2 = w.get_literal();
if (l.index() > l2.index())
continue;
TRACE("cleanup_bug", tout << "collected: " << l << " " << l2 << "\n";);
r.push_back(bin_clause(l, l2));
}
}
}
bool solver::check_invariant() const {
if (!m_rlimit.inc()) return true;
integrity_checker checker(*this);
VERIFY(checker());
VERIFY(!m_ext || m_ext->validate());
return true;
}
bool solver::check_marks() const {
for (bool_var v = 0; v < num_vars(); v++) {
SASSERT(!is_marked(v));
}
return true;
}
std::ostream& solver::display_model(std::ostream& out) const {
unsigned num = num_vars();
for (bool_var v = 0; v < num; v++) {
out << v << ": " << m_model[v] << "\n";
}
return out;
}
void solver::display_binary(std::ostream & out) const {
unsigned sz = m_watches.size();
for (unsigned l_idx = 0; l_idx < sz; l_idx++) {
literal l = to_literal(l_idx);
l.neg();
for (watched const& w : m_watches[l_idx]) {
if (!w.is_binary_clause())
continue;
literal l2 = w.get_literal();
if (l.index() > l2.index())
continue;
out << "(" << l << " " << l2 << ")";
if (w.is_learned()) out << "*";
out << "\n";
}
}
}
void solver::display_units(std::ostream & out) const {
unsigned level = 0;
for (literal lit : m_trail) {
if (lvl(lit) > level) {
level = lvl(lit);
out << level << ": ";
}
else {
out << " ";
}
out << lit << " ";
if (lvl(lit) < level) {
out << "@" << lvl(lit) << " ";
}
display_justification(out, m_justification[lit.var()]) << "\n";
}
}
void solver::display(std::ostream & out) const {
out << "(sat\n";
display_units(out);
display_binary(out);
out << m_clauses << m_learned;
if (m_ext) {
m_ext->display(out);
}
out << ")\n";
}
std::ostream& solver::display_justification(std::ostream & out, justification const& js) const {
switch (js.get_kind()) {
case justification::NONE:
out << "none @" << js.level();
break;
case justification::BINARY:
out << "binary " << js.get_literal() << "@" << lvl(js.get_literal());
break;
case justification::TERNARY:
out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " ";
out << js.get_literal2() << "@" << lvl(js.get_literal2());
break;
case justification::CLAUSE: {
out << "(";
bool first = true;
for (literal l : get_clause(js)) {
if (first) first = false; else out << " ";
out << l << "@" << lvl(l);
}
out << ")";
break;
}
case justification::EXT_JUSTIFICATION:
if (m_ext)
m_ext->display_justification(out << "ext ", js.get_ext_justification_idx());
break;
default:
break;
}
return out;
}
unsigned solver::num_clauses() const {
unsigned num_cls = m_trail.size();
unsigned l_idx = 0;
for (auto const& wl : m_watches) {
literal l = ~to_literal(l_idx++);
for (auto const& w : wl) {
if (w.is_binary_clause() && l.index() < w.get_literal().index())
num_cls++;
}
}
return num_cls + m_clauses.size() + m_learned.size();
}
void solver::num_binary(unsigned& given, unsigned& redundant) const {
given = redundant = 0;
unsigned l_idx = 0;
for (auto const& wl : m_watches) {
literal l = ~to_literal(l_idx++);
for (auto const& w : wl) {
if (w.is_binary_clause() && l.index() < w.get_literal().index()) {
if (w.is_learned()) ++redundant; else ++given;
}
}
}
}
void solver::display_dimacs(std::ostream & out) const {
out << "p cnf " << num_vars() << " " << num_clauses() << "\n";
for (literal lit : m_trail) {
out << dimacs_lit(lit) << " 0\n";
}
unsigned l_idx = 0;
for (auto const& wlist : m_watches) {
literal l = ~to_literal(l_idx++);
for (auto const& w : wlist) {
if (w.is_binary_clause() && l.index() < w.get_literal().index())
out << dimacs_lit(l) << " " << dimacs_lit(w.get_literal()) << " 0\n";
}
}
clause_vector const * vs[2] = { &m_clauses, &m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector const & cs = *(vs[i]);
for (auto cp : cs) {
for (literal l : *cp) {
out << dimacs_lit(l) << " ";
}
out << "0\n";
}
}
}
void solver::display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const {
unsigned max_weight = 0;
for (unsigned i = 0; i < sz; ++i)
max_weight += weights[i];
++max_weight;
if (m_ext)
throw default_exception("wcnf is only supported for pure CNF problems");
out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
out << "c soft " << sz << "\n";
for (literal lit : m_trail)
out << max_weight << " " << dimacs_lit(lit) << " 0\n";
unsigned l_idx = 0;
for (watch_list const& wlist : m_watches) {
literal l = ~to_literal(l_idx);
for (watched const& w : wlist) {
if (w.is_binary_clause() && l.index() < w.get_literal().index())
out << max_weight << " " << dimacs_lit(l) << " " << dimacs_lit(w.get_literal()) << " 0\n";
}
++l_idx;
}
clause_vector const * vs[2] = { &m_clauses, &m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector const & cs = *(vs[i]);
for (clause const* cp : cs) {
clause const & c = *cp;
out << max_weight << " ";
for (literal l : c)
out << dimacs_lit(l) << " ";
out << "0\n";
}
}
for (unsigned i = 0; i < sz; ++i) {
out << weights[i] << " " << lits[i] << " 0\n";
}
out.flush();
}
void solver::display_watches(std::ostream & out, literal lit) const {
display_watch_list(out << lit << ": ", get_wlist(lit)) << "\n";
}
void solver::display_watches(std::ostream & out) const {
unsigned l_idx = 0;
for (watch_list const& wlist : m_watches) {
literal l = to_literal(l_idx++);
if (!wlist.empty())
display_watch_list(out << l << ": ", wlist) << "\n";
}
}
std::ostream& solver::display_watch_list(std::ostream& out, watch_list const& wl) const {
return sat::display_watch_list(out, cls_allocator(), wl, m_ext.get());
}
void solver::display_assignment(std::ostream & out) const {
out << m_trail << "\n";
}
\brief Return true, if c is a clause containing one unassigned literal.
*/
bool solver::is_unit(clause const & c) const {
bool found_undef = false;
for (literal l : c) {
switch (value(l)) {
case l_undef:
if (found_undef)
return false;
found_undef = true;
break;
case l_true:
return false;
case l_false:
break;
}
}
return found_undef;
}
\brief Return true, if all literals in c are assigned to false.
*/
bool solver::is_empty(clause const & c) const {
for (literal lit : c)
if (value(lit) != l_false)
return false;
return true;
}
bool solver::check_missed_propagation(clause_vector const & cs) const {
for (clause* cp : cs) {
clause const & c = *cp;
if (c.frozen())
continue;
if (is_empty(c) || is_unit(c)) {
TRACE("sat_missed_prop", tout << "missed_propagation: " << c << "\n";
for (literal l : c) tout << l << ": " << value(l) << "\n";);
UNREACHABLE();
}
SASSERT(!is_empty(c));
SASSERT(!is_unit(c));
}
return true;
}
bool solver::check_missed_propagation() const {
if (inconsistent())
return true;
return check_missed_propagation(m_clauses) && check_missed_propagation(m_learned);
}
bool solver::do_cleanup(bool force) {
if (m_conflicts_since_init == 0 && !force)
return false;
if (at_base_lvl() && !inconsistent() && m_cleaner(force)) {
if (m_ext)
m_ext->clauses_modifed();
return true;
}
return false;
}
void solver::simplify(bool redundant) {
if (!at_base_lvl() || inconsistent())
return;
m_simplifier(redundant);
m_simplifier.finalize();
if (m_ext)
m_ext->clauses_modifed();
}
unsigned solver::scc_bin() {
if (!at_base_lvl() || inconsistent())
return 0;
unsigned r = m_scc();
if (r > 0 && m_ext)
m_ext->clauses_modifed();
return r;
}
struct neg_literal {
unsigned negate(unsigned idx) {
return (~to_literal(idx)).index();
}
};
lbool solver::find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes) {
max_cliques<neg_literal> mc;
m_user_bin_clauses.reset();
m_binary_clause_graph.reset();
collect_bin_clauses(m_user_bin_clauses, true, false);
hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc;
for (auto const& b : m_user_bin_clauses) {
literal l1 = b.first;
literal l2 = b.second;
literal_pair p(l1, l2);
if (!seen_bc.contains(p)) {
seen_bc.insert(p);
mc.add_edge(l1.index(), l2.index());
}
}
vector<unsigned_vector> _mutexes;
literal_vector _lits(lits);
if (m_ext) {
}
unsigned_vector ps;
for (literal lit : _lits) {
ps.push_back(lit.index());
}
mc.cliques(ps, _mutexes);
for (auto const& mux : _mutexes) {
literal_vector clique;
for (auto const& idx : mux) {
clique.push_back(to_literal(idx));
}
mutexes.push_back(clique);
}
return l_true;
}
static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
for (unsigned i = 0; i < lambda.size(); ++i) {
if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
lambda[i] = lambda.back();
lambda.pop_back();
--i;
}
}
}
static void back_remove(sat::literal_vector& lits, sat::literal l) {
for (unsigned i = lits.size(); i > 0; ) {
--i;
if (lits[i] == l) {
lits[i] = lits.back();
lits.pop_back();
return;
}
}
UNREACHABLE();
}
static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_vector>& conseq) {
for (literal lit : gamma) {
sat::literal_vector asms1(asms);
asms1.push_back(~lit);
lbool r = s.check(asms1.size(), asms1.data());
if (r == l_false) {
conseq.push_back(s.get_core());
}
}
}
static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
sat::literal_vector lambda;
for (bool_var v : vars) {
lambda.push_back(sat::literal(v, m[v] == l_false));
}
while (!lambda.empty()) {
IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";);
unsigned k = std::min(K, lambda.size());
sat::literal_vector gamma, omegaN;
for (unsigned i = 0; i < k; ++i) {
sat::literal l = lambda[lambda.size() - i - 1];
gamma.push_back(l);
omegaN.push_back(~l);
}
while (true) {
sat::literal_vector asms1(asms);
asms1.append(omegaN);
lbool r = s.check(asms1.size(), asms1.data());
if (r == l_true) {
IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
prune_unfixed(lambda, s.get_model());
break;
}
sat::literal_vector const& core = s.get_core();
sat::literal_vector occurs;
IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";);
for (unsigned i = 0; i < omegaN.size(); ++i) {
if (core.contains(omegaN[i])) {
occurs.push_back(omegaN[i]);
}
}
if (occurs.size() == 1) {
sat::literal lit = occurs.back();
sat::literal nlit = ~lit;
conseq.push_back(core);
back_remove(lambda, ~lit);
back_remove(gamma, ~lit);
s.mk_clause(1, &nlit);
}
for (unsigned i = 0; i < omegaN.size(); ++i) {
if (occurs.contains(omegaN[i])) {
omegaN[i] = omegaN.back();
omegaN.pop_back();
--i;
}
}
if (omegaN.empty() && occurs.size() > 1) {
brute_force_consequences(s, asms, gamma, conseq);
for (unsigned i = 0; i < gamma.size(); ++i) {
back_remove(lambda, gamma[i]);
}
break;
}
}
}
return l_true;
}
lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
literal_vector lits;
lbool is_sat = l_true;
if (m_config.m_restart_max != UINT_MAX && !m_model_is_current) {
return get_bounded_consequences(asms, vars, conseq);
}
if (!m_model_is_current) {
is_sat = check(asms.size(), asms.data());
}
if (is_sat != l_true) {
return is_sat;
}
model mdl = get_model();
for (unsigned i = 0; i < vars.size(); ++i) {
bool_var v = vars[i];
switch (get_model()[v]) {
case l_true: lits.push_back(literal(v, false)); break;
case l_false: lits.push_back(literal(v, true)); break;
default: break;
}
}
if (false && asms.empty()) {
is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
}
else {
is_sat = get_consequences(asms, lits, conseq);
}
set_model(mdl, !mdl.empty());
return is_sat;
}
void solver::fixup_consequence_core() {
index_set s;
TRACE("sat", tout << m_core << "\n";);
for (unsigned i = 0; i < m_core.size(); ++i) {
TRACE("sat", tout << m_core[i] << ": "; display_index_set(tout, m_antecedents.find(m_core[i].var())) << "\n";);
s |= m_antecedents.find(m_core[i].var());
}
m_core.reset();
for (unsigned idx : s) {
m_core.push_back(to_literal(idx));
}
TRACE("sat", tout << m_core << "\n";);
}
bool solver::reached_max_conflicts() {
if (m_config.m_max_conflicts == 0 || m_conflicts_since_init > m_config.m_max_conflicts) {
if (m_reason_unknown != "sat.max.conflicts") {
m_reason_unknown = "sat.max.conflicts";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts_since_init << "\")\n";);
}
return !inconsistent();
}
return false;
}
lbool solver::get_bounded_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
bool_var_set unfixed_vars;
unsigned num_units = 0, num_iterations = 0;
for (bool_var v : vars) {
unfixed_vars.insert(v);
}
TRACE("sat", tout << asms << "\n";);
m_antecedents.reset();
pop_to_base_level();
if (inconsistent()) return l_false;
flet<bool> _searching(m_searching, true);
init_search();
propagate(false);
if (inconsistent()) return l_false;
if (asms.empty()) {
bool_var v = mk_var(true, false);
literal lit(v, false);
init_assumptions(1, &lit);
}
else {
init_assumptions(asms.size(), asms.data());
}
propagate(false);
if (check_inconsistent()) return l_false;
extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
do_simplify();
if (check_inconsistent()) {
fixup_consequence_core();
return l_false;
}
while (true) {
++num_iterations;
SASSERT(!inconsistent());
lbool r = bounded_search();
if (r != l_undef) {
fixup_consequence_core();
return r;
}
extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
do_restart(true);
do_simplify();
if (check_inconsistent()) {
fixup_consequence_core();
return l_false;
}
do_gc();
if (should_cancel()) {
return l_undef;
}
}
}
lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector<literal_vector>& conseq) {
TRACE("sat", tout << asms << "\n";);
m_antecedents.reset();
literal_set unfixed_lits(lits), assumptions(asms);
bool_var_set unfixed_vars;
for (literal lit : lits) {
unfixed_vars.insert(lit.var());
}
pop_to_base_level();
if (inconsistent()) return l_false;
init_search();
propagate(false);
if (inconsistent()) return l_false;
if (asms.empty()) {
bool_var v = mk_var(true, false);
literal lit(v, false);
init_assumptions(1, &lit);
}
else {
init_assumptions(asms.size(), asms.data());
}
propagate(false);
if (check_inconsistent()) return l_false;
SASSERT(search_lvl() == 1);
unsigned num_iterations = 0;
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
while (!unfixed_lits.empty()) {
if (scope_lvl() > search_lvl()) {
pop(scope_lvl() - search_lvl());
}
propagate(false);
++num_iterations;
checkpoint();
unsigned num_resolves = 0;
unsigned num_fixed = 0;
unsigned num_assigned = 0;
lbool is_sat = l_true;
for (literal lit : unfixed_lits) {
if (value(lit) != l_undef) {
++num_fixed;
if (lvl(lit) <= 1 && value(lit) == l_true) {
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
}
continue;
}
push();
++num_assigned;
assign_scoped(~lit);
propagate(false);
while (inconsistent()) {
if (!resolve_conflict()) {
TRACE("sat", display(tout << "inconsistent\n"););
m_inconsistent = false;
is_sat = l_undef;
break;
}
propagate(false);
++num_resolves;
}
}
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
if (is_sat == l_true) {
if (scope_lvl() == search_lvl() && num_resolves > 0) {
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";);
is_sat = l_undef;
}
else {
is_sat = bounded_search();
if (is_sat == l_undef) {
do_restart(true);
propagate(false);
}
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
}
}
if (is_sat == l_false) {
TRACE("sat", tout << "unsat\n";);
m_inconsistent = false;
}
if (is_sat == l_true) {
delete_unfixed(unfixed_lits, unfixed_vars);
}
update_unfixed_literals(unfixed_lits, unfixed_vars);
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
<< " iterations: " << num_iterations
<< " variables: " << unfixed_lits.size()
<< " fixed: " << conseq.size()
<< " status: " << is_sat
<< " pre-assigned: " << num_fixed
<< " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size()
<< ")\n";);
if (!unfixed_lits.empty() && m_config.m_restart_max <= num_iterations) {
return l_undef;
}
}
return l_true;
}
void solver::delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars) {
literal_set to_keep;
for (literal lit : unfixed_lits) {
if (value(lit) == l_true) {
to_keep.insert(lit);
}
else {
unfixed_vars.remove(lit.var());
}
}
unfixed_lits = to_keep;
}
void solver::update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars) {
literal_vector to_delete;
for (literal lit : unfixed_lits) {
if (!unfixed_vars.contains(lit.var())) {
to_delete.push_back(lit);
}
}
for (unsigned i = 0; i < to_delete.size(); ++i) {
unfixed_lits.remove(to_delete[i]);
}
}
void solver::extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
SASSERT(!inconsistent());
unsigned sz = m_trail.size();
for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) {
extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq);
}
start = sz;
}
void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector<literal_vector>& conseq) {
for (literal lit: unfixed_lits) {
TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";);
if (lvl(lit) <= 1 && value(lit) == l_true) {
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
}
}
}
bool solver::check_domain(literal lit, literal lit2) {
if (!m_antecedents.contains(lit2.var())) {
SASSERT(value(lit2) == l_true);
SASSERT(m_todo_antecedents.empty() || m_todo_antecedents.back() != lit2);
m_todo_antecedents.push_back(lit2);
return false;
}
else {
return true;
}
}
bool solver::extract_assumptions(literal lit, index_set& s) {
justification js = m_justification[lit.var()];
TRACE("sat", tout << lit << " " << js << "\n";);
bool all_found = true;
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
if (!check_domain(lit, ~js.get_literal())) return false;
s |= m_antecedents.find(js.get_literal().var());
break;
case justification::TERNARY:
if (!check_domain(lit, ~js.get_literal1()) ||
!check_domain(lit, ~js.get_literal2())) return false;
s |= m_antecedents.find(js.get_literal1().var());
s |= m_antecedents.find(js.get_literal2().var());
break;
case justification::CLAUSE: {
clause & c = get_clause(js);
for (literal l : c) {
if (l != lit) {
if (check_domain(lit, ~l) && all_found) {
s |= m_antecedents.find(l.var());
}
else {
all_found = false;
}
}
}
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(lit, js, true);
for (literal l : m_ext_antecedents) {
if (check_domain(lit, l) && all_found) {
s |= m_antecedents.find(l.var());
}
else {
all_found = false;
}
}
break;
}
default:
UNREACHABLE();
break;
}
TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";);
return all_found;
}
std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const {
for (unsigned idx : s) {
out << to_literal(idx) << " ";
}
return out;
}
bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
index_set s;
if (m_antecedents.contains(lit.var())) {
return true;
}
if (assumptions.contains(lit)) {
s.insert(lit.index());
}
else {
if (!extract_assumptions(lit, s)) {
SASSERT(!m_todo_antecedents.empty());
return false;
}
add_assumption(lit);
}
m_antecedents.insert(lit.var(), s);
if (unfixed.contains(lit.var())) {
literal_vector cons;
cons.push_back(lit);
for (unsigned idx : s) {
cons.push_back(to_literal(idx));
}
unfixed.remove(lit.var());
conseq.push_back(cons);
}
return true;
}
void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
SASSERT(m_todo_antecedents.empty());
m_todo_antecedents.push_back(lit);
while (!m_todo_antecedents.empty()) {
if (extract_fixed_consequences1(m_todo_antecedents.back(), assumptions, unfixed, conseq)) {
m_todo_antecedents.pop_back();
}
}
}
void solver::display_status(std::ostream & out) const {
unsigned num_bin = 0;
unsigned num_ext = 0;
unsigned num_lits = 0;
unsigned l_idx = 0;
for (watch_list const& wlist : m_watches) {
literal l = ~to_literal(l_idx++);
for (watched const& w : wlist) {
switch (w.get_kind()) {
case watched::BINARY:
if (l.index() < w.get_literal().index()) {
num_lits += 2;
num_bin++;
}
break;
case watched::EXT_CONSTRAINT:
num_ext++;
break;
default:
break;
}
}
}
unsigned num_elim = 0;
for (bool_var v = 0; v < num_vars(); v++) {
if (m_eliminated[v])
num_elim++;
}
unsigned num_ter = 0;
unsigned num_cls = 0;
clause_vector const * vs[2] = { &m_clauses, &m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector const & cs = *(vs[i]);
for (clause* cp : cs) {
clause & c = *cp;
if (ENABLE_TERNARY && c.size() == 3)
num_ter++;
else
num_cls++;
num_lits += c.size();
}
}
unsigned total_cls = num_cls + num_ter + num_bin;
double mem = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
out << "(sat-status\n";
out << " :inconsistent " << (m_inconsistent ? "true" : "false") << "\n";
out << " :vars " << num_vars() << "\n";
out << " :elim-vars " << num_elim << "\n";
out << " :lits " << num_lits << "\n";
out << " :assigned " << m_trail.size() << "\n";
out << " :binary-clauses " << num_bin << "\n";
out << " :ternary-clauses " << num_ter << "\n";
out << " :clauses " << num_cls << "\n";
out << " :del-clause " << m_stats.m_del_clause << "\n";
out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast<double>(num_lits) / static_cast<double>(total_cls)) << "\n";
out << " :memory " << std::fixed << std::setprecision(2) << mem << ")" << std::endl;
}
void stats::collect_statistics(statistics & st) const {
st.update("sat mk clause 2ary", m_mk_bin_clause);
st.update("sat mk clause 3ary", m_mk_ter_clause);
st.update("sat mk clause nary", m_mk_clause);
st.update("sat mk var", m_mk_var);
st.update("sat gc clause", m_gc_clause);
st.update("sat del clause", m_del_clause);
st.update("sat conflicts", m_conflict);
st.update("sat decisions", m_decision);
st.update("sat propagations 2ary", m_bin_propagate);
st.update("sat propagations 3ary", m_ter_propagate);
st.update("sat propagations nary", m_propagate);
st.update("sat restarts", m_restart);
st.update("sat minimized lits", m_minimized_lits);
st.update("sat subs resolution dyn", m_dyn_sub_res);
st.update("sat blocked correction sets", m_blocked_corr_sets);
st.update("sat units", m_units);
st.update("sat elim bool vars res", m_elim_var_res);
st.update("sat elim bool vars bdd", m_elim_var_bdd);
st.update("sat backjumps", m_backjumps);
st.update("sat backtracks", m_backtracks);
}
void stats::reset() {
memset(this, 0, sizeof(*this));
}
void mk_stat::display(std::ostream & out) const {
unsigned given, redundant;
m_solver.num_binary(given, redundant);
out << " " << std::setw(5) << m_solver.m_clauses.size() + given << "/" << given;
out << " " << std::setw(5) << (m_solver.m_learned.size() + redundant - m_solver.m_num_frozen) << "/" << redundant;
out << " " << std::setw(3) << m_solver.init_trail_size();
out << " " << std::setw(7) << m_solver.m_stats.m_gc_clause << " ";
out << " " << std::setw(7) << mem_stat();
}
std::ostream & operator<<(std::ostream & out, mk_stat const & stat) {
stat.display(out);
return out;
}
bool solver::all_distinct(literal_vector const& lits) {
init_visited();
for (literal l : lits) {
if (is_visited(l.var())) {
return false;
}
mark_visited(l.var());
}
return true;
}
bool solver::all_distinct(clause const& c) {
init_visited();
for (literal l : c) {
if (is_visited(l.var())) {
return false;
}
mark_visited(l.var());
}
return true;
}
void solver::init_visited() {
if (m_visited.empty()) {
m_visited_ts = 0;
}
m_visited_ts++;
if (m_visited_ts == 0) {
m_visited_ts = 1;
m_visited.reset();
}
while (m_visited.size() < 2*num_vars()) {
m_visited.push_back(0);
}
}
};