6

z3pyで不思議に思っているのですが、特定の定数式が変数または値であるかどうかを確認するにはどうすればよいですか? 例えば 

x = Int('x')
x_ = IntVal(7)
ColorVal, (White,Black)  = EnumSort("ColorVal",["While","Black"])
mycolor = Const("mycolor",ColorVal)

したがって、 x,mycolor はすべて変数になり、 x_,True,False,White,Black は変数ではなく値になります。

z3py には is_var 述語がありますが、目的が異なります。これは、数式内のすべての変数の名前を別の名前に変更したい場合に便利です。

4

2 に答える 2

7

変数と呼ばれるものは、（技術的には）Z3では未解釈の定数と呼ばれます。1値（ 、、など）はtrue、#x01解釈された定数と呼ばれます。したがって、原則として、aが「変数」であるかどうかをすばやく確認するには、次のコードを使用します。

is_const(a) and a.decl().kind() == Z3_OP_UNINTERPRETED

このコードは、データ型以外のすべてに対して機能します。Z3_OP_UNINTERPRETEDあなたの例を試した後、私はZ3がデータ型コンストラクターに対して誤って返されていることに気づきました。Z34.2で修正しました。それまでの間、関数が定数コンストラクターをis_datatype_const_value(a)返す場合Trueは、次の回避策を使用できます。a

def is_datatype_sort(s):
  return s.kind() == Z3_DATATYPE_SORT

def is_datatype_constructor(x):
  s = x.sort()
  if is_datatype_sort(s):
    n = s.num_constructors()
    f = x.decl()
    for i in range(n):
      c = s.constructor(i)
      if eq(c, f):
        return True
  return False 

# Return True if x is a constant constructor, that is, a constructor without arguments.
def is_datatype_const_value(x):
  return is_const(x) and is_datatype_constructor(x)

次に、次のコードは、解釈されていないすべての定数をキャッチします。

 is_const(a) and a.decl().kind() == Z3_OP_UNINTERPRETED and not is_datatype_const_value(a)

次のリンクには、完全な例が含まれています。 http://rise4fun.com/Z3Py/vjb

于 2012-09-07T19:52:08.383 に答える
0

整数に対してこれを行う 1 つの方法は、is_intand を使用することis_int_valueです。

x = Int('x')
print "x types"
print is_int(x) # true, is of sort int
print is_int_value(x) # false, not a "value"

x_ = IntVal(7)
print "x_ types"
print is_int(x_) # true, is also of sort int
print is_int_value(x_) # true, is a value

実数の場合、これを使用is_realして変数の並べ替えをチェックし、(の論理和)is_algebraic_valueとis_rational_value値を使用してこれを行うことができます (API のような関数は見ませんでしたis_real_valueが、この論理和で実行できると思います)。ビットベクトルの場合、is_bv_valuefor 値を使用しis_bvて、変数の並べ替えを確認できます。

.NET API には がありExpr.IsNumeral、これらが API でどのように実装されているかをここで確認できます (たとえば、Expr.IsIntNum[Python に相当する] はとの両方が trueかどうかをis_int_valueチェックします): http://research.microsoft.com/en-us/ um/redmond/projects/z3/_expr_8cs_source.htmlExpr.IsNumeralExpr.IsInt

カスタム定義の列挙型の並べ替えでこれを行う方法はすぐにはわかりませんでした。別の方法として、ビットベクトルを使用して列挙型をエンコードし、is_bv_value. ただし、より良い回避策として、より一般的な代数データ型とそれらの自動的に作成された「認識機能」を使用する必要があるようです。Python API は、列挙型の並べ替えとして宣言した場合、レコグナイザーを適切に作成しないようです。これは、事実上列挙型の並べ替えである (ただし、より一般的なデータ型として宣言されている) ものに対して行う 1 つの方法です。

以下の Z3Py エンコーディング: http://rise4fun.com/Z3Py/ELtn

ColorVal = Datatype('ColorVal')
ColorVal.declare('white')
ColorVal.declare('black')
ColorVal = ColorVal.create()

mycolor = Const("mycolor", ColorVal)

print ColorVal.recognizer(0) # is_white
print ColorVal.recognizer(1) # is_black

print simplify(ColorVal.is_white(mycolor)) # returns is_white(mycolor)
print simplify(ColorVal.is_black(mycolor)) # returns is_black(mycolor)

mycolorVal = ColorVal.white # set to value white
print simplify(ColorVal.is_white(mycolorVal)) # true
print simplify(ColorVal.is_black(mycolorVal)) # false

# compare "variable" versus "value" with return of is_white, is_black, etc.: if it gives a boolean value, it's a value, if not, it's a variable
print "var vs. value"
x = simplify(ColorVal.is_white(mycolor))
print is_true(x) or is_false(x) # returns false, since x is is_white(mycolor)
y = simplify(ColorVal.is_white(mycolorVal))
print is_true(y) or is_false(y) # true

ColorValEnum, (whiteEnum,blackEnum)  = EnumSort("ColorValEnum",["whiteEnum","blackEnum"])
mycolorEnum = Const("mycolorEnum",ColorValEnum)

print ColorValEnum.recognizer(0) # is_whiteEnum
print ColorValEnum.recognizer(1) # is_blackEnum

# it appears that declaring an enum does not properly create the recognizers in the Python API:
#print simplify(ColorValEnum.is_whiteEnum(mycolorEnum)) # error: gives DatatypeSortRef instance has no attribute 'is_whiteEnum'
#print simplify(ColorValEnum.is_blackEnum(mycolorEnum)) # error: gives DatatypeSortRef instance has no attribute 'is_blackEnum'
于 2012-09-04T17:26:33.460 に答える