Я хотел бы знать, что такое определение sort Seq. Я не смог найти его определение в руководстве Z3 SMT 2.0. Я понял, что Seq уже определен, потому что я пытался определить сортировку Seq. Существуют ли некоторые утверждения, связанные с Seq?Определение sort Seq
Спасибо!
Maxi
Да, Seq, RegEx (регулярные выражения) и FP (с плавающей точкой) "зарезервированы" в Z3 4.0. Они еще не были реализованы, но они будут доступны в будущих выпусках. Например, Z3 будет иметь встроенные функции, такие как: seq-last, seq-concat, seq-length и многие другие. В Z3 4.0 эти сорта и функции являются просто «заглушками» и ведут себя как неинтерпретированные сорта и функции. Вот почему у нас нет документации для них.