Не удается выполнить пример scala^z3 fibonacci

Я пытаюсь использовать Scala^Z3 в 64-разрядной версии MacOS со следующими настройками:

res0: String = Z3 4.0 (сборка 0, ред. 0), ScalaZ3 3.2.c (в разработке)

Теперь, когда я пытаюсь выполнить пример Фибоначчи с главной страницы ScalaZ3, я получаю следующий вывод, а затем выполнение останавливается:

fib0 ::: (= (fib!0 0) 0)
fib1 ::: (= (fib!0 1) 1)
fibN ::: (forall (k!0 Int)
  (implies (> k!0 1) (= (fib!0 k!0) (+ (fib!0 (- k!0 1)) (fib!0 (- k!0 2)))))
  :pat {(fib!0 k!0)})
Query ::: (= x (fib!0 1))

Я ждал несколько часов, но больше ничего не происходит ;) У кого-нибудь есть идеи, что я делаю неправильно? Слишком новая версия scala или z3? С уважением, Флориан


scala z3
person user1428162    schedule 31.05.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

(Обратите внимание, что у нас еще не было возможности протестировать Scala^Z3 с последней версией Z3. Спасибо за открытие здесь.)

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

Вы можете попробовать невыполнимый запрос, который должен работать лучше. Попробуйте, например:

(= (fib 10) (fib 12))

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

person Philippe    schedule 31.05.2012
comment
Спасибо за быстрый ответ! Ожидал хотя бы несколько дней, не меньше часа ;) Запрос действительно был оценен как неудовлетворительный. Значит, я правильно настроил программы. Спасибо за помощь! :) - person user1428162; 31.05.2012