mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-22 12:52:53 -07:00
parent d1fec7c029
commit 71eb7e81b5
2 changed files with 18 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -423,6 +423,7 @@ struct pb2bv_rewriter::imp {
vector<rational> coeffs(m_coeffs); vector<rational> coeffs(m_coeffs);
result = m.mk_true(); result = m.mk_true();
expr_ref_vector carry(m), new_carry(m); expr_ref_vector carry(m), new_carry(m);
m_base.push_back(bound + rational::one());
for (rational b_i : m_base) { for (rational b_i : m_base) {
unsigned B = b_i.get_unsigned(); unsigned B = b_i.get_unsigned();
unsigned d_i = (bound % b_i).get_unsigned(); unsigned d_i = (bound % b_i).get_unsigned();
@ -454,10 +455,7 @@ struct pb2bv_rewriter::imp {
carry.reset(); carry.reset();
carry.append(new_carry); carry.append(new_carry);
} }
if (!carry.empty()) { TRACE("pb", tout << "bound: " << bound << " Carry: " << carry << " result: " << result << "\n";);
result = m.mk_or(result, carry[0].get());
}
TRACE("pb", tout << "Carry: " << carry << " result: " << result << "\n";);
return true; return true;
} }

30
src/util/sorting_network.h
View file

@ -337,7 +337,7 @@ Notes:
} }
literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors, bool use_ors) { literal mk_at_most_1(bool full, unsigned n, literal const* xs, literal_vector& ors, bool use_ors) {
TRACE("pb", tout << (full?"full":"partial") << " "; TRACE("pb_verbose", tout << (full?"full":"partial") << " ";
for (unsigned i = 0; i < n; ++i) tout << xs[i] << " "; for (unsigned i = 0; i < n; ++i) tout << xs[i] << " ";
tout << "\n";); tout << "\n";);
@ -513,7 +513,7 @@ Notes:
for (unsigned i = 0; i < N; ++i) { for (unsigned i = 0; i < N; ++i) {
in.push_back(ctx.mk_not(xs[i])); in.push_back(ctx.mk_not(xs[i]));
} }
TRACE("pb", TRACE("pb_verbose",
pp(tout << N << ": ", in); pp(tout << N << ": ", in);
tout << " ~ " << k << "\n";); tout << " ~ " << k << "\n";);
return true; return true;
@ -595,7 +595,7 @@ Notes:
} }
void card(unsigned k, unsigned n, literal const* xs, literal_vector& out) { void card(unsigned k, unsigned n, literal const* xs, literal_vector& out) {
TRACE("pb", tout << "card k: " << k << " n: " << n << "\n";); TRACE("pb_verbose", tout << "card k: " << k << " n: " << n << "\n";);
if (n <= k) { if (n <= k) {
psort_nw<psort_expr>::sorting(n, xs, out); psort_nw<psort_expr>::sorting(n, xs, out);
} }
@ -609,7 +609,7 @@ Notes:
card(k, n-l, xs + l, out2); card(k, n-l, xs + l, out2);
smerge(k, out1.size(), out1.c_ptr(), out2.size(), out2.c_ptr(), out); smerge(k, out1.size(), out1.c_ptr(), out2.size(), out2.c_ptr(), out);
} }
TRACE("pb", tout << "card k: " << k << " n: " << n << "\n"; TRACE("pb_verbose", tout << "card k: " << k << " n: " << n << "\n";
pp(tout << "in:", n, xs) << "\n"; pp(tout << "in:", n, xs) << "\n";
pp(tout << "out:", out) << "\n";); pp(tout << "out:", out) << "\n";);
@ -637,7 +637,7 @@ Notes:
void merge(unsigned a, literal const* as, void merge(unsigned a, literal const* as,
unsigned b, literal const* bs, unsigned b, literal const* bs,
literal_vector& out) { literal_vector& out) {
TRACE("pb", tout << "merge a: " << a << " b: " << b << "\n";); TRACE("pb_verbose", tout << "merge a: " << a << " b: " << b << "\n";);
if (a == 1 && b == 1) { if (a == 1 && b == 1) {
literal y1 = mk_max(as[0], bs[0]); literal y1 = mk_max(as[0], bs[0]);
literal y2 = mk_min(as[0], bs[0]); literal y2 = mk_min(as[0], bs[0]);
@ -672,7 +672,7 @@ Notes:
odd_b.size(), odd_b.c_ptr(), out2); odd_b.size(), odd_b.c_ptr(), out2);
interleave(out1, out2, out); interleave(out1, out2, out);
} }
TRACE("pb", tout << "merge a: " << a << " b: " << b << "\n"; TRACE("pb_verbose", tout << "merge a: " << a << " b: " << b << "\n";
pp(tout << "a:", a, as) << "\n"; pp(tout << "a:", a, as) << "\n";
pp(tout << "b:", b, bs) << "\n"; pp(tout << "b:", b, bs) << "\n";
pp(tout << "out:", out) << "\n";); pp(tout << "out:", out) << "\n";);
@ -709,7 +709,7 @@ Notes:
void interleave(literal_vector const& as, void interleave(literal_vector const& as,
literal_vector const& bs, literal_vector const& bs,
literal_vector& out) { literal_vector& out) {
TRACE("pb", tout << "interleave: " << as.size() << " " << bs.size() << "\n";); TRACE("pb_verbose", tout << "interleave: " << as.size() << " " << bs.size() << "\n";);
SASSERT(as.size() >= bs.size()); SASSERT(as.size() >= bs.size());
SASSERT(as.size() <= bs.size() + 2); SASSERT(as.size() <= bs.size() + 2);
SASSERT(!as.empty()); SASSERT(!as.empty());
@ -729,7 +729,7 @@ Notes:
out.push_back(as[sz+1]); out.push_back(as[sz+1]);
} }
SASSERT(out.size() == as.size() + bs.size()); SASSERT(out.size() == as.size() + bs.size());
TRACE("pb", tout << "interleave: " << as.size() << " " << bs.size() << "\n"; TRACE("pb_verbose", tout << "interleave: " << as.size() << " " << bs.size() << "\n";
pp(tout << "a: ", as) << "\n"; pp(tout << "a: ", as) << "\n";
pp(tout << "b: ", bs) << "\n"; pp(tout << "b: ", bs) << "\n";
pp(tout << "out: ", out) << "\n";); pp(tout << "out: ", out) << "\n";);
@ -741,7 +741,7 @@ Notes:
public: public:
void sorting(unsigned n, literal const* xs, literal_vector& out) { void sorting(unsigned n, literal const* xs, literal_vector& out) {
TRACE("pb", tout << "sorting: " << n << "\n";); TRACE("pb_verbose", tout << "sorting: " << n << "\n";);
switch(n) { switch(n) {
case 0: case 0:
break; break;
@ -766,7 +766,7 @@ Notes:
} }
break; break;
} }
TRACE("pb", tout << "sorting: " << n << "\n"; TRACE("pb_verbose", tout << "sorting: " << n << "\n";
pp(tout << "in:", n, xs) << "\n"; pp(tout << "in:", n, xs) << "\n";
pp(tout << "out:", out) << "\n";); pp(tout << "out:", out) << "\n";);
} }
@ -802,7 +802,7 @@ Notes:
unsigned a, literal const* as, unsigned a, literal const* as,
unsigned b, literal const* bs, unsigned b, literal const* bs,
literal_vector& out) { literal_vector& out) {
TRACE("pb", tout << "smerge: c:" << c << " a:" << a << " b:" << b << "\n";); TRACE("pb_verbose", tout << "smerge: c:" << c << " a:" << a << " b:" << b << "\n";);
if (a == 1 && b == 1 && c == 1) { if (a == 1 && b == 1 && c == 1) {
literal y = mk_max(as[0], bs[0]); literal y = mk_max(as[0], bs[0]);
if (m_t != GE) { if (m_t != GE) {
@ -876,7 +876,7 @@ Notes:
out.push_back(y); out.push_back(y);
} }
} }
TRACE("pb", tout << "smerge: c:" << c << " a:" << a << " b:" << b << "\n"; TRACE("pb_verbose", tout << "smerge: c:" << c << " a:" << a << " b:" << b << "\n";
pp(tout << "a:", a, as) << "\n"; pp(tout << "a:", a, as) << "\n";
pp(tout << "b:", b, bs) << "\n"; pp(tout << "b:", b, bs) << "\n";
pp(tout << "out:", out) << "\n"; pp(tout << "out:", out) << "\n";
@ -920,7 +920,7 @@ Notes:
unsigned a, literal const* as, unsigned a, literal const* as,
unsigned b, literal const* bs, unsigned b, literal const* bs,
literal_vector& out) { literal_vector& out) {
TRACE("pb", tout << "dsmerge: c:" << c << " a:" << a << " b:" << b << "\n";); TRACE("pb_verbose", tout << "dsmerge: c:" << c << " a:" << a << " b:" << b << "\n";);
SASSERT(a <= c); SASSERT(a <= c);
SASSERT(b <= c); SASSERT(b <= c);
SASSERT(a + b >= c); SASSERT(a + b >= c);
@ -979,7 +979,7 @@ Notes:
void dsorting(unsigned m, unsigned n, literal const* xs, void dsorting(unsigned m, unsigned n, literal const* xs,
literal_vector& out) { literal_vector& out) {
TRACE("pb", tout << "dsorting m: " << m << " n: " << n << "\n";); TRACE("pb_verbose", tout << "dsorting m: " << m << " n: " << n << "\n";);
SASSERT(m <= n); SASSERT(m <= n);
literal_vector lits; literal_vector lits;
for (unsigned i = 0; i < m; ++i) { for (unsigned i = 0; i < m; ++i) {
@ -1014,7 +1014,7 @@ Notes:
void add_subset(bool polarity, unsigned k, unsigned offset, literal_vector& lits, void add_subset(bool polarity, unsigned k, unsigned offset, literal_vector& lits,
unsigned n, literal const* xs) { unsigned n, literal const* xs) {
TRACE("pb", tout << "k:" << k << " offset: " << offset << " n: " << n << " "; TRACE("pb_verbose", tout << "k:" << k << " offset: " << offset << " n: " << n << " ";
pp(tout, lits) << "\n";); pp(tout, lits) << "\n";);
SASSERT(k + offset <= n); SASSERT(k + offset <= n);
if (k == 0) { if (k == 0) {