mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 21:08:46 +00:00
1931 lines
68 KiB
C++
1931 lines
68 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_simplifier.cpp
|
|
|
|
Abstract:
|
|
|
|
SAT simplification procedures that use a "full" occurrence list:
|
|
Subsumption, Blocked Clause Removal, Variable Elimination, ...
|
|
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2011-05-24.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "sat/sat_simplifier.h"
|
|
#include "sat/sat_simplifier_params.hpp"
|
|
#include "sat/sat_solver.h"
|
|
#include "sat/sat_elim_vars.h"
|
|
#include "sat/sat_integrity_checker.h"
|
|
#include "util/stopwatch.h"
|
|
#include "util/trace.h"
|
|
|
|
namespace sat {
|
|
|
|
void use_list::init(unsigned num_vars) {
|
|
m_use_list.reset();
|
|
unsigned num_lits = 2 * num_vars;
|
|
m_use_list.resize(num_lits);
|
|
}
|
|
|
|
void use_list::insert(clause & c) {
|
|
for (literal l : c)
|
|
m_use_list[l.index()].insert(c);
|
|
}
|
|
|
|
void use_list::erase(clause & c) {
|
|
for (literal l : c)
|
|
m_use_list[l.index()].erase(c);
|
|
}
|
|
|
|
void use_list::erase(clause & c, literal l) {
|
|
for (literal l2 : c)
|
|
if (l2 != l)
|
|
m_use_list[l2.index()].erase(c);
|
|
}
|
|
|
|
void use_list::block(clause& c) {
|
|
for (literal l : c)
|
|
m_use_list[l.index()].block(c);
|
|
}
|
|
|
|
void use_list::unblock(clause& c) {
|
|
for (literal l : c)
|
|
m_use_list[l.index()].unblock(c);
|
|
}
|
|
|
|
simplifier::simplifier(solver & _s, params_ref const & p):
|
|
s(_s),
|
|
m_num_calls(0) {
|
|
updt_params(p);
|
|
reset_statistics();
|
|
}
|
|
|
|
simplifier::~simplifier() {
|
|
finalize();
|
|
}
|
|
|
|
inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
|
|
|
|
inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
|
|
|
|
inline bool simplifier::is_external(bool_var v) const {
|
|
return
|
|
s.is_assumption(v) ||
|
|
(s.is_external(v) && s.is_incremental()) ||
|
|
(s.is_external(v) && s.m_ext &&
|
|
(!m_ext_use_list.get(literal(v, false)).empty() ||
|
|
!m_ext_use_list.get(literal(v, true)).empty()));
|
|
}
|
|
|
|
inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); }
|
|
|
|
lbool simplifier::value(bool_var v) const { return s.value(v); }
|
|
|
|
lbool simplifier::value(literal l) const { return s.value(l); }
|
|
|
|
inline void simplifier::checkpoint() { s.checkpoint(); }
|
|
|
|
bool simplifier::single_threaded() const { return s.m_config.m_num_threads == 1; }
|
|
|
|
bool simplifier::bce_enabled() const {
|
|
return
|
|
!m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay &&
|
|
(m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled());
|
|
}
|
|
bool simplifier::acce_enabled() const {
|
|
return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce;
|
|
}
|
|
bool simplifier::cce_enabled() const {
|
|
return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled());
|
|
}
|
|
bool simplifier::abce_enabled() const {
|
|
return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce;
|
|
}
|
|
bool simplifier::bca_enabled() const {
|
|
return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded();
|
|
}
|
|
bool simplifier::elim_vars_bdd_enabled() const {
|
|
return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded();
|
|
}
|
|
bool simplifier::elim_vars_enabled() const {
|
|
return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars && single_threaded();
|
|
}
|
|
|
|
void simplifier::register_clauses(clause_vector & cs) {
|
|
std::stable_sort(cs.begin(), cs.end(), size_lt());
|
|
for (clause* c : cs) {
|
|
if (!c->frozen()) {
|
|
m_use_list.insert(*c);
|
|
if (c->strengthened())
|
|
m_sub_todo.insert(*c);
|
|
}
|
|
}
|
|
}
|
|
|
|
inline void simplifier::remove_clause_core(clause & c) {
|
|
for (literal l : c)
|
|
insert_elim_todo(l.var());
|
|
m_sub_todo.erase(c);
|
|
c.set_removed(true);
|
|
TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
|
|
m_need_cleanup = true;
|
|
}
|
|
|
|
inline void simplifier::remove_clause(clause & c) {
|
|
remove_clause_core(c);
|
|
m_use_list.erase(c);
|
|
}
|
|
|
|
inline void simplifier::remove_clause(clause & c, literal l) {
|
|
remove_clause_core(c);
|
|
m_use_list.erase(c, l);
|
|
}
|
|
|
|
inline void simplifier::block_clause(clause & c) {
|
|
if (m_retain_blocked_clauses) {
|
|
c.block();
|
|
m_use_list.block(c);
|
|
}
|
|
else {
|
|
remove_clause(c);
|
|
}
|
|
|
|
}
|
|
|
|
inline void simplifier::unblock_clause(clause & c) {
|
|
c.unblock();
|
|
m_use_list.unblock(c);
|
|
}
|
|
|
|
inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
|
|
get_wlist(~l1).erase(watched(l2, learned));
|
|
m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
|
|
m_sub_bin_todo.erase(bin_clause(l2, l1, learned));
|
|
}
|
|
|
|
void simplifier::init_visited() {
|
|
m_visited.reset();
|
|
m_visited.resize(2*s.num_vars(), false);
|
|
}
|
|
|
|
void simplifier::finalize() {
|
|
m_use_list.finalize();
|
|
m_sub_todo.finalize();
|
|
m_sub_bin_todo.finalize();
|
|
m_elim_todo.finalize();
|
|
m_visited.finalize();
|
|
m_bs_cs.finalize();
|
|
m_bs_ls.finalize();
|
|
m_ext_use_list.finalize();
|
|
}
|
|
|
|
void simplifier::initialize() {
|
|
m_need_cleanup = false;
|
|
s.m_cleaner(true);
|
|
m_last_sub_trail_sz = s.m_trail.size();
|
|
m_use_list.init(s.num_vars());
|
|
if (s.m_ext) s.m_ext->init_use_list(m_ext_use_list);
|
|
m_sub_todo.reset();
|
|
m_sub_bin_todo.reset();
|
|
m_elim_todo.reset();
|
|
init_visited();
|
|
TRACE("after_cleanup", s.display(tout););
|
|
CASSERT("sat_solver", s.check_invariant());
|
|
}
|
|
|
|
void simplifier::operator()(bool learned) {
|
|
|
|
integrity_checker si(s);
|
|
si.check_watches();
|
|
|
|
if (s.inconsistent())
|
|
return;
|
|
if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
|
|
return;
|
|
|
|
// solver::scoped_disable_checkpoint _scoped_disable_checkpoint(s);
|
|
|
|
initialize();
|
|
|
|
CASSERT("sat_solver", s.check_invariant());
|
|
TRACE("before_simplifier", s.display(tout););
|
|
|
|
s.m_cleaner(true);
|
|
TRACE("after_cleanup", s.display(tout););
|
|
CASSERT("sat_solver", s.check_invariant());
|
|
m_need_cleanup = false;
|
|
m_use_list.init(s.num_vars());
|
|
m_learned_in_use_lists = learned;
|
|
if (learned) {
|
|
register_clauses(s.m_learned);
|
|
}
|
|
register_clauses(s.m_clauses);
|
|
|
|
if (bce_enabled() || abce_enabled() || bca_enabled()) {
|
|
elim_blocked_clauses();
|
|
}
|
|
si.check_watches();
|
|
|
|
if (!learned) {
|
|
m_num_calls++;
|
|
}
|
|
|
|
m_sub_counter = m_subsumption_limit;
|
|
m_elim_counter = m_res_limit;
|
|
m_old_num_elim_vars = m_num_elim_vars;
|
|
|
|
for (bool_var v = 0; v < s.num_vars(); ++v) {
|
|
if (!s.m_eliminated[v] && !is_external(v)) {
|
|
insert_elim_todo(v);
|
|
}
|
|
}
|
|
|
|
do {
|
|
if (m_subsumption)
|
|
subsume();
|
|
if (s.inconsistent())
|
|
return;
|
|
if (!learned && elim_vars_enabled())
|
|
elim_vars();
|
|
if (s.inconsistent())
|
|
return;
|
|
if (!m_subsumption || m_sub_counter < 0)
|
|
break;
|
|
}
|
|
while (!m_sub_todo.empty());
|
|
|
|
bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
|
|
|
|
if (m_need_cleanup || vars_eliminated) {
|
|
TRACE("after_simplifier", tout << "cleanning watches...\n";);
|
|
cleanup_watches();
|
|
cleanup_clauses(s.m_learned, true, vars_eliminated, m_learned_in_use_lists);
|
|
cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
|
|
}
|
|
si.check_watches();
|
|
|
|
CASSERT("sat_solver", s.check_invariant());
|
|
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
|
|
|
|
finalize();
|
|
|
|
si.check_watches();
|
|
}
|
|
|
|
/**
|
|
\brief Eliminate all ternary and clause watches.
|
|
*/
|
|
void simplifier::cleanup_watches() {
|
|
for (watch_list& wlist : s.m_watches) {
|
|
watch_list::iterator it2 = wlist.begin();
|
|
watch_list::iterator itprev = it2;
|
|
watch_list::iterator end2 = wlist.end();
|
|
for (; it2 != end2; ++it2) {
|
|
switch (it2->get_kind()) {
|
|
case watched::TERNARY:
|
|
case watched::CLAUSE:
|
|
// consume
|
|
break;
|
|
default:
|
|
*itprev = *it2;
|
|
itprev++;
|
|
break;
|
|
}
|
|
}
|
|
wlist.set_end(itprev);
|
|
}
|
|
}
|
|
|
|
void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
|
|
TRACE("sat", tout << "cleanup_clauses\n";);
|
|
clause_vector::iterator it = cs.begin();
|
|
clause_vector::iterator it2 = it;
|
|
clause_vector::iterator end = cs.end();
|
|
for (; it != end; ++it) {
|
|
clause & c = *(*it);
|
|
if (c.was_removed()) {
|
|
s.del_clause(c);
|
|
continue;
|
|
}
|
|
|
|
if (learned && vars_eliminated) {
|
|
unsigned sz = c.size();
|
|
unsigned i;
|
|
for (i = 0; i < sz; i++) {
|
|
if (was_eliminated(c[i].var()))
|
|
break;
|
|
}
|
|
if (i < sz) {
|
|
s.del_clause(c);
|
|
continue;
|
|
}
|
|
}
|
|
|
|
if (cleanup_clause(c, in_use_lists)) {
|
|
s.del_clause(c);
|
|
continue;
|
|
}
|
|
unsigned sz = c.size();
|
|
if (sz == 0) {
|
|
s.set_conflict(justification());
|
|
for (; it != end; ++it, ++it2) {
|
|
*it2 = *it;
|
|
++it2;
|
|
}
|
|
break;
|
|
}
|
|
if (sz == 1) {
|
|
s.assign(c[0], justification());
|
|
s.del_clause(c);
|
|
continue;
|
|
}
|
|
if (sz == 2) {
|
|
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
|
s.del_clause(c);
|
|
continue;
|
|
}
|
|
// clause became a problem clause
|
|
if (learned && !c.is_learned()) {
|
|
SASSERT(!c.frozen());
|
|
s.m_clauses.push_back(&c);
|
|
continue;
|
|
}
|
|
*it2 = *it;
|
|
it2++;
|
|
if (!c.frozen()) {
|
|
if (sz == 3)
|
|
s.attach_ter_clause(c);
|
|
else
|
|
s.attach_nary_clause(c);
|
|
if (s.m_config.m_drat) {
|
|
s.m_drat.add(c, true);
|
|
}
|
|
}
|
|
}
|
|
cs.set_end(it2);
|
|
}
|
|
|
|
void simplifier::mark_all_but(clause const & c, literal l1) {
|
|
for (literal l2 : c)
|
|
if (l2 != l1)
|
|
mark_visited(l2);
|
|
}
|
|
|
|
void simplifier::unmark_all(clause const & c) {
|
|
for (literal l : c)
|
|
unmark_visited(l);
|
|
}
|
|
|
|
/**
|
|
\brief Return the variable in c with the minimal number positive+negative occurrences.
|
|
*/
|
|
bool_var simplifier::get_min_occ_var(clause const & c) const {
|
|
literal l_best = null_literal;
|
|
unsigned best = UINT_MAX;
|
|
for (literal l : c) {
|
|
unsigned num = m_use_list.get(l).size() + m_use_list.get(~l).size();
|
|
if (num < best) {
|
|
l_best = l;
|
|
best = num;
|
|
}
|
|
}
|
|
return l_best.var();
|
|
}
|
|
|
|
/**
|
|
If c1 subsumes c2, return true
|
|
If c2 can self subsumed by c1, return true and store the literal that can be removed from c2 in l.
|
|
Otherwise return false
|
|
*/
|
|
bool simplifier::subsumes1(clause const & c1, clause const & c2, literal & l) {
|
|
for (literal lit : c2)
|
|
mark_visited(lit);
|
|
|
|
bool r = true;
|
|
l = null_literal;
|
|
for (literal lit : c1) {
|
|
if (!is_marked(lit)) {
|
|
if (l == null_literal && is_marked(~lit)) {
|
|
l = ~lit;
|
|
}
|
|
else {
|
|
l = null_literal;
|
|
r = false;
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
|
|
for (literal lit : c2)
|
|
unmark_visited(lit);
|
|
return r;
|
|
}
|
|
|
|
/**
|
|
\brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1.
|
|
The collections is populated using the use list of target.
|
|
*/
|
|
void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits,
|
|
literal target) {
|
|
if (c1.is_blocked()) return;
|
|
clause_use_list const & cs = m_use_list.get(target);
|
|
for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
|
|
clause & c2 = it.curr();
|
|
CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";);
|
|
SASSERT(!c2.was_removed());
|
|
if (&c2 != &c1 &&
|
|
c1.size() <= c2.size() &&
|
|
approx_subset(c1.approx(), c2.approx())) {
|
|
m_sub_counter -= c1.size() + c2.size();
|
|
literal l;
|
|
if (subsumes1(c1, c2, l)) {
|
|
out.push_back(&c2);
|
|
out_lits.push_back(l);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1.
|
|
*/
|
|
void simplifier::collect_subsumed1(clause const & c1, clause_vector & out, literal_vector & out_lits) {
|
|
bool_var v = get_min_occ_var(c1);
|
|
collect_subsumed1_core(c1, out, out_lits, literal(v, false));
|
|
collect_subsumed1_core(c1, out, out_lits, literal(v, true));
|
|
}
|
|
|
|
/**
|
|
\brief Perform backward subsumption and self-subsumption resolution using c1.
|
|
*/
|
|
void simplifier::back_subsumption1(clause & c1) {
|
|
m_bs_cs.reset();
|
|
m_bs_ls.reset();
|
|
collect_subsumed1(c1, m_bs_cs, m_bs_ls);
|
|
SASSERT(m_bs_cs.size() == m_bs_ls.size());
|
|
clause_vector::iterator it = m_bs_cs.begin();
|
|
clause_vector::iterator end = m_bs_cs.end();
|
|
literal_vector::iterator l_it = m_bs_ls.begin();
|
|
for (; it != end; ++it, ++l_it) {
|
|
clause & c2 = *(*it);
|
|
if (!c2.was_removed() && !c1.is_blocked() && *l_it == null_literal) {
|
|
// c2 was subsumed
|
|
if (c1.is_learned() && !c2.is_learned())
|
|
c1.unset_learned();
|
|
else if (c1.is_blocked() && !c2.is_learned() && !c2.is_blocked())
|
|
unblock_clause(c1);
|
|
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
|
|
remove_clause(c2);
|
|
m_num_subsumed++;
|
|
}
|
|
else if (!c2.was_removed() && !c1.is_blocked()) {
|
|
// subsumption resolution
|
|
TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";);
|
|
elim_lit(c2, *l_it);
|
|
m_num_sub_res++;
|
|
TRACE("subsumption_resolution", tout << "result: " << c2 << "\n";);
|
|
}
|
|
if (s.inconsistent())
|
|
break;
|
|
}
|
|
}
|
|
|
|
void simplifier::back_subsumption1(literal l1, literal l2, bool learned) {
|
|
m_dummy.set(l1, l2, learned);
|
|
clause & c = *(m_dummy.get());
|
|
back_subsumption1(c);
|
|
}
|
|
|
|
/**
|
|
\brief Return the literal in c with the minimal number of occurrences.
|
|
*/
|
|
literal simplifier::get_min_occ_var0(clause const & c) const {
|
|
literal l_best = null_literal;
|
|
unsigned best = UINT_MAX;
|
|
for (literal l : c) {
|
|
unsigned num = m_use_list.get(l).size();
|
|
if (num < best) {
|
|
l_best = l;
|
|
best = num;
|
|
}
|
|
}
|
|
return l_best;
|
|
}
|
|
|
|
/**
|
|
If c1 subsumes c2, return true
|
|
Otherwise return false
|
|
*/
|
|
bool simplifier::subsumes0(clause const & c1, clause const & c2) {
|
|
for (literal l : c2)
|
|
mark_visited(l);
|
|
|
|
bool r = true;
|
|
for (literal l : c1) {
|
|
if (!is_marked(l)) {
|
|
r = false;
|
|
break;
|
|
}
|
|
}
|
|
|
|
for (literal l : c2)
|
|
unmark_visited(l);
|
|
|
|
return r;
|
|
}
|
|
|
|
/**
|
|
\brief Collect the clauses subsumed by c1 (using the occurrence list of target).
|
|
*/
|
|
void simplifier::collect_subsumed0_core(clause const & c1, clause_vector & out, literal target) {
|
|
if (c1.is_blocked()) return;
|
|
clause_use_list const & cs = m_use_list.get(target);
|
|
clause_use_list::iterator it = cs.mk_iterator();
|
|
for (; !it.at_end(); it.next()) {
|
|
clause & c2 = it.curr();
|
|
SASSERT(!c2.was_removed());
|
|
if (&c2 != &c1 &&
|
|
c1.size() <= c2.size() &&
|
|
approx_subset(c1.approx(), c2.approx())) {
|
|
m_sub_counter -= c1.size() + c2.size();
|
|
if (subsumes0(c1, c2)) {
|
|
out.push_back(&c2);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Collect the clauses subsumed by c1
|
|
*/
|
|
void simplifier::collect_subsumed0(clause const & c1, clause_vector & out) {
|
|
literal l = get_min_occ_var0(c1);
|
|
collect_subsumed0_core(c1, out, l);
|
|
}
|
|
|
|
|
|
/**
|
|
\brief Perform backward subsumption using c1.
|
|
*/
|
|
void simplifier::back_subsumption0(clause & c1) {
|
|
m_bs_cs.reset();
|
|
collect_subsumed0(c1, m_bs_cs);
|
|
for (clause* cp : m_bs_cs) {
|
|
clause & c2 = *cp;
|
|
// c2 was subsumed
|
|
if (c1.is_learned() && !c2.is_learned())
|
|
c1.unset_learned();
|
|
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
|
|
remove_clause(c2);
|
|
m_num_subsumed++;
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Eliminate false literals from c, and update occurrence lists
|
|
|
|
Return true if the clause is satisfied
|
|
*/
|
|
bool simplifier::cleanup_clause(clause & c, bool in_use_list) {
|
|
bool r = false;
|
|
unsigned sz = c.size();
|
|
unsigned j = 0;
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
literal l = c[i];
|
|
switch (value(l)) {
|
|
case l_undef:
|
|
if (i != j) {
|
|
std::swap(c[j], c[i]);
|
|
}
|
|
j++;
|
|
break;
|
|
case l_false:
|
|
m_need_cleanup = true;
|
|
if (in_use_list && !c.frozen()) {
|
|
// Remark: if in_use_list is false, then the given clause was not added to the use lists.
|
|
// Remark: frozen clauses are not added to the use lists.
|
|
m_use_list.get(l).erase_not_removed(c);
|
|
}
|
|
break;
|
|
case l_true:
|
|
r = true;
|
|
if (i != j) {
|
|
std::swap(c[j], c[i]);
|
|
}
|
|
j++;
|
|
break;
|
|
}
|
|
}
|
|
if (j < sz) {
|
|
if (s.m_config.m_drat) s.m_drat.del(c);
|
|
c.shrink(j);
|
|
if (s.m_config.m_drat) s.m_drat.add(c, true);
|
|
}
|
|
return r;
|
|
}
|
|
|
|
/**
|
|
\brief Eliminate false literals from c.
|
|
|
|
Return true if the clause is satisfied
|
|
*/
|
|
bool simplifier::cleanup_clause(literal_vector & c) {
|
|
unsigned sz = c.size();
|
|
unsigned j = 0;
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
literal l = c[i];
|
|
switch (value(l)) {
|
|
case l_undef:
|
|
if (i != j) {
|
|
std::swap(c[j], c[i]);
|
|
}
|
|
j++;
|
|
break;
|
|
case l_false:
|
|
break;
|
|
case l_true:
|
|
return true;
|
|
}
|
|
}
|
|
c.shrink(j);
|
|
return false;
|
|
}
|
|
|
|
inline void simplifier::propagate_unit(literal l) {
|
|
unsigned old_trail_sz = s.m_trail.size();
|
|
s.assign(l, justification());
|
|
s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
|
|
if (s.inconsistent())
|
|
return;
|
|
unsigned new_trail_sz = s.m_trail.size();
|
|
for (unsigned i = old_trail_sz; i < new_trail_sz; i++) {
|
|
literal l = s.m_trail[i];
|
|
// put clauses with literals assigned to false back into todo-list
|
|
for (auto it = m_use_list.get(~l).mk_iterator(); !it.at_end(); it.next()) {
|
|
m_sub_todo.insert(it.curr());
|
|
}
|
|
clause_use_list& cs = m_use_list.get(l);
|
|
for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
|
|
clause & c = it.curr();
|
|
remove_clause(c, l);
|
|
}
|
|
cs.reset();
|
|
}
|
|
}
|
|
|
|
void simplifier::elim_lit(clause & c, literal l) {
|
|
TRACE("elim_lit", tout << "processing: " << c << "\n";);
|
|
m_need_cleanup = true;
|
|
m_num_elim_lits++;
|
|
insert_elim_todo(l.var());
|
|
c.elim(l);
|
|
if (s.m_config.m_drat) s.m_drat.add(c, true);
|
|
// if (s.m_config.m_drat) s.m_drat.del(c0); // can delete previous version
|
|
clause_use_list & occurs = m_use_list.get(l);
|
|
occurs.erase_not_removed(c);
|
|
m_sub_counter -= occurs.size()/2;
|
|
if (cleanup_clause(c, true /* clause is in the use lists */)) {
|
|
// clause was satisfied
|
|
TRACE("elim_lit", tout << "clause was satisfied\n";);
|
|
remove_clause(c);
|
|
return;
|
|
}
|
|
switch (c.size()) {
|
|
case 0:
|
|
TRACE("elim_lit", tout << "clause is empty\n";);
|
|
s.set_conflict(justification());
|
|
return;
|
|
case 1:
|
|
TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
|
|
propagate_unit(c[0]);
|
|
// propagate_unit will delete c.
|
|
// remove_clause(c);
|
|
return;
|
|
case 2:
|
|
TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
|
|
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
|
m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
|
|
remove_clause(c);
|
|
return;
|
|
default:
|
|
TRACE("elim_lit", tout << "result: " << c << "\n";);
|
|
m_sub_todo.insert(c);
|
|
return;
|
|
}
|
|
}
|
|
|
|
bool simplifier::subsume_with_binaries() {
|
|
unsigned init = s.m_rand(); // start in a random place, since subsumption can be aborted
|
|
unsigned num_lits = s.m_watches.size();
|
|
for (unsigned i = 0; i < num_lits; i++) {
|
|
unsigned l_idx = (i + init) % num_lits;
|
|
watch_list & wlist = get_wlist(to_literal(l_idx));
|
|
literal l = ~to_literal(l_idx);
|
|
// should not traverse wlist using iterators, since back_subsumption1 may add new binary clauses there
|
|
for (unsigned j = 0; j < wlist.size(); j++) {
|
|
watched w = wlist[j];
|
|
if (w.is_binary_non_learned_clause()) {
|
|
literal l2 = w.get_literal();
|
|
if (l.index() < l2.index()) {
|
|
m_dummy.set(l, l2, w.is_learned());
|
|
clause & c = *(m_dummy.get());
|
|
back_subsumption1(c);
|
|
if (w.is_learned() && !c.is_learned()) {
|
|
SASSERT(wlist[j] == w);
|
|
TRACE("set_not_learned_bug",
|
|
tout << "marking as not learned: " << l2 << " " << wlist[j].is_learned() << "\n";);
|
|
wlist[j].set_not_learned();
|
|
mark_as_not_learned_core(get_wlist(~l2), l);
|
|
}
|
|
if (s.inconsistent())
|
|
return false;
|
|
}
|
|
}
|
|
}
|
|
if (m_sub_counter < 0)
|
|
break;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void simplifier::mark_as_not_learned_core(watch_list & wlist, literal l2) {
|
|
for (watched & w : wlist) {
|
|
if (w.is_binary_clause() && w.get_literal() == l2 && w.is_learned()) {
|
|
w.set_not_learned();
|
|
return;
|
|
}
|
|
}
|
|
}
|
|
|
|
void simplifier::mark_as_not_learned(literal l1, literal l2) {
|
|
mark_as_not_learned_core(get_wlist(~l1), l2);
|
|
mark_as_not_learned_core(get_wlist(~l2), l1);
|
|
}
|
|
|
|
struct bin_lt {
|
|
bool operator()(watched const & w1, watched const & w2) const {
|
|
if (!w1.is_binary_clause()) return false;
|
|
if (!w2.is_binary_clause()) return true;
|
|
unsigned l1_idx = w1.get_literal().index();
|
|
unsigned l2_idx = w2.get_literal().index();
|
|
if (l1_idx < l2_idx) return true;
|
|
if (l1_idx == l2_idx && !w1.is_learned() && w2.is_learned()) return true;
|
|
return false;
|
|
}
|
|
};
|
|
|
|
/**
|
|
\brief Eliminate duplicated binary clauses.
|
|
*/
|
|
void simplifier::elim_dup_bins() {
|
|
#ifdef _TRACE
|
|
unsigned l_idx = 0;
|
|
#endif
|
|
unsigned elim = 0;
|
|
for (watch_list & wlist : s.m_watches) {
|
|
checkpoint();
|
|
std::stable_sort(wlist.begin(), wlist.end(), bin_lt());
|
|
literal last_lit = null_literal;
|
|
watch_list::iterator it = wlist.begin();
|
|
watch_list::iterator itprev = it;
|
|
watch_list::iterator end = wlist.end();
|
|
for (; it != end; ++it) {
|
|
if (!it->is_binary_clause()) {
|
|
*itprev = *it;
|
|
itprev++;
|
|
continue;
|
|
}
|
|
if (it->get_literal() == last_lit) {
|
|
TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx)
|
|
<< " " << it->get_literal() << "\n";);
|
|
elim++;
|
|
}
|
|
else {
|
|
last_lit = it->get_literal();
|
|
*itprev = *it;
|
|
itprev++;
|
|
}
|
|
}
|
|
wlist.set_end(itprev);
|
|
TRACE_CODE(l_idx++;);
|
|
}
|
|
m_num_subsumed += elim/2; // each binary clause is "eliminated" twice.
|
|
}
|
|
|
|
struct simplifier::subsumption_report {
|
|
simplifier & m_simplifier;
|
|
stopwatch m_watch;
|
|
unsigned m_num_subsumed;
|
|
unsigned m_num_sub_res;
|
|
subsumption_report(simplifier & s):
|
|
m_simplifier(s),
|
|
m_num_subsumed(s.m_num_subsumed),
|
|
m_num_sub_res(s.m_num_sub_res) {
|
|
m_watch.start();
|
|
}
|
|
|
|
~subsumption_report() {
|
|
m_watch.stop();
|
|
IF_VERBOSE(SAT_VB_LVL,
|
|
verbose_stream() << " (sat-subsumer :subsumed "
|
|
<< (m_simplifier.m_num_subsumed - m_num_subsumed)
|
|
<< " :subsumption-resolution " << (m_simplifier.m_num_sub_res - m_num_sub_res)
|
|
<< " :threshold " << m_simplifier.m_sub_counter
|
|
<< mem_stat()
|
|
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
|
|
}
|
|
};
|
|
|
|
void simplifier::subsume() {
|
|
subsumption_report rpt(*this);
|
|
elim_dup_bins();
|
|
subsume_with_binaries();
|
|
TRACE("subsumption_bug", s.display(tout););
|
|
while (true) {
|
|
TRACE("subsumption", tout << "sub_todo size: " << m_sub_todo.size() << "\n";);
|
|
|
|
m_sub_counter -= m_sub_bin_todo.size();
|
|
while (!m_sub_bin_todo.empty()) {
|
|
checkpoint();
|
|
m_dummy.set(m_sub_bin_todo.back());
|
|
m_sub_bin_todo.pop_back();
|
|
clause & c = *(m_dummy.get());
|
|
bool was_learned = c.is_learned();
|
|
back_subsumption1(c);
|
|
if (was_learned && !c.is_learned()) {
|
|
mark_as_not_learned(c[0], c[1]);
|
|
}
|
|
}
|
|
|
|
checkpoint();
|
|
|
|
TRACE("subsumption_bug", s.display(tout););
|
|
|
|
if (m_sub_todo.empty()) {
|
|
m_last_sub_trail_sz = s.m_trail.size();
|
|
break;
|
|
}
|
|
|
|
if (m_sub_counter < 0)
|
|
break;
|
|
|
|
clause & c = m_sub_todo.erase();
|
|
c.unmark_strengthened();
|
|
m_sub_counter--;
|
|
TRACE("subsumption", tout << "next: " << c << "\n";);
|
|
if (s.m_trail.size() > m_last_sub_trail_sz) {
|
|
if (cleanup_clause(c, true /* clause is in the use_lists */)) {
|
|
remove_clause(c);
|
|
continue;
|
|
}
|
|
unsigned sz = c.size();
|
|
if (sz == 0) {
|
|
s.set_conflict(justification());
|
|
return;
|
|
}
|
|
if (sz == 1) {
|
|
propagate_unit(c[0]);
|
|
// propagate_unit will delete c.
|
|
// remove_clause(c);
|
|
continue;
|
|
}
|
|
if (sz == 2) {
|
|
TRACE("subsumption", tout << "clause became binary: " << c << "\n";);
|
|
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
|
m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
|
|
remove_clause(c);
|
|
continue;
|
|
}
|
|
}
|
|
TRACE("subsumption", tout << "using: " << c << "\n";);
|
|
back_subsumption1(c);
|
|
}
|
|
}
|
|
|
|
struct simplifier::blocked_clause_elim {
|
|
class literal_lt {
|
|
use_list const & m_use_list;
|
|
vector<watch_list> const & m_watches;
|
|
public:
|
|
literal_lt(use_list const & l, vector<watch_list> const & ws):m_use_list(l), m_watches(ws) {}
|
|
|
|
unsigned weight(unsigned l_idx) const {
|
|
return 2*m_use_list.get(~to_literal(l_idx)).size() + m_watches[l_idx].size();
|
|
}
|
|
|
|
bool operator()(unsigned l_idx1, unsigned l_idx2) const {
|
|
return weight(l_idx1) < weight(l_idx2);
|
|
}
|
|
};
|
|
|
|
class queue {
|
|
heap<literal_lt> m_queue;
|
|
public:
|
|
queue(use_list const & l, vector<watch_list> const & ws):m_queue(128, literal_lt(l, ws)) {}
|
|
void insert(literal l) {
|
|
unsigned idx = l.index();
|
|
m_queue.reserve(idx + 1);
|
|
SASSERT(!m_queue.contains(idx));
|
|
m_queue.insert(idx);
|
|
}
|
|
void decreased(literal l) {
|
|
unsigned idx = l.index();
|
|
if (m_queue.contains(idx))
|
|
m_queue.decreased(idx);
|
|
else
|
|
m_queue.insert(idx);
|
|
}
|
|
literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
|
|
bool empty() const { return m_queue.empty(); }
|
|
void reset() { m_queue.reset(); }
|
|
};
|
|
|
|
simplifier & s;
|
|
int m_counter;
|
|
model_converter & mc;
|
|
queue m_queue;
|
|
clause_vector m_to_remove;
|
|
|
|
literal_vector m_covered_clause;
|
|
literal_vector m_intersection;
|
|
literal_vector m_new_intersection;
|
|
svector<bool> m_in_intersection;
|
|
sat::model_converter::elim_stackv m_elim_stack;
|
|
unsigned m_ala_qhead;
|
|
|
|
blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
|
|
vector<watch_list> & wlist):
|
|
s(_s),
|
|
m_counter(limit),
|
|
mc(_mc),
|
|
m_queue(l, wlist) {
|
|
m_in_intersection.resize(s.s.num_vars() * 2, false);
|
|
}
|
|
|
|
void insert(literal l) {
|
|
m_queue.insert(l);
|
|
}
|
|
|
|
bool process_var(bool_var v) {
|
|
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
|
|
}
|
|
|
|
void operator()() {
|
|
integrity_checker si(s.s);
|
|
si.check_watches();
|
|
if (s.bce_enabled())
|
|
block_clauses();
|
|
si.check_watches();
|
|
if (s.abce_enabled())
|
|
cce<false>();
|
|
si.check_watches();
|
|
if (s.cce_enabled())
|
|
cce<true>();
|
|
si.check_watches();
|
|
if (s.bca_enabled())
|
|
bca();
|
|
si.check_watches();
|
|
}
|
|
|
|
void block_clauses() {
|
|
insert_queue();
|
|
while (!m_queue.empty() && m_counter >= 0) {
|
|
s.checkpoint();
|
|
process(m_queue.next());
|
|
}
|
|
}
|
|
|
|
void insert_queue() {
|
|
unsigned num_vars = s.s.num_vars();
|
|
for (bool_var v = 0; v < num_vars; v++) {
|
|
if (process_var(v)) {
|
|
insert(literal(v, false));
|
|
insert(literal(v, true));
|
|
}
|
|
}
|
|
}
|
|
|
|
void process(literal l) {
|
|
TRACE("blocked_clause", tout << "processing: " << l << "\n";);
|
|
if (!process_var(l.var())) {
|
|
return;
|
|
}
|
|
integrity_checker si(s.s);
|
|
//si.check_watches();
|
|
process_clauses(l);
|
|
process_binary(l);
|
|
//si.check_watches();
|
|
}
|
|
|
|
void process_binary(literal l) {
|
|
model_converter::entry* new_entry = 0;
|
|
watch_list & wlist = s.get_wlist(~l);
|
|
m_counter -= wlist.size();
|
|
watch_list::iterator it = wlist.begin();
|
|
watch_list::iterator it2 = it;
|
|
watch_list::iterator end = wlist.end();
|
|
|
|
for (; it != end; ++it) {
|
|
if (!it->is_binary_non_learned_clause()) {
|
|
*it2 = *it; it2++;
|
|
continue;
|
|
}
|
|
literal l2 = it->get_literal();
|
|
s.mark_visited(l2);
|
|
if (all_tautology(l)) {
|
|
block_binary(it, l, new_entry);
|
|
s.m_num_blocked_clauses++;
|
|
}
|
|
else {
|
|
*it2 = *it; it2++;
|
|
}
|
|
s.unmark_visited(l2);
|
|
}
|
|
wlist.set_end(it2);
|
|
}
|
|
|
|
void process_clauses(literal l) {
|
|
model_converter::entry* new_entry = 0;
|
|
m_to_remove.reset();
|
|
clause_use_list & occs = s.m_use_list.get(l);
|
|
clause_use_list::iterator it = occs.mk_iterator();
|
|
for (; !it.at_end(); it.next()) {
|
|
clause & c = it.curr();
|
|
if (c.is_blocked()) continue;
|
|
m_counter -= c.size();
|
|
SASSERT(c.contains(l));
|
|
s.mark_all_but(c, l);
|
|
if (all_tautology(l)) {
|
|
block_clause(c, l, new_entry);
|
|
s.m_num_blocked_clauses++;
|
|
}
|
|
s.unmark_all(c);
|
|
}
|
|
for (clause* c : m_to_remove)
|
|
s.block_clause(*c);
|
|
}
|
|
|
|
void reset_intersection() {
|
|
for (literal l : m_intersection) m_in_intersection[l.index()] = false;
|
|
m_intersection.reset();
|
|
}
|
|
|
|
void add_intersection(literal lit) {
|
|
m_intersection.push_back(lit);
|
|
m_in_intersection[lit.index()] = true;
|
|
}
|
|
|
|
|
|
|
|
//
|
|
// Resolve intersection
|
|
// Find literals that are in the intersection of all resolvents with l.
|
|
//
|
|
bool resolution_intersection(literal l, bool adding) {
|
|
if (!process_var(l.var())) return false;
|
|
bool first = true;
|
|
reset_intersection();
|
|
for (watched & w : s.get_wlist(l)) {
|
|
// when adding a blocked clause, then all non-learned clauses have to be considered for the
|
|
// resolution intersection.
|
|
bool process_bin = adding ? w.is_binary_clause() : w.is_binary_non_learned_clause();
|
|
if (process_bin) {
|
|
literal lit = w.get_literal();
|
|
if (s.is_marked(~lit) && lit != ~l) {
|
|
continue; // tautology
|
|
}
|
|
if (!first || s.is_marked(lit)) {
|
|
reset_intersection();
|
|
return false; // intersection is empty or does not add anything new.
|
|
}
|
|
first = false;
|
|
SASSERT(m_intersection.empty());
|
|
add_intersection(lit);
|
|
}
|
|
}
|
|
clause_use_list & neg_occs = s.m_use_list.get(~l);
|
|
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
|
|
bool tautology = false;
|
|
clause & c = it.curr();
|
|
if (c.is_blocked() && !adding) continue;
|
|
for (literal lit : c) {
|
|
if (s.is_marked(~lit) && lit != ~l) {
|
|
tautology = true;
|
|
break;
|
|
}
|
|
}
|
|
if (!tautology) {
|
|
if (first) {
|
|
for (literal lit : c)
|
|
if (lit != ~l && !s.is_marked(lit))
|
|
add_intersection(lit);
|
|
first = false;
|
|
}
|
|
else {
|
|
m_new_intersection.reset();
|
|
for (literal lit : c)
|
|
if (m_in_intersection[lit.index()])
|
|
m_new_intersection.push_back(lit);
|
|
reset_intersection();
|
|
for (literal lit : m_new_intersection)
|
|
add_intersection(lit);
|
|
}
|
|
if (m_intersection.empty())
|
|
return false;
|
|
}
|
|
}
|
|
return first;
|
|
}
|
|
|
|
bool check_abce_tautology(literal l) {
|
|
if (!process_var(l.var())) return false;
|
|
for (watched & w : s.get_wlist(l)) {
|
|
if (w.is_binary_non_learned_clause()) {
|
|
literal lit = w.get_literal();
|
|
if (!s.is_marked(~lit) || lit == ~l) return false;
|
|
}
|
|
}
|
|
clause_use_list & neg_occs = s.m_use_list.get(~l);
|
|
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
|
|
clause & c = it.curr();
|
|
if (c.is_blocked()) continue;
|
|
bool tautology = false;
|
|
for (literal lit : c) {
|
|
if (s.is_marked(~lit) && lit != ~l) {
|
|
tautology = true;
|
|
break;
|
|
}
|
|
}
|
|
if (!tautology) return false;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
/*
|
|
* C \/ l l \/ lit
|
|
* -------------------
|
|
* C \/ l \/ ~lit
|
|
*/
|
|
void add_ala() {
|
|
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
|
|
literal l = m_covered_clause[m_ala_qhead];
|
|
for (watched & w : s.get_wlist(~l)) {
|
|
if (w.is_binary_non_learned_clause()) {
|
|
literal lit = w.get_literal();
|
|
if (!s.is_marked(lit) && !s.is_marked(~lit)) {
|
|
m_covered_clause.push_back(~lit);
|
|
s.mark_visited(~lit);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
/*
|
|
* C \/ l ~l \/ lit \/ D_i for i = 1...N all the clauses that have ~l
|
|
* -------------------------
|
|
* C \/ l \/ lit
|
|
*
|
|
*
|
|
*/
|
|
bool add_cla(literal& blocked) {
|
|
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
|
|
if (resolution_intersection(m_covered_clause[i], false)) {
|
|
blocked = m_covered_clause[i];
|
|
return true;
|
|
}
|
|
if (!m_intersection.empty()) {
|
|
m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
|
|
}
|
|
for (literal l : m_intersection) {
|
|
if (!s.is_marked(l)) {
|
|
s.mark_visited(l);
|
|
m_covered_clause.push_back(l);
|
|
}
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool above_threshold(unsigned sz0) const {
|
|
return sz0 * 10 < m_covered_clause.size();
|
|
}
|
|
|
|
template<bool use_ri>
|
|
bool cla(literal& blocked, model_converter::kind& k) {
|
|
bool is_tautology = false;
|
|
for (literal l : m_covered_clause) s.mark_visited(l);
|
|
unsigned num_iterations = 0, sz;
|
|
m_elim_stack.reset();
|
|
m_ala_qhead = 0;
|
|
k = model_converter::CCE;
|
|
unsigned sz0 = m_covered_clause.size();
|
|
|
|
/*
|
|
* For blocked clause elimination with asymmetric literal addition (ABCE)
|
|
* it suffices to check if one of the original
|
|
* literals in the clause is blocked modulo the additional literals added to the clause.
|
|
* So we record sz0, the original set of literals in the clause, mark additional literals,
|
|
* and then check if any of the first sz0 literals are blocked.
|
|
*/
|
|
if (s.abce_enabled() && !use_ri) {
|
|
add_ala();
|
|
for (unsigned i = 0; i < sz0; ++i) {
|
|
if (check_abce_tautology(m_covered_clause[i])) {
|
|
blocked = m_covered_clause[i];
|
|
is_tautology = true;
|
|
break;
|
|
}
|
|
}
|
|
k = model_converter::BLOCK_LIT; // actually ABCE
|
|
for (literal l : m_covered_clause) s.unmark_visited(l);
|
|
m_covered_clause.shrink(sz0);
|
|
return is_tautology;
|
|
}
|
|
|
|
/*
|
|
* For CCE we add the resolution intersection while checking if the clause becomes a tautology.
|
|
* For ACCE, in addition, we add literals.
|
|
*/
|
|
do {
|
|
do {
|
|
if (above_threshold(sz0)) break;
|
|
++num_iterations;
|
|
sz = m_covered_clause.size();
|
|
is_tautology = add_cla(blocked);
|
|
}
|
|
while (m_covered_clause.size() > sz && !is_tautology);
|
|
if (above_threshold(sz0)) break;
|
|
if (s.acce_enabled() && !is_tautology) {
|
|
sz = m_covered_clause.size();
|
|
add_ala();
|
|
k = model_converter::ACCE;
|
|
}
|
|
}
|
|
while (m_covered_clause.size() > sz && !is_tautology);
|
|
// if (is_tautology) std::cout << num_iterations << " " << m_covered_clause.size() << " " << sz0 << " " << is_tautology << " " << m_elim_stack.size() << "\n";
|
|
for (literal l : m_covered_clause) s.unmark_visited(l);
|
|
return is_tautology && !above_threshold(sz0);
|
|
}
|
|
|
|
// perform covered clause elimination.
|
|
// first extract the covered literal addition (CLA).
|
|
// then check whether the CLA is blocked.
|
|
template<bool use_ri>
|
|
bool cce(clause& c, literal& blocked, model_converter::kind& k) {
|
|
m_covered_clause.reset();
|
|
for (literal l : c) m_covered_clause.push_back(l);
|
|
return cla<use_ri>(blocked, k);
|
|
}
|
|
|
|
template<bool use_ri>
|
|
bool cce(literal l1, literal l2, literal& blocked, model_converter::kind& k) {
|
|
m_covered_clause.reset();
|
|
m_covered_clause.push_back(l1);
|
|
m_covered_clause.push_back(l2);
|
|
return cla<use_ri>(blocked, k);
|
|
}
|
|
|
|
template<bool use_ri>
|
|
void cce() {
|
|
insert_queue();
|
|
cce_clauses<use_ri>();
|
|
cce_binary<use_ri>();
|
|
}
|
|
|
|
template<bool use_ri>
|
|
void cce_binary() {
|
|
while (!m_queue.empty() && m_counter >= 0) {
|
|
s.checkpoint();
|
|
process_cce_binary<use_ri>(m_queue.next());
|
|
}
|
|
}
|
|
|
|
template<bool use_ri>
|
|
void process_cce_binary(literal l) {
|
|
literal blocked = null_literal;
|
|
watch_list & wlist = s.get_wlist(~l);
|
|
m_counter -= wlist.size();
|
|
watch_list::iterator it = wlist.begin();
|
|
watch_list::iterator it2 = it;
|
|
watch_list::iterator end = wlist.end();
|
|
model_converter::kind k;
|
|
for (; it != end; ++it) {
|
|
if (!it->is_binary_non_learned_clause()) {
|
|
*it2 = *it;
|
|
it2++;
|
|
continue;
|
|
}
|
|
literal l2 = it->get_literal();
|
|
if (cce<use_ri>(l, l2, blocked, k)) {
|
|
block_covered_binary(it, l, blocked, k);
|
|
s.m_num_covered_clauses++;
|
|
}
|
|
else {
|
|
*it2 = *it;
|
|
it2++;
|
|
}
|
|
}
|
|
wlist.set_end(it2);
|
|
}
|
|
|
|
|
|
template<bool use_ri>
|
|
void cce_clauses() {
|
|
m_to_remove.reset();
|
|
literal blocked;
|
|
model_converter::kind k;
|
|
for (clause* cp : s.s.m_clauses) {
|
|
clause& c = *cp;
|
|
if (!c.was_removed() && !c.is_blocked() && cce<use_ri>(c, blocked, k)) {
|
|
block_covered_clause(c, blocked, k);
|
|
s.m_num_covered_clauses++;
|
|
}
|
|
}
|
|
for (clause* c : m_to_remove) {
|
|
s.block_clause(*c);
|
|
}
|
|
m_to_remove.reset();
|
|
}
|
|
|
|
|
|
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
|
|
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
|
|
//VERIFY(!s.is_external(l));
|
|
if (new_entry == 0)
|
|
new_entry = &(mc.mk(k, l.var()));
|
|
m_to_remove.push_back(&c);
|
|
for (literal lit : c) {
|
|
if (lit != l && process_var(lit.var())) {
|
|
m_queue.decreased(~lit);
|
|
}
|
|
}
|
|
}
|
|
|
|
void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
|
|
SASSERT(!s.is_external(l.var()));
|
|
prepare_block_clause(c, l, new_entry, model_converter::BLOCK_LIT);
|
|
mc.insert(*new_entry, c);
|
|
}
|
|
|
|
void block_covered_clause(clause& c, literal l, model_converter::kind k) {
|
|
SASSERT(!s.is_external(l.var()));
|
|
model_converter::entry * new_entry = 0;
|
|
prepare_block_clause(c, l, new_entry, k);
|
|
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
|
}
|
|
|
|
void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
|
|
SASSERT(!s.is_external(blocked));
|
|
if (new_entry == 0)
|
|
new_entry = &(mc.mk(k, blocked.var()));
|
|
literal l2 = it->get_literal();
|
|
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
|
|
s.remove_bin_clause_half(l2, l1, it->is_learned());
|
|
m_queue.decreased(~l2);
|
|
}
|
|
|
|
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
|
|
literal l2 = it->get_literal();
|
|
prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT);
|
|
mc.insert(*new_entry, l, l2);
|
|
}
|
|
|
|
void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) {
|
|
model_converter::entry * new_entry = 0;
|
|
prepare_block_binary(it, l, blocked, new_entry, k);
|
|
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
|
}
|
|
|
|
void bca() {
|
|
m_queue.reset();
|
|
insert_queue();
|
|
while (!m_queue.empty() && m_counter >= 0) {
|
|
s.checkpoint();
|
|
bca(m_queue.next());
|
|
}
|
|
}
|
|
|
|
/*
|
|
\brief blocked binary clause addition for literal l
|
|
Let RI be the resolution intersection with l, e.g, RI are the literals
|
|
that are in all clauses of the form ~l \/ C.
|
|
If RI is non-empty, then let l' be a literal in RI.
|
|
Then the following binary clause is blocked: l \/ ~l'
|
|
*/
|
|
void bca(literal l) {
|
|
if (resolution_intersection(l, true)) {
|
|
// this literal is pure.
|
|
return;
|
|
}
|
|
for (literal l2 : m_intersection) {
|
|
l2.neg();
|
|
watched* w = find_binary_watch(s.get_wlist(~l), l2);
|
|
if (!w) {
|
|
IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
|
|
s.get_wlist(~l).push_back(watched(l2, true));
|
|
VERIFY(!find_binary_watch(s.get_wlist(~l2), l));
|
|
s.get_wlist(~l2).push_back(watched(l, true));
|
|
++s.m_num_bca;
|
|
}
|
|
}
|
|
}
|
|
|
|
bool all_tautology(literal l) {
|
|
watch_list & wlist = s.get_wlist(l);
|
|
m_counter -= wlist.size();
|
|
for (auto const& w : wlist) {
|
|
if (w.is_binary_non_learned_clause() &&
|
|
!s.is_marked(~w.get_literal()))
|
|
return false;
|
|
}
|
|
|
|
clause_use_list & neg_occs = s.m_use_list.get(~l);
|
|
clause_use_list::iterator it = neg_occs.mk_iterator();
|
|
for (; !it.at_end(); it.next()) {
|
|
clause & c = it.curr();
|
|
if (c.is_blocked()) continue;
|
|
m_counter -= c.size();
|
|
unsigned sz = c.size();
|
|
unsigned i;
|
|
for (i = 0; i < sz; i++) {
|
|
if (s.is_marked(~c[i]))
|
|
break;
|
|
}
|
|
if (i == sz)
|
|
return false;
|
|
}
|
|
|
|
if (s.s.m_ext) {
|
|
ext_constraint_list const& ext_list = s.m_ext_use_list.get(~l);
|
|
for (ext_constraint_idx idx : ext_list) {
|
|
if (!s.s.m_ext->is_blocked(l, idx)) {
|
|
return false;
|
|
}
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
};
|
|
|
|
struct simplifier::blocked_cls_report {
|
|
simplifier & m_simplifier;
|
|
stopwatch m_watch;
|
|
unsigned m_num_blocked_clauses;
|
|
unsigned m_num_covered_clauses;
|
|
unsigned m_num_added_clauses;
|
|
blocked_cls_report(simplifier & s):
|
|
m_simplifier(s),
|
|
m_num_blocked_clauses(s.m_num_blocked_clauses),
|
|
m_num_covered_clauses(s.m_num_covered_clauses),
|
|
m_num_added_clauses(s.m_num_bca) {
|
|
m_watch.start();
|
|
}
|
|
|
|
~blocked_cls_report() {
|
|
m_watch.stop();
|
|
IF_VERBOSE(SAT_VB_LVL,
|
|
verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
|
|
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
|
|
<< " :elim-covered-clauses "
|
|
<< (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
|
|
<< " :added-clauses "
|
|
<< (m_simplifier.m_num_bca - m_num_added_clauses)
|
|
<< mem_stat()
|
|
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
|
|
}
|
|
};
|
|
|
|
void simplifier::elim_blocked_clauses() {
|
|
TRACE("blocked_clause_bug", tout << "trail: " << s.m_trail.size() << "\n"; s.display_watches(tout); s.display(tout););
|
|
blocked_cls_report rpt(*this);
|
|
blocked_clause_elim elim(*this, m_blocked_clause_limit, s.m_mc, m_use_list, s.m_watches);
|
|
elim();
|
|
}
|
|
|
|
unsigned simplifier::get_num_unblocked_bin(literal l) const {
|
|
unsigned r = 0;
|
|
watch_list const & wlist = get_wlist(~l);
|
|
for (auto & w : wlist) {
|
|
if (w.is_binary_non_learned_clause())
|
|
r++;
|
|
}
|
|
return r;
|
|
}
|
|
|
|
unsigned simplifier::get_to_elim_cost(bool_var v) const {
|
|
literal pos_l(v, false);
|
|
literal neg_l(v, true);
|
|
unsigned num_pos = m_use_list.get(pos_l).size();
|
|
unsigned num_neg = m_use_list.get(neg_l).size();
|
|
unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
|
|
unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
|
|
unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
|
|
CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
|
|
<< " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
|
|
return cost;
|
|
}
|
|
|
|
typedef std::pair<bool_var, unsigned> bool_var_and_cost;
|
|
|
|
struct bool_var_and_cost_lt {
|
|
bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; }
|
|
};
|
|
|
|
void simplifier::order_vars_for_elim(bool_var_vector & r) {
|
|
svector<bool_var_and_cost> tmp;
|
|
for (bool_var v : m_elim_todo) {
|
|
if (is_external(v))
|
|
continue;
|
|
if (was_eliminated(v))
|
|
continue;
|
|
if (value(v) != l_undef)
|
|
continue;
|
|
unsigned c = get_to_elim_cost(v);
|
|
tmp.push_back(bool_var_and_cost(v, c));
|
|
}
|
|
m_elim_todo.reset();
|
|
std::stable_sort(tmp.begin(), tmp.end(), bool_var_and_cost_lt());
|
|
TRACE("elim_vars",
|
|
for (auto& p : tmp) tout << "(" << p.first << ", " << p.second << ") ";
|
|
tout << "\n";);
|
|
for (auto& p : tmp)
|
|
r.push_back(p.first);
|
|
}
|
|
|
|
/**
|
|
\brief Collect clauses and binary clauses containing l.
|
|
*/
|
|
void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
|
|
clause_use_list const & cs = m_use_list.get(l);
|
|
for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
|
|
if (!it.curr().is_blocked()) {
|
|
r.push_back(clause_wrapper(it.curr()));
|
|
SASSERT(r.back().size() == it.curr().size());
|
|
}
|
|
}
|
|
|
|
watch_list & wlist = get_wlist(~l);
|
|
for (auto & w : wlist) {
|
|
if (w.is_binary_non_learned_clause()) {
|
|
r.push_back(clause_wrapper(l, w.get_literal()));
|
|
SASSERT(r.back().size() == 2);
|
|
}
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Resolve clauses c1 and c2.
|
|
c1 must contain l.
|
|
c2 must contain ~l.
|
|
Store result in r.
|
|
Return false if the result is a tautology
|
|
*/
|
|
bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) {
|
|
CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
|
|
SASSERT(c1.contains(l));
|
|
SASSERT(c2.contains(~l));
|
|
bool res = true;
|
|
m_elim_counter -= c1.size() + c2.size();
|
|
unsigned sz1 = c1.size();
|
|
for (unsigned i = 0; i < sz1; ++i) {
|
|
literal l1 = c1[i];
|
|
if (l == l1)
|
|
continue;
|
|
m_visited[l1.index()] = true;
|
|
r.push_back(l1);
|
|
}
|
|
|
|
literal not_l = ~l;
|
|
unsigned sz2 = c2.size();
|
|
for (unsigned i = 0; i < sz2; ++i) {
|
|
literal l2 = c2[i];
|
|
if (not_l == l2)
|
|
continue;
|
|
if (m_visited[(~l2).index()]) {
|
|
res = false;
|
|
break;
|
|
}
|
|
if (!m_visited[l2.index()])
|
|
r.push_back(l2);
|
|
}
|
|
|
|
for (unsigned i = 0; i < sz1; ++i) {
|
|
literal l1 = c1[i];
|
|
m_visited[l1.index()] = false;
|
|
}
|
|
return res;
|
|
}
|
|
|
|
void simplifier::save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs) {
|
|
model_converter & mc = s.m_mc;
|
|
for (auto & e : cs) {
|
|
mc.insert(mc_entry, e);
|
|
}
|
|
}
|
|
|
|
void simplifier::add_non_learned_binary_clause(literal l1, literal l2) {
|
|
watched* w;
|
|
watch_list & wlist1 = get_wlist(~l1);
|
|
watch_list & wlist2 = get_wlist(~l2);
|
|
w = find_binary_watch(wlist1, l2);
|
|
if (w) {
|
|
if (w->is_learned())
|
|
w->set_not_learned();
|
|
}
|
|
else {
|
|
wlist1.push_back(watched(l2, false));
|
|
}
|
|
|
|
w = find_binary_watch(wlist2, l1);
|
|
if (w) {
|
|
if (w->is_learned())
|
|
w->set_not_learned();
|
|
}
|
|
else {
|
|
wlist2.push_back(watched(l1, false));
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Eliminate the binary clauses watched by l, when l.var() is being eliminated
|
|
*/
|
|
void simplifier::remove_bin_clauses(literal l) {
|
|
watch_list & wlist = get_wlist(~l);
|
|
for (auto & w : wlist) {
|
|
if (w.is_binary_clause()) {
|
|
literal l2 = w.get_literal();
|
|
watch_list & wlist2 = get_wlist(~l2);
|
|
watch_list::iterator it2 = wlist2.begin();
|
|
watch_list::iterator itprev = it2;
|
|
watch_list::iterator end2 = wlist2.end();
|
|
for (; it2 != end2; ++it2) {
|
|
if (it2->is_binary_clause() && it2->get_literal() == l) {
|
|
TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";);
|
|
m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned()));
|
|
continue;
|
|
}
|
|
*itprev = *it2;
|
|
itprev++;
|
|
}
|
|
wlist2.set_end(itprev);
|
|
m_sub_bin_todo.erase(bin_clause(l, l2, w.is_learned()));
|
|
}
|
|
}
|
|
TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);
|
|
wlist.finalize();
|
|
}
|
|
|
|
/**
|
|
\brief Eliminate the clauses where the variable being eliminated occur.
|
|
*/
|
|
void simplifier::remove_clauses(clause_use_list const & cs, literal l) {
|
|
for (auto it = cs.mk_iterator(); !it.at_end(); ) {
|
|
clause & c = it.curr();
|
|
it.next();
|
|
SASSERT(c.contains(l));
|
|
c.set_removed(true);
|
|
m_use_list.erase(c, l);
|
|
m_sub_todo.erase(c);
|
|
TRACE("resolution_bug", tout << "del_clause (elim_var): " << c << "\n";);
|
|
m_need_cleanup = true;
|
|
}
|
|
}
|
|
|
|
bool simplifier::try_eliminate(bool_var v) {
|
|
TRACE("resolution_bug", tout << "processing: " << v << "\n";);
|
|
if (value(v) != l_undef)
|
|
return false;
|
|
|
|
literal pos_l(v, false);
|
|
literal neg_l(v, true);
|
|
unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
|
|
unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
|
|
clause_use_list & pos_occs = m_use_list.get(pos_l);
|
|
clause_use_list & neg_occs = m_use_list.get(neg_l);
|
|
unsigned num_pos = pos_occs.non_blocked_size() + num_bin_pos;
|
|
unsigned num_neg = neg_occs.non_blocked_size() + num_bin_neg;
|
|
|
|
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
|
|
|
|
if (num_pos >= m_res_occ_cutoff && num_neg >= m_res_occ_cutoff)
|
|
return false;
|
|
|
|
unsigned before_lits = num_bin_pos*2 + num_bin_neg*2;
|
|
|
|
for (auto it = pos_occs.mk_iterator(); !it.at_end(); it.next()) {
|
|
if (!it.curr().is_blocked())
|
|
before_lits += it.curr().size();
|
|
}
|
|
|
|
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
|
|
if (!it.curr().is_blocked())
|
|
before_lits += it.curr().size();
|
|
}
|
|
|
|
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";);
|
|
|
|
if (num_pos >= m_res_occ_cutoff3 && num_neg >= m_res_occ_cutoff3 && before_lits > m_res_lit_cutoff3 && s.m_clauses.size() > m_res_cls_cutoff2)
|
|
return false;
|
|
if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 &&
|
|
s.m_clauses.size() > m_res_cls_cutoff1 && s.m_clauses.size() <= m_res_cls_cutoff2)
|
|
return false;
|
|
if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 &&
|
|
s.m_clauses.size() <= m_res_cls_cutoff1)
|
|
return false;
|
|
|
|
m_pos_cls.reset();
|
|
m_neg_cls.reset();
|
|
collect_clauses(pos_l, m_pos_cls);
|
|
collect_clauses(neg_l, m_neg_cls);
|
|
|
|
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
|
|
unsigned before_clauses = num_pos + num_neg;
|
|
unsigned after_clauses = 0;
|
|
for (clause_wrapper& c1 : m_pos_cls) {
|
|
for (clause_wrapper& c2 : m_neg_cls) {
|
|
m_new_cls.reset();
|
|
if (resolve(c1, c2, pos_l, m_new_cls)) {
|
|
TRACE("resolution_detail", tout << c1 << "\n" << c2 << "\n-->\n";
|
|
for (literal l : m_new_cls) tout << l << " "; tout << "\n";);
|
|
after_clauses++;
|
|
if (after_clauses > before_clauses) {
|
|
TRACE("resolution", tout << "too many after clauses: " << after_clauses << "\n";);
|
|
return false;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
|
|
m_elim_counter -= num_pos * num_neg + before_lits;
|
|
|
|
m_elim_counter -= num_pos * num_neg + before_lits;
|
|
|
|
// eliminate variable
|
|
++s.m_stats.m_elim_var_res;
|
|
//VERIFY(!is_external(v));
|
|
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
|
save_clauses(mc_entry, m_pos_cls);
|
|
save_clauses(mc_entry, m_neg_cls);
|
|
s.m_eliminated[v] = true;
|
|
remove_bin_clauses(pos_l);
|
|
remove_bin_clauses(neg_l);
|
|
remove_clauses(pos_occs, pos_l);
|
|
remove_clauses(neg_occs, neg_l);
|
|
pos_occs.reset();
|
|
neg_occs.reset();
|
|
|
|
m_elim_counter -= num_pos * num_neg + before_lits;
|
|
|
|
for (auto & c1 : m_pos_cls) {
|
|
for (auto & c2 : m_neg_cls) {
|
|
m_new_cls.reset();
|
|
if (!resolve(c1, c2, pos_l, m_new_cls))
|
|
continue;
|
|
TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
|
|
if (cleanup_clause(m_new_cls))
|
|
continue; // clause is already satisfied.
|
|
switch (m_new_cls.size()) {
|
|
case 0:
|
|
s.set_conflict(justification());
|
|
break;
|
|
case 1:
|
|
propagate_unit(m_new_cls[0]);
|
|
break;
|
|
case 2:
|
|
s.m_stats.m_mk_bin_clause++;
|
|
add_non_learned_binary_clause(m_new_cls[0], m_new_cls[1]);
|
|
back_subsumption1(m_new_cls[0], m_new_cls[1], false);
|
|
break;
|
|
default:
|
|
if (m_new_cls.size() == 3)
|
|
s.m_stats.m_mk_ter_clause++;
|
|
else
|
|
s.m_stats.m_mk_clause++;
|
|
clause * new_c = s.m_cls_allocator.mk_clause(m_new_cls.size(), m_new_cls.c_ptr(), false);
|
|
|
|
if (s.m_config.m_drat) s.m_drat.add(*new_c, true);
|
|
s.m_clauses.push_back(new_c);
|
|
m_use_list.insert(*new_c);
|
|
if (m_sub_counter > 0)
|
|
back_subsumption1(*new_c);
|
|
else
|
|
back_subsumption0(*new_c);
|
|
break;
|
|
}
|
|
if (s.inconsistent())
|
|
return true;
|
|
}
|
|
}
|
|
|
|
return true;
|
|
}
|
|
|
|
struct simplifier::elim_var_report {
|
|
simplifier & m_simplifier;
|
|
stopwatch m_watch;
|
|
unsigned m_num_elim_vars;
|
|
elim_var_report(simplifier & s):
|
|
m_simplifier(s),
|
|
m_num_elim_vars(s.m_num_elim_vars) {
|
|
m_watch.start();
|
|
}
|
|
|
|
~elim_var_report() {
|
|
m_watch.stop();
|
|
IF_VERBOSE(SAT_VB_LVL,
|
|
verbose_stream() << " (sat-resolution :elim-bool-vars "
|
|
<< (m_simplifier.m_num_elim_vars - m_num_elim_vars)
|
|
<< " :threshold " << m_simplifier.m_elim_counter
|
|
<< mem_stat()
|
|
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
|
|
}
|
|
};
|
|
|
|
void simplifier::elim_vars() {
|
|
if (!elim_vars_enabled()) return;
|
|
elim_var_report rpt(*this);
|
|
bool_var_vector vars;
|
|
order_vars_for_elim(vars);
|
|
sat::elim_vars elim_bdd(*this);
|
|
for (bool_var v : vars) {
|
|
checkpoint();
|
|
if (m_elim_counter < 0)
|
|
break;
|
|
if (is_external(v)) {
|
|
// skip
|
|
}
|
|
else if (try_eliminate(v)) {
|
|
m_num_elim_vars++;
|
|
}
|
|
else if (elim_vars_bdd_enabled() && elim_bdd(v)) {
|
|
m_num_elim_vars++;
|
|
}
|
|
}
|
|
|
|
m_pos_cls.finalize();
|
|
m_neg_cls.finalize();
|
|
m_new_cls.finalize();
|
|
}
|
|
|
|
void simplifier::updt_params(params_ref const & _p) {
|
|
sat_simplifier_params p(_p);
|
|
m_cce = p.cce();
|
|
m_acce = p.acce();
|
|
m_bca = p.bca();
|
|
m_abce = p.abce();
|
|
m_bce_delay = p.bce_delay();
|
|
m_elim_blocked_clauses = p.elim_blocked_clauses();
|
|
m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
|
|
m_retain_blocked_clauses = p.retain_blocked_clauses();
|
|
m_blocked_clause_limit = p.blocked_clause_limit();
|
|
m_res_limit = p.resolution_limit();
|
|
m_res_occ_cutoff = p.resolution_occ_cutoff();
|
|
m_res_occ_cutoff1 = p.resolution_occ_cutoff_range1();
|
|
m_res_occ_cutoff2 = p.resolution_occ_cutoff_range2();
|
|
m_res_occ_cutoff3 = p.resolution_occ_cutoff_range3();
|
|
m_res_lit_cutoff1 = p.resolution_lit_cutoff_range1();
|
|
m_res_lit_cutoff2 = p.resolution_lit_cutoff_range2();
|
|
m_res_lit_cutoff3 = p.resolution_lit_cutoff_range3();
|
|
m_res_cls_cutoff1 = p.resolution_cls_cutoff1();
|
|
m_res_cls_cutoff2 = p.resolution_cls_cutoff2();
|
|
m_subsumption = p.subsumption();
|
|
m_subsumption_limit = p.subsumption_limit();
|
|
m_elim_vars = p.elim_vars();
|
|
m_elim_vars_bdd = p.elim_vars_bdd();
|
|
m_elim_vars_bdd_delay = p.elim_vars_bdd_delay();
|
|
m_incremental_mode = s.get_config().m_incremental && !p.override_incremental();
|
|
}
|
|
|
|
void simplifier::collect_param_descrs(param_descrs & r) {
|
|
sat_simplifier_params::collect_param_descrs(r);
|
|
}
|
|
|
|
void simplifier::collect_statistics(statistics & st) const {
|
|
st.update("subsumed", m_num_subsumed);
|
|
st.update("subsumption resolution", m_num_sub_res);
|
|
st.update("elim literals", m_num_elim_lits);
|
|
st.update("elim blocked clauses", m_num_blocked_clauses);
|
|
st.update("elim covered clauses", m_num_covered_clauses);
|
|
st.update("blocked clauses added", m_num_bca);
|
|
}
|
|
|
|
void simplifier::reset_statistics() {
|
|
m_num_blocked_clauses = 0;
|
|
m_num_covered_clauses = 0;
|
|
m_num_subsumed = 0;
|
|
m_num_sub_res = 0;
|
|
m_num_elim_lits = 0;
|
|
m_num_elim_vars = 0;
|
|
m_num_bca = 0;
|
|
}
|
|
};
|