diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /test/regress/regress0/uf/mkpidgeon | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'test/regress/regress0/uf/mkpidgeon')
-rwxr-xr-x | test/regress/regress0/uf/mkpidgeon | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/mkpidgeon b/test/regress/regress0/uf/mkpidgeon new file mode 100755 index 000000000..6852145ac --- /dev/null +++ b/test/regress/regress0/uf/mkpidgeon @@ -0,0 +1,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)" |