Skip to content

Commit d6f522e

Browse files
NikolajBjornerNikolajBjorner
committed
na
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent 531bda3 commit d6f522e

File tree

5 files changed

+83
-27
lines changed

5 files changed

+83
-27
lines changed

‎src/ast/sls/bv_sls.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ namespace bv {
7070
void sls::reinit_eval() {
7171
std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
7272
auto should_keep = [&]() {
73-
return m_rand() % 100 >= 98;
73+
return m_rand() % 100 <= 92;
7474
};
7575
if (m.is_bool(e)) {
7676
if (m_eval.is_fixed0(e) || should_keep())
@@ -127,11 +127,12 @@ namespace bv {
127127
if (!e)
128128
return l_true;
129129

130-
++m_stats.m_moves;
131130

132131
trace_repair(down, e);
133132

134-
if (down)
133+
++m_stats.m_moves;
134+
135+
if (down)
135136
try_repair_down(e);
136137
else
137138
try_repair_up(e);

‎src/ast/sls/bv_sls_eval.cpp

+44-20
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ namespace bv {
3030
continue;
3131
app* a = to_app(e);
3232
if (bv.is_bv(e))
33-
add_bit_vector(e);
33+
add_bit_vector(a);
3434
if (a->get_family_id() == basic_family_id)
3535
init_eval_basic(a);
3636
else if (a->get_family_id() == bv.get_family_id())
@@ -40,7 +40,7 @@ namespace bv {
4040
auto& v = wval(e);
4141
for (unsigned i = 0; i < v.bw; ++i)
4242
m_tmp.set(i, eval(e, i));
43-
v.set(m_tmp);
43+
v.set_repair(random_bool(), m_tmp);
4444
}
4545
else if (m.is_bool(e))
4646
m_eval.setx(e->get_id(), eval(e, 0), false);
@@ -78,16 +78,21 @@ namespace bv {
7878
return m_todo;
7979
}
8080

81-
bool sls_eval::add_bit_vector(expr* e) {
82-
auto bw = bv.get_bv_size(e);
81+
bool sls_eval::add_bit_vector(app* e) {
8382
m_values.reserve(e->get_id() + 1);
8483
if (m_values.get(e->get_id()))
8584
return false;
86-
m_values.set(e->get_id(), alloc_valuation(bw));
85+
auto v = alloc_valuation(e);
86+
m_values.set(e->get_id(), v);
87+
if (bv.is_sign_ext(e)) {
88+
unsigned p = e->get_parameter(0).get_int();
89+
v->set_signed(p);
90+
}
8791
return true;
8892
}
8993

90-
sls_valuation* sls_eval::alloc_valuation(unsigned bit_width) {
94+
sls_valuation* sls_eval::alloc_valuation(app* e) {
95+
auto bit_width = bv.get_bv_size(e);
9196
auto* r = alloc(sls_valuation, bit_width);
9297
while (m_tmp.size() < 2 * r->nw) {
9398
m_tmp.push_back(0);
@@ -905,8 +910,14 @@ namespace bv {
905910
}
906911

907912
bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
908-
if (is_true)
909-
return a.try_set(b.bits());
913+
if (is_true) {
914+
if (m_rand() % 20 != 0)
915+
if (a.try_set(b.bits()))
916+
return true;
917+
918+
a.get_variant(m_tmp, m_rand);
919+
return a.set_repair(random_bool(), m_tmp);
920+
}
910921
else {
911922
bool try_above = m_rand() % 2 == 0;
912923
if (try_above) {
@@ -1004,22 +1015,26 @@ namespace bv {
10041015
// If this fails, set a to a random value
10051016
//
10061017
bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
1007-
a.set_sub(m_tmp, e, b.bits());
1008-
if (a.try_set(m_tmp))
1009-
return true;
1018+
if (m_rand() % 20 != 0) {
1019+
a.set_sub(m_tmp, e, b.bits());
1020+
if (a.try_set(m_tmp))
1021+
return true;
1022+
}
10101023
a.get_variant(m_tmp, m_rand);
10111024
return a.set_repair(random_bool(), m_tmp);
10121025
}
10131026

10141027
bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
1015-
if (i == 0)
1016-
// e = a - b -> a := e + b
1017-
a.set_add(m_tmp, e, b.bits());
1018-
else
1019-
// b := a - e
1020-
b.set_sub(m_tmp, a.bits(), e);
1021-
if (a.try_set(m_tmp))
1022-
return true;
1028+
if (m_rand() % 20 != 0) {
1029+
if (i == 0)
1030+
// e = a - b -> a := e + b
1031+
a.set_add(m_tmp, e, b.bits());
1032+
else
1033+
// b := a - e
1034+
b.set_sub(m_tmp, a.bits(), e);
1035+
if (a.try_set(m_tmp))
1036+
return true;
1037+
}
10231038
// fall back to a random value
10241039
a.get_variant(m_tmp, m_rand);
10251040
return a.set_repair(random_bool(), m_tmp);
@@ -1045,6 +1060,11 @@ namespace bv {
10451060
return a.set_repair(random_bool(), m_tmp);
10461061
}
10471062

1063+
if (m_rand() % 20 == 0) {
1064+
a.get_variant(m_tmp, m_rand);
1065+
return a.set_repair(random_bool(), m_tmp);
1066+
}
1067+
10481068
#if 0
10491069
verbose_stream() << "solve for " << e << "\n";
10501070

@@ -1125,7 +1145,11 @@ namespace bv {
11251145
if (parity_e > 0 && parity_b > 0)
11261146
b.shift_right(m_tmp2, std::min(parity_b, parity_e));
11271147
a.set_mul(m_tmp, tb, m_tmp2);
1128-
return a.set_repair(random_bool(), m_tmp);
1148+
if (a.set_repair(random_bool(), m_tmp))
1149+
return true;
1150+
1151+
a.get_variant(m_tmp, m_rand);
1152+
return a.set_repair(random_bool(), m_tmp);
11291153
}
11301154

11311155
bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {

‎src/ast/sls/bv_sls_eval.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,8 @@ namespace bv {
5959
* Register e as a bit-vector.
6060
* Return true if not already registered, false if already registered.
6161
*/
62-
bool add_bit_vector(expr* e);
63-
sls_valuation* alloc_valuation(unsigned bit_width);
62+
bool add_bit_vector(app* e);
63+
sls_valuation* alloc_valuation(app* e);
6464

6565
bool bval1_basic(app* e) const;
6666
bool bval1_bv(app* e) const;
@@ -143,7 +143,7 @@ namespace bv {
143143

144144
sls_valuation& wval(expr* e) const;
145145

146-
bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; }
146+
bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
147147

148148
/**
149149
* Retrieve evaluation based on immediate children.

‎src/ast/sls/sls_valuation.cpp

+28-1
Original file line numberDiff line numberDiff line change
@@ -307,18 +307,21 @@ namespace bv {
307307
void sls_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
308308
for (unsigned i = bw; !is_feasible(dst) && i-- > 0; )
309309
if (!fixed.get(i) && dst.get(i))
310-
dst.set(i, false);
310+
dst.set(i, false);
311+
repair_sign_bits(dst);
311312
}
312313

313314
void sls_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
314315
for (unsigned i = 0; !is_feasible(dst) && i < bw; ++i)
315316
if (!fixed.get(i) && !dst.get(i))
316317
dst.set(i, true);
318+
repair_sign_bits(dst);
317319
}
318320

319321
void sls_valuation::set_random_above(bvect& dst, random_gen& r) {
320322
for (unsigned i = 0; i < nw; ++i)
321323
dst[i] = dst[i] | (random_bits(r) & ~fixed[i]);
324+
repair_sign_bits(dst);
322325
}
323326

324327
void sls_valuation::set_random_below(bvect& dst, random_gen& r) {
@@ -335,12 +338,14 @@ namespace bv {
335338
for (unsigned i = 0; i < idx; ++i)
336339
if (!fixed.get(i))
337340
dst.set(i, r() % 2 == 0);
341+
repair_sign_bits(dst);
338342
}
339343

340344
bool sls_valuation::set_repair(bool try_down, bvect& dst) {
341345
for (unsigned i = 0; i < nw; ++i)
342346
dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
343347

348+
repair_sign_bits(dst);
344349
if (in_range(dst)) {
345350
set(eval, dst);
346351
return true;
@@ -363,6 +368,7 @@ namespace bv {
363368
if (!fixed.get(i) && dst.get(i))
364369
dst.set(i, false);
365370
}
371+
repair_sign_bits(dst);
366372
if (in_range(dst)) {
367373
set(eval, dst);
368374
repaired = true;
@@ -378,6 +384,7 @@ namespace bv {
378384
for (unsigned i = 0; i < nw; ++i)
379385
out[i] = fixed[i] & m_bits[i];
380386
}
387+
repair_sign_bits(out);
381388
SASSERT(!has_overflow(out));
382389
}
383390

@@ -390,6 +397,7 @@ namespace bv {
390397
for (unsigned i = 0; i < nw; ++i)
391398
out[i] = ~fixed[i] | m_bits[i];
392399
}
400+
repair_sign_bits(out);
393401
SASSERT(!has_overflow(out));
394402
}
395403

@@ -421,9 +429,28 @@ namespace bv {
421429
void sls_valuation::get_variant(bvect& dst, random_gen& r) const {
422430
for (unsigned i = 0; i < nw; ++i)
423431
dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]);
432+
repair_sign_bits(dst);
424433
clear_overflow_bits(dst);
425434
}
426435

436+
void sls_valuation::repair_sign_bits(bvect& dst) const {
437+
if (m_signed_prefix == 0)
438+
return;
439+
bool sign = dst.get(bw - 1);
440+
for (unsigned i = bw; i-- >= bw - m_signed_prefix; ) {
441+
if (dst.get(i) != sign) {
442+
if (fixed.get(i)) {
443+
for (unsigned i = bw; i-- >= bw - m_signed_prefix; )
444+
if (!fixed.get(i))
445+
dst.set(i, !sign);
446+
return;
447+
}
448+
else
449+
dst.set(i, sign);
450+
}
451+
}
452+
}
453+
427454
//
428455
// new_bits != bits => ~fixed
429456
// 0 = (new_bits ^ bits) & fixed

‎src/ast/sls/sls_valuation.h

+4
Original file line numberDiff line numberDiff line change
@@ -96,11 +96,14 @@ namespace bv {
9696
protected:
9797
bvect m_bits;
9898
bvect m_lo, m_hi; // range assignment to bit-vector, as wrap-around interval
99+
unsigned m_signed_prefix = 0;
99100

100101
unsigned mask;
101102
bool round_up(bvect& dst) const;
102103
bool round_down(bvect& dst) const;
103104

105+
void repair_sign_bits(bvect& dst) const;
106+
104107

105108
public:
106109
unsigned bw; // bit-width
@@ -111,6 +114,7 @@ namespace bv {
111114
sls_valuation(unsigned bw);
112115

113116
void set_bw(unsigned bw);
117+
void set_signed(unsigned prefix) { m_signed_prefix = prefix; }
114118

115119
unsigned num_bytes() const { return (bw + 7) / 8; }
116120

0 commit comments

Comments
 (0)