The crosshair Package

crosshair.register_type(typ: Type, creator: Callable[[SymbolicFactory], object] | Callable[[SymbolicFactory, Type], object] | Callable[[SymbolicFactory, Type, Type], object] | Callable[[SymbolicFactory, Type, Type, Type], object] | Callable[[SymbolicFactory, Type, Type, Type, Type], object]) → None[source]

Register a custom creation function to create symbolic values for a type.

Parameters:

typ – The Python type (or typing annotation) to handle.
creator – A function that takes a SymbolicFactory instance and returns a symbolic value. When creating a parameterized type (e.g. List[int]), type parameters will be given to creator as additional arguments following the factory.

class crosshair.SymbolicFactory(space: StateSpace, pytype: object, varname: str)[source]

A callable object that creates symbolic values.

__call__(typ: Callable[[...], _T], suffix: str = '', allow_subtypes: bool = True) → _T[source]

__call__(typ: Any, suffix: str = '', allow_subtypes: bool = True) → Any

Create a new symbolic value.

Parameters:

typ (type) – The corresponding Python type for the returned symbolic.
suffix (str) – A descriptive suffix used to name variable(s) in the solver.
allow_subtypes (bool) – Whether it’s ok to return a subtype of given type.

Returns:

A new symbolic value.

class crosshair.StateSpace(execution_deadline: float, model_check_timeout: float, search_root: RootNode)[source]

Holds various information about the SMT solver’s current state.

Methods:

`add`(expr)
`is_possible`(expr)