python_math Class Reference

Handles mathematical operations for Python-to-C conversion. More...

#include <python_math.h>

Public Member Functions
std::optional< double >	try_resolve_constant_double (const exprt &operand) const
	Resolve a constant-like expression (constant or constant-valued symbol) to a host double when possible.
	python_math (python_converter &conv, contextt &ctx, type_handler &th)
	Constructor.
bool	is_math_dispatch_target (const std::string &caller, const std::string &func_name) const
	Classify whether a call should be handled by math dispatch.
bool	is_math_dispatch_target_cached (const std::string &caller, const std::string &func_name)
	Cached variant of is_math_dispatch_target.
bool	is_unary_dispatch_function (std::string_view func_name) const
	Return true when func_name is handled by unary math dispatch.
bool	is_binary_dispatch_function (std::string_view func_name) const
	Return true when func_name is handled by binary math dispatch.
exprt	handle (std::string_view func_name, exprt operand, const nlohmann::json &element)
	Dispatch supported unary math functions through a single entrypoint.
exprt	handle (std::string_view func_name, exprt lhs, exprt rhs, const nlohmann::json &element)
	Dispatch supported binary math functions through a single entrypoint.
exprt	compute_expr (const exprt &expr) const
	Fold a +,-,*,/ expression to a constant when it is genuinely one.
exprt	handle_power (exprt lhs, exprt rhs)
	Handle Python's power operator (**).
exprt	handle_power_symbolic (exprt base, exprt exp)
	Handle power operation symbolically using C's pow() function.
exprt	handle_power_symbolic_exponent (exprt lhs, exprt rhs)
	An integer power whose exponent is not a constant: pow(), or the bits of 2.0 ** n for a base of 2.
exprt	build_power_expression (const exprt &base, const BigInt &exp)
	Build power expression using exponentiation by squaring.
exprt	handle_modulo (exprt lhs, exprt rhs, const nlohmann::json &element)
	Handle Python's modulo operator (%).
exprt	handle_int_modulo (const exprt &lhs, const exprt &rhs, const exprt &bin_expr)
	Handle Python's integer modulo operator (%).
exprt	handle_floor_division (const exprt &lhs, const exprt &rhs, const exprt &bin_expr)
	Handle Python's floor division operator (//).
void	handle_float_division (exprt &lhs, exprt &rhs, exprt &bin_expr) const
	Handle Python's true division operator (/).
void	promote_int_to_float (exprt &op, const typet &target_type) const
	Promote integer expression to floating-point type.
exprt	handle_sqrt (exprt operand, const nlohmann::json &element)
	Handle square root operation (math.sqrt).
exprt	handle_sin (exprt operand, const nlohmann::json &element)
	Handle sine function (math.sin).
exprt	handle_cos (exprt operand, const nlohmann::json &element)
	Handle cosine function (math.cos).
exprt	handle_divmod (exprt dividend, exprt divisor, const nlohmann::json &element)
	Handle divmod() built-in function.
exprt	handle_numeric_divmod (exprt dividend, exprt divisor, const nlohmann::json &element)
exprt	raise_divmod_type_error (const typet &dividend_type, const typet &divisor_type, const nlohmann::json &element)
	The TypeError is planted as a statement ahead of the call, and an (int, int) tuple stands in for the result so a caller that unpacks it still converts.
exprt	handle_exp (exprt operand, const nlohmann::json &element)
	Handle exponential function (math.exp).
exprt	handle_log (exprt operand, const nlohmann::json &element)
	Handle natural logarithm function (math.log).
exprt	handle_acos (exprt operand, const nlohmann::json &element)
	Handle arccosine function (math.acos).
exprt	handle_atan (exprt operand, const nlohmann::json &element)
	Handle arctangent function (math.atan).
exprt	handle_atan2 (exprt y_operand, exprt x_operand, const nlohmann::json &element)
	Handle two-argument arctangent function (math.atan2).
exprt	handle_log2 (exprt operand, const nlohmann::json &element)
	Handle base-2 logarithm function (math.log2).
exprt	handle_pow (exprt base, exprt exp, const nlohmann::json &element)
	Handle power function (math.pow).
exprt	handle_fabs (exprt operand, const nlohmann::json &element)
	Handle absolute value for floats (math.fabs).
exprt	handle_trunc (exprt operand, const nlohmann::json &element)
	Handle truncate to integer towards zero (math.trunc).
exprt	handle_fmod (exprt lhs, exprt rhs, const nlohmann::json &element)
	Handle floating-point remainder (math.fmod).
exprt	handle_copysign (exprt lhs, exprt rhs, const nlohmann::json &element)
	Handle copy sign (math.copysign).
exprt	handle_tan (exprt operand, const nlohmann::json &element)
	Handle tangent function (math.tan).
exprt	handle_asin (exprt operand, const nlohmann::json &element)
	Handle arcsine function (math.asin).
exprt	handle_sinh (exprt operand, const nlohmann::json &element)
	Handle hyperbolic sine function (math.sinh).
exprt	handle_cosh (exprt operand, const nlohmann::json &element)
	Handle hyperbolic cosine function (math.cosh).
exprt	handle_tanh (exprt operand, const nlohmann::json &element)
	Handle hyperbolic tangent function (math.tanh).
exprt	handle_log10 (exprt operand, const nlohmann::json &element)
	Handle base-10 logarithm function (math.log10).
exprt	handle_expm1 (exprt operand, const nlohmann::json &element)
	Handle expm1 function (math.expm1).
exprt	handle_log1p (exprt operand, const nlohmann::json &element)
	Handle log1p function (math.log1p).
exprt	handle_exp2 (exprt operand, const nlohmann::json &element)
	Handle exp2 function (math.exp2).
exprt	handle_asinh (exprt operand, const nlohmann::json &element)
	Handle asinh function (math.asinh).
exprt	handle_acosh (exprt operand, const nlohmann::json &element)
	Handle acosh function (math.acosh).
exprt	handle_atanh (exprt operand, const nlohmann::json &element)
	Handle atanh function (math.atanh).
exprt	handle_hypot (exprt lhs, exprt rhs, const nlohmann::json &element)
	Handle hypot function (math.hypot).
exprt	handle_dist (exprt p, exprt q, const nlohmann::json &element)
	Handle dist function (math.dist) for tuple arguments.

Static Public Member Functions
static BigInt	pow_bigint_non_negative (BigInt base, BigInt exp)
static bool	fits_in_width (const BigInt &value, unsigned width, bool is_signed)

Static Public Attributes
static const BigInt	kMaxConstantFoldExponent = 1024

Detailed Description

Handles mathematical operations for Python-to-C conversion.

This class encapsulates all math-related operations in the ESBMC Python frontend, including arithmetic evaluation, power operations, division variants (true division, floor division, modulo), and type promotions required by Python's semantics.

Constructor & Destructor Documentation

python_math()

python_math::python_math	(	python_converter &	conv,
		contextt &	ctx,
		type_handler &	th )

Constructor.

Parameters

conv	Reference to the parent python_converter
ctx	Reference to the symbol table context
th	Reference to the type handler

Member Function Documentation

build_power_expression()

exprt python_math::build_power_expression	(	const exprt &	base,
		const BigInt &	exp )

Build power expression using exponentiation by squaring.

Efficiently constructs a multiplication tree for base**exp using the binary exponentiation algorithm, reducing operations from O(n) to O(log n).

Parameters

base	The base expression
exp	The exponent (must be non-negative integer)

Returns

Expression tree representing the power operation

compute_expr()

exprt python_math::compute_expr

(

const exprt &

expr

)

const

Fold a +,-,*,/ expression to a constant when it is genuinely one.

Returns a constant expression when expr (and all its operands) resolve to integer constants; otherwise returns expr unchanged so callers keep a symbolic encoding. Never fabricates a 0 from a non-constant operand (issue #5915).

Parameters

expr	A +,-,*,/ binary expression

Returns

The folded constant, or expr unchanged if not constant

fits_in_width()

bool python_math::fits_in_width ( const BigInt & value, unsigned width, bool is_signed )

static

handle() [1/2]

exprt python_math::handle	(	std::string_view	func_name,
		exprt	lhs,
		exprt	rhs,
		const nlohmann::json &	element )

Dispatch supported binary math functions through a single entrypoint.

Returns nil_exprt() when func_name is not a supported binary-dispatch target.

handle() [2/2]

exprt python_math::handle	(	std::string_view	func_name,
		exprt	operand,
		const nlohmann::json &	element )

Dispatch supported unary math functions through a single entrypoint.

Returns nil_exprt() when func_name is not a supported unary-dispatch target.

handle_acos()

exprt python_math::handle_acos	(	exprt	operand,
		const nlohmann::json &	element )

Handle arccosine function (math.acos).

handle_acosh()

exprt python_math::handle_acosh	(	exprt	operand,
		const nlohmann::json &	element )

Handle acosh function (math.acosh).

handle_asin()

exprt python_math::handle_asin	(	exprt	operand,
		const nlohmann::json &	element )

Handle arcsine function (math.asin).

handle_asinh()

exprt python_math::handle_asinh	(	exprt	operand,
		const nlohmann::json &	element )

Handle asinh function (math.asinh).

handle_atan()

exprt python_math::handle_atan	(	exprt	operand,
		const nlohmann::json &	element )

Handle arctangent function (math.atan).

handle_atan2()

exprt python_math::handle_atan2	(	exprt	y_operand,
		exprt	x_operand,
		const nlohmann::json &	element )

Handle two-argument arctangent function (math.atan2).

handle_atanh()

exprt python_math::handle_atanh	(	exprt	operand,
		const nlohmann::json &	element )

Handle atanh function (math.atanh).

handle_copysign()

exprt python_math::handle_copysign	(	exprt	lhs,
		exprt	rhs,
		const nlohmann::json &	element )

Handle copy sign (math.copysign).

handle_cos()

exprt python_math::handle_cos	(	exprt	operand,
		const nlohmann::json &	element )

Handle cosine function (math.cos).

Implements Python's math.cos() function by creating a call to C's cos(). Always returns a float (double) result representing the cosine of the angle in radians.

Parameters

operand	The angle in radians (promoted to float if needed)
element	JSON AST node for location information

Returns

Function call expression to cos()

Exceptions

std::runtime_error

if cos symbol not found in symbol table

Examples: math.cos(0) -> 1.0 math.cos(math.pi/2) -> 0.0 (approximately) math.cos(math.pi) -> -1.0 math.cos(2*math.pi) -> 1.0

handle_cosh()

exprt python_math::handle_cosh	(	exprt	operand,
		const nlohmann::json &	element )

Handle hyperbolic cosine function (math.cosh).

handle_dist()

exprt python_math::handle_dist	(	exprt	p,
		exprt	q,
		const nlohmann::json &	element )

Handle dist function (math.dist) for tuple arguments.

handle_divmod()

exprt python_math::handle_divmod	(	exprt	dividend,
		exprt	divisor,
		const nlohmann::json &	element )

Handle divmod() built-in function.

Implements Python's divmod(a, b) function, which returns a tuple containing the quotient and remainder of division: (a // b, a % b).

The function follows Python's floor division semantics:

• The quotient is computed using floor division (rounds toward negative infinity)
• The remainder has the same sign as the divisor
• The mathematical property always holds: a == (a // b) * b + (a % b)

Type handling:

• If either operand is float, both are promoted to float (double)
• Integer operands use integer floor division and modulo
• Float operands use C's floor() function and floating-point modulo

Parameters

dividend	The numerator (value to be divided)
divisor	The denominator (value to divide by)
element	JSON AST node for location information

Returns

Struct expression representing tuple (quotient, remainder) with components named "element_0" (quotient) and "element_1" (remainder)

Exceptions

std::runtime_error

if floor symbol not found (for float division)

Examples: divmod(7, 3) -> (2, 1) [7 = 3*2 + 1] divmod(-7, 3) -> (-3, 2) [-7 = 3*(-3) + 2] divmod(7, -3) -> (-3, -2) [7 = (-3)*(-3) + (-2)] divmod(-7, -3) -> (2, -1) [-7 = (-3)*2 + (-1)] divmod(7.5, 2.0) -> (3.0, 1.5) [7.5 = 2.0*3.0 + 1.5] divmod(10, 5) -> (2, 0) [exact division]

handle_exp()

exprt python_math::handle_exp	(	exprt	operand,
		const nlohmann::json &	element )

Handle exponential function (math.exp).

Implements Python's math.exp() function by creating a call to C's exp(). Always returns a float (double) result representing e raised to the power of the operand.

Parameters

operand	The exponent value (promoted to float if needed)
element	JSON AST node for location information

Returns

Function call expression to exp()

Exceptions

std::runtime_error

if exp symbol not found in symbol table

Examples: math.exp(0) -> 1.0 math.exp(1) -> 2.718... (e) math.exp(2) -> 7.389... math.exp(-1) -> 0.368...

handle_exp2()

exprt python_math::handle_exp2	(	exprt	operand,
		const nlohmann::json &	element )

Handle exp2 function (math.exp2).

handle_expm1()

exprt python_math::handle_expm1	(	exprt	operand,
		const nlohmann::json &	element )

Handle expm1 function (math.expm1).

handle_fabs()

exprt python_math::handle_fabs	(	exprt	operand,
		const nlohmann::json &	element )

Handle absolute value for floats (math.fabs).

handle_float_division()

void python_math::handle_float_division	(	exprt &	lhs,
		exprt &	rhs,
		exprt &	bin_expr ) const

Handle Python's true division operator (/).

Python 3's / operator always performs floating-point division, even with integer operands. This function promotes operands to float and sets up IEEE floating-point division.

Parameters

lhs	Left operand (modified to float if needed)
rhs	Right operand (modified to float if needed)
bin_expr	Binary expression (modified to ieee_div)

handle_floor_division()

exprt python_math::handle_floor_division	(	const exprt &	lhs,
		const exprt &	rhs,
		const exprt &	bin_expr )

Handle Python's floor division operator (//).

Implements floor division: (lhs // rhs) = floor(lhs / rhs) Special handling ensures correct behavior with negative operands: result = (lhs / rhs) - (1 if (lhs % rhs != 0) and signs_differ else 0)

Parameters

lhs	Dividend expression
rhs	Divisor expression
bin_expr	The division expression to modify

Returns

Expression implementing floor division

handle_fmod()

exprt python_math::handle_fmod	(	exprt	lhs,
		exprt	rhs,
		const nlohmann::json &	element )

Handle floating-point remainder (math.fmod).

handle_hypot()

exprt python_math::handle_hypot	(	exprt	lhs,
		exprt	rhs,
		const nlohmann::json &	element )

Handle hypot function (math.hypot).

handle_int_modulo()

exprt python_math::handle_int_modulo	(	const exprt &	lhs,
		const exprt &	rhs,
		const exprt &	bin_expr )

Handle Python's integer modulo operator (%).

Python's % result has the sign of the divisor (floored modulo), unlike C's truncated remainder which has the sign of the dividend. Corrects the C remainder bin_expr so that, e.g., -7 % 3 == 2 and 7 % -3 == -2: result = rem + (rhs if (rem != 0 and signs_differ) else 0)

Parameters

lhs	Dividend expression
rhs	Divisor expression
bin_expr	The C remainder expression (lhs % rhs) to correct

Returns

Expression implementing Python integer modulo

handle_log()

exprt python_math::handle_log	(	exprt	operand,
		const nlohmann::json &	element )

Handle natural logarithm function (math.log).

Implements Python's math.log() function by creating a call to C's log(). Always returns a float (double) result representing the natural logarithm (base e) of the operand.

Domain: x > 0 (positive values only)

• log(0) produces domain error
• log(negative) produces domain error

Parameters

operand	The value to take logarithm of (promoted to float if needed)
element	JSON AST node for location information

Returns

Function call expression to log()

Exceptions

std::runtime_error

if log symbol not found in symbol table

Examples: math.log(1) -> 0.0 math.log(math.e) -> 1.0 math.log(10) -> 2.302... math.log(0) -> domain error at runtime math.log(-1) -> domain error at runtime

handle_log10()

exprt python_math::handle_log10	(	exprt	operand,
		const nlohmann::json &	element )

Handle base-10 logarithm function (math.log10).

handle_log1p()

exprt python_math::handle_log1p	(	exprt	operand,
		const nlohmann::json &	element )

Handle log1p function (math.log1p).

handle_log2()

exprt python_math::handle_log2	(	exprt	operand,
		const nlohmann::json &	element )

Handle base-2 logarithm function (math.log2).

handle_modulo()

exprt python_math::handle_modulo	(	exprt	lhs,
		exprt	rhs,
		const nlohmann::json &	element )

Handle Python's modulo operator (%).

Implements Python's modulo semantics where the result has the sign of the divisor: x % y = x - floor(x/y) * y

This differs from C's fmod where result has the sign of the dividend.

Parameters

lhs	Dividend expression
rhs	Divisor expression
element	JSON AST node for location information

Returns

Expression implementing Python modulo semantics

Exceptions

std::runtime_error

if floor function not found

handle_numeric_divmod()

exprt python_math::handle_numeric_divmod	(	exprt	dividend,
		exprt	divisor,
		const nlohmann::json &	element )

handle_pow()

exprt python_math::handle_pow	(	exprt	base,
		exprt	exp,
		const nlohmann::json &	element )

Handle power function (math.pow).

handle_power()

exprt python_math::handle_power	(	exprt	lhs,
		exprt	rhs )

Handle Python's power operator (**).

Implements Python's exponentiation with special handling for:

• Floating-point operands (delegates to symbolic pow)
• Constant integer exponents (compile-time evaluation)
• Negative exponents (converts to symbolic)
• Special cases (0**n, 1**n, (-1)**n)

Parameters

lhs	Base expression
rhs	Exponent expression

Returns

Expression representing base**exponent

handle_power_symbolic()

exprt python_math::handle_power_symbolic	(	exprt	base,
		exprt	exp )

Handle power operation symbolically using C's pow() function.

Creates a function call to C's pow(base, exp) for cases where compile-time evaluation isn't possible or operands are floating-point.

Parameters

base	Base expression (promoted to double if needed)
exp	Exponent expression (promoted to double if needed)

Returns

Function call expression to pow()

Exceptions

std::runtime_error

if pow symbol not found

handle_power_symbolic_exponent()

exprt python_math::handle_power_symbolic_exponent	(	exprt	lhs,
		exprt	rhs )

An integer power whose exponent is not a constant: pow(), or the bits of 2.0 ** n for a base of 2.

handle_sin()

exprt python_math::handle_sin	(	exprt	operand,
		const nlohmann::json &	element )

Handle sine function (math.sin).

Implements Python's math.sin() function by creating a call to C's sin(). Always returns a float (double) result representing the sine of the angle in radians.

Parameters

operand	The angle in radians (promoted to float if needed)
element	JSON AST node for location information

Returns

Function call expression to sin()

Exceptions

std::runtime_error

if sin symbol not found in symbol table

Examples: math.sin(0) -> 0.0 math.sin(math.pi/2) -> 1.0 math.sin(math.pi) -> 0.0 (approximately) math.sin(-math.pi/2) -> -1.0

handle_sinh()

exprt python_math::handle_sinh	(	exprt	operand,
		const nlohmann::json &	element )

Handle hyperbolic sine function (math.sinh).

handle_sqrt()

exprt python_math::handle_sqrt	(	exprt	operand,
		const nlohmann::json &	element )

Handle square root operation (math.sqrt).

Implements Python's math.sqrt() function by creating a call to C's sqrt(). Always returns a float (double) result. Negative inputs will produce domain errors at runtime (matching Python behavior).

Parameters

operand	The value to take square root of (promoted to float if needed)
element	JSON AST node for location information (optional)

Returns

Function call expression to sqrt()

Exceptions

std::runtime_error

if sqrt symbol not found in symbol table

Examples: math.sqrt(4) -> 2.0 math.sqrt(2) -> 1.414... math.sqrt(0) -> 0.0 math.sqrt(-1) -> domain error at runtime

handle_tan()

exprt python_math::handle_tan	(	exprt	operand,
		const nlohmann::json &	element )

Handle tangent function (math.tan).

handle_tanh()

exprt python_math::handle_tanh	(	exprt	operand,
		const nlohmann::json &	element )

Handle hyperbolic tangent function (math.tanh).

handle_trunc()

exprt python_math::handle_trunc	(	exprt	operand,
		const nlohmann::json &	element )

Handle truncate to integer towards zero (math.trunc).

is_binary_dispatch_function()

bool python_math::is_binary_dispatch_function

(

std::string_view

func_name

)

const

Return true when func_name is handled by binary math dispatch.

is_math_dispatch_target()

bool python_math::is_math_dispatch_target	(	const std::string &	caller,
		const std::string &	func_name ) const

Classify whether a call should be handled by math dispatch.

Returns true for:

• direct math.<func> calls supported by the frontend, and
• internal math wrappers such as __ESBMC_*.

Parameters

caller	Module/object name for attribute calls (e.g., "math")
func_name	Called function name

Returns

true when the call belongs to math dispatch

is_math_dispatch_target_cached()

bool python_math::is_math_dispatch_target_cached	(	const std::string &	caller,
		const std::string &	func_name )

Cached variant of is_math_dispatch_target.

Uses function_call_cache to memoize math-dispatch classification, reducing repeated set lookups during large regression batches.

Parameters

caller	Module/object name for attribute calls (e.g., "math")
func_name	Called function name

Returns

true when the call belongs to math dispatch

is_unary_dispatch_function()

bool python_math::is_unary_dispatch_function

(

std::string_view

func_name

)

const

Return true when func_name is handled by unary math dispatch.

pow_bigint_non_negative()

BigInt python_math::pow_bigint_non_negative ( BigInt base, BigInt exp )

static

promote_int_to_float()

void python_math::promote_int_to_float	(	exprt &	op,
		const typet &	target_type ) const

Promote integer expression to floating-point type.

Converts integer operands to floatbv type, typically for Python's true division where / must always yield float results.

Handles both constant integers (converts literal value) and non-constant integers (updates type metadata).

Parameters

op	The operand to promote (modified in place)
target_type	The target floating-point type

raise_divmod_type_error()

exprt python_math::raise_divmod_type_error	(	const typet &	dividend_type,
		const typet &	divisor_type,
		const nlohmann::json &	element )

The TypeError is planted as a statement ahead of the call, and an (int, int) tuple stands in for the result so a caller that unpacks it still converts.

try_resolve_constant_double()

std::optional< double > python_math::try_resolve_constant_double

(

const exprt &

operand

)

const

Resolve a constant-like expression (constant or constant-valued symbol) to a host double when possible.

Member Data Documentation

kMaxConstantFoldExponent

const BigInt python_math::kMaxConstantFoldExponent = 1024

static

---

The documentation for this class was generated from the following files:

• src/python-frontend/math/python_math.h
• src/python-frontend/math/python_math.cpp