mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +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-02-19 11:35:46 -08:00
commit cb050998e5
3 changed files with 263 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

188
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -96,10 +96,10 @@ struct pb2bv_rewriter::imp {
case l_undef: tout << "= "; break; case l_undef: tout << "= "; break;
case l_false: tout << ">= "; break; case l_false: tout << ">= "; break;
} }
tout << m_k << "\n";); tout << k << "\n";);
if (k.is_zero()) { if (k.is_zero()) {
if (is_le != l_false) { if (is_le != l_false) {
return expr_ref(m.mk_not(mk_or(m, sz, args)), m); return expr_ref(m.mk_not(::mk_or(m, sz, args)), m);
} }
else { else {
return expr_ref(m.mk_true(), m); return expr_ref(m.mk_true(), m);
@ -108,6 +108,15 @@ struct pb2bv_rewriter::imp {
if (k.is_neg()) { if (k.is_neg()) {
return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m); return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
} }
expr_ref result(m);
switch (is_le) {
case l_true: if (mk_le(sz, args, k, result)) return result; else break;
case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
}
// fall back to divide and conquer encoding.
SASSERT(k.is_pos()); SASSERT(k.is_pos());
expr_ref zero(m), bound(m); expr_ref zero(m), bound(m);
expr_ref_vector es(m), fmls(m); expr_ref_vector es(m), fmls(m);
@ -139,12 +148,12 @@ struct pb2bv_rewriter::imp {
} }
switch (is_le) { switch (is_le) {
case l_true: case l_true:
return mk_and(fmls); return ::mk_and(fmls);
case l_false: case l_false:
if (!es.empty()) { if (!es.empty()) {
fmls.push_back(bv.mk_ule(bound, es.back())); fmls.push_back(bv.mk_ule(bound, es.back()));
} }
return mk_or(fmls); return ::mk_or(fmls);
case l_undef: case l_undef:
if (es.empty()) { if (es.empty()) {
fmls.push_back(m.mk_bool_val(k.is_zero())); fmls.push_back(m.mk_bool_val(k.is_zero()));
@ -152,13 +161,180 @@ struct pb2bv_rewriter::imp {
else { else {
fmls.push_back(m.mk_eq(bound, es.back())); fmls.push_back(m.mk_eq(bound, es.back()));
} }
return mk_and(fmls); return ::mk_and(fmls);
default: default:
UNREACHABLE(); UNREACHABLE();
return expr_ref(m.mk_true(), m); return expr_ref(m.mk_true(), m);
} }
} }
/**
\brief MiniSat+ based encoding of PB constraints.
The procedure is described in "Translating Pseudo-Boolean Constraints into SAT "
         Niklas Een, Niklas Sörensson, JSAT 2006.
*/
const unsigned primes[7] = { 2, 3, 5, 7, 11, 13, 17};
vector<rational> m_min_base;
rational m_min_cost;
vector<rational> m_base;
void create_basis(vector<rational> const& seq, rational carry_in, rational cost) {
if (cost >= m_min_cost) {
return;
}
rational delta_cost(0);
for (unsigned i = 0; i < seq.size(); ++i) {
delta_cost += seq[i];
}
if (cost + delta_cost < m_min_cost) {
m_min_cost = cost + delta_cost;
m_min_base = m_base;
m_min_base.push_back(delta_cost + rational::one());
}
for (unsigned i = 0; i < sizeof(primes)/sizeof(*primes); ++i) {
vector<rational> seq1;
rational p(primes[i]);
rational rest = carry_in;
// create seq1
for (unsigned j = 0; j < seq.size(); ++j) {
rest += seq[j] % p;
if (seq[j] >= p) {
seq1.push_back(div(seq[j], p));
}
}
m_base.push_back(p);
create_basis(seq1, div(rest, p), cost + rest);
m_base.pop_back();
}
}
bool create_basis() {
m_base.reset();
m_min_cost = rational(INT_MAX);
m_min_base.reset();
rational cost(0);
create_basis(m_coeffs, rational::zero(), cost);
m_base = m_min_base;
TRACE("pb",
tout << "Base: ";
for (unsigned i = 0; i < m_base.size(); ++i) {
tout << m_base[i] << " ";
}
tout << "\n";);
return
!m_base.empty() &&
m_base.back().is_unsigned() &&
m_base.back().get_unsigned() <= 20*m_base.size();
}
/**
\brief Check if 'out mod n >= lim'.
*/
expr_ref mod_ge(ptr_vector<expr> const& out, unsigned n, unsigned lim) {
TRACE("pb", for (unsigned i = 0; i < out.size(); ++i) tout << mk_pp(out[i], m) << " "; tout << "\n";
tout << "n:" << n << " lim: " << lim << "\n";);
if (lim == n) {
return expr_ref(m.mk_false(), m);
}
if (lim == 0) {
return expr_ref(m.mk_true(), m);
}
SASSERT(0 < lim && lim < n);
expr_ref_vector ors(m);
for (unsigned j = 0; j + lim - 1 < out.size(); j += n) {
expr_ref tmp(m);
tmp = out[j + lim - 1];
if (j + n < out.size()) {
tmp = m.mk_and(tmp, m.mk_not(out[j + n]));
}
ors.push_back(tmp);
}
return ::mk_or(ors);
}
bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) {
if (!create_basis()) return false;
if (!bound.is_unsigned()) return false;
vector<rational> coeffs(m_coeffs);
result = m.mk_true();
expr_ref_vector carry(m), new_carry(m);
for (unsigned i = 0; i < m_base.size(); ++i) {
rational b_i = m_base[i];
unsigned B = b_i.get_unsigned();
unsigned d_i = (bound % b_i).get_unsigned();
bound = div(bound, b_i);
for (unsigned j = 0; j < coeffs.size(); ++j) {
rational c = coeffs[j] % b_i;
SASSERT(c.is_unsigned());
for (unsigned k = 0; k < c.get_unsigned(); ++k) {
carry.push_back(args[j]);
}
coeffs[j] = div(coeffs[j], b_i);
}
TRACE("pb", tout << "Carry: " << carry << "\n";
for (unsigned j = 0; j < coeffs.size(); ++j) tout << coeffs[j] << " ";
tout << "\n";
);
ptr_vector<expr> out;
m_sort.sorting(carry.size(), carry.c_ptr(), out);
expr_ref gt = mod_ge(out, B, d_i + 1);
expr_ref ge = mod_ge(out, B, d_i);
result = mk_or(gt, mk_and(ge, result));
TRACE("pb", tout << result << "\n";);
new_carry.reset();
for (unsigned j = B - 1; j < out.size(); j += B) {
new_carry.push_back(out[j]);
}
carry.reset();
carry.append(new_carry);
}
TRACE("pb", tout << result << "\n";);
return true;
}
expr_ref mk_and(expr_ref& a, expr_ref& b) {
if (m.is_true(a)) return b;
if (m.is_true(b)) return a;
if (m.is_false(a)) return a;
if (m.is_false(b)) return b;
return expr_ref(m.mk_and(a, b), m);
}
expr_ref mk_or(expr_ref& a, expr_ref& b) {
if (m.is_true(a)) return a;
if (m.is_true(b)) return b;
if (m.is_false(a)) return b;
if (m.is_false(b)) return a;
return expr_ref(m.mk_or(a, b), m);
}
bool mk_le(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
expr_ref_vector args1(m);
rational bound(-k);
for (unsigned i = 0; i < sz; ++i) {
args1.push_back(mk_not(args[i]));
bound += m_coeffs[i];
}
return mk_ge(sz, args1.c_ptr(), bound, result);
}
bool mk_eq(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
expr_ref r1(m), r2(m);
if (mk_ge(sz, args, k, r1) && mk_le(sz, args, k, r2)) {
result = m.mk_and(r1, r2);
return true;
}
else {
return false;
}
}
expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) { expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
decl_kind kind = f->get_decl_kind(); decl_kind kind = f->get_decl_kind();
rational k = pb.get_k(f); rational k = pb.get_k(f);
@ -403,7 +579,7 @@ struct pb2bv_rewriter::imp {
} }
void mk_clause(unsigned n, literal const* lits) { void mk_clause(unsigned n, literal const* lits) {
m_imp.m_lemmas.push_back(mk_or(m, n, lits)); m_imp.m_lemmas.push_back(::mk_or(m, n, lits));
} }
void keep_cardinality_constraints(bool f) { void keep_cardinality_constraints(bool f) {

149
src/sat/sat_lookahead.h
View file

@ -33,6 +33,7 @@ namespace sat {
literal_vector m_units; literal_vector m_units;
unsigned_vector m_units_lim; unsigned_vector m_units_lim;
unsigned_vector m_learned_lim; unsigned_vector m_learned_lim;
unsigned_vector m_binary;
void init() { void init() {
@ -44,6 +45,7 @@ namespace sat {
m_learned_lim.push_back(s.m_learned.size()); m_learned_lim.push_back(s.m_learned.size());
m_units_lim.push_back(m_units.size()); m_units_lim.push_back(m_units.size());
m_trail.push_back(lit); m_trail.push_back(lit);
m_binary.push_back(0);
s.push(); s.push();
assign(lit); assign(lit);
} }
@ -58,27 +60,31 @@ namespace sat {
s.m_cls_allocator.del_clause(r); s.m_cls_allocator.del_clause(r);
} }
s.m_learned.shrink(old_sz); s.m_learned.shrink(old_sz);
literal lits[2] = { m_trail.back(), null_literal };
unsigned new_unit_sz = m_units_lim.back(); unsigned new_unit_sz = m_units_lim.back();
for (unsigned i = m_units.size(); i > new_unit_sz; ) { for (unsigned i = new_unit_sz; i < m_units.size(); ++i) {
--i; literal lits[2] = { ~m_trail.back(), m_units[i] };
lits[1] = m_units[i];
clause * r = s.m_cls_allocator.mk_clause(2, lits, true); clause * r = s.m_cls_allocator.mk_clause(2, lits, true);
s.m_learned.push_back(r); s.m_learned.push_back(r);
} }
m_units.shrink(new_unit_sz); m_units.shrink(new_unit_sz);
m_units_lim.pop_back(); m_units_lim.pop_back();
m_trail.pop_back(); m_trail.pop_back();
m_binary.pop_back();
} }
unsigned diff(unsigned value0) const { unsigned diff() const { return m_binary.back() + m_units.size() - m_units_lim.back(); }
unsigned value1 = get_state_value();
SASSERT(value1 >= value0); unsigned mix_diff(unsigned l, unsigned r) const { return l + r + (1 << 10) * l * r; }
return value1 - value0;
clause const& get_clause(watch_list::iterator it) const {
clause_offset cls_off = it->get_clause_offset();
return *(s.m_cls_allocator.get_clause(cls_off));
} }
unsigned mix_diff(unsigned l, unsigned r) const { bool is_nary_propagation(clause const& c, literal l) const {
return l + r + (1 << 10) * l * r; bool r = c.size() > 2 && ((c[0] == l && s.value(c[1]) == l_false) || (c[1] == l && s.value(c[0]) == l_false));
DEBUG_CODE(if (r) for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
return r;
} }
void get_resolvent_units(literal lit) { void get_resolvent_units(literal lit) {
@ -94,25 +100,17 @@ namespace sat {
switch (it->get_kind()) { switch (it->get_kind()) {
case watched::TERNARY: case watched::TERNARY:
if (s.value(it->get_literal1()) == l_false && if (s.value(it->get_literal1()) == l_false &&
s.value(it->get_literal()) == l_false) { s.value(it->get_literal2()) == l_false) {
m_units.push_back(l); m_units.push_back(l);
goto done_watch_list; goto done_finding_unit;
} }
break; break;
case watched::CLAUSE: { case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset(); clause const & c = get_clause(it);
clause & c = *(s.m_cls_allocator.get_clause(cls_off)); SASSERT(c[0] == l || c[1] == l);
if (c.size() == 2) break; if (is_nary_propagation(c, l)) {
SASSERT(c.size() > 2);
if (c[0] == l && s.value(c[1]) == l_false) {
DEBUG_CODE(for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
m_units.push_back(l); m_units.push_back(l);
goto done_watch_list; goto done_finding_unit;
}
if (c[1] == l && s.value(c[0]) == l_false) {
DEBUG_CODE(for (unsigned j = 2; j < c.size(); ++j) SASSERT(s.value(c[j]) == l_false););
m_units.push_back(l);
goto done_watch_list;
} }
break; break;
} }
@ -120,8 +118,15 @@ namespace sat {
break; break;
} }
} }
done_watch_list: done_finding_unit:
//
// TBD: count binary clauses created by propagation.
// They used to be in the watch list of l.index(),
// both new literals in watch list should be unassigned.
//
continue; continue;
} }
} }
@ -131,10 +136,6 @@ namespace sat {
return l; return l;
} }
unsigned get_state_value() const {
return s.m_learned.size();
}
bool choose1(literal& l) { bool choose1(literal& l) {
literal_vector P; literal_vector P;
pre_select(P); pre_select(P);
@ -142,28 +143,26 @@ namespace sat {
if (P.empty()) { if (P.empty()) {
return true; return true;
} }
unsigned value0 = get_state_value();
unsigned h = 0, count = 1; unsigned h = 0, count = 1;
literal_vector& units = m_units;;
for (unsigned i = 0; i < P.size(); ++i) { for (unsigned i = 0; i < P.size(); ++i) {
literal lit = P[i]; literal lit = P[i];
push(lit); push(lit);
if (do_double(value0)) double_look(); if (do_double()) double_look(P);
if (inconsistent()) { if (inconsistent()) {
pop(); pop();
assign(~lit); assign(~lit);
if (do_double(value0)) double_look(); if (do_double()) double_look(P);
if (inconsistent()) return true; if (inconsistent()) return true;
continue; continue;
} }
unsigned diff1 = diff(value0); unsigned diff1 = diff();
pop(); pop();
push(~lit); push(~lit);
if (do_double(value0)) double_look(); if (do_double()) double_look(P);
bool unsat2 = inconsistent(); bool unsat2 = inconsistent();
unsigned diff2 = diff(value0); unsigned diff2 = diff();
pop(); pop();
if (unsat2) { if (unsat2) {
@ -173,25 +172,28 @@ namespace sat {
unsigned mixd = mix_diff(diff1, diff2); unsigned mixd = mix_diff(diff1, diff2);
if (mixd > h || (mixd == h && s.m_rand(count) == 0)) { if (mixd > h || (mixd == h && s.m_rand(count) == 0)) {
CTRACE("sat", l != null_literal, tout << lit << " diff1: " << diff1 << " diff2: " << diff2 << "\n";);
if (mixd > h) count = 1; else ++count;
h = mixd; h = mixd;
l = diff1 < diff2 ? lit : ~lit; l = diff1 < diff2 ? lit : ~lit;
++count;
} }
} }
return l != null_literal; return l != null_literal;
} }
void double_look() { void double_look(literal_vector const& P) {
literal_vector P; bool unsat;
pre_select(P);
for (unsigned i = 0; !inconsistent() && i < P.size(); ++i) { for (unsigned i = 0; !inconsistent() && i < P.size(); ++i) {
literal lit = P[i]; literal lit = P[i];
if (s.value(lit) != l_undef) continue;
push(lit); push(lit);
bool unsat = inconsistent(); unsat = inconsistent();
pop(); pop();
if (unsat) { if (unsat) {
TRACE("sat", tout << "unit: " << ~lit << "\n";);
assign(~lit); assign(~lit);
continue; continue;
} }
@ -200,6 +202,7 @@ namespace sat {
unsat = inconsistent(); unsat = inconsistent();
pop(); pop();
if (unsat) { if (unsat) {
TRACE("sat", tout << "unit: " << lit << "\n";);
assign(lit); assign(lit);
} }
@ -211,6 +214,7 @@ namespace sat {
s.assign(l, justification()); s.assign(l, justification());
s.propagate(false); s.propagate(false);
get_resolvent_units(l); get_resolvent_units(l);
TRACE("sat", s.display(tout << l << " @ " << s.scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
} }
bool inconsistent() { return s.inconsistent(); } bool inconsistent() { return s.inconsistent(); }
@ -220,6 +224,18 @@ namespace sat {
order_by_implication_trees(P); order_by_implication_trees(P);
} }
void check_binary(clause const& c, literal lit1, literal& lit2) {
if (c.size() == 2) {
if (c[0] == lit1) {
lit2 = c[1];
}
else {
SASSERT(c[1] == lit1);
lit2 = c[0];
}
}
}
void order_by_implication_trees(literal_vector& P) { void order_by_implication_trees(literal_vector& P) {
literal_set roots; literal_set roots;
literal_vector nodes, parent; literal_vector nodes, parent;
@ -246,28 +262,19 @@ namespace sat {
lit2 = it->get_literal(); lit2 = it->get_literal();
break; break;
case watched::CLAUSE: { case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset(); clause const & c = get_clause(it);
clause & c = *(s.m_cls_allocator.get_clause(cls_off)); check_binary(c, lit1, lit2);
if (c.size() == 2) {
if (c[0] == ~lit1) {
lit2 = c[1];
}
else {
SASSERT(c[1] == ~lit1);
lit2 = c[0];
}
}
break; break;
} }
default: default:
break; break;
} }
if (lit2 != null_literal && roots.contains(lit2)) { if (lit2 != null_literal && roots.contains(~lit2)) {
// lit2 => lit1 // ~lit2 => lit1
// if lit2 is a root, put it under lit2 // if lit2 is a root, put it under lit2
parent.setx(lit2.index(), lit1, null_literal); parent.setx((~lit2).index(), lit1, null_literal);
roots.remove(lit2); roots.remove(~lit2);
roots.insert(lit1); roots.insert(lit1);
goto found; goto found;
} }
@ -287,17 +294,8 @@ namespace sat {
lit2 = it->get_literal(); lit2 = it->get_literal();
break; break;
case watched::CLAUSE: { case watched::CLAUSE: {
clause_offset cls_off = it->get_clause_offset(); clause const & c = get_clause(it);
clause & c = *(s.m_cls_allocator.get_clause(cls_off)); check_binary(c, ~lit1, lit2);
if (c.size() == 2) {
if (c[0] == lit1) {
lit2 = c[1];
}
else {
SASSERT(c[1] == lit1);
lit2 = c[0];
}
}
break; break;
} }
default: default:
@ -311,19 +309,21 @@ namespace sat {
goto found; goto found;
} }
} }
std::cout << "no parents or children of literal " << lit1 << "\n";
nodes.push_back(lit1); nodes.push_back(lit1);
roots.insert(lit1); roots.insert(lit1);
found: found:
; ;
} }
std::cout << "implication trees\n"; TRACE("sat",
tout << "implication trees\n";
for (unsigned i = 0; i < parent.size(); ++i) { for (unsigned i = 0; i < parent.size(); ++i) {
literal p = parent[i]; literal p = parent[i];
if (p != null_literal) { if (p != null_literal) {
std::cout << to_literal(i) << " |-> " << p << "\n"; tout << to_literal(i) << " |-> " << p << "\n";
}
} }
});
// TBD: extract ordering.
} }
@ -335,9 +335,8 @@ namespace sat {
} }
} }
bool do_double(unsigned value0) { bool do_double() {
unsigned value1 = get_state_value(); return !inconsistent() && diff() > m_delta_trigger;
return !inconsistent() && value1 - value0 > m_delta_trigger;
} }
void update_delta_trigger() { void update_delta_trigger() {
@ -368,11 +367,11 @@ namespace sat {
s.checkpoint(); s.checkpoint();
BACKTRACK; BACKTRACK;
literal l = choose(); literal l = choose();
TRACE("sat", tout << l << "\n";);
BACKTRACK; BACKTRACK;
if (l == null_literal) { if (l == null_literal) {
return l_true; return l_true;
} }
TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
push(l); push(l);
trail.push_back(l); trail.push_back(l);
} }

2
src/util/sorting_network.h
View file

@ -558,7 +558,7 @@ Notes:
m_stats.m_num_compiled_clauses++; m_stats.m_num_compiled_clauses++;
m_stats.m_num_clause_vars += n; m_stats.m_num_clause_vars += n;
literal_vector tmp(n, ls); literal_vector tmp(n, ls);
TRACE("pb", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";); TRACE("pb_verbose", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";);
ctx.mk_clause(n, tmp.c_ptr()); ctx.mk_clause(n, tmp.c_ptr());
} }