z3py将数据类型/枚举与字符串进行比较

在此示例中（在此处找到：z3py），我可以将c与例如Color.green。z3py将数据类型/枚举与字符串进行比较

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)

来源

2017-08-15 stklik

一个解决方案为我工作（比较数据类型/枚举为字符串）是一个cast例程z3.py添加到class DatatypeSortRef(SortRef) 。它会尝试查找指定的字符串相匹配，并使用它构造，否则继续使用现有的行为（super().cast(val)）

下面是我使用的代码：

def cast(self, val): 
    """This is so we can cast a string to a Z3 DatatypeRef. This is useful if we want to compare strings with a Datatype/Enum to a String. 

    >>> Color = Datatype("Color") 
    >>> Color.declare("red") 
    >>> Color.declare("green") 
    >>> Color.declare("blue") 
    >>> Color = Color.create() 

    >>> x = Const("x", Color) 
    >>> solve(x != "red", x != "blue") 
    [x = green] 
    """ 
    if type(val) == str: 
     for i in range(self.num_constructors()): 
      if self.constructor(i).name() == val: 
       return self.constructor(i)() 
    return super().cast(val)

注：我没注意以一般的正确性。此方法适用于我，但可能会导致您的代码出现问题。

来源

2017-08-16 14:07:59 stklik

Z3 python接口对字符串的重载非常有限。您可以使用字符串文字作为'String'类型。否则，字符串不会被强制转换为其他类型。此外，使用字符串的方法也不适用于整数，例如，

I = Int("I") 
solve(I < "10")

将引发错误。

注意，您可以使用Color.red已经或宣布自己的速记：

red = Color.red

来源

2017-08-15 14:35:22

我想过创建名称到值的全局映射（类似于你的“简写”），但我希望有一种“官方”方式。你认为有可能通过合理的努力来实现这样的事情吗？ – stklik

请参阅下面的我的（潜在）解决方案。我没有发现任何python测试运行，所以我不想创建拉请求。 @尼古拉 - Bjorner – stklik

z3py将数据类型/枚举与字符串进行比较

回答

相关问题