SMT¶

SMT solver functions.

class hal_py.SMT.Constraint¶

Represents a constraint to the SMT query. A constraint is either an assignment of two Boolean functions or a single Boolean function, e.g., an equality check or similar.

__init__(*args, **kwargs)¶

Overloaded function.

__init__(self: hal_py.SMT.Constraint, constraint: hal_py.BooleanFunction) -> None

Constructs a new constraint from one Boolean function that evaluates to a single bit.

param hal_py.BooleanFunction constraint:

The constraint function.
__init__(self: hal_py.SMT.Constraint, lhs: hal_py.BooleanFunction, rhs: hal_py.BooleanFunction) -> None

Constructs a new equality constraint from two Boolean functions.

param hal_py.BooleanFunction lhs:

The left-hand side of the equality constraint.

param hal_py.BooleanFunction rhs:

The right-hand side of the equality constraint.

__module__ = 'hal_py.SMT'¶

constraint¶

A constraint that is either an assignment of two Boolean functions or a single Boolean function, e.g., an equality check or similar.

Type:	hal_py.BooleanFunction or tuple(hal_py.BooleanFunction, hal_py.BooleanFunction)

get_assignment(self: hal_py.SMT.Constraint) → Optional[Tuple[hal_py.BooleanFunction, hal_py.BooleanFunction]]¶

Returns the assignment constraint as a pair of Boolean functions.

Returns:	The assignment constraint on success, None otherwise.
Return type:	tuple(hal_py.BooleanFunction,hal_py.BooleanFunction) or None

get_function(self: hal_py.SMT.Constraint) → Optional[hal_py.BooleanFunction]¶

Returns the function constraint as a Boolean function.

Returns:	The function constraint on success, None otherwise.
Return type:	hal_py.BooleanFunction or None

is_assignment(self: hal_py.SMT.Constraint) → bool¶

Checks whether the constraint is an assignment constraint.

Returns:	True of the constraint is an assignment, False otherwise.
Return type:	bool

class hal_py.SMT.Model¶

Represents a list of assignments for variable nodes that yield a satisfiable assignment for a given list of constraints.

__eq__(self: hal_py.SMT.Model, arg0: hal_py.SMT.Model) → bool¶

Checks whether two SMT models are equal.

Returns:	True if both models are equal, False otherwise.
Return type:	bool

__hash__ = None¶

__init__(self: hal_py.SMT.Model, model: Dict[str, Tuple[int, int]] = {}) → None¶

Constructs a new model from a map of variable names to value and bit-size.

Parameters:	model (dict[str,tuple(int,int)]) – A dict from variable name to value and bit-size.

__module__ = 'hal_py.SMT'¶

__ne__(self: hal_py.SMT.Model, arg0: hal_py.SMT.Model) → bool¶

Checks whether two SMT models are unequal.

Returns:	True if both models are unequal, False otherwise.
Return type:	bool

evaluate(self: hal_py.SMT.Model, bf: hal_py.BooleanFunction) → Optional[hal_py.BooleanFunction]¶

Evaluates the given Boolean function by replacing all variables contained in the model with their corresponding value and simplifying the result.

Parameters:	bf (hal_py.BooleanFunction) – The Boolean function to evaluate.
Returns:	The evaluated function on success, None otherwise.
Return type:	hal_py.BooleanFunction or None

model¶

A dict from variable identifiers to a (1) value and (2) its bit-size.

Type:	dict(str,tuple(int,int))

static parse(model_str: str, solver: hal_py.SMT.SolverType) → Optional[hal_py.SMT.Model]¶

Parses an SMT-Lib model from a string output by a solver of the given type.

Parameters:	model_str (str) – The SMT-Lib model string. solver (hal_py.SMT.SolverType) – The solver that computed the model.
Returns:	The model on success, None otherwise.
Return type:	hal_py.SMT.Model or None

class hal_py.SMT.QueryConfig¶

Represents the data structure to configure an SMT query.

__init__(self: hal_py.SMT.QueryConfig) → None¶: Constructs a new query configuration.

__module__ = 'hal_py.SMT'¶

generate_model¶

Controls whether the SMT solver should generate a model in case formula is satisfiable.

Type:	bool

local¶

Controls whether the SMT query is performed on a local or a remote machine.

Type:	bool

solver¶

The SMT solver identifier.

Type:	hal_py.SMT.SolverType

timeout_in_seconds¶

The timeout after which the SMT solver is killed in seconds.

Type:	int

with_call(self: hal_py.SMT.QueryConfig, call: hal::SMT::SolverCall) → hal_py.SMT.QueryConfig¶

Sets the call type to the desired target.

Parameters:	call (hal_py.SMT.CallTyepe) – The solver type identifier.
Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

with_local_solver(self: hal_py.SMT.QueryConfig) → hal_py.SMT.QueryConfig¶

Activates local SMT solver execution.

Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

with_model_generation(self: hal_py.SMT.QueryConfig) → hal_py.SMT.QueryConfig¶

Indicates that the SMT solver should generate a model in case the formula is satisfiable.

Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

with_remote_solver(self: hal_py.SMT.QueryConfig) → hal_py.SMT.QueryConfig¶

Activates remote SMT solver execution.

Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

with_solver(self: hal_py.SMT.QueryConfig, solver: hal_py.SMT.SolverType) → hal_py.SMT.QueryConfig¶

Sets the solver type to the desired SMT solver.

Parameters:	solver (hal_py.SMT.SolverType) – The solver type identifier.
Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

with_timeout(self: hal_py.SMT.QueryConfig, seconds: int) → hal_py.SMT.QueryConfig¶

Sets a timeout in seconds that terminates an SMT query after the specified time has passed.

Parameters:	seconds (int) – The timeout in seconds.
Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

without_model_generation(self: hal_py.SMT.QueryConfig) → hal_py.SMT.QueryConfig¶

Indicates that the SMT solver should not generate a model.

Returns:	The updated SMT query configuration.
Return type:	hal_py.SMT.QueryConfig

class hal_py.SMT.Solver¶

Provides an interface to query SMT solvers for a list of constraints, i.e. statements that have to be equal. To this end, we translate constraints to a SMT-LIB v2 string representation and query solvers with a defined configuration, i.e., chosen solver, model generation etc.

__init__(self: hal_py.SMT.Solver, constraints: List[hal_py.SMT.Constraint] = []) → None¶

Constructs an solver with an optional list of constraints.

Parameters:	constraints (list[hal_py.SMT.Constraint]) – The (optional) list of constraints.

__module__ = 'hal_py.SMT'¶

constraints¶

The list of constraints.

Type:	list[hal_py.SMT.Constraint]

get_constraints(self: hal_py.SMT.Solver) → List[hal_py.SMT.Constraint]¶

Returns the list of constraints.

Returns:	The list of constraints.
Return type:	list[hal_py.SMT.Constraint]

static has_local_solver_for(type: hal_py.SMT.SolverType, call: hal::SMT::SolverCall) → bool¶

Checks whether a SMT solver of the given type is available on the local machine.

Parameters:	type (hal_py.SMT.SolverType) – The SMT solver type. call (hal_py.SMT.SolverCall) – The call to the SMT solver.
Returns:	True if an SMT solver of the requested type is available, False otherwise.
Return type:	bool

query(self: hal_py.SMT.Solver, config: hal_py.SMT.QueryConfig = <hal_py.SMT.QueryConfig object at 0x7fdb82ac2930>) → Optional[hal_py.SMT.SolverResult]¶

Queries an SMT solver with the specified query configuration.

Parameters:	config (hal_py.SMT.QueryConfig) – The SMT solver query configuration.
Returns:	The result on success, a string error message otherwise.
Return type:	hal_py.SMT.Result or str

query_local(self: hal_py.SMT.Solver, config: hal_py.SMT.QueryConfig) → hal::Result<hal::SMT::SolverResult>¶

Queries a local SMT solver with the specified query configuration.

Parameters:	config (hal_py.SMT.QueryConfig) – The SMT solver query configuration.
Returns:	The result on success, a string error message otherwise.
Return type:	hal_py.SMT.Result or str

query_remote(self: hal_py.SMT.Solver, config: hal_py.SMT.QueryConfig) → hal::Result<hal::SMT::SolverResult>¶

Queries a remote SMT solver with the specified query configuration.

WARNING: This function is not yet implemented.

Parameters:	config (hal_py.SMT.QueryConfig) – The SMT solver query configuration.
Returns:	The result on success, a string error message otherwise.
Return type:	hal_py.SMT.Result or str

with_constraint(self: hal_py.SMT.Solver, constraint: hal_py.SMT.Constraint) → hal_py.SMT.Solver¶

Adds a constraint to the SMT solver.

Parameters:	constraint (hal_py.SMT.Constraint) – The constraint.
Returns:	The updated SMT solver.
Return type:	hal_py.SMT.Solver

with_constraints(self: hal_py.SMT.Solver, constraints: List[hal_py.SMT.Constraint]) → hal_py.SMT.Solver¶

Adds a list of constraints to the SMT solver.

Parameters:	constraints (list[hal_py.SMT.Constraint]) – The constraints.
Returns:	The updated SMT solver.
Return type:	hal_py.SMT.Solver

class hal_py.SMT.SolverResult¶

Represents the result of an SMT query.

static Sat(model: Optional[hal_py.SMT.Model] = None) → hal_py.SMT.SolverResult¶

Creates a satisfiable result with an optional model.

Parameters:	model (hal_py.SMT.Model) – Optional model for satisfiable formula.
Returns:	The result.
Return type:	hal_py.SMT.SolverResult

static UnSat() → hal_py.SMT.SolverResult¶

Creates an unsatisfiable result.

Returns:	The result.
Return type:	hal_py.SMT.SolverResult

static Unknown() → hal_py.SMT.SolverResult¶

Creates an unknown result.

Returns:	The result.
Return type:	hal_py.SMT.SolverResult

__init__¶: Initialize self. See help(type(self)) for accurate signature.

__module__ = 'hal_py.SMT'¶

is(self: hal_py.SMT.SolverResult, type: hal_py.SMT.SolverResultType) → bool¶

Checks whether the result is of a specific type.

Parameters:	type (hal_py.SMT.ResultType) – The type to check.
Returns:	True in case result matches the given type, False otherwise.
Return type:	bool

is_sat(self: hal_py.SMT.SolverResult) → bool¶

Checks whether the result is satisfiable.

Returns:	True in case result is satisfiable, False otherwise.
Return type:	bool

is_unknown(self: hal_py.SMT.SolverResult) → bool¶

Checks whether the result is unknown.

Returns:	True in case result is unknown, False otherwise.
Return type:	bool

is_unsat(self: hal_py.SMT.SolverResult) → bool¶

Checks whether the result is unsatisfiable.

Returns:	True in case result is unsatisfiable, False otherwise.
Return type:	bool

model¶

The (optional) model that is only available if type == SMT.ResultType.Sat and model generation is enabled.

Type:	hal_py.SMT.Model

type¶

Result type of the SMT query.

Type:	hal_py.SMT.ResultType

class hal_py.SMT.SolverResultType¶

Result type of an SMT solver query.

Members:

Sat : The list of constraints is satisfiable.

UnSat : The list of constraints is not satisfiable.

Unknown : A result could not be obtained, e.g., due to a time-out.

Sat = <SolverResultType.Sat: 0>¶

UnSat = <SolverResultType.UnSat: 1>¶

Unknown = <SolverResultType.Unknown: 2>¶

__eq__(self: object, other: object) → bool¶

__getstate__(self: object) → int¶

__hash__(self: object) → int¶

__index__(self: hal_py.SMT.SolverResultType) → int¶

__init__(self: hal_py.SMT.SolverResultType, value: int) → None¶

__int__(self: hal_py.SMT.SolverResultType) → int¶

__members__ = {'Sat': <SolverResultType.Sat: 0>, 'UnSat': <SolverResultType.UnSat: 1>, 'Unknown': <SolverResultType.Unknown: 2>}¶

__module__ = 'hal_py.SMT'¶

__ne__(self: object, other: object) → bool¶

__repr__(self: object) → str¶

__setstate__(self: hal_py.SMT.SolverResultType, state: int) → None¶

__str__()¶: name(self: handle) -> str

name¶

value¶

class hal_py.SMT.SolverType¶

Identifier for the SMT solver type.

Members:

Z3 : Z3 SMT solver.

Boolector : Boolector SMT solver.

Unknown : Unknown (unsupported) SMT solver.

Boolector = <SolverType.Boolector: 1>¶

Unknown = <SolverType.Unknown: 3>¶

Z3 = <SolverType.Z3: 0>¶

__eq__(self: object, other: object) → bool¶

__getstate__(self: object) → int¶

__hash__(self: object) → int¶

__index__(self: hal_py.SMT.SolverType) → int¶

__init__(self: hal_py.SMT.SolverType, value: int) → None¶

__int__(self: hal_py.SMT.SolverType) → int¶

__members__ = {'Boolector': <SolverType.Boolector: 1>, 'Unknown': <SolverType.Unknown: 3>, 'Z3': <SolverType.Z3: 0>}¶

__module__ = 'hal_py.SMT'¶

__ne__(self: object, other: object) → bool¶

__repr__(self: object) → str¶

__setstate__(self: hal_py.SMT.SolverType, state: int) → None¶

__str__()¶: name(self: handle) -> str

name¶

value¶

class hal_py.SMT.SymbolicExecution¶

Represents the symbolic execution engine that handles the evaluation and simplification of Boolean function abstract syntax trees.

__init__(self: hal_py.SMT.SymbolicExecution, variables: List[hal_py.BooleanFunction] = []) → None¶

Creates a symbolic execution engine and (optionally) initializes the variables.

Parameters:	variables (list[hal_py.BooleanFunction]) – The (optional) list of variables.

__module__ = 'hal_py.SMT'¶

evaluate(*args, **kwargs)¶

Overloaded function.

evaluate(self: hal_py.SMT.SymbolicExecution, function: hal_py.BooleanFunction) -> hal::Result<hal::BooleanFunction>

Evaluates a Boolean function within the symbolic state of the symbolic execution.

param hal_py.BooleanFunction function:

The Boolean function to evaluate.

returns: The evaluated Boolean function on success, a string error message otherwise.

rtype: hal_py.BooleanFunction or str

evaluate(self: hal_py.SMT.SymbolicExecution, constraint: hal_py.SMT.Constraint) -> hal::Result<std::monostate>

Evaluates an equality constraint and applies it to the symbolic state of the symbolic execution.

param hal_py.SMT.Constraint constraint:

The equality constraint to evaluate.

returns: None on success, a string error message otherwise.

rtype: None or str

state¶

The current symbolic state.

Type:	hal_py.SMT.SymbolicState

class hal_py.SMT.SymbolicState¶

Represents the data structure that keeps track of symbolic variable values (e.g., required for symbolic simplification).

__init__(self: hal_py.SMT.SymbolicState, variables: List[hal_py.BooleanFunction] = []) → None¶

Constructs a symbolic state and (optionally) initializes the variables.

Parameters:	variables (list[hal_py.BooleanFunction]) – The (optional) list of variables.

__module__ = 'hal_py.SMT'¶

get(self: hal_py.SMT.SymbolicState, key: hal_py.BooleanFunction) → hal_py.BooleanFunction¶

Looks up the Boolean function equivalent in the symbolic state.

Parameters:	key (hal_py.BooleanFunction) – The Boolean function to look up.
Returns:	The Boolean function equivalent from the symbolic state or the key itself if it is not contained in the symbolic state.
Return type:	hal_py.BooleanFunction

set(self: hal_py.SMT.SymbolicState, key: hal_py.BooleanFunction, value: hal_py.BooleanFunction) → None¶

Sets a Boolean function equivalent in the symbolic state.

Parameters:	key (hal_py.BooleanFunction) – The Boolean function. value (hal_py.BooleanFunction) – The equivalent Boolean function.