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

一个对我有效的解决方案(将数据类型/枚举与字符串进行比较)是添加一个 cast 例行程序 class DatatypeSortRef(SortRef) 在里面 z3.py 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)

注意:我没有注意一般的正确性。这种方法适用于

Z3 python接口对字符串执行非常有限的重载。可以对类型“string”使用字符串文字。否则字符串不会被强制为其他类型。此外,使用字符串的方法也不适用于整数,例如。,

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

将抛出错误。

red = Color.red