В настоящее время я работаю над кодом, который переводит «путь» через программу C в соответствующий запрос SMT, чтобы проверить возможность этого пути. У меня есть рабочий код, который создает запрос SMT-LIB v1.2 и использует Z3 2.11 и логику QF_AUFBV для решения запроса. В настоящее время я переношу этот код на Z3 4.3, чтобы воспользоваться преимуществами любого повышения скорости, которое могло произойти с тех пор, тем более что мой прежний код, похоже, занимает много времени (около 22 минут) на запрос, который просто присваивает 24 значения для трехмерный массив и проверяет значение определенного места в массиве.
Однако похоже, что логика QF_AUFBV (начиная со стандарта SMT-LIB v2.0) больше не поддерживает многомерные массивы, точнее массивы, значения которых также являются массивами (потенциально более глубокими). Как только я уберу строку "(set-logic QF_AUFBV)" из своего запроса, Z3 4.3 сможет обработать запрос, но это все равно займет много времени.
Мне было интересно, знает ли кто-нибудь, почему поддержка многомерных массивов была остановлена в стандарте SMT-LIB v2.0, и какую альтернативную логику я мог бы использовать. Мне также было интересно, какую логику в любом случае использовал Z3, когда я удалил строку, определяющую теорию QF_AUFBV.
Спасибо!
