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

updated resolvents

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-03 11:17:50 -07:00
parent 43807a7edc
commit c39d7c8565
6 changed files with 349 additions and 183 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/opt/opt_context.cpp
View file

@ -351,7 +351,7 @@ namespace opt {
void context::get_model_core(model_ref& mdl) {
mdl = m_model;
fix_model(mdl);
mdl->set_model_completion(true);
if (mdl) mdl->set_model_completion(true);
TRACE("opt", tout << *mdl;);
}

443
src/sat/ba_solver.cpp
View file

@ -49,6 +49,11 @@ namespace sat {
return static_cast<pb const&>(*this);
}
ba_solver::pb_base const& ba_solver::constraint::to_pb_base() const{
SASSERT(is_pb() || is_card());
return static_cast<pb_base const&>(*this);
}
ba_solver::xr& ba_solver::constraint::to_xr() {
SASSERT(is_xr());
return static_cast<xr&>(*this);
@ -1015,6 +1020,7 @@ namespace sat {
bool_var v = l.var();
SASSERT(v != null_bool_var);
m_coeffs.reserve(v + 1, 0);
TRACE("ba_verbose", tout << l << " " << offset << "\n";);
int64_t coeff0 = m_coeffs[v];
if (coeff0 == 0) {
@ -1064,6 +1070,7 @@ namespace sat {
l = literal(v, c1 < 0);
c1 = std::abs(c1);
c = static_cast<unsigned>(c1);
// TRACE("ba", tout << l << " " << c << "\n";);
m_overflow |= c != c1;
}
@ -1096,6 +1103,17 @@ namespace sat {
m_active_vars.reset();
}
void ba_solver::init_visited() {
m_visited_ts++;
if (m_visited_ts == 0) {
m_visited_ts = 1;
m_visited.reset();
}
while (m_visited.size() < 2*s().num_vars()) {
m_visited.push_back(0);
}
}
static bool _debug_conflict = false;
static literal _debug_consequent = null_literal;
static unsigned_vector _debug_var2position;
@ -1120,7 +1138,7 @@ namespace sat {
IF_VERBOSE(0,
active2pb(m_A);
uint64_t c = 0;
for (uint64_t c1 : m_A.m_coeffs) c += c1;
for (wliteral l : m_A.m_wlits) c += l.first;
verbose_stream() << "sum of coefficients: " << c << "\n";
display(verbose_stream(), m_A, true);
verbose_stream() << "conflicting literal: " << s().m_not_l << "\n";);
@ -1154,6 +1172,9 @@ namespace sat {
justification js = s().m_conflict;
TRACE("ba", tout << consequent << " " << js << "\n";);
m_conflict_lvl = s().get_max_lvl(consequent, js);
if (m_conflict_lvl == 0) {
return l_undef;
}
if (consequent != null_literal) {
consequent.neg();
process_antecedent(consequent, 1);
@ -1316,27 +1337,14 @@ namespace sat {
DEBUG_CODE(for (bool_var i = 0; i < static_cast<bool_var>(s().num_vars()); ++i) SASSERT(!s().is_marked(i)););
SASSERT(validate_lemma());
if (!create_asserting_lemma()) {
goto bail_out;
}
active2card();
DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A)););
TRACE("ba", tout << m_lemma << "\n";);
if (get_config().m_drat) {
svector<drat::premise> ps; // TBD fill in
drat_add(m_lemma, ps);
}
s().m_lemma.reset();
s().m_lemma.append(m_lemma);
for (unsigned i = 1; i < m_lemma.size(); ++i) {
CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";);
s().mark(m_lemma[i].var());
}
return l_true;
bail_out:
@ -1345,8 +1353,7 @@ namespace sat {
}
uint64_t ba_solver::ineq::coeff(literal l) const {
bool_var v = l.var();
unsigned ba_solver::ineq::bv_coeff(bool_var v) const {
for (unsigned i = size(); i-- > 0; ) {
if (lit(i).var() == v) return coeff(i);
}
@ -1354,10 +1361,10 @@ namespace sat {
return 0;
}
void ba_solver::ineq::divide(uint64_t c) {
void ba_solver::ineq::divide(unsigned c) {
if (c == 1) return;
for (unsigned i = size(); i-- > 0; ) {
m_coeffs[i] = (m_coeffs[i] + c - 1) / c;
m_wlits[i].first = (coeff(i) + c - 1) / c;
}
m_k = (m_k + c - 1) / c;
}
@ -1366,48 +1373,57 @@ namespace sat {
* Remove literal at position i, subtract coefficient from bound.
*/
void ba_solver::ineq::weaken(unsigned i) {
uint64_t ci = coeff(i);
unsigned ci = coeff(i);
SASSERT(m_k >= ci);
m_k -= ci;
m_lits[i] = m_lits.back();
m_coeffs[i] = m_coeffs.back();
m_lits.pop_back();
m_coeffs.pop_back();
m_wlits[i] = m_wlits.back();
m_wlits.pop_back();
}
/**
* Round coefficient of inequality to 1.
*/
void ba_solver::round_to_one(ineq& ineq, literal lit) {
uint64_t c = ineq.coeff(lit);
void ba_solver::round_to_one(ineq& ineq, bool_var v) {
unsigned c = ineq.bv_coeff(v);
if (c == 1) return;
unsigned sz = ineq.size();
for (unsigned i = 0; i < sz; ++i) {
uint64_t ci = ineq.coeff(i);
if (ci % c != 0 && !is_false(ineq.lit(i))) {
ineq.weaken(i);
--i;
--sz;
unsigned ci = ineq.coeff(i);
unsigned q = ci % c;
if (q != 0 && !is_false(ineq.lit(i))) {
if (q == ci) {
ineq.weaken(i);
--i;
--sz;
}
else {
ineq.m_wlits[i].first -= q;
ineq.m_k -= q;
}
}
}
ineq.divide(c);
}
void ba_solver::round_to_one(literal lit) {
uint64_t c = get_coeff(lit);
if (c == 1) return;
void ba_solver::round_to_one(bool_var w) {
unsigned c = get_abs_coeff(w);
if (c == 1 || c == 0) return;
for (bool_var v : m_active_vars) {
literal l;
unsigned ci;
get_coeff(v, l, ci);
if (ci > 0 && ci % c != 0 && !is_false(l)) {
m_coeffs[v] = 0;
unsigned q = ci % c;
if (q != 0 && !is_false(l)) {
m_coeffs[v] = ci - q;
m_bound -= q;
SASSERT(m_bound > 0);
}
}
divide(c);
SASSERT(validate_lemma());
}
void ba_solver::divide(uint64_t c) {
void ba_solver::divide(unsigned c) {
SASSERT(c != 0);
if (c == 1) return;
reset_active_var_set();
@ -1426,20 +1442,17 @@ namespace sat {
m_active_vars[j++] = v;
}
m_active_vars.shrink(j);
if (m_bound % c != 0) {
++m_stats.m_num_cut;
m_bound = static_cast<unsigned>((m_bound + c - 1) / c);
}
m_bound = static_cast<unsigned>((m_bound + c - 1) / c);
}
void ba_solver::resolve_on(literal consequent) {
round_to_one(consequent);
round_to_one(consequent.var());
m_coeffs[consequent.var()] = 0;
}
void ba_solver::resolve_with(ineq const& ineq) {
TRACE("ba", display(tout, ineq, true););
inc_bound(1 + ineq.m_k);
inc_bound(ineq.m_k);
for (unsigned i = ineq.size(); i-- > 0; ) {
literal l = ineq.lit(i);
inc_coeff(l, static_cast<unsigned>(ineq.coeff(i)));
@ -1457,6 +1470,23 @@ namespace sat {
--idx;
}
}
/**
* \brief mark variables that are on the assignment stack but
* below the current processing level.
*/
void ba_solver::mark_variables(ineq const& ineq) {
for (wliteral wl : ineq.m_wlits) {
literal l = wl.second;
if (!is_false(l)) continue;
bool_var v = l.var();
unsigned level = lvl(v);
if (!s().is_marked(v) && !is_visited(v) && level == m_conflict_lvl) {
s().mark(v);
++m_num_marks;
}
}
}
lbool ba_solver::resolve_conflict_rs() {
if (0 == m_num_propagations_since_pop) {
@ -1464,49 +1494,56 @@ namespace sat {
}
m_overflow = false;
reset_coeffs();
init_visited();
m_num_marks = 0;
m_bound = 0;
literal consequent = s().m_not_l;
justification js = s().m_conflict;
TRACE("ba", tout << consequent << " " << js << "\n";);
m_conflict_lvl = s().get_max_lvl(consequent, js);
if (m_conflict_lvl == 0) {
return l_undef;
}
if (consequent != null_literal) {
consequent.neg();
process_antecedent(consequent, 1);
}
TRACE("ba", tout << consequent << " " << js << "\n";);
unsigned idx = s().m_trail.size() - 1;
do {
// TBD: termination condition
// if UIP is below m_conflict level
TRACE("ba", s().display_justification(tout << "process consequent: " << consequent << " : ", js) << "\n";
active2pb(m_A); display(tout, m_A, true);
if (consequent != null_literal) { active2pb(m_A); display(tout, m_A, true); }
);
switch (js.get_kind()) {
case justification::NONE:
SASSERT(consequent != null_literal);
resolve_on(consequent);
inc_bound(1);
round_to_one(consequent.var());
inc_coeff(consequent, 1);
break;
case justification::BINARY:
SASSERT(consequent != null_literal);
resolve_on(consequent);
inc_bound(1);
round_to_one(consequent.var());
inc_coeff(consequent, 1);
process_antecedent(js.get_literal());
break;
case justification::TERNARY:
SASSERT(consequent != null_literal);
resolve_on(consequent);
inc_bound(1);
round_to_one(consequent.var());
inc_coeff(consequent, 1);
process_antecedent(js.get_literal1());
process_antecedent(js.get_literal2());
break;
case justification::CLAUSE: {
inc_bound(1);
clause & c = s().get_clause(js);
unsigned i = 0;
if (consequent == null_literal) {
m_bound = 1;
}
else {
resolve_on(consequent);
if (consequent != null_literal) {
round_to_one(consequent.var());
inc_coeff(consequent, 1);
if (c[0] == consequent) {
i = 1;
}
@ -1525,25 +1562,51 @@ namespace sat {
++m_stats.m_num_resolves;
ext_justification_idx index = js.get_ext_justification_idx();
constraint& cnstr = index2constraint(index);
constraint2pb(cnstr, consequent, 1, m_A);
switch (cnstr.tag()) {
case card_t:
case pb_t: {
pb_base const& p = cnstr.to_pb_base();
unsigned k = p.k(), sz = p.size();
m_A.reset(0);
for (unsigned i = 0; i < sz; ++i) {
literal l = p.get_lit(i);
unsigned c = p.get_coeff(i);
if (l == consequent || !is_visited(l.var())) {
m_A.push(l, c);
}
else {
SASSERT(k > c);
k -= c;
}
}
SASSERT(k > 0);
if (p.lit() != null_literal) m_A.push(~p.lit(), k);
m_A.m_k = k;
break;
}
default:
constraint2pb(cnstr, consequent, 1, m_A);
break;
}
mark_variables(m_A);
if (consequent == null_literal) {
m_bound = static_cast<unsigned>(m_A.m_k);
for (unsigned i = m_A.size(); i-- > 0; ) {
inc_coeff(m_A.lit(i), static_cast<unsigned>(m_A.coeff(i)));
for (wliteral wl : m_A.m_wlits) {
process_antecedent(wl.second, wl.first);
}
}
else {
round_to_one(consequent);
round_to_one(m_A, consequent);
round_to_one(consequent.var());
if (cnstr.tag() == pb_t) round_to_one(m_A, consequent.var());
resolve_with(m_A);
}
break;
}
default:
UNREACHABLE();
break;
}
SASSERT(validate_lemma());
cut();
// find the next marked variable in the assignment stack
@ -1551,7 +1614,14 @@ namespace sat {
while (true) {
consequent = s().m_trail[idx];
v = consequent.var();
if (s().is_marked(v)) break;
mark_visited(v);
if (s().is_marked(v)) {
if (get_coeff(v) != 0) {
break;
}
s().reset_mark(v);
--m_num_marks;
}
if (idx == 0) {
goto bail_out;
}
@ -1567,20 +1637,24 @@ namespace sat {
while (m_num_marks > 0 && !m_overflow);
TRACE("ba", active2pb(m_A); display(tout, m_A, true););
active2constraint();
if (!m_overflow) {
#if 0
// why this?
if (!m_overflow && consequent != null_literal) {
round_to_one(consequent.var());
}
#endif
if (!m_overflow && create_asserting_lemma()) {
active2constraint();
return l_true;
}
bail_out:
IF_VERBOSE(1, verbose_stream() << "bail\n");
m_overflow = false;
return l_undef;
}
bool ba_solver::create_asserting_lemma() {
bool adjusted = false;
adjust_conflict_level:
int64_t bound64 = m_bound;
int64_t slack = -bound64;
for (bool_var v : m_active_vars) {
@ -1629,20 +1703,22 @@ namespace sat {
if (m_lemma[0] == null_literal) {
if (m_lemma.size() == 1) {
s().set_conflict(justification());
return false;
}
return false;
unsigned old_level = m_conflict_lvl;
m_conflict_lvl = 0;
for (unsigned i = 1; i < m_lemma.size(); ++i) {
m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i]));
}
IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";);
adjusted = true;
goto adjust_conflict_level;
}
if (!adjusted) {
active2card();
TRACE("ba", tout << m_lemma << "\n";);
if (get_config().m_drat) {
svector<drat::premise> ps; // TBD fill in
drat_add(m_lemma, ps);
}
s().m_lemma.reset();
s().m_lemma.append(m_lemma);
for (unsigned i = 1; i < m_lemma.size(); ++i) {
CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";);
s().mark(m_lemma[i].var());
}
return true;
}
@ -1732,7 +1808,7 @@ namespace sat {
bool_var v = l.var();
unsigned level = lvl(v);
if (level > 0 && !s().is_marked(v) && level == m_conflict_lvl) {
if (!s().is_marked(v) && level == m_conflict_lvl) {
s().mark(v);
++m_num_marks;
if (_debug_conflict && _debug_consequent != null_literal && _debug_var2position[_debug_consequent.var()] < _debug_var2position[l.var()]) {
@ -2724,7 +2800,8 @@ namespace sat {
set_non_external();
if (get_config().m_elim_vars) elim_pure();
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
unit_strengthen();
cleanup_clauses();
cleanup_constraints();
update_pure();
@ -3170,9 +3247,10 @@ namespace sat {
bool found_dup = false;
bool found_root = false;
init_visited();
for (unsigned i = 0; i < c.size(); ++i) {
literal l = c.get_lit(i);
if (is_marked(l)) {
if (is_visited(l)) {
found_dup = true;
break;
}
@ -3182,10 +3260,7 @@ namespace sat {
}
}
for (unsigned i = 0; i < c.size(); ++i) {
literal l = c.get_lit(i);
unmark_visited(l);
unmark_visited(~l);
found_root |= l.var() == root.var();
found_root |= c.get_lit(i).var() == root.var();
}
if (found_root) {
@ -3342,6 +3417,78 @@ namespace sat {
return pure_literals;
}
/**
* Strengthen inequalities using binary implication information.
*
* x -> ~y, x -> ~z, y + z + u >= 2
* ----------------------------------
* y + z + u + ~x >= 3
*
* for c : constraints
* for l : c:
* slack <- of c under root(~l)
* if slack < 0:
* add ~root(~l) to c, k <- k + 1
*/
void ba_solver::unit_strengthen() {
big big(s().m_rand);
big.init(s(), true);
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i)
unit_strengthen(big, *m_constraints[i]);
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i)
unit_strengthen(big, *m_learned[i]);
}
void ba_solver::unit_strengthen(big& big, constraint& c) {
if (c.was_removed()) return;
switch (c.tag()) {
case card_t:
unit_strengthen(big, c.to_card());
break;
case pb_t:
unit_strengthen(big, c.to_pb());
break;
default:
break;
}
}
void ba_solver::unit_strengthen(big& big, card& c) {
for (literal l : c) {
literal r = big.get_root(~l);
if (r == ~l) continue;
unsigned k = c.k();
for (literal u : c) {
if (big.reaches(r, ~u)) {
if (k == 0) {
// ~r + C >= c.k() + 1
IF_VERBOSE(0, verbose_stream() << "TBD add " << ~r << " to " << c << "\n";);
return;
}
--k;
}
}
}
}
void ba_solver::unit_strengthen(big& big, pb& p) {
for (wliteral wl : p) {
literal r = big.get_root(~wl.second);
if (r == ~wl.second) continue;
unsigned k = p.k();
for (wliteral u : p) {
if (big.reaches(r, ~u.second)) {
if (k < u.first) {
// ~r + p >= p.k() + 1
IF_VERBOSE(0, verbose_stream() << "TBD add " << ~r << " to " << p << "\n";);
return;
}
k -= u.first;
}
}
}
}
void ba_solver::subsumption(constraint& cnstr) {
if (cnstr.was_removed()) return;
switch (cnstr.tag()) {
@ -3430,10 +3577,10 @@ namespace sat {
unsigned common = 0;
comp.reset();
for (literal l : c2) {
if (is_marked(l)) {
if (is_visited(l)) {
++common;
}
else if (is_marked(~l)) {
else if (is_visited(~l)) {
comp.push_back(l);
}
else {
@ -3455,10 +3602,10 @@ namespace sat {
self = false;
for (literal l : c2) {
if (is_marked(l)) {
if (is_visited(l)) {
++common;
}
else if (is_marked(~l)) {
else if (is_visited(~l)) {
++complement;
}
else {
@ -3482,10 +3629,10 @@ namespace sat {
unsigned num_sub = 0;
for (unsigned i = 0; i < p2.size(); ++i) {
literal l = p2.get_lit(i);
if (is_marked(l) && m_weights[l.index()] <= p2.get_coeff(i)) {
if (is_visited(l) && m_weights[l.index()] <= p2.get_coeff(i)) {
++num_sub;
}
if (p1.size() + i > p2.size() + num_sub) return false;
if (p1.size() + i > p2.size() + num_sub) return false;
}
return num_sub == p1.size();
}
@ -3550,7 +3697,7 @@ namespace sat {
clear_watch(c2);
unsigned j = 0;
for (unsigned i = 0; i < c2.size(); ++i) {
if (!is_marked(~c2[i])) {
if (!is_visited(~c2[i])) {
c2[j++] = c2[i];
}
}
@ -3586,7 +3733,7 @@ namespace sat {
void ba_solver::binary_subsumption(card& c1, literal lit) {
if (c1.k() + 1 != c1.size()) return;
SASSERT(is_marked(lit));
SASSERT(is_visited(lit));
SASSERT(!c1.was_removed());
watch_list & wlist = get_wlist(~lit);
watch_list::iterator it = wlist.begin();
@ -3594,7 +3741,7 @@ namespace sat {
watch_list::iterator end = wlist.end();
for (; it != end; ++it) {
watched w = *it;
if (w.is_binary_clause() && is_marked(w.get_literal())) {
if (w.is_binary_clause() && is_visited(w.get_literal())) {
++m_stats.m_num_bin_subsumes;
IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
if (!w.is_learned()) {
@ -3616,6 +3763,7 @@ namespace sat {
return;
}
clause_vector removed_clauses;
init_visited();
for (literal l : c1) mark_visited(l);
for (unsigned i = 0; i < std::min(c1.size(), c1.k() + 1); ++i) {
literal lit = c1[i];
@ -3623,7 +3771,6 @@ namespace sat {
clause_subsumption(c1, lit, removed_clauses);
binary_subsumption(c1, lit);
}
for (literal l : c1) unmark_visited(l);
m_clause_removed |= !removed_clauses.empty();
for (clause *c : removed_clauses) {
c->set_removed(true);
@ -3635,6 +3782,7 @@ namespace sat {
if (p1.was_removed() || p1.lit() != null_literal) {
return;
}
init_visited();
for (wliteral l : p1) {
SASSERT(m_weights[l.second.index()] == 0);
m_weights.setx(l.second.index(), l.first, 0);
@ -3646,7 +3794,6 @@ namespace sat {
}
for (wliteral l : p1) {
m_weights[l.second.index()] = 0;
unmark_visited(l.second);
}
}
@ -3844,9 +3991,9 @@ namespace sat {
}
void ba_solver::display(std::ostream& out, ineq const& ineq, bool values) const {
for (unsigned i = 0; i < ineq.m_lits.size(); ++i) {
out << ineq.m_coeffs[i] << "*" << ineq.m_lits[i] << " ";
if (values) out << value(ineq.m_lits[i]) << " ";
for (unsigned i = 0; i < ineq.size(); ++i) {
out << ineq.coeff(i) << "*" << ineq.lit(i) << " ";
if (values) out << value(ineq.lit(i)) << " ";
}
out << ">= " << ineq.m_k << "\n";
}
@ -4031,14 +4178,11 @@ namespace sat {
reset_active_var_set();
for (bool_var v : m_active_vars) {
if (m_active_var_set.contains(v)) continue;
int64_t coeff = get_coeff(v);
unsigned coeff;
literal lit;
get_coeff(v, lit, coeff);
if (coeff == 0) continue;
m_active_var_set.insert(v);
literal lit(v, false);
if (coeff < 0 && value(lit) != l_true) {
val -= coeff;
}
else if (coeff > 0 && value(lit) != l_false) {
if (!is_false(lit)) {
val += coeff;
}
}
@ -4051,31 +4195,26 @@ namespace sat {
}
void ba_solver::active2pb(ineq& p) {
reset_active_var_set();
p.reset(m_bound);
active2wlits(p.m_wlits);
}
void ba_solver::active2wlits() {
m_wlits.reset();
active2wlits(m_wlits);
}
void ba_solver::active2wlits(svector<wliteral>& wlits) {
reset_active_var_set();
uint64_t sum = 0;
for (bool_var v : m_active_vars) {
if (m_active_var_set.contains(v)) continue;
if (m_active_var_set.contains(v)) continue;
unsigned coeff;
literal lit;
get_coeff(v, lit, coeff);
if (coeff == 0) continue;
m_active_var_set.insert(v);
p.m_lits.push_back(lit);
p.m_coeffs.push_back(coeff);
}
}
void ba_solver::active2wlits() {
reset_active_var_set();
m_wlits.reset();
uint64_t sum = 0;
for (bool_var v : m_active_vars) {
unsigned coeff;
literal lit;
get_coeff(v, lit, coeff);
if (m_active_var_set.contains(v) || coeff == 0) continue;
m_active_var_set.insert(v);
m_wlits.push_back(wliteral(static_cast<unsigned>(coeff), lit));
wlits.push_back(wliteral(coeff, lit));
sum += coeff;
}
m_overflow |= sum >= UINT_MAX/2;
@ -4086,7 +4225,9 @@ namespace sat {
if (m_overflow) {
return nullptr;
}
return add_pb_ge(null_literal, m_wlits, m_bound, true);
constraint* c = add_pb_ge(null_literal, m_wlits, m_bound, true);
TRACE("ba", if (c) display(tout, *c, true););
return c;
}
/*
@ -4269,14 +4410,14 @@ namespace sat {
return true;
u_map<uint64_t> coeffs;
uint64_t k = m_A.m_k + m_B.m_k;
for (unsigned i = 0; i < m_A.m_lits.size(); ++i) {
uint64_t 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_A.size(); ++i) {
uint64_t coeff = m_A.coeff(i);
SASSERT(!coeffs.contains(m_A.lit(i).index()));
coeffs.insert(m_A.lit(i).index(), coeff);
}
for (unsigned i = 0; i < m_B.m_lits.size(); ++i) {
uint64_t coeff1 = m_B.m_coeffs[i], coeff2;
literal lit = m_B.m_lits[i];
for (unsigned i = 0; i < m_B.size(); ++i) {
uint64_t coeff1 = m_B.coeff(i), coeff2;
literal lit = m_B.lit(i);
if (coeffs.find((~lit).index(), coeff2)) {
if (coeff1 == coeff2) {
coeffs.remove((~lit).index());
@ -4301,11 +4442,11 @@ namespace sat {
}
}
// 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];
for (unsigned i = 0; i < m_C.size(); ++i) {
literal lit = m_C.lit(i);
uint64_t coeff;
if (coeffs.find(lit.index(), coeff)) {
if (coeff > m_C.m_coeffs[i] && m_C.m_coeffs[i] < m_C.m_k) {
if (coeff > m_C.coeff(i) && m_C.coeff(i) < m_C.m_k) {
goto violated;
}
coeffs.remove(lit.index());
@ -4352,15 +4493,15 @@ namespace sat {
*/
literal ba_solver::translate_to_sat(solver& s, u_map<bool_var>& translation, ineq const& pb) {
SASSERT(pb.m_k > 0);
if (pb.m_lits.size() > 1) {
if (pb.size() > 1) {
ineq a, b;
a.reset(pb.m_k);
b.reset(pb.m_k);
for (unsigned i = 0; i < pb.m_lits.size()/2; ++i) {
a.push(pb.m_lits[i], pb.m_coeffs[i]);
for (unsigned i = 0; i < pb.size()/2; ++i) {
a.push(pb.lit(i), pb.coeff(i));
}
for (unsigned i = pb.m_lits.size()/2; i < pb.m_lits.size(); ++i) {
b.push(pb.m_lits[i], pb.m_coeffs[i]);
for (unsigned i = pb.size()/2; i < pb.size(); ++i) {
b.push(pb.lit(i), pb.coeff(i));
}
bool_var v = s.mk_var();
literal lit(v, false);
@ -4372,8 +4513,8 @@ namespace sat {
s.mk_clause(lits);
return lit;
}
if (pb.m_coeffs[0] >= pb.m_k) {
return translate_to_sat(s, translation, pb.m_lits[0]);
if (pb.coeff(0) >= pb.m_k) {
return translate_to_sat(s, translation, pb.lit(0));
}
else {
return null_literal;
@ -4425,9 +4566,9 @@ namespace sat {
ba_solver::ineq ba_solver::negate(ineq const& a) const {
ineq result;
uint64_t sum = 0;
for (unsigned i = 0; i < a.m_lits.size(); ++i) {
result.push(~a.m_lits[i], a.m_coeffs[i]);
sum += a.m_coeffs[i];
for (unsigned i = 0; i < a.size(); ++i) {
result.push(~a.lit(i), a.coeff(i));
sum += a.coeff(i);
}
SASSERT(sum >= a.m_k + 1);
result.m_k = sum + 1 - a.m_k;
@ -4446,15 +4587,15 @@ namespace sat {
TRACE("ba", tout << "literal " << l << " is not false\n";);
return false;
}
if (!p.m_lits.contains(l)) {
if (!p.contains(l)) {
TRACE("ba", tout << "lemma contains literal " << l << " not in inequality\n";);
return false;
}
}
uint64_t value = 0;
for (unsigned i = 0; i < p.m_lits.size(); ++i) {
uint64_t coeff = p.m_coeffs[i];
if (!lits.contains(p.m_lits[i])) {
for (unsigned i = 0; i < p.size(); ++i) {
uint64_t coeff = p.coeff(i);
if (!lits.contains(p.lit(i))) {
value += coeff;
}
}

46
src/sat/ba_solver.h
View file

@ -25,6 +25,7 @@ Revision History:
#include "sat/sat_solver.h"
#include "sat/sat_lookahead.h"
#include "sat/sat_unit_walk.h"
#include "sat/sat_big.h"
#include "util/scoped_ptr_vector.h"
#include "util/sorting_network.h"
@ -57,6 +58,7 @@ namespace sat {
class card;
class pb;
class xr;
class pb_base;
class constraint {
protected:
@ -104,6 +106,7 @@ namespace sat {
card const& to_card() const;
pb const& to_pb() const;
xr const& to_xr() const;
pb_base const& to_pb_base() const;
bool is_card() const { return m_tag == card_t; }
bool is_pb() const { return m_tag == pb_t; }
bool is_xr() const { return m_tag == xr_t; }
@ -118,7 +121,7 @@ namespace sat {
};
friend std::ostream& operator<<(std::ostream& out, constraint const& c);
// base class for pb and cardinality constraints
class pb_base : public constraint {
protected:
@ -204,18 +207,18 @@ namespace sat {
protected:
struct ineq {
literal_vector m_lits;
svector<uint64_t> m_coeffs;
svector<wliteral> m_wlits;
uint64_t m_k;
ineq(): m_k(0) {}
unsigned size() const { return m_lits.size(); }
literal lit(unsigned i) const { return m_lits[i]; }
uint64_t coeff(unsigned i) const { return m_coeffs[i]; }
void reset(uint64_t k) { m_lits.reset(); m_coeffs.reset(); m_k = k; }
void push(literal l, uint64_t c) { m_lits.push_back(l); m_coeffs.push_back(c); }
uint64_t coeff(literal lit) const;
void divide(uint64_t c);
unsigned size() const { return m_wlits.size(); }
literal lit(unsigned i) const { return m_wlits[i].second; }
unsigned coeff(unsigned i) const { return m_wlits[i].first; }
void reset(uint64_t k) { m_wlits.reset(); m_k = k; }
void push(literal l, unsigned c) { m_wlits.push_back(wliteral(c,l)); }
unsigned bv_coeff(bool_var v) const;
void divide(unsigned c);
void weaken(unsigned i);
bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; }
};
solver* m_solver;
@ -279,7 +282,8 @@ namespace sat {
// simplification routines
svector<bool> m_visited;
svector<unsigned> m_visited;
unsigned m_visited_ts;
vector<svector<constraint*>> m_cnstr_use_list;
use_list m_clause_use_list;
bool m_simplify_change;
@ -298,9 +302,11 @@ namespace sat {
void binary_subsumption(card& c1, literal lit);
void clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses);
void card_subsumption(card& c1, literal lit);
void mark_visited(literal l) { m_visited[l.index()] = true; }
void unmark_visited(literal l) { m_visited[l.index()] = false; }
bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
void init_visited();
void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
bool is_visited(bool_var v) const { return is_visited(literal(v, false)); }
bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; }
unsigned get_num_unblocked_bin(literal l);
literal get_min_occurrence_literal(card const& c);
void init_use_lists();
@ -308,6 +314,10 @@ namespace sat {
unsigned set_non_external();
unsigned elim_pure();
bool elim_pure(literal lit);
void unit_strengthen();
void unit_strengthen(big& big, constraint& cs);
void unit_strengthen(big& big, card& c);
void unit_strengthen(big& big, pb& p);
void subsumption(constraint& c1);
void subsumption(card& c1);
void gc_half(char const* _method);
@ -404,12 +414,13 @@ namespace sat {
// RoundingPb conflict resolution
lbool resolve_conflict_rs();
void round_to_one(ineq& ineq, literal lit);
void round_to_one(literal lit);
void divide(uint64_t c);
void round_to_one(ineq& ineq, bool_var v);
void round_to_one(bool_var v);
void divide(unsigned c);
void resolve_on(literal lit);
void resolve_with(ineq const& ineq);
void reset_marks(unsigned idx);
void mark_variables(ineq const& ineq);
void bail_resolve_conflict(unsigned idx);
@ -487,6 +498,7 @@ namespace sat {
constraint* active2constraint();
constraint* active2card();
void active2wlits();
void active2wlits(svector<wliteral>& wlits);
void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p);
void constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& p);
bool validate_resolvent();

34
src/sat/sat_big.cpp
View file

@ -22,7 +22,8 @@ Revision History:
namespace sat {
big::big(random_gen& rand):
m_rand(rand) {
m_rand(rand),
m_include_cardinality(false) {
}
void big::init(solver& s, bool learned) {
@ -42,22 +43,22 @@ namespace sat {
m_roots[v.index()] = false;
edges.push_back(v);
}
#if 0
if (w.is_ext_constraint() &&
if (m_include_cardinality &&
w.is_ext_constraint() &&
s.m_ext &&
learned &&
learned && // cannot (yet) observe if ext constraints are learned
!seen_idx.contains(w.get_ext_constraint_idx()) &&
s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), r)) {
seen_idx.insert(w.get_ext_constraint_idx(), true);
for (unsigned i = 0; i < r.size(); ++i) {
literal u = r[i];
for (unsigned j = i + 1; j < r.size(); ++j) {
// add ~r[i] -> r[j]
literal v = r[j];
literal u = ~r[j];
for (unsigned i = 0; i < std::min(4u, r.size()); ++i) {
shuffle<literal>(r.size(), r.c_ptr(), m_rand);
literal u = r[0];
for (unsigned j = 1; j < r.size(); ++j) {
literal v = ~r[j];
// add u -> v
m_roots[v.index()] = false;
m_dag[u.index()].push_back(v);
// add ~r[j] -> r[i]
// add ~v -> ~u
v.neg();
u.neg();
m_roots[u.index()] = false;
@ -65,7 +66,6 @@ namespace sat {
}
}
}
#endif
}
}
done_adding_edges();
@ -268,6 +268,16 @@ namespace sat {
return out << v;
}
literal big::get_root(literal l) {
literal r = l;
do {
l = r;
r = m_root[l.index()];
}
while (r != l);
return r;
}
void big::display(std::ostream& out) const {
unsigned idx = 0;
for (auto& next : m_dag) {

6
src/sat/sat_big.h
View file

@ -34,6 +34,7 @@ namespace sat {
svector<int> m_left, m_right;
literal_vector m_root, m_parent;
bool m_learned;
bool m_include_cardinality;
svector<std::pair<literal, literal>> m_del_bin;
@ -54,6 +55,9 @@ namespace sat {
// static svector<std::pair<literal, literal>> s_del_bin;
big(random_gen& rand);
void set_include_cardinality(bool f) { m_include_cardinality = f; }
/**
\brief initialize a BIG from a solver.
*/
@ -77,7 +81,7 @@ namespace sat {
int get_left(literal l) const { return m_left[l.index()]; }
int get_right(literal l) const { return m_right[l.index()]; }
literal get_parent(literal l) const { return m_parent[l.index()]; }
literal get_root(literal l) const { return m_root[l.index()]; }
literal get_root(literal l);
bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); }
void display(std::ostream& out) const;

1
src/sat/sat_scc.h
View file

@ -60,7 +60,6 @@ namespace sat {
void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); }
int get_left(literal l) const { return m_big.get_left(l); }
int get_right(literal l) const { return m_big.get_right(l); }
literal get_root(literal l) const { return m_big.get_root(l); }
bool connected(literal u, literal v) const { return m_big.connected(u, v); }
};
};