z3py, список функций, объявленных в типе данных - PullRequest
Новая
       13

z3py, список функций, объявленных в типе данных

0 голосов
/ 04 февраля 2020 
from z3 import *

record = Datatype("record")
record.declare('cons', ('f1', BoolSort()), ('f2', BoolSort()), ('f3', BoolSort()))
record = record.create()

tmp = Const('tmp', record)

data_type = tmp.sort()  # get the sort of the tmp var, which will be "record"
functions = data_type.functions  # returns the list of functions declared in "record" [cons, f1, f2, f3]

Как получить список объявленных функций из сортировки? Пожалуйста, посмотрите на последнюю строку кода.

1 Ответ

0 голосов
/ 04 февраля 2020

Вы ищете поле constructors, здесь: https://z3prover.github.io/api/html/z3py_8py_source.html#l04711

Обратите внимание, что, перезаписав значение record, вы загнали себя в угол. Лучше держать имена явными, если вы хотите заниматься этим уровнем программирования. То есть, называйте тип данных другим именем, а когда вы create, назначаете ему другое имя. Таким образом, вы можете легко отслеживать тип данных и сортировать. Вот ваш пример, кодированный более четко: 

from z3 import *

record_dt = Datatype("record")
record_dt.declare('cons', ('f1', BoolSort()), ('f2', BoolSort()), ('f3', BoolSort()))
record_sort = record_dt.create()

functions = record_dt.constructors
print functions

Это печатает: 

[('cons', 'is-cons', (('f1', Bool), ('f2', Bool), ('f3', Bool)))]

Это дает вам имя конструктора (cons), распознаватель (is-cons), и имена и виды всех полей (f1, f2, f3), которые вы затем можете использовать по мере того, как вы будете sh.

...