megamanmalte/aba2sat
0
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

scripting and tweaking

Browse source
This commit is contained in:
Malte Tammena 2024-06-18 08:41:09 +02:00
parent 7e8d83b871
commit 06641ddc80
6 changed files with 382 additions and 274 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

357
flake.nix
View file

@ -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
];
};
};
};
}

174
scripts/aba-generator-acyclic.py Executable file
View file

@ -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",
)

100
scripts/aba_generator_acyclic.py
View file

@ -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",
)

6
scripts/aba_generator_acyclic_starter.sh Executable file
View file

@ -0,0 +1,6 @@
#!/bin/bash
#SBATCH --ntasks=1
#SBATCH --time=10:00:00
./scripts/aba_generator_acyclic.py

13
scripts/decode-result-folder.py
View file

@ -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()

6
scripts/run-gen.sh Executable file
View file

@ -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"