Модели и рекурсивные функции

Question

As previously asked Z3 не может предоставить модель для рекурсивных функций. Однако можно ли указать Z3 (желательно через Java API), что модель без определения для рекурсивных функций является достаточной (или действительно выбирает интересующие меня функции, по сути, мне не нужна модель для непостоянных функций) ? Очевидно, что это может привести к возвращению запросов, хотя некоторые функции не имеют модели. В принципе, пользователь должен обеспечить, чтобы эти функции имели некоторую модель. Однако я бы предположил, что это невозможно реализовать, как работают решатели Z3 или SMT, т. Е. Я бы предположил, что Z3 нуждается в (частичной) модели рекурсивных функций для evalutate выражений.

Answer 1

Реализация MBQI для квантификаторов на самом деле не очень хорошо работает с рекурсивными функциями. Есть одна вещь, которая могла бы сделать трюк для вас: заменить определения рекурсивных функций на ограниченные рекурсивные функции. Вы добавляете дополнительный аргумент, который подсчитывает количество разверток, которые вы хотите изучить в функции. Всякий раз, когда вы применяете рекурсивную функцию в остальной части ввода, задайте параметр глубины. Вы можете использовать либо алгебраические данные типа Peano, либо целые числа. Инструментарий символических автоматов использует этот подход, например.

Answer 2

Я нашел один документ, в котором исследуется идея, изложенная в ответе Николая Бьорнера далее: «Вычисление с помощью SMT-решения» Амина, Лейно и Ромфа (2014).

Кроме того, я нашел «выполнимость Modulo рекурсивной программу» по Сутеру, köksal и Kuncak (2011), который развертывается вызовов рекурсивных функции последовательно до тех пор, выполнимости не могут быть решены.