From 0cb97f705ffe44e126a9d521279c60f9a7b85360 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 16 Jun 2020 17:32:38 -0500
Subject: [PATCH] Simplify sygus conversion script. (#4627)

---
 contrib/sygus-v1-to-v2.sh | 61 +++++++--------------------------------
 1 file changed, 11 insertions(+), 50 deletions(-)
 mode change 100644 => 100755 contrib/sygus-v1-to-v2.sh

diff --git a/contrib/sygus-v1-to-v2.sh b/contrib/sygus-v1-to-v2.sh
old mode 100644
new mode 100755
index efc77f256..0d1ac17e4
--- a/contrib/sygus-v1-to-v2.sh
+++ b/contrib/sygus-v1-to-v2.sh
@@ -2,59 +2,20 @@
 # 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
+if [[ "$#" < 3 || ! -f "$1" || ! -f "$2" ]]; then
+  echo "Usage: $0 [<path to cvc4>] [<path to sygus file>] [<path to output file>] [<additional 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
+output=$("$1" "$2" --lang=sygus1 --dump-to="$3" --output-lang=sygus2 --dump=raw-benchmark --preprocess-only "${@:4}" 2>&1)
 
-# Find v1 sygus files
-v1Files=$(find "$2" -name "*.sy" -type f)
-v1FilesCount=$(echo "$v1Files" | wc -l)
+exitCode=$?
 
-# 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}")
+if [[ "$exitCode" == 0 ]]; then
+  # Remove incremental and produce-models options
+  sed -i '/(set-option :incremental false)/d' "$3"
+  sed -i '/(set-option :produce-models "true")/d' "$3"
 else
-    v2Files=$(find "$2" -name "*_v2.sy" -type f)
+  echo "$1 failed with exit code $exitCode:"
+  echo "$output"
 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."
-- 
2.30.2