Actions
Feature #8203
closedbv2nat\int2bv operations
Start date:
05/20/2017
Due date:
% Done:
100%
Estimated time:
Published in build:
0.4.25
Description
bv2int converts bit vector argument to integer
int2bv takes integer length parameter and an integer argument and converts it to bit vector of the specified length
Updated by Sergey Smolov almost 7 years ago
- Assignee changed from Andrei Tatarnikov to Sergey Smolov
Updated by Sergey Smolov almost 7 years ago
Here is a fragment of the header for the newest Z3 release 4.3.5:
- Z3_OP_INT2BV Coerce integer to bit-vector. NB. This function
is not supported by the decision procedures. Only the most
rudimentary simplification rules are applied to this function.
- Z3_OP_BV2INT Coerce bit-vector to integer. NB. This function
is not supported by the decision procedures. Only the most
rudimentary simplification rules are applied to this function.
It seems that CVC4 supports operations that are called bv2nat\int2bv
Updated by Sergey Smolov almost 7 years ago
- Subject changed from bv2int\int2bv operations to bv2nat\int2bv operations
Updated by Sergey Smolov almost 7 years ago
- Status changed from New to Resolved
- % Done changed from 0 to 100
Updated by Andrei Tatarnikov almost 7 years ago
- Status changed from Resolved to Closed
- Published in build set to 0.4.25
Actions