Z3-Python：无效的有界变量以复数反击

Question

使用 Z3（在 Python 中），Z3Exception: Invalid bounded variable(s) 错误（与Z3: Invalid bounded variables 中的问题相同）反击。但我猜是不同的形状。

具体来说，当使用 de Moura 在 (https://leodemoura.github.io/blog/2013/01/26/complex.html) 中的复数编码时，就会发生这种情况。我们可以在下面看到它：

x = Complex('x')
y = Complex('y')
vars = [x,y]

l_1 = (-1000.5 == x*x)
l_2 = (y == x)

phi = Implies(l_1, l_2)

solve(Exists([x], (x==1)))

它返回最后一行的错误。

这个问题与l_1、l_2（也与vars）无关，因为它也因此而失败：

x = Complex('x')

solve(Exists([x], (x==1)))

如果我只更改变量的类型，它会毫无问题地返回[]：

x = Int('x')
y = Int('y')
vars = [x,y]

l_1 = (-1000.5 == x*x)
l_2 = (y == x)

phi = Implies(l_1, l_2)

solve(Exists([x], And(l_1, l_2)))

因此，Complex 的编码存在问题，而不是 Z3: Invalid bounded variables 中的列表问题

有什么想法吗？

编辑

尝试变量列表的答案：

def ComplexExists(ls, phi):
  existential_ls = []
  for i in range(0, len(ls)):
    existential_ls.append([ls[i].r, ls[i].i])
  print(existential_ls)
  return Exists(existential_ls, phi)

x = Complex('x')
y = Complex('y')
vars = [x,y]

l_1 = (-1000.5 == x*x)
l_2 = (y == x)

phi = Implies(l_1, l_2)

solve(ComplexExists(vars, phi))

同样的错误。明显地。 ComplexExists 返回如下列表：[[x.r, x.i], [y.r, y.i], ...]

这是另一种选择：

def ComplexExists(ls, phi):
  existential_ls = []
  for i in range(0, len(ls)):
    existential_ls.append(ls[i].r)
    existential_ls.append(ls[i].i)
  print(existential_ls)
  return Exists(existential_ls, phi)

它返回一个列表并且可以工作，但是所有变量（实部和虚部）都是同一个列表的一部分，这听起来很奇怪：[x.r, x.i, y.r, y.i, ...]

Answer 1

这里的问题是z3不知道Complex类；因此，当它尝试创建量化表达式时，无法将它们映射到正确的内部值。

解决方法很简单；只需确保告诉 z3 您正在量化哪些“基础”变量。也就是说，而不是：

solve(Exists([x], And(l_1, l_2)))

用途：

solve(Exists([x.r, x.i], (x==1)))

或者，您可以定义：

def ComplexExists(cv, e):
    return Exists([cv.r, cv.i], e)

然后：

solve(ComplexExists(x, x==1))

您可以创建ComplexExists 的变体，将列表作为第一个参数处理，就像z3 的Exists 方法一样；等等

请注意，当您运行它时，您会得到一个空列表作为模型，因为您断言的唯一内容是局部量化的；因此您没有任何“顶级”变量来显示其值。我宁愿这样编码：

s = Solver()
s.add(Exists([x.r, x.i], (x==1)))
s.add(phi)
print(s.check())
print(s.model())

然后你得到：

sat
[x.r = 0, y.r = 0, x.i = 0, y.i = 0]

现在输出很清楚了。 （请注意，该模型不满足您的局部量化存在，因为 x 与顶级 x 不同；并且由于 phi 是一个暗示，它满足使先行词为假。`)

使ComplexExists 为变量列表工作

这是ComplexExists 的一个版本，它采用复数列表：

def ComplexExists(ls, phi):
    return Exists([qv for v in ls for qv in [v.r, v.i]], phi)

有了这个定义，你可以调用：

solve(ComplexExists(vars, phi))

它应该可以正常工作。