#!/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."