mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-01-30 18:42:53 -08:00
commit 1a95c33775
26 changed files with 1307 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

803
src/sat/card_extension.cpp Normal file
View file

@ -0,0 +1,803 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
card_extension.cpp
Abstract:
Extension for cardinality reasoning.
Author:
Nikolaj Bjorner (nbjorner) 2017-01-30
Revision History:
--*/
#include"card_extension.h"
#include"sat_types.h"
namespace sat {
card_extension::card::card(unsigned index, literal lit, literal_vector const& lits, unsigned k):
m_index(index),
m_lit(lit),
m_k(k),
m_size(lits.size()),
m_lits(lits) {
}
void card_extension::card::negate() {
m_lit.neg();
for (unsigned i = 0; i < m_size; ++i) {
m_lits[i].neg();
}
m_k = m_size - m_k + 1;
SASSERT(m_size >= m_k && m_k > 0);
}
void card_extension::init_watch(bool_var v) {
if (m_var_infos.size() <= static_cast<unsigned>(v)) {
m_var_infos.resize(static_cast<unsigned>(v)+100);
}
}
void card_extension::init_watch(card& c, bool is_true) {
clear_watch(c);
if (c.lit().sign() == is_true) {
c.negate();
}
SASSERT(value(c.lit()) == l_true);
unsigned j = 0, sz = c.size(), bound = c.k();
if (bound == sz) {
for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
assign(c, c[i]);
}
return;
}
// put the non-false literals into the head.
for (unsigned i = 0; i < sz; ++i) {
if (value(c[i]) != l_false) {
if (j != i) {
c.swap(i, j);
}
++j;
}
}
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;
});
// j is the number of non-false, sz - j the number of false.
if (j < bound) {
SASSERT(0 < bound && bound < sz);
literal alit = c[j];
//
// we need the assignment level of the asserting literal to be maximal.
// such that conflict resolution can use the asserting literal as a starting
// point.
//
for (unsigned i = bound; i < sz; ++i) {
if (lvl(alit) < lvl(c[i])) {
c.swap(i, j);
alit = c[j];
}
}
set_conflict(c, alit);
}
else if (j == bound) {
for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
assign(c, c[i]);
}
}
else {
for (unsigned i = 0; i <= bound; ++i) {
watch_literal(c, c[i]);
}
}
}
void card_extension::clear_watch(card& c) {
unsigned sz = std::min(c.k() + 1, c.size());
for (unsigned i = 0; i < sz; ++i) {
unwatch_literal(c[i], &c);
}
}
void card_extension::unwatch_literal(literal lit, card* c) {
if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
return;
}
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
if (cards) {
remove(*cards, c);
}
}
void card_extension::remove(ptr_vector<card>& cards, card* c) {
for (unsigned j = 0; j < cards.size(); ++j) {
if (cards[j] == c) {
std::swap(cards[j], cards[cards.size()-1]);
cards.pop_back();
break;
}
}
}
void card_extension::assign(card& c, literal lit) {
if (value(lit) == l_true) {
return;
}
m_stats.m_num_propagations++;
//TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
SASSERT(validate_unit_propagation(c));
s().assign(lit, justification::mk_ext_justification(c.index()));
}
void card_extension::watch_literal(card& c, literal lit) {
init_watch(lit.var());
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
if (cards == 0) {
cards = alloc(ptr_vector<card>);
m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;
}
cards->push_back(&c);
}
void card_extension::set_conflict(card& c, literal lit) {
SASSERT(validate_conflict(c));
m_stats.m_num_conflicts++;
if (!resolve_conflict(c, lit)) {
literal_vector& lits = get_literals();
SASSERT(value(lit) == l_false);
SASSERT(value(c.lit()) == l_true);
lits.push_back(~c.lit());
lits.push_back(lit);
unsigned sz = c.size();
for (unsigned i = c.k(); i < sz; ++i) {
SASSERT(value(c[i]) == l_false);
lits.push_back(c[i]);
}
s().mk_clause_core(lits.size(), lits.c_ptr(), true);
}
SASSERT(s().inconsistent());
}
void card_extension::normalize_active_coeffs() {
while (!m_active_var_set.empty()) m_active_var_set.erase();
unsigned i = 0, j = 0, sz = m_active_vars.size();
for (; i < sz; ++i) {
bool_var v = m_active_vars[i];
if (!m_active_var_set.contains(v) && get_coeff(v) != 0) {
m_active_var_set.insert(v);
if (j != i) {
m_active_vars[j] = m_active_vars[i];
}
++j;
}
}
sz = j;
m_active_vars.shrink(sz);
}
void card_extension::inc_coeff(literal l, int offset) {
SASSERT(offset > 0);
bool_var v = l.var();
SASSERT(v != null_bool_var);
if (static_cast<bool_var>(m_coeffs.size()) <= v) {
m_coeffs.resize(v + 1, 0);
}
int coeff0 = m_coeffs[v];
if (coeff0 == 0) {
m_active_vars.push_back(v);
}
int inc = l.sign() ? -offset : offset;
int coeff1 = inc + coeff0;
m_coeffs[v] = coeff1;
if (coeff0 > 0 && inc < 0) {
m_bound -= coeff0 - std::max(0, coeff1);
}
else if (coeff0 < 0 && inc > 0) {
m_bound -= std::min(0, coeff1) - coeff0;
}
}
int card_extension::get_coeff(bool_var v) const {
return m_coeffs.get(v, 0);
}
int card_extension::get_abs_coeff(bool_var v) const {
int coeff = get_coeff(v);
if (coeff < 0) coeff = -coeff;
return coeff;
}
void card_extension::reset_coeffs() {
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
m_coeffs[m_active_vars[i]] = 0;
}
m_active_vars.reset();
}
bool card_extension::resolve_conflict(card& c, literal alit) {
bool_var v;
m_conflict_lvl = 0;
for (unsigned i = 0; i < c.size(); ++i) {
literal lit = c[i];
SASSERT(value(lit) == l_false);
m_conflict_lvl = std::max(m_conflict_lvl, lvl(lit));
}
if (m_conflict_lvl < lvl(c.lit()) || m_conflict_lvl == 0) {
return false;
}
reset_coeffs();
m_num_marks = 0;
m_bound = c.k();
m_conflict.reset();
literal_vector const& lits = s().m_trail;
unsigned idx = lits.size()-1;
justification js;
literal consequent = ~alit;
process_card(c, 1);
DEBUG_CODE(active2pb(m_A););
while (m_num_marks > 0) {
SASSERT(value(consequent) == l_true);
v = consequent.var();
int offset = get_abs_coeff(v);
if (offset == 0) {
goto process_next_resolvent;
}
if (offset > 1000) {
goto bail_out;
}
SASSERT(validate_lemma());
SASSERT(offset > 0);
js = s().m_justification[v];
DEBUG_CODE(justification2pb(js, consequent, offset, m_B););
int bound = 1;
switch(js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
inc_coeff(consequent, offset);
process_antecedent(~(js.get_literal()), offset);
break;
case justification::TERNARY:
inc_coeff(consequent, offset);
process_antecedent(~(js.get_literal1()), offset);
process_antecedent(~(js.get_literal2()), offset);
break;
case justification::CLAUSE: {
inc_coeff(consequent, offset);
clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
unsigned i = 0;
SASSERT(c[0] == consequent || c[1] == consequent);
if (c[0] == consequent) {
i = 1;
}
else {
process_antecedent(~c[0], offset);
i = 2;
}
unsigned sz = c.size();
for (; i < sz; i++)
process_antecedent(~c[i], offset);
break;
}
case justification::EXT_JUSTIFICATION: {
unsigned index = js.get_ext_justification_idx();
card& c2 = *m_constraints[index];
process_card(c2, offset);
bound = c2.k();
break;
}
default:
UNREACHABLE();
break;
}
m_bound += offset * bound;
DEBUG_CODE(
active2pb(m_C);
SASSERT(validate_resolvent());
m_A = m_C;);
// cut();
process_next_resolvent:
// find the next marked variable in the assignment stack
//
while (true) {
consequent = lits[idx];
v = consequent.var();
if (s().is_marked(v)) break;
SASSERT(idx > 0);
--idx;
}
SASSERT(lvl(v) == m_conflict_lvl);
s().reset_mark(v);
--idx;
--m_num_marks;
}
SASSERT(validate_lemma());
normalize_active_coeffs();
if (m_bound > 0 && m_active_vars.empty()) {
return false;
}
int slack = -m_bound;
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
slack += get_abs_coeff(v);
}
alit = get_asserting_literal(~consequent);
slack -= get_abs_coeff(alit.var());
m_conflict.push_back(alit);
for (unsigned i = lits.size(); 0 <= slack && i > 0; ) {
--i;
literal lit = lits[i];
bool_var v = lit.var();
if (m_active_var_set.contains(v) && v != alit.var()) {
int coeff = get_coeff(v);
if (coeff < 0 && !lit.sign()) {
slack += coeff;
m_conflict.push_back(~lit);
}
else if (coeff > 0 && lit.sign()) {
slack -= coeff;
m_conflict.push_back(~lit);
}
}
}
SASSERT(slack < 0);
SASSERT(validate_conflict(m_conflict));
s().mk_clause_core(m_conflict.size(), m_conflict.c_ptr(), true);
return true;
bail_out:
while (m_num_marks > 0 && idx > 0) {
v = lits[idx].var();
if (s().is_marked(v)) {
s().reset_mark(v);
}
--idx;
}
return false;
}
void card_extension::process_card(card& c, int offset) {
SASSERT(c.k() <= c.size());
SASSERT(value(c.lit()) == l_true);
for (unsigned i = c.k(); i < c.size(); ++i) {
process_antecedent(c[i], offset);
}
for (unsigned i = 0; i < c.k(); ++i) {
inc_coeff(c[i], offset);
}
if (lvl(c.lit()) > 0) {
m_conflict.push_back(~c.lit());
}
}
void card_extension::process_antecedent(literal l, int offset) {
SASSERT(value(l) == l_false);
bool_var v = l.var();
unsigned level = lvl(v);
if (level > 0 && !s().is_marked(v) && level == m_conflict_lvl) {
s().mark(v);
++m_num_marks;
}
inc_coeff(l, offset);
}
literal card_extension::get_asserting_literal(literal p) {
if (get_abs_coeff(p.var()) != 0) {
return p;
}
unsigned level = 0;
for (unsigned i = 0; i < m_active_vars.size(); ++i) {
bool_var v = m_active_vars[i];
literal lit(v, get_coeff(v) < 0);
if (value(lit) == l_false && lvl(lit) > level) {
p = lit;
level = lvl(lit);
}
}
return p;
}
card_extension::card_extension(): m_solver(0) {}
card_extension::~card_extension() {
for (unsigned i = 0; i < m_var_infos.size(); ++i) {
m_var_infos[i].reset();
}
m_var_trail.reset();
m_var_lim.reset();
m_stats.reset();
}
void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
unsigned index = m_constraints.size();
card* c = alloc(card, index, literal(v, false), lits, k);
m_constraints.push_back(c);
init_watch(v);
m_var_infos[v].m_card = c;
m_var_trail.push_back(v);
}
void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
UNREACHABLE();
}
void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
card& c = *m_constraints[idx];
DEBUG_CODE(
bool found = false;
for (unsigned i = 0; !found && i < c.k(); ++i) {
found = c[i] == l;
}
SASSERT(found););
r.push_back(c.lit());
SASSERT(value(c.lit()) == l_true);
for (unsigned i = c.k(); i < c.size(); ++i) {
SASSERT(value(c[i]) == l_false);
r.push_back(~c[i]);
}
}
lbool card_extension::add_assign(card& c, literal alit) {
// literal is assigned to false.
unsigned sz = c.size();
unsigned bound = c.k();
TRACE("sat", tout << "assign: " << c.lit() << " " << ~alit << " " << bound << "\n";);
SASSERT(0 < bound && bound < sz);
SASSERT(value(alit) == l_false);
SASSERT(value(c.lit()) == l_true);
unsigned index = 0;
for (index = 0; index <= bound; ++index) {
if (c[index] == alit) {
break;
}
}
if (index == bound + 1) {
// literal is no longer watched.
return l_undef;
}
SASSERT(index <= bound);
SASSERT(c[index] == alit);
// find a literal to swap with:
for (unsigned i = bound + 1; i < sz; ++i) {
literal lit2 = c[i];
if (value(lit2) != l_false) {
c.swap(index, i);
watch_literal(c, lit2);
return l_undef;
}
}
// conflict
if (bound != index && value(c[bound]) == l_false) {
TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";);
set_conflict(c, alit);
return l_false;
}
TRACE("sat", tout << "no swap " << index << " " << alit << "\n";);
// there are no literals to swap with,
// prepare for unit propagation by swapping the false literal into
// position bound. Then literals in positions 0..bound-1 have to be
// assigned l_true.
if (index != bound) {
c.swap(index, bound);
}
SASSERT(validate_unit_propagation(c));
for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
assign(c, c[i]);
}
return s().inconsistent() ? l_false : l_true;
}
void card_extension::asserted(literal l) {
bool_var v = l.var();
ptr_vector<card>* cards = m_var_infos[v].m_lit_watch[!l.sign()];
if (cards != 0 && !cards->empty() && !s().inconsistent()) {
ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
for (; it != end; ++it) {
card& c = *(*it);
if (value(c.lit()) != l_true) {
continue;
}
switch (add_assign(c, l)) {
case l_false: // conflict
for (; it != end; ++it, ++it2) {
*it2 = *it;
}
SASSERT(s().inconsistent());
cards->set_end(it2);
return;
case l_undef: // watch literal was swapped
break;
case l_true: // unit propagation, keep watching the literal
if (it2 != it) {
*it2 = *it;
}
++it2;
break;
}
}
cards->set_end(it2);
}
card* crd = m_var_infos[v].m_card;
if (crd != 0 && !s().inconsistent()) {
init_watch(*crd, !l.sign());
}
}
check_result card_extension::check() { return CR_DONE; }
void card_extension::push() {
m_var_lim.push_back(m_var_trail.size());
}
void card_extension::pop(unsigned n) {
unsigned new_lim = m_var_lim.size() - n;
unsigned sz = m_var_lim[new_lim];
while (m_var_trail.size() > sz) {
bool_var v = m_var_trail.back();
m_var_trail.pop_back();
if (v != null_bool_var) {
card* c = m_var_infos[v].m_card;
clear_watch(*c);
m_var_infos[v].m_card = 0;
dealloc(c);
}
}
m_var_lim.resize(new_lim);
}
void card_extension::simplify() {}
void card_extension::clauses_modifed() {}
lbool card_extension::get_phase(bool_var v) { return l_undef; }
void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const {
watch const* w = m_var_infos[v].m_lit_watch[sign];
if (w) {
watch const& wl = *w;
out << "watch: " << literal(v, sign) << " |-> ";
for (unsigned i = 0; i < wl.size(); ++i) {
out << wl[i]->lit() << " ";
}
out << "\n";
}
}
void card_extension::display(std::ostream& out, card& c, bool values) const {
out << c.lit();
if (c.lit() != null_literal) {
if (values) {
out << "@(" << value(c.lit());
if (value(c.lit()) != l_undef) {
out << ":" << lvl(c.lit());
}
out << ")";
}
out << c.lit() << "\n";
}
else {
out << " ";
}
for (unsigned i = 0; i < c.size(); ++i) {
literal l = c[i];
out << l;
if (values) {
out << "@(" << value(l);
if (value(l) != l_undef) {
out << ":" << lvl(l);
}
out << ") ";
}
}
out << " >= " << c.k() << "\n";
}
std::ostream& card_extension::display(std::ostream& out) const {
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
display_watch(out, vi, false);
display_watch(out, vi, true);
}
for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) {
card* c = m_var_infos[vi].m_card;
if (c) {
display(out, *c, true);
}
}
return out;
}
void card_extension::collect_statistics(statistics& st) const {
st.update("card propagations", m_stats.m_num_propagations);
st.update("card conflicts", m_stats.m_num_conflicts);
}
bool card_extension::validate_conflict(card& c) {
if (!validate_unit_propagation(c)) return false;
for (unsigned i = 0; i < c.k(); ++i) {
if (value(c[i]) == l_false) return true;
}
return false;
}
bool card_extension::validate_unit_propagation(card const& c) {
if (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 card_extension::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];
int coeff = get_coeff(v);
literal lit(v, false);
SASSERT(coeff != 0);
if (coeff < 0 && value(lit) != l_true) {
val -= coeff;
}
else if (coeff > 0 && value(lit) != l_false) {
val += coeff;
}
}
return val < 0;
}
void card_extension::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];
literal lit(v, get_coeff(v) < 0);
p.m_lits.push_back(lit);
p.m_coeffs.push_back(get_abs_coeff(v));
}
}
void card_extension::justification2pb(justification const& js, literal lit, unsigned offset, ineq& p) {
switch (js.get_kind()) {
case justification::NONE:
p.reset(0);
break;
case justification::BINARY:
p.reset(offset);
p.push(lit, offset);
p.push(~js.get_literal(), offset);
break;
case justification::TERNARY:
p.reset(offset);
p.push(lit, offset);
p.push(~(js.get_literal1()), offset);
p.push(~(js.get_literal2()), offset);
break;
case justification::CLAUSE: {
p.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++)
p.push(~c[i], offset);
break;
}
case justification::EXT_JUSTIFICATION: {
unsigned index = js.get_ext_justification_idx();
card& c = *m_constraints[index];
p.reset(offset*c.k());
for (unsigned i = 0; i < c.size(); ++i) {
p.push(c[i], offset);
}
break;
}
default:
UNREACHABLE();
break;
}
}
// validate that m_A & m_B implies m_C
bool card_extension::validate_resolvent() {
u_map<unsigned> coeffs;
unsigned k = m_A.m_k + m_B.m_k;
for (unsigned i = 0; i < m_A.m_lits.size(); ++i) {
unsigned coeff = m_A.m_coeffs[i];
SASSERT(!coeffs.contains(m_A.m_lits[i].index()));
coeffs.insert(m_A.m_lits[i].index(), coeff);
}
for (unsigned i = 0; i < m_B.m_lits.size(); ++i) {
unsigned coeff1 = m_B.m_coeffs[i], coeff2;
literal lit = m_B.m_lits[i];
if (coeffs.find((~lit).index(), coeff2)) {
if (coeff1 == coeff2) {
coeffs.remove((~lit).index());
k += coeff1;
}
else if (coeff1 < coeff2) {
coeffs.insert((~lit).index(), coeff2 - coeff1);
k += coeff1;
}
else {
SASSERT(coeff2 < coeff1);
coeffs.remove((~lit).index());
coeffs.insert(lit.index(), coeff1 - coeff2);
k += coeff2;
}
}
else if (coeffs.find(lit.index(), coeff2)) {
coeffs.insert(lit.index(), coeff1 + coeff2);
}
else {
coeffs.insert(lit.index(), coeff1);
}
}
// C is above the sum of A and B
for (unsigned i = 0; i < m_C.m_lits.size(); ++i) {
literal lit = m_C.m_lits[i];
unsigned coeff;
if (coeffs.find(lit.index(), coeff)) {
SASSERT(coeff <= m_C.m_coeffs[i]);
coeffs.remove(lit.index());
}
}
SASSERT(coeffs.empty());
SASSERT(m_C.m_k <= k);
return true;
}
bool card_extension::validate_conflict(literal_vector const& lits) {
for (unsigned i = 0; i < lits.size(); ++i) {
if (value(lits[i]) != l_false) return false;
}
return true;
}
};

159
src/sat/card_extension.h Normal file
View file

@ -0,0 +1,159 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
card_extension.h
Abstract:
Cardinality extensions.
Author:
Nikolaj Bjorner (nbjorner) 2017-01-30
Revision History:
--*/
#ifndef CARD_EXTENSION_H_
#define CARD_EXTENSION_H_
#include"sat_extension.h"
#include"sat_solver.h"
namespace sat {
class card_extension : public extension {
struct stats {
unsigned m_num_propagations;
unsigned m_num_conflicts;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
class card {
unsigned m_index;
literal m_lit;
unsigned m_k;
unsigned m_size;
literal_vector m_lits;
public:
card(unsigned index, literal lit, literal_vector const& lits, unsigned k);
unsigned index() const { return m_index; }
literal lit() const { return m_lit; }
literal operator[](unsigned i) const { return m_lits[i]; }
unsigned k() const { return m_k; }
unsigned size() const { return m_size; }
void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
void negate();
};
struct ineq {
literal_vector m_lits;
unsigned_vector m_coeffs;
unsigned m_k;
void reset(unsigned k) { m_lits.reset(); m_coeffs.reset(); m_k = k; }
void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); }
};
typedef ptr_vector<card> watch;
struct var_info {
watch* m_lit_watch[2];
card* m_card;
var_info(): m_card(0) {
m_lit_watch[0] = 0;
m_lit_watch[1] = 0;
}
void reset() {
dealloc(m_card);
dealloc(m_lit_watch[0]);
dealloc(m_lit_watch[1]);
}
};
solver* m_solver;
stats m_stats;
ptr_vector<card> m_constraints;
// watch literals
svector<var_info> m_var_infos;
unsigned_vector m_var_trail;
unsigned_vector m_var_lim;
// conflict resolution
unsigned m_num_marks;
unsigned m_conflict_lvl;
svector<int> m_coeffs;
svector<bool_var> m_active_vars;
int m_bound;
tracked_uint_set m_active_var_set;
literal_vector m_conflict;
literal_vector m_literals;
solver& s() const { return *m_solver; }
void init_watch(card& c, bool is_true);
void init_watch(bool_var v);
void assign(card& c, literal lit);
lbool add_assign(card& c, literal lit);
void watch_literal(card& c, literal lit);
void set_conflict(card& c, literal lit);
void clear_watch(card& c);
void reset_coeffs();
inline lbool value(literal lit) const { return 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); }
void unwatch_literal(literal w, card* c);
void remove(ptr_vector<card>& cards, card* c);
void normalize_active_coeffs();
void inc_coeff(literal l, int offset);
int get_coeff(bool_var v) const;
int get_abs_coeff(bool_var v) const;
literal_vector& get_literals() { m_literals.reset(); return m_literals; }
literal get_asserting_literal(literal conseq);
bool resolve_conflict(card& c, literal alit);
void process_antecedent(literal l, int offset);
void process_card(card& c, int offset);
void cut();
// validation utilities
bool validate_conflict(card& c);
bool validate_assign(literal_vector const& lits, literal lit);
bool validate_lemma();
bool validate_unit_propagation(card const& c);
bool validate_conflict(literal_vector const& lits);
ineq m_A, m_B, m_C;
void active2pb(ineq& p);
void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p);
bool validate_resolvent();
void display(std::ostream& out, card& c, bool values) const;
void display_watch(std::ostream& out, bool_var v, bool sign) const;
public:
card_extension();
virtual ~card_extension();
void set_solver(solver* s) { m_solver = s; }
void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
virtual void asserted(literal l);
virtual check_result check();
virtual void push();
virtual void pop(unsigned n);
virtual void simplify();
virtual void clauses_modifed();
virtual lbool get_phase(bool_var v);
virtual std::ostream& display(std::ostream& out) const;
virtual void collect_statistics(statistics& st) const;
};
};
#endif

1
src/sat/sat_config.cpp
View file

@ -77,6 +77,7 @@ namespace sat {
m_burst_search = p.burst_search();
m_max_conflicts = p.max_conflicts();
m_num_parallel = p.parallel_threads();
// These parameters are not exposed
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);

1
src/sat/sat_config.h
View file

@ -57,6 +57,7 @@ namespace sat {
unsigned m_random_seed;
unsigned m_burst_search;
unsigned m_max_conflicts;
unsigned m_num_parallel;
unsigned m_simplify_mult1;
double m_simplify_mult2;

4
src/sat/sat_extension.h
View file

@ -21,6 +21,7 @@ Revision History:
#include"sat_types.h"
#include"params.h"
#include"statistics.h"
namespace sat {
@ -30,6 +31,7 @@ namespace sat {
class extension {
public:
virtual ~extension() {}
virtual void propagate(literal l, ext_constraint_idx idx, bool & keep) = 0;
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
virtual void asserted(literal l) = 0;
@ -39,6 +41,8 @@ namespace sat {
virtual void simplify() = 0;
virtual void clauses_modifed() = 0;
virtual lbool get_phase(bool_var v) = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
virtual void collect_statistics(statistics& st) const = 0;
};
};

2
src/sat/sat_justification.h
View file

@ -33,7 +33,7 @@ namespace sat {
explicit justification(literal l):m_val1(l.to_uint()), m_val2(BINARY) {}
justification(literal l1, literal l2):m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
explicit justification(clause_offset cls_off):m_val1(cls_off), m_val2(CLAUSE) {}
justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
static justification mk_ext_justification(ext_justification_idx idx) { return justification(idx, EXT_JUSTIFICATION); }
kind get_kind() const { return static_cast<kind>(m_val2 & 7); }

59
src/sat/sat_mus.cpp
View file

@ -23,7 +23,7 @@ Notes:
namespace sat {
mus::mus(solver& s):s(s), m_is_active(false),m_restart(0), m_max_restarts(0) {}
mus::mus(solver& s):s(s), m_is_active(false), m_max_num_restarts(UINT_MAX) {}
mus::~mus() {}
@ -31,8 +31,6 @@ namespace sat {
m_core.reset();
m_mus.reset();
m_model.reset();
m_max_restarts = (s.m_stats.m_restart - m_restart) + 10;
m_restart = s.m_stats.m_restart;
}
void mus::set_core() {
@ -49,12 +47,12 @@ namespace sat {
}
lbool mus::operator()() {
m_max_num_restarts = s.m_config.m_core_minimize_partial ? s.num_restarts() + 10 : UINT_MAX;
flet<bool> _disable_min(s.m_config.m_core_minimize, false);
flet<bool> _is_active(m_is_active, true);
IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
IF_VERBOSE(3, verbose_stream() << "(sat.mus size: " << s.get_core().size() << " core: [" << s.get_core() << "])\n";);
reset();
lbool r = mus1();
m_restart = s.m_stats.m_restart;
return r;
}
@ -63,13 +61,13 @@ namespace sat {
TRACE("sat", tout << "old core: " << s.get_core() << "\n";);
literal_vector& core = get_core();
literal_vector& mus = m_mus;
if (core.size() > 64) {
if (!minimize_partial && core.size() > 64) {
return mus2();
}
unsigned delta_time = 0;
unsigned core_miss = 0;
while (!core.empty()) {
IF_VERBOSE(3, verbose_stream() << "(opt.mus reducing core: " << core.size() << " mus: " << mus.size() << ")\n";);
IF_VERBOSE(1, verbose_stream() << "(sat.mus num-to-process: " << core.size() << " mus: " << mus.size();
if (minimize_partial) verbose_stream() << " max-restarts: " << m_max_num_restarts;
verbose_stream() << ")\n";);
TRACE("sat",
tout << "core: " << core << "\n";
tout << "mus: " << mus << "\n";);
@ -78,34 +76,35 @@ namespace sat {
set_core();
return l_undef;
}
if (minimize_partial && 3*delta_time > core.size() && core.size() < mus.size()) {
break;
}
unsigned num_literals = core.size() + mus.size();
if (num_literals <= 2) {
// IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";);
break;
}
if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
set_core();
return l_true;
}
literal lit = core.back();
core.pop_back();
lbool is_sat;
{
flet<unsigned> _restart_bound(s.m_config.m_restart_max, m_max_num_restarts);
scoped_append _sa(mus, core);
mus.push_back(~lit);
is_sat = s.check(mus.size(), mus.c_ptr());
TRACE("sat", tout << "mus: " << mus << "\n";);
}
IF_VERBOSE(1, verbose_stream() << "(sat.mus " << is_sat << ")\n";);
switch (is_sat) {
case l_undef:
core.push_back(lit);
set_core();
return l_undef;
if (!s.canceled()) {
// treat restart max as sat, so literal is in the mus
mus.push_back(lit);
}
else {
core.push_back(lit);
set_core();
return l_undef;
}
break;
case l_true: {
SASSERT(value_at(lit, s.get_model()) == l_false);
mus.push_back(lit);
@ -115,11 +114,9 @@ namespace sat {
case l_false:
literal_vector const& new_core = s.get_core();
if (new_core.contains(~lit)) {
IF_VERBOSE(3, verbose_stream() << "miss core " << lit << "\n";);
++core_miss;
IF_VERBOSE(3, verbose_stream() << "(sat.mus unit reduction, literal is in both cores " << lit << ")\n";);
}
else {
core_miss = 0;
TRACE("sat", tout << "core: " << new_core << " mus: " << mus << "\n";);
core.reset();
for (unsigned i = 0; i < new_core.size(); ++i) {
@ -131,14 +128,6 @@ namespace sat {
}
break;
}
unsigned new_num_literals = core.size() + mus.size();
if (new_num_literals == num_literals) {
delta_time++;
}
else {
delta_time = 0;
}
}
set_core();
IF_VERBOSE(3, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";);
@ -159,13 +148,9 @@ namespace sat {
lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) {
lbool is_sat = l_true;
if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
return l_true;
}
if (has_support) {
scoped_append _sa(m_mus, support.to_vector());
is_sat = s.check(m_mus.size(), m_mus.c_ptr());
is_sat = s.check(m_mus.size(), m_mus.c_ptr());
switch (is_sat) {
case l_false: {
literal_set core(s.get_core());
@ -173,7 +158,7 @@ namespace sat {
assignment.reset();
return l_true;
}
case l_undef:
case l_undef:
return l_undef;
case l_true:
update_model();

3
src/sat/sat_mus.h
View file

@ -26,8 +26,7 @@ namespace sat {
literal_vector m_mus;
bool m_is_active;
model m_model; // model obtained during minimal unsat core
unsigned m_restart;
unsigned m_max_restarts;
unsigned m_max_num_restarts;
public:

45
src/sat/sat_par.cpp Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_par.cpp
Abstract:
Utilities for parallel SAT solving.
Author:
Nikolaj Bjorner (nbjorner) 2017-1-29.
Revision History:
--*/
#include "sat_par.h"
namespace sat {
par::par() {}
void par::exchange(literal_vector const& in, unsigned& limit, literal_vector& out) {
#pragma omp critical (par_solver)
{
if (limit < m_units.size()) {
// this might repeat some literals.
out.append(m_units.size() - limit, m_units.c_ptr() + limit);
}
for (unsigned i = 0; i < in.size(); ++i) {
literal lit = in[i];
if (!m_unit_set.contains(lit.index())) {
m_unit_set.insert(lit.index());
m_units.push_back(lit);
}
}
limit = m_units.size();
}
}
};

39
src/sat/sat_par.h Normal file
View file

@ -0,0 +1,39 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_par.h
Abstract:
Utilities for parallel SAT solving.
Author:
Nikolaj Bjorner (nbjorner) 2017-1-29.
Revision History:
--*/
#ifndef SAT_PAR_H_
#define SAT_PAR_H_
#include"sat_types.h"
#include"hashtable.h"
#include"map.h"
namespace sat {
class par {
typedef hashtable<unsigned, u_hash, u_eq> index_set;
literal_vector m_units;
index_set m_unit_set;
public:
par();
void exchange(literal_vector const& in, unsigned& limit, literal_vector& out);
};
};
#endif

1
src/sat/sat_params.pyg
View file

@ -22,4 +22,5 @@ def_module_params('sat',
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('core.minimize', BOOL, False, 'minimize computed core'),
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('parallel_threads', UINT, 1, 'number of parallel threads to use'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

25
src/sat/sat_simplifier.cpp
View file

@ -896,7 +896,7 @@ namespace sat {
unsigned idx = l.index();
if (m_queue.contains(idx))
m_queue.decreased(idx);
else
else
m_queue.insert(idx);
}
literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
@ -918,16 +918,19 @@ namespace sat {
}
void insert(literal l) {
bool_var v = l.var();
if (s.is_external(v) || s.was_eliminated(v))
return;
m_queue.insert(l);
}
bool process_var(bool_var v) {
return !s.is_external(v) && !s.was_eliminated(v);
}
void operator()(unsigned num_vars) {
for (bool_var v = 0; v < num_vars; v++) {
insert(literal(v, false));
insert(literal(v, true));
if (process_var(v)) {
insert(literal(v, false));
insert(literal(v, true));
}
}
while (!m_queue.empty()) {
s.checkpoint();
@ -941,9 +944,9 @@ namespace sat {
void process(literal l) {
TRACE("blocked_clause", tout << "processing: " << l << "\n";);
model_converter::entry * new_entry = 0;
if (s.is_external(l.var()) || s.was_eliminated(l.var()))
if (!process_var(l.var())) {
return;
}
{
m_to_remove.reset();
{
@ -963,8 +966,10 @@ namespace sat {
mc.insert(*new_entry, c);
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
if (c[i] != l)
m_queue.decreased(~c[i]);
literal lit = c[i];
if (lit != l && process_var(lit.var())) {
m_queue.decreased(~lit);
}
}
}
s.unmark_all(c);

150
src/sat/sat_solver.cpp
View file

@ -35,6 +35,7 @@ namespace sat {
m_rlimit(l),
m_config(p),
m_ext(ext),
m_par(0),
m_cleaner(*this),
m_simplifier(*this, p),
m_scc(*this, p),
@ -72,6 +73,8 @@ namespace sat {
void solver::copy(solver const & src) {
SASSERT(m_mc.empty() && src.m_mc.empty());
SASSERT(scope_lvl() == 0);
SASSERT(src.scope_lvl() == 0);
// create new vars
if (num_vars() < src.num_vars()) {
for (bool_var v = num_vars(); v < src.num_vars(); v++) {
@ -81,19 +84,25 @@ namespace sat {
VERIFY(v == mk_var(ext, dvar));
}
}
unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
for (unsigned i = 0; i < sz; ++i) {
assign(src.m_trail[i], justification());
}
{
// copy binary clauses
vector<watch_list>::const_iterator it = src.m_watches.begin();
vector<watch_list>::const_iterator end = src.m_watches.begin();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
watch_list const & wlist = *it;
unsigned sz = src.m_watches.size();
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
literal l = ~to_literal(l_idx);
watch_list::const_iterator it2 = wlist.begin();
watch_list::const_iterator end2 = wlist.end();
for (; it2 != end2; ++it2) {
if (!it2->is_binary_non_learned_clause())
watch_list const & wlist = src.m_watches[l_idx];
watch_list::const_iterator it = wlist.begin();
watch_list::const_iterator end = wlist.end();
for (; it != end; ++it) {
if (!it->is_binary_non_learned_clause())
continue;
literal l2 = it->get_literal();
if (l.index() > l2.index())
continue;
literal l2 = it2->get_literal();
mk_clause_core(l, l2);
}
}
@ -711,6 +720,9 @@ namespace sat {
pop_to_base_level();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(scope_lvl() == 0);
if (m_config.m_num_parallel > 0 && !m_par) {
return check_par(num_lits, lits);
}
#ifdef CLONE_BEFORE_SOLVING
if (m_mc.empty()) {
m_clone = alloc(solver, m_params, 0 /* do not clone extension */);
@ -759,6 +771,7 @@ namespace sat {
restart();
simplify_problem();
exchange_par();
if (check_inconsistent()) return l_false;
gc();
@ -774,6 +787,121 @@ namespace sat {
}
}
enum par_exception_kind {
DEFAULT_EX,
ERROR_EX
};
lbool solver::check_par(unsigned num_lits, literal const* lits) {
int num_threads = static_cast<int>(m_config.m_num_parallel);
scoped_limits scoped_rlimit(rlimit());
vector<reslimit> rlims(num_threads);
ptr_vector<sat::solver> solvers(num_threads);
sat::par par;
for (int i = 0; i < num_threads; ++i) {
m_params.set_uint("random_seed", i);
solvers[i] = alloc(sat::solver, m_params, rlims[i], 0);
solvers[i]->copy(*this);
solvers[i]->set_par(&par);
scoped_rlimit.push_child(&solvers[i]->rlimit());
}
int finished_id = -1;
std::string ex_msg;
par_exception_kind ex_kind;
unsigned error_code = 0;
lbool result = l_undef;
#pragma omp parallel for
for (int i = 0; i < num_threads; ++i) {
try {
lbool r = solvers[i]->check(num_lits, lits);
bool first = false;
#pragma omp critical (par_solver)
{
if (finished_id == UINT_MAX) {
finished_id = i;
first = true;
result = r;
}
}
if (first) {
if (r == l_true) {
set_model(solvers[i]->get_model());
}
else if (r == l_false) {
m_core.reset();
m_core.append(solvers[i]->get_core());
}
for (int j = 0; j < num_threads; ++j) {
if (i != j) {
rlims[j].cancel();
}
}
}
}
catch (z3_error & err) {
if (i == 0) {
error_code = err.error_code();
ex_kind = ERROR_EX;
}
}
catch (z3_exception & ex) {
if (i == 0) {
ex_msg = ex.msg();
ex_kind = DEFAULT_EX;
}
}
}
for (int i = 0; i < num_threads; ++i) {
dealloc(solvers[i]);
}
if (finished_id == -1) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
default: throw default_exception(ex_msg.c_str());
}
}
return result;
}
/*
\brief import lemmas/units from parallel sat solvers.
*/
void solver::exchange_par() {
if (m_par && scope_lvl() == 0) {
unsigned num_in = 0, num_out = 0;
SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
literal_vector in, out;
for (unsigned i = m_par_limit_out; i < m_trail.size(); ++i) {
literal lit = m_trail[i];
if (lit.var() < m_par_num_vars) {
++num_out;
out.push_back(lit);
}
}
m_par_limit_out = m_trail.size();
m_par->exchange(out, m_par_limit_in, in);
for (unsigned i = 0; !inconsistent() && i < in.size(); ++i) {
literal lit = in[i];
SASSERT(lit.var() < m_par_num_vars);
if (lvl(lit.var()) != 0 || value(lit) != l_true) {
++num_in;
assign(lit, justification());
}
}
if (num_in > 0 || num_out > 0) {
IF_VERBOSE(1, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";);
}
}
}
void solver::set_par(par* p) {
m_par = p;
m_par_num_vars = num_vars();
m_par_limit_in = 0;
m_par_limit_out = 0;
}
bool_var solver::next_var() {
bool_var next;
@ -2624,6 +2752,7 @@ namespace sat {
m_scc.collect_statistics(st);
m_asymm_branch.collect_statistics(st);
m_probing.collect_statistics(st);
if (m_ext) m_ext->collect_statistics(st);
}
void solver::reset_statistics() {
@ -2728,6 +2857,9 @@ namespace sat {
display_units(out);
display_binary(out);
out << m_clauses << m_learned;
if (m_ext) {
m_ext->display(out);
}
out << ")\n";
}

12
src/sat/sat_solver.h
View file

@ -33,6 +33,7 @@ Revision History:
#include"sat_iff3_finder.h"
#include"sat_probing.h"
#include"sat_mus.h"
#include"sat_par.h"
#include"params.h"
#include"statistics.h"
#include"stopwatch.h"
@ -74,6 +75,7 @@ namespace sat {
config m_config;
stats m_stats;
extension * m_ext;
par* m_par;
random_gen m_rand;
clause_allocator m_cls_allocator;
cleaner m_cleaner;
@ -128,6 +130,10 @@ namespace sat {
literal_set m_assumption_set; // set of enabled assumptions
literal_vector m_core; // unsat core
unsigned m_par_limit_in;
unsigned m_par_limit_out;
unsigned m_par_num_vars;
void del_clauses(clause * const * begin, clause * const * end);
friend class integrity_checker;
@ -139,6 +145,7 @@ namespace sat {
friend class probing;
friend class iff3_finder;
friend class mus;
friend class card_extension;
friend struct mk_stat;
public:
solver(params_ref const & p, reslimit& l, extension * ext);
@ -209,6 +216,7 @@ namespace sat {
bool inconsistent() const { return m_inconsistent; }
unsigned num_vars() const { return m_level.size(); }
unsigned num_clauses() const;
unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; }
@ -240,7 +248,9 @@ namespace sat {
m_num_checkpoints = 0;
if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
}
void set_par(par* p);
bool canceled() { return !m_rlimit.inc(); }
config const& get_config() { return m_config; }
typedef std::pair<literal, literal> bin_clause;
protected:
watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
@ -316,6 +326,8 @@ namespace sat {
bool check_model(model const & m) const;
void restart();
void sort_watch_lits();
void exchange_par();
lbool check_par(unsigned num_lits, literal const* lits);
// -----------------------
//

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -140,6 +140,7 @@ public:
if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
switch (r) {
case l_true:
if (sz > 0) {
@ -276,6 +277,8 @@ public:
return r;
}
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
sat::literal_vector ls;
u_map<expr*> lit2var;