Z3 не может найти удовлетворяющее назначение для простой формулы с квантификаторами и шаблонами

Question

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

Кажется, что работает, если программа ввода правильная, т. Е. Генерирует разумный ввод для Z3, а Z3 говорит, что он неудовлетворителен, что означает в моем контексте, что программа верна. Но когда я изменил одну инициализацию переменной и, таким образом, сделал программу неправильной, мой верификатор придумал следующую формулу Z3, которая не кажется мне слишком сложной, но Z3 говорит «неизвестно».

(set-option :smt.auto-config false) 
(set-option :smt.mbqi false) 
(declare-fun fib (Int) Int) 
(declare-fun fakeFib (Int) Int) 
(declare-fun n() Int) 
(assert (forall ((n Int)) 
    (! (= (fib n) 
     (ite (= n 0) 0 
      (ite (= n 1) 1 
       (+ (fakeFib (- n 1)) (fakeFib (- n 2)))))) 
     :pattern ((fib n))))) 
(assert (forall ((n Int)) 
    (! (= (fib n) (fakeFib n)) :pattern ((fib n))))) 
(assert (>= n 0)) 
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0))))) 
(check-sat) 

Обратите внимание, что два квантора представляют собой рекурсивное определение фибоначчи. Один мой друг сказал мне этот трюк, чтобы избежать совпадающего цикла: вместо определения fib как рекурсивной функции я представляю еще одну функцию fakeFib, для которой я не предоставляю определение, и использую его в рекурсивном определении fib. Кроме того, я говорю верификатору, что они равны, но этот квантификатор получает только шаблон для fib, а не для fakeFib. Из-за ограничительных паттернов он является неполным, т. Е. Он может доказать только правильность программы, если достаточно проверить один уровень рекурсии, чтобы доказать это (но его можно легко расширить до k уровней). Но я могу жить с этим ограничением, чтобы избежать совпадения циклов.

«Ошибка» кода заключалась в том, что я инициализировал переменную неправильно, и это в конечном итоге приведет к неправильному компоненту (= 1 (fib 0)) в последнем утверждении. Для правильной программы это будет (= 0 (fib 0)).

Некоторые наблюдения:

• Если я заменяю (= 1 (fib 0)) на (= 0 (fib 0)), то Z3 сразу находит, что это невыполнимо.
• Раньше у меня не было опций (set-option :smt.auto-config false) и (set-option :smt.mbqi false), а затем у меня закончилась память на моей машине и вне времени на подъеме4fun.
• Установка (set-option :smt.macro-finder true), которая, похоже, работала для людей с подобными вопросами, не работала для меня. Я предполагаю, что это вызвано тем, что у меня есть два квантора для fib, а не только один.
• Я попытался использовать cvc4 для сравнения, и он сразу же сказал «неизвестно». Поэтому мои проблемы не кажутся специфичными для Z3.
• Формула явно выполнима. (= 1 (fib 0)) - false, поэтому все последнее утверждение автоматически верное. (>= n 0) также легко удовлетворить.

Answer 1

Я не эксперт Z3, но, возможно, я могу пролить немного света.

Отключив MBQI, вы отключите возможность Z3 создавать модели для количественных формул, поэтому я предполагаю, что, когда Z3 не может найти способ доказать свою неподобающую проблему, он быстро сообщает об этом как unknown.

Обратите внимание, что модель для вашей проблемы должна удовлетворяться четырьмя утверждениями не только двумя последними. Как вы указываете, Z3 не может устранить ваше первое утверждение, как будто это макрос, потому что вы предоставляете два определения для fib n.

Если вы включите MBQI, вы увидите, что Z3 пытается найти модель и потребляет довольно много памяти!Я предполагаю, что это потому, что единственный способ удовлетворить вашу спецификацию требует создания рекурсивной функции fib, функции, которую Z3 не поддерживает.

как я буду подходить к этому

То, что вы делаете сейчас это хороший трюк, который позволяет Z3 расширить fib определение столько, сколько нужно для того, чтобы доказать проблему unsat. Но он не очень хорошо сочетается с поиском модели, потому что вы косвенно вводите рекурсивное определение.

Итак, если Z3 сообщает unsat, тогда вы знаете, что ваша программа верна. Если он сообщает unknown, вы должны начать итеративный процесс. Перед этим вы удаляете второе утверждение (= (fib n) (fakeFib n)), чтобы предотвратить бесконечный цикл построения модели.

1. В каждой итерации вы предоставите к-разворачивание fib, где fib(k+1) забирается с точки зрения fakeFib. Вы можете оставить fakeFib n без ограничений, или вы можете наложить на него ограничения света (например, должно быть положительным целым), без добавления рекурсии.
2. Если Z3 сообщает unsat, значит ваша программа верна.
3. Если Z3 сообщает sat, вы должны проверить соответствие модели с fib. Если это согласовано, то вы получите контрпример. Если не соответствует, то вы увеличиваете k и шаг Гото 1.

Вы можете прочитать о к-индукции, что я предлагаю вам более или менее.