Z3SmtSolver

Warning

The stormpy developer API is internal and can be subject to change.

class Z3SmtSolver(

self: stormpy.developer._core.Z3SmtSolver,

manager: stormpy.expressions.ExpressionManager,

)

Bases: SmtSolver

z3 API for storm smtsolver wrapper

add(

self: stormpy.developer._core.SmtSolver,

assertion: stormpy.expressions.Expression,

) → None

Add constraint

check(self: stormpy.developer._core.SmtSolver) → stormpy.developer._core.SmtCheckResult

Check

get_model(

self: stormpy.developer._core.SmtSolver,

) → stormpy.developer._core.ModelReference

Get the model

pop(

self: stormpy.developer._core.SmtSolver,

n: SupportsInt | SupportsIndex,

) → None

Pop

push(self: stormpy.developer._core.SmtSolver) → None

Push

reset(self: stormpy.developer._core.SmtSolver) → None

Reset