python_set Class Reference

Handles Python set operations and set-specific functionality. More...

#include <python_set.h>

Public Member Functions
	python_set (python_converter &converter, const nlohmann::json &set_node)
exprt	get ()
	Create a set from a set literal.
exprt	get_empty_set ()
	Create an empty set.
exprt	get_from_iterable (const exprt &iterable, const nlohmann::json &element)
	Create a set from an iterable (e.g., set(list) or set(str)).
exprt	build_set_difference_call (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
	Build set difference operation (set1 - set2).
exprt	build_set_intersection_call (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
	Build set intersection operation (set1 & set2).
exprt	build_set_union_call (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
	Build set union operation (set1 | set2).
exprt	build_set_copy (const symbolt &self, const nlohmann::json &element)
	Build a fresh shallow copy of self as a new set.
exprt	build_set_symmetric_difference_call (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
	Build set symmetric difference (set1 ^ set2): (lhs - rhs) ∪ (rhs - lhs), collected into a fresh set.
exprt	build_set_method_call (const symbolt &self, const exprt &other, const nlohmann::json &element, const std::string &method_name)
	Emit the IR for a binary set method (issubset / issuperset / isdisjoint / update / symmetric_difference / union / intersection / difference) called on self with other.
exprt	build_set_relation_call (const exprt &self, const exprt &other, const nlohmann::json &element, const std::string &method_name)
	Emit the IR for issubset / issuperset / isdisjoint over two list-typed expressions and return the bool result expression.

Static Public Member Functions
static exprt	handle_operations (python_converter &converter, const std::string &op, exprt &lhs, exprt &rhs, const nlohmann::json &element)
	Handle set operations (difference, intersection, union) Entry point for all set binary operations.

Detailed Description

Handles Python set operations and set-specific functionality.

This class is responsible for converting Python set operations into ESBMC's intermediate representation. Sets are internally represented as lists with unique elements.

Constructor & Destructor Documentation

python_set()

python_set::python_set ( python_converter & converter, const nlohmann::json & set_node )

inline

Member Function Documentation

build_set_copy()

exprt python_set::build_set_copy	(	const symbolt &	self,
		const nlohmann::json &	element )

Build a fresh shallow copy of self as a new set.

Used for the zero-argument variadic forms s.union()/intersection()/difference(), which return a copy of the set in CPython.

build_set_difference_call()

exprt python_set::build_set_difference_call	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

Build set difference operation (set1 - set2).

Parameters

lhs	Left operand (set expression)
rhs	Right operand (set expression)
element	AST node for location information

Returns

Expression representing the result set

build_set_intersection_call()

exprt python_set::build_set_intersection_call	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

Build set intersection operation (set1 & set2).

Parameters

lhs	Left operand (set expression)
rhs	Right operand (set expression)
element	AST node for location information

Returns

Expression representing the result set

build_set_method_call()

exprt python_set::build_set_method_call	(	const symbolt &	self,
		const exprt &	other,
		const nlohmann::json &	element,
		const std::string &	method_name )

Emit the IR for a binary set method (issubset / issuperset / isdisjoint / update / symmetric_difference / union / intersection / difference) called on self with other.

• issubset / issuperset / isdisjoint return a bool expression.
• update mutates self in place and returns nil.
• symmetric_difference / union / intersection / difference return a fresh set expression and leave self unchanged.

Reuses the same loop / contains / push primitives as build_set_union_call to keep encoding consistent.

build_set_relation_call()

exprt python_set::build_set_relation_call	(	const exprt &	self,
		const exprt &	other,
		const nlohmann::json &	element,
		const std::string &	method_name )

Emit the IR for issubset / issuperset / isdisjoint over two list-typed expressions and return the bool result expression.

Set materialization is unnecessary for these relations (deduplication cannot change a subset/superset/disjoint verdict), so callers may pass any list expression as self — e.g. the iterable argument of a set(<iterable>).issuperset(...) receiver — without building the set.

build_set_symmetric_difference_call()

exprt python_set::build_set_symmetric_difference_call	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

Build set symmetric difference (set1 ^ set2): (lhs - rhs) ∪ (rhs - lhs), collected into a fresh set.

Parameters

lhs	Left operand (set expression)
rhs	Right operand (set expression)
element	AST node for location information

Returns

Expression representing the result set

build_set_union_call()

exprt python_set::build_set_union_call	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

Build set union operation (set1 | set2).

Parameters

lhs	Left operand (set expression)
rhs	Right operand (set expression)
element	AST node for location information

Returns

Expression representing the result set

get()

exprt python_set::get

(

)

Create a set from a set literal.

Returns

Expression representing the set

get_empty_set()

exprt python_set::get_empty_set

(

)

Create an empty set.

Returns

Expression representing the empty set

get_from_iterable()

exprt python_set::get_from_iterable	(	const exprt &	iterable,
		const nlohmann::json &	element )

Create a set from an iterable (e.g., set(list) or set(str)).

Parameters

iterable	Expression for the iterable
element	AST node for location info

Returns

Expression representing the set

handle_operations()

exprt python_set::handle_operations ( python_converter & converter, const std::string & op, exprt & lhs, exprt & rhs, const nlohmann::json & element )

static

Handle set operations (difference, intersection, union) Entry point for all set binary operations.

Parameters

converter	Reference to python_converter
op	Operation type ("Sub", "BitAnd", "BitOr")
lhs	Left operand
rhs	Right operand
element	JSON element with location info

Returns

Expression representing the result set, or nil_exprt if not a set operation

---

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

• src/python-frontend/set/python_set.h
• src/python-frontend/set/python_set.cpp