有界的普遍量化变量

Question

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

例如，让我们假设我有一个Real类型的变量，称为"；时间"；其用于对系统中的时间进行建模。假设我有一个断言，它说某个一元函数的值"；func1"；应始终在1和100之间。函数将时间变量作为输入。用Z3表示，我将属性编码如下：

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

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

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

   就我对Z3的理解而言，所有常数都有数学（理论）实现，而不是计算机（实践）实现，即它们的值不受约束（不幸的是，我目前无法指向我读到这篇文章的资源）。假设有了时间，我在系统中对时间进行建模，根据系统约束，它不能运行超过x小时，我可以使用它，并说时间值在0和x*60'*60之间，以给出以秒为单位的最大执行时间。我知道我可以通过以下断言断言时间的允许值：

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

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

因此，这将导致这样一种情况：如果属性2被注入，并且对于时间值I指定x*60*60 + 1，则不应取消设置，因为ForAll仅对时间值有效。

Answer 1

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

注意

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

将变量"时间"视为绑定。该公式的含义与：

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

当您断言上述内容时，其含义是xx的任何实例化都成立（断言）。特别是，您可以用自由变量"时间"实例化量化变量，特别是，可以用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支持标准的一阶多排序逻辑（具有背景理论）。