为什么Z3对下面的输入没有反应？

Question

我最初发布的问题如下虚线所示，但从那以后我有了一个更简单的例子：

(declare-fun f (Int) Int)
(assert (= (f 10) 1))
(check-sat)
(get-model)

按预期生成 f 的解释。但是，将常量更改为 10 以外的任何值，Z3 只是旋转箭头几次，然后什么也没打印！

--------------------------- 原始问题 ------ ----------------------

我在以下输入上尝试了 Z3，箭头转动了几次并停止，但 Z3 打印或什么也没说。为什么？

(declare-fun f (Int Int) Int)
(assert (>= (f 1 1) 1)) 
(assert (>= (f 1 2) 2))
(assert (>= (f 2 1) 2))
(assert (>= (f 2 2) 2))
(assert (= (f 1 1) 1))
(assert (= (f 2 2) 2))
(assert (or (= (f 1 2) 1)  (= (f 1 2) 2)))
(assert (or (= (f 2 1) 1)  (= (f 2 1) 2)))
(check-sat)
(get-model)

我觉得我错过了一些非常明显的东西..

Answer 1

我正在获取（使用iZ3，Z3不稳定分支）

sat 
(model 
  (define-fun f ((x!1 Int) (x!2 Int)) Int 
    (ite (and (= x!1 1) (= x!2 1)) 1 
    (ite (and (= x!1 2) (= x!2 2)) 2 
    (ite (and (= x!1 1) (= x!2 2)) 2 
    (ite (and (= x!1 2) (= x!2 1)) 2 2))))) 
 )

在线运行这个例子here

Answer 2

我猜你在rise4fun 上使用的是Z3？那里运行的版本可能有点过时了。我们必须在那里手动更新二进制文件。如果它没有回复，要么是因为超时，要么是因为存在其他问题（例如，segfault）。 rise4fun 上的版本很可能存在一些已经在其他版本的 Z3 中修复的错误（例如，不稳定的、iZ3 等）。