Project

General

Profile

Feature #8203

bv2nat\int2bv operations

Added by Sergey Smolov about 3 years ago. Updated about 3 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Category:
Solver
Target version:
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

History

#1

Updated by Sergey Smolov about 3 years ago

  • Assignee changed from Andrei Tatarnikov to Sergey Smolov
#2

Updated by Sergey Smolov about 3 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

#3

Updated by Sergey Smolov about 3 years ago

  • Subject changed from bv2int\int2bv operations to bv2nat\int2bv operations
#4

Updated by Sergey Smolov about 3 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100
#5

Updated by Andrei Tatarnikov about 3 years ago

  • Status changed from Resolved to Closed
  • Published in build set to 0.4.25

Also available in: Atom PDF