Skip to content

Commit

Permalink
na
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Mar 5, 2024
1 parent 0e5b504 commit 58474df
Show file tree
Hide file tree
Showing 4 changed files with 169 additions and 54 deletions.
148 changes: 94 additions & 54 deletions src/ast/sls/bv_sls_eval.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -686,10 +686,7 @@ namespace bv {
}

digit_t sls_eval::random_bits() {
digit_t r = 0;
for (digit_t i = 0; i < sizeof(digit_t); ++i)
r ^= m_rand() << (8 * i);
return r;
return sls_valuation::random_bits(m_rand);
}

bool sls_eval::try_repair(app* e, unsigned i) {
Expand Down Expand Up @@ -826,7 +823,7 @@ namespace bv {
case OP_ZERO_EXT:
return try_repair_zero_ext(wval0(e), wval0(e, 0));
case OP_SIGN_EXT:
return try_repair_zero_ext(wval0(e), wval0(e, 0));
return try_repair_sign_ext(wval0(e), wval0(e, 0));
case OP_CONCAT:
return try_repair_concat(wval0(e), wval0(e, 0), wval0(e, 1), i);
case OP_EXTRACT: {
Expand Down Expand Up @@ -886,33 +883,33 @@ namespace bv {

bool sls_eval::try_repair_eq(app* e, unsigned i) {
auto child = e->get_arg(i);
auto ev = bval0(e);
auto is_true = bval0(e);
if (m.is_bool(child)) {
SASSERT(!is_fixed0(child));
auto bv = bval0(e->get_arg(1 - i));
m_eval[child->get_id()] = ev == bv;
m_eval[child->get_id()] = is_true == bv;
return true;
}
else if (bv.is_bv(child)) {
auto & a = wval0(e->get_arg(i));
auto & b = wval0(e->get_arg(1 - i));
if (ev)
if (is_true)
return a.try_set(b.bits());
else {
// pick random bit to differ
a.get(m_tmp);
unsigned start = m_rand(a.bw);
for (unsigned idx = 0; idx < a.bw; ++idx) {
unsigned j = (idx + start) % a.bw;
if (!a.fixed.get(j)) {
m_tmp.set(idx, !b.get_bit(j));
bool r = a.try_set(m_tmp);
if (r)
return true;
m_tmp.set(j, b.get_bit(j));
}
bool try_above = m_rand() % 2 == 0;
if (try_above) {
a.set_add(m_tmp, b.bits(), m_one);
if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
return true;
}
a.set_sub(m_tmp, b.bits(), m_one);
if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand))
return true;
if (!try_above) {
a.set_add(m_tmp, b.bits(), m_one);
if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
return true;
}
// could be due to bounds?
return false;
}
}
Expand Down Expand Up @@ -1144,6 +1141,18 @@ namespace bv {

// a <=s b <-> a + p2 <=u b + p2

//
// to solve x for x <=s b:
// y := at most (b + p2) - p2
// x := random_at_most y
// or
// x := random_at_least y - p2 if y < p2
//
// to solve x for x >s b:
// infeasible if b + p2 = 0
// y := at least (b + 1 + p2) - p2
// TODO
//
bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
a.set(m_tmp, b.bits());
if (e) {
Expand Down Expand Up @@ -1175,33 +1184,30 @@ namespace bv {

bool sls_eval::try_repair_ule(bool e, bvval& a, bvect const& t) {
if (e) {
if (!a.get_at_most(t, m_tmp))
return false;
// a <= t
return a.set_random_at_most(t, m_tmp, m_rand);
}
else {
// a > b
a.set_add(m_tmp2, t, m_one);
if (a.is_zero(m_tmp2))
return false;
if (!a.get_at_least(m_tmp2, m_tmp))
return false;
}
return a.set_repair(random_bool(), m_tmp);
// a > t
a.set_add(m_tmp, t, m_one);
if (a.is_zero(m_tmp))
return false;
return a.set_random_at_least(m_tmp, m_tmp2, m_rand);
}
}

bool sls_eval::try_repair_uge(bool e, bvval& a, bvect const& t) {
if (e) {
if (!a.get_at_least(t, m_tmp))
return false;
// a >= t
return a.set_random_at_least(t, m_tmp, m_rand);
}
else {
// a < t
if (a.is_zero(t))
return false;
a.set_sub(m_tmp2, t, m_one);
if (!a.get_at_most(m_tmp2, m_tmp))
return false;
}
return a.set_repair(random_bool(), m_tmp);
a.set_sub(m_tmp, t, m_one);
return a.set_random_at_most(m_tmp, m_tmp2, m_rand);
}
}

bool sls_eval::try_repair_bit2bool(bvval& a, unsigned idx) {
Expand Down Expand Up @@ -1300,13 +1306,12 @@ namespace bv {
return a.set_repair(false, m_tmp);
}
// b * e + r = a
for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = (random_bits() & ~b.fixed[i]) | (b.fixed[i] & b.bits()[i]);
b.clear_overflow_bits(m_tmp);
b.get_variant(m_tmp, m_rand);
while (mul_overflow_on_fixed(e, m_tmp)) {
auto i = b.msb(m_tmp);
m_tmp.set(i, false);
}

for (unsigned i = 0; i < a.nw; ++i)
m_tmp2[i] = random_bits();
b.clear_overflow_bits(m_tmp2);
Expand Down Expand Up @@ -1477,35 +1482,70 @@ namespace bv {
}
}

//
// prefix of e must be 1s or 0 and match bit position of last bit in a.
// set a to suffix of e, matching signs.
//
bool sls_eval::try_repair_sign_ext(bvval const& e, bvval& a) {
for (unsigned i = a.bw; i < e.bw; ++i)
if (e.get_bit(i) != e.get_bit(a.bw - 1))
return false;
e.get(m_tmp);
a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp);
}

//
// prefix of e must be 0s.
//
bool sls_eval::try_repair_zero_ext(bvval const& e, bvval& a) {
bool change = false;
for (unsigned i = 0; i < a.bw; ++i)
if (a.try_set_bit(i, e.get_bit(i)))
change = true;
return change;
for (unsigned i = a.bw; i < e.bw; ++i)
if (e.get_bit(i))
return false;
e.get(m_tmp);
a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp);
}

bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i) {
if (i == 0) {
bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned idx) {
if (idx == 0) {
for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, e.get_bit(i + b.bw));
a.clear_overflow_bits(m_tmp);
return a.set_repair(random_bool(), m_tmp);
return a.try_set(m_tmp);
}
else {
for (unsigned i = 0; i < b.bw; ++i)
m_tmp.set(i, e.get_bit(i));
b.clear_overflow_bits(m_tmp);
return b.set_repair(random_bool(), m_tmp);
return b.try_set(m_tmp);
}
}

//
// e = a[hi:lo], where hi = e.bw + lo - 1
// for the randomized assignment,
// set a outside of [hi:lo] to random values with preference to 0 or 1 bits
//
bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) {
bool change = false;
if (m_rand() % m_config.m_prob_randomize_extract <= 100) {
a.get_variant(m_tmp, m_rand);
if (0 == (m_rand() % 2)) {
auto bit = 0 == (m_rand() % 2);
if (!a.try_set_range(m_tmp, 0, lo, bit))
a.try_set_range(m_tmp, 0, lo, !bit);
}
if (0 == (m_rand() % 2)) {
auto bit = 0 == (m_rand() % 2);
if (!a.try_set_range(m_tmp, lo + e.bw, a.bw, bit))
a.try_set_range(m_tmp, lo + e.bw, a.bw, !bit);
}
}
else
a.get(m_tmp);
for (unsigned i = 0; i < e.bw; ++i)
if (a.try_set_bit(i + lo, e.get_bit(i)))
change = true;
return change;
m_tmp.set(i + lo, e.get_bit(i));
return a.try_set(m_tmp);
}

void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
Expand Down
8 changes: 8 additions & 0 deletions src/ast/sls/bv_sls_eval.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,10 @@ namespace bv {
class sls_fixed;

class sls_eval {
struct config {
unsigned m_prob_randomize_extract = 50;
};

friend class sls_fixed;
friend class sls_test;
ast_manager& m;
Expand All @@ -34,6 +38,9 @@ namespace bv {
mutable mpn_manager mpn;
ptr_vector<expr> m_todo;
random_gen m_rand;
config m_config;



scoped_ptr_vector<sls_valuation> m_values0; // expr-id -> bv valuation
scoped_ptr_vector<sls_pre_valuation> m_values1; // expr-id -> bv valuation
Expand Down Expand Up @@ -95,6 +102,7 @@ namespace bv {
bool try_repair_uge(bool e, bvval& a, bvect const& t);
bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i);
bool try_repair_zero_ext(bvval const& e, bvval& a);
bool try_repair_sign_ext(bvval const& e, bvval& a);
bool try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_extract(bvval const& e, bvval& a, unsigned lo);
void add_p2_1(bvval const& a, bvect& t) const;
Expand Down
51 changes: 51 additions & 0 deletions src/ast/sls/sls_valuation.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,44 @@ namespace bv {
return true;
}

bool sls_valuation::set_random_at_most(bvect const& src, bvect& tmp, random_gen& r) {
if (!get_at_most(src, tmp))
return false;
if (is_zero(tmp) || (0 == r() % 2))
return try_set(tmp);


// random value below tmp
auto msb_bit = msb(tmp);
for (unsigned i = 0; i < nw; ++i)
tmp[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & tmp[i]);
for (unsigned i = msb_bit; i < bw; ++i)
tmp.set(i, false);
if (m_lo == m_hi || is_zero(m_lo) || m_lo <= tmp)
return try_set(tmp);

// for simplicity, bail out if we were not lucky
return get_at_most(src, tmp) && try_set(tmp);
}

bool sls_valuation::set_random_at_least(bvect const& src, bvect& tmp, random_gen& r) {
if (!get_at_least(src, tmp))
return false;
if (is_ones(tmp) || (0 == r() % 2))
return try_set(tmp);

// random value at least tmp
auto msb_bit = msb(tmp);
for (unsigned i = 0; i < nw; ++i)
tmp[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & tmp[i]);
tmp.set(msb_bit, true);
if (m_lo == m_hi || is_zero(m_hi) || m_hi > tmp)
return try_set(tmp);

// for simplicity, bail out if we were not lucky
return get_at_least(src, tmp) && try_set(tmp);
}

bool sls_valuation::set_repair(bool try_down, bvect& dst) {
for (unsigned i = 0; i < nw; ++i)
dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
Expand Down Expand Up @@ -266,6 +304,19 @@ namespace bv {
dst[i] = m_bits[i];
}

digit_t sls_valuation::random_bits(random_gen& rand) {
digit_t r = 0;
for (digit_t i = 0; i < sizeof(digit_t); ++i)
r ^= rand() << (8 * i);
return r;
}

void sls_valuation::get_variant(bvect& dst, random_gen& r) const {
for (unsigned i = 0; i < nw; ++i)
dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]);
clear_overflow_bits(dst);
}

//
// new_bits != bits => ~fixed
// 0 = (new_bits ^ bits) & fixed
Expand Down
16 changes: 16 additions & 0 deletions src/ast/sls/sls_valuation.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,8 +186,15 @@ namespace bv {
bool get_at_most(bvect const& src, bvect& dst) const;
bool get_at_least(bvect const& src, bvect& dst) const;

bool set_random_at_most(bvect const& src, bvect& tmp, random_gen& r);
bool set_random_at_least(bvect const& src, bvect& tmp, random_gen& r);

bool set_repair(bool try_down, bvect& dst);


static digit_t random_bits(random_gen& r);
void get_variant(bvect& dst, random_gen& r) const;

bool try_set(bvect const& src) {
if (!can_set(src))
return false;
Expand Down Expand Up @@ -237,6 +244,15 @@ namespace bv {
dst.set(i, b);
}

bool try_set_range(bvect& dst, unsigned lo, unsigned hi, bool b) {
for (unsigned i = lo; i < hi; ++i)
if (fixed.get(i) && get_bit(i) != b)
return false;
for (unsigned i = lo; i < hi; ++i)
dst.set(i, b);
return true;
}

void set(bvect& dst, unsigned v) const {
dst[0] = v;
for (unsigned i = 1; i < nw; ++i)
Expand Down

0 comments on commit 58474df

Please sign in to comment.