将未解释的排序替换为 Int 后的 Z3 超时答案

【问题标题】：Z3 timeout after replacement of uninterpreted sort to Int将未解释的排序替换为 Int 后的 Z3 超时
【发布时间】：2014-03-16 13:14:43
【问题描述】：

对于具有未解释排序的公式B Z3 打印unsat 但是当我将排序B 替换为Int 时，它会打印timeout（第二个脚本）。我想了解它的原因。

第一：

(declare-sort A)
(declare-sort B)
(declare-fun f (B) A)
(declare-fun f-inv (A) B)
(declare-const b0 B)
(declare-const b1 B)

(assert (forall ((x B)) (= (f-inv (f x)) x)))
(assert (not (= (f b0) (f b1))))

(check-sat)

秒：

(declare-sort A)
(declare-fun f (Int) A)
(declare-fun f-inv (A) Int)

(assert (forall ((x Int)) (= (f-inv (f x)) x)))
(assert (not (= (f 0) (f 1))))

(check-sat)

【问题讨论】：

标签： z3

【解决方案1】：

原因是Z3无法决定“第一”和“第二”。

对于“第一”，我得到的是：“sat”。

为“第一”当行

(assert (not (= (f b0) (f b1))))

被替换为

(assert  (= (f b0) (f b1)))

结果是“sat”。换句话说，Z3 无法决定“第一”。 Z3的有效结果是“第一”和“第二”的“超时”。

Z3 存在未解释函数组合的问题。

你同意吗？

【讨论】：

“有效”是什么意思？在第一种情况下，正确答案是sat，在第二种情况下也是如此。 1 的模型：b0 != b1。 2 的模型：b0 = b1。所以timeout 在这里不正确。我认为timeout 出现第二种情况是因为Int 是无限排序，但我想得到更详细的答案。
你说得对，知道“超时”的深层原因是什么非常有趣。一切顺利。

【解决方案2】：

在Compsys tools 上在线试用时，两个版本现在都是sat。

【讨论】：