C to Z3 Cheat Sheet
This C to Z3 cheat sheet provides a comprehensive guide for converting C data types and operations to their corresponding Z3 representations. Z3 is a high-performance theorem prover developed by Microsoft Research, and it is often used in formal verification of software and hardware.
Types
This section lists the mapping between common C data types and their corresponding sorts in Z3. For the purpose of this cheat sheet, we assume that `long` is 64-bit, `int` is 32-bit, `short` is 16-bit, and `char` is 8-bit. Note that in C, the sizes of these types can vary depending on the platform and compiler.
| C Type | Z3 Sort |
|---|---|
_Bool
|
Bool
|
char
|
(_ BitVec 8)
|
short
|
(_ BitVec 16)
|
int
|
(_ BitVec 32)
|
long
|
(_ BitVec 64)
|
float
|
Float32(_ FloatingPoint 8 24)
|
double
|
Float64(_ FloatingPoint 11 53)
|
BASE array[N]
|
(Array (_ BitVec M) BASE)
|
Constants
| C Constant | Z3 Sort | Comment |
|---|---|---|
123
|
(_ bv123 32)
|
|
-123
|
(bvneg (_ bv123 32))
|
|
12.3f
|
((_ to_fp 8 24) RNE 12.3)
|
|
-12.3f
|
(fp.neg ((_ to_fp 8 24) RNE 12.3))
|
|
12.3
|
((_ to_fp 11 53) RNE 12.3)
|
|
-12.3
|
(fp.neg ((_ to_fp 11 53) RNE 12.3))
|
|
NAN
|
(_ NaN 8 24)
|
|
INFINITY
|
(_ +oo 8 24)
|
|
-INFINITY
|
(_ -oo 8 24)
|
|
0.0f
|
(_ +zero 8 24)
|
|
-0.0f
|
(_ -zero 8 24)
|
|
| 12.3e-9 | ((_ to_fp 8 24) RNE (/ 12.3 1000000000))((_ to_fp 8 24) RNE 0.0000000123)
|
SMT2/Z3 does not support scientific notation of floating point numbers. |
C Operators
| C Operator | Z3 Integer | Z3 Floating Point | Comment |
|---|---|---|---|
| a + b | (+ a b)
|
(fp.add RNE a b)
|
|
| a - b | (- a b)
|
(fp.sub RNE a b)
|
|
| a * b | (* a b)
|
(fp.mul RNE a b)
|
|
| a / b | (div a b)
|
(fp.div RNE a b)
|
|
| a % b | (mod a b)
|
||
| a == b | (= a b)
|
(fp.eq a b)
|
|
| a != b | (not (= a b))
|
(not (fp.eq a b))
|
|
| a < b | (< a b)
|
(fp.lt a b)
|
|
| a <= b | (<= a b)
|
(fp.leq a b)
|
|
| a > b | (> a b)
|
(fp.gt a b)
|
|
| a >= b | (>= a b)
|
(fp.geq a b)
|
|
| a && b | (ite (and a b) (_ bv1 32) (_ bv0 32))
|
(ite (and a b) ((_ to_fp 8 24) RNE 1.0) ((_ to_fp 8 24) RNE 0.0))
|
a and b must be first converted to _Bool.
The result of these operators is int in C (and not _Bool). |
| a || b | (ite (or a b) (_ bv1 32) (_ bv0 32))
|
(ite (or a b) ((_ to_fp 8 24) RNE 1.0) ((_ to_fp 8 24) RNE 0.0))
| |
| !a | (ite (not a) (_ bv1 32) (_ bv0 32))
|
(ite (not a) ((_ to_fp 8 24) RNE 1.0) ((_ to_fp 8 24) RNE 0.0))
| |
| a & b | (bvand a b)
|
||
| a | b | (bvor a b)
|
||
| a ^ b | (bvxor a b)
|
||
| ~a | (bvnot a)
|
Type Conversion
This section provides a detailed guide on how to convert between different C data types using Z3 representations. The first column indicates the source type, while the first row shows the target type. For each conversion:
- If there are two lines in the cell, the first line represents the conversion for unsigned types and the second line for signed types.
- In the conversion formulas,
fis used as a placeholder for the value being converted. - For all floating-point to integer conversions, the truncation towards zero (RTZ) rounding mode is used in conformance to the C/C++ standards.
- For all integer to floating-point conversions, the round to nearest, ties to even (RNE) rounding mode is shown in the table. According to the C/C++ standards, the rounding mode can be changed by the
fesetroundfunction. Please note that gcc and clang compilers use RNE unless-frounding-mathis used.
| From \ To | _Bool | char | short | int | long | float | double |
|---|---|---|---|---|---|---|---|
| _Bool | f
|
(ite f (_ bv1 8) (_ bv0 8))
|
(ite f (_ bv1 16) (_ bv0 16))
|
(ite f (_ bv1 32) (_ bv0 32))
|
(ite f (_ bv1 64) (_ bv0 64))
|
(ite f ((_ to_fp 8 24) RNE 1.0) ((_ to_fp 8 24) RNE 0.0))
|
(ite f ((_ to_fp 11 53) RNE 1.0) ((_ to_fp 11 53) RNE 0.0))
|
| char | (not (= f (_ bv0 8)))
|
f
|
((_ zero_extend 8) f)
|
((_ zero_extend 24) f)
|
((_ zero_extend 56) f)
|
((_ to_fp_unsigned 8 24) RNE f)
|
((_ to_fp_unsigned 11 53) RNE f)
|
| short | (not (= f (_ bv0 16)))
|
((_ extract 7 0) f)
|
f
|
((_ zero_extend 16) f)
|
((_ zero_extend 48) f)
|
((_ to_fp_unsigned 8 24) RNE f)
|
((_ to_fp_unsigned 11 53) RNE f)
|
| int | (not (= f (_ bv0 32)))
|
((_ extract 7 0) f)
|
((_ extract 15 0) f)
|
f
|
((_ zero_extend 32) f)
|
((_ to_fp_unsigned 8 24) RNE f)
|
((_ to_fp_unsigned 11 53) RNE f)
|
| long | (not (= f (_ bv0 64)))
|
((_ extract 7 0) f)
|
((_ extract 15 0) f)
|
((_ extract 31 0) f)
|
f
|
((_ to_fp_unsigned 8 24) RNE f)
|
((_ to_fp_unsigned 11 53) RNE f)
|
| float | (not (fp.eq f ((_ to_fp 8 24) RNE 0.0)))
|
((_ fp.to_ubv 8) RTZ f)
|
((_ fp.to_ubv 16) RTZ f)
|
((_ fp.to_ubv 32) RTZ f)
|
((_ fp.to_ubv 64) RTZ f)
|
f
|
((_ to_fp 11 53) RNE f)
|
| double | (not (fp.eq f ((_ to_fp 11 53) RNE 0.0)))
|
((_ fp.to_ubv 8) RTZ f)
|
((_ fp.to_ubv 16) RTZ f)
|
((_ fp.to_ubv 32) RTZ f)
|
((_ fp.to_ubv 64) RTZ f)
|
((_ to_fp 8 24) RNE f)
|
f
|
Floating Point Rounding Modes
This section describes the mapping between C rounding macros and Z3 rounding modes. The macros are defined in fenv.h and are used by fesetround and fefetround (see [1]). C uses FE_TONEAREST as default rounding mode.
| C Rounding Macro | Z3 Short Mode | Z3 Long Mode | Explanation |
|---|---|---|---|
| FE_TONEAREST | RNE | roundNearestTiesToEven | Round to the nearest value; if the number falls midway, round to the nearest even number. |
| FE_DOWNWARD | RTN | roundTowardNegative | Round towards negative infinity (i.e., round down). |
| FE_UPWARD | RTP | roundTowardPositive | Round towards positive infinity (i.e., round up). |
| FE_TOWARDZERO | RTZ | roundTowardZero | Round towards zero (i.e., truncate the decimal part). |
| N/A | RNA | roundNearestTiesToAway | Round to the nearest value; if the number falls midway, round to the nearest value away from zero. Not supported by C. |
External Links
- The Z3 Theorem Prover
- Floating point module implementation in Z3
- Function
fpa_decl_plugin::get_op_namescontains a list of all floating point functions and rounding modes.
- Function
- C language rounding modes