From 06641ddc8023dd36db27eeac2a842b3ba1ff3ddf Mon Sep 17 00:00:00 2001 From: Malte Tammena Date: Tue, 18 Jun 2024 08:41:09 +0200 Subject: [PATCH] scripting and tweaking --- flake.nix | 357 ++++++++++++----------- scripts/aba-generator-acyclic.py | 174 +++++++++++ scripts/aba_generator_acyclic.py | 100 ------- scripts/aba_generator_acyclic_starter.sh | 6 + scripts/decode-result-folder.py | 13 +- scripts/run-gen.sh | 6 + 6 files changed, 382 insertions(+), 274 deletions(-) create mode 100755 scripts/aba-generator-acyclic.py delete mode 100755 scripts/aba_generator_acyclic.py create mode 100755 scripts/aba_generator_acyclic_starter.sh create mode 100755 scripts/run-gen.sh diff --git a/flake.nix b/flake.nix index 589b665..aabbb97 100644 --- a/flake.nix +++ b/flake.nix @@ -30,17 +30,18 @@ }; }; - outputs = inputs @ { - self, - nixpkgs, - flake-parts, - crane, - fenix, - flake-utils, - advisory-db, - rust-overlay, - }: - flake-parts.lib.mkFlake {inherit inputs self;} { + outputs = + inputs @ { self + , nixpkgs + , flake-parts + , crane + , fenix + , flake-utils + , advisory-db + , rust-overlay + , + }: + flake-parts.lib.mkFlake { inherit inputs self; } { imports = [ ]; @@ -52,196 +53,214 @@ flake.hydraJobs.devShells.x86_64-linux = self.devShells.x86_64-linux; flake.hydraJobs.checks.x86_64-linux = self.checks.x86_64-linux; - perSystem = { - self', - pkgs, - lib, - config, - system, - ... - }: let - # Load toolchain from file and extend with rust-src and rust-analyzer + clippy - rustToolchain = (pkgs.rust-bin.fromRustupToolchainFile (self + /rust-toolchain.toml)).override { - extensions = [ - "rust-src" - "rust-analyzer" - "clippy" - ]; - }; - - # NB: we don't need to overlay our custom toolchain for the *entire* - # pkgs (which would require rebuidling anything else which uses rust). - # Instead, we just want to update the scope that crane will use by appending - # our specific toolchain there. - craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain; - - src = craneLib.cleanCargoSource (craneLib.path ./.); - - # Common arguments can be set here to avoid repeating them later - commonArgs = { - inherit src; - strictDeps = true; - - buildInputs = - [ - # Add additional build inputs here - ] - ++ lib.optionals pkgs.stdenv.isDarwin [ - # Additional darwin specific inputs can be set here - pkgs.libiconv + perSystem = + { self' + , pkgs + , lib + , config + , system + , ... + }: + let + # Load toolchain from file and extend with rust-src and rust-analyzer + clippy + rustToolchain = (pkgs.rust-bin.fromRustupToolchainFile (self + /rust-toolchain.toml)).override { + extensions = [ + "rust-src" + "rust-analyzer" + "clippy" ]; + }; - # Additional environment variables can be set directly - # MY_CUSTOM_VAR = "some value"; - }; + # NB: we don't need to overlay our custom toolchain for the *entire* + # pkgs (which would require rebuidling anything else which uses rust). + # Instead, we just want to update the scope that crane will use by appending + # our specific toolchain there. + craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain; - craneLibLLvmTools = - craneLib.overrideToolchain - (fenix.packages.${system}.complete.withComponents [ - "cargo" - "llvm-tools" - "rustc" - ]); + src = craneLib.cleanCargoSource (craneLib.path ./.); - # Build *just* the cargo dependencies, so we can reuse - # all of that work (e.g. via cachix) when running in CI - cargoArtifacts = craneLib.buildDepsOnly commonArgs; + # Common arguments can be set here to avoid repeating them later + commonArgs = { + inherit src; + strictDeps = true; - # Build the actual crate itself, reusing the dependency - # artifacts from above. - aba2sat = craneLib.buildPackage (commonArgs - // { + buildInputs = + [ + # Add additional build inputs here + ] + ++ lib.optionals pkgs.stdenv.isDarwin [ + # Additional darwin specific inputs can be set here + pkgs.libiconv + ]; + + # Additional environment variables can be set directly + # MY_CUSTOM_VAR = "some value"; + }; + + craneLibLLvmTools = + craneLib.overrideToolchain + (fenix.packages.${system}.complete.withComponents [ + "cargo" + "llvm-tools" + "rustc" + ]); + + # Build *just* the cargo dependencies, so we can reuse + # all of that work (e.g. via cachix) when running in CI + cargoArtifacts = craneLib.buildDepsOnly commonArgs; + + # Build the actual crate itself, reusing the dependency + # artifacts from above. + aba2sat = craneLib.buildPackage (commonArgs + // { inherit cargoArtifacts; }); - in { - _module.args.pkgs = import nixpkgs { - inherit system; - overlays = [ - (import rust-overlay) - ]; - }; + in + { + _module.args.pkgs = import nixpkgs { + inherit system; + overlays = [ + (import rust-overlay) + ]; + }; - checks = { - # Build the crate as part of `nix flake check` for convenience - inherit aba2sat; + checks = { + # Build the crate as part of `nix flake check` for convenience + inherit aba2sat; - # Run clippy (and deny all warnings) on the crate source, - # again, reusing the dependency artifacts from above. - # - # Note that this is done as a separate derivation so that - # we can block the CI if there are issues here, but not - # prevent downstream consumers from building our crate by itself. - aba2sat-clippy = craneLib.cargoClippy (commonArgs - // { + # Run clippy (and deny all warnings) on the crate source, + # again, reusing the dependency artifacts from above. + # + # Note that this is done as a separate derivation so that + # we can block the CI if there are issues here, but not + # prevent downstream consumers from building our crate by itself. + aba2sat-clippy = craneLib.cargoClippy (commonArgs + // { inherit cargoArtifacts; cargoClippyExtraArgs = "--all-targets -- --deny warnings"; }); - aba2sat-doc = craneLib.cargoDoc (commonArgs - // { + aba2sat-doc = craneLib.cargoDoc (commonArgs + // { inherit cargoArtifacts; }); - # Check formatting - aba2sat-fmt = craneLib.cargoFmt { - inherit src; - }; + # Check formatting + aba2sat-fmt = craneLib.cargoFmt { + inherit src; + }; - # Audit dependencies - aba2sat-audit = craneLib.cargoAudit { - inherit src advisory-db; - }; + # Audit dependencies + aba2sat-audit = craneLib.cargoAudit { + inherit src advisory-db; + }; - # Audit licenses - aba2sat-deny = crane.lib.${system}.cargoDeny { - inherit src; - }; + # Audit licenses + aba2sat-deny = crane.lib.${system}.cargoDeny { + inherit src; + }; - # Run tests with cargo-nextest - # Consider setting `doCheck = false` on `aba2sat` if you do not want - # the tests to run twice - aba2sat-nextest = craneLib.cargoNextest (commonArgs - // { + # Run tests with cargo-nextest + # Consider setting `doCheck = false` on `aba2sat` if you do not want + # the tests to run twice + aba2sat-nextest = craneLib.cargoNextest (commonArgs + // { inherit cargoArtifacts; partitions = 1; partitionType = "count"; }); - }; - - 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; - }; + packages = + let + validate = pkgs.writeShellApplication { + name = "validate"; + runtimeInputs = [ + aba2sat + aspforaba + pkgs.coreutils + pkgs.hyperfine + pkgs.jq + ]; + text = builtins.readFile ./scripts/validate.sh; + }; - decode-result-folder = pkgs.writeShellApplication { - name = "decode-result-folder"; - runtimeInputs = [ - pkgs.python3 - ]; - text = '' - python3 ${./scripts/decode-result-folder.py} - ''; - }; + 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 decode-result-folder; - default = aba2sat; - clingo = pkgs.callPackage ./nix/packages/clingo.nix {}; - } - // lib.optionalAttrs (!pkgs.stdenv.isDarwin) { - aba2sat-llvm-coverage = craneLibLLvmTools.cargoLlvmCov (commonArgs + decode-result-folder = pkgs.python3.pkgs.buildPythonApplication { + name = "decode-result-folder"; + version = "0.0.1"; + src = lib.sourceByRegex ./. [ "scripts" "scripts/decode-result-folder.py" ]; + format = "other"; + installPhase = '' + mkdir -p $out/bin + cp scripts/decode-result-folder.py $out/bin/decode-result-folder + chmod +x $out/bin/decode-result-folder + ''; + }; + + aba-generator-acyclic = pkgs.python3.pkgs.buildPythonApplication { + name = "aba-generator-acyclic"; + version = "0.0.1"; + src = lib.sourceByRegex ./. [ "scripts" "scripts/aba-generator-acyclic.py" ]; + format = "other"; + installPhase = '' + mkdir -p $out/bin + cp scripts/aba-generator-acyclic.py $out/bin/aba-generator-acyclic + chmod +x $out/bin/aba-generator-acyclic + ''; + }; + + aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix { inherit (self'.packages) clingo; }; + in + { + inherit validate aba2sat aspforaba sc-batch decode-result-folder aba-generator-acyclic; + default = aba2sat; + clingo = pkgs.callPackage ./nix/packages/clingo.nix { }; + } + // lib.optionalAttrs (!pkgs.stdenv.isDarwin) { + aba2sat-llvm-coverage = craneLibLLvmTools.cargoLlvmCov (commonArgs // { inherit cargoArtifacts; }); + }; + + apps.default = flake-utils.lib.mkApp { + drv = aba2sat; }; - apps.default = flake-utils.lib.mkApp { - drv = aba2sat; + devShells.default = + let + python = pkgs.python3.withPackages (ps: [ ps.torch ps.torchvision ps.psutil ps.pandas ps.matplotlib ps.seaborn ]); + in + craneLib.devShell { + # Inherit inputs from checks. + checks = self.checks.${system}; + + RUST_LOG = "trace"; + + inputsFrom = [ ]; + + packages = [ + pkgs.hyperfine + pkgs.lldb + pkgs.nil + pkgs.nodejs + pkgs.pre-commit + pkgs.pyright + pkgs.ruff-lsp + pkgs.shellcheck + pkgs.shfmt + python + self'.packages.aspforaba + ]; + }; }; - - devShells.default = let - python = pkgs.python3.withPackages (ps: [ps.torch ps.torchvision ps.psutil ps.pandas ps.matplotlib ps.seaborn]); - in - craneLib.devShell { - # Inherit inputs from checks. - checks = self.checks.${system}; - - RUST_LOG = "trace"; - - inputsFrom = []; - - packages = [ - pkgs.hyperfine - pkgs.lldb - pkgs.nil - pkgs.nodejs - pkgs.pre-commit - pkgs.pyright - pkgs.ruff-lsp - pkgs.shellcheck - pkgs.shfmt - python - self'.packages.aspforaba - ]; - }; - }; }; } diff --git a/scripts/aba-generator-acyclic.py b/scripts/aba-generator-acyclic.py new file mode 100755 index 0000000..ae6363b --- /dev/null +++ b/scripts/aba-generator-acyclic.py @@ -0,0 +1,174 @@ +#!/usr/bin/env python3 + +import argparse +import random +import os +import concurrent.futures + + +def create_framework( + n_sentences, n_assumptions, n_rules_per_head, size_of_bodies, cycle_prob +): + """ + Create a random framework. + + sentences contains the non-assumption sentences. + n_rules_per_head should be a list exhausting the possible number of rules each head can have + size_of_bodies should be a list exhausting the possible number of sentences in any rule body + These should hold in order to get non-counterintuitive results: + - n_assumptions < n_sentences + - max(size_of_bodies) <= n_sentences+n_assumptions + """ + + assumptions = [str(i) for i in range(1, n_assumptions + 1)] + sentences = [str(i) for i in range(n_assumptions + 1, n_sentences + 1)] + + contraries = { + asmpt: random.choice(sentences + assumptions) for asmpt in assumptions + } + + # order sentences to avoid cycles + random.shuffle(sentences) + rules = [] + for i, head in enumerate(sentences): + n_rules_in_this_head = random.choice(n_rules_per_head) + for _ in range(n_rules_in_this_head): + size_of_body = random.choice(size_of_bodies) + + # only allow stuff to occur in body if it is lower in the (topological) order + n_available = len(assumptions) + i + + selection_set = assumptions + sentences[:i] + # add potentially cycle creating sentences to the selection set with a given probability + extra_selection = random.sample( + sentences[i:], min(len(sentences[i:]), int(cycle_prob * len(sentences))) + ) + selection_set.extend(extra_selection) + + # body = random.sample(assumptions+sentences[:i], min(size_of_body, n_available)) + body = random.sample( + assumptions + selection_set, min(size_of_body, n_available) + ) + rules.append((head, body)) + + return assumptions, sentences, contraries, rules + + +def print_ICCMA_format(assumptions, contraries, rules, n_sentences, out_filename): + """ + Print the given framework in the ICCMA 2023 format. + """ + offset = len(assumptions) + + with open(out_filename, "w") as out: + out.write(f"p aba {n_sentences}\n") + for i, asm in enumerate(assumptions): + out.write(f"a {asm}\n") + # print(f"a {asm}") + for ctr in contraries: + out.write(f"c {ctr} {contraries.get(ctr)}\n") + # print(f"c {ctr} {contraries.get(ctr)}") + for rule in rules: + out.write(f"r {rule[0]} {' '.join(rule[1])}\n") + # print(f"r {rule[0]} {' '.join(rule[1])}") + + +def generate_configs( + sentences, + max_rules_per_head_list, + max_rule_size_list, + assumption_ratios, + cycle_props, + count, + directory, + identifier, +): + for sentence in sentences: + for assumption_ratio in assumption_ratios: + for max_rules_per_head in max_rules_per_head_list: + for max_rule_size in max_rule_size_list: + for cycle_prop in cycle_props: + for i in range(count): + yield { + "sentence": sentence, + "assumption_ratio": assumption_ratio, + "max_rules_per_head": max_rules_per_head, + "max_rule_size": max_rule_size, + "cycle_prop": cycle_prop, + "count": i, + "directory": directory, + "identifier": identifier, + } + + +def executor_main(config): + sentence = config["sentence"] + assumption_ratio = config["assumption_ratio"] + max_rules_per_head = config["max_rules_per_head"] + max_rule_size = config["max_rule_size"] + cycle_prop = config["cycle_prop"] + i = config["count"] + directory = config["directory"] + identifier = config["identifier"] + + number_assumptions = int(round(assumption_ratio * sentence)) + number_rules_per_head = range(1, max_rules_per_head + 1) + n_spb = range(1, max_rule_size + 1) + + filename = f"{directory}/{identifier}_{sentence}_{assumption_ratio}_{max_rules_per_head}_{max_rule_size}_{cycle_prop}_{i}.aba" + print(filename) + framework = create_framework( + sentence, number_assumptions, number_rules_per_head, n_spb, cycle_prop + ) + query = random.randint(1, number_assumptions) + with open(f"{filename}.asm", "w") as out: + print(f"{filename}.asm") + out.write(f"{query}") + print_ICCMA_format(framework[0], framework[2], framework[3], sentence, filename) + + +def ICCMA23_benchmarks( + sentences=[1000, 2000, 3000, 4000, 5000], + max_rules_per_head_list=[5, 10], + max_rule_size_list=[5, 10], + assumption_ratios=[0.1, 0.3], + cycle_props=[0, 0.1, 0.2, 0.4, 0.6, 0.8, 1.0], + count=10, + directory="iccma23_aba_benchmarks", + identifier="aba", +): + random.seed(811543731122527) + os.makedirs(directory, exist_ok=True) + + with concurrent.futures.ProcessPoolExecutor(max_workers=os.cpu_count()) as executor: + print(f"Starting generation in {directory}..") + configs = generate_configs( + sentences=sentences, + max_rules_per_head_list=max_rules_per_head_list, + max_rule_size_list=max_rule_size_list, + assumption_ratios=assumption_ratios, + cycle_props=cycle_props, + count=count, + directory=directory, + identifier=identifier, + ) + list(executor.map(executor_main, configs)) + print("Done") + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("-d", "--directory") + parser.add_argument("-i", "--identifier") + args = parser.parse_args() + + ICCMA23_benchmarks( + sentences=[50, 100, 300, 500, 1000, 2000, 4000, 6000], + max_rules_per_head_list=[1, 2, 8, 16, 64], + max_rule_size_list=[1, 2, 8, 16, 32], + assumption_ratios=[0.1, 0.3, 0.5, 0.7, 0.9], + cycle_props=[0, 0.1, 0.2, 0.4, 0.6, 0.8, 1.0], + count=2, + directory=args.directory if args.directory is not None else "acyclic", + identifier=args.identifier if args.identifier is not None else "aba", + ) diff --git a/scripts/aba_generator_acyclic.py b/scripts/aba_generator_acyclic.py deleted file mode 100755 index b69bfc2..0000000 --- a/scripts/aba_generator_acyclic.py +++ /dev/null @@ -1,100 +0,0 @@ -#!/usr/bin/env python3 - -import argparse -import random -import os - -def create_framework(n_sentences, n_assumptions, n_rules_per_head, size_of_bodies, cycle_prob): - """ - Create a random framework. - - sentences contains the non-assumption sentences. - n_rules_per_head should be a list exhausting the possible number of rules each head can have - size_of_bodies should be a list exhausting the possible number of sentences in any rule body - These should hold in order to get non-counterintuitive results: - - n_assumptions < n_sentences - - max(size_of_bodies) <= n_sentences+n_assumptions - """ - - assumptions = [str(i) for i in range(1,n_assumptions+1)] - sentences = [str(i) for i in range(n_assumptions+1,n_sentences+1)] - - contraries = {asmpt: random.choice(sentences+assumptions) for asmpt in assumptions} - - # order sentences to avoid cycles - random.shuffle(sentences) - rules = [] - for i, head in enumerate(sentences): - n_rules_in_this_head = random.choice(n_rules_per_head) - for _ in range(n_rules_in_this_head): - size_of_body = random.choice(size_of_bodies) - - # only allow stuff to occur in body if it is lower in the (topological) order - n_available = len(assumptions) + i - - selection_set = assumptions+sentences[:i] - # add potentially cycle creating sentences to the selection set with a given probability - extra_selection = random.sample(sentences[i:], min(len(sentences[i:]), int(cycle_prob*len(sentences)))) - selection_set.extend(extra_selection) - - #body = random.sample(assumptions+sentences[:i], min(size_of_body, n_available)) - body = random.sample(assumptions+selection_set, min(size_of_body, n_available)) - rules.append((head, body)) - - return assumptions, sentences, contraries, rules - -def print_ICCMA_format(assumptions, contraries, rules, n_sentences, out_filename): - """ - Print the given framework in the ICCMA 2023 format. - """ - offset = len(assumptions) - - with open(out_filename, 'w') as out: - out.write(f"p aba {n_sentences}\n") - for i, asm in enumerate(assumptions): - out.write(f"a {asm}\n") - #print(f"a {asm}") - for ctr in contraries: - out.write(f"c {ctr} {contraries.get(ctr)}\n") - #print(f"c {ctr} {contraries.get(ctr)}") - for rule in rules: - out.write(f"r {rule[0]} {' '.join(rule[1])}\n") - #print(f"r {rule[0]} {' '.join(rule[1])}") - -def ICCMA23_benchmarks(sentences=[1000,2000,3000,4000,5000], max_rules_per_head_list=[5,10], max_rule_size_list=[5,10], assumption_ratios=[0.1,0.3], cycle_props=[0, 0.1, 0.2, 0.4, 0.6, 0.8, 1.0], count=10, directory="iccma23_aba_benchmarks", identifier="aba"): - random.seed(811543731122527) - # Create directory if missing - os.makedirs(directory, exist_ok=True) - for sentence in sentences: - for assumption_ratio in assumption_ratios: - for max_rules_per_head in max_rules_per_head_list: - for max_rule_size in max_rule_size_list: - for cycle_prop in cycle_props: - for i in range(count): - number_assumptions = int(round(assumption_ratio*sentence)) - number_rules_per_head = range(1,max_rules_per_head+1) - n_spb = range(1,max_rule_size+1) - filename = f"{directory}/{identifier}_{sentence}_{assumption_ratio}_{max_rules_per_head}_{max_rule_size}_{cycle_prop}_{i}.aba" - print(filename) - framework = create_framework(sentence, number_assumptions, number_rules_per_head, n_spb, cycle_prop) - query = random.randint(1,number_assumptions) - with open(f"{filename}.asm", 'w') as out: - print(f"{filename}.asm") - out.write(f"{query}") - print_ICCMA_format(framework[0], framework[2], framework[3], sentence, filename) - -parser = argparse.ArgumentParser() -parser.add_argument('-d', '--directory') -parser.add_argument('-i', '--identifier') -args = parser.parse_args() - -ICCMA23_benchmarks( - sentences = [50,100,200,300,400,500,1000,2000,5000], - max_rules_per_head_list = [1,2,4,8,16], - max_rule_size_list = [1,2,4,8,16], - assumption_ratios = [0.1,0.3,0.5,0.7,0.9], - cycle_props=[0, 0.1, 0.2, 0.4, 0.6, 0.8, 1.0], - count = 1, - directory=args.directory if args.directory is not None else "acyclic", - identifier=args.identifier if args.identifier is not None else "aba", -) diff --git a/scripts/aba_generator_acyclic_starter.sh b/scripts/aba_generator_acyclic_starter.sh new file mode 100755 index 0000000..84adbf9 --- /dev/null +++ b/scripts/aba_generator_acyclic_starter.sh @@ -0,0 +1,6 @@ +#!/bin/bash + +#SBATCH --ntasks=1 +#SBATCH --time=10:00:00 + +./scripts/aba_generator_acyclic.py diff --git a/scripts/decode-result-folder.py b/scripts/decode-result-folder.py index 6c566ab..b8bc15f 100755 --- a/scripts/decode-result-folder.py +++ b/scripts/decode-result-folder.py @@ -57,10 +57,13 @@ def run(): count += 1 except Exception: print(f'Failed to read {file_path}. Skipping..') - with open(output, 'w') as output_file: - output_file.write - writer = csv.DictWriter(output_file, fieldnames=out[0].keys()) - writer.writeheader() - writer.writerows(out) + if len(out) > 0: + with open(output, 'w') as output_file: + output_file.write + writer = csv.DictWriter(output_file, fieldnames=out[0].keys()) + writer.writeheader() + writer.writerows(out) + else: + print('Empty set') run() diff --git a/scripts/run-gen.sh b/scripts/run-gen.sh new file mode 100755 index 0000000..76db312 --- /dev/null +++ b/scripts/run-gen.sh @@ -0,0 +1,6 @@ +#!/bin/bash +#SBATCH --ntasks=1 +#SBATCH --cpus-per-task=32 +#SBATCH --time=10:00:00 + +./aba-generator-acyclic --directory "$(pwd)/instances"