blob: efc77f2569b116a967435927760dc4dcab5bc1b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
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."
|
