\brief Get or create the basic block with the given name

\brief Lower or equal comparison This is an optimized implementation.

\brief Equality comparison

\brief Get the variable

\brief Left shift Returns the left binary shift of `lhs` by `rhs`, with wrapping. For signed integers, `overflow` is set to true if it shifts out an

\brief Logical shift right Returns the logical right binary shift of `lhs` by `rhs`. The most significant bits of the result are filled with zero bit

\brief Arithmetic shift right Returns the arithmetic right binary shift of `lhs` by `rhs`. The most significant bits of the result are filled with th

\brief Get the n-th argument

\brief Left shift without wrapping The right hand side has to be between 0 and bit_width - 1

\brief Exact logical shift right The right hand side has to be between 0 and bit_width - 1

\brief Exact arithmetic shift right The right hand side has to be between 0 and bit_width - 1

\brief Addition Returns the sum of the operands, with wrapping.

\brief Return the symbol with the given name, or nullptr

\brief Subtraction Returns the difference of the operands, with wrapping.

\brief Remainder Returns the remainder of the operands. For unsigned integers, the result is the classic modulo operator. For signed integers, the r

\brief Bitwise AND Returns the bitwise AND of the operands.

\brief Bitwise XOR Returns the bitwise XOR of the operands.

Helper for enumerations

\brief Get the gauge for the given variable

\brief Division Returns the quotient of the operands. For unsigned integers, this is the unsigned division. For signed integers, this is the signed

\brief Bitwise OR Returns the bitwise OR of the operands.

\brief Forget all informations about variable k

\brief Multiplication Returns the product of the operands, with wrapping.

\brief Addition without wrapping

\brief Substraction without wrapping

\brief Return `n mod d` The result `r` will satisfy: `n = q * abs(d) + r` with `0 <= r < abs(d)` The sign of `d` is ignored, and the result is alway

\brief Get the result variable

Gets a value from statistics table

\brief Return true if the literal is a pointer variable

\brief Convert the gauge to an interval Return boost::none if one of the bound contains a variable.

\brief Return the greatest common divisor of the given numbers The result is always positive even if one or both input operands are negative. Except

\brief Return the bit width of the integer

\brief Return the constant

\brief Return the bit width of the constant

\brief Get the called value

\brief Cast the machine integer to the given bit width and sign This is equivalent to trunc()/ext() + sign_cast() (in this specific order)

\brief Return the machine integer as a ZNumber If this is a signed integer, the result is within [-2**(n-1), 2**(n-1)-1] Otherwise, the result is wit

\brief Return the type of the variable

\brief End iterator over the list of basic blocks

\brief Return the signedness (Signed or Unsigned) of the constant

\brief Return true if the literal is a machine integer variable

\brief Return the signedness (Signed or Unsigned) of the integer

\brief Add a successor

\brief Truncate the machine integer to the given bit width

\brief Get the value operand

\brief If the cell set is a singleton {c}, return c, otherwise return boost::none

\brief Return true if bit-width <= 64

\brief End iterator over the pairs (variable, interval)

\brief Change the machine integer sign (bitcast)

\brief Begin iterator over the list of basic blocks

\brief Extend the machine integer to the given bit width

\brief Return the signedness (Signed or Unsigned) of the interval

\brief Multiplication without wrapping

\brief Return the bit width of the interval

\brief Clear the matrix

\brief Return true if the literal is a constant machine integer