pyfcstm.utils.fixed

Fixed-width integer types matching C/C++/Java and Z3 BitVec behavior.

This module provides immutable fixed-width integer types (int8, int16, int32, int64, uint8, uint16, uint32, uint64) that wrap ctypes and replicate the overflow/underflow behavior of C/C++/Java integer arithmetic. All operations are designed to align exactly with Z3 BitVec semantics for use alongside the constraint solver.

All arithmetic operations follow C/C++/Java and Z3 BitVec semantics including:

• Two’s complement representation for signed integers

• Wraparound on overflow/underflow

• Bitwise operations

• Implicit conversion when operating with Python int

Z3 BitVec operation correspondence:

Python operator	Z3 equivalent	Notes
//, / (s)	/ (SDiv/bvsdiv)	Truncate toward zero; INT_MIN//-1 wraps
% (signed)	SRem (bvsrem)	Sign follows dividend; differs from Z3’s % (bvsmod, sign follows divisor)
//, / (u)	UDiv (bvudiv)	Standard unsigned division
% (unsigned)	URem (bvurem)	Standard unsigned remainder; differs from Z3’s % (bvsmod)
>> (signed)	>> (bvashr)	Arithmetic: fills with sign bit
>> (unsigned)	LShR (bvlshr)	Logical: fills with 0
<<	<< (bvshl)	Shift >= bit-width yields 0
~	~	Bitwise NOT (complement all bits)
Unary -	Unary -	Two’s complement; -INT_MIN == INT_MIN

Shift amount convention: When a _FixedInt value is used as the shift amount, its bit pattern is interpreted as unsigned (matching Z3 bvshl/bvashr/ bvlshr). For example, Int8(1) << Int8(-1) shifts by 255 positions (the unsigned value of the 8-bit pattern 0xFF), yielding Int8(0). Plain Python int shift amounts retain standard Python behaviour (negative values raise ValueError).

Example:

>>> from pyfcstm.utils.fixed import Int8, UInt8
>>> x = Int8(127)
>>> x + 1
Int8(-128)
>>> y = UInt8(255)
>>> y + 1
UInt8(0)

__all__

pyfcstm.utils.fixed.__all__ = ['Int8', 'Int16', 'Int32', 'Int64', 'UInt8', 'UInt16', 'UInt32', 'UInt64']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

Int8

class pyfcstm.utils.fixed.Int8(value: int | _FixedInt = 0)

8-bit signed integer (-128 to 127).

Wraps ctypes.c_int8 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = Int8(127)
>>> x + 1
Int8(-128)
>>> x - 200
Int8(183)

Int16

class pyfcstm.utils.fixed.Int16(value: int | _FixedInt = 0)

16-bit signed integer (-32768 to 32767).

Wraps ctypes.c_int16 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = Int16(32767)
>>> x + 1
Int16(-32768)

Int32

class pyfcstm.utils.fixed.Int32(value: int | _FixedInt = 0)

32-bit signed integer (-2147483648 to 2147483647).

Wraps ctypes.c_int32 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = Int32(2147483647)
>>> x + 1
Int32(-2147483648)

Int64

class pyfcstm.utils.fixed.Int64(value: int | _FixedInt = 0)

64-bit signed integer (-9223372036854775808 to 9223372036854775807).

Wraps ctypes.c_int64 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = Int64(9223372036854775807)
>>> x + 1
Int64(-9223372036854775808)

UInt8

class pyfcstm.utils.fixed.UInt8(value: int | _FixedInt = 0)

8-bit unsigned integer (0 to 255).

Wraps ctypes.c_uint8 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = UInt8(255)
>>> x + 1
UInt8(0)
>>> x - 1
UInt8(254)

UInt16

class pyfcstm.utils.fixed.UInt16(value: int | _FixedInt = 0)

16-bit unsigned integer (0 to 65535).

Wraps ctypes.c_uint16 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = UInt16(65535)
>>> x + 1
UInt16(0)

UInt32

class pyfcstm.utils.fixed.UInt32(value: int | _FixedInt = 0)

32-bit unsigned integer (0 to 4294967295).

Wraps ctypes.c_uint32 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = UInt32(4294967295)
>>> x + 1
UInt32(0)

UInt64

class pyfcstm.utils.fixed.UInt64(value: int | _FixedInt = 0)

64-bit unsigned integer (0 to 18446744073709551615).

Wraps ctypes.c_uint64 to provide C/C++/Java-style overflow behavior.

Parameters:

value (Union[int, _FixedInt], optional) – Initial value, defaults to 0

Example:

>>> x = UInt64(18446744073709551615)
>>> x + 1
UInt64(0)