From b8d5a748fcd6bc550ef2ea92b129c77bae717773 Mon Sep 17 00:00:00 2001
From: Pamina Georgiou <gpamina@amazon.com>
Date: Thu, 22 Oct 2020 17:51:53 +0200
Subject: [PATCH 1/2] batch convert from smt2 to sygus

---
 .../chc-comp/batch-convert-to-sygus.sh        | 82 +++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100755 work-in-progress/chc-comp/batch-convert-to-sygus.sh

diff --git a/work-in-progress/chc-comp/batch-convert-to-sygus.sh b/work-in-progress/chc-comp/batch-convert-to-sygus.sh
new file mode 100755
index 0000000..3d34c4b
--- /dev/null
+++ b/work-in-progress/chc-comp/batch-convert-to-sygus.sh
@@ -0,0 +1,82 @@
+#!/usr/bin/env bash
+
+set -Euo pipefail
+
+if (( ${BASH_VERSION%%.*} < 4 )); then echo "ERROR: [bash] version 4.0+ required!" ; exit -1 ; fi
+
+USER_DIR="$(pwd)"
+ROOT_DIR="$(cd -P -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd -P)/.."
+
+SYGUS_EXTENSION="sl"
+SMT_EXTENSION="smt2"
+SOURCE_SYGUS_STANDARD="1"
+TARGET_SYGUS_STANDARD="2"
+
+IS_VERBOSE=""
+DO_COLLECT_ERRORS=""
+OUTPUT_DIR=""
+INTERNAL_OPTIONS=""
+
+usage() {
+  if [ -n "$1" ]; then echo -e "\nERROR: $1" >&2 ; fi
+  echo -en "
+Usage: $0 [flags] -o <dir> <dir>
+
+Parameters:
+    [--output-dir, -o]          The output directory for converted files
+
+Flags:
+    [--verbose, -v]             Increase output verbosity (list PASSsed files too)
+" 1>&2 ; exit 1
+}
+
+for opt in "$@"; do
+  shift
+  case "$opt" in
+    "--output-dir")         set -- "$@" "-o" ;;
+    "--verbose")            set -- "$@" "-v" ;;
+    "--")             set -- "$@" "--" ;;
+    "--"*)            usage "Unrecognized option: $opt." ;;
+    *)                set -- "$@" "$opt"
+  esac
+done
+
+OPTIND=1
+while getopts ':e:I:o:s:t:v' OPTION ; do
+  case "$OPTION" in
+    "o" ) OUTPUT_DIR="$OPTARG"
+          ;;
+    "v" ) IS_VERBOSE="yes"
+          ;;
+      * ) usage "Unrecognized option: -$OPTARG." ;;
+  esac
+done
+shift $(($OPTIND -1))
+
+[ -n "$OUTPUT_DIR" ] || usage "Missing required parameter: --output-dir | -o <dir>."
+OUTPUT_DIR="$(realpath $USER_DIR/$OUTPUT_DIR)"
+mkdir -p "$OUTPUT_DIR" || usage "Could not locate or create output directory: $OUTPUT_DIR."
+
+[ "$#" -eq "1" ] || usage "This script accepts exactly 1 input directory ($# provided)."
+[ -d "$1" ] || usage "Could not locate source directory: $1."
+SRC_DIR="$(realpath $USER_DIR/$1)"
+
+cd "$ROOT_DIR"
+for FILE in $(find "$SRC_DIR" -name *".$SMT_EXTENSION" | sort) ; do
+    FILE_REL_PATH="${FILE#$SRC_DIR/}"
+    OUTPUT_REL_PATH=${FILE_REL_PATH%.*}.$SYGUS_EXTENSION
+    echo $OUTPUT_REL_PATH
+    mkdir -p "$OUTPUT_DIR/$(dirname $OUTPUT_REL_PATH$)"
+
+    python3 -m chc-comp.to-sygus  \
+            "$FILE"                                                     \
+            2> "$OUTPUT_DIR/$OUTPUT_REL_PATH.err" > "$OUTPUT_DIR/$OUTPUT_REL_PATH"
+
+    if [ "$?" -eq "0" ]; then
+        rm -rf "$OUTPUT_DIR/$OUTPUT_REL_PATH.err"
+        [ "$IS_VERBOSE" == "yes" ] && echo "  [PASS]  $OUTPUT_REL_PATH"
+    else
+        rm -rf "$OUTPUT_DIR/$OUTPUT_REL_PATH"
+        echo "  [FAIL]  $OUTPUT_REL_PATH"
+    fi
+done

From 0e02153731711c79642d916c343ce8a8c3f82f25 Mon Sep 17 00:00:00 2001
From: Pamina Georgiou <gpamina@amazon.com>
Date: Fri, 23 Oct 2020 11:00:42 +0200
Subject: [PATCH 2/2] minor refactoring

---
 .../batch-translate-from-smt.sh                      | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)
 rename work-in-progress/chc-comp/batch-convert-to-sygus.sh => scripts/batch-translate-from-smt.sh (89%)

diff --git a/work-in-progress/chc-comp/batch-convert-to-sygus.sh b/scripts/batch-translate-from-smt.sh
similarity index 89%
rename from work-in-progress/chc-comp/batch-convert-to-sygus.sh
rename to scripts/batch-translate-from-smt.sh
index 3d34c4b..7d2b44a 100755
--- a/work-in-progress/chc-comp/batch-convert-to-sygus.sh
+++ b/scripts/batch-translate-from-smt.sh
@@ -9,8 +9,6 @@ ROOT_DIR="$(cd -P -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd -P)/.."
 
 SYGUS_EXTENSION="sl"
 SMT_EXTENSION="smt2"
-SOURCE_SYGUS_STANDARD="1"
-TARGET_SYGUS_STANDARD="2"
 
 IS_VERBOSE=""
 DO_COLLECT_ERRORS=""
@@ -35,9 +33,10 @@ for opt in "$@"; do
   case "$opt" in
     "--output-dir")         set -- "$@" "-o" ;;
     "--verbose")            set -- "$@" "-v" ;;
-    "--")             set -- "$@" "--" ;;
-    "--"*)            usage "Unrecognized option: $opt." ;;
-    *)                set -- "$@" "$opt"
+
+    "--")                   set -- "$@" "--" ;;
+    "--"*)                  usage "Unrecognized option: $opt." ;;
+    *)                      set -- "$@" "$opt"
   esac
 done
 
@@ -65,10 +64,9 @@ cd "$ROOT_DIR"
 for FILE in $(find "$SRC_DIR" -name *".$SMT_EXTENSION" | sort) ; do
     FILE_REL_PATH="${FILE#$SRC_DIR/}"
     OUTPUT_REL_PATH=${FILE_REL_PATH%.*}.$SYGUS_EXTENSION
-    echo $OUTPUT_REL_PATH
     mkdir -p "$OUTPUT_DIR/$(dirname $OUTPUT_REL_PATH$)"
 
-    python3 -m chc-comp.to-sygus  \
+    python3 -m work-in-progress.chc-comp.to-sygus  \
             "$FILE"                                                     \
             2> "$OUTPUT_DIR/$OUTPUT_REL_PATH.err" > "$OUTPUT_DIR/$OUTPUT_REL_PATH"