z3py：如何询问我的 adt 实例有哪个构造函数？

Question

假设我有一个数据类型，例如：

List = Datatype('List')
List.declare('cons', ('car', IntSort()), ('cdr', List))
List.declare('nil')
List = List.create()

我有一个实例，来自：

s.check()
instance = s.model()[var]

如何查询我的实例有哪个构造函数？我知道我可以做这样的事情：

for i in range(List.num_constructors()):
    if List.recognizer(i)(instance):
        break
return List.constructor(i)

但是当构造函数的数量很大时，这不是一个很实用的方法。我怎么能问这个？

Answer 1

Python 接口为您定义了识别器 is_cons、is_nil，然后您可以使用它们来简化代码。类似于：

from z3 import *

List = Datatype('List')
List.declare('cons', ('car', IntSort()), ('cdr', List))
List.declare('nil')
List = List.create()

# constructors
cons = List.cons
car  = List.car
cdr  = List.cdr
nil  = List.nil

# recognizers
def is_cons (x): return simplify(List.is_cons(x))
def is_nil  (x): return simplify(List.is_nil(x))

def valToConstructor(l):
    if is_cons(l):
        return "Found cons"
    elif is_nil(l):
        return "Found nil"
    else:
        raise Exception('Unexpected list value: {}'.format(l))

# example:
ex1 = nil
ex2 = cons (0, cons (1, ex1))

print valToConstructor(ex1)
print valToConstructor(ex2)

当运行时，会产生：

Found nil
Found cons

请注意，您不能跳过valToConstructor中的异常情况，因为此函数也可能使用符号值调用；并且识别器不会为这些值开火。但是如果你总是用你从模型中得到的值来调用它，它应该工作得很好。

直接访问构造函数

您还可以对基础 AST 使用 decl 函数：

>>> ex1.decl()
nil
>>> ex2.decl()
cons

但是当你传递的对象是一个符号值时你必须要小心；在那种情况下 decl returns 它的名字：

>>> ex3 = Const('ex3_name', List)
>>> ex3.decl()
ex3_name

但这也许正是您要寻找的。

z3py：如何询问我的 adt 实例有哪个构造函数？

z3py: how to ask which constructor my adt instance has?

python

z3py

直接访问构造函数