mirror of
https://github.com/Z3Prover/z3
synced 2025-08-26 21:16:02 +00:00
9fc4015c46
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
113 lines
3.5 KiB
C++
113 lines
3.5 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_watched.cpp
|
|
|
|
Abstract:
|
|
|
|
Element of the SAT solver watchlist.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2011-05-24.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "sat/sat_watched.h"
|
|
#include "sat/sat_clause.h"
|
|
#include "sat/sat_extension.h"
|
|
|
|
namespace sat {
|
|
|
|
bool erase_clause_watch(watch_list & wlist, clause_offset c) {
|
|
watch_list::iterator it = wlist.begin();
|
|
watch_list::iterator end = wlist.end();
|
|
for (; it != end; ++it) {
|
|
if (it->is_clause() && it->get_clause_offset() == c) {
|
|
watch_list::iterator it2 = it;
|
|
++it;
|
|
for (; it != end; ++it, ++it2) {
|
|
SASSERT(!((it->is_clause() && it->get_clause_offset() == c)));
|
|
*it2 = *it;
|
|
}
|
|
wlist.set_end(it2);
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
watched* find_binary_watch(watch_list & wlist, literal l) {
|
|
for (watched& w : wlist) {
|
|
if (w.is_binary_clause() && w.get_literal() == l) return &w;
|
|
}
|
|
return nullptr;
|
|
}
|
|
|
|
watched const* find_binary_watch(watch_list const& wlist, literal l) {
|
|
for (watched const& w : wlist) {
|
|
if (w.is_binary_clause() && w.get_literal() == l) return &w;
|
|
}
|
|
return nullptr;
|
|
}
|
|
|
|
void erase_binary_watch(watch_list& wlist, literal l) {
|
|
watch_list::iterator it = wlist.begin(), end = wlist.end();
|
|
watch_list::iterator it2 = it;
|
|
bool found = false;
|
|
for (; it != end; ++it) {
|
|
if (it->is_binary_clause() && it->get_literal() == l && !found) {
|
|
found = true;
|
|
}
|
|
else {
|
|
*it2 = *it;
|
|
++it2;
|
|
}
|
|
}
|
|
wlist.set_end(it2);
|
|
VERIFY(found);
|
|
}
|
|
|
|
void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
|
|
watch_list::iterator end = wlist.end();
|
|
for (; it != end; ++it, ++it2)
|
|
*it2 = *it;
|
|
wlist.set_end(it2);
|
|
}
|
|
|
|
|
|
std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext) {
|
|
bool first = true;
|
|
for (watched const& w : wlist) {
|
|
if (first)
|
|
first = false;
|
|
else
|
|
out << " ";
|
|
switch (w.get_kind()) {
|
|
case watched::BINARY:
|
|
out << w.get_literal();
|
|
if (w.is_learned())
|
|
out << "*";
|
|
break;
|
|
case watched::CLAUSE:
|
|
out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")";
|
|
break;
|
|
case watched::EXT_CONSTRAINT:
|
|
if (ext) {
|
|
ext->display_constraint(out, w.get_ext_constraint_idx());
|
|
}
|
|
else {
|
|
out << "ext: " << w.get_ext_constraint_idx();
|
|
}
|
|
break;
|
|
default:
|
|
UNREACHABLE();
|
|
}
|
|
}
|
|
return out;
|
|
}
|
|
|
|
};
|