z3py: как узнать, какой конструктор у моего экземпляра adt? - PullRequest
Новая
       4

z3py: как узнать, какой конструктор у моего экземпляра adt?

0 голосов
/ 07 ноября 2018

Предположим, у меня есть тип данных, например: 

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)

Но это не очень практичный способ, когда число конструкторов велико. Как я могу спросить это?

1 Ответ

0 голосов
/ 07 ноября 2018

Интерфейс 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, поскольку эта функция также может вызываться с символическим значением; и распознаватели не будут стрелять в эти ценности. Но если вы всегда называете это значениями, которые вы получаете из модели, это должно работать просто отлично.

Прямой доступ к конструктору

Вы также можете использовать функцию decl для базового AST: 

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

Но вы должны быть осторожны, когда объект, который вы передаете, является символическим значением; как в этом случае decl возвращает свое имя: 

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

Но, возможно, это именно то, что вы ищете.

...