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 表达式的 Python 变量3.14。我们可以在构建 Z3 表达式/公式时x用作简写。3.14Python 变量z是指向 Z3 表达式y。最后，z > x返回 Z3 表达式y > 3.14。Z3Py 初学者通常会将 Python 变量与 Z3 表达式混淆。区别清楚后，一切都开始变得有意义。

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