merge from symmetry branch

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)"