В z3 Как получить верхнюю часть строки в?

Question

Я хочу утверждать, что верхняя моей строковой переменной равна строковому значению.Например,

> v = z3.String('var')
> v.upper() == z3.StringVal('HELLO')

Однако я не вижу способа получить верх из строкового API z3 .Как мне это сделать?

Я нахожу два похожих вопроса 1 и 2 , которые кажутся болезненными.Это все еще состояние?

Answer 1

Да, это современное состояние.Нет другого способа сделать это, используя строковый API, предоставленный z3.

Обратите внимание, что это проблема как для строк, так и для последовательностей, и суть в том, что нет API для доступа к «элементу»на позиции.(В Z3 строки - это просто последовательности битовых векторов шириной 8).

Был давно отправлен запрос на z3 для добавления этого API: https://github.com/Z3Prover/z3/issues/1302

Возможно, вы захотитеозвучить ваш запрос, чтобы они могли добавить поддержку!

(Обратите внимание, что некоторые высокоуровневые API скрывают эту сложность от пользователя, предоставляя простой способ доступа к элементу в позиции.Вот как это делается в библиотеке SBV: https://github.com/LeventErkok/sbv/blob/master/Data/SBV/List.hs#L135-L171. Но для чего-то настолько простого, что хотелось бы, чтобы базовый решатель просто поддержал его.)