объявление алгебраического типа данных другого алгебраического типа данных?

Мне интересно, возможно ли создать алгебраический тип данных, который зависит от другого алгебраического типа данных в 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() ?

Заранее спасибо! Карстен


person Carsten Rütz    schedule 08.05.2014    source источник


Ответы (1)


Что ж, оказывается, я использовал скобки там, где не должен был - ссылка на пользовательский тип данных "Bool" не нуждается в вызове:

BoolList.declare('bCONS', ('hd', Bool), ('tail', BoolList))

работает просто отлично :)

person Carsten Rütz    schedule 12.05.2014