utils package

Submodules

utils.auxiliary_operator module

Auxiliary Operator

This module provides functionality for constructing symbols and conditions, including: 1. Symbol wrapper (CustomSym) 2. Condition wrapper (CustomCond) 3. Utility functions for generating random indices, evaluating conditions, and managing symbol metadata.

class utils.auxiliary_operator.CustomCond(domain: int = 0, desc: str = '', data: list = None)

Bases: str

Condition wrapper class for structured condition modeling

Extends metadata support based on the standard string class to achieve: - Binding of conditional expressions to descriptive text - Domain identification classification - Additional data payload

domain

Number of expressions

Type:

int

data

Additional data payload

Type:

list

Inherits:

All native functionalities and methods of str

Example

>>> cond = CustomCond(domain=1, desc="Score should be greater than 60", data=[[...], [...]])
>>> print(cond)  # "Score should be greater than 60"
>>> cond.domain  # 1

property desc

Natural langauge description

Type:

str

class utils.auxiliary_operator.CustomSym(name: str, source: Dict[str, List[str | int]], attr: List[str] | None = None, type: str | List[str] = 'Int', desc: str | List[str] | None = None)

Bases: dict

Symbol wrapper class supporting structured symbol modeling and Z3 variable integration

name

Symbol group name, used as symbol prefix

Type:

str

source

Data source

• Example: {“Grade”: [1,2,3], “Subject”: [“Math”, “Chinese”]}

Type:

Dict[str, List[Union[str, int]]]

attr

Attributes

• Example: [“Score”, “Difficulty”]

Type:

Optional[List[str]]

type

Variable type definition, supports:

• ‘Int’ (default)/’Bool’/’Real’/’Float’/’BitVec’

• Type list (needs equal length when attr exists)

Type:

Union[str, List[str]]

desc

Description template system

• Single attribute mode: “Grade variable description”

• Multi-attribute mode: [“Score description”, “Difficulty description”]

Type:

Optional[Union[str, List[str]]]

Examples

>>> grade_system = CustomSym(
...     name="Grade",
...     source={"Level": ["A", "B"]},
...     attr=["Score"],
...     type="Int"
... )
>>> grade_system[("A")]["Score"]  # Returns Int('Grade_A_Score')

get(attr: str) → List[Any]

Batch retrieve all variable instances of the specified attribute.

Parameters:

attr – Target attribute name

Returns:

A list of attribute variables/instances arranged in the order of initialization.

Raises:

ValueError – When attr does not exist or is currently in single-attribute mode.

to_list() → List[Any] | List[List[Any]]

Output a list of Z3 symbols.

Returns

• Single attribute: [Var1, Var2, …]

• Multiple attributes: [[Attribute1 variable list], [Attribute2 variable list], …]

Example

>>> # Example of multiple attributes and multiple dimensions
... [
...     [Grade_A_Math_Score, Grade_A_Chinese_Score, ...],  # Score attribute
...     [Grade_A_Math_Diff, Grade_A_Chinese_Diff, ...]    # Difficulty attribute
... ]

class utils.auxiliary_operator.SafeTemplate(template)

Bases: object

render(context)

utils.auxiliary_operator.choose(candidates, group_size, group_num)

Select group_num tuples of length group_size from a set of symbols/events (candidates).

utils.auxiliary_operator.generate_letters(n, lang='en')

Generate a set of letter identifiers.

Parameters:

• n (int) – The number of identifiers to generate.

• lang (str) – Language option, ‘en’ for English (default), other values for Chinese.

Returns:

In English mode, returns a list formatted like [‘A1’, ‘A2’, …]. str: In Chinese mode, returns a string containing the specified number of characters.

Return type:

list

Description:

• English mode: Uses a looped sequence of letters A-Z combined with numbers (resets letters every 26 iterations).

• Chinese mode: Uses a fixed alphabet “甲乙丙丁…” to return the first n characters.

utils.auxiliary_operator.generate_random_indices(choose, amount, domain, domain_cond=True, dim=1, dim_cond=[], custom_cond=[], order=[], duplicate=[], env={})

Generate random index combinations.

Parameters:

• choose (List[any]) – Number of available elements in each data source, similar to DerivedSymbol.source.

• amount (List[int]) – Number of elements to choose in each data source, similar to DerivedSymbol.amount. Example: [“2”, “1”] indicates selecting 2 from the first data source and 1 from the second source.

• domain (int) – Total number of groups to select, similar to DerivedSymbol.domain.

• domain_cond (bool) – Same as DerivedSymbol.domain_cond, default True.

• dim (int) – Number of dimensions in each symbol, similar to DerivedSymbol.dim.

• dim_cond (List[List[int]]) – Same as DerivedSymbol.dim_cond.

• custom_cond (List[Dict]) – List of custom constraints, each dictionary contains: (Same as DerivedSymbol.custom_cond) - scope: Level of application (‘dim’/’domain’). - fields: List of indices of the involved data sources. - constraint: Logical expression for constraints (callable object).

• order (List[bool]) – Configuration of arrangement for each dimension. Same as DerivedSymbol.order. - True: Arrangement (considering order). - False: Combination (not considering order).

• duplicate (List[bool]) – Initialization repetition rules. Same as DerivedSymbol.duplicate. - True: Allow repeated selections. - False: Prohibit repetition.

• env (Dict) – Importing the environment variables from code generated by the translator. Used for evaluating some conditional expressions in custom_cond.

Returns:

(Selected indices, Formatted selected indices)

• Example: ([[[1, 2], [3]], [[4, 5], [6]]], [“__1__, __2__”, “__3__”])

• Note: The formatted indices are for configuration purposes, not for direct use in the program. In config files, strings that start and end with “__” are considered as indices rather than values.

Return type:

tuple

Raises:

• AssertionError – Raised when parameter lengths do not match.

• Exception – Raised when unable to generate valid combinations.

Implementation Process:

1. Parameter validation and initialization.

2. Generate a base pool of combinations based on the provided choose and amount.

3. Handling custom conditions.

utils.auxiliary_operator.generate_random_list(size, ele_type, ele_domain, cond=[], per_ele_domain=None)

Return a random array with element-level range control.

Parameters:

• size (int) – Length of the array.

• ele_type (str) – Type of elements in the array, such as ‘int’, ‘bool’, ‘enum’, ‘float’.

• ele_domain (list or tuple) – Global value range for elements (used when element-level range is not defined).

• cond (list) – List of conditions that elements must satisfy, each as a function string, e.g., “lambda l: sum(l) == 5”.

• per_ele_domain (list, optional) – Independent value range for each element, must have the same length as size. Can be None or contain None values, indicating that the element should use the global value range.

utils.auxiliary_operator.generate_random_list_with_total(size, ele_domain, total, per_ele_domain=None)

Return a random integer array with a total sum of total, supporting element-level range control.

Parameters:

• size (int) – Length of the array.

• ele_domain (list or tuple) – Global value range for elements (two integers: [min, max]).

• total (int) – The total sum of all elements in the array.

• per_ele_domain (list, optional) – Independent value range for each element, must have the same length as size. Can be None or contain None values, indicating that the element should use the global value range.

utils.auxiliary_operator.generate_var_names(n)

Return an array of default variable names with a length of n.

• When n <= 3, the order is x, y, z.

• When 4 <= n <= 11, the order is p, q, r, … .

• When n > 11, the order is x1, x2, … .

utils.auxiliary_operator.get_data(cond)

Return the random data bound to the condition ‘sym’; if ‘sym’ is a list, do this for each element.

utils.auxiliary_operator.get_desc(sym)

Return the description of the symbol ‘sym’; if ‘sym’ is a list, do this for each element.

utils.auxiliary_operator.get_p(sym, p)

Return the value of the binded variable named ‘p’ for the symbol ‘sym’; if ‘sym’ is a list, do this for each element.

utils.auxiliary_operator.get_value(sol, vars)

Return the values of ‘vars’ in the solution ‘sol’ of the z3-solver.

utils.auxiliary_operator.get_var_name(z3_var)

Return the string representation of the variable name of the z3 variable.

utils.auxiliary_operator.is_option_valid(opt, formula, cond, result, env)

utils.auxiliary_operator.make_expr(op: str, *operands)

Construct a Z3 expression.

Parameters:

• op (str) –

  Operator identifier, supporting the following forms:

  • Comparison operators: “eq”/”==”, “neq”/”!=”, “gt”/”>”, “ge”/”>=”, “lt”/”<”, “le”/”<=”

  • Logical operators: “and”/”&&”, “or”/”||”, “not”/”!”, “implies”/”=>”

  • Arithmetic operators: “add”/”+”, “sub”/”-”, “mul”/”*”, “div”/”/”

• *operands (z3.ExprRef) –

  Z3 expression operands, the number determined by the operator:

  • Unary operators: 1 operand (e.g., not)

  • Binary operators: 2 operands (e.g., +, ==)

  • N-ary operators: Any number (e.g., and, or)

Returns:

The generated Z3 expression object.

Return type:

z3.ExprRef

Raises:

ValueError –

• When an unsupported operator is used. - When the number of operands does not meet the operator’s requirements.

Examples

>>> x, y = Ints('x y')
>>> make_expr(">=", x, 5)     # Creates x >= 5
>>> make_expr("&&", x > 0, y < 10)  # Creates And(x > 0, y < 10)

Notes

• Logical operators and/or support any number of operands.

• Arithmetic operator + actually calls the Sum function (e.g., a + b + c converts to Sum(a, b, c)).

utils.auxiliary_operator.set_global_context(ctx)

utils.auxiliary_operator.set_local_context(ctx)

utils.auxiliary_operator.sort_solutions(solutions, key_func=None)

Sort the list of solutions obtained from the Z3 solver.

Parameters:

• solutions (list) – The list of solutions to be sorted, where each element is a Z3 model.

• key_func (callable, optional) – A function to generate the sorting key, which takes a model and returns a sortable value. Defaults to a tuple of values sorted by variable names.

utils.auxiliary_operator.store_sym_config(key, value)

utils.auxiliary_operator.to_hashable(element)

Recursively convert nested structures to hashable types.

Parameters:

element (Any) – Input element, supports nested lists/tuples.

Returns:

Converts lists to tuples, preserving the nested structure.

Return type:

Hashable object

Examples

>>> to_hashable([1, [2, 3]])  # Returns (1, (2, 3))
>>> to_hashable({1, 2})       # Returns the original set (since sets are not hashable).

Notes

• Mainly used to use nested structures as dictionary keys or set elements.

• Only processes list types; other container types (e.g., dict) need to be handled separately.

utils.auxiliary_operator.to_unique(l)

Remove duplicates from a list (preserving order).

Parameters:

l (Union[list, Any]) – Input list or any type.

Returns:

A deduplicated list (maintaining the order of elements); returns the input directly if it’s not a list.

Examples

>>> to_unique([1, 2, 1, 3])  # Returns [1, 2, 3]
>>> to_unique("abcaba")      # Returns ["a", "b", "c"]

utils.condition_generator module

该模块用来生成不同模板问题的约束条件

utils.condition_generator.gen_event_count_condition(events, fact, num=0)

Return conditions where at most, least, or exactly num events are true in the event array.

Parameters:

• events – Array of type z3.Bool.

• fact – Objective fact about the events: “most” (at most), “least” (least), or “equal” (exactly).

• num – The quantity, which must be greater than 0 and less than or equal to the length of the event list.

utils.condition_generator.gen_multi_event_count_condition(events, op, target)

Generate conditions based on a multidimensional event array.

Parameters:

• events – Array of events, where each element is a symbol.

• op – Operator, such as wc (word count).

• target – The target value for the condition.

utils.faker_utils module

utils.faker_utils.get_faker(num, provider_name, locale='zh_CN', seed=None)

Generate a specified number of unique fake data entries using Faker.

Parameters:

• num – The number of data entries to generate.

• provider_name – Name of the provider (also the method name to call).

• providers – List of provider classes to add.

• locale – Locale setting (default is Chinese).

• seed – Random seed.

Returns:

A list of generated unique data.

Exceptions:

AttributeError: When the provider_name does not exist.

ValueError: When it is not possible to generate enough unique data.

utils.mathexpr_generator module

Mathematical Expression Generator

This module provides functionality for generating, manipulating, and evaluating mathematical expressions, including: 1. Expression tree nodes (Variable, Constant, Add, Subtract, Multiply, Divide, Power, Comparison) 2. Formula configuration and serialization/deserialization 3. Random expression generation with configurable complexity 4. Z3 integration for constraint solving 5. LaTeX output for mathematical notation

class utils.mathexpr_generator.Add(left, right)

Bases: ExprNode

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.Comparison(left, op, right)

Bases: ExprNode

OPS = {'<': (<function Comparison.<lambda>>, '<'), '<=': (<function Comparison.<lambda>>, '\\leq'), '==': (<function Comparison.<lambda>>, '='), '>': (<function Comparison.<lambda>>, '>'), '>=': (<function Comparison.<lambda>>, '\\geq')}

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.Constant(value)

Bases: ExprNode

evaluate(_)

serialize()

to_latex(_)

to_z3(_)

class utils.mathexpr_generator.Divide(num, den)

Bases: ExprNode

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.ExprNode

Bases: object

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.FormulaConfig(root, vars_num)

Bases: object

classmethod deserialize(s, vars_num)

get_latex(vars)

get_value(values)

get_z3_expr(z3_vars)

serialize()

class utils.mathexpr_generator.Multiply(left, right)

Bases: ExprNode

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.Power(var, exponent)

Bases: ExprNode

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.Subtract(left, right)

Bases: ExprNode

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

class utils.mathexpr_generator.Variable(index)

Bases: ExprNode

evaluate(values)

serialize()

to_latex(var_names)

to_z3(vars)

utils.mathexpr_generator.build_system(configs, vars, var_names=None)

Build equation system, generate Z3 expressions and LaTeX format strings.

Parameters:

• configs (list[str]) – List of serialized formula configurations

• vars (list) – Z3 variable list

• var_names (list[str], optional) – Variable name list, used for LaTeX output

Returns:

Dictionary containing the following keys:

• ’z3_expr’: List of Z3 expressions for all formulas

• ’z3_constraint’: List of all constraint conditions

• ’latex_str’: LaTeX format string representation of the system

Return type:

dict

Notes

1. When there’s only one formula, returns a single LaTeX expression

2. Multiple formulas are wrapped in cases environment

3. Automatically adds positive exponent constraints for power operations

utils.mathexpr_generator.generate_expr(vars_num, depth=0, max_depth=5, allow_const=True, force_var=False, parent_op=None, allow_power=True, max_const=10)

Generate expression tree.

Parameters:

• vars_num (int) – Number of variables, determines the variable index range (0 to vars_num-1)

• depth (int) – Current recursion depth, used to control expression complexity, default 0

• max_depth (int) – Maximum recursion depth, controls maximum expression complexity, default 5

• allow_const (bool) – Whether to allow generating constant terms, default True

• force_var (bool) – Whether to force generating variables (automatically effective when allow_const is False), default False

• parent_op (str) – Parent node operation type, used for special handling of certain operations, default None

• allow_power (bool) – Whether to allow generating power operations (x² or x³), default True

• max_const (int) – Maximum value for generated constants, default 10

Returns:

Generated expression tree object (can be Variable, Constant, Add, Subtract, Multiply or Power)

Return type:

Expression

Notes

1. When depth >= max_depth, will force generating leaf nodes (variables or constants)

2. Multiplication operations receive special handling to ensure no two constants are multiplied

3. Power operations only allow x² or x³ forms

4. Addition/subtraction prevents generating two constants being added/subtracted

utils.mathexpr_generator.generate_formula(vars_num, is_cond=False, allow_power=True, max_depth=5)

Generate a single mathematical formula expression.

Parameters:

• vars_num (int) – Number of variables, determines the variable index range (0 to vars_num-1)

• is_cond (bool) – Whether to generate comparison condition expressions (like x > 0), default False

• allow_power (bool) – Whether to allow generating power operations (x² or x³), default True

• max_depth (int) – Maximum depth of expression tree, controls expression complexity, default 5

Returns:

Serialized formula configuration string

Return type:

str

Notes

1. When is_cond is True, generates condition expressions compared with 0

2. Comparison operators are randomly chosen from [‘<=’, ‘>=’, ‘==’, ‘<’, ‘>’]

utils.mathexpr_generator.generate_formulas(formula_num, vars_num, is_cond=False, allow_power=True, max_depth=5)

Generate a specified number of valid formulas.

Parameters:

• formula_num (int) – Number of formulas to generate

• vars_num (int) – Number of variables

• is_cond (bool) – Whether to generate comparison expressions (like x > 0), default False

• allow_power (bool) – Whether to allow using power operations (x², x³ etc.), default True

• max_depth (int) – Maximum depth of expression tree, controls expression complexity, default 5

Returns:

List containing all valid formulas, each element is a serialized formula configuration string

Return type:

list[str]

Raises:

ValueError – Raised when unable to generate any valid formulas

Notes

1. Will attempt multiple times until generating enough valid formulas or reaching maximum attempts

2. Each generated formula undergoes validity verification

3. Ensures no duplicate formulas are generated

utils.mathexpr_generator.get_formula_value(config, values)

Calculate the value of a formula given variable values.

Parameters:

• config (str) – Serialized formula configuration

• values (list) – List of variable values, order corresponds to variable indices

Returns:

Formula calculation result

Return type:

float

Notes

1. Variable value list length must match the number of variables in the formula

2. Handles all supported operation types (addition, subtraction, multiplication, division, power operations, etc.)

utils.mathexpr_generator.to_value(s)

utils.option_generator module

This module provides functions to generate options based on Z3 solver models.

utils.option_generator.find_always_TF_combined_events(events, solutions, require=True, num=2)

Analyze which combinations of num events in solutions are always true or false.

Parameters:

• events – List[BoolRef], array of Z3 boolean variables (event array).

• solutions – List[Model], multiple feasible solutions (array of solver.model()).

• require – bool, whether the events should be true (True) or false (False).

• num – int, the number of event combinations. When num = 1, it degenerates into find_always_TF_events.

Returns:

List[Tuple[BoolRef]], list of combinations of num events that satisfy the condition.

utils.option_generator.find_always_TF_events(events, solutions, require=True)

Identify events (events) that are always True/False in all feasible solutions (solutions).

Parameters:

• events – Array of z3.Bool type.

• solutions – Array composed of multiple Solver.model() instances.

• require – Whether the events should be true (True) or false (False).

Returns:

List of events that are always True in all solutions, satisfied_res, and the results that do not meet the condition, unsatisfied_res.

utils.option_generator.find_required_event_groups(events, correct_num, incorrect_num, solutions, formula, cond='all', event_num=[2], order=None, duplicate=None, custom_cond=[], env={})

Find event_num events that satisfy the condition among all feasible solutions. By default, it identifies all pairs of events where at most one is true.

Parameters:

• events – Array of events, similar to DerivedSymbol.source in DSL.

• correct_num – Number of correct items.

• incorrect_num – Number of incorrect items.

• solutions – Array of feasible solutions (array of Z3 models).

• formula – Similar to formula in DSL.

• cond – Whether all solutions must satisfy (“all”) or if at least one satisfying solution is enough (“any”), similar to DerivedSymbol.cond in DSL.

• event_num – Array specifying the number of sub-events, similar to DerivedSymbol.amount in DSL.

• order – Similar to DerivedSymbol.order in DSL, default is all False.

• duplicate – Similar to duplicate in DSL, default is all False.

• custom_cond – Similar to custom_cond in DSL.

• env – Environment variables imported from the program generated by the translator.

Returns:

Returns a list of satisfied event pairs satisfied and their index list satisfied_indices, as well as the unsatisfied combinations unsatisfied and their index list unsatisfied_indices.

utils.option_generator.get_TF_events_for_each_solution(events, solutions, require=True)

Return the events that are true/false in each feasible solution from solutions.

Parameters:

• events – Array of z3.Bool type.

• solutions – Array composed of multiple Solver.model() instances.

• require – Whether the events should be true (True) or false (False).

utils.option_generator.get_required_non_solutions(solutions, conditions=[], num=5)

Find num infeasible solutions that satisfy the conditions (conditions) but are not in solutions, for use as incorrect options.

Parameters:

• solutions – Array composed of multiple Solver.model() instances.

• conditions – Conditions that the incorrect options need to satisfy.

• num – The number of groups of incorrect options to return.

Module contents