6

只是想在z3py中，如何检查给定的常量表达式是变量还是值？例如 

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

所以 x,mycolor 都是 variables 而 x_,True,False,White,Black 是 values 而不是 variables 。

z3py 有 is_var 谓词，但目的不同。如果我想将公式中的所有变量重命名为其他变量，这很有用。

4

2 回答 2

7

您所说的变量（技术上）在 Z3 中称为未解释的常量。值（例如1, true, #x01）称为解释常量。a因此，原则上，可以使用以下代码来快速检查是否是“变量”：

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

这段代码适用于所有东西，但数据类型除外。在尝试了您的示例后，我意识到 Z3 错误地返回Z3_OP_UNINTERPRETED了数据类型构造函数。我为 Z3 4.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

对整数执行此操作的一种方法是使用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值（我没有is_real_value在 API 中看到类似的函数，但我认为这种析取会做到这一点）。对于位向量，您可以使用is_bv_value值，并is_bv检查变量排序。

.NET API 具有Expr.IsNumeral，您可以在此处查看这些 API 是如何实现的（例如，Expr.IsIntNum[相当于 Python is_int_value] 检查两者Expr.IsNumeral是否Expr.IsInt为真）：http ://research.microsoft.com/en-us/嗯/redmond/projects/z3/_expr_8cs_source.html

我没有立即看到为自定义枚举排序执行此操作的方法。作为一种选择，您可以使用位向量对枚举进行编码，并使用is_bv_value. 不过，作为一种更好的解决方法，您似乎需要使用更通用的代数数据类型及其自动创建的“识别器”。如果您将它们声明为枚举排序，Python API 似乎无法正确创建识别器。这是一种有效的枚举排序方法（但声明为更通用的数据类型）。

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 回答