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.

__annotations__ = {}

__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'

property 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.

__annotations__ = {}

__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

property 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.

__annotations__ = {}

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

__module__ = 'hal_py.SMT'

property generate_model

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

Type: bool

property local

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

Type: bool

property solver

The SMT solver identifier.

Type: hal_py.SMT.SolverType

property 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.

__annotations__ = {}

__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'

property 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 0x7f53981483b0>) → 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) → Optional[hal_py.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

static query_local_with_smt2(config: hal_py.SMT.QueryConfig, smt2: str) → Optional[hal_py.SMT.SolverResult]

Queries a local SMT solver with the specified query configuration and the smt2 formatted query.

Parameters

config (hal_py.SMT.QueryConfig) – The SMT solver query configuration.
smt2 (string) – A solver query formatted in smt2 style.

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

__annotations__ = {}

__init__(*args, **kwargs)

__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

property model

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

Type: hal_py.SMT.Model

property 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>

__annotations__ = {}

__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

property name

property 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>

__annotations__ = {}

__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

property name

property value

class hal_py.SMT.SymbolicExecution

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

__annotations__ = {}

__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

property 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).

__annotations__ = {}

__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.