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

Question

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

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

现在，当我尝试从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版本太新？问候，弗洛里安

Answer 1

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

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

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

(= (fib 10) (fib 12))

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