mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
add missing caching of PB/cardinality constraints, increase limit for compiling cardinalities to circuits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4695ca16c8
commit
8fb7fb9f98
|
|
@ -610,7 +610,7 @@ struct pb2bv_rewriter::imp {
|
|||
m_keep_pb_constraints(false),
|
||||
m_pb_num_system(false),
|
||||
m_pb_totalizer(false),
|
||||
m_min_arity(3)
|
||||
m_min_arity(9)
|
||||
{}
|
||||
|
||||
bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
|
|
@ -797,7 +797,7 @@ struct pb2bv_rewriter::imp {
|
|||
m_trail.push_back(l);
|
||||
return l;
|
||||
}
|
||||
literal fresh(char const* n) {
|
||||
literal fresh(char const* n) {
|
||||
expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m);
|
||||
m_imp.m_fresh.push_back(to_app(fr)->get_decl());
|
||||
return trail(fr);
|
||||
|
|
|
|||
|
|
@ -47,6 +47,16 @@ namespace sat {
|
|||
return static_cast<pb const&>(*this);
|
||||
}
|
||||
|
||||
ba_solver::eq& ba_solver::constraint::to_eq() {
|
||||
SASSERT(is_eq());
|
||||
return static_cast<eq&>(*this);
|
||||
}
|
||||
|
||||
ba_solver::eq const& ba_solver::constraint::to_eq() const{
|
||||
SASSERT(is_eq());
|
||||
return static_cast<eq const&>(*this);
|
||||
}
|
||||
|
||||
ba_solver::xr& ba_solver::constraint::to_xr() {
|
||||
SASSERT(is_xr());
|
||||
return static_cast<xr&>(*this);
|
||||
|
|
@ -85,6 +95,15 @@ namespace sat {
|
|||
}
|
||||
break;
|
||||
}
|
||||
case ba_solver::eq_t: {
|
||||
ba_solver::eq const& e = cnstr.to_eq();
|
||||
for (ba_solver::eliteral wl : e) {
|
||||
if (wl.weight != 1) out << wl.weight << " * ";
|
||||
out << wl.lit << " ";
|
||||
}
|
||||
out << " = " << e.k();
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
@ -186,6 +205,33 @@ namespace sat {
|
|||
}
|
||||
|
||||
|
||||
// -----------------------------------
|
||||
// eq
|
||||
|
||||
ba_solver::eq::eq(unsigned id, literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
|
||||
constraint(eq_t, id, lit, wlits.size(), eq::get_obj_size(wlits.size())),
|
||||
m_lo(0),
|
||||
m_hi(0),
|
||||
m_max(0),
|
||||
m_k(k)
|
||||
{
|
||||
unsigned i = 0;
|
||||
for (wliteral const& w : wlits) {
|
||||
m_wlits[i++] = eliteral(w.first, w.second);
|
||||
m_max += w.first;
|
||||
}
|
||||
m_hi = m_max;
|
||||
m_trail_sz = 0;
|
||||
}
|
||||
|
||||
unsigned ba_solver::eq::index(literal l) const {
|
||||
for (unsigned i = 0; i < size(); ++i) {
|
||||
if (l.var() == m_wlits[i].lit.var()) return i;
|
||||
}
|
||||
UNREACHABLE();
|
||||
return UINT_MAX;
|
||||
}
|
||||
|
||||
// -----------------------------------
|
||||
// xr
|
||||
|
||||
|
|
@ -451,7 +497,6 @@ namespace sat {
|
|||
// display(verbose_stream(), c, true);
|
||||
_bad_id = 11111111;
|
||||
SASSERT(p.well_formed());
|
||||
if (p.is_pb()) simplify2(p.to_pb());
|
||||
m_simplify_change = true;
|
||||
}
|
||||
}
|
||||
|
|
@ -847,28 +892,6 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
void ba_solver::simplify2(pb& p) {
|
||||
return;
|
||||
|
||||
if (p.is_cardinality()) {
|
||||
literal_vector lits(p.literals());
|
||||
unsigned k = (p.k() + p[0].first - 1) / p[0].first;
|
||||
add_at_least(p.lit(), lits, k, p.learned());
|
||||
remove_constraint(p, "simplified to cardinality");
|
||||
}
|
||||
else if (p.lit() == null_literal) {
|
||||
for (wliteral wl : p) {
|
||||
if (p.k() > p.max_sum() - wl.first) {
|
||||
TRACE("ba",
|
||||
tout << "unit literal " << wl.second << "\n";
|
||||
display(tout, p, true););
|
||||
|
||||
s().assign(wl.second, justification());
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void ba_solver::display(std::ostream& out, pb const& p, bool values) const {
|
||||
if (p.lit() != null_literal) out << p.lit() << " == ";
|
||||
if (values) {
|
||||
|
|
@ -902,6 +925,250 @@ namespace sat {
|
|||
out << ">= " << p.k() << "\n";
|
||||
}
|
||||
|
||||
// --------------------
|
||||
// eq:
|
||||
|
||||
ba_solver::constraint* ba_solver::add_eq(literal lit, svector<wliteral> const& wlits, unsigned k, bool learned) {
|
||||
void * mem = m_allocator.allocate(eq::get_obj_size(wlits.size()));
|
||||
eq* e = new (mem) eq(next_id(), lit, wlits, k);
|
||||
e->set_learned(learned);
|
||||
add_constraint(e);
|
||||
for (eliteral const& wl : *e) {
|
||||
watch_literal(wl.lit, *e);
|
||||
watch_literal(~(wl.lit), *e);
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
||||
void ba_solver::display(std::ostream& out, eq const& e, bool values) const {
|
||||
display_lit(out, e.lit(), e.size(), values);
|
||||
if (values) {
|
||||
if (e.trail_sz() > 0) {
|
||||
out << "trail: ";
|
||||
for (unsigned i = 0; i < e.trail_sz(); ++i) {
|
||||
out << e[i].tweight << " * " << e[i].tlit << " ";
|
||||
}
|
||||
}
|
||||
out << "[" << e.lo() << ":" << e.hi() << "] ";
|
||||
}
|
||||
for (eliteral wl : e) {
|
||||
literal l = wl.lit;
|
||||
unsigned w = wl.weight;
|
||||
if (w > 1) out << w << " * ";
|
||||
out << l;
|
||||
if (values) {
|
||||
out << "@(" << value(l);
|
||||
if (value(l) != l_undef) {
|
||||
out << ":" << lvl(l);
|
||||
}
|
||||
out << ") ";
|
||||
}
|
||||
else {
|
||||
out << " ";
|
||||
}
|
||||
}
|
||||
out << "= " << e.k() << "\n";
|
||||
}
|
||||
|
||||
bool ba_solver::init_watch(eq& e) {
|
||||
return true;
|
||||
}
|
||||
|
||||
void ba_solver::clear_watch(eq& e) {
|
||||
for (eliteral const& wl : e) {
|
||||
unwatch_literal(wl.lit, e);
|
||||
unwatch_literal(~(wl.lit), e);
|
||||
}
|
||||
if (e.lit() != null_literal) {
|
||||
unwatch_literal(e.lit(), e);
|
||||
unwatch_literal(~e.lit(), e);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* \update the bounds for [lo,hi] based on what is unassigned on the trail.
|
||||
*/
|
||||
void ba_solver::pop_eq(eq& e) {
|
||||
unsigned idx = e.trail_sz() - 1;
|
||||
literal tlit = e[idx].tlit;
|
||||
if (tlit.sign()) {
|
||||
e.inc_hi(e[idx].tweight);
|
||||
}
|
||||
else {
|
||||
e.dec_lo(e[idx].tweight);
|
||||
}
|
||||
e.set_trail_sz(idx);
|
||||
}
|
||||
|
||||
lbool ba_solver::add_assign(eq& e, literal nl) {
|
||||
//IF_VERBOSE(0, verbose_stream() << nl << "@" << lvl(nl) << ": " << e << "\n");
|
||||
SASSERT(value(nl) == l_false);
|
||||
if (nl.var() == e.lit().var()) {
|
||||
// no-op
|
||||
}
|
||||
else {
|
||||
unsigned i = e.index(nl);
|
||||
eliteral wl = e[i];
|
||||
if (wl.lit == nl) {
|
||||
e.dec_hi(wl);
|
||||
}
|
||||
else {
|
||||
SASSERT(wl.lit == ~nl);
|
||||
e.inc_lo(wl);
|
||||
}
|
||||
m_eq_to_pop.push_back(&e);
|
||||
}
|
||||
if (e.lo() > e.k() || e.hi() < e.k()) {
|
||||
if (e.lit() == null_literal || value(e.lit()) == l_true) {
|
||||
set_conflict(e, nl);
|
||||
return l_false;
|
||||
}
|
||||
if (e.lit() != null_literal && value(e.lit()) == l_undef) {
|
||||
assign(e, ~e.lit());
|
||||
}
|
||||
}
|
||||
else if (e.lo() == e.hi()) {
|
||||
SASSERT(e.lo() == e.k());
|
||||
if (e.lit() != null_literal && value(e.lit()) == l_false) {
|
||||
set_conflict(e, nl);
|
||||
return l_false;
|
||||
}
|
||||
if (e.lit() != null_literal && value(e.lit()) == l_undef) {
|
||||
assign(e, e.lit());
|
||||
}
|
||||
}
|
||||
else if ((e.lit() == null_literal || value(e.lit()) == l_true)) {
|
||||
if (e.lo() == e.k()) {
|
||||
for (eliteral el : e) {
|
||||
if (value(el.lit) == l_undef) {
|
||||
//IF_VERBOSE(0, display(verbose_stream() << "proapgate " << ~el.lit << " ", e, true));
|
||||
assign(e, ~el.lit);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (e.hi() == e.k()) {
|
||||
for (eliteral el : e) {
|
||||
if (value(el.lit) == l_undef) {
|
||||
//IF_VERBOSE(0, display(verbose_stream() << "proapgate " << el.lit << " ", e, true));
|
||||
assign(e, el.lit);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return l_true;
|
||||
}
|
||||
|
||||
void ba_solver::simplify(eq& e) {
|
||||
// no-op for now
|
||||
}
|
||||
|
||||
void ba_solver::recompile(eq& e) {
|
||||
for (eliteral const& el : e) {
|
||||
m_weights[el.lit.index()] += el.weight;
|
||||
}
|
||||
unsigned k = e.k(), sz = e.size();
|
||||
unsigned j = 0;
|
||||
bool is_false = false;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
eliteral el = e[i];
|
||||
unsigned w1 = m_weights[el.lit.index()];
|
||||
unsigned w2 = m_weights[(~el.lit).index()];
|
||||
if (w1 == 0 || w1 < w2) continue;
|
||||
if (k < w2) {
|
||||
is_false = true;
|
||||
break;
|
||||
}
|
||||
k -= w2;
|
||||
w1 -= w2;
|
||||
if (w1 == 0) continue;
|
||||
e[j++] = eliteral(w1, el.lit);
|
||||
}
|
||||
sz = j;
|
||||
for (eliteral const& el : e) {
|
||||
m_weights[el.lit.index()] = 0;
|
||||
m_weights[(~el.lit).index()] = 0;
|
||||
}
|
||||
if (is_false) {
|
||||
if (e.lit() == null_literal) {
|
||||
s().mk_clause(0, 0, true);
|
||||
}
|
||||
else {
|
||||
literal lit = ~e.lit();
|
||||
s().mk_clause(1, &lit, true);
|
||||
}
|
||||
remove_constraint(e, "recompiled to false");
|
||||
return;
|
||||
}
|
||||
// update trail
|
||||
e.set_size(sz);
|
||||
e.set_k(k);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
e[i].tlit = null_literal;
|
||||
}
|
||||
e.set_trail_sz(0);
|
||||
e.reset_lo();
|
||||
e.reset_hi();
|
||||
for (eliteral const& el : e) {
|
||||
switch (value(el.lit)) {
|
||||
case l_true: e.inc_lo(el); break;
|
||||
case l_false: e.dec_hi(el); break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void ba_solver::split_root(eq& e) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
void ba_solver::get_antecedents(literal l, eq const& e, literal_vector& r) {
|
||||
for (eliteral wl : e) {
|
||||
if (wl.lit.var() == l.var()) continue;
|
||||
switch (value(wl.lit)) {
|
||||
case l_true: r.push_back(wl.lit); break;
|
||||
case l_false: r.push_back(~wl.lit); break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
if (e.lit() != null_literal && l.var() != e.lit().var()) {
|
||||
switch (value(e.lit())) {
|
||||
case l_true: r.push_back(e.lit()); break;
|
||||
case l_false: r.push_back(~e.lit()); break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
lbool ba_solver::eval(eq const& e) const {
|
||||
unsigned trues = 0, undefs = 0;
|
||||
for (eliteral wl : e) {
|
||||
switch (value(wl.lit)) {
|
||||
case l_true: trues += wl.weight; break;
|
||||
case l_undef: undefs += wl.weight; break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
if (trues + undefs < e.k()) return l_false;
|
||||
if (trues > e.k()) return l_false;
|
||||
if (trues == e.k() && undefs == 0) return l_true;
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
lbool ba_solver::eval(model const& m, eq const& e) const {
|
||||
unsigned trues = 0, undefs = 0;
|
||||
for (eliteral wl : e) {
|
||||
switch (value(m, wl.lit)) {
|
||||
case l_true: trues += wl.weight; break;
|
||||
case l_undef: undefs += wl.weight; break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
if (trues + undefs < e.k()) return l_false;
|
||||
if (trues > e.k()) return l_false;
|
||||
if (trues == e.k() && undefs == 0) return l_true;
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
|
||||
// --------------------
|
||||
// xr:
|
||||
|
|
@ -1245,6 +1512,17 @@ namespace sat {
|
|||
for (literal l : m_lemma) process_antecedent(~l, offset);
|
||||
break;
|
||||
}
|
||||
case eq_t: {
|
||||
eq& e = cnstr.to_eq();
|
||||
m_lemma.reset();
|
||||
inc_bound(offset);
|
||||
inc_coeff(consequent, offset);
|
||||
get_antecedents(consequent, e, m_lemma);
|
||||
TRACE("ba", display(tout, e, true); tout << m_lemma << "\n";);
|
||||
for (literal l : m_lemma) process_antecedent(~l, offset);
|
||||
break;
|
||||
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
|
|
@ -1487,7 +1765,7 @@ namespace sat {
|
|||
void ba_solver::process_card(card& c, unsigned offset) {
|
||||
literal lit = c.lit();
|
||||
SASSERT(c.k() <= c.size());
|
||||
SASSERT(lit == null_literal || value(lit) == l_true);
|
||||
SASSERT(lit == null_literal || value(lit) != l_undef);
|
||||
SASSERT(0 < offset);
|
||||
for (unsigned i = c.k(); i < c.size(); ++i) {
|
||||
process_antecedent(c[i], offset);
|
||||
|
|
@ -1500,9 +1778,12 @@ namespace sat {
|
|||
if (offset1 > UINT_MAX) {
|
||||
m_overflow = true;
|
||||
}
|
||||
else {
|
||||
if (value(lit) == l_true) {
|
||||
process_antecedent(~lit, static_cast<unsigned>(offset1));
|
||||
}
|
||||
else {
|
||||
process_antecedent(lit, static_cast<unsigned>(offset1));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1607,6 +1888,7 @@ namespace sat {
|
|||
case card_t: return init_watch(c.to_card());
|
||||
case pb_t: return init_watch(c.to_pb());
|
||||
case xr_t: return init_watch(c.to_xr());
|
||||
case eq_t: return init_watch(c.to_eq());
|
||||
}
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
|
|
@ -1616,7 +1898,8 @@ namespace sat {
|
|||
switch (c.tag()) {
|
||||
case card_t: return add_assign(c.to_card(), l);
|
||||
case pb_t: return add_assign(c.to_pb(), l);
|
||||
case xr_t: return add_assign(c.to_xr(), l);
|
||||
case xr_t: return add_assign(c.to_xr(), l);
|
||||
case eq_t: return add_assign(c.to_eq(), l);
|
||||
}
|
||||
UNREACHABLE();
|
||||
return l_undef;
|
||||
|
|
@ -1667,7 +1950,7 @@ namespace sat {
|
|||
init_watch(c);
|
||||
return true;
|
||||
}
|
||||
else if (c.lit() != null_literal && value(c.lit()) != l_true) {
|
||||
else if (c.lit() != null_literal && value(c.lit()) != l_true && c.tag() != eq_t) {
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
|
|
@ -1722,6 +2005,7 @@ namespace sat {
|
|||
case card_t: return get_reward(c.to_card(), occs);
|
||||
case pb_t: return get_reward(c.to_pb(), occs);
|
||||
case xr_t: return 0;
|
||||
case eq_t: return 1;
|
||||
default: UNREACHABLE(); return 0;
|
||||
}
|
||||
}
|
||||
|
|
@ -1982,8 +2266,9 @@ namespace sat {
|
|||
}
|
||||
SASSERT(found););
|
||||
|
||||
if (c.lit() != null_literal) r.push_back(c.lit());
|
||||
SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
|
||||
// IF_VERBOSE(0, if (_debug_conflict) verbose_stream() << "ante " << l << " " << c << "\n");
|
||||
SASSERT(c.lit() == null_literal || value(c.lit()) != l_false);
|
||||
if (c.lit() != null_literal) r.push_back(value(c.lit()) == l_true ? c.lit() : ~c.lit());
|
||||
for (unsigned i = c.k(); i < c.size(); ++i) {
|
||||
SASSERT(value(c[i]) == l_false);
|
||||
r.push_back(~c[i]);
|
||||
|
|
@ -2033,6 +2318,7 @@ namespace sat {
|
|||
case card_t: get_antecedents(l, c.to_card(), r); break;
|
||||
case pb_t: get_antecedents(l, c.to_pb(), r); break;
|
||||
case xr_t: get_antecedents(l, c.to_xr(), r); break;
|
||||
case eq_t: get_antecedents(l, c.to_eq(), r); break;
|
||||
default: UNREACHABLE(); break;
|
||||
}
|
||||
}
|
||||
|
|
@ -2056,6 +2342,9 @@ namespace sat {
|
|||
case xr_t:
|
||||
clear_watch(c.to_xr());
|
||||
break;
|
||||
case eq_t:
|
||||
clear_watch(c.to_eq());
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
@ -2078,6 +2367,7 @@ namespace sat {
|
|||
case card_t: return validate_unit_propagation(c.to_card(), l);
|
||||
case pb_t: return validate_unit_propagation(c.to_pb(), l);
|
||||
case xr_t: return true;
|
||||
case eq_t: return validate_unit_propagation(c.to_eq(), l);
|
||||
default: UNREACHABLE(); break;
|
||||
}
|
||||
return false;
|
||||
|
|
@ -2093,6 +2383,7 @@ namespace sat {
|
|||
case card_t: return eval(v1, eval(c.to_card()));
|
||||
case pb_t: return eval(v1, eval(c.to_pb()));
|
||||
case xr_t: return eval(v1, eval(c.to_xr()));
|
||||
case eq_t: return eval(v1, eval(c.to_eq()));
|
||||
default: UNREACHABLE(); break;
|
||||
}
|
||||
return l_undef;
|
||||
|
|
@ -2103,7 +2394,8 @@ namespace sat {
|
|||
switch (c.tag()) {
|
||||
case card_t: return eval(v1, eval(m, c.to_card()));
|
||||
case pb_t: return eval(v1, eval(m, c.to_pb()));
|
||||
case xr_t: return eval(v1, eval(m, c.to_xr()));
|
||||
case xr_t: return eval(v1, eval(m, c.to_xr()));
|
||||
case eq_t: return eval(v1, eval(m, c.to_eq()));
|
||||
default: UNREACHABLE(); break;
|
||||
}
|
||||
return l_undef;
|
||||
|
|
@ -2360,6 +2652,10 @@ namespace sat {
|
|||
|
||||
SASSERT(0 < bound && bound <= sz);
|
||||
if (bound == sz) {
|
||||
if (c.lit() != null_literal && value(c.lit()) == l_undef) {
|
||||
assign(c, ~c.lit());
|
||||
return inconsistent() ? l_false : l_true;
|
||||
}
|
||||
set_conflict(c, alit);
|
||||
return l_false;
|
||||
}
|
||||
|
|
@ -2391,6 +2687,10 @@ namespace sat {
|
|||
// conflict
|
||||
if (bound != index && value(c[bound]) == l_false) {
|
||||
TRACE("ba", tout << "conflict " << c[bound] << " " << alit << "\n";);
|
||||
if (c.lit() != null_literal && value(c.lit()) == l_undef) {
|
||||
assign(c, ~c.lit());
|
||||
return inconsistent() ? l_false : l_true;
|
||||
}
|
||||
set_conflict(c, alit);
|
||||
return l_false;
|
||||
}
|
||||
|
|
@ -2403,6 +2703,11 @@ namespace sat {
|
|||
if (index != bound) {
|
||||
c.swap(index, bound);
|
||||
}
|
||||
|
||||
if (c.lit() != null_literal && value(c.lit()) == l_undef) {
|
||||
return l_true;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < bound; ++i) {
|
||||
assign(c, c[i]);
|
||||
}
|
||||
|
|
@ -2425,6 +2730,7 @@ namespace sat {
|
|||
|
||||
void ba_solver::push() {
|
||||
m_constraint_to_reinit_lim.push_back(m_constraint_to_reinit.size());
|
||||
m_eq_to_pop_lim.push_back(m_eq_to_pop.size());
|
||||
}
|
||||
|
||||
void ba_solver::pop(unsigned n) {
|
||||
|
|
@ -2433,6 +2739,13 @@ namespace sat {
|
|||
m_constraint_to_reinit_last_sz = m_constraint_to_reinit_lim[new_lim];
|
||||
m_constraint_to_reinit_lim.shrink(new_lim);
|
||||
m_num_propagations_since_pop = 0;
|
||||
|
||||
new_lim = m_eq_to_pop_lim.size() - n;
|
||||
for (unsigned i = m_eq_to_pop_lim[new_lim]; i < m_eq_to_pop.size(); ++i) {
|
||||
pop_eq(*m_eq_to_pop[i]);
|
||||
}
|
||||
m_eq_to_pop.shrink(m_eq_to_pop_lim[new_lim]);
|
||||
m_eq_to_pop_lim.shrink(new_lim);
|
||||
}
|
||||
|
||||
void ba_solver::pop_reinit() {
|
||||
|
|
@ -2451,16 +2764,16 @@ namespace sat {
|
|||
SASSERT(s().at_base_lvl());
|
||||
switch (c.tag()) {
|
||||
case card_t:
|
||||
if (!clausify(c.to_card()))
|
||||
simplify(c.to_card());
|
||||
simplify(c.to_card());
|
||||
break;
|
||||
case pb_t:
|
||||
if (!clausify(c.to_pb()))
|
||||
simplify(c.to_pb());
|
||||
simplify(c.to_pb());
|
||||
break;
|
||||
case xr_t:
|
||||
if (!clausify(c.to_xr()))
|
||||
simplify(c.to_xr());
|
||||
simplify(c.to_xr());
|
||||
break;
|
||||
case eq_t:
|
||||
simplify(c.to_eq());
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
|
@ -2498,6 +2811,7 @@ namespace sat {
|
|||
<< " :gc " << m_stats.m_num_gc
|
||||
<< ")\n";);
|
||||
|
||||
// IF_VERBOSE(0, s().display(verbose_stream()));
|
||||
// mutex_reduction();
|
||||
// if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
|
||||
|
||||
|
|
@ -2616,6 +2930,9 @@ namespace sat {
|
|||
case pb_t:
|
||||
recompile(c.to_pb());
|
||||
break;
|
||||
case eq_t:
|
||||
recompile(c.to_eq());
|
||||
break;
|
||||
case xr_t:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
break;
|
||||
|
|
@ -2631,7 +2948,6 @@ namespace sat {
|
|||
if (c.id() == _bad_id) std::cout << "recompile: " << c << "\n";
|
||||
// IF_VERBOSE(0, verbose_stream() << c << "\n";);
|
||||
m_weights.resize(2*s().num_vars(), 0);
|
||||
// for (unsigned w : m_weights) VERIFY(w == 0);
|
||||
for (literal l : c) {
|
||||
++m_weights[l.index()];
|
||||
}
|
||||
|
|
@ -2828,6 +3144,7 @@ namespace sat {
|
|||
case card_t: split_root(c.to_card()); break;
|
||||
case pb_t: split_root(c.to_pb()); break;
|
||||
case xr_t: NOT_IMPLEMENTED_YET(); break;
|
||||
case eq_t: split_root(c.to_eq()); break;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -2948,6 +3265,15 @@ namespace sat {
|
|||
}
|
||||
break;
|
||||
}
|
||||
case eq_t: {
|
||||
eq& e = cp->to_eq();
|
||||
for (eliteral wl : e) {
|
||||
literal l = wl.lit;
|
||||
m_cnstr_use_list[l.index()].push_back(&e);
|
||||
m_cnstr_use_list[(~l).index()].push_back(&e);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2970,6 +3296,8 @@ namespace sat {
|
|||
}
|
||||
break;
|
||||
}
|
||||
case eq_t:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
|
@ -3044,6 +3372,8 @@ namespace sat {
|
|||
if (p.k() > 1) subsumption(p);
|
||||
break;
|
||||
}
|
||||
case eq_t:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
|
@ -3185,6 +3515,8 @@ namespace sat {
|
|||
case pb_t:
|
||||
s = subsumes(p1, c->to_pb());
|
||||
break;
|
||||
case eq_t:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
|
@ -3413,6 +3745,15 @@ namespace sat {
|
|||
result->add_xr(lits, x.learned());
|
||||
break;
|
||||
}
|
||||
case eq_t: {
|
||||
eq const& e = cp->to_eq();
|
||||
wlits.reset();
|
||||
for (eliteral w : e) {
|
||||
wlits.push_back(wliteral(w.weight, w.lit));
|
||||
}
|
||||
result->add_eq(e.lit(), wlits, e.k(), e.learned());
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
@ -3450,6 +3791,14 @@ namespace sat {
|
|||
}
|
||||
break;
|
||||
}
|
||||
case eq_t: {
|
||||
eq const& e = cp->to_eq();
|
||||
for (eliteral w : e) {
|
||||
ul.insert(w.lit, idx);
|
||||
ul.insert(~(w.lit), idx);
|
||||
}
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
@ -3491,6 +3840,8 @@ namespace sat {
|
|||
}
|
||||
return weight >= p.k();
|
||||
}
|
||||
case eq_t:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
|
@ -3555,20 +3906,24 @@ namespace sat {
|
|||
out << "\n";
|
||||
}
|
||||
|
||||
void ba_solver::display(std::ostream& out, card const& c, bool values) const {
|
||||
if (c.lit() != null_literal) {
|
||||
void ba_solver::display_lit(std::ostream& out, literal lit, unsigned sz, bool values) const {
|
||||
if (lit != null_literal) {
|
||||
if (values) {
|
||||
out << c.lit() << "[" << c.size() << "]";
|
||||
out << "@(" << value(c.lit());
|
||||
if (value(c.lit()) != l_undef) {
|
||||
out << ":" << lvl(c.lit());
|
||||
out << lit << "[" << sz << "]";
|
||||
out << "@(" << value(lit);
|
||||
if (value(lit) != l_undef) {
|
||||
out << ":" << lvl(lit);
|
||||
}
|
||||
out << "): ";
|
||||
}
|
||||
else {
|
||||
out << c.lit() << " == ";
|
||||
out << lit << " == ";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void ba_solver::display(std::ostream& out, card const& c, bool values) const {
|
||||
display_lit(out, c.lit(), c.size(), values);
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
literal l = c[i];
|
||||
out << l;
|
||||
|
|
@ -3608,6 +3963,7 @@ namespace sat {
|
|||
case card_t: display(out, c.to_card(), values); break;
|
||||
case pb_t: display(out, c.to_pb(), values); break;
|
||||
case xr_t: display(out, c.to_xr(), values); break;
|
||||
case eq_t: display(out, c.to_eq(), values); break;
|
||||
default: UNREACHABLE(); break;
|
||||
}
|
||||
}
|
||||
|
|
@ -3924,6 +4280,13 @@ namespace sat {
|
|||
if (lxr != null_literal) ineq.push(~lxr, offset);
|
||||
break;
|
||||
}
|
||||
case eq_t: {
|
||||
eq& e = cnstr.to_eq();
|
||||
ineq.reset(e.k());
|
||||
for (eliteral wl : e) ineq.push(wl.lit, wl.weight);
|
||||
if (e.lit() != null_literal) ineq.push(~e.lit(), e.k());
|
||||
break;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -51,12 +51,14 @@ namespace sat {
|
|||
enum tag_t {
|
||||
card_t,
|
||||
pb_t,
|
||||
xr_t
|
||||
xr_t,
|
||||
eq_t
|
||||
};
|
||||
|
||||
class card;
|
||||
class pb;
|
||||
class xr;
|
||||
class eq;
|
||||
|
||||
class constraint {
|
||||
protected:
|
||||
|
|
@ -98,12 +100,15 @@ namespace sat {
|
|||
card& to_card();
|
||||
pb& to_pb();
|
||||
xr& to_xr();
|
||||
eq& to_eq();
|
||||
card const& to_card() const;
|
||||
pb const& to_pb() const;
|
||||
xr const& to_xr() const;
|
||||
eq const& to_eq() 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; }
|
||||
bool is_eq() const { return m_tag == eq_t; }
|
||||
|
||||
virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
|
||||
virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
|
||||
|
|
@ -180,6 +185,60 @@ namespace sat {
|
|||
virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; }
|
||||
};
|
||||
|
||||
struct eliteral {
|
||||
unsigned weight;
|
||||
literal lit;
|
||||
unsigned tweight;
|
||||
literal tlit;
|
||||
eliteral(unsigned w, literal lit):
|
||||
weight(w), lit(lit), tweight(0), tlit(null_literal)
|
||||
{}
|
||||
eliteral(): weight(0), lit(null_literal), tweight(0), tlit(null_literal) {}
|
||||
};
|
||||
class eq : public constraint {
|
||||
unsigned m_lo, m_hi, m_max, m_k, m_trail_sz;
|
||||
eliteral m_wlits[0];
|
||||
public:
|
||||
static size_t get_obj_size(unsigned num_lits) { return sizeof(eq) + num_lits * sizeof(eliteral); }
|
||||
eq(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
|
||||
literal lit() const { return m_lit; }
|
||||
eliteral operator[](unsigned i) const { return m_wlits[i]; }
|
||||
eliteral& operator[](unsigned i) { return m_wlits[i]; }
|
||||
eliteral const* begin() const { return m_wlits; }
|
||||
eliteral const* end() const { return begin() + m_size; }
|
||||
unsigned index(literal l) const;
|
||||
unsigned k() const { return m_k; }
|
||||
void reset_lo() { m_lo = 0; }
|
||||
void reset_hi() { m_hi = m_max; }
|
||||
unsigned lo() const { return m_lo; }
|
||||
unsigned hi() const { return m_hi; }
|
||||
void inc_hi(unsigned d) { m_hi += d; }
|
||||
void dec_lo(unsigned d) { SASSERT(d <= m_lo); m_lo -= d; }
|
||||
// increment/decrement lo/hi save delta and variable in a trail.
|
||||
void inc_lo(eliteral const& e) {
|
||||
m_lo += e.weight;
|
||||
m_wlits[m_trail_sz].tlit = literal(e.lit.var(), false);
|
||||
m_wlits[m_trail_sz++].tweight = e.weight;
|
||||
}
|
||||
void dec_hi(eliteral const& e) {
|
||||
m_hi -= e.weight;
|
||||
m_wlits[m_trail_sz].tlit = literal(e.lit.var(), true);
|
||||
m_wlits[m_trail_sz++].tweight = e.weight;
|
||||
}
|
||||
unsigned trail_sz() const { return m_trail_sz; }
|
||||
void set_trail_sz(unsigned sz) { m_trail_sz = sz; }
|
||||
|
||||
virtual void negate() { SASSERT(lit() != null_literal); m_lit.neg(); }
|
||||
virtual void set_k(unsigned k) { m_k = k; }
|
||||
virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
|
||||
virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.lit); return lits; }
|
||||
virtual bool is_watching(literal l) const { return true; }
|
||||
virtual literal get_lit(unsigned i) const { return m_wlits[i].lit; }
|
||||
virtual void set_lit(unsigned i, literal l) { m_wlits[i].lit = l; }
|
||||
virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].weight; }
|
||||
|
||||
};
|
||||
|
||||
class xr : public constraint {
|
||||
literal m_lits[0];
|
||||
public:
|
||||
|
|
@ -222,6 +281,8 @@ namespace sat {
|
|||
unsigned_vector m_constraint_to_reinit_lim;
|
||||
unsigned m_constraint_to_reinit_last_sz;
|
||||
unsigned m_constraint_id;
|
||||
ptr_vector<eq> m_eq_to_pop;
|
||||
unsigned_vector m_eq_to_pop_lim;
|
||||
|
||||
// conflict resolution
|
||||
unsigned m_num_marks;
|
||||
|
|
@ -390,6 +451,19 @@ namespace sat {
|
|||
lbool eval(model const& m, pb const& p) const;
|
||||
double get_reward(pb const& p, literal_occs_fun& occs) const;
|
||||
|
||||
// eq functionality
|
||||
void pop_eq(eq& e);
|
||||
bool init_watch(eq& e);
|
||||
void clear_watch(eq& e);
|
||||
lbool add_assign(eq& e, literal alit);
|
||||
void get_antecedents(literal l, eq const& e, literal_vector& r);
|
||||
void simplify(eq& e);
|
||||
void recompile(eq& e);
|
||||
void split_root(eq& e);
|
||||
void calibrate(eq& e);
|
||||
lbool eval(eq const& e) const;
|
||||
lbool eval(model const& m, eq const& e) const;
|
||||
|
||||
// access solver
|
||||
inline lbool value(bool_var v) const { return value(literal(v, false)); }
|
||||
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
|
||||
|
|
@ -467,10 +541,13 @@ namespace sat {
|
|||
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, xr const& c, bool values) const;
|
||||
void display(std::ostream& out, eq const& e, bool values) const;
|
||||
void display_lit(std::ostream& out, literal l, unsigned sz, bool values) const;
|
||||
|
||||
constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
|
||||
constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
|
||||
constraint* add_xr(literal_vector const& lits, bool learned);
|
||||
constraint* add_eq(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
|
||||
|
||||
void copy_core(ba_solver* result, bool learned);
|
||||
void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
|
||||
|
|
@ -484,6 +561,7 @@ namespace sat {
|
|||
void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
|
||||
void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
|
||||
void add_xr(literal_vector const& lits);
|
||||
void add_eq(literal l, svector<wliteral> const& wlits, unsigned k) { add_eq(l, wlits, k, false); }
|
||||
|
||||
virtual bool propagate(literal l, ext_constraint_idx idx);
|
||||
virtual lbool resolve_conflict();
|
||||
|
|
|
|||
|
|
@ -1052,10 +1052,10 @@ namespace sat {
|
|||
// Find literals that are in the intersection of all resolvents with l.
|
||||
//
|
||||
bool resolution_intersection(literal l, bool adding) {
|
||||
if (!process_var(l.var())) return false;
|
||||
bool first = true;
|
||||
reset_intersection();
|
||||
m_tautology.reset();
|
||||
if (!process_var(l.var())) return false;
|
||||
bool first = true;
|
||||
for (watched & w : s.get_wlist(l)) {
|
||||
// when adding a blocked clause, then all non-learned clauses have to be considered for the
|
||||
// resolution intersection.
|
||||
|
|
|
|||
|
|
@ -60,7 +60,6 @@ class inc_sat_solver : public solver {
|
|||
sat::literal_vector m_asms;
|
||||
goal_ref_buffer m_subgoals;
|
||||
proof_converter_ref m_pc;
|
||||
model_converter_ref m_mc;
|
||||
mutable model_converter_ref m_mc0;
|
||||
mutable obj_hashtable<func_decl> m_inserted_const2bits;
|
||||
mutable ref<sat2goal::mc> m_sat_mc;
|
||||
|
|
@ -120,7 +119,6 @@ public:
|
|||
for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
|
||||
for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
|
||||
for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
|
||||
if (m_mc) result->m_mc = m_mc->translate(tr);
|
||||
if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
|
||||
if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
|
||||
// copy m_bb_rewriter?
|
||||
|
|
@ -189,6 +187,7 @@ public:
|
|||
|
||||
init_reason_unknown();
|
||||
try {
|
||||
// IF_VERBOSE(0, m_solver.display(verbose_stream()));
|
||||
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
|
||||
}
|
||||
catch (z3_exception& ex) {
|
||||
|
|
@ -526,7 +525,6 @@ private:
|
|||
|
||||
|
||||
lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
|
||||
m_mc.reset();
|
||||
m_pc.reset();
|
||||
m_subgoals.reset();
|
||||
init_preprocess();
|
||||
|
|
@ -553,7 +551,7 @@ private:
|
|||
g = m_subgoals[0];
|
||||
expr_ref_vector atoms(m);
|
||||
m_pc = g->pc();
|
||||
m_mc = g->mc();
|
||||
m_mc0 = concat(m_mc0.get(), g->mc());
|
||||
TRACE("sat", g->display_with_dependencies(tout););
|
||||
|
||||
// ensure that if goal is already internalized, then import mc from m_solver.
|
||||
|
|
|
|||
|
|
@ -491,6 +491,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
|
||||
void convert_pb_eq(app* t, bool root, bool sign) {
|
||||
IF_VERBOSE(0, verbose_stream() << "pbeq: " << mk_pp(t, m) << "\n";);
|
||||
rational k = pb.get_k(t);
|
||||
SASSERT(k.is_unsigned());
|
||||
svector<wliteral> wlits;
|
||||
|
|
@ -515,11 +516,13 @@ struct goal2sat::imp {
|
|||
mk_clause(~l, l1);
|
||||
mk_clause(~l, l2);
|
||||
mk_clause(~l1, ~l2, l);
|
||||
m_cache.insert(t, l);
|
||||
m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
|
||||
m_result_stack.push_back(sign ? ~l : l);
|
||||
if (sign) l.neg();
|
||||
m_result_stack.push_back(l);
|
||||
if (root) {
|
||||
m_result_stack.reset();
|
||||
mk_clause(~l);
|
||||
mk_clause(l);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -535,8 +538,10 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.mk_var(true);
|
||||
sat::literal lit(v, sign);
|
||||
sat::literal lit(v, false);
|
||||
m_ext->add_at_least(v, lits, k.get_unsigned());
|
||||
m_cache.insert(t, lit);
|
||||
if (sign) lit.neg();
|
||||
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
|
||||
m_result_stack.shrink(sz - t->get_num_args());
|
||||
m_result_stack.push_back(lit);
|
||||
|
|
@ -557,15 +562,39 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.mk_var(true);
|
||||
sat::literal lit(v, sign);
|
||||
sat::literal lit(v, false);
|
||||
m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned());
|
||||
m_cache.insert(t, lit);
|
||||
m_result_stack.shrink(sz - t->get_num_args());
|
||||
if (sign) lit.neg();
|
||||
m_result_stack.push_back(lit);
|
||||
}
|
||||
}
|
||||
|
||||
void convert_eq_k(app* t, rational const& k, bool root, bool sign) {
|
||||
SASSERT(k.is_unsigned());
|
||||
#if 0
|
||||
IF_VERBOSE(0, verbose_stream() << t->get_id() << ": " << mk_pp(t, m) << "\n";);
|
||||
svector<wliteral> wlits;
|
||||
convert_pb_args(t, wlits);
|
||||
if (root && !sign) {
|
||||
m_ext->add_eq(sat::null_literal, wlits, k.get_unsigned());
|
||||
m_result_stack.reset();
|
||||
}
|
||||
else {
|
||||
sat::bool_var v = m_solver.mk_var();
|
||||
sat::literal l(v, false);
|
||||
m_ext->add_eq(l, wlits, k.get_unsigned());
|
||||
m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
|
||||
m_cache.insert(t, l);
|
||||
if (sign) l.neg();
|
||||
m_result_stack.push_back(l);
|
||||
if (root) {
|
||||
mk_clause(l);
|
||||
m_result_stack.reset();
|
||||
}
|
||||
}
|
||||
#else
|
||||
sat::literal_vector lits;
|
||||
convert_pb_args(t->get_num_args(), lits);
|
||||
sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
|
||||
|
|
@ -587,13 +616,16 @@ struct goal2sat::imp {
|
|||
mk_clause(~l, l1);
|
||||
mk_clause(~l, l2);
|
||||
mk_clause(~l1, ~l2, l);
|
||||
m_cache.insert(t, l);
|
||||
m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
|
||||
m_result_stack.push_back(sign ? ~l : l);
|
||||
if (sign) l.neg();
|
||||
m_result_stack.push_back(l);
|
||||
if (root) {
|
||||
mk_clause(~l);
|
||||
mk_clause(l);
|
||||
m_result_stack.reset();
|
||||
}
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
void ensure_extension() {
|
||||
|
|
|
|||
|
|
@ -15,24 +15,6 @@ Author:
|
|||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
lia2card_tactic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Convert 0-1 integer variables cardinality constraints to built-in cardinality operator.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-11-5
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include "util/cooperate.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
|
|
|||
Loading…
Reference in a new issue