aba2sat/scripts/validate.sh

#!/usr/bin/env bash

# Validate the correctness and optionally measure times of aba2sat and aspforaba
# best used through the bundled nix version `nix run .#validate`

print_help_and_exit() {
  if [ -n "$1" ]; then
    printf "%s\n\n" "$1"
  fi
  printf "Usage: validate [OPTIONS] \n"
  printf "\n"
  printf "Options:\n"
  printf "  --aspforaba EXE\n"
  printf "          Binary to use when calling aspforaba\n"
  printf "  -p, --problem\n"
  printf "          The problem to solve\n"
  printf "  -a, --arg\n"
  printf "          The additional argument for the problem\n"
  printf "  -f, --file\n"
  printf "          The file containing the problem in ABA format\n"
  printf "  -t, --time\n"
  printf "          Execute hyperfine to determine runtimes\n"
  printf "  --files-from\n"
  printf "          Use the following dir to read files, specify a single file with --file instead\n"
  printf "  --aba2sat EXE\n"
  printf "          Binary to use when calling aba2sat\n"
  printf "  --max-loops NUM (Default: 0)\n"
  printf "          Set the maximum number of loops aba2sat should try to fix\n"
  exit 1
}

format_time() {
  COMMAND="$1"
  FILE="$2"
  mean=$(jq ".results[]   | select(.command == \"$COMMAND\") | (.mean   * 1000)" "$FILE")
  stddev=$(jq ".results[] | select(.command == \"$COMMAND\") | (.stddev * 1000)" "$FILE")
  printf "%7.3f±%7.3fms" "$mean" "$stddev"
}

run_dc_co() {
  OUTPUT_DIR=${OUTPUT_DIR:-$(mktemp -d)}
  mkdir -p "$OUTPUT_DIR"
  JSON_FILE="$OUTPUT_DIR/$(basename "$ABA_FILE")-hyperfine.json"
  # Restrict memory to 20GB
  ulimit -v 20000000
  if [ -z "$ADDITIONAL_ARG" ]; then
    print_help_and_exit "Parameter --arg is missing!"
  fi
  if [ -z "$ABA_FILE" ]; then
    print_help_and_exit "Parameter --file is missing!"
  fi
  printf "===== %s ==== " "$(basename "$ABA_FILE")"
  our_result=$("$ABA2SAT" --max-loops "$MAX_LOOPS" --file "$ABA_FILE" dc-co --query "$ADDITIONAL_ARG" | tee "$OUTPUT_DIR/$(basename "$ABA_FILE")-aba2sat-result")
  other_result=$("$ASPFORABA" --file "$ABA_FILE" --problem DC-CO --query "$ADDITIONAL_ARG" | tee "$OUTPUT_DIR/$(basename "$ABA_FILE")-aspforaba-result")
  if [ "$our_result" != "$other_result" ]; then
    printf "❌\n"
  else
    printf "✅\n"
  fi
  printf "Argument: %s\n" "$ADDITIONAL_ARG"

  if [ -n "$TIME_COMMANDS" ]; then
    $HYPERFINE --shell=none \
      --export-json "$JSON_FILE" \
      --command-name "aba2sat" \
      "$ABA2SAT --max-loops \"$MAX_LOOPS\" --file \"$ABA_FILE\" dc-co --query \"$ADDITIONAL_ARG\"" \
      --command-name "aspforaba" \
      "$ASPFORABA --file \"$ABA_FILE\" --problem DC-CO --query \"$ADDITIONAL_ARG\"" 1>/dev/null 2>&1
    printf "Our:      %3s %30s\n" "$our_result" "$(format_time "aba2sat" "$JSON_FILE")"
    printf "Their:    %3s %30s\n" "$other_result" "$(format_time "aspforaba" "$JSON_FILE")"
  else
    printf "Our:      %3s\n" "$our_result"
    printf "Their:    %3s\n" "$other_result"
  fi

}

POSITIONAL_ARGS=()
ASPFORABA=ASPforABA
ABA2SAT=aba2sat
ABA_FILE=
ABA_FILE_DIR=
ABA_FILE_EXT=aba
HYPERFINE=hyperfine
MAX_LOOPS=0
PROBLEM=
ADDITIONAL_ARG=
TIME_COMMANDS=

while [[ $# -gt 0 ]]; do
  case $1 in
  -h | --help)
    print_help_and_exit ""
    ;;
  --aspforaba)
    shift
    ASPFORABA=$1
    shift
    ;;
  -p | --problem)
    shift
    PROBLEM=$1
    shift
    ;;
  -f | --file)
    if [ -n "$ABA_FILE_DIR" ]; then
      print_help_and_exit "Parameters --file and --files-from cannot be mixed"
    fi
    shift
    ABA_FILE=$1
    shift
    ;;
  --files-from)
    if [ -n "$ABA_FILE" ]; then
      print_help_and_exit "Parameters --file and --files-from cannot be mixed"
    fi
    if [ -n "$ADDITIONAL_ARG" ]; then
      print_help_and_exit "Parameters --arg and --files-from cannot be mixed"
    fi
    shift
    ABA_FILE_DIR=$1
    shift
    ;;
  -a | --arg)
    if [ -n "$ABA_FILE_DIR" ]; then
      print_help_and_exit "Parameters --arg and --files-from cannot be mixed"
    fi
    shift
    ADDITIONAL_ARG=$1
    shift
    ;;
  -t | --time)
    shift
    TIME_COMMANDS=yes
    ;;
  --aba2sat)
    shift
    ABA2SAT=$1
    shift
    ;;
  --max-loops)
    shift
    echo "MAX LOOPS $1"
    MAX_LOOPS=$1
    shift
    ;;
  -*)
    echo "Unknown option $1"
    print_help_and_exit
    ;;
  *)
    POSITIONAL_ARGS+=("$1") # save positional arg
    shift                   # past argument
    ;;
  esac
done

set -- "${POSITIONAL_ARGS[@]}" # restore positional parameters

case "$PROBLEM" in
dc-co | DC-CO)
  if [ -n "$ABA_FILE_DIR" ]; then
    # run for every file found in the directory
    for file in $(find "$ABA_FILE_DIR" -type f -iname "*.$ABA_FILE_EXT" | shuf); do
      ABA_FILE="$file" ADDITIONAL_ARG="$(cat "$file.asm")" run_dc_co
    done
  else
    # run for the single configured file
    run_dc_co
  fi
  ;;
*)
  print_help_and_exit "Problem $PROBLEM is not supported"
  ;;
esac