z3pyデータ型/列挙型を文字列と比較する

Question

この例の後に（ここでは：z3py）、私はcを次のように比較できます。 Color.green。

私のpython-文字列に cを比較する必要が自分のアプリケーションで

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 = Const('c', Color) 
solve(c == "green") # this doesn't work, but it works with Color.green 

： 私はこのような何かをしたいと思いますIntSort（下記参照）では、私自身のデータ型ではありません。

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

Answer 1

一つの解決策は、z3.pyにclass DatatypeSortRef(SortRef)にcastルーチンを追加しました。

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) 

注： それがそうでなければ、既存の行動を続け、与えられた文字列と一致し、それを使用するコンストラクタを見つけようとします（super().cast(val)）

は、ここで私が使用したコードだ私は注意を払っていません一般的な正しさこの方法は私ので動作しますが、コードに問題が生じる可能性があります。

Answer 2

Z3 pythonインターフェイスは、文字列のオーバーロードが非常に制限されています。 'String'型の文字列リテラルを使用できます。さもなければ、文字列は他の型に強制されません。さらに、文字列を使用するアプローチも整数に対しては機能しません。たとえば、

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

はエラーをスローします。すでにColor.redを使用するか、または独自の速記宣言することができ

注：（文字列へのデータ型/列挙型を比較す​​る）私のために働いた

red = Color.red