通过加法减少 z3 中的整数集

Question

我正在尝试（但失败了）z3 中的减少集合，而不是加法等操作。这个想法最终是为了证明在合理大小的固定大小的集合上任意减少的东西。

下面两个示例中的第一个似乎应该产生unsat，但事实并非如此。第二个确实有效，但我不想使用它，因为它需要逐步摆弄模型。

def test_reduce():
  LIM = 5
  VARS = 10
  poss = [Int('i%d'%x) for x in range(VARS)]
  i = Int('i')
  s = Solver()
  arr = Array('arr', IntSort(), BoolSort())
  s.add(arr == Lambda(i, And(i < LIM, i >= 0)))
  a = arr
  for x in range(len(poss)):
    s.add(Implies(a != EmptySet(IntSort()), arr[poss[x]]))
    a = SetDel(a, poss[x])
  def final_stmt(l):
    if len(l) == 0: return 0
    return If(Not(arr[l[0]]), 0, l[0] + (0 if len(l) == 1 else final_stmt(l[1:])))
  sm = final_stmt(poss)
  s.push()
  s.add(sm == 1)
  assert s.check() == unsat

有趣的是，下面的例子效果更好，但我不知道为什么......

def test_reduce_with_loop_model():
  s = Solver()
  i = Int('i')
  arr = Array('arr', IntSort(), BoolSort())
  LIM = 1000
  s.add(arr == Lambda(i, And(i < LIM, i >= 0)))
  sm = 0
  f = Int(str(uuid4()))
  while True:
    s.push()
    s.add(arr[f])
    chk = s.check()
    if chk == unsat:
      s.pop()
      break
    tmp = s.model()[f]
    sm = sm + tmp
    s.pop()
    s.add(f != tmp)
  s.push()
  s.add(sm == sum(range(LIM)))
  assert s.check() == sat
  s.pop()
  s.push()
  s.add(sm == 11)
  assert s.check() == unsat

Answer 1

请注意，您致电：

    f = Int(str(uuid4()))

第一种情况是inside循环，第二种情况是outside循环。因此，第二种情况仅适用于一个变量，因此收敛速度很快。而第一个不断创建变量并为 z3 创建一个更难的问题。毫不奇怪，这两者的行为明显不同，因为它们编码完全不同的约束。

作为一般说明，通过操作减少元素数组对于 z3 来说并不是一个简单的问题。首先，您必须假设元素的上限。如果是这样，那为什么还要打扰Lambda 或Array 呢？只需创建一个包含那么多变量的 Python 列表，然后完全忽略数组逻辑。那就是：

elts = [Int("s%d"%i) for i in range(100)]

然后要访问“数组”的元素，只需使用 Python 访问器符号 elts[12]。

请注意，仅仅在您的所有访问都使用常量整数时才有效；即，您的索引不能是符号的。但是，如果您正在寻找证明减少属性，那应该就足够了；并且会更有效率。