Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added rewriting distinct with bitvectors to false if bit-size is too low #5956

Merged
merged 10 commits into from
Apr 9, 2022
Merged

Added rewriting distinct with bitvectors to false if bit-size is too low #5956

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
01af7ac
Fixed problem with registering bitvector functions
CEisenhofer Mar 25, 2022
dc55a23
Merge branch 'Z3Prover:master' into master
CEisenhofer Mar 27, 2022
a99d121
Merge branch 'Z3Prover:master' into master
CEisenhofer Mar 29, 2022
49028b3
Merge branch 'Z3Prover:master' into master
CEisenhofer Apr 4, 2022
77c2bb4
Merge branch 'Z3Prover:master' into master
CEisenhofer Apr 6, 2022
1c1efe5
Added rewriting distinct with bitvectors to false if bit-size is too low
CEisenhofer Apr 8, 2022
ff9bc8c
Merge branch 'Z3Prover:master' into master
CEisenhofer Apr 8, 2022
df36213
Removed debug output
CEisenhofer Apr 8, 2022
bacfb75
Incorporated Nikolaj's comments
CEisenhofer Apr 8, 2022
281bf7d
Simplifications
CEisenhofer Apr 9, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions src/ast/rewriter/bv_rewriter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2803,6 +2803,27 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu
return BR_FAILED;
}

br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
if (num_args <= 1) {
result = m().mk_true();
return BR_DONE;
}
unsigned sz = get_bv_size(args[0]);
// check if num_args > 2^sz
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this may be clever code, but not easy to read.
Here is something simpler:

if (sz >= 32) 
    return BR_FAILED;
if (num_args <= 1u << sz)
    return BR_FAILED;
result = m().mk_false();
return BR_DONE;

bool exact = true;
while (num_args > 1 && sz > 0) {
exact &= (num_args % 2) == 0;
num_args /= 2;
sz--;
}

if (sz + exact < num_args) {
result = m().mk_false();
return BR_DONE;
}
return BR_FAILED;
}

br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) {
SASSERT(num == 2);
unsigned bv_sz;
Expand Down
3 changes: 2 additions & 1 deletion src/ast/rewriter/bv_rewriter.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,8 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {

bool is_urem_any(expr * e, expr * & dividend, expr * & divisor);
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul);
br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
br_status mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);

bool hi_div0() const { return m_hi_div0; }

Expand Down
22 changes: 13 additions & 9 deletions src/ast/rewriter/th_rewriter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr_substitution * m_subst = nullptr;
unsigned long long m_max_memory; // in bytes
bool m_new_subst = false;
unsigned m_max_steps = UINT_MAX;
unsigned m_max_steps = UINT_MAX;
bool m_pull_cheap_ite = true;
bool m_flat = true;
bool m_cache_all = false;
Expand Down Expand Up @@ -180,7 +180,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = args[0]->get_sort()->get_family_id();
if (s_fid == m_a_rw.get_fid())
if (s_fid == m_a_rw.get_fid())
st = m_a_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_eq_core(args[0], args[1], result);
Expand All @@ -193,10 +193,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
else if (s_fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
if (k == OP_EQ) {
SASSERT(num == 2);
return st;
st = apply_tamagotchi(args[0], args[1], result);
if (st != BR_FAILED)
return st;
Expand All @@ -210,16 +207,23 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return st;
}
if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
st = m_seq_rw.mk_bool_app(f, num, args, result);
st = m_seq_rw.mk_bool_app(f, num, args, result);
if (st != BR_FAILED)
return st;
}
if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
if (k == OP_DISTINCT && num > 0) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why two nested ifs?

if (m_bv_rw.is_bv(args[0])) {
st = m_bv_rw.mk_distinct(num, args, result);
if (st != BR_FAILED)
return st;
}
}

return m_b_rw.mk_app_core(f, num, args, result);
}
Expand Down Expand Up @@ -250,7 +254,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (fid == m_seq_rw.get_fid())
return m_seq_rw.mk_app_core(f, num, args, result);
if (fid == m_char_rw.get_fid())
return m_char_rw.mk_app_core(f, num, args, result);
return m_char_rw.mk_app_core(f, num, args, result);
if (fid == m_rec_rw.get_fid())
return m_rec_rw.mk_app_core(f, num, args, result);
return BR_FAILED;
Expand Down