mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
2495 lines
88 KiB
C++
2495 lines
88 KiB
C++
/*++
|
|
Copyright (c) 2017 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_lookahead.h
|
|
|
|
Abstract:
|
|
|
|
Lookahead SAT solver in the style of March.
|
|
Thanks also to the presentation in sat11.w.
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2017-2-11
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
|
|
#include <cmath>
|
|
#include "sat/sat_solver.h"
|
|
#include "sat/sat_extension.h"
|
|
#include "sat/sat_lookahead.h"
|
|
#include "sat/sat_scc.h"
|
|
#include "util/union_find.h"
|
|
|
|
namespace sat {
|
|
lookahead::scoped_ext::scoped_ext(lookahead& p): p(p) {
|
|
if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(&p);
|
|
}
|
|
|
|
lookahead::scoped_ext::~scoped_ext() {
|
|
if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(0);
|
|
}
|
|
|
|
lookahead::scoped_assumptions::scoped_assumptions(lookahead& p, literal_vector const& lits): p(p), lits(lits) {
|
|
for (auto l : lits) {
|
|
p.push(l, p.c_fixed_truth);
|
|
}
|
|
}
|
|
lookahead::scoped_assumptions::~scoped_assumptions() {
|
|
for (auto l : lits) {
|
|
(void)l;
|
|
p.pop();
|
|
}
|
|
}
|
|
|
|
void lookahead::flip_prefix() {
|
|
if (m_trail_lim.size() < 64) {
|
|
uint64_t mask = (1ull << m_trail_lim.size());
|
|
m_prefix = mask | (m_prefix & (mask - 1));
|
|
}
|
|
}
|
|
|
|
void lookahead::prune_prefix() {
|
|
if (m_trail_lim.size() < 64) {
|
|
m_prefix &= (1ull << m_trail_lim.size()) - 1;
|
|
}
|
|
}
|
|
|
|
void lookahead::update_prefix(literal l) {
|
|
bool_var x = l.var();
|
|
unsigned p = m_vprefix[x].m_prefix;
|
|
unsigned pl = m_vprefix[x].m_length;
|
|
unsigned mask = (1 << std::min(31u, pl)) - 1;
|
|
if (pl >= m_trail_lim.size() || (p & mask) != (m_prefix & mask)) {
|
|
m_vprefix[x].m_length = m_trail_lim.size();
|
|
m_vprefix[x].m_prefix = static_cast<unsigned>(m_prefix);
|
|
}
|
|
}
|
|
|
|
bool lookahead::active_prefix(bool_var x) {
|
|
unsigned lvl = m_trail_lim.size();
|
|
unsigned p = m_vprefix[x].m_prefix;
|
|
unsigned l = m_vprefix[x].m_length;
|
|
if (l > lvl) return false;
|
|
if (l == lvl || l >= 31) return m_prefix == p;
|
|
unsigned mask = ((1 << std::min(l,31u)) - 1);
|
|
return (m_prefix & mask) == (p & mask);
|
|
}
|
|
|
|
void lookahead::add_binary(literal l1, literal l2) {
|
|
TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";);
|
|
SASSERT(l1 != l2);
|
|
// don't add tautologies and don't add already added binaries
|
|
if (~l1 == l2) return;
|
|
if (!m_binary[(~l1).index()].empty() && m_binary[(~l1).index()].back() == l2) return;
|
|
m_binary[(~l1).index()].push_back(l2);
|
|
m_binary[(~l2).index()].push_back(l1);
|
|
m_binary_trail.push_back((~l1).index());
|
|
++m_stats.m_add_binary;
|
|
if (m_s.m_config.m_drat) validate_binary(l1, l2);
|
|
}
|
|
|
|
void lookahead::del_binary(unsigned idx) {
|
|
// TRACE("sat", display(tout << "Delete " << to_literal(idx) << "\n"););
|
|
literal_vector & lits = m_binary[idx];
|
|
SASSERT(!lits.empty());
|
|
literal l = lits.back();
|
|
lits.pop_back();
|
|
SASSERT(!m_binary[(~l).index()].empty());
|
|
IF_VERBOSE(0, if (m_binary[(~l).index()].back() != ~to_literal(idx)) verbose_stream() << "pop bad literal: " << idx << " " << (~l).index() << "\n";);
|
|
SASSERT(m_binary[(~l).index()].back() == ~to_literal(idx));
|
|
m_binary[(~l).index()].pop_back();
|
|
++m_stats.m_del_binary;
|
|
}
|
|
|
|
|
|
void lookahead::validate_binary(literal l1, literal l2) {
|
|
if (m_search_mode == lookahead_mode::searching) {
|
|
m_assumptions.push_back(l1);
|
|
m_assumptions.push_back(l2);
|
|
m_drat.add(m_assumptions);
|
|
m_assumptions.pop_back();
|
|
m_assumptions.pop_back();
|
|
}
|
|
}
|
|
|
|
void lookahead::inc_bstamp() {
|
|
++m_bstamp_id;
|
|
if (m_bstamp_id == 0) {
|
|
++m_bstamp_id;
|
|
m_bstamp.fill(0);
|
|
}
|
|
}
|
|
|
|
void lookahead::inc_istamp() {
|
|
++m_istamp_id;
|
|
if (m_istamp_id == 0) {
|
|
++m_istamp_id;
|
|
for (unsigned i = 0; i < m_lits.size(); ++i) {
|
|
m_lits[i].m_double_lookahead = 0;
|
|
}
|
|
}
|
|
}
|
|
|
|
void lookahead::set_bstamps(literal l) {
|
|
inc_bstamp();
|
|
set_bstamp(l);
|
|
literal_vector const& conseq = m_binary[l.index()];
|
|
for (literal l : conseq) {
|
|
set_bstamp(l);
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief add one-step transitive closure of binary implications
|
|
return false if we learn a unit literal.
|
|
\pre all implicants of ~u are stamped.
|
|
u \/ v is true
|
|
**/
|
|
|
|
bool lookahead::add_tc1(literal u, literal v) {
|
|
unsigned sz = m_binary[v.index()].size();
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
literal w = m_binary[v.index()][i];
|
|
// ~v \/ w
|
|
if (!is_fixed(w)) {
|
|
if (is_stamped(~w)) {
|
|
// u \/ v, ~v \/ w, u \/ ~w => u is unit
|
|
TRACE("sat", tout << "tc1: " << u << "\n";);
|
|
propagated(u);
|
|
return false;
|
|
}
|
|
if (m_num_tc1 < m_config.m_tc1_limit) {
|
|
++m_num_tc1;
|
|
IF_VERBOSE(30, verbose_stream() << "tc1: " << u << " " << w << "\n";);
|
|
add_binary(u, w);
|
|
}
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
|
|
/**
|
|
\brief main routine for adding a new binary clause dynamically.
|
|
*/
|
|
void lookahead::try_add_binary(literal u, literal v) {
|
|
SASSERT(m_search_mode == lookahead_mode::searching);
|
|
SASSERT(u.var() != v.var());
|
|
if (!is_undef(u) || !is_undef(v)) {
|
|
IF_VERBOSE(0, verbose_stream() << "adding assigned binary " << v << " " << u << "\n";);
|
|
}
|
|
set_bstamps(~u);
|
|
if (is_stamped(~v)) {
|
|
TRACE("sat", tout << "try_add_binary: " << u << "\n";);
|
|
propagated(u); // u \/ ~v, u \/ v => u is a unit literal
|
|
}
|
|
else if (!is_stamped(v) && add_tc1(u, v)) {
|
|
// u \/ v is not in index
|
|
set_bstamps(~v);
|
|
if (is_stamped(~u)) {
|
|
TRACE("sat", tout << "try_add_binary: " << v << "\n";);
|
|
propagated(v); // v \/ ~u, u \/ v => v is a unit literal
|
|
}
|
|
else if (add_tc1(v, u)) {
|
|
update_prefix(u);
|
|
update_prefix(v);
|
|
add_binary(u, v);
|
|
}
|
|
}
|
|
}
|
|
|
|
// -------------------------------------
|
|
// pre-selection
|
|
// see also 91 - 102 sat11.w
|
|
|
|
|
|
void lookahead::pre_select() {
|
|
IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :freevars " << m_freevars.size() << ")\n";);
|
|
m_lookahead.reset();
|
|
for (bool_var x : m_freevars) { // tree lookahead leaves literals fixed in lower truth levels
|
|
literal l(x, false);
|
|
set_undef(l);
|
|
set_undef(~l);
|
|
}
|
|
if (select(scope_lvl())) {
|
|
get_scc();
|
|
if (inconsistent()) return;
|
|
find_heights();
|
|
construct_lookahead_table();
|
|
}
|
|
}
|
|
|
|
|
|
bool lookahead::select(unsigned level) {
|
|
init_pre_selection(level);
|
|
unsigned level_cand = std::max(m_config.m_level_cand, m_freevars.size() / 50);
|
|
unsigned max_num_cand = (level > 0 && m_config.m_preselect) ? level_cand / level : m_freevars.size();
|
|
max_num_cand = std::max(m_config.m_min_cutoff, max_num_cand);
|
|
|
|
double sum = 0;
|
|
for (bool newbies = false; ; newbies = true) {
|
|
sum = init_candidates(level, newbies);
|
|
if (!m_candidates.empty()) break;
|
|
if (is_sat()) {
|
|
return false;
|
|
}
|
|
}
|
|
SASSERT(!m_candidates.empty());
|
|
// cut number of candidates down to max_num_cand.
|
|
// step 1. cut it to at most 2*max_num_cand.
|
|
// step 2. use a heap to sift through the rest.
|
|
bool progress = true;
|
|
while (progress && m_candidates.size() >= max_num_cand * 2) {
|
|
progress = false;
|
|
double mean = sum / (double)(m_candidates.size() + 0.0001);
|
|
sum = 0;
|
|
for (unsigned i = 0; i < m_candidates.size() && m_candidates.size() >= max_num_cand * 2; ++i) {
|
|
if (m_candidates[i].m_rating >= mean) {
|
|
sum += m_candidates[i].m_rating;
|
|
}
|
|
else {
|
|
m_candidates[i] = m_candidates.back();
|
|
m_candidates.pop_back();
|
|
--i;
|
|
progress = true;
|
|
}
|
|
}
|
|
}
|
|
TRACE("sat", display_candidates(tout););
|
|
SASSERT(!m_candidates.empty());
|
|
heap_sort();
|
|
while (m_candidates.size() > max_num_cand) {
|
|
m_candidates.pop_back();
|
|
}
|
|
SASSERT(!m_candidates.empty() && m_candidates.size() <= max_num_cand);
|
|
TRACE("sat", display_candidates(tout););
|
|
return true;
|
|
}
|
|
|
|
void lookahead::heap_sort() {
|
|
if (m_candidates.size() > 1) {
|
|
heapify();
|
|
for (unsigned i = m_candidates.size() - 1; i > 0; --i) {
|
|
candidate c = m_candidates[i];
|
|
m_candidates[i] = m_candidates[0];
|
|
m_candidates[0] = c;
|
|
sift_down(0, i);
|
|
}
|
|
}
|
|
SASSERT(validate_heap_sort());
|
|
}
|
|
|
|
void lookahead::heapify() {
|
|
unsigned i = 1 + (m_candidates.size() - 2) / 2;
|
|
while(i > 0) {
|
|
sift_down(--i, m_candidates.size());
|
|
}
|
|
}
|
|
|
|
void lookahead::sift_down(unsigned j, unsigned sz) {
|
|
unsigned i = j;
|
|
candidate c = m_candidates[j];
|
|
for (unsigned k = 2 * j + 1; k < sz; i = k, k = 2 * k + 1) {
|
|
// pick smallest child
|
|
if (k + 1 < sz && m_candidates[k].m_rating > m_candidates[k + 1].m_rating) {
|
|
++k;
|
|
}
|
|
if (c.m_rating <= m_candidates[k].m_rating) break;
|
|
m_candidates[i] = m_candidates[k];
|
|
}
|
|
if (i > j) m_candidates[i] = c;
|
|
}
|
|
|
|
/**
|
|
* \brief validate that the result of heap sort sorts the candidates
|
|
* in descending order of their rating.
|
|
*/
|
|
bool lookahead::validate_heap_sort() {
|
|
for (unsigned i = 0; i + 1 < m_candidates.size(); ++i)
|
|
if (m_candidates[i].m_rating < m_candidates[i + 1].m_rating)
|
|
return false;
|
|
return true;
|
|
}
|
|
|
|
double lookahead::init_candidates(unsigned level, bool newbies) {
|
|
m_candidates.reset();
|
|
double sum = 0;
|
|
unsigned skip_candidates = 0;
|
|
bool autarky = get_config().m_lookahead_global_autarky;
|
|
for (bool_var x : m_freevars) {
|
|
SASSERT(is_undef(x));
|
|
if (!m_select_lookahead_vars.empty()) {
|
|
if (m_select_lookahead_vars.contains(x)) {
|
|
if (!autarky || newbies || in_reduced_clause(x)) {
|
|
m_candidates.push_back(candidate(x, m_rating[x]));
|
|
sum += m_rating[x];
|
|
}
|
|
else {
|
|
skip_candidates++;
|
|
}
|
|
}
|
|
}
|
|
else if (newbies || active_prefix(x)) {
|
|
m_candidates.push_back(candidate(x, m_rating[x]));
|
|
sum += m_rating[x];
|
|
}
|
|
}
|
|
TRACE("sat", display_candidates(tout << "sum: " << sum << "\n"););
|
|
if (skip_candidates > 0) {
|
|
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :candidates " << m_candidates.size() << " :skipped " << skip_candidates << ")\n";);
|
|
}
|
|
return sum;
|
|
}
|
|
|
|
|
|
std::ostream& lookahead::display_candidates(std::ostream& out) const {
|
|
for (unsigned i = 0; i < m_candidates.size(); ++i) {
|
|
out << "var: " << m_candidates[i].m_var << " rating: " << m_candidates[i].m_rating << "\n";
|
|
}
|
|
return out;
|
|
}
|
|
|
|
bool lookahead::is_unsat() const {
|
|
for (unsigned idx = 0; idx < m_binary.size(); ++idx) {
|
|
literal l = to_literal(idx);
|
|
for (literal lit : m_binary[idx]) {
|
|
if (is_true(l) && is_false(lit))
|
|
return true;
|
|
}
|
|
}
|
|
// check if there is a clause whose literals are false.
|
|
// every clause is terminated by a null-literal.
|
|
for (nary* n : m_nary_clauses) {
|
|
bool all_false = true;
|
|
for (literal l : *n) {
|
|
all_false &= is_false(l);
|
|
}
|
|
if (all_false) return true;
|
|
}
|
|
// check if there is a ternary whose literals are false.
|
|
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
|
literal lit = to_literal(idx);
|
|
if (is_false(lit)) {
|
|
unsigned sz = m_ternary_count[lit.index()];
|
|
for (binary const& b : m_ternary[lit.index()]) {
|
|
if (sz-- == 0) break;
|
|
if (is_false(b.m_u) && is_false(b.m_v))
|
|
return true;
|
|
}
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool lookahead::is_sat() const {
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
literal_vector const& lits1 = m_binary[l.index()];
|
|
for (literal lit1 : lits1) {
|
|
if (!is_true(lit1)) {
|
|
TRACE("sat", tout << l << " " << lit1 << "\n";);
|
|
return false;
|
|
}
|
|
}
|
|
l.neg();
|
|
literal_vector const& lits2 = m_binary[l.index()];
|
|
for (literal lit2 : lits2) {
|
|
if (!is_true(lit2)) {
|
|
TRACE("sat", tout << l << " " << lit2 << "\n";);
|
|
return false;
|
|
}
|
|
}
|
|
}
|
|
// check if there is a clause whose literals are false.
|
|
// every clause is terminated by a null-literal.
|
|
for (nary * n : m_nary_clauses) {
|
|
bool no_true = true;
|
|
for (literal l : *n) {
|
|
no_true &= !is_true(l);
|
|
}
|
|
if (no_true) return false;
|
|
}
|
|
// check if there is a ternary whose literals are false.
|
|
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
|
literal lit = to_literal(idx);
|
|
if (!is_true(lit)) {
|
|
unsigned sz = m_ternary_count[lit.index()];
|
|
for (binary const& b : m_ternary[lit.index()]) {
|
|
if (sz-- == 0) break;
|
|
if (!is_true(b.m_u) && !is_true(b.m_v))
|
|
return false;
|
|
}
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool lookahead::missed_propagation() const {
|
|
if (inconsistent()) return false;
|
|
for (literal l1 : m_trail) {
|
|
SASSERT(is_true(l1));
|
|
for (literal l2 : m_binary[l1.index()]) {
|
|
VERIFY(is_true(l2));
|
|
if (is_undef(l2)) return true;
|
|
}
|
|
unsigned sz = m_ternary_count[(~l1).index()];
|
|
for (binary b : m_ternary[(~l1).index()]) {
|
|
if (sz-- == 0) break;
|
|
if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) {
|
|
IF_VERBOSE(0, verbose_stream() << b.m_u << " " << b.m_v << "\n"
|
|
<< get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n";);
|
|
UNREACHABLE();
|
|
}
|
|
if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u)))
|
|
return true;
|
|
}
|
|
}
|
|
for (nary * n : m_nary_clauses) {
|
|
if (n->size() == 1 && !is_true(n->get_head())) {
|
|
for (literal lit : *n) {
|
|
VERIFY(!is_undef(lit));
|
|
if (is_undef(lit)) return true;
|
|
}
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool lookahead::missed_conflict() const {
|
|
if (inconsistent()) return false;
|
|
for (literal l1 : m_trail) {
|
|
for (literal l2 : m_binary[l1.index()]) {
|
|
if (is_false(l2))
|
|
return true;
|
|
}
|
|
unsigned sz = m_ternary_count[(~l1).index()];
|
|
for (binary b : m_ternary[(~l1).index()]) {
|
|
if (sz-- == 0) break;
|
|
if ((is_false(b.m_u) && is_false(b.m_v)))
|
|
return true;
|
|
}
|
|
}
|
|
for (nary * n : m_nary_clauses) {
|
|
if (n->size() == 0)
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void lookahead::init_pre_selection(unsigned level) {
|
|
switch (m_config.m_reward_type) {
|
|
case ternary_reward: {
|
|
unsigned max_level = m_config.m_max_hlevel;
|
|
if (level <= 1) {
|
|
ensure_H(2);
|
|
h_scores(m_H[0], m_H[1]);
|
|
for (unsigned j = 0; j < 2; ++j) {
|
|
for (unsigned i = 0; i < 2; ++i) {
|
|
h_scores(m_H[i + 1], m_H[(i + 2) % 3]);
|
|
}
|
|
}
|
|
m_heur = &m_H[1];
|
|
}
|
|
else if (level < max_level) {
|
|
ensure_H(level);
|
|
h_scores(m_H[level-1], m_H[level]);
|
|
m_heur = &m_H[level];
|
|
}
|
|
else {
|
|
ensure_H(max_level);
|
|
h_scores(m_H[max_level-1], m_H[max_level]);
|
|
m_heur = &m_H[max_level];
|
|
}
|
|
break;
|
|
}
|
|
case heule_schur_reward:
|
|
heule_schur_scores();
|
|
break;
|
|
case heule_unit_reward:
|
|
heule_unit_scores();
|
|
break;
|
|
case march_cu_reward:
|
|
march_cu_scores();
|
|
break;
|
|
case unit_literal_reward:
|
|
heule_schur_scores();
|
|
break;
|
|
}
|
|
}
|
|
|
|
void lookahead::heule_schur_scores() {
|
|
if (m_rating_throttle++ % 10 != 0) return;
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
m_rating[l.var()] = heule_schur_score(l) * heule_schur_score(~l);
|
|
}
|
|
}
|
|
|
|
double lookahead::heule_schur_score(literal l) {
|
|
double sum = 0;
|
|
for (literal lit : m_binary[l.index()]) {
|
|
if (is_undef(lit)) sum += literal_occs(lit) / 4.0;
|
|
}
|
|
unsigned sz = m_ternary_count[(~l).index()];
|
|
for (binary const& b : m_ternary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
sum += (literal_occs(b.m_u) + literal_occs(b.m_v)) / 8.0;
|
|
}
|
|
sz = m_nary_count[(~l).index()];
|
|
for (nary * n : m_nary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
double to_add = 0;
|
|
for (literal lit : *n) {
|
|
if (!is_fixed(lit) && lit != ~l) {
|
|
to_add += literal_occs(lit);
|
|
}
|
|
}
|
|
unsigned len = n->size();
|
|
sum += pow(0.5, len) * to_add / len;
|
|
}
|
|
return sum;
|
|
}
|
|
|
|
void lookahead::heule_unit_scores() {
|
|
if (m_rating_throttle++ % 10 != 0) return;
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
m_rating[l.var()] = heule_unit_score(l) * heule_unit_score(~l);
|
|
}
|
|
}
|
|
|
|
double lookahead::heule_unit_score(literal l) {
|
|
double sum = 0;
|
|
for (literal lit : m_binary[l.index()]) {
|
|
if (is_undef(lit)) sum += 0.5;
|
|
}
|
|
sum += 0.25 * m_ternary_count[(~l).index()];
|
|
unsigned sz = m_nary_count[(~l).index()];
|
|
for (nary * n : m_nary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
sum += pow(0.5, n->size());
|
|
}
|
|
return sum;
|
|
}
|
|
|
|
void lookahead::march_cu_scores() {
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
double pos = march_cu_score(l), neg = march_cu_score(~l);
|
|
m_rating[l.var()] = 1024 * pos * neg + pos + neg + 1;
|
|
}
|
|
}
|
|
|
|
double lookahead::march_cu_score(literal l) {
|
|
double sum = 1.0 + literal_big_occs(~l);
|
|
for (literal lit : m_binary[l.index()]) {
|
|
if (is_undef(lit)) sum += literal_big_occs(lit);
|
|
}
|
|
return sum;
|
|
}
|
|
|
|
void lookahead::ensure_H(unsigned level) {
|
|
while (m_H.size() <= level) {
|
|
m_H.push_back(svector<double>());
|
|
m_H.back().resize(m_num_vars * 2, 0);
|
|
}
|
|
}
|
|
|
|
void lookahead::h_scores(svector<double>& h, svector<double>& hp) {
|
|
double sum = 0;
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
sum += h[l.index()] + h[(~l).index()];
|
|
}
|
|
if (sum == 0) sum = 0.0001;
|
|
double factor = 2 * m_freevars.size() / sum;
|
|
double sqfactor = factor * factor;
|
|
double afactor = factor * m_config.m_alpha;
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
double pos = l_score(l, h, factor, sqfactor, afactor);
|
|
double neg = l_score(~l, h, factor, sqfactor, afactor);
|
|
hp[l.index()] = pos;
|
|
hp[(~l).index()] = neg;
|
|
m_rating[l.var()] = pos * neg;
|
|
}
|
|
}
|
|
|
|
double lookahead::l_score(literal l, svector<double> const& h, double factor, double sqfactor, double afactor) {
|
|
double sum = 0, tsum = 0;
|
|
for (literal lit : m_binary[l.index()]) {
|
|
if (is_undef(lit)) sum += h[lit.index()];
|
|
// if (m_freevars.contains(lit.var())) sum += h[lit.index()];
|
|
}
|
|
unsigned sz = m_ternary_count[(~l).index()];
|
|
for (binary const& b : m_ternary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
tsum += h[b.m_u.index()] * h[b.m_v.index()];
|
|
}
|
|
// std::cout << "sum: " << sum << " afactor " << afactor << " sqfactor " << sqfactor << " tsum " << tsum << "\n";
|
|
sum = (double)(0.1 + afactor*sum + sqfactor*tsum);
|
|
// std::cout << "sum: " << sum << " max score " << m_config.m_max_score << "\n";
|
|
return std::min(m_config.m_max_score, sum);
|
|
}
|
|
|
|
// ------------------------------------
|
|
// Implication graph
|
|
// Compute implication ordering and strongly connected components.
|
|
// sat11.w 103 - 114.
|
|
|
|
void lookahead::get_scc() {
|
|
unsigned num_candidates = m_candidates.size();
|
|
init_scc();
|
|
for (unsigned i = 0; i < num_candidates && !inconsistent(); ++i) {
|
|
literal lit(m_candidates[i].m_var, false);
|
|
if (get_rank(lit) == 0) get_scc(lit);
|
|
if (get_rank(~lit) == 0) get_scc(~lit);
|
|
}
|
|
TRACE("sat", display_scc(tout););
|
|
}
|
|
void lookahead::init_scc() {
|
|
inc_bstamp();
|
|
for (unsigned i = 0; i < m_candidates.size(); ++i) {
|
|
literal lit(m_candidates[i].m_var, false);
|
|
init_dfs_info(lit);
|
|
init_dfs_info(~lit);
|
|
}
|
|
for (unsigned i = 0; i < m_candidates.size(); ++i) {
|
|
literal lit(m_candidates[i].m_var, false);
|
|
init_arcs(lit);
|
|
init_arcs(~lit);
|
|
}
|
|
m_rank = 0;
|
|
m_rank_max = UINT_MAX;
|
|
m_active = null_literal;
|
|
m_settled = null_literal;
|
|
TRACE("sat", display_dfs(tout););
|
|
}
|
|
void lookahead::init_dfs_info(literal l) {
|
|
unsigned idx = l.index();
|
|
m_dfs[idx].reset();
|
|
set_bstamp(l);
|
|
}
|
|
// arcs are added in the opposite direction of implications.
|
|
// So for implications l => u we add arcs u -> l
|
|
void lookahead::init_arcs(literal l) {
|
|
literal_vector lits;
|
|
literal_vector const& succ = m_binary[l.index()];
|
|
for (literal u : succ) {
|
|
SASSERT(u != l);
|
|
// l => u
|
|
// NB. u.index() > l.index() iff u.index() > (~l).index().
|
|
// since indices for the same boolean variables occupy
|
|
// two adjacent numbers.
|
|
if (u.index() > l.index() && is_stamped(u) && ~l != u) {
|
|
add_arc(~l, ~u);
|
|
add_arc( u, l);
|
|
}
|
|
}
|
|
for (auto w : m_watches[l.index()]) {
|
|
lits.reset();
|
|
if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) {
|
|
for (literal u : lits) {
|
|
// u is positive in lits, l is negative:
|
|
if (~l != u && u.index() > l.index() && is_stamped(u)) {
|
|
add_arc(~l, ~u);
|
|
add_arc( u, l);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void lookahead::add_arc(literal u, literal v) {
|
|
auto & lst = m_dfs[u.index()].m_next;
|
|
if (lst.empty() || lst.back() != v) lst.push_back(v);
|
|
}
|
|
|
|
void lookahead::get_scc(literal v) {
|
|
TRACE("scc", tout << v << "\n";);
|
|
set_parent(v, null_literal);
|
|
activate_scc(v);
|
|
do {
|
|
literal ll = get_min(v);
|
|
if (has_arc(v)) {
|
|
literal u = pop_arc(v);
|
|
unsigned r = get_rank(u);
|
|
if (r > 0) {
|
|
// u was processed before ll
|
|
if (r < get_rank(ll)) set_min(v, u);
|
|
}
|
|
else {
|
|
// process u in dfs order, add v to dfs stack for u
|
|
set_parent(u, v);
|
|
v = u;
|
|
activate_scc(v);
|
|
}
|
|
}
|
|
else {
|
|
literal u = get_parent(v);
|
|
if (v == ll) {
|
|
found_scc(v);
|
|
}
|
|
else if (get_rank(ll) < get_rank(get_min(u))) {
|
|
set_min(u, ll);
|
|
}
|
|
// walk back in the dfs stack
|
|
v = u;
|
|
}
|
|
}
|
|
while (v != null_literal && !inconsistent());
|
|
}
|
|
|
|
void lookahead::activate_scc(literal l) {
|
|
SASSERT(get_rank(l) == 0);
|
|
set_rank(l, ++m_rank);
|
|
set_link(l, m_active);
|
|
set_min(l, l);
|
|
m_active = l;
|
|
}
|
|
// make v root of the scc equivalence class
|
|
// set vcomp to be the highest rated literal
|
|
void lookahead::found_scc(literal v) {
|
|
literal t = m_active;
|
|
m_active = get_link(v);
|
|
literal best = v;
|
|
double best_rating = get_rating(v);
|
|
set_rank(v, m_rank_max);
|
|
set_link(v, m_settled); m_settled = t;
|
|
while (t != v) {
|
|
if (t == ~v) {
|
|
TRACE("sat", display_scc(tout << "found contradiction during scc search\n"););
|
|
set_conflict();
|
|
break;
|
|
}
|
|
set_rank(t, m_rank_max);
|
|
set_parent(t, v);
|
|
double t_rating = get_rating(t);
|
|
if (t_rating > best_rating) {
|
|
best = t;
|
|
best_rating = t_rating;
|
|
}
|
|
t = get_link(t);
|
|
}
|
|
set_parent(v, v);
|
|
set_vcomp(v, best);
|
|
if (maxed_rank(~v)) {
|
|
set_vcomp(v, ~get_vcomp(get_parent(~v)));
|
|
}
|
|
}
|
|
|
|
std::ostream& lookahead::display_dfs(std::ostream& out) const {
|
|
for (unsigned i = 0; i < m_candidates.size(); ++i) {
|
|
literal l(m_candidates[i].m_var, false);
|
|
display_dfs(out, l);
|
|
display_dfs(out, ~l);
|
|
}
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display_dfs(std::ostream& out, literal l) const {
|
|
arcs const& a1 = get_arcs(l);
|
|
if (!a1.empty()) {
|
|
out << l << " -> " << a1 << "\n";
|
|
}
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display_scc(std::ostream& out) const {
|
|
display_dfs(out);
|
|
for (unsigned i = 0; i < m_candidates.size(); ++i) {
|
|
literal l(m_candidates[i].m_var, false);
|
|
display_scc(out, l);
|
|
display_scc(out, ~l);
|
|
}
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display_scc(std::ostream& out, literal l) const {
|
|
out << l << " := " << get_parent(l)
|
|
<< " min: " << get_min(l)
|
|
<< " rank: " << get_rank(l)
|
|
<< " height: " << get_height(l)
|
|
<< " link: " << get_link(l)
|
|
<< " child: " << get_child(l)
|
|
<< " vcomp: " << get_vcomp(l) << "\n";
|
|
return out;
|
|
}
|
|
|
|
|
|
// ------------------------------------
|
|
// lookahead forest
|
|
// sat11.w 115-121
|
|
|
|
literal lookahead::get_child(literal u) const {
|
|
if (u == null_literal) return m_root_child;
|
|
return m_dfs[u.index()].m_min;
|
|
}
|
|
|
|
void lookahead::set_child(literal v, literal u) {
|
|
if (v == null_literal) m_root_child = u;
|
|
else m_dfs[v.index()].m_min = u;
|
|
}
|
|
|
|
/*
|
|
\brief Assign heights to the nodes.
|
|
Nodes within the same strongly connected component are given the same height.
|
|
The code assumes that m_settled is topologically sorted such that
|
|
1. nodes in the same equivalence class come together
|
|
2. the equivalence class representative is last
|
|
|
|
*/
|
|
void lookahead::find_heights() {
|
|
m_root_child = null_literal;
|
|
literal pp = null_literal;
|
|
unsigned h = 0;
|
|
literal w, uu;
|
|
TRACE("sat",
|
|
for (literal u = m_settled; u != null_literal; u = get_link(u)) {
|
|
tout << u << " ";
|
|
}
|
|
tout << "\n";);
|
|
for (literal u = m_settled; u != null_literal; u = uu) {
|
|
TRACE("sat", tout << "process: " << u << "\n";);
|
|
uu = get_link(u);
|
|
literal p = get_parent(u);
|
|
if (p != pp) {
|
|
// new equivalence class
|
|
h = 0;
|
|
w = null_literal;
|
|
pp = p;
|
|
}
|
|
// traverse nodes in order of implication
|
|
unsigned sz = num_next(~u);
|
|
for (unsigned j = 0; j < sz; ++j) {
|
|
literal v = ~get_next(~u, j);
|
|
TRACE("sat", tout << "child " << v << " link: " << get_link(v) << "\n";);
|
|
literal pv = get_parent(v);
|
|
// skip nodes in same equivalence, they will all be processed
|
|
if (pv == p) continue;
|
|
unsigned hh = get_height(pv);
|
|
// update the maximal height descendant
|
|
if (hh >= h) {
|
|
h = hh + 1;
|
|
w = pv;
|
|
}
|
|
}
|
|
if (p == u) {
|
|
// u is an equivalence class representative
|
|
// it is processed last
|
|
literal v = get_child(w);
|
|
set_height(u, h);
|
|
set_child(u, null_literal);
|
|
set_link(u, v);
|
|
set_child(w, u);
|
|
TRACE("sat", tout << "child(" << w << ") = " << u << " link(" << u << ") = " << v << "\n";);
|
|
}
|
|
}
|
|
TRACE("sat",
|
|
display_forest(tout << "forest: ", get_child(null_literal));
|
|
tout << "\n";
|
|
display_scc(tout); );
|
|
}
|
|
std::ostream& lookahead::display_forest(std::ostream& out, literal l) {
|
|
for (literal u = l; u != null_literal; u = get_link(u)) {
|
|
out << u << " ";
|
|
l = get_child(u);
|
|
if (l != null_literal) {
|
|
out << "(";
|
|
display_forest(out, l);
|
|
out << ") ";
|
|
}
|
|
}
|
|
return out;
|
|
}
|
|
|
|
void lookahead::display_search_string() {
|
|
printf("\r");
|
|
uint64_t q = m_prefix;
|
|
unsigned depth = m_trail_lim.size();
|
|
unsigned d = std::min(63u, depth);
|
|
unsigned new_prefix_length = d;
|
|
for (unsigned i = 0; i <= d; ++i) {
|
|
printf((0 != (q & (1ull << i)))? "1" : "0");
|
|
}
|
|
if (d < depth) {
|
|
printf(" d: %d", depth);
|
|
new_prefix_length += 10;
|
|
}
|
|
for (unsigned i = new_prefix_length; i < m_last_prefix_length; ++i) {
|
|
printf(" ");
|
|
}
|
|
m_last_prefix_length = new_prefix_length;
|
|
fflush(stdout);
|
|
}
|
|
|
|
void lookahead::construct_lookahead_table() {
|
|
literal u = get_child(null_literal), v = null_literal;
|
|
unsigned offset = 0;
|
|
SASSERT(m_lookahead.empty());
|
|
while (u != null_literal) {
|
|
set_rank(u, m_lookahead.size());
|
|
set_lookahead(get_vcomp(u));
|
|
if (null_literal != get_child(u)) {
|
|
set_parent(u, v);
|
|
v = u;
|
|
u = get_child(u);
|
|
}
|
|
else {
|
|
while (true) {
|
|
set_offset(get_rank(u), offset);
|
|
offset += 2;
|
|
set_parent(u, v == null_literal ? v : get_vcomp(v));
|
|
u = get_link(u);
|
|
if (u == null_literal && v != null_literal) {
|
|
u = v;
|
|
v = get_parent(u);
|
|
}
|
|
else {
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
SASSERT(2*m_lookahead.size() == offset);
|
|
TRACE("sat", for (unsigned i = 0; i < m_lookahead.size(); ++i)
|
|
tout << m_lookahead[i].m_lit << " : " << m_lookahead[i].m_offset << "\n";);
|
|
}
|
|
|
|
|
|
|
|
// ------------------------------------
|
|
// initialization
|
|
|
|
void lookahead::init_var(bool_var v) {
|
|
m_binary.push_back(literal_vector());
|
|
m_binary.push_back(literal_vector());
|
|
m_watches.push_back(watch_list());
|
|
m_watches.push_back(watch_list());
|
|
m_ternary.push_back(svector<binary>());
|
|
m_ternary.push_back(svector<binary>());
|
|
m_ternary_count.push_back(0);
|
|
m_ternary_count.push_back(0);
|
|
m_nary.push_back(ptr_vector<nary>());
|
|
m_nary.push_back(ptr_vector<nary>());
|
|
m_nary_count.push_back(0);
|
|
m_nary_count.push_back(0);
|
|
m_bstamp.push_back(0);
|
|
m_bstamp.push_back(0);
|
|
m_stamp.push_back(0);
|
|
m_dfs.push_back(dfs_info());
|
|
m_dfs.push_back(dfs_info());
|
|
m_lits.push_back(lit_info());
|
|
m_lits.push_back(lit_info());
|
|
m_rating.push_back(0);
|
|
m_vprefix.push_back(prefix());
|
|
if (!m_s.was_eliminated(v))
|
|
m_freevars.insert(v);
|
|
}
|
|
|
|
void lookahead::init(bool learned) {
|
|
m_delta_trigger = 0.0;
|
|
m_delta_decrease = 0.0;
|
|
m_config.m_dl_success = 0.8;
|
|
m_inconsistent = false;
|
|
m_qhead = 0;
|
|
m_bstamp_id = 0;
|
|
|
|
for (unsigned i = 0; i < m_num_vars; ++i) {
|
|
init_var(i);
|
|
}
|
|
|
|
// copy binary clauses
|
|
unsigned sz = m_s.m_watches.size();
|
|
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
|
|
literal l = ~to_literal(l_idx);
|
|
if (m_s.was_eliminated(l.var())) continue;
|
|
watch_list const & wlist = m_s.m_watches[l_idx];
|
|
for (auto& w : wlist) {
|
|
if (!w.is_binary_clause())
|
|
continue;
|
|
if (!learned && w.is_learned())
|
|
continue;
|
|
literal l2 = w.get_literal();
|
|
if (l.index() < l2.index() && !m_s.was_eliminated(l2.var()))
|
|
add_binary(l, l2);
|
|
}
|
|
}
|
|
|
|
copy_clauses(m_s.m_clauses, false);
|
|
if (learned) copy_clauses(m_s.m_learned, true);
|
|
|
|
// copy units
|
|
unsigned trail_sz = m_s.init_trail_size();
|
|
for (unsigned i = 0; i < trail_sz; ++i) {
|
|
literal l = m_s.m_trail[i];
|
|
if (!m_s.was_eliminated(l.var())) {
|
|
if (m_s.m_config.m_drat) m_drat.add(l, false);
|
|
assign(l);
|
|
}
|
|
}
|
|
|
|
if (m_s.m_ext) {
|
|
// m_ext = m_s.m_ext->copy(this, learned);
|
|
}
|
|
propagate();
|
|
m_qhead = m_trail.size();
|
|
m_init_freevars = m_freevars.size();
|
|
TRACE("sat", m_s.display(tout); display(tout););
|
|
}
|
|
|
|
void lookahead::copy_clauses(clause_vector const& clauses, bool learned) {
|
|
// copy clauses
|
|
for (clause* cp : clauses) {
|
|
clause& c = *cp;
|
|
if (c.was_removed()) continue;
|
|
// enable when there is a non-ternary reward system.
|
|
bool was_eliminated = false;
|
|
for (unsigned i = 0; !was_eliminated && i < c.size(); ++i) {
|
|
was_eliminated = m_s.was_eliminated(c[i].var());
|
|
}
|
|
if (was_eliminated) continue;
|
|
|
|
switch (c.size()) {
|
|
case 0: set_conflict(); break;
|
|
case 1: assign(c[0]); break;
|
|
case 2: add_binary(c[0],c[1]); break;
|
|
case 3: add_ternary(c[0],c[1],c[2]); break;
|
|
default: if (!learned) add_clause(c); break;
|
|
}
|
|
if (m_s.m_config.m_drat) m_drat.add(c, false);
|
|
}
|
|
}
|
|
|
|
// ------------------------------------
|
|
// search
|
|
|
|
|
|
void lookahead::push(literal lit, unsigned level) {
|
|
SASSERT(m_search_mode == lookahead_mode::searching);
|
|
m_binary_trail_lim.push_back(m_binary_trail.size());
|
|
m_trail_lim.push_back(m_trail.size());
|
|
m_num_tc1_lim.push_back(m_num_tc1);
|
|
m_qhead_lim.push_back(m_qhead);
|
|
scoped_level _sl(*this, level);
|
|
m_assumptions.push_back(~lit);
|
|
assign(lit);
|
|
propagate();
|
|
}
|
|
|
|
void lookahead::pop() {
|
|
SASSERT(!m_assumptions.empty());
|
|
m_assumptions.pop_back();
|
|
m_inconsistent = false;
|
|
SASSERT(m_search_mode == lookahead_mode::searching);
|
|
|
|
// m_freevars only for main search
|
|
// undo assignments
|
|
unsigned old_sz = m_trail_lim.back();
|
|
for (unsigned i = m_trail.size(); i > old_sz; ) {
|
|
--i;
|
|
literal l = m_trail[i];
|
|
set_undef(l);
|
|
TRACE("sat", tout << "inserting free var v" << l.var() << "\n";);
|
|
m_freevars.insert(l.var());
|
|
}
|
|
|
|
m_num_tc1 = m_num_tc1_lim.back();
|
|
m_num_tc1_lim.pop_back();
|
|
|
|
for (unsigned i = m_qhead; i > m_qhead_lim.back(); ) {
|
|
--i;
|
|
restore_ternary(m_trail[i]);
|
|
restore_clauses(m_trail[i]);
|
|
}
|
|
|
|
m_trail.shrink(old_sz); // reset assignment.
|
|
m_trail_lim.pop_back();
|
|
|
|
|
|
// remove local binary clauses
|
|
old_sz = m_binary_trail_lim.back();
|
|
for (unsigned i = m_binary_trail.size(); i > old_sz; ) {
|
|
del_binary(m_binary_trail[--i]);
|
|
}
|
|
m_binary_trail.shrink(old_sz);
|
|
m_binary_trail_lim.pop_back();
|
|
|
|
// reset propagation queue
|
|
m_qhead = m_qhead_lim.back();
|
|
m_qhead_lim.pop_back();
|
|
}
|
|
|
|
bool lookahead::push_lookahead2(literal lit, unsigned level) {
|
|
scoped_level _sl(*this, level);
|
|
SASSERT(m_search_mode == lookahead_mode::lookahead1);
|
|
m_search_mode = lookahead_mode::lookahead2;
|
|
lookahead_backtrack();
|
|
assign(lit);
|
|
propagate();
|
|
bool unsat = inconsistent();
|
|
SASSERT(m_search_mode == lookahead_mode::lookahead2);
|
|
m_search_mode = lookahead_mode::lookahead1;
|
|
m_inconsistent = false;
|
|
return unsat;
|
|
}
|
|
|
|
unsigned lookahead::push_lookahead1(literal lit, unsigned level) {
|
|
SASSERT(m_search_mode == lookahead_mode::searching);
|
|
m_search_mode = lookahead_mode::lookahead1;
|
|
scoped_level _sl(*this, level);
|
|
lookahead_backtrack();
|
|
unsigned old_sz = m_trail.size();
|
|
assign(lit);
|
|
propagate();
|
|
return m_trail.size() - old_sz;
|
|
}
|
|
|
|
void lookahead::pop_lookahead1(literal lit, unsigned num_units) {
|
|
bool unsat = inconsistent();
|
|
SASSERT(m_search_mode == lookahead_mode::lookahead1);
|
|
m_inconsistent = false;
|
|
m_search_mode = lookahead_mode::searching;
|
|
// convert windfalls to binary clauses.
|
|
if (!unsat) {
|
|
literal nlit = ~lit;
|
|
|
|
for (unsigned i = 0; i < m_wstack.size(); ++i) {
|
|
literal l2 = m_wstack[i];
|
|
//update_prefix(~lit);
|
|
//update_prefix(m_wstack[i]);
|
|
TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";);
|
|
// if we use try_add_binary, then this may produce new assignments
|
|
// these assignments get put on m_trail, and they are cleared by
|
|
// lookahead_backtrack.
|
|
add_binary(nlit, l2);
|
|
}
|
|
m_stats.m_windfall_binaries += m_wstack.size();
|
|
}
|
|
switch (m_config.m_reward_type) {
|
|
case unit_literal_reward:
|
|
m_lookahead_reward += num_units;
|
|
break;
|
|
case heule_unit_reward:
|
|
case march_cu_reward:
|
|
case heule_schur_reward:
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
m_wstack.reset();
|
|
}
|
|
|
|
void lookahead::lookahead_backtrack() {
|
|
literal lit = null_literal;
|
|
while (!m_trail.empty() && is_undef((lit = m_trail.back()))) {
|
|
if (m_qhead == m_trail.size()) {
|
|
unsigned sz = m_nary_count[(~lit).index()];
|
|
for (nary* n : m_nary[(~lit).index()]) {
|
|
if (sz-- == 0) break;
|
|
n->inc_size();
|
|
}
|
|
--m_qhead;
|
|
}
|
|
m_trail.pop_back();
|
|
}
|
|
SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back());
|
|
}
|
|
|
|
//
|
|
// The current version is modeled after CDCL SAT solving data-structures.
|
|
// It borrows from the watch list data-structure. The cost tradeoffs are somewhat
|
|
// biased towards CDCL search overheads.
|
|
// If we walk over the positive occurrences of l, then those clauses can be retired so
|
|
// that they don't interfere with calculation of H. Instead of removing clauses from the watch
|
|
// list one can swap them to the "back" and adjust a size indicator of the watch list
|
|
// Only the size indicator needs to be updated on backtracking.
|
|
//
|
|
|
|
class lookahead_literal_occs_fun : public literal_occs_fun {
|
|
lookahead& lh;
|
|
public:
|
|
lookahead_literal_occs_fun(lookahead& lh): lh(lh) {}
|
|
double operator()(literal l) { return lh.literal_occs(l); }
|
|
};
|
|
|
|
// Ternary clause managagement:
|
|
|
|
void lookahead::add_ternary(literal u, literal v, literal w) {
|
|
SASSERT(u != w && u != v && v != w && ~u != w && ~u != v && ~w != v);
|
|
m_ternary[u.index()].push_back(binary(v, w));
|
|
m_ternary[v.index()].push_back(binary(w, u));
|
|
m_ternary[w.index()].push_back(binary(u, v));
|
|
m_ternary_count[u.index()]++;
|
|
m_ternary_count[v.index()]++;
|
|
m_ternary_count[w.index()]++;
|
|
}
|
|
|
|
lbool lookahead::propagate_ternary(literal l1, literal l2) {
|
|
if (is_fixed(l1)) {
|
|
if (is_false(l1)) {
|
|
if (is_false(l2)) {
|
|
TRACE("sat", tout << l1 << " " << l2 << " " << "\n";);
|
|
set_conflict();
|
|
return l_false;
|
|
}
|
|
else if (is_undef(l2)) {
|
|
propagated(l2);
|
|
}
|
|
return l_true;
|
|
}
|
|
else {
|
|
return l_true;
|
|
}
|
|
}
|
|
|
|
if (is_fixed(l2)) {
|
|
if (is_false(l2)) {
|
|
propagated(l1);
|
|
return l_false;
|
|
}
|
|
else {
|
|
return l_true;
|
|
}
|
|
}
|
|
return l_undef;
|
|
}
|
|
|
|
void lookahead::propagate_ternary(literal l) {
|
|
unsigned sz = m_ternary_count[(~l).index()];
|
|
|
|
switch (m_search_mode) {
|
|
case lookahead_mode::searching: {
|
|
|
|
// ternary clauses where l is negative become binary
|
|
for (binary const& b : m_ternary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
// this could create a conflict from propagation, but we complete the transaction.
|
|
TRACE("sat", display(tout););
|
|
literal l1 = b.m_u;
|
|
literal l2 = b.m_v;
|
|
switch (propagate_ternary(l1, l2)) {
|
|
case l_undef:
|
|
try_add_binary(l1, l2);
|
|
break;
|
|
default:
|
|
// propagated or tautology or conflict
|
|
break;
|
|
}
|
|
remove_ternary(l1, l2, ~l);
|
|
remove_ternary(l2, ~l, l1);
|
|
}
|
|
|
|
sz = m_ternary_count[l.index()];
|
|
// ternary clauses where l is positive are tautologies
|
|
for (binary const& b : m_ternary[l.index()]) {
|
|
if (sz-- == 0) break;
|
|
remove_ternary(b.m_u, b.m_v, l);
|
|
remove_ternary(b.m_v, l, b.m_u);
|
|
}
|
|
break;
|
|
}
|
|
case lookahead_mode::lookahead1:
|
|
// this could create a conflict from propagation, but we complete the loop.
|
|
for (binary const& b : m_ternary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
literal l1 = b.m_u;
|
|
literal l2 = b.m_v;
|
|
switch (propagate_ternary(l1, l2)) {
|
|
case l_undef:
|
|
update_binary_clause_reward(l1, l2);
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
}
|
|
break;
|
|
case lookahead2:
|
|
// this could create a conflict from propagation, but we complete the loop.
|
|
for (binary const& b : m_ternary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
propagate_ternary(b.m_u, b.m_v);
|
|
}
|
|
break;
|
|
}
|
|
}
|
|
|
|
void lookahead::remove_ternary(literal l, literal u, literal v) {
|
|
unsigned idx = l.index();
|
|
unsigned sz = m_ternary_count[idx]--;
|
|
auto& tv = m_ternary[idx];
|
|
for (unsigned i = sz; i-- > 0; ) {
|
|
binary const& b = tv[i];
|
|
if (b.m_u == u && b.m_v == v) {
|
|
std::swap(tv[i], tv[sz-1]);
|
|
return;
|
|
}
|
|
}
|
|
UNREACHABLE();
|
|
}
|
|
|
|
void lookahead::restore_ternary(literal l) {
|
|
unsigned sz = m_ternary_count[(~l).index()];
|
|
for (binary const& b : m_ternary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
m_ternary_count[b.m_u.index()]++;
|
|
m_ternary_count[b.m_v.index()]++;
|
|
}
|
|
sz = m_ternary_count[l.index()];
|
|
for (binary const& b : m_ternary[l.index()]) {
|
|
if (sz-- == 0) break;
|
|
m_ternary_count[b.m_u.index()]++;
|
|
m_ternary_count[b.m_v.index()]++;
|
|
}
|
|
}
|
|
|
|
void lookahead::propagate_external(literal l) {
|
|
SASSERT(is_true(l));
|
|
if (!m_s.m_ext || inconsistent()) return;
|
|
watch_list& wlist = m_watches[l.index()];
|
|
watch_list::iterator it = wlist.begin(), it2 = it, end = wlist.end();
|
|
for (; it != end && !inconsistent(); ++it) {
|
|
SASSERT(it->get_kind() == watched::EXT_CONSTRAINT);
|
|
bool keep = m_s.m_ext->propagate(l, it->get_ext_constraint_idx());
|
|
if (m_search_mode == lookahead_mode::lookahead1 && !m_inconsistent) {
|
|
lookahead_literal_occs_fun literal_occs_fn(*this);
|
|
m_lookahead_reward += m_s.m_ext->get_reward(l, it->get_ext_constraint_idx(), literal_occs_fn);
|
|
}
|
|
if (inconsistent()) {
|
|
if (!keep) ++it;
|
|
}
|
|
else if (keep) {
|
|
*it2 = *it;
|
|
it2++;
|
|
}
|
|
}
|
|
for (; it != end; ++it, ++it2) {
|
|
*it2 = *it;
|
|
}
|
|
wlist.set_end(it2);
|
|
}
|
|
|
|
|
|
// new n-ary clause managment
|
|
|
|
void lookahead::add_clause(clause const& c) {
|
|
SASSERT(c.size() > 3);
|
|
void * mem = m_allocator.allocate(nary::get_obj_size(c.size()));
|
|
nary * n = new (mem) nary(c.size(), c.begin());
|
|
m_nary_clauses.push_back(n);
|
|
for (literal l : c) {
|
|
m_nary[l.index()].push_back(n);
|
|
m_nary_count[l.index()]++;
|
|
}
|
|
}
|
|
|
|
|
|
void lookahead::propagate_clauses_searching(literal l) {
|
|
// clauses where l is negative
|
|
unsigned sz = m_nary_count[(~l).index()];
|
|
literal lit;
|
|
SASSERT(m_search_mode == lookahead_mode::searching);
|
|
for (nary* n : m_nary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
unsigned len = n->dec_size();
|
|
if (is_true(n->get_head())) continue;
|
|
if (inconsistent()) continue;
|
|
if (len <= 1) continue; // already processed
|
|
// find the two unassigned literals, if any
|
|
if (len == 2) {
|
|
literal l1 = null_literal;
|
|
literal l2 = null_literal;
|
|
bool found_true = false;
|
|
for (literal lit : *n) {
|
|
if (!is_fixed(lit)) {
|
|
if (l1 == null_literal) {
|
|
l1 = lit;
|
|
}
|
|
else {
|
|
SASSERT(l2 == null_literal);
|
|
l2 = lit;
|
|
break;
|
|
}
|
|
}
|
|
else if (is_true(lit)) {
|
|
n->set_head(lit);
|
|
found_true = true;
|
|
break;
|
|
}
|
|
}
|
|
if (found_true) {
|
|
// skip, the clause will be removed when propagating on 'lit'
|
|
}
|
|
else if (l1 == null_literal) {
|
|
set_conflict();
|
|
}
|
|
else if (l2 == null_literal) {
|
|
// clause may get revisited during propagation, when l2 is true in this clause.
|
|
// m_removed_clauses.push_back(std::make_pair(~l, idx));
|
|
// remove_clause_at(~l, idx);
|
|
propagated(l1);
|
|
}
|
|
else {
|
|
// extract binary clause. A unary or empty clause may get revisited,
|
|
// but we skip it then because it is already handled as a binary clause.
|
|
// m_removed_clauses.push_back(std::make_pair(~l, idx)); // need to restore this clause.
|
|
// remove_clause_at(~l, idx);
|
|
try_add_binary(l1, l2);
|
|
}
|
|
}
|
|
}
|
|
// clauses where l is positive:
|
|
sz = m_nary_count[l.index()];
|
|
for (nary* n : m_nary[l.index()]) {
|
|
if (sz-- == 0) break;
|
|
remove_clause_at(l, *n);
|
|
}
|
|
}
|
|
|
|
void lookahead::propagate_clauses_lookahead(literal l) {
|
|
// clauses where l is negative
|
|
unsigned sz = m_nary_count[(~l).index()];
|
|
SASSERT(m_search_mode == lookahead_mode::lookahead1 ||
|
|
m_search_mode == lookahead_mode::lookahead2);
|
|
|
|
for (nary* n : m_nary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
unsigned nonfixed = n->dec_size();
|
|
// if (is_true(n->get_head())) continue;
|
|
if (inconsistent()) continue;
|
|
if (nonfixed <= 1 && !is_true(n->get_head())) {
|
|
bool found_conflict = true;
|
|
for (literal lit : *n) {
|
|
if (!is_fixed(lit)) {
|
|
propagated(lit);
|
|
found_conflict = false;
|
|
break;
|
|
}
|
|
else if (is_true(lit)) {
|
|
n->set_head(lit);
|
|
found_conflict = false;
|
|
break;
|
|
}
|
|
}
|
|
if (found_conflict) {
|
|
set_conflict();
|
|
continue;
|
|
}
|
|
}
|
|
if (m_search_mode == lookahead_mode::lookahead1) {
|
|
//SASSERT(nonfixed >= 2);
|
|
switch (m_config.m_reward_type) {
|
|
case heule_schur_reward: {
|
|
double to_add = 0;
|
|
for (literal lit : *n) {
|
|
if (!is_fixed(lit)) {
|
|
to_add += literal_occs(lit);
|
|
}
|
|
}
|
|
m_lookahead_reward += pow(0.5, nonfixed) * to_add / nonfixed;
|
|
break;
|
|
}
|
|
case heule_unit_reward:
|
|
m_lookahead_reward += pow(0.5, nonfixed);
|
|
break;
|
|
case march_cu_reward:
|
|
m_lookahead_reward += nonfixed >= 2 ? 3.3 * pow(0.5, nonfixed - 2) : 0.0;
|
|
break;
|
|
case ternary_reward:
|
|
UNREACHABLE();
|
|
break;
|
|
case unit_literal_reward:
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
// clauses where l is positive:
|
|
sz = m_nary_count[l.index()];
|
|
for (nary* n : m_nary[l.index()]) {
|
|
if (sz-- == 0) break;
|
|
if (get_level(l) > get_level(n->get_head())) {
|
|
n->set_head(l);
|
|
}
|
|
}
|
|
}
|
|
|
|
void lookahead::remove_clause_at(literal l, nary& n) {
|
|
for (literal lit : n) {
|
|
if (lit != l) {
|
|
remove_clause(lit, n);
|
|
}
|
|
}
|
|
}
|
|
|
|
void lookahead::remove_clause(literal l, nary& n) {
|
|
ptr_vector<nary>& pclauses = m_nary[l.index()];
|
|
unsigned sz = m_nary_count[l.index()]--;
|
|
for (unsigned i = sz; i > 0; ) {
|
|
--i;
|
|
if (&n == pclauses[i]) {
|
|
std::swap(pclauses[i], pclauses[sz-1]);
|
|
return;
|
|
}
|
|
}
|
|
UNREACHABLE();
|
|
}
|
|
|
|
void lookahead::restore_clauses(literal l) {
|
|
SASSERT(m_search_mode == lookahead_mode::searching);
|
|
// increase the length of clauses where l is negative
|
|
unsigned sz = m_nary_count[(~l).index()];
|
|
for (nary* n : m_nary[(~l).index()]) {
|
|
if (sz-- == 0) break;
|
|
n->inc_size();
|
|
}
|
|
// add idx back to clause list where l is positive
|
|
// add them back in the same order as they were inserted
|
|
// in this way we can check that the clauses are the same.
|
|
sz = m_nary_count[l.index()];
|
|
ptr_vector<nary>& pclauses = m_nary[l.index()];
|
|
for (unsigned i = sz; i-- > 0; ) {
|
|
for (literal lit : *pclauses[i]) {
|
|
if (lit != l) {
|
|
SASSERT(m_nary[lit.index()][m_nary_count[lit.index()]] == pclauses[i]);
|
|
m_nary_count[lit.index()]++;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void lookahead::propagate_clauses(literal l) {
|
|
SASSERT(is_true(l));
|
|
propagate_ternary(l);
|
|
switch (m_search_mode) {
|
|
case lookahead_mode::searching:
|
|
propagate_clauses_searching(l);
|
|
break;
|
|
default:
|
|
propagate_clauses_lookahead(l);
|
|
break;
|
|
}
|
|
propagate_external(l);
|
|
}
|
|
|
|
void lookahead::update_binary_clause_reward(literal l1, literal l2) {
|
|
SASSERT(!is_false(l1));
|
|
SASSERT(!is_false(l2));
|
|
switch (m_config.m_reward_type) {
|
|
case ternary_reward:
|
|
m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()];
|
|
break;
|
|
case heule_schur_reward:
|
|
m_lookahead_reward += (literal_occs(l1) + literal_occs(l2)) / 8.0;
|
|
break;
|
|
case heule_unit_reward:
|
|
m_lookahead_reward += 0.25;
|
|
break;
|
|
case march_cu_reward:
|
|
m_lookahead_reward += 3.3;
|
|
break;
|
|
case unit_literal_reward:
|
|
break;
|
|
}
|
|
}
|
|
|
|
void lookahead::update_nary_clause_reward(clause const& c) {
|
|
if (m_config.m_reward_type == ternary_reward && m_lookahead_reward != 0) {
|
|
return;
|
|
}
|
|
literal const * l_it = c.begin() + 2, *l_end = c.end();
|
|
unsigned sz = 0;
|
|
for (; l_it != l_end; ++l_it) {
|
|
if (is_true(*l_it)) return;
|
|
if (!is_false(*l_it)) ++sz;
|
|
}
|
|
switch (m_config.m_reward_type) {
|
|
case heule_schur_reward: {
|
|
SASSERT(sz > 0);
|
|
double to_add = 0;
|
|
for (literal l : c) {
|
|
if (!is_false(l)) {
|
|
to_add += literal_occs(l);
|
|
}
|
|
}
|
|
m_lookahead_reward += pow(0.5, sz) * to_add / sz;
|
|
break;
|
|
}
|
|
case heule_unit_reward:
|
|
m_lookahead_reward += pow(0.5, sz);
|
|
break;
|
|
case march_cu_reward:
|
|
m_lookahead_reward += 3.3 * pow(0.5, sz - 2);
|
|
break;
|
|
case ternary_reward:
|
|
m_lookahead_reward = (double)0.001;
|
|
break;
|
|
case unit_literal_reward:
|
|
break;
|
|
}
|
|
}
|
|
|
|
// Sum_{ clause C that contains ~l } 1
|
|
// FIXME: counts occurences of ~l; misleading
|
|
double lookahead::literal_occs(literal l) {
|
|
double result = m_binary[l.index()].size();
|
|
result += literal_big_occs(l);
|
|
return result;
|
|
}
|
|
|
|
// Sum_{ clause C that contains ~l such that |C| > 2} 1
|
|
// FIXME: counts occurences of ~l; misleading
|
|
double lookahead::literal_big_occs(literal l) {
|
|
double result = m_nary_count[(~l).index()];
|
|
result += m_ternary_count[(~l).index()];
|
|
return result;
|
|
}
|
|
|
|
void lookahead::propagate_binary(literal l) {
|
|
literal_vector const& lits = m_binary[l.index()];
|
|
TRACE("sat", tout << l << " => " << lits << "\n";);
|
|
for (literal lit : lits) {
|
|
if (inconsistent()) break;
|
|
assign(lit);
|
|
}
|
|
}
|
|
|
|
void lookahead::propagate() {
|
|
unsigned i = m_qhead;
|
|
for (; i < m_trail.size() && !inconsistent(); ++i) {
|
|
literal l = m_trail[i];
|
|
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
|
|
propagate_binary(l);
|
|
}
|
|
while (m_qhead < m_trail.size() && !inconsistent()) {
|
|
propagate_clauses(m_trail[m_qhead++]);
|
|
}
|
|
SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
|
|
//SASSERT(!missed_conflict());
|
|
//VERIFY(!missed_propagation());
|
|
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
|
|
}
|
|
|
|
|
|
void lookahead::compute_lookahead_reward() {
|
|
TRACE("sat", display_lookahead(tout); );
|
|
m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size());
|
|
unsigned base = 2;
|
|
bool change = true;
|
|
literal last_changed = null_literal;
|
|
while (change && !inconsistent()) {
|
|
change = false;
|
|
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
|
|
checkpoint();
|
|
literal lit = m_lookahead[i].m_lit;
|
|
if (lit == last_changed) {
|
|
SASSERT(!change);
|
|
break;
|
|
}
|
|
if (scope_lvl() == 1) {
|
|
IF_VERBOSE(30, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";);
|
|
}
|
|
unsigned level = base + m_lookahead[i].m_offset;
|
|
unsigned dl_lvl = level;
|
|
if (is_fixed_at(lit, c_fixed_truth) || is_true_at(lit, level)) continue;
|
|
bool unsat = false;
|
|
if (is_false_at(lit, level)) {
|
|
unsat = true;
|
|
}
|
|
else {
|
|
TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";);
|
|
reset_lookahead_reward(lit);
|
|
unsigned num_units = push_lookahead1(lit, level);
|
|
update_lookahead_reward(lit, level);
|
|
num_units += do_double(lit, dl_lvl);
|
|
if (dl_lvl > level) {
|
|
base = dl_lvl;
|
|
//SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
|
|
SASSERT(get_level(m_trail.back()) == base);
|
|
}
|
|
unsat = inconsistent();
|
|
pop_lookahead1(lit, num_units);
|
|
}
|
|
// VERIFY(!missed_propagation());
|
|
if (unsat) {
|
|
TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
|
|
lookahead_backtrack();
|
|
assign(~lit);
|
|
propagate();
|
|
change = true;
|
|
last_changed = lit;
|
|
continue;
|
|
}
|
|
// if l was derived from lit and ~lit -> l, then l is a necessary assignment
|
|
literal_vector necessary_lits;
|
|
for (literal l : m_binary[(~lit).index()]) {
|
|
if (is_true_at(l, dl_lvl) && !is_fixed_at(l, c_fixed_truth)) {
|
|
necessary_lits.push_back(l);
|
|
}
|
|
}
|
|
if (!necessary_lits.empty()) {
|
|
change = true;
|
|
last_changed = lit;
|
|
lookahead_backtrack();
|
|
for (literal l : necessary_lits) {
|
|
if (inconsistent()) break;
|
|
assign(l);
|
|
propagate();
|
|
}
|
|
}
|
|
SASSERT(inconsistent() || !is_unsat());
|
|
}
|
|
if (c_fixed_truth - 2 * m_lookahead.size() < base) {
|
|
break;
|
|
}
|
|
base += 2 * m_lookahead.size();
|
|
}
|
|
lookahead_backtrack();
|
|
TRACE("sat", display_lookahead(tout); );
|
|
}
|
|
|
|
literal lookahead::select_literal() {
|
|
literal l = null_literal;
|
|
double h = 0;
|
|
unsigned count = 1;
|
|
for (unsigned i = 0; i < m_lookahead.size(); ++i) {
|
|
literal lit = m_lookahead[i].m_lit;
|
|
if (lit.sign() || !is_undef(lit)) {
|
|
continue;
|
|
}
|
|
double diff1 = get_lookahead_reward(lit), diff2 = get_lookahead_reward(~lit);
|
|
double mixd = mix_diff(diff1, diff2);
|
|
|
|
if (mixd == h) ++count;
|
|
if (mixd > h || (mixd == h && m_s.m_rand(count) == 0)) {
|
|
CTRACE("sat", l != null_literal, tout << lit << " mix diff: " << mixd << "\n";);
|
|
if (mixd > h) count = 1;
|
|
h = mixd;
|
|
l = diff1 < diff2 ? lit : ~lit;
|
|
}
|
|
}
|
|
TRACE("sat", tout << "selected: " << l << "\n";);
|
|
return l;
|
|
}
|
|
|
|
|
|
double lookahead::mix_diff(double l, double r) const {
|
|
switch (m_config.m_reward_type) {
|
|
case ternary_reward: return l + r + (1 << 10) * l * r;
|
|
case heule_schur_reward: return l * r;
|
|
case heule_unit_reward: return l * r;
|
|
case march_cu_reward: return 1024 * (1024 * l * r + l + r);
|
|
case unit_literal_reward: return l * r;
|
|
default: UNREACHABLE(); return l * r;
|
|
}
|
|
}
|
|
|
|
void lookahead::reset_lookahead_reward(literal l) {
|
|
|
|
m_lookahead_reward = 0;
|
|
|
|
// inherit propagation effect from parent.
|
|
literal p = get_parent(l);
|
|
set_lookahead_reward(l, (p == null_literal || is_undef(p) || is_fixed_at(p, c_fixed_truth)) ?
|
|
0 : get_lookahead_reward(p));
|
|
}
|
|
|
|
void lookahead::update_lookahead_reward(literal l, unsigned level) {
|
|
if (m_lookahead_reward != 0) {
|
|
inc_lookahead_reward(l, m_lookahead_reward);
|
|
}
|
|
}
|
|
|
|
unsigned lookahead::do_double(literal l, unsigned& base) {
|
|
unsigned num_units = 0;
|
|
if (!inconsistent() && dl_enabled(l)) {
|
|
if (get_lookahead_reward(l) > m_delta_trigger) {
|
|
if (dl_no_overflow(base)) {
|
|
++m_stats.m_double_lookahead_rounds;
|
|
num_units = double_look(l, base);
|
|
if (!inconsistent()) {
|
|
m_delta_trigger = get_lookahead_reward(l);
|
|
dl_disable(l);
|
|
}
|
|
}
|
|
}
|
|
else {
|
|
SASSERT(m_delta_decrease > 0.0);
|
|
m_delta_trigger *= m_delta_decrease;
|
|
}
|
|
}
|
|
return num_units;
|
|
}
|
|
|
|
unsigned lookahead::double_look(literal l, unsigned& base) {
|
|
SASSERT(!inconsistent());
|
|
SASSERT(dl_no_overflow(base));
|
|
SASSERT(is_fixed_at(l, base));
|
|
base += m_lookahead.size();
|
|
unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
|
|
scoped_level _sl(*this, dl_truth);
|
|
//SASSERT(get_level(m_trail.back()) == dl_truth);
|
|
IF_VERBOSE(3, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
|
|
lookahead_backtrack();
|
|
assign(l);
|
|
propagate();
|
|
unsigned old_sz = m_trail.size();
|
|
bool change = true;
|
|
literal last_changed = null_literal;
|
|
unsigned num_iterations = 0;
|
|
while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) {
|
|
num_iterations++;
|
|
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
|
|
literal lit = m_lookahead[i].m_lit;
|
|
if (lit == last_changed) {
|
|
SASSERT(change == false);
|
|
break;
|
|
}
|
|
unsigned level = base + m_lookahead[i].m_offset;
|
|
if (level + m_lookahead.size() >= dl_truth) {
|
|
change = false;
|
|
break;
|
|
}
|
|
bool unsat = false;
|
|
if (is_false_at(lit, level) && !is_fixed_at(lit, dl_truth)) {
|
|
unsat = true;
|
|
}
|
|
else {
|
|
if (is_fixed_at(lit, level)) continue;
|
|
unsat = push_lookahead2(lit, level);
|
|
}
|
|
if (unsat) {
|
|
TRACE("sat", tout << "unit: " << ~lit << "\n";);
|
|
++m_stats.m_double_lookahead_propagations;
|
|
SASSERT(m_level == dl_truth);
|
|
lookahead_backtrack();
|
|
assign(~lit);
|
|
propagate();
|
|
change = true;
|
|
last_changed = lit;
|
|
m_wstack.push_back(~lit);
|
|
}
|
|
}
|
|
base += 2 * m_lookahead.size();
|
|
SASSERT(dl_truth >= base);
|
|
}
|
|
lookahead_backtrack();
|
|
SASSERT(get_level(m_trail.back()) == dl_truth);
|
|
SASSERT(m_level == dl_truth);
|
|
base = dl_truth;
|
|
return m_trail.size() - old_sz;
|
|
}
|
|
|
|
/**
|
|
\brief check if literal occurs in a non-tautological reduced clause.
|
|
*/
|
|
bool lookahead::in_reduced_clause(bool_var v) {
|
|
return
|
|
in_reduced_clause(literal(v, false)) ||
|
|
in_reduced_clause(literal(v, true));
|
|
}
|
|
|
|
bool lookahead::in_reduced_clause(literal lit) {
|
|
if (lit == null_literal) return true;
|
|
if (m_trail_lim.empty()) return true;
|
|
unsigned sz = m_nary_count[lit.index()];
|
|
for (nary* n : m_nary[lit.index()]) {
|
|
if (sz-- == 0) break;
|
|
if (!n->is_reduced()) continue;
|
|
bool has_true = false;
|
|
for (literal l : *n) {
|
|
if (is_true(l)) {
|
|
has_true = true;
|
|
break;
|
|
}
|
|
}
|
|
if (!has_true) return true;
|
|
}
|
|
|
|
auto const& tv = m_ternary[lit.index()];
|
|
sz = tv.size();
|
|
unsigned i = m_ternary_count[lit.index()];
|
|
for (; i < sz; ++i) {
|
|
binary const& b = tv[i];
|
|
if (!is_true(b.m_u) && !is_true(b.m_v))
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void lookahead::validate_assign(literal l) {
|
|
if (m_s.m_config.m_drat && m_search_mode == lookahead_mode::searching) {
|
|
m_assumptions.push_back(l);
|
|
m_drat.add(m_assumptions);
|
|
m_assumptions.pop_back();
|
|
}
|
|
}
|
|
|
|
void lookahead::assign(literal l) {
|
|
SASSERT(m_level > 0);
|
|
if (is_undef(l)) {
|
|
TRACE("sat", tout << "assign: " << l << " @ " << m_level << " " << m_trail_lim.size() << " " << m_search_mode << "\n";);
|
|
set_true(l);
|
|
SASSERT(m_trail.empty() || get_level(m_trail.back()) >= get_level(l));
|
|
m_trail.push_back(l);
|
|
if (m_search_mode == lookahead_mode::searching) {
|
|
m_stats.m_propagations++;
|
|
TRACE("sat", tout << "removing free var v" << l.var() << "\n";);
|
|
if (l.var() > m_freevars.max_var()) IF_VERBOSE(0, verbose_stream() << "bigger than max-var: " << l << " " << " " << m_freevars.max_var() << "\n";);
|
|
if (!m_freevars.contains(l.var())) IF_VERBOSE(0, verbose_stream() << "does not contain: " << l << " eliminated: " << m_s.was_eliminated(l.var()) << "\n";);
|
|
if (m_freevars.contains(l.var())) { m_freevars.remove(l.var()); }
|
|
validate_assign(l);
|
|
}
|
|
}
|
|
else if (is_false(l)) {
|
|
TRACE("sat", tout << "conflict: " << l << " @ " << m_level << " " << m_search_mode << "\n";);
|
|
SASSERT(!is_true(l));
|
|
validate_assign(l);
|
|
set_conflict();
|
|
}
|
|
}
|
|
|
|
void lookahead::propagated(literal l) {
|
|
assign(l);
|
|
for (unsigned i = m_trail.size()-1; i < m_trail.size() && !inconsistent(); ++i) {
|
|
literal l = m_trail[i];
|
|
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
|
|
propagate_binary(l);
|
|
}
|
|
if (m_search_mode == lookahead_mode::lookahead1) {
|
|
m_wstack.push_back(l);
|
|
}
|
|
}
|
|
|
|
bool lookahead::backtrack(literal_vector& trail) {
|
|
while (inconsistent()) {
|
|
if (trail.empty()) return false;
|
|
pop();
|
|
flip_prefix();
|
|
assign(~trail.back());
|
|
trail.pop_back();
|
|
propagate();
|
|
}
|
|
return true;
|
|
}
|
|
|
|
lbool lookahead::search() {
|
|
m_model.reset();
|
|
scoped_level _sl(*this, c_fixed_truth);
|
|
literal_vector trail;
|
|
m_search_mode = lookahead_mode::searching;
|
|
while (true) {
|
|
TRACE("sat", display(tout););
|
|
inc_istamp();
|
|
checkpoint();
|
|
literal l = choose();
|
|
if (inconsistent()) {
|
|
if (!backtrack(trail)) return l_false;
|
|
continue;
|
|
}
|
|
if (l == null_literal) {
|
|
return l_true;
|
|
}
|
|
TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
|
|
++m_stats.m_decisions;
|
|
IF_VERBOSE(1, display_search_string(););
|
|
push(l, c_fixed_truth);
|
|
trail.push_back(l);
|
|
SASSERT(inconsistent() || !is_unsat());
|
|
}
|
|
}
|
|
|
|
bool lookahead::backtrack(literal_vector& trail, svector<bool> & is_decision) {
|
|
while (inconsistent()) {
|
|
if (trail.empty()) return false;
|
|
if (is_decision.back()) {
|
|
pop();
|
|
trail.back().neg();
|
|
assign(trail.back());
|
|
is_decision.back() = false;
|
|
propagate();
|
|
}
|
|
else {
|
|
trail.pop_back();
|
|
is_decision.pop_back();
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void lookahead::update_cube_statistics(statistics& st) {
|
|
st.update("lh cube cutoffs", m_cube_state.m_cutoffs);
|
|
st.update("lh cube conflicts", m_cube_state.m_conflicts);
|
|
}
|
|
|
|
double lookahead::psat_heur() {
|
|
double h = 0.0;
|
|
for (bool_var x : m_freevars) {
|
|
literal l(x, false);
|
|
for (literal lit : m_binary[l.index()]) {
|
|
h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0;
|
|
}
|
|
for (literal lit : m_binary[(~l).index()]) {
|
|
h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0;
|
|
}
|
|
for (binary b : m_ternary[l.index()]) {
|
|
h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ?
|
|
1.0 / pow(m_config.m_cube_psat_clause_base, 2) :
|
|
0.0;
|
|
}
|
|
for (binary b : m_ternary[(~l).index()]) {
|
|
h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ?
|
|
1.0 / pow(m_config.m_cube_psat_clause_base, 2) :
|
|
0.0;
|
|
}
|
|
}
|
|
for (nary * n : m_nary_clauses) {
|
|
h += 1.0 / pow(m_config.m_cube_psat_clause_base, n->size() - 1);
|
|
}
|
|
h /= pow(m_freevars.size(), m_config.m_cube_psat_var_exp);
|
|
IF_VERBOSE(10, verbose_stream() << "(sat-cube-psat :val " << h << ")\n";);
|
|
return h;
|
|
}
|
|
|
|
lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
|
|
scoped_ext _scoped_ext(*this);
|
|
lits.reset();
|
|
bool is_first = m_cube_state.m_first;
|
|
if (is_first) {
|
|
m_select_lookahead_vars.reset();
|
|
for (auto v : vars) {
|
|
m_select_lookahead_vars.insert(v);
|
|
}
|
|
init_search();
|
|
m_model.reset();
|
|
m_cube_state.m_first = false;
|
|
}
|
|
scoped_level _sl(*this, c_fixed_truth);
|
|
m_search_mode = lookahead_mode::searching;
|
|
unsigned depth = 0;
|
|
// unsigned init_trail = m_trail.size();
|
|
|
|
m_cube_state.reset_stats();
|
|
if (!is_first) {
|
|
goto pick_up_work;
|
|
}
|
|
|
|
while (true) {
|
|
TRACE("sat", display(tout););
|
|
checkpoint();
|
|
inc_istamp();
|
|
if (inconsistent()) {
|
|
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
|
|
m_cube_state.m_freevars_threshold = m_freevars.size();
|
|
m_cube_state.m_psat_threshold = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : dbl_max; // MN. only compute PSAT if enabled
|
|
m_cube_state.inc_conflict();
|
|
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
|
|
continue;
|
|
}
|
|
pick_up_work:
|
|
if (m_cube_state.m_cube.size() >= backtrack_level) {
|
|
IF_VERBOSE(10, verbose_stream() << "(sat-cube :cube: " << m_cube_state.m_cube.size() << " :backtrack_level " << backtrack_level << ")\n";);
|
|
while (m_cube_state.m_cube.size() >= backtrack_level) {
|
|
set_conflict();
|
|
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
|
|
}
|
|
}
|
|
backtrack_level = UINT_MAX;
|
|
depth = m_cube_state.m_cube.size();
|
|
if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) ||
|
|
(m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) ||
|
|
(m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) ||
|
|
(m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) ||
|
|
(m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) {
|
|
double dec = (1.0 - pow(m_config.m_cube_fraction, depth));
|
|
m_cube_state.m_freevars_threshold *= dec;
|
|
m_cube_state.m_psat_threshold *= 2.0 - dec;
|
|
set_conflict();
|
|
m_cube_state.inc_cutoff();
|
|
#if 0
|
|
// return cube of all literals, not just the ones in the main cube
|
|
lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail);
|
|
#else
|
|
lits.append(m_cube_state.m_cube);
|
|
#endif
|
|
vars.reset();
|
|
for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
|
|
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
|
|
return l_undef;
|
|
}
|
|
int prev_nfreevars = m_freevars.size();
|
|
double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : dbl_max; // MN. only compute PSAT if enabled
|
|
literal lit = choose();
|
|
if (inconsistent()) {
|
|
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
|
|
m_cube_state.m_freevars_threshold = prev_nfreevars;
|
|
m_cube_state.m_psat_threshold = prev_psat;
|
|
m_cube_state.inc_conflict();
|
|
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
|
|
continue;
|
|
}
|
|
if (lit == null_literal) {
|
|
vars.reset();
|
|
for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
|
|
return l_true;
|
|
}
|
|
TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);
|
|
++m_stats.m_decisions;
|
|
push(lit, c_fixed_truth);
|
|
m_cube_state.m_cube.push_back(lit);
|
|
m_cube_state.m_is_decision.push_back(true);
|
|
SASSERT(inconsistent() || !is_unsat());
|
|
}
|
|
m_cube_state.reset();
|
|
return l_undef;
|
|
}
|
|
|
|
void lookahead::init_model() {
|
|
m_model.reset();
|
|
for (unsigned i = 0; i < m_num_vars; ++i) {
|
|
lbool val;
|
|
literal lit(i, false);
|
|
if (is_undef(lit)) {
|
|
val = l_undef;
|
|
}
|
|
if (is_true(lit)) {
|
|
val = l_true;
|
|
}
|
|
else {
|
|
val = l_false;
|
|
}
|
|
m_model.push_back(val);
|
|
}
|
|
}
|
|
|
|
std::ostream& lookahead::display_cube(std::ostream& out, literal_vector const& cube) const {
|
|
out << "c";
|
|
for (literal l : cube) {
|
|
out << " " << ~l;
|
|
}
|
|
return out << " 0\n";
|
|
}
|
|
|
|
std::ostream& lookahead::display_binary(std::ostream& out) const {
|
|
for (unsigned i = 0; i < m_binary.size(); ++i) {
|
|
literal_vector const& lits = m_binary[i];
|
|
if (!lits.empty()) {
|
|
out << to_literal(i) << " -> " << lits << "\n";
|
|
}
|
|
}
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display_clauses(std::ostream& out) const {
|
|
for (unsigned idx = 0; idx < m_ternary.size(); ++idx) {
|
|
literal lit = to_literal(idx);
|
|
unsigned sz = m_ternary_count[idx];
|
|
for (binary const& b : m_ternary[idx]) {
|
|
if (sz-- == 0) break;
|
|
if (idx < b.m_u.index() && idx << b.m_v.index()) {
|
|
out << lit << " " << b.m_u << " " << b.m_v << "\n";
|
|
}
|
|
}
|
|
}
|
|
|
|
for (nary * n : m_nary_clauses) {
|
|
for (literal l : *n) out << l << " ";
|
|
out << "\n";
|
|
}
|
|
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display_values(std::ostream& out) const {
|
|
for (literal l : m_trail) {
|
|
out << l << "\n";
|
|
}
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display_lookahead(std::ostream& out) const {
|
|
for (unsigned i = 0; i < m_lookahead.size(); ++i) {
|
|
literal lit = m_lookahead[i].m_lit;
|
|
unsigned offset = m_lookahead[i].m_offset;
|
|
out << lit << "\toffset: " << offset;
|
|
out << (is_undef(lit)?" undef": (is_true(lit) ? " true": " false"));
|
|
out << " lookahead_reward: " << get_lookahead_reward(lit);
|
|
out << "\n";
|
|
}
|
|
return out;
|
|
}
|
|
|
|
void lookahead::init_search() {
|
|
m_search_mode = lookahead_mode::searching;
|
|
scoped_level _sl(*this, c_fixed_truth);
|
|
init(m_s.m_config.m_lookahead_use_learned);
|
|
}
|
|
|
|
void lookahead::checkpoint() {
|
|
if (!m_rlimit.inc()) {
|
|
throw solver_exception(Z3_CANCELED_MSG);
|
|
}
|
|
if (memory::get_allocation_size() > m_s.m_config.m_max_memory) {
|
|
throw solver_exception(Z3_MAX_MEMORY_MSG);
|
|
}
|
|
}
|
|
|
|
literal lookahead::choose() {
|
|
literal l = null_literal;
|
|
while (l == null_literal && !inconsistent()) {
|
|
pre_select();
|
|
if (m_lookahead.empty()) {
|
|
break;
|
|
}
|
|
compute_lookahead_reward();
|
|
if (inconsistent()) {
|
|
break;
|
|
}
|
|
l = select_literal();
|
|
}
|
|
SASSERT(inconsistent() || !is_unsat());
|
|
return l;
|
|
}
|
|
|
|
/**
|
|
\brief simplify set of clauses by extracting units from a lookahead at base level.
|
|
*/
|
|
void lookahead::simplify(bool learned) {
|
|
scoped_ext _scoped_ext(*this);
|
|
SASSERT(m_prefix == 0);
|
|
SASSERT(m_watches.empty());
|
|
m_search_mode = lookahead_mode::searching;
|
|
scoped_level _sl(*this, c_fixed_truth);
|
|
init(learned);
|
|
if (inconsistent()) return;
|
|
inc_istamp();
|
|
choose();
|
|
if (inconsistent()) return;
|
|
SASSERT(m_trail_lim.empty());
|
|
unsigned num_units = 0;
|
|
|
|
for (unsigned i = 0; i < m_trail.size() && !m_s.inconsistent(); ++i) {
|
|
literal lit = m_trail[i];
|
|
if (m_s.value(lit) == l_undef && !m_s.was_eliminated(lit.var())) {
|
|
m_s.assign(lit, justification());
|
|
++num_units;
|
|
}
|
|
}
|
|
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << " :propagations " << m_stats.m_propagations << ")\n";);
|
|
|
|
if (m_s.inconsistent()) return;
|
|
|
|
if (num_units > 0) {
|
|
m_s.propagate_core(false);
|
|
m_s.m_simplifier(false);
|
|
}
|
|
|
|
if (select(0)) {
|
|
get_scc();
|
|
if (!inconsistent()) {
|
|
normalize_parents();
|
|
literal_vector roots;
|
|
bool_var_vector to_elim;
|
|
for (unsigned i = 0; i < m_num_vars; ++i) {
|
|
roots.push_back(literal(i, false));
|
|
}
|
|
for (auto const& c : m_candidates) {
|
|
bool_var v = c.m_var;
|
|
literal q(v, false);
|
|
literal p = get_parent(q);
|
|
if (p != null_literal && p.var() != v && !m_s.is_external(v) &&
|
|
!m_s.was_eliminated(v) && !m_s.was_eliminated(p.var())) {
|
|
to_elim.push_back(v);
|
|
roots[v] = p;
|
|
VERIFY(get_parent(p) == p);
|
|
VERIFY(get_parent(~p) == ~p);
|
|
}
|
|
}
|
|
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";);
|
|
elim_eqs elim(m_s);
|
|
elim(roots, to_elim);
|
|
|
|
if (learned && get_config().m_lookahead_simplify_bca) {
|
|
add_hyper_binary();
|
|
}
|
|
}
|
|
}
|
|
m_lookahead.reset();
|
|
}
|
|
|
|
|
|
/**
|
|
\brief reduction based on binary implication graph
|
|
*/
|
|
|
|
void lookahead::add_hyper_binary() {
|
|
|
|
unsigned num_lits = m_s.num_vars() * 2;
|
|
unsigned num_bins = 0;
|
|
|
|
typedef std::pair<unsigned, unsigned> u_pair;
|
|
hashtable<u_pair, pair_hash<unsigned_hash, unsigned_hash>, default_eq<u_pair> > imp;
|
|
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
|
literal u = get_parent(to_literal(idx));
|
|
if (null_literal != u) {
|
|
for (watched const& w : m_s.m_watches[idx]) {
|
|
if (!w.is_binary_clause()) continue;
|
|
literal v = get_parent(w.get_literal());
|
|
if (null_literal != v) {
|
|
imp.insert(std::make_pair(u.index(), v.index()));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
big big(m_s.m_rand);
|
|
big.init(m_s, true);
|
|
svector<std::pair<literal, literal>> candidates;
|
|
|
|
unsigned_vector bin_size(num_lits);
|
|
for (unsigned idx : m_binary_trail) {
|
|
bin_size[idx]++;
|
|
}
|
|
for (unsigned idx = 0; idx < num_lits; ++idx) {
|
|
literal u = to_literal(idx);
|
|
if (u != get_parent(u)) continue;
|
|
if (m_s.was_eliminated(u.var())) continue;
|
|
literal_vector const& lits = m_binary[idx];
|
|
for (unsigned sz = bin_size[idx]; sz > 0; --sz) {
|
|
literal v = lits[lits.size() - sz];
|
|
if (v == get_parent(v) &&
|
|
!m_s.was_eliminated(v.var()) &&
|
|
!imp.contains(std::make_pair(u.index(), v.index())) &&
|
|
!big.connected(u, v)) {
|
|
candidates.push_back(std::make_pair(u, v));
|
|
}
|
|
}
|
|
}
|
|
|
|
for (unsigned count = 0; count < 5; ++count) {
|
|
big.init(m_s, true);
|
|
unsigned k = 0;
|
|
union_find_default_ctx ufctx;
|
|
union_find<union_find_default_ctx> uf(ufctx);
|
|
for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
|
|
for (unsigned j = 0; j < candidates.size(); ++j) {
|
|
literal u = candidates[j].first;
|
|
literal v = candidates[j].second;
|
|
if (!big.connected(u, v)) {
|
|
if (uf.find(u.index()) != uf.find(v.index())) {
|
|
++num_bins;
|
|
uf.merge(u.index(), v.index());
|
|
uf.merge((~u).index(), (~v).index());
|
|
VERIFY(!m_s.was_eliminated(u.var()));
|
|
VERIFY(!m_s.was_eliminated(v.var()));
|
|
m_s.mk_clause(~u, v, true);
|
|
}
|
|
else {
|
|
candidates[k] = candidates[j];
|
|
++k;
|
|
}
|
|
}
|
|
}
|
|
// std::cout << candidates.size() << " -> " << k << "\n";
|
|
if (k == candidates.size()) break;
|
|
candidates.shrink(k);
|
|
if (k == 0) break;
|
|
}
|
|
|
|
IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << num_bins << ")\n";);
|
|
m_stats.m_bca += num_bins;
|
|
}
|
|
|
|
void lookahead::normalize_parents() {
|
|
literal_vector roots;
|
|
for (unsigned i = 0; i < m_num_vars; ++i) {
|
|
literal lit(i, false);
|
|
roots.push_back(lit);
|
|
roots.push_back(~lit);
|
|
SASSERT(roots[lit.index()] == lit);
|
|
}
|
|
for (auto const& c : m_candidates) {
|
|
bool_var v = c.m_var;
|
|
literal p(v, false);
|
|
literal q = get_parent(p);
|
|
literal r = ~get_parent(~p);
|
|
if (q != r) {
|
|
if (q.var() < r.var()) {
|
|
roots[q.index()] = r;
|
|
}
|
|
else {
|
|
roots[r.index()] = q;
|
|
}
|
|
}
|
|
}
|
|
for (auto const& c : m_candidates) {
|
|
literal p(c.m_var, false);
|
|
literal q = roots[get_parent(p).index()];
|
|
set_parent(p, q);
|
|
set_parent(~p, ~q);
|
|
}
|
|
}
|
|
|
|
std::ostream& lookahead::display_summary(std::ostream& out) const {
|
|
out << "Prefix: " << pp_prefix(m_prefix, m_trail_lim.size()) << "\n";
|
|
out << "Level: " << m_level << "\n";
|
|
out << "Free vars: " << m_freevars.size() << "\n";
|
|
return out;
|
|
}
|
|
|
|
std::ostream& lookahead::display(std::ostream& out) const {
|
|
display_summary(out);
|
|
display_values(out);
|
|
display_binary(out);
|
|
display_clauses(out);
|
|
out << "free vars: ";
|
|
for (bool_var b : m_freevars) out << b << " ";
|
|
out << "\n";
|
|
clause_allocator dummy_allocator;
|
|
for (unsigned i = 0; i < m_watches.size(); ++i) {
|
|
watch_list const& wl = m_watches[i];
|
|
if (!wl.empty()) {
|
|
sat::display_watch_list(out << to_literal(i) << " -> ", dummy_allocator, wl);
|
|
out << "\n";
|
|
}
|
|
}
|
|
return out;
|
|
}
|
|
|
|
model const& lookahead::get_model() {
|
|
if (m_model.empty()) {
|
|
init_model();
|
|
}
|
|
return m_model;
|
|
}
|
|
|
|
void lookahead::init_config() {
|
|
m_config.m_reward_type = m_s.m_config.m_lookahead_reward;
|
|
m_config.m_cube_cutoff = m_s.m_config.m_lookahead_cube_cutoff;
|
|
m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction;
|
|
m_config.m_cube_depth = m_s.m_config.m_lookahead_cube_depth;
|
|
m_config.m_cube_freevars = m_s.m_config.m_lookahead_cube_freevars;
|
|
m_config.m_cube_psat_var_exp = m_s.m_config.m_lookahead_cube_psat_var_exp;
|
|
m_config.m_cube_psat_clause_base = m_s.m_config.m_lookahead_cube_psat_clause_base;
|
|
m_config.m_cube_psat_trigger = m_s.m_config.m_lookahead_cube_psat_trigger;
|
|
}
|
|
|
|
void lookahead::collect_statistics(statistics& st) const {
|
|
st.update("lh bool var", m_vprefix.size());
|
|
// TBD: keep count of ternary and >3-ary clauses.
|
|
st.update("lh bca", m_stats.m_bca);
|
|
st.update("lh add binary", m_stats.m_add_binary);
|
|
st.update("lh del binary", m_stats.m_del_binary);
|
|
st.update("lh propagations", m_stats.m_propagations);
|
|
st.update("lh decisions", m_stats.m_decisions);
|
|
st.update("lh windfalls", m_stats.m_windfall_binaries);
|
|
st.update("lh double lookahead propagations", m_stats.m_double_lookahead_propagations);
|
|
st.update("lh double lookahead rounds", m_stats.m_double_lookahead_rounds);
|
|
}
|
|
|
|
}
|