Skip to content

Instantly share code, notes, and snippets.

@Mr-Slippery
Created November 19, 2020 17:15
Show Gist options
  • Save Mr-Slippery/6618c833b048a00664b80b7d4fef5c74 to your computer and use it in GitHub Desktop.
Save Mr-Slippery/6618c833b048a00664b80b7d4fef5c74 to your computer and use it in GitHub Desktop.
Solving 8-queens with KLEE
#include <klee/klee.h>
#include <assert.h>
#define N 8
unsigned char queens[N];
int abs(int x)
{
return x >= 0 ? x: -x;
}
int attack()
{
int i, j;
for (i = 0; i < N; i++) {
for (j = i + 1; j < N; j++) {
if ((queens[i] == queens[j]) ||
(abs(queens[i] - queens[j]) == j - i)) {
return 1;
}
}
}
return 0;
}
int main(int argc, char *argv[])
{
int i;
klee_make_symbolic(&queens[0], sizeof(unsigned char) * N, "queens");
for (i = 0; i < N; i++) {
queens[i] %= N;
}
klee_assert(attack());
return 0;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment