mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-29 08:11:27 -07:00
parent 085c18a92a
commit 7580644d15
4 changed files with 336 additions and 279 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

473
src/sat/ba_solver.cpp
View file

@ -53,7 +53,7 @@ namespace sat {
}
ba_solver::card::card(literal lit, literal_vector const& lits, unsigned k):
constraint(card_t, lit, lits.size()),
constraint(card_t, lit, lits.size(), get_obj_size(lits.size())),
m_k(k) {
for (unsigned i = 0; i < size(); ++i) {
m_lits[i] = lits[i];
@ -104,7 +104,7 @@ namespace sat {
}
ba_solver::pb::pb(literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
constraint(pb_t, lit, wlits.size()),
constraint(pb_t, lit, wlits.size(), get_obj_size(wlits.size())),
m_k(k),
m_slack(0),
m_num_watch(0),
@ -137,8 +137,7 @@ namespace sat {
}
ba_solver::xor::xor(literal lit, literal_vector const& lits):
constraint(xor_t, lit, lits.size())
{
constraint(xor_t, lit, lits.size(), get_obj_size(lits.size())) {
for (unsigned i = 0; i < size(); ++i) {
m_lits[i] = lits[i];
}
@ -169,9 +168,9 @@ namespace sat {
}
DEBUG_CODE(
bool is_false = false;
for (unsigned k = 0; k < sz; ++k) {
SASSERT(!is_false || value(c[k]) == l_false);
is_false = value(c[k]) == l_false;
for (literal l : c) {
SASSERT(!is_false || value(l) == l_false);
is_false = value(l) == l_false;
});
// j is the number of non-false, sz - j the number of false.
@ -220,7 +219,18 @@ namespace sat {
get_wlist(~lit).push_back(watched(c.index()));
}
void ba_solver::assign(card& c, literal lit) {
void ba_solver::set_conflict(constraint& c, literal lit) {
m_stats.m_num_conflicts++;
TRACE("sat", display(tout, c, true); );
SASSERT(validate_conflict(c));
if (c.is_xor() && value(lit) == l_true) lit.neg();
SASSERT(value(lit) == l_false);
set_conflict(justification::mk_ext_justification(c.index()), ~lit);
SASSERT(inconsistent());
}
void ba_solver::assign(constraint& c, literal lit) {
switch (value(lit)) {
case l_true:
break;
@ -228,17 +238,14 @@ namespace sat {
set_conflict(c, lit);
break;
default:
m_stats.m_num_card_propagations++;
m_stats.m_num_propagations++;
m_num_propagations_since_pop++;
//TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
SASSERT(validate_unit_propagation(c));
SASSERT(validate_unit_propagation(c, lit));
if (get_config().m_drat) {
svector<drat::premise> ps;
literal_vector lits;
if (c.lit() != null_literal) lits.push_back(~c.lit());
for (unsigned i = c.k(); i < c.size(); ++i) {
lits.push_back(c[i]);
}
get_antecedents(lit, c, lits);
lits.push_back(lit);
ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case.
drat_add(lits, ps);
@ -248,15 +255,6 @@ namespace sat {
}
}
void ba_solver::set_conflict(card& c, literal lit) {
m_stats.m_num_card_conflicts++;
TRACE("sat", display(tout, c, true); );
SASSERT(validate_conflict(c));
SASSERT(value(lit) == l_false);
set_conflict(justification::mk_ext_justification(c.index()), ~lit);
SASSERT(inconsistent());
}
// pb:
@ -370,6 +368,10 @@ namespace sat {
add_index(p, index, lit);
}
SASSERT(index < num_watch);
if (index >= num_watch) {
std::cout << "BAD assign. " << alit << " not found within " << num_watch << "\n";
std::cout << p << "\n";
}
unsigned index1 = index + 1;
for (; m_a_max == 0 && index1 < num_watch; ++index1) {
@ -423,6 +425,10 @@ namespace sat {
while (!m_pb_undef.empty()) {
index1 = m_pb_undef.back();
if (index1 == num_watch) index1 = index; // it was swapped with index above.
if (index1 >= num_watch) {
std::cout << "BAD assignment at position " << index1 << " with " << num_watch << "\n";
std::cout << p << "\n";
}
literal lit = p[index1].second;
SASSERT(value(lit) == l_undef);
TRACE("sat", tout << index1 << " " << lit << "\n";);
@ -450,43 +456,7 @@ namespace sat {
}
void ba_solver::clear_watch(pb& p) {
unsigned sz = p.size();
for (unsigned i = 0; i < sz; ++i) {
unwatch_literal(p[i].second, p);
}
}
void ba_solver::set_conflict(pb& p, literal lit) {
m_stats.m_num_pb_conflicts++;
TRACE("sat", display(tout, p, true); );
// SASSERT(validate_conflict(p));
SASSERT(value(lit) == l_false);
set_conflict(justification::mk_ext_justification(p.index()), ~lit);
SASSERT(inconsistent());
}
void ba_solver::assign(pb& p, literal lit) {
switch (value(lit)) {
case l_true:
break;
case l_false:
set_conflict(p, lit);
break;
default:
SASSERT(validate_unit_propagation(p, lit));
m_stats.m_num_pb_propagations++;
m_num_propagations_since_pop++;
if (get_config().m_drat) {
svector<drat::premise> ps;
literal_vector lits;
get_pb_antecedents(lit, p, lits);
lits.push_back(lit);
ps.push_back(drat::premise(drat::s_ext(), p.lit()));
drat_add(lits, ps);
}
assign(lit, justification::mk_ext_justification(p.index()));
break;
}
for (wliteral wl : p) unwatch_literal(wl.second, p);
}
void ba_solver::unit_propagation_simplification(literal lit, literal_vector const& lits) {
@ -515,9 +485,7 @@ namespace sat {
bool ba_solver::is_cardinality(pb const& p) {
if (p.size() == 0) return false;
unsigned w = p[0].first;
for (unsigned i = 1; i < p.size(); ++i) {
if (w != p[i].first) return false;
}
for (wliteral wl : p) if (w != wl.first) return false;
return true;
}
@ -604,6 +572,7 @@ namespace sat {
// std::cout << "new size: " << sz << " old size " << p.size() << "\n";
p.update_size(sz);
p.update_k(p.k() - true_val);
p.update_max_sum();
// display(verbose_stream(), c, true);
if (p.lit() == null_literal) {
init_watch(p, true);
@ -617,11 +586,13 @@ namespace sat {
}
}
void ba_solver::remove_constraint(pb& p) {
clear_watch(p);
nullify_tracking_literal(p);
p.remove();
m_constraint_removed = true;
void ba_solver::display(std::ostream& out, constraint const& c, bool values) const {
switch (c.tag()) {
case card_t: display(out, c.to_card(), values); break;
case pb_t: display(out, c.to_pb(), values); break;
case xor_t: display(out, c.to_xor(), values); break;
default: UNREACHABLE(); break;
}
}
void ba_solver::display(std::ostream& out, pb const& p, bool values) const {
@ -711,44 +682,6 @@ namespace sat {
}
}
void ba_solver::assign(xor& x, literal lit) {
SASSERT(!inconsistent());
switch (value(lit)) {
case l_true:
break;
case l_false:
set_conflict(x, lit);
SASSERT(inconsistent());
break;
default:
m_stats.m_num_xor_propagations++;
m_num_propagations_since_pop++;
if (get_config().m_drat) {
svector<drat::premise> ps;
literal_vector lits;
if (x.lit() != null_literal) lits.push_back(~x.lit());
for (unsigned i = 1; i < x.size(); ++i) {
lits.push_back(x[i]);
}
lits.push_back(lit);
ps.push_back(drat::premise(drat::s_ext(), x.lit()));
drat_add(lits, ps);
}
TRACE("sat", display(tout << lit << " ", x, true););
assign(lit, justification::mk_ext_justification(x.index()));
break;
}
}
void ba_solver::set_conflict(xor& x, literal lit) {
m_stats.m_num_xor_conflicts++;
TRACE("sat", display(tout, x, true); );
if (value(lit) == l_true) lit.neg();
SASSERT(validate_conflict(x));
TRACE("sat", display(tout << lit << " ", x, true););
set_conflict(justification::mk_ext_justification(x.index()), ~lit);
SASSERT(inconsistent());
}
lbool ba_solver::add_assign(xor& x, literal alit) {
// literal is assigned
@ -854,6 +787,8 @@ namespace sat {
m_active_vars.reset();
}
static bool _debug_conflict = false;
bool ba_solver::resolve_conflict() {
if (0 == m_num_propagations_since_pop) {
return false;
@ -879,6 +814,8 @@ namespace sat {
vector<justification> jus;
// if (null_literal != consequent) std::cout << "resolve " << consequent << " " << value(consequent) << "\n";
do {
if (offset == 0) {
@ -900,6 +837,11 @@ namespace sat {
DEBUG_CODE(justification2pb(js, consequent, offset, m_B););
if (_debug_conflict) {
std::cout << consequent << "\n";
s().display_justification(std::cout, js);
std::cout << "\n";
}
switch(js.get_kind()) {
case justification::NONE:
SASSERT (consequent != null_literal);
@ -940,12 +882,12 @@ namespace sat {
}
case justification::EXT_JUSTIFICATION: {
constraint& cnstr = index2constraint(js.get_ext_justification_idx());
++m_stats.m_num_resolves;
switch (cnstr.tag()) {
case card_t: {
card& c = cnstr.to_card();
m_bound += offset * c.k();
process_card(c, offset);
++m_stats.m_num_card_resolves;
break;
}
case pb_t: {
@ -953,10 +895,13 @@ namespace sat {
m_lemma.reset();
m_bound += offset;
inc_coeff(consequent, offset);
get_pb_antecedents(consequent, p, m_lemma);
get_antecedents(consequent, p, m_lemma);
TRACE("sat", display(tout, p, true); tout << m_lemma << "\n";);
if (_debug_conflict) {
std::cout << consequent << " ";
std::cout << "antecedents: " << m_lemma << "\n";
}
for (literal l : m_lemma) process_antecedent(~l, offset);
++m_stats.m_num_pb_resolves;
break;
}
case xor_t: {
@ -966,7 +911,6 @@ namespace sat {
inc_coeff(consequent, offset);
get_xor_antecedents(consequent, idx, js, m_lemma);
for (literal l : m_lemma) process_antecedent(~l, offset);
++m_stats.m_num_xor_resolves;
break;
}
default:
@ -1118,6 +1062,19 @@ namespace sat {
s().reset_mark(v);
--m_num_marks;
}
if (idx == 0 && !_debug_conflict) {
_debug_conflict = true;
// s().display(std::cout);
std::cout << s().m_not_l << "\n";
for (literal l : lits) {
if (s().is_marked(l.var())) {
std::cout << "missing mark: " << l << "\n";
s().reset_mark(l.var());
}
}
m_num_marks = 0;
resolve_conflict();
}
--idx;
}
return false;
@ -1185,7 +1142,8 @@ namespace sat {
}
void ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(lit, lits, k);
void * mem = m_allocator.allocate(card::get_obj_size(lits.size()));
card* c = new (mem) card(lit, lits, k);
add_constraint(c);
}
@ -1222,7 +1180,8 @@ namespace sat {
}
void ba_solver::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k) {
pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(lit, wlits, k);
void * mem = m_allocator.allocate(pb::get_obj_size(wlits.size()));
pb* p = new (mem) pb(lit, wlits, k);
add_constraint(p);
}
@ -1236,7 +1195,8 @@ namespace sat {
}
void ba_solver::add_xor(literal lit, literal_vector const& lits) {
xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(lit, lits);
void * mem = m_allocator.allocate(xor::get_obj_size(lits.size()));
xor* x = new (mem) xor(lit, lits);
add_constraint(x);
for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this.
}
@ -1287,7 +1247,6 @@ namespace sat {
unsigned level = lvl(l);
bool_var v = l.var();
SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION);
SASSERT(index2constraint(index).is_xor());
TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";);
unsigned num_marks = 0;
@ -1362,24 +1321,47 @@ namespace sat {
TRACE("sat", tout << r << "\n";);
}
void ba_solver::get_pb_antecedents(literal l, pb const& p, literal_vector& r) {
void ba_solver::get_antecedents(literal l, pb const& p, literal_vector& r) {
if (p.lit() != null_literal) r.push_back(p.lit());
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
TRACE("sat", display(tout, p, true););
if (value(l) == l_false) {
// The literal comes from a conflict.
// it is forced true, but assigned to false.
unsigned slack = 0;
unsigned miss = 0;
unsigned worth = 0;
unsigned k = p.k();
for (wliteral wl : p) {
literal lit = wl.second;
if (lit != l && value(lit) == l_false) {
r.push_back(~lit);
if (lit == l) {
worth = wl.first;
}
else if (value(lit) == l_false) {
miss += wl.first;
}
}
else {
slack += wl.first;
}
}
SASSERT(slack < k);
SASSERT(0 < worth);
slack += worth;
for (wliteral wl : p) {
literal lit = wl.second;
if (lit != l && value(lit) == l_false) {
unsigned w = wl.first;
if (slack + w >= k) {
r.push_back(~lit);
}
else {
slack += w;
std::cout << "increase slack by " << w << " to " << slack << " worth: " << worth << "\n";
}
}
}
#if 0
std::cout << p << "\n";
std::cout << r << "\n";
@ -1388,7 +1370,6 @@ namespace sat {
return;
}
// unsigned coeff = get_coeff(p, l);
unsigned coeff = 0;
for (unsigned j = 0; j < p.num_watch(); ++j) {
if (p[j].second == l) {
@ -1396,6 +1377,11 @@ namespace sat {
break;
}
}
if (_debug_conflict) {
std::cout << p << "\n";
std::cout << l << " " << coeff << " num_watch: " << p.num_watch() << "\n";
}
CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true););
@ -1423,7 +1409,7 @@ namespace sat {
// no-op
}
void ba_solver::get_card_antecedents(literal l, card const& c, literal_vector& r) {
void ba_solver::get_antecedents(literal l, card const& c, literal_vector& r) {
DEBUG_CODE(
bool found = false;
for (unsigned i = 0; !found && i < c.k(); ++i) {
@ -1439,7 +1425,7 @@ namespace sat {
}
}
void ba_solver::get_xor_antecedents(literal l, xor const& x, literal_vector& r) {
void ba_solver::get_antecedents(literal l, xor const& x, literal_vector& r) {
if (x.lit() != null_literal) r.push_back(x.lit());
// TRACE("sat", display(tout << l << " ", x, true););
SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
@ -1459,15 +1445,68 @@ namespace sat {
}
void ba_solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
constraint& c = index2constraint(idx);
get_antecedents(l, index2constraint(idx), r);
}
void ba_solver::get_antecedents(literal l, constraint const& c, literal_vector& r) {
switch (c.tag()) {
case card_t: get_card_antecedents(l, c.to_card(), r); break;
case pb_t: get_pb_antecedents(l, c.to_pb(), r); break;
case xor_t: get_xor_antecedents(l, c.to_xor(), r); break;
case card_t: get_antecedents(l, c.to_card(), r); break;
case pb_t: get_antecedents(l, c.to_pb(), r); break;
case xor_t: get_antecedents(l, c.to_xor(), r); break;
default: UNREACHABLE(); break;
}
}
bool ba_solver::validate_unit_propagation(constraint const& c, literal l) const {
switch (c.tag()) {
case card_t: return validate_unit_propagation(c.to_card(), l);
case pb_t: return validate_unit_propagation(c.to_pb(), l);
case xor_t: return true;
default: UNREACHABLE(); break;
}
return false;
}
bool ba_solver::validate_conflict(constraint const& c) const {
switch (c.tag()) {
case card_t: return validate_conflict(c.to_card());
case pb_t: return validate_conflict(c.to_pb());
case xor_t: return validate_conflict(c.to_xor());
default: UNREACHABLE(); break;
}
return false;
}
/**
\brief Lex on (glue, size)
*/
struct constraint_glue_lt {
bool operator()(ba_solver::constraint const * c1, ba_solver::constraint const * c2) const {
return
(c1->glue() < c2->glue()) ||
(c1->glue() == c2->glue() && c1->size() < c2->size());
}
};
void ba_solver::gc() {
std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_lt());
gc_half("glue");
cleanup_constraints(m_learned);
}
void ba_solver::gc_half(char const* st_name) {
TRACE("sat", tout << "gc\n";);
unsigned sz = m_learned.size();
unsigned new_sz = sz/2;
unsigned j = new_sz;
for (unsigned i = new_sz; i < sz; i++) {
remove_constraint(*(m_learned[i]));
}
m_learned.shrink(j);
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - j) << ")\n";);
}
void ba_solver::nullify_tracking_literal(constraint& c) {
if (c.lit() != null_literal) {
get_wlist(c.lit()).erase(watched(c.index()));
@ -1476,9 +1515,21 @@ namespace sat {
}
}
void ba_solver::remove_constraint(card& c) {
clear_watch(c);
void ba_solver::remove_constraint(constraint& c) {
nullify_tracking_literal(c);
switch (c.tag()) {
case card_t:
clear_watch(c.to_card());
break;
case pb_t:
clear_watch(c.to_pb());
break;
case xor_t:
clear_watch(c.to_xor());
break;
default:
UNREACHABLE();
}
c.remove();
m_constraint_removed = true;
}
@ -1616,9 +1667,7 @@ namespace sat {
// assigned l_true.
if (index != bound) {
c.swap(index, bound);
}
SASSERT(validate_unit_propagation(c));
}
for (unsigned i = 0; i < bound && !inconsistent(); ++i) {
assign(c, c[i]);
}
@ -1639,23 +1688,11 @@ namespace sat {
void ba_solver::pop_constraint() {
constraint* c = m_constraints.back();
m_constraints.pop_back();
nullify_tracking_literal(*c);
switch (c->tag()) {
case card_t:
clear_watch(c->to_card());
break;
case pb_t:
clear_watch(c->to_pb());
break;
case xor_t:
clear_watch(c->to_xor());
break;
default:
UNREACHABLE();
}
dealloc(c);
remove_constraint(*c);
m_allocator.deallocate(c->obj_size(), c);
}
void ba_solver::pop(unsigned n) {
TRACE("sat_verbose", tout << "pop:" << n << "\n";);
unsigned new_lim = m_constraint_lim.size() - n;
@ -1693,7 +1730,15 @@ namespace sat {
m_constraint_removed = false;
trail_sz = s().init_trail_size();
for (constraint* c : m_constraints) simplify(*c);
gc();
init_use_lists();
remove_unused_defs();
// take ownership of interface variables
for (constraint* c : m_constraints) {
if (c->lit() != null_literal) m_var_used[c->lit().var()] = true;
}
set_non_external();
elim_pure();
subsumption();
cleanup_clauses();
cleanup_constraints();
}
@ -1910,15 +1955,17 @@ namespace sat {
return;
}
p.update_size(sz);
p.update_k(k);
for (unsigned i = 0; i < sz; ++i) {
wliteral wl = p[i];
unsigned w = std::min(k, wl.first);
p[i] = wliteral(w, wl.second);
}
p.update_size(sz);
p.update_k(k);
p.update_max_sum();
literal root = null_literal;
if (p.lit() != null_literal) root = m_roots[p.lit().index()];
@ -2000,9 +2047,7 @@ namespace sat {
- resolution
- blocked literals
*/
void ba_solver::gc() {
// remove constraints where indicator literal isn't used.
void ba_solver::init_use_lists() {
m_visited.resize(s().num_vars()*2, false);
m_clause_use_list.init(s().num_vars());
m_var_used.reset();
@ -2051,6 +2096,10 @@ namespace sat {
}
}
}
}
void ba_solver::remove_unused_defs() {
// remove constraints where indicator literal isn't used.
for (constraint* cp : m_constraints) {
switch (cp->tag()) {
case card_t: {
@ -2081,12 +2130,9 @@ namespace sat {
break;
}
}
}
// take ownership of interface variables
for (constraint* cp : m_constraints) {
if (cp->lit() != null_literal) m_var_used[cp->lit().var()] = true;
}
unsigned ba_solver::set_non_external() {
// set variables to be non-external if they are not used in theory constraints.
unsigned ext = 0;
for (unsigned v = 0; v < s().num_vars(); ++v) {
@ -2095,7 +2141,11 @@ namespace sat {
++ext;
}
}
IF_VERBOSE(10, verbose_stream() << "non-external variables converted: " << ext << "\n";);
return ext;
}
unsigned ba_solver::elim_pure() {
// eliminate pure literals
unsigned pure_literals = 0;
for (unsigned v = 0; v < s().num_vars(); ++v) {
@ -2113,10 +2163,11 @@ namespace sat {
++pure_literals;
}
}
IF_VERBOSE(10,
verbose_stream() << "non-external variables converted: " << ext << "\n";
verbose_stream() << "pure literals converted: " << pure_literals << "\n";);
IF_VERBOSE(10, verbose_stream() << "pure literals converted: " << pure_literals << "\n";);
return pure_literals;
}
void ba_solver::subsumption() {
unsigned bin_sub = m_stats.m_num_bin_subsumes;
unsigned clause_sub = m_stats.m_num_clause_subsumes;
unsigned card_sub = m_stats.m_num_card_subsumes;
@ -2163,13 +2214,19 @@ namespace sat {
void ba_solver::cleanup_constraints() {
if (!m_constraint_removed) return;
ptr_vector<constraint>::iterator it = m_constraints.begin();
cleanup_constraints(m_constraints);
cleanup_constraints(m_learned);
m_constraint_removed = false;
}
void ba_solver::cleanup_constraints(ptr_vector<constraint>& cs) {
ptr_vector<constraint>::iterator it = cs.begin();
ptr_vector<constraint>::iterator it2 = it;
ptr_vector<constraint>::iterator end = m_constraints.end();
ptr_vector<constraint>::iterator end = cs.end();
for (; it != end; ++it) {
constraint& c = *(*it);
if (c.was_removed()) {
dealloc(&c);
m_allocator.deallocate(c.obj_size(), &c);
}
else {
if (it != it2) {
@ -2178,8 +2235,7 @@ namespace sat {
++it2;
}
}
m_constraints.set_end(it2);
m_constraint_removed = false;
cs.set_end(it2);
}
/*
@ -2517,54 +2573,74 @@ namespace sat {
}
void ba_solver::collect_statistics(statistics& st) const {
st.update("cardinality propagations", m_stats.m_num_card_propagations);
st.update("cardinality conflicts", m_stats.m_num_card_conflicts);
st.update("cardinality resolves", m_stats.m_num_card_resolves);
st.update("xor propagations", m_stats.m_num_xor_propagations);
st.update("xor conflicts", m_stats.m_num_xor_conflicts);
st.update("xor resolves", m_stats.m_num_xor_resolves);
st.update("pb propagations", m_stats.m_num_pb_propagations);
st.update("pb conflicts", m_stats.m_num_pb_conflicts);
st.update("pb resolves", m_stats.m_num_pb_resolves);
st.update("ba propagations", m_stats.m_num_propagations);
st.update("ba conflicts", m_stats.m_num_conflicts);
st.update("ba resolves", m_stats.m_num_resolves);
}
bool ba_solver::validate_conflict(card& c) {
if (!validate_unit_propagation(c)) return false;
bool ba_solver::validate_conflict(card const& c) const {
if (c.lit() != null_literal && value(c.lit()) != l_true) {
return false;
}
for (unsigned i = c.k(); i < c.size(); ++i) {
if (value(c[i]) != l_false) return false;
}
for (unsigned i = 0; i < c.k(); ++i) {
if (value(c[i]) == l_false) return true;
}
return false;
}
bool ba_solver::validate_conflict(xor& x) {
bool ba_solver::validate_conflict(xor const& x) const {
return !parity(x, 0);
}
bool ba_solver::validate_unit_propagation(card const& c) {
bool ba_solver::validate_conflict(pb const& p) const {
unsigned slack = 0;
for (wliteral wl : p) {
if (value(wl.second) != l_false) {
slack += wl.first;
}
}
return slack < p.k();
}
bool ba_solver::validate_unit_propagation(card const& c, literal alit) const {
(void) alit;
if (c.lit() != null_literal && value(c.lit()) != l_true) return false;
for (unsigned i = c.k(); i < c.size(); ++i) {
if (value(c[i]) != l_false) return false;
}
return true;
}
bool ba_solver::validate_unit_propagation(pb const& p, literal alit) {
bool ba_solver::validate_unit_propagation(pb const& p, literal alit) const {
if (p.lit() != null_literal && value(p.lit()) != l_true) return false;
unsigned sum = 0;
TRACE("sat", display(tout << "validate: " << alit << "\n", p, true););
for (unsigned i = 0; i < p.size(); ++i) {
literal lit = p[i].second;
for (wliteral wl : p) {
literal lit = wl.second;
lbool val = value(lit);
if (val != l_false && lit != alit) {
sum += p[i].first;
sum += wl.first;
}
}
return sum < p.k();
}
bool ba_solver::validate_unit_propagation(xor const& x, literal alit) const {
if (value(x.lit()) != l_true) return false;
for (unsigned i = 1; i < x.size(); ++i) {
if (value(x[i]) == l_undef) return false;
}
return true;
}
bool ba_solver::validate_lemma() {
int val = -m_bound;
normalize_active_coeffs();
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
for (bool_var v : m_active_vars) {
int coeff = get_coeff(v);
literal lit(v, false);
SASSERT(coeff != 0);
@ -2582,8 +2658,7 @@ namespace sat {
void ba_solver::active2pb(ineq& p) {
normalize_active_coeffs();
p.reset(m_bound);
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
for (bool_var v : m_active_vars) {
literal lit(v, get_coeff(v) < 0);
p.m_lits.push_back(lit);
p.m_coeffs.push_back(get_abs_coeff(v));
@ -2610,9 +2685,7 @@ namespace sat {
case justification::CLAUSE: {
ineq.reset(offset);
clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++)
ineq.push(c[i], offset);
for (literal l : c) ineq.push(l, offset);
break;
}
case justification::EXT_JUSTIFICATION: {
@ -2622,29 +2695,23 @@ namespace sat {
case card_t: {
card& c = cnstr.to_card();
ineq.reset(offset*c.k());
for (unsigned i = 0; i < c.size(); ++i) {
ineq.push(c[i], offset);
}
for (literal l : c) ineq.push(l, offset);
if (c.lit() != null_literal) ineq.push(~c.lit(), offset*c.k());
break;
}
case pb_t: {
pb& p = cnstr.to_pb();
ineq.reset(p.k());
for (unsigned i = 0; i < p.size(); ++i) {
ineq.push(p[i].second, p[i].first);
}
for (wliteral wl : p) ineq.push(wl.second, wl.first);
if (p.lit() != null_literal) ineq.push(~p.lit(), p.k());
break;
}
case xor_t: {
xor& x = cnstr.to_xor();
literal_vector ls;
get_xor_antecedents(lit, x, ls);
get_antecedents(lit, x, ls);
ineq.reset(offset);
for (unsigned i = 0; i < ls.size(); ++i) {
ineq.push(~ls[i], offset);
}
for (literal l : ls) ineq.push(~l, offset);
literal lxor = x.lit();
if (lxor != null_literal) ineq.push(~lxor, offset);
break;
@ -2729,13 +2796,13 @@ namespace sat {
}
bool ba_solver::validate_conflict(literal_vector const& lits, ineq& p) {
for (unsigned i = 0; i < lits.size(); ++i) {
if (value(lits[i]) != l_false) {
TRACE("sat", tout << "literal " << lits[i] << " is not false\n";);
for (literal l : lits) {
if (value(l) != l_false) {
TRACE("sat", tout << "literal " << l << " is not false\n";);
return false;
}
}
unsigned value = 0;
unsigned value = 0;
for (unsigned i = 0; i < p.m_lits.size(); ++i) {
unsigned coeff = p.m_coeffs[i];
if (!lits.contains(p.m_lits[i])) {

84
src/sat/ba_solver.h
View file

@ -32,15 +32,9 @@ namespace sat {
friend class local_search;
struct stats {
unsigned m_num_card_propagations;
unsigned m_num_card_conflicts;
unsigned m_num_card_resolves;
unsigned m_num_xor_propagations;
unsigned m_num_xor_conflicts;
unsigned m_num_xor_resolves;
unsigned m_num_pb_propagations;
unsigned m_num_pb_conflicts;
unsigned m_num_pb_resolves;
unsigned m_num_propagations;
unsigned m_num_conflicts;
unsigned m_num_resolves;
unsigned m_num_bin_subsumes;
unsigned m_num_clause_subsumes;
unsigned m_num_card_subsumes;
@ -64,9 +58,11 @@ namespace sat {
tag_t m_tag;
bool m_removed;
literal m_lit;
unsigned m_glue;
unsigned m_size;
size_t m_obj_size;
public:
constraint(tag_t t, literal l, unsigned sz): m_tag(t), m_removed(false), m_lit(l), m_size(sz) {}
constraint(tag_t t, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_size(sz), m_obj_size(osz) {}
ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
tag_t tag() const { return m_tag; }
literal lit() const { return m_lit; }
@ -76,8 +72,10 @@ namespace sat {
bool was_removed() const { return m_removed; }
void remove() { m_removed = true; }
void nullify_literal() { m_lit = null_literal; }
unsigned glue() const { return m_glue; }
void set_glue(unsigned g) { m_glue = g; }
size_t obj_size() const { return m_obj_size; }
card& to_card();
pb& to_pb();
xor& to_xor();
@ -117,7 +115,6 @@ namespace sat {
unsigned m_num_watch;
unsigned m_max_sum;
wliteral m_wlits[0];
void update_max_sum();
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); }
pb(literal lit, svector<wliteral> const& wlits, unsigned k);
@ -136,6 +133,7 @@ namespace sat {
void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
void negate();
void update_k(unsigned k) { m_k = k; }
void update_max_sum();
literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
};
@ -162,14 +160,15 @@ namespace sat {
void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); }
};
solver* m_solver;
lookahead* m_lookahead;
stats m_stats;
solver* m_solver;
lookahead* m_lookahead;
stats m_stats;
small_object_allocator m_allocator;
ptr_vector<constraint> m_constraints;
// watch literals
unsigned_vector m_constraint_lim;
ptr_vector<constraint> m_learned;
unsigned_vector m_constraint_lim;
// conflict resolution
unsigned m_num_marks;
@ -190,8 +189,6 @@ namespace sat {
void inc_parity(bool_var v);
void reset_parity(bool_var v);
void pop_constraint();
solver& s() const { return *m_solver; }
@ -206,7 +203,6 @@ namespace sat {
bool m_constraint_removed;
literal_vector m_roots;
unsigned_vector m_weights;
void gc();
bool subsumes(card& c1, card& c2, literal_vector& comp);
bool subsumes(card& c1, clause& c2, literal_vector& comp);
bool subsumed(card& c1, literal l1, literal l2);
@ -218,11 +214,22 @@ namespace sat {
bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
unsigned get_num_non_learned_bin(literal l);
literal get_min_occurrence_literal(card const& c);
void init_use_lists();
void remove_unused_defs();
unsigned set_non_external();
unsigned elim_pure();
void subsumption();
void subsumption(card& c1);
void gc_half(char const* _method);
void cleanup_clauses();
void cleanup_constraints();
void cleanup_constraints(ptr_vector<constraint>& cs);
void remove_constraint(constraint& c);
// constraints
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); }
void pop_constraint();
void unwatch_literal(literal w, constraint& c);
void watch_literal(literal w, constraint& c);
void watch_literal(wliteral w, pb& p);
@ -232,18 +239,20 @@ namespace sat {
lbool add_assign(constraint& c, literal l);
void simplify(constraint& c);
void nullify_tracking_literal(constraint& c);
void set_conflict(constraint& c, literal lit);
void assign(constraint& c, literal lit);
void get_antecedents(literal l, constraint const& c, literal_vector & r);
bool validate_conflict(constraint const& c) const;
bool validate_unit_propagation(constraint const& c, literal alit) const;
// cardinality
void init_watch(card& c, bool is_true);
void assign(card& c, literal lit);
lbool add_assign(card& c, literal lit);
void set_conflict(card& c, literal lit);
void clear_watch(card& c);
void reset_coeffs();
void reset_marked_literals();
void get_card_antecedents(literal l, card const& c, literal_vector & r);
void get_antecedents(literal l, card const& c, literal_vector & r);
void simplify(card& c);
void remove_constraint(card& c);
void unit_propagation_simplification(literal lit, literal_vector const& lits);
void flush_roots(card& c);
void recompile(card& c);
@ -251,34 +260,27 @@ namespace sat {
// xor specific functionality
void clear_watch(xor& x);
void init_watch(xor& x, bool is_true);
void assign(xor& x, literal lit);
void set_conflict(xor& x, literal lit);
bool parity(xor const& x, unsigned offset) const;
lbool add_assign(xor& x, literal alit);
void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
void get_xor_antecedents(literal l, xor const& x, literal_vector & r);
void get_antecedents(literal l, xor const& x, literal_vector & r);
void simplify(xor& x);
void flush_roots(xor& x);
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); }
// pb functionality
unsigned m_a_max;
void init_watch(pb& p, bool is_true);
lbool add_assign(pb& p, literal alit);
void add_index(pb& p, unsigned index, literal lit);
void clear_watch(pb& p);
void set_conflict(pb& p, literal lit);
void assign(pb& p, literal l);
void get_pb_antecedents(literal l, pb const& p, literal_vector & r);
void get_antecedents(literal l, pb const& p, literal_vector & r);
void simplify(pb& p);
void simplify2(pb& p);
bool is_cardinality(pb const& p);
void remove_constraint(pb& p);
void flush_roots(pb& p);
void recompile(pb& p);
// access solver
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }
inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); }
@ -301,12 +303,14 @@ namespace sat {
void cut();
// validation utilities
bool validate_conflict(card& c);
bool validate_conflict(xor& x);
bool validate_conflict(card const& c) const;
bool validate_conflict(xor const& x) const;
bool validate_conflict(pb const& p) const;
bool validate_assign(literal_vector const& lits, literal lit);
bool validate_lemma();
bool validate_unit_propagation(card const& c);
bool validate_unit_propagation(pb const& p, literal lit);
bool validate_unit_propagation(card const& c, literal alit) const;
bool validate_unit_propagation(pb const& p, literal alit) const;
bool validate_unit_propagation(xor const& x, literal alit) const;
bool validate_conflict(literal_vector const& lits, ineq& p);
ineq m_A, m_B, m_C;
@ -315,6 +319,7 @@ namespace sat {
bool validate_resolvent();
void display(std::ostream& out, ineq& p) const;
void display(std::ostream& out, constraint const& c, bool values) const;
void display(std::ostream& out, card const& c, bool values) const;
void display(std::ostream& out, pb const& p, bool values) const;
void display(std::ostream& out, xor const& c, bool values) const;
@ -349,6 +354,7 @@ namespace sat {
virtual void collect_statistics(statistics& st) const;
virtual extension* copy(solver* s);
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes);
virtual void gc();
ptr_vector<constraint> const & constraints() const { return m_constraints; }

1
src/sat/sat_extension.h
View file

@ -52,6 +52,7 @@ namespace sat {
virtual void collect_statistics(statistics& st) const = 0;
virtual extension* copy(solver* s) = 0;
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
virtual void gc() = 0;
};
};

57
src/sat/sat_solver.cpp
View file

@ -1641,6 +1641,7 @@ namespace sat {
UNREACHABLE();
break;
}
if (m_ext) m_ext->gc();
m_conflicts_since_gc = 0;
m_gc_threshold += m_config.m_gc_increment;
CASSERT("sat_gc_bug", check_invariant());
@ -3148,26 +3149,16 @@ namespace sat {
}
unsigned solver::num_clauses() const {
unsigned num_cls = 0;
num_cls += m_trail.size(); // units;
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l = ~to_literal(l_idx);
watch_list const & wlist = *it;
watch_list::const_iterator it2 = wlist.begin();
watch_list::const_iterator end2 = wlist.end();
for (; it2 != end2; ++it2) {
if (it2->is_binary_clause() && l.index() < it2->get_literal().index())
unsigned num_cls = m_trail.size(); // units;
unsigned l_idx = 0;
for (auto const& wl : m_watches) {
literal l = ~to_literal(l_idx++);
for (auto const& w : wl) {
if (w.is_binary_clause() && l.index() < w.get_literal().index())
num_cls++;
}
}
clause_vector const * vs[2] = { &m_clauses, &m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector const & cs = *(vs[i]);
num_cls += cs.size();
}
return num_cls;
return num_cls + m_clauses.size() + m_learned.size();
}
void solver::display_dimacs(std::ostream & out) const {
@ -3175,28 +3166,21 @@ namespace sat {
for (unsigned i = 0; i < m_trail.size(); i++) {
out << dimacs_lit(m_trail[i]) << " 0\n";
}
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l = ~to_literal(l_idx);
watch_list const & wlist = *it;
watch_list::const_iterator it2 = wlist.begin();
watch_list::const_iterator end2 = wlist.end();
for (; it2 != end2; ++it2) {
if (it2->is_binary_clause() && l.index() < it2->get_literal().index())
out << dimacs_lit(l) << " " << dimacs_lit(it2->get_literal()) << " 0\n";
unsigned l_idx = 0;
for (auto const& wlist : m_watches) {
literal l = ~to_literal(l_idx++);
for (auto const& w : wlist) {
if (w.is_binary_clause() && l.index() < w.get_literal().index())
out << dimacs_lit(l) << " " << dimacs_lit(w.get_literal()) << " 0\n";
}
}
clause_vector const * vs[2] = { &m_clauses, &m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector const & cs = *(vs[i]);
clause_vector::const_iterator it = cs.begin();
clause_vector::const_iterator end = cs.end();
for (; it != end; ++it) {
clause const & c = *(*it);
unsigned sz = c.size();
for (unsigned j = 0; j < sz; j++)
out << dimacs_lit(c[j]) << " ";
for (auto cp : cs) {
for (literal l : *cp) {
out << dimacs_lit(l) << " ";
}
out << "0\n";
}
}
@ -3269,9 +3253,8 @@ namespace sat {
*/
bool solver::is_unit(clause const & c) const {
bool found_undef = false;
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
switch (value(c[i])) {
for (literal l : c) {
switch (value(l)) {
case l_undef:
if (found_undef)
return false;