边界通用量化变量

Question

我想知道是否可以在 Z3 中限制通用量化变量的取值范围。

例如，假设我有一个名为“time”的 Real 类型变量，用于对系统中的时间建模。 假设我有一个断言，它说某个一元函数“func1”的值应始终在 1 到 100 之间。该函数将输入作为时间变量。在 Z3 中，我将 属性 编码如下：

1. ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

   请注意，我明确需要对时间变量进行普遍量化，因为如果我注入以下类型的 属性，我希望 Z3 给我不满意的结果：

2. Exists(time, func1(time) == 101)

   据我对 Z3 的理解，所有常量都具有数学（理论）而非计算机（实际）实现，即它们的值不受约束（不幸的是，我无法指向我在片刻）。假设随着时间的推移，我在我的系统中对时间进行建模，并且根据系统限制，它不能 运行 超过 x 小时，我可以使用它并说时间值在 0 到 x*60'*60 之间给出以秒为单位的最长执行时间。我知道我可以使用以下断言断言允许的时间值：

3. And(time >= 0, time <= x*60*60)

   但是会影响1中给出的通用量化吗？

因此，这应该会导致这样一种情况，如果 属性 2 被注入并且我指定 x*60*60 + 1 的时间值，它不应该被取消设置，因为 ForAll 是有效的仅针对时间值。

Answer 1

but will it affect the universal quantification given in 1)?

请注意

ForAll(time, And(func1(time) >= 1, func1(time) <= 100))

将变量 "time" 视为绑定。公式同义：

ForAll(xx, And(func1(xx) >= 1, func1(xx) <= 100))

当您断言以上内容时，意思是 xx 的任何实例化都成立（被断言）。特别是，您可以使用自由变量 "time" 实例化量化变量，特别是，您可以使用 x*60*60+1 实例化产生断言：

 And(func1(x*60*60+1) >= 1, func1(x*60*60+1) <= 100)

假设你想说

 And(func1(xx) >= 1, func1(xx) <= 100))

对于 0 到 x*60*60 之间的每个值 xx 都成立，那么你可以写：

ForAll(xx, Implies(And(xx >= 0, xx <= x*60*60), And(func1(xx) >= 1, func1(xx) <= 100)))

(unfortunately I cannot point to the resource where I have read this at the moment).

合理的逻辑教科书或计算机科学基础书籍应该对此进行深入解释。 Z3 支持标准的一阶多排序逻辑（有背景理论）。