Z3：无效的有界变量 [英] Z3: Invalid bounded variables

问题描述

我正在尝试查看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，也不会发生任何变化。所以我不知道这个错误指的是什么界限。

有什么想法吗？

推荐答案

您到处都有几个打字错误，因此很难复制。但底线是，您需要一个单变量或一个量化位置的变量列表，并且它们都需要事先声明。修复您的其他拼写错误时，请执行以下操作：

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中正确地编写量化公式。

这篇关于Z3：无效的有界变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！