|
@ -22,8 +22,8 @@ class TestSmtSolver(): |
|
|
manager = stormpy.ExpressionManager() |
|
|
manager = stormpy.ExpressionManager() |
|
|
x = manager.create_integer_variable("x") |
|
|
x = manager.create_integer_variable("x") |
|
|
xe = x.get_expression() |
|
|
xe = x.get_expression() |
|
|
c1 = stormpy.Expression.geq(xe, manager.create_integer(1)) |
|
|
|
|
|
c2 = stormpy.Expression.less(xe, manager.create_integer(0)) |
|
|
|
|
|
|
|
|
c1 = stormpy.Expression.Geq(xe, manager.create_integer(1)) |
|
|
|
|
|
c2 = stormpy.Expression.Less(xe, manager.create_integer(0)) |
|
|
solver = stormpy.utility.Z3SmtSolver(manager) |
|
|
solver = stormpy.utility.Z3SmtSolver(manager) |
|
|
solver.add(c1) |
|
|
solver.add(c1) |
|
|
solver.add(c2) |
|
|
solver.add(c2) |
|
@ -33,8 +33,8 @@ class TestSmtSolver(): |
|
|
manager = stormpy.ExpressionManager() |
|
|
manager = stormpy.ExpressionManager() |
|
|
x = manager.create_integer_variable("x") |
|
|
x = manager.create_integer_variable("x") |
|
|
xe = x.get_expression() |
|
|
xe = x.get_expression() |
|
|
c1 = stormpy.Expression.geq(xe, manager.create_integer(1)) |
|
|
|
|
|
c2 = stormpy.Expression.less(xe, manager.create_integer(0)) |
|
|
|
|
|
|
|
|
c1 = stormpy.Expression.Geq(xe, manager.create_integer(1)) |
|
|
|
|
|
c2 = stormpy.Expression.Less(xe, manager.create_integer(0)) |
|
|
solver = stormpy.utility.Z3SmtSolver(manager) |
|
|
solver = stormpy.utility.Z3SmtSolver(manager) |
|
|
solver.add(c1) |
|
|
solver.add(c1) |
|
|
solver.add(c2) |
|
|
solver.add(c2) |
|
@ -44,8 +44,8 @@ class TestSmtSolver(): |
|
|
manager = stormpy.ExpressionManager() |
|
|
manager = stormpy.ExpressionManager() |
|
|
x = manager.create_integer_variable("x") |
|
|
x = manager.create_integer_variable("x") |
|
|
xe = x.get_expression() |
|
|
xe = x.get_expression() |
|
|
c1 = stormpy.Expression.geq(xe, manager.create_integer(1)) |
|
|
|
|
|
c2 = stormpy.Expression.less(xe, manager.create_integer(2)) |
|
|
|
|
|
|
|
|
c1 = stormpy.Expression.Geq(xe, manager.create_integer(1)) |
|
|
|
|
|
c2 = stormpy.Expression.Less(xe, manager.create_integer(2)) |
|
|
solver = stormpy.utility.Z3SmtSolver(manager) |
|
|
solver = stormpy.utility.Z3SmtSolver(manager) |
|
|
solver.add(c1) |
|
|
solver.add(c1) |
|
|
solver.add(c2) |
|
|
solver.add(c2) |
|
|