2

我想知道是否可以在 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它仅对时间值有效。

4

1 回答 1

1

但它会影响 1) 中给出的普遍量化吗？

注意

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

将变量“时间”视为绑定。该公式的含义与以下相同：

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)))

（不幸的是，我目前无法指出我读过这篇文章的资源）。

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

于 2016-04-19T14:30:09.660 回答