如何获得 CBMC 中的所有排列？答案

【问题标题】：How to get all permutations in CBMC?如何获得 CBMC 中的所有排列？
【发布时间】：2020-04-15 09:06:13
【问题描述】：

我正在尝试在 CBMC 中获取数组的所有排列。对于小的情况，例如 [1,2,3]，我想我可以写

i1 = nondet()
i2 = nondet()
i3 = nondet()
assume (i > 0 && i < 4); ...
assume (i1 != i2 && i2 != i3 && i1 != i3);
// do stuffs with i1,i2,i3

但是对于较大的元素，代码会非常混乱。所以我的问题是有没有更好/通用的方式来表达这一点？

【问题讨论】：

使用数组怎么样？（例如）#define COUNT 1000 int array[COUNT]; for (int i = 0; i < COUNT; ++i) array[i] = nondet();
@CraigEstey 问题在于它不会是一个排列 - 相同的值可能会在数组中出现多次。我正在研究一个答案，您将数组中的 nondet 值设置为 i，但由于某种原因，它没有按我的预期工作。
Steinhaus–Johnson–Trotter 算法可用于循环遍历所有排列。您可以检查它是否适用于您的问题。也许有一些技巧，如stackoverflow.com/questions/46919309/… 中所述
感谢大家的cmets和建议。最后，我以不同的方式处理了这个要求，并编写了一个可能很慢的替代方案（由于使用了额外的数组和防御性代码 - 循环），但它做了我认为它做的事情。

标签： c math combinations model-checking cbmc

【解决方案1】：

根据 Craig 的使用数组的建议，您可以循环遍历要置换的值，并以节点方式选择尚未被占用的位置。例如，像这样的循环（其中所有值的序列预初始化为 -1）。

for(int i = 1; i <= count; ++i) {
  int nondet;
  assume(nondet >= 0 && nondet < count);
  // ensure we don't pick a spot already picked
  assume(sequence[nondet] == -1); 
  sequence[nondet] = i;
}

所以一个完整的程序应该是这样的：

#include <assert.h>
#include <memory.h>

int sum(int *array, int count) {
    int total = 0;
    for(int i = 0; i < count; ++i) {
        total += array[i];
    }
    return total;
}

int main(){

    int count = 5; // 1, ..., 6
    int *sequence = malloc(sizeof(int) * count);

    // this isn't working - not sure why, but constant propagator should
    // unroll the loop anyway
    // memset(sequence, -1, count);
    for(int i = 0; i < count; ++i) {
        sequence[i] = -1;
    }

    assert(sum(sequence, count) == -1 * count);

    for(int i = 1; i <= count; ++i) {
      int nondet;
      __CPROVER_assume(nondet >= 0);
      __CPROVER_assume(nondet < count);
      __CPROVER_assume(sequence[nondet] == -1); // ensure we don't pick a spot already picked
      sequence[nondet] = i;
    }

    int total = (count * (count + 1)) / 2;
    // verify this is a permuation
    assert(sum(sequence, count) == total);
}

但是，对于大于 6 的值，这非常慢（尽管我没有将它与您的方法进行比较 - 它不会卡在展开，它会卡在求解）。

【讨论】：