将 Z3 与具体数组一起使用

Question

我想用Z3解决这个问题：

给定两个具有具体值的大小相等的数组 a 和 b，select 满足这些约束的索引：

0 < selection < [length of array]
forall i, a[selection] <= a[i]
forall i, b[selection] >= b[i]

我的 z3py 程序如下所示：

def selectIndex(array1, array2):
   n= len(a) #assume both lists are same size
   s = Solver()
   selection = Int('selection')
   i = Int('i')
   j = Int('j')
   a= Array('a', IntSort(), IntSort())
   b= Array('b', IntSort(), RealSort())

   for idx in range(n):
      Store(a, idx, array1[idx])
      Store(b, idx, array2[idx])

   constraint1 = And(selection >= 0, selection <= n)
   constraint2 = And(i >= 0, i <= n)
   constraint3 = And(j >= 0, j <= n)
   constraint4 = ForAll([i], a[selection] <= a[i])
   constraint5 = ForAll([j], b[selection] >= b[j])

   s.add(And(constraint1, constraint2, constraint3, constraint4, constraint5))

   s.check()
   m = s.model()
   return m[selection].as_long()

模型总是 returns 0，即使给定的输入数组只有一个 selection 满足约束条件。我认为它没有使用数组 a 和 b 中的具体值。我该如何解决这个问题？

Answer 1

这个例子有很多问题，但最关键的是 Store(...) 表达式什么都不做。 Store(...) 的结果是一个新的数组表达式，表示一个旧数组 (a、b)，其中一个索引 (idx) 已更新为新值 (array1[idx], array2[idx]).目前这些新数组被丢弃了，但我们可以保存它们：

for idx in range(n):
    a = Store(a, idx, array1[idx])
    b = Store(b, idx, array2[idx])

此外，我认为

    constraint1 = And(selection >= 0, selection <= n)

不应包含索引 n，即 <= 应为 < 并且对 i 和 j[=25= 的约束]

constraint2 = And(i >= 0, i <= n)
constraint3 = And(j >= 0, j <= n)

不需要。

将 Z3 与具体数组一起使用

Using Z3 with concrete arrays

z3