Z3：用量词建模
Z3: Modeling with Quantifiers
我想用z3证明(∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)。它的否定是：∀i(0≤i<k→a[i]>0)∧a[k]>0∧∃i(0≤i≤k∧¬(a[i]>0))。首先，我将 k 的值设置为 5 并忽略 a[k]>0 部分，然后尝试：
from z3 import *
i = Int('i')`
a = Array('a',IntSort(),IntSort())
solver = Solver()
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0)))
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0))))
print solver.check()
print solver.model()
输出为：
sat
[i!0 = 5,
a = [else -> k!8!10(k!9(Var(0)))],
k!8 = [else -> k!8!10(k!9(Var(0)))],
k!9 = [else -> If(Var(0) >= 4, If(Var(0) >= 5, 5, 4), 0)],
k!8!10 = [0 -> 7720, 4 -> 1, else -> -38]]
我不知道输出的意思，我想它的模型应该是i = 5。然后，我加上a[5] > 0，我想应该是不满足吧。代码如下：
from z3 import *
i = Int('i')
a = Array('a',IntSort(),IntSort())
solver = Solver()
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0)))
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0))))
solver.add(a[5] > 0)
print solver.check()
print solver.model()
输出为：
unsat
那么，我如何通过z3py证明(∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)，输出的含义是什么？
我有点不清楚你想用你的查询做什么。你为什么"set"k的值？根据问题的开头，这似乎与您要证明的一般情况不符，但也许您现在只对特殊情况感兴趣。
您已正确地将有效性问题转变为可满足性问题：公式的否定是可满足的，前提是原始公式有效。
在Z3的第一个回复中，确实得到了模型；这表示您试图证明的（较弱的）第一个蕴涵的反例。如果你想想这个反例的演示需要什么，你不得不选择将（绑定的）存在变量实例化为5。这就是模型中i!0的意义；它是一个新的（免费的）名称，代表存在绑定变量被分配到的模型元素。
从另一个角度来看（更准确地说，关于工具的作用），存在量词在 Z3 之前 "skolemised" 已经消失（存在绑定变量被新常量替换）有趣的工作，所以它实际上是在处理一个等同于查询公式可满足性的查询：
∀i(0≤i<k→a[i]>0)∧a[k]>0∧(0≤ i!0 ≤k∧¬(a[ i!0 ]>0))
当您将查询加强到原始蕴涵的否定时，您会从 Z3 中得到不满意。这意味着这个否定的公式是不可满足的，所以你感兴趣的蕴涵是有效的；你已经证明
∀i(0≤i<5→a[i]>0)∧a[5]>0)→∀i(0≤i≤5→a[i]>0)
如果您在问题中跳过将 k 设置为 5，您应该会得到相同的结果。
关于 Z3 的第一个响应中的其他信息，模型不仅必须包含 (skolemised) i 的值，还必须包含问题中数组 a 的值。数组被表示为函数，可以在这样的模型中由案例定义； "else" 案例是包罗万象的，也是此处使用的每个函数中唯一的案例。 Var(0) 是函数的（第一个也是唯一的）参数的语法。在这个模型中，数组是通过其他两个函数的组合间接定义的，k!9（它似乎用于标识与模型相关的部分索引集；在本例中为 0,4 和 5），以及k!8!10（它定义了这些索引到值的映射）。特别是，在这个模型中，数组在索引 0 处存储 7720，在索引 4 处存储 1，在索引 5 处存储 -38（k!9 定义的情况下不会产生其他索引；从概念上讲，我会理解这意味着此模型中的数组在其他索引处未定义）。
我想用z3证明(∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)。它的否定是：∀i(0≤i<k→a[i]>0)∧a[k]>0∧∃i(0≤i≤k∧¬(a[i]>0))。首先，我将 k 的值设置为 5 并忽略 a[k]>0 部分，然后尝试：
from z3 import *
i = Int('i')`
a = Array('a',IntSort(),IntSort())
solver = Solver()
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0)))
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0))))
print solver.check()
print solver.model()
输出为：
sat
[i!0 = 5,
a = [else -> k!8!10(k!9(Var(0)))],
k!8 = [else -> k!8!10(k!9(Var(0)))],
k!9 = [else -> If(Var(0) >= 4, If(Var(0) >= 5, 5, 4), 0)],
k!8!10 = [0 -> 7720, 4 -> 1, else -> -38]]
我不知道输出的意思，我想它的模型应该是i = 5。然后，我加上a[5] > 0，我想应该是不满足吧。代码如下：
from z3 import *
i = Int('i')
a = Array('a',IntSort(),IntSort())
solver = Solver()
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0)))
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0))))
solver.add(a[5] > 0)
print solver.check()
print solver.model()
输出为：
unsat
那么，我如何通过z3py证明(∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)，输出的含义是什么？
我有点不清楚你想用你的查询做什么。你为什么"set"k的值？根据问题的开头，这似乎与您要证明的一般情况不符，但也许您现在只对特殊情况感兴趣。
您已正确地将有效性问题转变为可满足性问题：公式的否定是可满足的，前提是原始公式有效。
在Z3的第一个回复中，确实得到了模型；这表示您试图证明的（较弱的）第一个蕴涵的反例。如果你想想这个反例的演示需要什么，你不得不选择将（绑定的）存在变量实例化为5。这就是模型中i!0的意义；它是一个新的（免费的）名称，代表存在绑定变量被分配到的模型元素。
从另一个角度来看（更准确地说，关于工具的作用），存在量词在 Z3 之前 "skolemised" 已经消失（存在绑定变量被新常量替换）有趣的工作，所以它实际上是在处理一个等同于查询公式可满足性的查询：
∀i(0≤i<k→a[i]>0)∧a[k]>0∧(0≤ i!0 ≤k∧¬(a[ i!0 ]>0))
当您将查询加强到原始蕴涵的否定时，您会从 Z3 中得到不满意。这意味着这个否定的公式是不可满足的，所以你感兴趣的蕴涵是有效的；你已经证明 ∀i(0≤i<5→a[i]>0)∧a[5]>0)→∀i(0≤i≤5→a[i]>0)
如果您在问题中跳过将 k 设置为 5，您应该会得到相同的结果。
关于 Z3 的第一个响应中的其他信息，模型不仅必须包含 (skolemised) i 的值，还必须包含问题中数组 a 的值。数组被表示为函数，可以在这样的模型中由案例定义； "else" 案例是包罗万象的，也是此处使用的每个函数中唯一的案例。 Var(0) 是函数的（第一个也是唯一的）参数的语法。在这个模型中，数组是通过其他两个函数的组合间接定义的，k!9（它似乎用于标识与模型相关的部分索引集；在本例中为 0,4 和 5），以及k!8!10（它定义了这些索引到值的映射）。特别是，在这个模型中，数组在索引 0 处存储 7720，在索引 4 处存储 1，在索引 5 处存储 -38（k!9 定义的情况下不会产生其他索引；从概念上讲，我会理解这意味着此模型中的数组在其他索引处未定义）。