Add a simple script to convert sygus v1 files to v2. (#4409)

diff --git a/contrib/sygus-v1-to-v2.sh b/contrib/sygus-v1-to-v2.sh
new file mode 100644 (file)
index 0000000..efc77f2
--- /dev/null
+++ b/contrib/sygus-v1-to-v2.sh
@@ -0,0 +1,60 @@
+#!/bin/bash
+# This is a simple script for converting v1 sygus files to v2.
+
+# Show how to use the script
+if [[ "$#" < 2 || ! -f "$1" || ! -e "$2" ]]; then
+    echo "Usage: $0 [<path to cvc4>] [<path to dir/file>] [--replace?] [<cvc4 options>*]"
+    exit 1
+fi
+
+# Find cvc4 options
+if [[ "$3" == "--replace" ]]; then
+    cvc4Ops="${@:4}"
+else
+    cvc4Ops="${@:3}"
+fi
+
+# Remove old v2 sygus files generated by the script
+find "$2" -name "*_v2.sy" -type f | xargs rm
+
+# Find v1 sygus files
+v1Files=$(find "$2" -name "*.sy" -type f)
+v1FilesCount=$(echo "$v1Files" | wc -l)
+
+# Convert v1 files to v2. The new ones end with "_v2.sy"
+while read -r v1File
+do
+    echo "Converting $v1File"
+    v2File=${v1File/.sy/_v2.sy}
+    "$1" $v1File --lang=sygus --dump-to=$v2File --output-lang=sygus2 --dump=raw-benchmark --preprocess-only $cvc4Ops 1> /dev/null
+    # Remove incremental and produce-models options
+    sed -i '/(set-option :incremental false)/d' $v2File
+    sed -i '/(set-option :produce-models "true")/d' $v2File
+done <<< "$v1Files"
+
+# Find and count the number of v2 files generated successfully
+if [[ -f "$2" ]]; then
+    v2Files=$(echo "${2/.sy/_v2.sy}")
+else
+    v2Files=$(find "$2" -name "*_v2.sy" -type f)
+fi
+
+v2Files=$(echo "$v2Files" | xargs grep -l "(check-synth)")
+
+if [[ $v2Files == "" ]]; then
+    v2FilesCount=0
+else
+    v2FilesCount=$(echo "$v2Files" | wc -l)
+fi
+
+# Replace the old v1 files with the new ones if script is called with --replace
+if [[ "$3" == "--replace" ]]; then
+    while read -r v2File
+    do
+        file=${v2File/_v2.sy/.sy}
+        mv $v2File $file
+    done <<< "$v2Files"
+fi
+
+# Converted successfully here means the v2 file contains "(check-synth)".
+echo "$v2FilesCount out of $v1FilesCount sygus files were converted successfully."