mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

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

Browse source 
* Fixed problem with registering bitvector functions

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

* Removed debug output

* Incorporated Nikolaj's comments

* Simplifications
This commit is contained in:
Clemens Eisenhofer 2022-04-09 21:46:21 +02:00 • committed by GitHub
parent f55b233228
commit 0b20a4ebf4
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 28 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2803,6 +2803,21 @@ 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
if (sz >= 32)
return BR_FAILED;
if (num_args <= 1u << sz)
return BR_FAILED;
result = m().mk_false();
return BR_DONE;
}
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;