无法执行 scala^z3 斐波那契示例

Question

我正在尝试在 MacOS 64 位上使用 Scala^Z3，设置如下：

res0: String = Z3 4.0 (build 0, rev. 0), ScalaZ3 3.2.c (in dev.)

现在，当我尝试从 the ScalaZ3 main page 执行斐波那契示例时，我得到以下输出，然后执行停止：

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版本太新？ 问候， 弗洛里安

Answer 1

（请注意，我们还没有机会使用最新版本的 Z3 测试 Scala^Z3。感谢您在这里破土动工。）

您尝试解决的问题包含全称量词并且可以满足。 Z3 的过去版本将以unknown 终止，您可以要求提供一个暂定模型（如您链接到的文档页面上所示）。很可能是新版本设置为非常努力地反驳公式而不是返回unknown，因此不会终止。

您可以尝试一个无法满足的查询，这应该会更好。例如尝试：

(= (fib 10) (fib 12))

Z3 应该能够多次实例化量词以得出公式不可满足的结论。