Как получить все перестановки в CBMC?

Question

Я пытаюсь получить все перестановки массива в 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

Но с более крупными элементами код будет очень запутанным. Итак, мой вопрос: есть ли лучший / общий способ выразить это?

Answer 1

Основываясь на предложении Крейга об использовании массива, вы можете перебрать значения, которые хотите переставить, и определенным образом выбрать место, которое еще не было занято. Например, такой цикл (где последовательность предварительно инициализируется -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 (хотя я не сравнивал это с вашим подходом - он не застревает при раскручивании, он застревает в решении).