diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-05-19 22:33:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-19 22:33:03 -0500 |
commit | 7b4084440bd9dde894ff46c2ba0197fed41d91d1 (patch) | |
tree | 48179d7c391b49b754af3e1a3df66067253fc093 /contrib | |
parent | af874a5c7a2ff134da0d4c20d06a0626d3e36d9b (diff) |
Add a simple script to convert sygus v1 files to v2. (#4409)
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/sygus-v1-to-v2.sh | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/contrib/sygus-v1-to-v2.sh b/contrib/sygus-v1-to-v2.sh new file mode 100644 index 000000000..efc77f256 --- /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." |