Properly delete old files when generating logs, improve z3 scripts

smt2/make_log.sh

@@ -1,31 +1,13 @@
-Z3_VERSION=$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')
-Z3_VERSION_REGEX="${Z3_VERSION//./\\.}"
+export Z3_VERSION=${Z3_VERSION:-$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')}
+DIRNAME="$(realpath "$(dirname "$0")")"
 
-cd "${1-$(dirname $0)}"
-while read -r file; do
-    # Check if the first line contains my Z3 version (and skip if it does)
-    [ "$(sed -n '/^;[^\n]*$Z3_VERSION_REGEX/p;q' "$file")" ] && echo "Skipping \"$file\" as the first line contains \"$Z3_VERSION\"" && continue || true
-
-    # Check if the (non-empty) log file exists
-    file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1)
-    base_name="../logs/${file%.*}"
-    log_file_name="$base_name-fHash-$file_hash.log"
-    test -s "$log_file_name" && echo "Skipping \"$file\" as \"$file_hash\" exists" && continue || true
+if [ -z "$1" ]; then
+    mkdir -p "$DIRNAME/../logs"
+    cd "$DIRNAME/../logs"
+else
+    cd "$1"
+fi
 
-    # Remove old logs
-    rm -f "$base_name-fHash-*.log"
-    mkdir -p $(dirname "$log_file_name")
-
-    echo "[.log] $file"
-    # Run Z3 solver for the file and save the log in the '../logs' directory.
-    # The memory limit is set to 15.5GB and the timeout is set to 10 seconds
-    # (this limits the log file size to roughly <=0.5GB). We redirect
-    # the output so that it doesn't get printed and listen for a
-    # timeout message in which case we remove the last line of the log
-    # file since it may be incomplete (and cause parsing errors).
-    output=$(z3 trace=true proof=true -memory:15872 -T:10 trace-file-name=$log_file_name "./$file")
-    echo "$output" | grep -q "timeout" || continue
-    echo "[Timeout] Removing last line of logfile"
-    tail -n 1 "$log_file_name" | wc -c | xargs -I {} truncate -s -{} "$log_file_name"
-    test -s "$log_file_name" || echo "!!! Log file not created for \"$file\""
-done <<<  "$(find . -name "*.smt2" -type f)"
+while read -r file; do
+    "$DIRNAME/z3.sh" "$file"
+done <<< "$(find "$DIRNAME" -name "*.smt2" -type f)"

smt2/z3.sh

@@ -0,0 +1,37 @@
+Z3_VERSION=${Z3_VERSION:-$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')}
+Z3_VERSION_REGEX="${Z3_VERSION//./\\.}"
+
+file_relative="${1#"$(dirname "$0")/"}"
+# Check if the first line contains my Z3 version (and skip if it does)
+[ "$(sed -n '/^;[^\n]*$Z3_VERSION_REGEX/p;q' "$1")" ] && echo "Skipping \"$file_relative\" as the first line contains \"$Z3_VERSION\"" && exit 0 || true
+
+# Check if the (non-empty) log file exists
+file_hash=$(shasum -a 256 "$0" | cut -d' ' -f1)
+base_name="${file_relative%.*}"
+log_file_name="$base_name-fHash-$file_hash.log"
+log_file_dir=$(dirname "$log_file_name")
+mkdir -p $log_file_dir
+
+# Find files with different hash
+old_files=$(find $log_file_dir -name "$(basename "$base_name")-fHash-*.log" -maxdepth 1 -type f)
+while read -r old_file; do
+    [ -n "$old_file" ] || continue
+    [ "$old_file" = "$log_file_name" ] && continue
+    echo "Rm old \"$(basename "$old_file")\""
+    # Remove old log
+    rm -f "$old_file"
+done <<< "$old_files"
+test -s "$log_file_name" && echo "Skipping \"$file_relative\" as \"$file_hash\" exists" && exit 0 || true
+
+echo "[.log] $file_relative"
+# Run Z3 solver for the file and save the log in the '../logs' directory.
+# The memory limit is set to 15.5GB and the timeout is set to 10 seconds
+# (this limits the log file size to roughly <=0.5GB). We redirect
+# the output so that it doesn't get printed and listen for a
+# timeout message in which case we remove the last line of the log
+# file since it may be incomplete (and cause parsing errors).
+output=$(z3 trace=true proof=true -memory:15872 -T:10 trace-file-name=$log_file_name "$1" 2>&1)
+echo "$output" | grep -q "timeout" || exit 0
+echo "[Timeout] Removing last line of logfile"
+tail -n 1 "$log_file_name" | wc -c | xargs -I {} truncate -s -{} "$log_file_name"
+test -s "$log_file_name" || echo "!!! Log file not created for \"$file_relative\""