如何检查z3中的const是变量还是值？

Question

只是想知道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谓词,但出于不同的目的.如果我想将公式中的所有变量重命名为其他变量,这将非常有用.

Answer 1

你所谓的变量是(技术上)在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

Answer 2

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

.NET API 有Expr.IsNumeral，您可以在此处查看它们是如何在 API 中实现的（例如，Expr.IsIntNum[Python 的等效项is_int_value] 检查 和 是否Expr.IsNumeral都Expr.IsInt为 true）：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'