blob: 6852145acfe26d9147735856ffb4593ffc9fd0bf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
#!/bin/bash
# Simple pidgeon-hole problem generator in SMT-LIBv2
# (c) 2011 Morgan Deters <mdeters@cs.nyu.edu>
# 2011 July 7
if [ $# -ne 1 ]; then
echo "usage: $(basename "$0") size" >&2
exit 1
fi
N=$1
echo "(set-logic QF_UF)"
echo "(declare-sort U 0)"
i=1; while [ $i -le $N ]; do
echo "(declare-fun p_$i () U)"
let ++i
done
i=1; while [ $i -le $(($N-1)) ]; do
echo "(declare-fun h_$i () U)"
let ++i
done
i=1; while [ $i -le $(($N-1)) ]; do
j=$(($i+1)); while [ $j -le $N ]; do
echo "(assert (not (= p_$i p_$j)))"
let ++j
done
let ++i
done
i=1; while [ $i -le $N ]; do
echo -n "(assert (or"
j=1; while [ $j -le $(($N-1)) ]; do
echo -n " (= p_$i h_$j)"
let ++j
done
echo "))"
let ++i
done
echo "(check-sat)"
|
