Z3:无效的有界变量

Question

我试图在Z3(Python(中查看一个句子的有效性，但我收到了以下消息：Invalid bounded variable(s)

我在这里复制我遵循的步骤：

v, a, b, c, d, e = Ints('v a b c d e') 
lt_1 = (v == 4)
lt_2 = (v == 2)
lt_3 = (v == 3)
lt_4 = (v == 5)
lt_5 = (v == 0)
lt_6 = (v >= 0)
lt_7 = (v <= 4)
s_vars = [v]
e_vars = [a, b, c, d]
pos_lts = [lt_1, lt_2, lt_3, lt_4, lt_5, lt_6, lt_7]
neg_lts = []
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
universal = ForAll([e_vars], (posNeg_Conjunction))
pol_phi = Exists([s_vars], universal)
solve(pol_phi)

请注意，有一个空列表neg_lts(故意执行(。

由于普遍量化的变量不会出现在公式中(也是故意的(，我测试了更改代码的最后一部分，以防万一：

...
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
universal = posNeg_Conjunction
pol_phi = Exists([s_vars], universal)
solve(pol_phi)

但仍然得到相同的错误(但现在在Exists部分(。如果我将变量设置为Reals，也不会有任何变化。所以我不知道什么是错误的界限。

知道吗？

Answer 1

这里和那里都有一些拼写错误，这使得复制变得困难。但最重要的是，在量化的位置上，你需要一个单一的变量或一系列变量，而且它们都需要事先声明。修复你的其他打字错误，以及，以下通过：

from z3 import *
v, a, b, c, d, e = Ints('v a b c d e').
lt_1 = (v == 4)
lt_2 = (v == 2)
lt_3 = (v == 3)
lt_4 = (v == 5)
lt_5 = (v == 0)
lt_6 = (v >= 0)
lt_7 = (v <= 4)
s_vars = [v]
e_vars = [a, b, c, d]
pos_lts = [lt_1, lt_2, lt_3, lt_4, lt_5, lt_6, lt_7]
neg_lts = []
posNeg_Conjunction = And(And(pos_lts), And(neg_lts))
universal = ForAll(e_vars, (posNeg_Conjunction))
pol_phi = Exists(s_vars, universal)
solve(pol_phi)

运行时，它会打印no solution。我没有试着理解你的公式，所以我猜这是意料之中的事；你的问题似乎主要是关于如何在z3py中正确地写出量化公式。