mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +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-11-22 14:38:57 -08:00
parent 5f0a02b5f7 1101c927c9
commit 15d8532d27
3 changed files with 74 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,7 +77,33 @@ struct pb2bv_rewriter::imp {
fmls.push_back(bv.mk_ule(bound, result));
}
return result;
}
typedef std::pair<rational, expr_ref> ca;
struct compare_coeffs {
bool operator()(ca const& x, ca const& y) const {
return x.first < y.first;
}
};
void sort_args() {
vector<ca> cas;
for (unsigned i = 0; i < m_args.size(); ++i) {
cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m)));
}
//for (ca const& ca : cas) std::cout << ca.first << " ";
//std::cout << "\n";
std::sort(cas.begin(), cas.end(), compare_coeffs());
//std::cout << "post-sort\n";
//for (ca const& ca : cas) std::cout << ca.first << " ";
//std::cout << "\n";
m_coeffs.reset();
m_args.reset();
for (ca const& ca : cas) {
m_coeffs.push_back(ca.first);
m_args.push_back(ca.second);
}
}
//
@ -93,7 +119,10 @@ struct pb2bv_rewriter::imp {
// is_le = l_false - >=
//
template<lbool is_le>
expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) {
expr_ref mk_le_ge(rational const & k) {
//sort_args();
unsigned sz = m_args.size();
expr * const* args = m_args.c_ptr();
TRACE("pb",
for (unsigned i = 0; i < sz; ++i) {
tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
@ -107,7 +136,7 @@ struct pb2bv_rewriter::imp {
tout << k << "\n";);
if (k.is_zero()) {
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_args)), m);
}
else {
return expr_ref(m.mk_true(), m);
@ -501,25 +530,25 @@ struct pb2bv_rewriter::imp {
decl_kind kind = f->get_decl_kind();
rational k = pb.get_k(f);
m_coeffs.reset();
m_args.reset();
for (unsigned i = 0; i < sz; ++i) {
m_coeffs.push_back(pb.get_coeff(f, i));
m_args.push_back(args[i]);
}
CTRACE("pb", k.is_neg(), tout << expr_ref(m.mk_app(f, sz, args), m) << "\n";);
SASSERT(!k.is_neg());
switch (kind) {
case OP_PB_GE:
case OP_AT_LEAST_K: {
expr_ref_vector nargs(m);
nargs.append(sz, args);
dualize(f, nargs, k);
dualize(f, m_args, k);
SASSERT(!k.is_neg());
return mk_le_ge<l_true>(sz, nargs.c_ptr(), k);
return mk_le_ge<l_true>(k);
}
case OP_PB_LE:
case OP_AT_MOST_K:
return mk_le_ge<l_true>(sz, args, k);
return mk_le_ge<l_true>(k);
case OP_PB_EQ:
return mk_le_ge<l_undef>(sz, args, k);
return mk_le_ge<l_undef>(k);
default:
UNREACHABLE();
return expr_ref(m.mk_true(), m);
@ -591,21 +620,21 @@ struct pb2bv_rewriter::imp {
// skip
}
else if (au.is_le(f) && is_pb(args[0], args[1])) {
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (au.is_lt(f) && is_pb(args[0], args[1])) {
++m_k;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (au.is_ge(f) && is_pb(args[1], args[0])) {
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (au.is_gt(f) && is_pb(args[1], args[0])) {
++m_k;
result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_true>(m_k);
}
else if (m.is_eq(f) && is_pb(args[0], args[1])) {
result = mk_le_ge<l_undef>(m_args.size(), m_args.c_ptr(), m_k);
result = mk_le_ge<l_undef>(m_k);
}
else {
return false;

37
src/sat/sat_lookahead.cpp
View file

@ -233,7 +233,6 @@ namespace sat {
if (is_sat()) {
return false;
}
std::cout << "include newbies\n";
}
SASSERT(!m_candidates.empty());
// cut number of candidates down to max_num_cand.
@ -437,8 +436,8 @@ namespace sat {
for (binary b : m_ternary[(~l1).index()]) {
if (sz-- == 0) break;
if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) {
std::cout << b.m_u << " " << b.m_v << "\n";
std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n";
IF_VERBOSE(0, verbose_stream() << b.m_u << " " << b.m_v << "\n"
<< get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n";);
UNREACHABLE();
}
if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u)))
@ -649,6 +648,7 @@ namespace sat {
TRACE("sat", display_scc(tout););
}
void lookahead::init_scc() {
std::cerr << "init-scc\n";
inc_bstamp();
for (unsigned i = 0; i < m_candidates.size(); ++i) {
literal lit(m_candidates[i].m_var, false);
@ -661,6 +661,7 @@ namespace sat {
init_arcs(~lit);
}
m_rank = 0;
m_rank_max = UINT_MAX;
m_active = null_literal;
m_settled = null_literal;
TRACE("sat", display_dfs(tout););
@ -678,15 +679,19 @@ namespace sat {
for (literal u : succ) {
SASSERT(u != l);
// l => u
if (u.index() > (~l).index() && is_stamped(u)) {
// NB. u.index() > l.index() iff u.index() > (~l).index().
// since indices for the same boolean variables occupy
// two adjacent numbers.
if (u.index() > l.index() && is_stamped(u)) {
add_arc(~l, ~u);
add_arc( u, l);
}
}
for (auto w : m_watches[l.index()]) {
lits.reset();
if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) {
for (literal u : lits) {
if (u.index() > (~l).index() && is_stamped(u)) {
if (u.index() > l.index() && is_stamped(u)) {
add_arc(~l, ~u);
add_arc( u, l);
}
@ -695,6 +700,11 @@ namespace sat {
}
}
void lookahead::add_arc(literal u, literal v) {
auto & lst = m_dfs[u.index()].m_next;
if (lst.empty() || lst.back() != v) lst.push_back(v);
}
void lookahead::get_scc(literal v) {
TRACE("scc", tout << v << "\n";);
set_parent(v, null_literal);
@ -744,7 +754,7 @@ namespace sat {
m_active = get_link(v);
literal best = v;
double best_rating = get_rating(v);
set_rank(v, UINT_MAX);
set_rank(v, m_rank_max);
set_link(v, m_settled); m_settled = t;
while (t != v) {
if (t == ~v) {
@ -752,7 +762,7 @@ namespace sat {
set_conflict();
break;
}
set_rank(t, UINT_MAX);
set_rank(t, m_rank_max);
set_parent(t, v);
double t_rating = get_rating(t);
if (t_rating > best_rating) {
@ -763,7 +773,7 @@ namespace sat {
}
set_parent(v, v);
set_vcomp(v, best);
if (get_rank(~v) == UINT_MAX) {
if (maxed_rank(~v)) {
set_vcomp(v, ~get_vcomp(get_parent(~v)));
}
}
@ -2279,6 +2289,17 @@ namespace sat {
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";);
elim_eqs elim(m_s);
elim(roots, to_elim);
#if 0
// TBD:
// Finally create a new graph between parents
// based on the arcs in the the m_dfs[index].m_next structure
// Visit all nodes, assign DFS numbers
// Then prune binary clauses that differ in DFS number more than 1
// Add binary clauses that have DFS number 1, but no companion binary clause.
//
#endif
}
}
m_lookahead.reset();

4
src/sat/sat_lookahead.h
View file

@ -387,6 +387,7 @@ namespace sat {
literal m_active;
unsigned m_rank;
unsigned m_rank_max;
literal m_settled;
vector<dfs_info> m_dfs;
@ -394,7 +395,7 @@ namespace sat {
void init_scc();
void init_dfs_info(literal l);
void init_arcs(literal l);
void add_arc(literal u, literal v) { m_dfs[u.index()].m_next.push_back(v); }
void add_arc(literal u, literal v);
bool has_arc(literal v) const { return m_dfs[v.index()].m_next.size() > m_dfs[v.index()].m_nextp; }
arcs get_arcs(literal v) const { return m_dfs[v.index()].m_next; }
literal pop_arc(literal u) { return m_dfs[u.index()].m_next[m_dfs[u.index()].m_nextp++]; }
@ -402,6 +403,7 @@ namespace sat {
literal get_next(literal u, unsigned i) const { return m_dfs[u.index()].m_next[i]; }
literal get_min(literal v) const { return m_dfs[v.index()].m_min; }
unsigned get_rank(literal v) const { return m_dfs[v.index()].m_rank; }
bool maxed_rank(literal v) const { return get_rank(v) >= m_rank_max; }
unsigned get_height(literal v) const { return m_dfs[v.index()].m_height; }
literal get_parent(literal u) const { return m_dfs[u.index()].m_parent; }
literal get_link(literal u) const { return m_dfs[u.index()].m_link; }