mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix https://z3.codeplex.com/workitem/62

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-04 11:57:29 -08:00
parent 8b10e13251
commit 825b72719c
2 changed files with 189 additions and 173 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

142
src/sat/sat_simplifier.cpp
View file

@ -9,7 +9,7 @@ Abstract:
SAT simplification procedures that use a "full" occurrence list:
Subsumption, Blocked Clause Removal, Variable Elimination, ...
Author:
@ -54,21 +54,21 @@ namespace sat {
m_use_list[l2.index()].erase(c);
}
}
simplifier::simplifier(solver & _s, params_ref const & p):
s(_s),
m_num_calls(0) {
updt_params(p);
reset_statistics();
}
simplifier::~simplifier() {
}
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_external(v); }
inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); }
@ -78,7 +78,7 @@ namespace sat {
lbool simplifier::value(literal l) const { return s.value(l); }
inline void simplifier::checkpoint() { s.checkpoint(); }
void simplifier::register_clauses(clause_vector & cs) {
std::stable_sort(cs.begin(), cs.end(), size_lt());
clause_vector::iterator it = cs.begin();
@ -117,7 +117,7 @@ namespace sat {
SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
s.get_wlist(~l1).erase(watched(l2, learned));
}
void simplifier::init_visited() {
m_visited.reset();
m_visited.resize(2*s.num_vars(), false);
@ -155,7 +155,7 @@ namespace sat {
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
elim_blocked_clauses();
if (!learned)
m_num_calls++;
@ -180,6 +180,7 @@ namespace sat {
bool vars_eliminated = m_num_elim_vars > old_num_elim_vars;
if (!m_need_cleanup) {
TRACE("after_simplifier", tout << "skipping cleanup...\n";);
if (vars_eliminated) {
// must remove learned clauses with eliminated variables
cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
@ -189,6 +190,7 @@ namespace sat {
free_memory();
return;
}
TRACE("after_simplifier", tout << "cleanning watches...\n";);
cleanup_watches();
cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists);
cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
@ -234,7 +236,7 @@ namespace sat {
s.del_clause(c);
continue;
}
if (learned && vars_eliminated) {
unsigned sz = c.size();
unsigned i;
@ -293,7 +295,7 @@ namespace sat {
mark_visited(c[i]);
}
}
void simplifier::unmark_all(clause const & c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++)
@ -325,7 +327,7 @@ namespace sat {
*/
bool simplifier::subsumes1(clause const & c1, clause const & c2, literal & l) {
unsigned sz2 = c2.size();
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
mark_visited(c2[i]);
bool r = true;
@ -344,7 +346,7 @@ namespace sat {
}
}
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
unmark_visited(c2[i]);
return r;
}
@ -353,7 +355,7 @@ namespace sat {
\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,
void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits,
literal target) {
clause_use_list const & cs = m_use_list.get(target);
clause_use_list::iterator it = cs.mk_iterator();
@ -362,7 +364,7 @@ namespace sat {
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() &&
c1.size() <= c2.size() &&
approx_subset(c1.approx(), c2.approx())) {
m_sub_counter -= c1.size() + c2.size();
literal l;
@ -373,7 +375,7 @@ namespace sat {
}
it.next();
}
}
}
/**
\brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1.
@ -400,7 +402,7 @@ namespace sat {
if (*l_it == null_literal) {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();
c1.unset_learned();
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
m_num_subsumed++;
@ -447,9 +449,9 @@ namespace sat {
*/
bool simplifier::subsumes0(clause const & c1, clause const & c2) {
unsigned sz2 = c2.size();
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
mark_visited(c2[i]);
bool r = true;
unsigned sz1 = c1.size();
for (unsigned i = 0; i < sz1; i++) {
@ -459,12 +461,12 @@ namespace sat {
}
}
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
unmark_visited(c2[i]);
return r;
}
/**
\brief Collect the clauses subsumed by c1 (using the occurrence list of target).
*/
@ -475,7 +477,7 @@ namespace sat {
clause & c2 = it.curr();
SASSERT(!c2.was_removed());
if (&c2 != &c1 &&
c1.size() <= c2.size() &&
c1.size() <= c2.size() &&
approx_subset(c1.approx(), c2.approx())) {
m_sub_counter -= c1.size() + c2.size();
if (subsumes0(c1, c2)) {
@ -485,7 +487,7 @@ namespace sat {
it.next();
}
}
/**
\brief Collect the clauses subsumed by c1
*/
@ -493,8 +495,8 @@ namespace sat {
literal l = get_min_occ_var0(c1);
collect_subsumed0_core(c1, out, l);
}
/**
\brief Perform backward subsumption using c1.
*/
@ -507,16 +509,16 @@ namespace sat {
clause & c2 = *(*it);
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_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) {
@ -666,7 +668,7 @@ namespace sat {
back_subsumption1(c);
if (w.is_learned() && !c.is_learned()) {
SASSERT(wlist[j] == w);
TRACE("mark_not_learned_bug",
TRACE("mark_not_learned_bug",
tout << "marking as not learned: " << l2 << " " << wlist[j].is_learned() << "\n";);
wlist[j].mark_not_learned();
mark_as_not_learned_core(get_wlist(~l2), l);
@ -735,7 +737,7 @@ namespace sat {
continue;
}
if (it2->get_literal() == last_lit) {
TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx)
TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx)
<< " " << it2->get_literal() << "\n";);
elim++;
}
@ -762,12 +764,12 @@ namespace sat {
m_num_sub_res(s.m_num_sub_res) {
m_watch.start();
}
~subsumption_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-subsumer :subsumed "
<< (m_simplifier.m_num_subsumed - m_num_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()
@ -847,12 +849,12 @@ namespace sat {
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 {
bool operator()(unsigned l_idx1, unsigned l_idx2) const {
return weight(l_idx1) < weight(l_idx2);
}
};
@ -861,9 +863,9 @@ namespace sat {
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) {
void insert(literal l) {
unsigned idx = l.index();
m_queue.reserve(idx + 1);
m_queue.reserve(idx + 1);
SASSERT(!m_queue.contains(idx));
m_queue.insert(idx);
}
@ -877,14 +879,14 @@ namespace sat {
literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
bool empty() const { return m_queue.empty(); }
};
simplifier & s;
int m_counter;
model_converter & mc;
queue m_queue;
clause_vector m_to_remove;
blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
vector<watch_list> & wlist):
s(_s),
m_counter(limit),
@ -946,7 +948,7 @@ namespace sat {
clause_vector::iterator it = m_to_remove.begin();
clause_vector::iterator end = m_to_remove.end();
for (; it != end; ++it) {
s.remove_clause(*(*it));
s.remove_clause(*(*it));
}
}
{
@ -1025,12 +1027,12 @@ namespace sat {
m_num_blocked_clauses(s.m_num_blocked_clauses) {
m_watch.start();
}
~blocked_cls_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
<< mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
@ -1062,8 +1064,8 @@ namespace sat {
unsigned num_neg = m_use_list.get(neg_l).size();
unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
unsigned num_bin_neg = get_num_non_learned_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
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;
}
@ -1071,7 +1073,7 @@ namespace sat {
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; }
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) {
@ -1104,7 +1106,7 @@ namespace sat {
r.push_back(it2->first);
}
}
/**
\brief Collect clauses and binary clauses containing l.
*/
@ -1116,7 +1118,7 @@ namespace sat {
SASSERT(r.back().size() == it.curr().size());
it.next();
}
watch_list & wlist = get_wlist(~l);
watch_list::iterator it2 = wlist.begin();
watch_list::iterator end2 = wlist.end();
@ -1129,7 +1131,7 @@ namespace sat {
}
/**
\brief Resolve clauses c1 and c2.
\brief Resolve clauses c1 and c2.
c1 must contain l.
c2 must contain ~l.
Store result in r.
@ -1149,7 +1151,7 @@ namespace sat {
m_visited[l2.index()] = true;
r.push_back(l2);
}
literal not_l = ~l;
sz = c2.size();
m_elim_counter -= sz;
@ -1164,7 +1166,7 @@ namespace sat {
if (!m_visited[l2.index()])
r.push_back(l2);
}
sz = c1.size();
for (unsigned i = 0; i < sz; i++) {
literal l2 = c1[i];
@ -1200,7 +1202,7 @@ namespace sat {
break;
}
}
CTRACE("resolve_bug", it2 == end2,
CTRACE("resolve_bug", it2 == end2,
tout << ~l1 << " -> ";
display(tout, s.m_cls_allocator, wlist1); tout << "\n" << ~l2 << " -> ";
display(tout, s.m_cls_allocator, wlist2); tout << "\n";);
@ -1262,7 +1264,7 @@ namespace sat {
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_non_learned_bin(pos_l);
@ -1274,12 +1276,12 @@ namespace sat {
m_elim_counter -= num_pos + num_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;
{
clause_use_list::iterator it = pos_occs.mk_iterator();
while (!it.at_end()) {
@ -1287,7 +1289,7 @@ namespace sat {
it.next();
}
}
{
clause_use_list::iterator it2 = neg_occs.mk_iterator();
while (!it2.at_end()) {
@ -1297,23 +1299,23 @@ namespace sat {
}
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 &&
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 &&
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);
m_elim_counter -= num_pos * num_neg + before_lits;
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
unsigned before_clauses = num_pos + num_neg;
unsigned after_clauses = 0;
@ -1350,7 +1352,7 @@ namespace sat {
neg_occs.reset();
m_elim_counter -= num_pos * num_neg + before_lits;
it1 = m_pos_cls.begin();
end1 = m_pos_cls.end();
for (; it1 != end1; ++it1) {
@ -1393,7 +1395,7 @@ namespace sat {
return true;
}
}
return true;
}
@ -1406,10 +1408,10 @@ namespace sat {
m_num_elim_vars(s.m_num_elim_vars) {
m_watch.start();
}
~elim_var_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
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
@ -1417,12 +1419,12 @@ namespace sat {
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
};
void simplifier::elim_vars() {
elim_var_report rpt(*this);
bool_var_vector vars;
order_vars_for_elim(vars);
bool_var_vector::iterator it = vars.begin();
bool_var_vector::iterator end = vars.end();
for (; it != end; ++it) {
@ -1463,7 +1465,7 @@ namespace sat {
void simplifier::collect_param_descrs(param_descrs & r) {
sat_simplifier_params::collect_param_descrs(r);
}
void simplifier::collect_statistics(statistics & st) {
st.update("subsumed", m_num_subsumed);
st.update("subsumption resolution", m_num_sub_res);
@ -1471,7 +1473,7 @@ namespace sat {
st.update("elim bool vars", m_num_elim_vars);
st.update("elim blocked clauses", m_num_blocked_clauses);
}
void simplifier::reset_statistics() {
m_num_blocked_clauses = 0;
m_num_subsumed = 0;

220
src/sat/sat_solver.cpp
View file

@ -27,7 +27,7 @@ Revision History:
// define to create a copy of the solver before starting the search
// useful for checking models
// #define CLONE_BEFORE_SOLVING
namespace sat {
solver::solver(params_ref const & p, extension * ext):
@ -103,7 +103,7 @@ namespace sat {
}
}
}
// -----------------------
//
// Variable & Clause creation
@ -312,7 +312,7 @@ namespace sat {
/**
\brief Select a watch literal starting the search at the given position.
This method is only used for clauses created during the search.
I use the following rules to select a watch literal.
1- select a literal l in idx >= starting_at such that value(l) = l_true,
@ -329,7 +329,7 @@ namespace sat {
lvl(l) >= lvl(l')
Without rule 3, boolean propagation is incomplete, that is, it may miss possible propagations.
\remark The method select_lemma_watch_lit is used to select the watch literal for regular learned clauses.
*/
unsigned solver::select_watch_lit(clause const & cls, unsigned starting_at) const {
@ -443,7 +443,7 @@ namespace sat {
erase_clause_watch(get_wlist(~c[0]), cls_off);
erase_clause_watch(get_wlist(~c[1]), cls_off);
}
void solver::dettach_ter_clause(clause & c) {
erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
@ -498,10 +498,10 @@ namespace sat {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
switch (value(c[i])) {
case l_true:
case l_true:
return l_true;
case l_undef:
found_undef = true;
case l_undef:
found_undef = true;
break;
default:
break;
@ -515,7 +515,7 @@ namespace sat {
// Propagation
//
// -----------------------
bool solver::propagate_core(bool update) {
if (m_inconsistent)
return false;
@ -545,7 +545,7 @@ namespace sat {
}
for (; it != end; ++it) {
switch (it->get_kind()) {
case watched::BINARY:
case watched::BINARY:
l1 = it->get_literal();
switch (value(l1)) {
case l_false:
@ -585,12 +585,26 @@ namespace sat {
break;
case watched::CLAUSE: {
if (value(it->get_blocked_literal()) == l_true) {
TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
clause_offset cls_off = it->get_clause_offset();
clause & c = *(m_cls_allocator.get_clause(cls_off));
tout << c << "\n";);
*it2 = *it;
it2++;
break;
}
clause_offset cls_off = it->get_clause_offset();
clause & c = *(m_cls_allocator.get_clause(cls_off));
TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";);
if (c.was_removed()) {
// Remark: this method may be invoked when the watch lists are not in a consistent state,
// and may contain dead/removed clauses.
// See: sat_simplifier.cpp
// So, we must check whether the clause was marked for deletion, and ignore it.
*it2 = *it;
it2++;
break;
}
if (c[0] == not_l)
std::swap(c[0], c[1]);
CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";);
@ -693,7 +707,7 @@ namespace sat {
m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial;
}
// iff3_finder(*this)();
simplify_problem();
@ -704,10 +718,10 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";);
return l_undef;
}
while (true) {
SASSERT(!inconsistent());
lbool r = bounded_search();
if (r != l_undef)
return r;
@ -716,7 +730,7 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = " << m_conflicts << "\"\n";);
return l_undef;
}
restart();
if (m_conflicts >= m_next_simplify) {
simplify_problem();
@ -734,7 +748,7 @@ namespace sat {
bool_var solver::next_var() {
bool_var next;
if (m_rand() < static_cast<int>(m_config.m_random_freq * random_gen::max_value())) {
if (num_vars() == 0)
return null_bool_var;
@ -743,16 +757,16 @@ namespace sat {
if (value(next) == l_undef && !was_eliminated(next))
return next;
}
while (!m_case_split_queue.empty()) {
next = m_case_split_queue.next_var();
if (value(next) == l_undef && !was_eliminated(next))
return next;
}
return null_bool_var;
}
bool solver::decide() {
bool_var next = next_var();
if (next == null_bool_var)
@ -760,7 +774,7 @@ namespace sat {
push();
m_stats.m_decision++;
lbool phase = m_ext ? m_ext->get_phase(next) : l_undef;
if (phase == l_undef) {
switch (m_config.m_phase) {
case PS_ALWAYS_TRUE:
@ -784,7 +798,7 @@ namespace sat {
break;
}
}
SASSERT(phase != l_undef);
literal next_lit(next, phase == l_false);
assign(next_lit, justification());
@ -807,23 +821,23 @@ namespace sat {
return l_undef;
if (scope_lvl() == 0) {
cleanup(); // cleaner may propagate frozen clauses
if (inconsistent())
if (inconsistent())
return l_false;
gc();
}
}
gc();
if (!decide()) {
if (m_ext) {
switch (m_ext->check()) {
case CR_DONE:
case CR_DONE:
mk_model();
return l_true;
case CR_CONTINUE:
case CR_CONTINUE:
break;
case CR_GIVEUP:
case CR_GIVEUP:
throw abort_solver();
}
}
@ -849,23 +863,23 @@ namespace sat {
m_stopwatch.reset();
m_stopwatch.start();
}
/**
\brief Apply all simplifications.
*/
void solver::simplify_problem() {
SASSERT(scope_lvl() == 0);
m_cleaner();
CASSERT("sat_simplify_bug", check_invariant());
m_scc();
CASSERT("sat_simplify_bug", check_invariant());
m_simplifier(false);
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
if (!m_learned.empty()) {
m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation());
@ -878,11 +892,11 @@ namespace sat {
m_probing();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
m_asymm_branch();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
if (m_ext) {
m_ext->clauses_modifed();
m_ext->simplify();
@ -956,7 +970,7 @@ namespace sat {
}
}
}
if (!m_mc.check_model(m))
if (!m_mc.check_model(m))
ok = false;
CTRACE("sat_model_bug", !ok, tout << m << "\n";);
return ok;
@ -964,9 +978,9 @@ namespace sat {
void solver::restart() {
m_stats.m_restart++;
IF_VERBOSE(1,
IF_VERBOSE(1,
verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
IF_VERBOSE(30, display_status(verbose_stream()););
pop(scope_lvl());
@ -991,9 +1005,9 @@ namespace sat {
// GC
//
// -----------------------
void solver::gc() {
if (m_conflicts_since_gc <= m_gc_threshold)
if (m_conflicts_since_gc <= m_gc_threshold)
return;
CASSERT("sat_gc_bug", check_invariant());
switch (m_config.m_gc_strategy) {
@ -1073,7 +1087,7 @@ namespace sat {
std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt());
gc_half("glue");
}
void solver::gc_psm() {
save_psm();
std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt());
@ -1134,8 +1148,8 @@ namespace sat {
void solver::gc_dyn_psm() {
// To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
// that I may miss some propagations for reactivated clauses.
SASSERT(scope_lvl() == 0);
// compute
SASSERT(scope_lvl() == 0);
// compute
// d_tk
unsigned h = 0;
unsigned V_tk = 0;
@ -1152,7 +1166,7 @@ namespace sat {
double d_tk = V_tk == 0 ? static_cast<double>(num_vars() + 1) : static_cast<double>(h)/static_cast<double>(V_tk);
if (d_tk < m_min_d_tk)
m_min_d_tk = d_tk;
TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";);
TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";);
unsigned frozen = 0;
unsigned deleted = 0;
unsigned activated = 0;
@ -1218,15 +1232,15 @@ namespace sat {
++it2;
}
m_learned.set_end(it2);
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk <<
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk <<
" :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";);
}
// return true if should keep the clause, and false if we should delete it.
bool solver::activate_frozen_clause(clause & c) {
bool solver::activate_frozen_clause(clause & c) {
TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";);
SASSERT(scope_lvl() == 0);
// do some cleanup
// do some cleanup
unsigned sz = c.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
@ -1292,7 +1306,7 @@ namespace sat {
bool r = resolve_conflict_core();
CASSERT("sat_check_marks", check_marks());
// after pop, clauses are reinitialized, this may trigger another conflict.
if (!r)
if (!r)
return false;
if (!inconsistent())
return true;
@ -1311,7 +1325,7 @@ namespace sat {
if (m_conflict_lvl == 0)
return false;
m_lemma.reset();
forget_phase_of_vars(m_conflict_lvl);
unsigned idx = skip_literals_above_conflict_level();
@ -1326,7 +1340,7 @@ namespace sat {
literal consequent = m_not_l;
justification js = m_conflict;
do {
TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
@ -1362,7 +1376,7 @@ namespace sat {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
for (; it != end; ++it)
process_antecedent(*it, num_marks);
break;
}
@ -1370,10 +1384,10 @@ namespace sat {
UNREACHABLE();
break;
}
while (true) {
literal l = m_trail[idx];
if (is_marked(l.var()))
if (is_marked(l.var()))
break;
SASSERT(idx > 0);
idx--;
@ -1386,9 +1400,9 @@ namespace sat {
idx--;
num_marks--;
reset_mark(c_var);
}
}
while (num_marks > 0);
m_lemma[0] = ~consequent;
TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
@ -1401,7 +1415,7 @@ namespace sat {
}
else
reset_lemma_var_marks();
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
unsigned new_scope_lvl = 0;
@ -1432,10 +1446,10 @@ namespace sat {
return 0;
unsigned r = 0;
if (consequent != null_literal)
r = lvl(consequent);
switch (js.get_kind()) {
case justification::NONE:
break;
@ -1468,7 +1482,7 @@ namespace sat {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
for (; it != end; ++it)
r = std::max(r, lvl(*it));
break;
}
@ -1497,7 +1511,7 @@ namespace sat {
}
return idx;
}
void solver::process_antecedent(literal antecedent, unsigned & num_marks) {
bool_var var = antecedent.var();
unsigned var_lvl = lvl(var);
@ -1511,7 +1525,7 @@ namespace sat {
m_lemma.push_back(~antecedent);
}
}
/**
\brief js is an external justification. Collect its antecedents and store at m_ext_antecedents.
*/
@ -1578,7 +1592,7 @@ namespace sat {
unsigned var_lvl = lvl(var);
if (!is_marked(var) && var_lvl > 0) {
if (m_lvl_set.may_contain(var_lvl)) {
mark(var);
mark(var);
m_unmark.push_back(var);
m_lemma_min_stack.push_back(var);
}
@ -1590,17 +1604,17 @@ namespace sat {
}
/**
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
The idea is to stop the recursive search with a failure
as soon as we find a literal assigned in a level that is not in lvl_set.
as soon as we find a literal assigned in a level that is not in lvl_set.
*/
bool solver::implied_by_marked(literal lit) {
m_lemma_min_stack.reset(); // avoid recursive function
m_lemma_min_stack.push_back(lit.var());
unsigned old_size = m_unmark.size();
while (!m_lemma_min_stack.empty()) {
bool_var var = m_lemma_min_stack.back();
m_lemma_min_stack.pop_back();
@ -1701,7 +1715,7 @@ namespace sat {
void solver::minimize_lemma() {
m_unmark.reset();
updt_lemma_lvl_set();
unsigned sz = m_lemma.size();
unsigned i = 1; // the first literal is the FUIP
unsigned j = 1;
@ -1717,12 +1731,12 @@ namespace sat {
j++;
}
}
reset_unmark(0);
m_lemma.shrink(j);
m_stats.m_minimized_lits += sz - j;
}
/**
\brief Reset the mark of the variables in the current lemma.
*/
@ -1742,17 +1756,17 @@ namespace sat {
Only binary and ternary clauses are used.
*/
void solver::dyn_sub_res() {
unsigned sz = m_lemma.size();
unsigned sz = m_lemma.size();
for (unsigned i = 0; i < sz; i++) {
mark_lit(m_lemma[i]);
}
literal l0 = m_lemma[0];
// l0 is the FUIP, and we never remove the FUIP.
//
//
// In the following loop, we use unmark_lit(l) to remove a
// literal from m_lemma.
for (unsigned i = 0; i < sz; i++) {
literal l = m_lemma[i];
if (!is_marked_lit(l))
@ -1764,8 +1778,8 @@ namespace sat {
for (; it != end; ++it) {
// In this for-loop, the conditions l0 != ~l2 and l0 != ~l3
// are not really needed if the solver does not miss unit propagations.
// However, we add them anyway because we don't want to rely on this
// property of the propagator.
// However, we add them anyway because we don't want to rely on this
// property of the propagator.
// For example, if this property is relaxed in the future, then the code
// without the conditions l0 != ~l2 and l0 != ~l3 may remove the FUIP
if (it->is_binary_clause()) {
@ -1811,10 +1825,10 @@ namespace sat {
// p1 \/ ~p2
// p2 \/ ~p3
// p3 \/ ~p4
// q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ...
//
// 2. Now suppose we learned the lemma
@ -1825,15 +1839,15 @@ namespace sat {
// That is, l \/ l2 is an implied clause. Note that probing does not add
// this clause to the clause database (there are too many).
//
// 4. Lemma (*) is deleted (garbage collected).
// 4. Lemma (*) is deleted (garbage collected).
//
// 5. l is decided to be false, p1, p2, p3 and p4 are propagated using BCP,
// but l2 is not since the lemma (*) was deleted.
//
//
// Probing module still "knows" that l \/ l2 is valid binary clause
//
//
// 6. A new lemma is created where ~l2 is the FUIP and the lemma also contains l.
// If we remove l0 != ~l2 may try to delete the FUIP.
// If we remove l0 != ~l2 may try to delete the FUIP.
if (is_marked_lit(~l2) && l0 != ~l2) {
// eliminate ~l2 from lemma because we have the clause l \/ l2
unmark_lit(~l2);
@ -1844,7 +1858,7 @@ namespace sat {
// can't eliminat FUIP
SASSERT(is_marked_lit(m_lemma[0]));
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
literal l = m_lemma[i];
@ -1856,7 +1870,7 @@ namespace sat {
}
m_stats.m_dyn_sub_res += sz - j;
SASSERT(j >= 1);
m_lemma.shrink(j);
}
@ -1949,7 +1963,7 @@ namespace sat {
// Misc
//
// -----------------------
void solver::updt_params(params_ref const & p) {
m_params = p;
m_config.updt_params(p);
@ -1971,7 +1985,7 @@ namespace sat {
void solver::set_cancel(bool f) {
m_cancel = f;
}
void solver::collect_statistics(statistics & st) {
m_stats.collect_statistics(st);
m_cleaner.collect_statistics(st);
@ -2067,7 +2081,7 @@ namespace sat {
}
}
}
void solver::display_units(std::ostream & out) const {
unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
for (unsigned i = 0; i < end; i++) {
@ -2221,26 +2235,26 @@ namespace sat {
// Simplification
//
// -----------------------
void solver::cleanup() {
if (scope_lvl() > 0 || inconsistent())
return;
void solver::cleanup() {
if (scope_lvl() > 0 || inconsistent())
return;
if (m_cleaner() && m_ext)
m_ext->clauses_modifed();
}
void solver::simplify(bool learned) {
if (scope_lvl() > 0 || inconsistent())
return;
m_simplifier(learned);
m_simplifier.free_memory();
void solver::simplify(bool learned) {
if (scope_lvl() > 0 || inconsistent())
return;
m_simplifier(learned);
m_simplifier.free_memory();
if (m_ext)
m_ext->clauses_modifed();
}
unsigned solver::scc_bin() {
if (scope_lvl() > 0 || inconsistent())
return 0;
unsigned r = m_scc();
unsigned solver::scc_bin() {
if (scope_lvl() > 0 || inconsistent())
return 0;
unsigned r = m_scc();
if (r > 0 && m_ext)
m_ext->clauses_modifed();
return r;
@ -2314,10 +2328,10 @@ namespace sat {
out << " :inconsistent " << (m_inconsistent ? "true" : "false") << "\n";
out << " :vars " << num_vars() << "\n";
out << " :elim-vars " << num_elim << "\n";
out << " :lits " << num_lits << "\n";
out << " :lits " << num_lits << "\n";
out << " :assigned " << m_trail.size() << "\n";
out << " :binary-clauses " << num_bin << "\n";
out << " :ternary-clauses " << num_ter << "\n";
out << " :binary-clauses " << num_bin << "\n";
out << " :ternary-clauses " << num_ter << "\n";
out << " :clauses " << num_cls << "\n";
out << " :del-clause " << m_stats.m_del_clause << "\n";
out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast<double>(num_lits) / static_cast<double>(total_cls)) << "\n";