python - z3 常量声明

Question

在 Z3 Python 中，1) x = Const("x",IntSort()) 与 2) x = Int("x") 之间有什么区别？ is_const 对两者都返回 true，并且它们都是 ArithRef。我认为 1) 适合定义一个 const，例如，x 是 3.14，而 2) 适合创建一个变量。

是否有正确的方法来创建像 x = 3.14 这样的 const 变量(除了生成公式 x == 3.14)

Answer 1

Const("x", IntSort()) 和 Int("x") 没有区别。我们应该将 Int("x") 视为前者的语法糖。函数 Const 通常用于定义用户定义类型的常量。示例:

S, (a, b, c) = EnumSort('S', ('a', 'b', 'c'))
x = Const("x", S)

在 Z3 中，我们使用术语“变量”来表示通用变量和存在变量。量词自由公式不包含变量，仅包含常量。在公式 x + 1 > 0 中，我们说 x 和 1 是常量。我们说 x 是一个未解释的常量，而 1 是一个已解释的常量。也就是说，1 的含义是固定的，但 Z3 可以自由地为 x 分配解释以使公式可满足。如果您只想创建解释常量 3.14，您可以使用 RealVal('3.14')。在以下示例中，x 不是 Z3 表达式，而是指向 Z3 表达式 3.14 的 Python 变量。在构建 Z3 表达式/公式时，我们可以使用 x 作为 3.14 的简写。 Python 变量 z 指向 Z3 表达式 y。最后，z > x 返回 Z3 表达式 y > 3.14。 Z3Py 初学者通常会将 Python 变量与 Z3 表达式混淆。清楚区别之后，一切都开始变得有意义了。

x = RealVal('3.14')
z = Real('y')
print z > x