API Reference¶

class zbitvector.Symbolic(term: Any, /)¶

Bases: ABC

Represents an immutable symbolic value. This abstract base class is inherited by Constraint, Uint and Int.

__eq__(other: Self, /) → Constraint¶

Check if this expression is equal to other.

SMT-LIB:: (= self other)

>>> Uint8(1) == Uint8(3)
Constraint(`false`)

__ne__(other: Self, /) → Constraint¶

Check if this expression is not equal to other.

SMT-LIB:: (distinct self other)

>>> Uint8(2) != Uint8(5)
Constraint(`true`)

class zbitvector.Constraint(value: bool | str, /)¶

Bases: Symbolic

Represents a symbolic boolean expression. Possible concrete values are True and False.

To create a Constraint representing a concrete value, pass a bool to the constructor:

>>> Constraint(True)
Constraint(`true`)

To create a Constraint representing a symbolic variable, pass a variable name to the constructor:

>>> Constraint("C")
Constraint(`C`)

__and__(other: Self, /) → Self¶

Compute the boolean AND of this constraint with other.

SMT-LIB:: (and self other)

>>> Constraint(True) & Constraint(False)
Constraint(`false`)

__bool__() → Never¶

Prohibit using Constraint in a boolean context.

Without this check, all instances of Constraint would be considered true and it would be easy to mis-use Constraint in an if statement:

a, b = Uint8(...), Uint8(...)
if a > b:
    ...
else:
    ...  # unreachable!

__invert__() → Self¶

Compute the boolean NOT of this constraint.

SMT-LIB:: (not self)

>>> ~Constraint(True)
Constraint(`false`)

__or__(other: Self, /) → Self¶

Compute the boolean OR of this constraint with other.

SMT-LIB:: (or self other)

>>> Constraint(True) | Constraint(False)
Constraint(`true`)

__xor__(other: Self, /) → Self¶

Compute the boolean XOR of this constraint with other.

SMT-LIB:: (xor self other)

>>> Constraint(True) ^ Constraint(False)
Constraint(`true`)

ite(then: Symbolic, else_: Symbolic, /) → Symbolic¶

Perform an if-then-else based on this constraint. The result is then if the constraint evaluates to True and else_ otherwise.

SMT-LIB:: (ite self then else_)

>>> Constraint(True).ite(Uint8(0xA), Uint8(0xB))
Uint8(`#x0a`)

reveal() → bool | None¶

Reveal the simplified value of this constraint without invoking the solver. If the constraint does not simplify to a constant literal, returns None.

>>> (Constraint("C") | Constraint(True)).reveal()
True

>>> (Constraint("C") | Constraint(False)).reveal() is None
True

class zbitvector.BitVector(value: int | str, /)¶

Bases: Symbolic, Generic[N]

Represents a symbolic N-bit bitvector. This abstract base class is inherited by Uint and Int.

SMT-LIB:: theory of fixed-sized bitvectors

To create a BitVector representing a concrete value, pass an int to the constructor:

>>> Uint8(0)
Uint8(`#x00`)

To create a BitVector representing a symbolic variable, pass a variable name to the constructor:

>>> Int8("I")
Int8(`I`)

__add__(other: Self, /) → Self¶

Compute the result of adding other to this bitvector.

SMT-LIB:: (bvadd self other)

>>> Uint8(7) + Uint8(3)
Uint8(`#x0a`)

>>> Int8(-1) + Int8(3)
Int8(`#x02`)

>>> Uint8(255) + Uint8(5)
Uint8(`#x04`)

__and__(other: Self, /) → Self¶

Compute the bitwise AND of this bitvector with other.

SMT-LIB:: (bvand self other)

>>> Uint8(7) & Uint8(9)
Uint8(`#x01`)

__invert__() → Self¶

Compute the bitwise NOT of this bitvector.

SMT-LIB:: (bvnot self)

>>> ~Uint8(7)
Uint8(`#xf8`)

abstract __le__(other: Self, /) → Constraint¶: Return self<=value.

__lshift__(other: Uint[N], /) → Self¶

Compute the result of left-shifting this bitvector by other bits. Note that other must be a Uint.

SMT-LIB:: (bvshl self other)

>>> Uint8(7) << Uint8(3)
Uint8(`#x38`)

>>> Int8(-1) << Int8(3)
Int8(`#xf8`)

abstract __lt__(other: Self, /) → Constraint¶: Return self<value.

__mul__(other: Self, /) → Self¶

Compute the result of multiplying this bitvector by other.

SMT-LIB:: (bvmul self other)

>>> Uint8(7) * Uint8(3)
Uint8(`#x15`)

>>> Int8(-1) * Int8(3)
Int8(`#xfd`)

>>> Uint8(16) * Uint8(23)
Uint8(`#x70`)

__or__(other: Self, /) → Self¶

Compute the bitwise OR of this bitvector with other.

SMT-LIB:: (bvor self other)

>>> Uint8(7) | Uint8(9)
Uint8(`#x0f`)

__sub__(other: Self, /) → Self¶

Compute the result of subtracting other from this bitvector.

SMT-LIB:: (bvsub self other)

>>> Uint8(7) - Uint8(3)
Uint8(`#x04`)

>>> Int8(-1) - Int8(3)
Int8(`#xfc`)

>>> Uint8(1) - Uint8(5)
Uint8(`#xfc`)

__xor__(other: Self, /) → Self¶

Compute the bitwise XOR of this bitvector with other.

SMT-LIB:: (bvxor self other)

>>> Uint8(7) ^ Uint8(9)
Uint8(`#x0e`)

class zbitvector.Uint(value: int | str, /)¶

Bases: BitVector[N]

Represents an N-bit unsigned integer.

__le__(other: Self, /) → Constraint¶

Check if this bitvector is less than or equal to other using an unsigned comparison.

SMT-LIB:: (bvule self other)

>>> Uint8(7) <= Uint8(3)
Constraint(`false`)

__lt__(other: Self, /) → Constraint¶

Check if this bitvector is strictly less than other using an unsigned comparison.

SMT-LIB:: (bvult self other)

>>> Uint8(7) < Uint8(3)
Constraint(`false`)

__mod__(other: Self, /) → Self¶

Compute the remainder when dividing this bitvector by other using unsigned integer division.

If the divisor is zero, the result is the dividend.

SMT-LIB:: (bvurem self other)

>>> Uint8(7) % Uint8(3)
Uint8(`#x01`)

>>> Uint8(7) % Uint8(0)
Uint8(`#x07`)

__rshift__(other: Uint[N], /) → Self¶

Compute the result of right-shifting this bitvector by other bits using a logical right shift.

SMT-LIB:: (bvlshr self other)

>>> Uint8(255) >> Uint8(2)
Uint8(`#x3f`)

__truediv__(other: Self, /) → Self¶

Compute the quotient when dividing this bitvector by other using unsigned integer division.

If the divisor is zero, the result is the bitvector of all ones.

SMT-LIB:: (bvudiv self other)

>>> Uint8(7) / Uint8(3)
Uint8(`#x02`)

>>> Uint8(7) / Uint8(0)
Uint8(`#xff`)

into(other: type[BitVector[M]], /) → BitVector[M]¶

Forcibly convert this bitvector to the given type.

When converting to an Int, the underlying bits are reinterpreted as a two’s complement signed integer:

>>> Uint8(255).into(Int8)
Int8(`#xff`)

When converting to a longer Uint, the underling bits are zero-extended:

>>> Uint8(0xFF).into(Uint64)
Uint64(`#x00000000000000ff`)

When converting to a shorter Uint, the underlying bits are truncated:

>>> Uint64(0x1234).into(Uint8)
Uint8(`#x34`)

reveal() → int | None¶

Reveal the simplified value of this constraint without invoking the solver. If the constraint does not simplify to a constant literal, returns None.

>>> (Uint8(2) + Uint8(3)).reveal()
5

>>> (Uint8("X") + Uint8(1)).reveal() is None
True

class zbitvector.Int(value: int | str, /)¶

Bases: BitVector[N]

Represents an N-bit signed integer in two’s complement form.

__le__(other: Self, /) → Constraint¶

Check if this bitvector is less than or equal to other using a signed comparison.

SMT-LIB:: (bvsle self other)

>>> Int8(-1) <= Int8(3)
Constraint(`true`)

__lt__(other: Self, /) → Constraint¶

Check if this bitvector is strictly less than other using a signed comparison.

SMT-LIB:: (bvslt self other)

>>> Int8(-1) < Int8(3)
Constraint(`true`)

__mod__(other: Self, /) → Self¶

Compute the remainder when dividing this bitvector by other using signed integer division.

The sign of the remainder follows the sign of the dividend. If the divisor is zero, the result is the dividend.

SMT-LIB:: (bvsrem self other)

>>> Int8(7) % Int8(-3)
Int8(`#x01`)

>>> Int8(-7) % Int8(3)
Int8(`#xff`)

>>> Int8(-7) % Int8(-3)
Int8(`#xff`)

>>> Int8(7) % Int8(0)
Int8(`#x07`)

__rshift__(other: Uint[N], /) → Self¶

Compute the result of right-shifting this bitvector by other bits using an arithmetic right shift. Note that other must be a Uint.

SMT-LIB:: (bvashr self other)

>>> Int8(-8) >> Uint8(2)
Int8(`#xfe`)

__truediv__(other: Self, /) → Self¶

Compute the quotient when dividing this bitvector by other using signed integer division.

If the divisor is zero, the result is -1.

SMT-LIB:: (bvsdiv self other)

>>> Int8(7) / Int8(-3)
Int8(`#xfe`)

>>> Int8(-7) / Int8(3)
Int8(`#xfe`)

>>> Int8(-7) / Int8(-3)
Int8(`#x02`)

>>> Int8(7) / Int8(0)
Int8(`#xff`)

into(other: type[BitVector[M]], /) → BitVector[M]¶

Forcibly convert this bitvector to the given type.

When converting to a Uint, the underlying bits are reinterpreted as an unsigned integer, from two’s complement form:

>>> Int8(-1).into(Uint8)
Uint8(`#xff`)

When converting to a longer Int, the underling bits are sign-extended:

>>> Int8(0xFF).into(Int64)
Int64(`#xffffffffffffffff`)

When converting to a shorter Int, the underlying bits are truncated:

>>> Int64(0xFFFFFFFFFFFFFF01).into(Int8)
Int8(`#x01`)

reveal() → int | None¶

Reveal the simplified value of this constraint without invoking the solver. If the constraint does not simplify to a constant literal, returns None.

>>> (Int8(2) - Int8(3)).reveal()
-1

>>> (Int8("Y") + Int8(1)).reveal() is None
True

class zbitvector.Array(value: V | str, /)¶

Bases: Generic[K, V]

Represents a mutable symbolic array mapping a BitVector to a BitVector. Arrays do not have a length: they map the full domain to the full range.

SMT-LIB:: theory of functional arrays

To create an Array where all keys map to a single default value, pass a BitVector to the constructor:

>>> Array[Uint8, Uint64](Uint64(0))
Array[Uint8, Uint64](`#x0000000000000000`)

To create a fully unconstrained Array, pass a variable name to the constructor:

>>> Array[Int8, Int64]("A")
Array[Int8, Int64](`A`)

__getitem__(key: K) → V¶

Look up the item at index key.

SMT-LIB:: (select self key)

>>> A = Array[Uint8, Uint64](Uint64(0))
>>> A[Uint8(100)]
Uint64(`#x0000000000000000`)

__setitem__(key: K, value: V) → None¶

Set the item at index key to value.

SMT-LIB:: (store self key value)

>>> A = Array[Uint8, Uint64](Uint64(0))
>>> A[Uint8(1)] = Uint64(0x1234)
>>> A[Uint8(1)]
Uint64(`#x0000000000001234`)

class zbitvector.Solver¶

Bases: object

A SAT solver instance.

>>> s = Solver()
>>> s.add(Uint8("B") == Uint8(1))
>>> s.check()
True
>>> s.evaluate(Uint8("B"))
1
>>> s.add(Uint8("B") == Uint8(2))
>>> s.check()
False

add(assertion: Constraint, /) → None¶: Permanently add an assertion to the solver state.

check(*assumptions: Constraint) → bool¶

Check whether the solver state is satisfiable.

If provided, assumptions are temporarily added to the solver state for this check only.

evaluate(bv: BitVector[N], /) → int¶

Return a value for the given BitVector consistent with the solver’s model.

Raises a ValueError if these preconditions are not met:

The most recent call to check() returned True.
No subsequent calls to add() have been made.
With the Bitwuzla backend: no subsequent calls to check() have been made with any other Solver instance.