在 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)
最佳答案
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
关于python - z3 常量声明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12448583/