Может ли Z3 проверить выполнимость формул, содержащих рекурсивные функции?

Question

Я пробую некоторые примеры учебника по Z3 , в которых используются рекурсивные функции.Я опробовал следующий пример.

1. Фибоначчи (раздел 8.3)
2. IsNat (раздел 8.3)
3. Индуктивный (Раздел 10.5)

Z3 превышен во всех приведенных выше примерах.Но из учебника, похоже, следует, что только Inductive не является завершающим.

Может ли Z3 проверить выполнимость формул, содержащих рекурсивные функции, или он не может обрабатывать никакие индуктивные факты?

Answer 1

Эти примеры из учебника по Z3 приведены для иллюстрации ограничений технологии, лежащей в основе Z3.

Z3 не работает в этих примерах по двум причинам:

1. Модели, выпускаемые Z3, назначают интерпретацию для каждого не интерпретируемого функционального символа. Модели можно рассматривать как функциональные программы. Текущая версия не дает рекурсивных определений. Первый пример выполним, но Z3 не может дать интерпретацию для fib, потому что он не поддерживает рекурсивные определения. У нас есть планы по расширению Z3 в этом направлении.

2. Z3 не поддерживает доказательства по индукции. Примеры 2 и 3 неудовлетворительны, но Z3 терпит неудачу, потому что не поддерживает доказательство по индукции. У нас также есть планы добавить базовую поддержку для этого.

Хотя эти предметы находятся в моем списке TODO, я не буду над ними работать в этом году.