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將數據類型/枚舉與字符串進行比較

回答

相關問題