Мне интересно, возможно ли создать алгебраический тип данных, который зависит от другого алгебраического типа данных в Z3Py.
Например, скажем, я определил свой собственный тип данных Bool и хочу сам определить список Bool:
from z3 import *
Bool = Datatype('Bool')
Bool.declare('TRUE')
Bool.declare('FALSE')
Bool = Bool.create()
TRUE = Bool.TRUE
FALSE = Bool.FALSE
это отлично работает, тогда:
BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
BoolList = BoolList.create()
Это не удается с сообщением:
>>> BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
AttributeError: DatatypeSortRef instance has no __call__ method
причина в использовании Bool() в качестве ссылки на ранее определенный тип данных. Вместо этого использование логической сортировки Z3 работает как шарм:
BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', BoolSort()), ('tail', BoolList))
Является ли определение алгебраического типа данных, который зависит от других алгебраических типов данных, невозможным, или мне нужно передать s.th. кроме Bool() ?
Заранее спасибо! Карстен