funman.utils package

Submodules

funman.utils.handlers module

Inheritance diagram of funman.utils.handlers

The handlers module includes several search handlers that deal with search episode data, such as plotting and writing results to a file.

class funman.utils.handlers.NoopResultHandler

Bases: ResultHandler

The NoopResultHandler is used in the absence of other handlers and performs no (i.e., noop) handling.

close() → None

Listener interface for ending handling.

open() → None

Listener interface for starting handling.

process(result: dict) → None

Listener interface for processing data in result.

Parameters:

result (dict) – data to process

class funman.utils.handlers.ResultCombinedHandler(handlers: List[ResultHandler])

Bases: ResultHandler

The ResultCombinedHandler combines multiple sub-handlers by iteratively invoking the sub-handler listener interfaces.

close() → None

Listener interface for ending handling.

open() → None

Listener interface for starting handling.

process(result: dict) → None

Listener interface for processing data in result.

Parameters:

result (dict) – data to process

class funman.utils.handlers.ResultHandler

Bases: ABC

The ResultHandler abstract class handles data produced by search processes.

abstract close() → None

Listener interface for ending handling.

abstract open() → None

Listener interface for starting handling.

abstract process(result: dict) → None

Listener interface for processing data in result.

Parameters:

result (dict) – data to process

class funman.utils.handlers.WaitAction

Bases: ABC

The WaitAction abstract class allows search processes to handle waiting for additional work.

abstract run() → None

funman.utils.logging module

funman.utils.logging.add_handler()
funman.utils.logging.add_log_level(levelName: str, levelNum: int)
funman.utils.logging.inherit_level(subLogger: Logger)
funman.utils.logging.set_level(level: int)
funman.utils.logging.setup_logging()

funman.utils.math_utils module

funman.utils.math_utils.div(numer: float, denom: float) → float
funman.utils.math_utils.gt(lhs, rhs)
funman.utils.math_utils.gte(lhs, rhs)
funman.utils.math_utils.lt(lhs, rhs)
funman.utils.math_utils.lte(lhs, rhs)
funman.utils.math_utils.minus(lhs, rhs)
funman.utils.math_utils.plus(numer, denom)

funman.utils.smtlib_utils module

Inheritance diagram of funman.utils.smtlib_utils

class funman.utils.smtlib_utils.FUNMANSmtDagPrinter(stream, template='.def_%d', annotations=None)

Bases: SmtDagPrinter

walk_real_constant(formula, *args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

class funman.utils.smtlib_utils.FUNMANSmtLibScript

Bases: SmtLibScript

serialize(outstream, daggify=True)

Serializes the SmtLibScript expanding commands

class funman.utils.smtlib_utils.FUNMANSmtPrinter(stream, annotations=None)

Bases: SmtPrinter

walk_real_constant(formula, *args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

funman.utils.smtlib_utils.model_to_dict(self)
funman.utils.smtlib_utils.smtlibscript_from_formula(formula, logic=None)
funman.utils.smtlib_utils.smtlibscript_from_formula_list(formulas, logic=None)

funman.utils.sympy_utils module

Inheritance diagram of funman.utils.sympy_utils

class funman.utils.sympy_utils.FUNMANFormulaManager(formula_manager, env=None)

Bases: FormulaManager

FormulaManager is responsible for the creation of all formulae.

Pow(base, exponent)

Creates the n-th power of the base.

The exponent must be a constant.

pydantic model funman.utils.sympy_utils.SympyBoundedSubstituter

Bases: BaseModel

Show JSON schema
{
   "title": "SympyBoundedSubstituter",
   "type": "object",
   "properties": {
      "bound_symbols": {
         "default": null,
         "title": "Bound Symbols"
      },
      "str_to_symbol": {
         "default": null,
         "title": "Str To Symbol"
      }
   }
}

Config:

  • arbitrary_types_allowed: bool = True

Fields:
field bound_symbols: Dict[Symbol, Dict[str, Symbol]] = {}
field str_to_symbol: Dict[str, Symbol] = {}
maximize(derivative_variables: List[str], expr: Expr) → str
minimize(derivative_variables: List[str], expr: Expr) → str
class funman.utils.sympy_utils.SympySerializer

Bases: IdentityDagWalker

to_sympy(f: FNode) → Expr
walk_div(formula, args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_minus(formula, args, **kwargs) → Expr

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_plus(formula, args, **kwargs) → Expr

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_pow(formula, args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_real_constant(formula, args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_symbol(formula, args, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_times(formula, args, **kwargs) → Expr

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

funman.utils.sympy_utils.has_reserved(str_expr, rw)
funman.utils.sympy_utils.rate_expr_to_pysmt(expr: str | Expr, state=None)
funman.utils.sympy_utils.replace_reserved(str_expr)
funman.utils.sympy_utils.series_approx(expr: Expr, vars: List[Symbol] = [], order=4) → Expr
funman.utils.sympy_utils.substitute(str_expr: str, values: Dict[str, float | str])
funman.utils.sympy_utils.sympy_subs(expr: Expr, substitution: Dict[str, float | str]) → Expr
funman.utils.sympy_utils.sympy_to_pysmt(expr)
funman.utils.sympy_utils.sympy_to_pysmt_abs(expr)
funman.utils.sympy_utils.sympy_to_pysmt_op(op, expr, explode=False)
funman.utils.sympy_utils.sympy_to_pysmt_piecewise(expr)
funman.utils.sympy_utils.sympy_to_pysmt_pow(expr)
funman.utils.sympy_utils.sympy_to_pysmt_real(expr, numerator_digits=6)
funman.utils.sympy_utils.sympy_to_pysmt_symbol(op, expr, op_type=None)
funman.utils.sympy_utils.to_sympy(formula: FNode | str, str_symbols: List[str]) → Expr

Module contents