diff --git a/flake.nix b/flake.nix index 9b2189c..4e74284 100644 --- a/flake.nix +++ b/flake.nix @@ -168,10 +168,32 @@ }); }; - packages = + packages = let + validate = pkgs.writeShellApplication { + name = "validate"; + runtimeInputs = [ + aba2sat + aspforaba + pkgs.coreutils + pkgs.hyperfine + pkgs.jq + ]; + text = builtins.readFile ./scripts/validate.sh; + }; + + sc-batch = pkgs.writeShellApplication { + name = "sc-batch"; + runtimeInputs = [ + validate + ]; + text = builtins.readFile ./scripts/sc-batch.sh; + }; + + aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix {inherit (self'.packages) clingo;}; + in { + inherit validate aba2sat aspforaba sc-batch; default = aba2sat; - aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix {inherit (self'.packages) clingo;}; clingo = pkgs.callPackage ./nix/packages/clingo.nix {}; } // lib.optionalAttrs (!pkgs.stdenv.isDarwin) { diff --git a/scripts/sc-batch.sh b/scripts/sc-batch.sh new file mode 100755 index 0000000..9ac2c32 --- /dev/null +++ b/scripts/sc-batch.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +# Batch script to run on sc.uni-leipzig.de cluster, i used +# sbatch -a "1-$(cat acyclic.list | wc -l)" ./scripts/sc-batch.sh + +FILE_LIST=acyclic.list + +file="$(pwd)/$(awk "NR == $SLURM_ARRAY_TASK_ID" "$FILE_LIST")" +arg=$(cat "$file.asm") + +OUTPUT_DIR="$(pwd)/output" + +export OUTPUT_DIR +./validate --file "$file" --arg "$arg" --time --problem dc-co diff --git a/scripts/validate.sh b/scripts/validate.sh index f830e1f..b4c7f40 100755 --- a/scripts/validate.sh +++ b/scripts/validate.sh @@ -1,5 +1,8 @@ #!/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" @@ -70,7 +73,7 @@ run_dc_co() { POSITIONAL_ARGS=() ASPFORABA=ASPforABA -ABA2SAT=result/bin/aba2sat +ABA2SAT=aba2sat ABA_FILE= ABA_FILE_DIR= ABA_FILE_EXT=aba