Сортировка наследования в z3

Question

Есть ли способ определить наследование между сортировками в z3? (Я использую Python API)

Я пытаюсь моделировать два разных типа событий, записывать события и читать события; для каждого из них я использую Сорт (WriteSort и ReadSort). Однако я хотел бы иметь «сумму» Сортировка (EventSort), которая представляет собой событие записи или чтения.

Я определения функций с помощью следующей области:

f1 = Function('f1', WriteSort, WriteSort, BoolSort()) 
f2 = Function('f2', ReadSort, ReadSort, BoolSort()) 
f3 = Function('f3', EventSort, EventSort, BoolSort()) 

Одним из возможных вариантов было бы определить EventSort, как и абстрактный тип данных, но область все мои функции должны быть (EventSort х EventSort), и единственный способ ограничить такой домен - это сделать это вручную.

Есть в любом случае, чтобы определить как WriteSort и ReadSort как "subsort" из EventSort?

Answer 1

Насколько я знаю, суб-сортировка не поддерживается Z3 (или любым другим решателем SMT). Вы можете объявить неинтерпретированную сортировку Top и использовать ее для встраивания подстрок в Top, например. box_int(i: Int): Top и обратная функция unbox_int(t: Top): Int вместе с аксиомой forall i: Int :: unbox_int(box_int(i)) = i.

Если вы кодирующая тип системы, один из способов кодирования подтипов является введение интерпретируемого Type рода, вместе с функциями typeOf(o: Object): Type и subtype(t1: Type, t2: Type): Bool, и транзитивностью аксиомой для подтипа соотношения (и потенциально возвратность аксиомы).

Хорошее обсуждение перевода систем типов на SMTLIB можно найти в this paper.