参照此示例(在此处找到:z3py),我可以将 c 与例如 Color.green 进行比较。
Color = Datatype('Color')
Color.declare('red')
Color.declare('green')
Color.declare('blue')
Color = Color.create()
# Let c be a constant of sort Color
c = Const('c', Color)
# Then, c must be red, green or blue
prove(Or(c == Color.green,
c == Color.blue,
c == Color.red))
在我的应用程序中,我需要将
c
与Python字符串进行比较:
我想要像这样的东西:c = Const('c', Color)
solve(c == "green") # this doesn't work, but it works with Color.green
这种方法适用于
IntSort
(见下文),但不适用于我的自定义数据类型。i = Int("i")
solve(i < 10)