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

no ∞. but formatting and pre-commit

Browse source
This commit is contained in:
Malte Tammena 2024-03-25 17:16:34 +01:00
parent 8ab001405a
commit 9f6a0da017
10 changed files with 398 additions and 521 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

119
Cargo.lock generated
View file

@ -8,11 +8,26 @@ version = "0.1.0"
dependencies = [ dependencies = [
"cadical", "cadical",
"clap", "clap",
"graph-cycles",
"iter_tools", "iter_tools",
"nom", "nom",
"petgraph",
"thiserror", "thiserror",
] ]
[[package]]
name = "ahash"
version = "0.8.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011"
dependencies = [
"cfg-if",
"getrandom",
"once_cell",
"version_check",
"zerocopy",
]
[[package]] [[package]]
name = "anstream" name = "anstream"
version = "0.6.12" version = "0.6.12"
@ -86,6 +101,12 @@ dependencies = [
"libc", "libc",
] ]
[[package]]
name = "cfg-if"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
[[package]] [[package]]
name = "clap" name = "clap"
version = "4.5.1" version = "4.5.1"
@ -139,6 +160,12 @@ version = "1.10.0"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a" checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a"
[[package]]
name = "equivalent"
version = "1.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
[[package]] [[package]]
name = "errno" name = "errno"
version = "0.3.8" version = "0.3.8"
@ -149,12 +176,56 @@ dependencies = [
"windows-sys 0.52.0", "windows-sys 0.52.0",
] ]
[[package]]
name = "fixedbitset"
version = "0.4.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80"
[[package]]
name = "getrandom"
version = "0.2.12"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "190092ea657667030ac6a35e305e62fc4dd69fd98ac98631e5d3a2b1575a12b5"
dependencies = [
"cfg-if",
"libc",
"wasi",
]
[[package]]
name = "graph-cycles"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3a6ad932c6dd3cfaf16b66754a42f87bbeefd591530c4b6a8334270a7df3e853"
dependencies = [
"ahash",
"petgraph",
"thiserror",
]
[[package]]
name = "hashbrown"
version = "0.14.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"
[[package]] [[package]]
name = "heck" name = "heck"
version = "0.4.1" version = "0.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
[[package]]
name = "indexmap"
version = "2.2.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26"
dependencies = [
"equivalent",
"hashbrown",
]
[[package]] [[package]]
name = "iter_tools" name = "iter_tools"
version = "0.10.0" version = "0.10.0"
@ -216,6 +287,22 @@ dependencies = [
"minimal-lexical", "minimal-lexical",
] ]
[[package]]
name = "once_cell"
version = "1.19.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92"
[[package]]
name = "petgraph"
version = "0.6.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9"
dependencies = [
"fixedbitset",
"indexmap",
]
[[package]] [[package]]
name = "proc-macro2" name = "proc-macro2"
version = "1.0.78" version = "1.0.78"
@ -306,6 +393,18 @@ version = "0.2.1"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
[[package]]
name = "version_check"
version = "0.9.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
[[package]]
name = "wasi"
version = "0.11.0+wasi-snapshot-preview1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
[[package]] [[package]]
name = "windows-sys" name = "windows-sys"
version = "0.48.0" version = "0.48.0"
@ -437,3 +536,23 @@ name = "windows_x86_64_msvc"
version = "0.52.0" version = "0.52.0"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04" checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
[[package]]
name = "zerocopy"
version = "0.7.32"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be"
dependencies = [
"zerocopy-derive",
]
[[package]]
name = "zerocopy-derive"
version = "0.7.32"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
dependencies = [
"proc-macro2",
"quote",
"syn",
]

2
Cargo.toml
View file

@ -10,6 +10,8 @@ license = "GPL3"
[dependencies] [dependencies]
cadical = "0.1.14" cadical = "0.1.14"
clap = { version = "4.4.8", features = ["wrap_help", "derive"] } clap = { version = "4.4.8", features = ["wrap_help", "derive"] }
graph-cycles = "0.1.0"
iter_tools = "0.10.0" iter_tools = "0.10.0"
nom = "7.1.3" nom = "7.1.3"
petgraph = "0.6.4"
thiserror = "1.0.50" thiserror = "1.0.50"

122
flake.nix
View file

@ -6,13 +6,13 @@
inputs.nixpkgs.follows = "nixpkgs"; inputs.nixpkgs.follows = "nixpkgs";
}; };
outputs = outputs = inputs @ {
inputs @ { self self,
, flake-parts flake-parts,
, fenix fenix,
, ... ...
}: }:
flake-parts.lib.mkFlake { inherit inputs self; } { flake-parts.lib.mkFlake {inherit inputs self;} {
imports = [ imports = [
]; ];
@ -24,72 +24,50 @@
flake.hydraJobs.devShells.x86_64-linux = self.devShells.x86_64-linux; flake.hydraJobs.devShells.x86_64-linux = self.devShells.x86_64-linux;
flake.hydraJobs.checks.x86_64-linux = self.checks.x86_64-linux; flake.hydraJobs.checks.x86_64-linux = self.checks.x86_64-linux;
perSystem = perSystem = {
{ self' self',
, pkgs pkgs,
, config config,
, system system,
, ... ...
}: }: let
let rustToolchain = with fenix.packages.${system};
rustToolchain = with fenix.packages.${system}; combine [
combine [ (complete.withComponents [
(complete.withComponents [ "cargo"
"cargo" "clippy"
"clippy" "rust-src"
"rust-src" "rustc"
"rustc" "rustfmt"
"rustfmt" ])
]) rust-analyzer
rust-analyzer ];
];
rustPlatform = pkgs.makeRustPlatform { rustPlatform = pkgs.makeRustPlatform {
cargo = rustToolchain; cargo = rustToolchain;
rustc = rustToolchain; rustc = rustToolchain;
};
rename = pkgs.writeShellApplication {
name = "rename";
runtimeInputs = [
pkgs.fd
pkgs.coreutils
pkgs.nixFlakes
pkgs.jq
];
text = ''
newName="$1"
pushd "$(nix flake metadata --json 2>/dev/null | jq .original.path -r)"
# This is only used to prevent the literal name from appearing here, as the rename would find it!
oldName=$(echo 'change_my_name' | sed 's/_/-/g')
stat "nix/packages/$oldName.nix" 2>/dev/null >/dev/null || echo -e "\033[31mCan only be done once\033[0m"
stat "nix/packages/$oldName.nix" 2>/dev/null >/dev/null || exit 1
fd --type f --exec sed "s/aba2sat/$newName/g" -i '{}'
mv nix/packages/aba2sat.nix "nix/packages/$newName.nix"
'';
};
in
{
packages.aba2sat = pkgs.callPackage ./nix/packages/aba2sat.nix { inherit rustPlatform; };
packages.aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix { };
packages.clingo = pkgs.callPackage ./nix/packages/clingo.nix { };
packages.default = self'.packages.aba2sat;
devShells.default = pkgs.mkShell {
name = "aba2sat";
nativeBuildInputs = [
pkgs.cargo-workspaces
pkgs.nil
pkgs.pre-commit
pkgs.nodejs
pkgs.shellcheck
pkgs.shfmt
rustToolchain
rename
self'.packages.aspforaba
];
RUST_LOG = "trace";
};
}; };
in {
packages.aba2sat = pkgs.callPackage ./nix/packages/aba2sat.nix {inherit rustPlatform;};
packages.aspforaba = pkgs.callPackage ./nix/packages/aspforaba.nix {};
packages.clingo = pkgs.callPackage ./nix/packages/clingo.nix {};
packages.default = self'.packages.aba2sat;
devShells.default = pkgs.mkShell {
name = "aba2sat";
nativeBuildInputs = [
pkgs.alejandra
pkgs.cargo-workspaces
pkgs.nil
pkgs.nodejs
pkgs.pre-commit
pkgs.shellcheck
pkgs.shfmt
rustToolchain
self'.packages.aspforaba
];
RUST_LOG = "trace";
};
};
}; };
} }

43
nix/packages/aba2sat.nix
View file

@ -1,28 +1,27 @@
{ rustPlatform {
, lib rustPlatform,
, lib,
}: }: let
let
config = lib.trivial.importTOML ../../Cargo.toml; config = lib.trivial.importTOML ../../Cargo.toml;
in in
rustPlatform.buildRustPackage { rustPlatform.buildRustPackage {
pname = config.package.name; pname = config.package.name;
version = config.package.version; version = config.package.version;
src = lib.sources.cleanSource ../..; src = lib.sources.cleanSource ../..;
cargoDeps = { cargoDeps = {
lockFile = "../../Cargo.lock"; lockFile = "../../Cargo.lock";
}; };
cargoLock = { cargoLock = {
lockFile = ../../Cargo.lock; lockFile = ../../Cargo.lock;
}; };
meta = { meta = {
description = "ABA solver using a SAT backend"; description = "ABA solver using a SAT backend";
# homepage = "https://your.new.homepage"; # homepage = "https://your.new.homepage";
license = lib.licenses.gpl3; license = lib.licenses.gpl3;
# maintainers = []; # maintainers = [];
}; };
} }

53
nix/packages/aspforaba.nix
View file

@ -1,9 +1,8 @@
{ fetchFromBitbucket {
, python3 fetchFromBitbucket,
, clingo python3,
, clingo,
}: }: let
let
name = "ASPforABA"; name = "ASPforABA";
version = "ICCMA23"; version = "ICCMA23";
src = fetchFromBitbucket { src = fetchFromBitbucket {
@ -13,32 +12,32 @@ let
hash = "sha256-QdcisBOsGPOq9/KCQAUpKzQS7E2Olg4Zv+0jmf3/GkU="; hash = "sha256-QdcisBOsGPOq9/KCQAUpKzQS7E2Olg4Zv+0jmf3/GkU=";
}; };
clingoWithPython = clingo.overrideAttrs (old: { clingoWithPython = clingo.overrideAttrs (old: {
cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=ON" ]; cmakeFlags = ["-DCLINGO_BUILD_WITH_PYTHON=ON"];
nativeBuildInputs = old.nativeBuildInputs ++ [ python3 ]; nativeBuildInputs = old.nativeBuildInputs ++ [python3];
}); });
in in
python3.pkgs.buildPythonPackage { python3.pkgs.buildPythonPackage {
inherit src version; inherit src version;
pname = name; pname = name;
format = "other"; format = "other";
pythonPath = [ clingoWithPython python3.pkgs.cffi ]; pythonPath = [clingoWithPython python3.pkgs.cffi];
makeWrapperArgs = [ "--run 'mkdir -p /tmp/clingo'" ]; makeWrapperArgs = ["--run 'mkdir -p /tmp/clingo'"];
patchPhase = '' patchPhase = ''
rm ./configure rm ./configure
''; '';
installPhase = '' installPhase = ''
mkdir -p $out/bin mkdir -p $out/bin
cp aspforaba.py $out/bin/ASPforABA cp aspforaba.py $out/bin/ASPforABA
cp -r encodings $out/bin/ cp -r encodings $out/bin/
cat << EOF > $out/bin/.config cat << EOF > $out/bin/.config
TEMP_PATH=/tmp/clingo TEMP_PATH=/tmp/clingo
CLINGO_PATH=${clingoWithPython}/bin/clingo CLINGO_PATH=${clingoWithPython}/bin/clingo
EOF EOF
''; '';
} }

18
nix/packages/clingo.nix
View file

@ -1,9 +1,9 @@
{ lib {
, stdenv lib,
, fetchFromGitHub stdenv,
, cmake fetchFromGitHub,
, python3 cmake,
, python3,
}: }:
stdenv.mkDerivation rec { stdenv.mkDerivation rec {
pname = "clingo"; pname = "clingo";
@ -16,14 +16,14 @@ stdenv.mkDerivation rec {
sha256 = "sha256-2vOscD5jengY3z9gHoY9y9y6RLfdzUj7BNKLyppNRac="; sha256 = "sha256-2vOscD5jengY3z9gHoY9y9y6RLfdzUj7BNKLyppNRac=";
}; };
nativeBuildInputs = [ cmake python3 ]; nativeBuildInputs = [cmake python3];
cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=ON" ]; cmakeFlags = ["-DCLINGO_BUILD_WITH_PYTHON=ON"];
meta = { meta = {
description = "ASP system to ground and solve logic programs"; description = "ASP system to ground and solve logic programs";
license = lib.licenses.mit; license = lib.licenses.mit;
maintainers = [ lib.maintainers.raskin ]; maintainers = [lib.maintainers.raskin];
platforms = lib.platforms.unix; platforms = lib.platforms.unix;
homepage = "https://potassco.org/"; homepage = "https://potassco.org/";
downloadPage = "https://github.com/potassco/clingo/releases/"; downloadPage = "https://github.com/potassco/clingo/releases/";

212
scripts/validate.sh
View file

@ -1,46 +1,46 @@
#!/usr/bin/env bash #!/usr/bin/env bash
print_help_and_exit() { print_help_and_exit() {
if [ -n "$1" ]; then if [ -n "$1" ]; then
printf "%s\n\n" "$1" printf "%s\n\n" "$1"
fi fi
printf "Usage: validate [OPTIONS] \n" printf "Usage: validate [OPTIONS] \n"
printf "\n" printf "\n"
printf "Options:\n" printf "Options:\n"
printf " --aspforaba\n" printf " --aspforaba\n"
printf " Binary to use when calling aspforaba\n" printf " Binary to use when calling aspforaba\n"
printf " -p, --problem\n" printf " -p, --problem\n"
printf " The problem to solve\n" printf " The problem to solve\n"
printf " -a, --arg\n" printf " -a, --arg\n"
printf " The additional argument for the problem\n" printf " The additional argument for the problem\n"
printf " -f, --file\n" printf " -f, --file\n"
printf " The file containing the problem in ABA format\n" printf " The file containing the problem in ABA format\n"
printf " --files-from\n" printf " --files-from\n"
printf " Use the following dir to read files, specify a single file with --file instead\n" printf " Use the following dir to read files, specify a single file with --file instead\n"
exit 1 exit 1
} }
run_dc_co() { run_dc_co() {
if [ -z "$ADDITIONAL_ARG" ]; then if [ -z "$ADDITIONAL_ARG" ]; then
print_help_and_exit "Parameter --arg is missing!" print_help_and_exit "Parameter --arg is missing!"
fi fi
if [ -z "$ABA_FILE" ]; then if [ -z "$ABA_FILE" ]; then
print_help_and_exit "Parameter --file is missing!" print_help_and_exit "Parameter --file is missing!"
fi fi
printf "%40s " "$(basename "$ABA_FILE")" printf "%40s " "$(basename "$ABA_FILE")"
TIMEFORMAT='{"wall":"%E","system":"%S","user":"%U"}' TIMEFORMAT='{"wall":"%E","system":"%S","user":"%U"}'
our_result=$(command time -f "$TIMEFORMAT" -o /tmp/aba2sat-time "$ABA2SAT" --file "$ABA_FILE" dc-co --query "$ADDITIONAL_ARG") our_result=$(command time -f "$TIMEFORMAT" -o /tmp/aba2sat-time "$ABA2SAT" --file "$ABA_FILE" dc-co --query "$ADDITIONAL_ARG")
other_result=$(command time -f "$TIMEFORMAT" -o /tmp/aspforaba-time "$ASPFORABA" --file "$ABA_FILE" --problem DC-CO --query "$ADDITIONAL_ARG") other_result=$(command time -f "$TIMEFORMAT" -o /tmp/aspforaba-time "$ASPFORABA" --file "$ABA_FILE" --problem DC-CO --query "$ADDITIONAL_ARG")
if [ "$our_result" != "$other_result" ]; then if [ "$our_result" != "$other_result" ]; then
printf "❌\n" printf "❌\n"
printf "%40s:%s\n" "arg" "$ADDITIONAL_ARG" printf "%40s:%s\n" "arg" "$ADDITIONAL_ARG"
printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output </tmp/aba2sat-time)" printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output </tmp/aba2sat-time)"
printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq --compact-output --color-output </tmp/aspforaba-time)" printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq --compact-output --color-output </tmp/aspforaba-time)"
else else
printf "✅\n" printf "✅\n"
printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output </tmp/aba2sat-time)" printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output </tmp/aba2sat-time)"
printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq --compact-output --color-output </tmp/aspforaba-time)" printf "%40s:%40s %s\n" "Theirs" "$other_result" "$(jq --compact-output --color-output </tmp/aspforaba-time)"
fi fi
} }
POSITIONAL_ARGS=() POSITIONAL_ARGS=()
@ -53,78 +53,78 @@ PROBLEM=
ADDITIONAL_ARG= ADDITIONAL_ARG=
while [[ $# -gt 0 ]]; do while [[ $# -gt 0 ]]; do
case $1 in case $1 in
-h | --help) -h | --help)
print_help_and_exit print_help_and_exit
;; ;;
--aspforaba) --aspforaba)
shift shift
ASPFORABA=$1 ASPFORABA=$1
shift shift
;; ;;
-p | --problem) -p | --problem)
shift shift
PROBLEM=$1 PROBLEM=$1
shift shift
;; ;;
-f | --file) -f | --file)
if [ -n "$ABA_FILE_DIR" ]; then if [ -n "$ABA_FILE_DIR" ]; then
print_help_and_exit "Parameters --file and --files-from cannot be mixed" print_help_and_exit "Parameters --file and --files-from cannot be mixed"
fi fi
shift shift
ABA_FILE=$1 ABA_FILE=$1
shift shift
;; ;;
--files-from) --files-from)
if [ -n "$ABA_FILE" ]; then if [ -n "$ABA_FILE" ]; then
print_help_and_exit "Parameters --file and --files-from cannot be mixed" print_help_and_exit "Parameters --file and --files-from cannot be mixed"
fi fi
if [ -n "$ADDITIONAL_ARG" ]; then if [ -n "$ADDITIONAL_ARG" ]; then
print_help_and_exit "Parameters --arg and --files-from cannot be mixed" print_help_and_exit "Parameters --arg and --files-from cannot be mixed"
fi fi
shift shift
ABA_FILE_DIR=$1 ABA_FILE_DIR=$1
shift shift
;; ;;
-a | --arg) -a | --arg)
if [ -n "$ABA_FILE_DIR" ]; then if [ -n "$ABA_FILE_DIR" ]; then
print_help_and_exit "Parameters --arg and --files-from cannot be mixed" print_help_and_exit "Parameters --arg and --files-from cannot be mixed"
fi fi
shift shift
ADDITIONAL_ARG=$1 ADDITIONAL_ARG=$1
shift shift
;; ;;
--aba2sat) --aba2sat)
shift shift
ABA2SAT=$1 ABA2SAT=$1
shift shift
;; ;;
-*) -*)
echo "Unknown option $1" echo "Unknown option $1"
print_help_and_exit print_help_and_exit
;; ;;
*) *)
POSITIONAL_ARGS+=("$1") # save positional arg POSITIONAL_ARGS+=("$1") # save positional arg
shift # past argument shift # past argument
;; ;;
esac esac
done done
set -- "${POSITIONAL_ARGS[@]}" # restore positional parameters set -- "${POSITIONAL_ARGS[@]}" # restore positional parameters
case "$PROBLEM" in case "$PROBLEM" in
dc-co | DC-CO) dc-co | DC-CO)
if [ -n "$ABA_FILE_DIR" ]; then if [ -n "$ABA_FILE_DIR" ]; then
# run for every file found in the directory # run for every file found in the directory
for file in "$ABA_FILE_DIR"/*."$ABA_FILE_EXT"; do for file in "$ABA_FILE_DIR"/*."$ABA_FILE_EXT"; do
ABA_FILE="$file" ADDITIONAL_ARG="$(cat "$file.asm")" run_dc_co ABA_FILE="$file" ADDITIONAL_ARG="$(cat "$file.asm")" run_dc_co
done done
else else
# run for the single configured file # run for the single configured file
run_dc_co run_dc_co
fi fi
;; ;;
*) *)
print_help_and_exit "Problem $PROBLEM is not supported" print_help_and_exit "Problem $PROBLEM is not supported"
;; ;;
esac esac

115
src/aba/prepared.rs
View file

@ -1,8 +1,17 @@
use std::collections::HashSet; use std::{
collections::{BTreeMap, HashSet},
fs::File,
io::Write,
};
use graph_cycles::Cycles;
use iter_tools::Itertools; use iter_tools::Itertools;
use petgraph::{
dot::{Config, Dot},
graph::DiGraph,
};
use crate::{aba::Num, clauses::Clause, graph::Graph, literal::TheoryAtom}; use crate::{aba::Num, clauses::Clause, literal::TheoryAtom};
use super::{theory::theory_helper, Aba, RuleList}; use super::{theory::theory_helper, Aba, RuleList};
@ -28,26 +37,19 @@ impl PreparedAba {
self.loops.iter().flat_map(|r#loop| { self.loops.iter().flat_map(|r#loop| {
let mut head_list: Vec<_> = r#loop.heads.iter().collect(); let mut head_list: Vec<_> = r#loop.heads.iter().collect();
head_list.push(head_list[0]); head_list.push(head_list[0]);
let loop_enforcement_clauses =
head_list
.into_iter()
.tuple_windows()
.flat_map(|(first, second)| {
[
Clause::from(vec![I::new(*first).pos(), I::new(*second).pos()]),
Clause::from(vec![I::new(*first).neg(), I::new(*second).neg()]),
]
});
let head_sample = *r#loop.heads.iter().next().unwrap();
let body_rules = r#loop.support.iter().map(|(_head, body)| body); let body_rules = r#loop.support.iter().map(|(_head, body)| body);
let clauses = body_rules.multi_cartesian_product().map(move |product| { let clauses = body_rules
product .multi_cartesian_product()
.into_iter() .flat_map(move |product| {
.map(|elem| I::new(*elem).pos()) r#loop.heads.iter().map(move |head| {
.chain(std::iter::once(I::new(head_sample).neg())) product
.collect() .iter()
}); .map(|elem| I::new(**elem).pos())
loop_enforcement_clauses.chain(clauses) .chain(std::iter::once(I::new(*head).neg()))
.collect()
})
});
clauses
}) })
} }
} }
@ -84,38 +86,51 @@ fn trim_unreachable_rules(aba: &mut Aba) {
} }
fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> { fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
// Construct the graph containing all elements of the universe let mut graph = DiGraph::<Num, ()>::new();
// with edges based on the aba's rules let universe = aba
let graph = aba.rules.iter().fold(Graph::new(), |graph, (head, body)| { .universe()
body.iter().fold(graph, |mut graph, elem| { .unique()
graph.add_edge(*elem, *head); .scan(&mut graph, |graph, element| {
graph let idx = graph.add_node(*element);
Some((*element, idx))
}) })
.collect::<BTreeMap<_, _>>();
aba.rules
.iter()
.flat_map(|(head, body)| body.iter().map(|body_element| (*body_element, *head)))
.for_each(|(from, to)| {
let from = universe.get(&from).unwrap();
let to = universe.get(&to).unwrap();
graph.update_edge(*from, *to, ());
});
let mut file = File::create("./graph.gv").unwrap();
let dot = Dot::with_config(&graph, &[Config::EdgeNoLabel]);
write!(file, "{dot:?}").unwrap();
// TODO: Write on debug, simplify for production
let mut loops = vec![];
graph.visit_cycles(|graph, cycle| {
let heads = cycle.iter().map(|idx| graph[*idx]).collect::<HashSet<_>>();
let loop_rules = aba
.rules
.iter()
.filter(|(head, _body)| heads.contains(head));
// Relevant rules are those that contain only elements from outside the loop
// All other rules cannot influence the value of the loop
let support = loop_rules
.filter(|(_head, body)| body.is_disjoint(&heads))
.cloned()
.collect();
loops.push(r#Loop { heads, support });
if loops.len() >= universe.len() {
if loops.len() == universe.len() {
eprintln!("Too... many... cycles... Aborting cycle detection. Solver? You're on your own now");
}
std::ops::ControlFlow::Break(())
} else {
std::ops::ControlFlow::Continue(())
}
}); });
// Use a linear time algorithm to calculate the strongly connected
// components of the derived graph
let scc = graph.tarjan_scc();
// Loops are strongly connected components that have more than one element
// These are just the largest loops. There may be smaller loops inside loops
// but it should suffice to prevent these loops
let loops = scc.into_iter().filter(|component| component.len() > 1);
// Iterate over all loops and apply the fixing-logic
loops loops
.map(|heads| {
let heads: HashSet<_> = heads.into_iter().map(|head| head as Num).collect();
let loop_rules = aba
.rules
.iter()
.filter(|(head, _body)| heads.contains(head));
// Relevant rules are those that contain only elements from outside the loop
// All other rules cannot influence the value of the loop
let support = loop_rules
.filter(|(_head, body)| body.is_disjoint(&heads))
.cloned()
.collect();
r#Loop { heads, support }
})
.collect()
} }
impl From<Aba> for PreparedAba { impl From<Aba> for PreparedAba {

234
src/graph/mod.rs
View file

@ -1,234 +0,0 @@
//! [SOURCE](https://github.com/TheAlgorithms/Rust)
//!
//! MIT License
//!
//! Copyright (c) 2019 The Algorithms
//!
//! Permission is hereby granted, free of charge, to any person obtaining a copy
//! of this software and associated documentation files (the "Software"), to deal
//! in the Software without restriction, including without limitation the rights
//! to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
//! copies of the Software, and to permit persons to whom the Software is
//! furnished to do so, subject to the following conditions:
//!
//! The above copyright notice and this permission notice shall be included in all
//! copies or substantial portions of the Software.
//!
//! THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
//! IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
//! FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
//! AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
//! LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
//! OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
//! SOFTWARE.
use std::collections::{BTreeMap, BTreeSet, HashSet};
use crate::aba::Num;
#[derive(Debug)]
pub struct Graph {
adj_list: BTreeMap<Num, Vec<Num>>,
}
impl Graph {
pub fn new() -> Self {
Self {
adj_list: BTreeMap::new(),
}
}
#[cfg(test)]
pub fn add_vertex(&mut self, vertex: Num) {
self.adj_list.entry(vertex).or_default();
}
pub fn add_edge(&mut self, from: Num, to: Num) {
self.adj_list.entry(from).or_default().push(to);
}
pub fn tarjan_scc(&self) -> Vec<HashSet<Num>> {
struct TarjanState {
index: i32,
stack: Vec<Num>,
on_stack: BTreeSet<Num>,
index_of: BTreeMap<Num, i32>,
lowlink_of: BTreeMap<Num, i32>,
components: Vec<HashSet<Num>>,
}
let mut state = TarjanState {
index: 0,
stack: Vec::new(),
on_stack: Default::default(),
index_of: Default::default(),
lowlink_of: Default::default(),
components: Vec::new(),
};
fn strong_connect(v: Num, graph: &Graph, state: &mut TarjanState) {
state.index_of.insert(v, state.index);
state.lowlink_of.insert(v, state.index);
state.index += 1;
state.stack.push(v);
state.on_stack.insert(v);
for &w in graph.adj_list.get(&v).unwrap_or(&vec![]) {
if !state.index_of.contains_key(&w) {
strong_connect(w, graph, state);
let curr = state.lowlink_of.get(&v).cloned();
let other = state.lowlink_of.get(&w).cloned();
match (curr, other) {
(Some(curr), Some(other)) => {
state.lowlink_of.insert(v, curr.min(other));
}
(Some(first), None) | (None, Some(first)) => {
state.lowlink_of.insert(v, first);
}
(None, None) => {
state.lowlink_of.remove(&v);
}
}
} else if state.on_stack.contains(&w) {
let curr = state.lowlink_of.get(&v).cloned();
let other = state.index_of.get(&w).cloned();
match (curr, other) {
(Some(curr), Some(other)) => {
state.lowlink_of.insert(v, curr.min(other));
}
(Some(first), None) | (None, Some(first)) => {
state.lowlink_of.insert(v, first);
}
(None, None) => {
state.lowlink_of.remove(&v);
}
}
}
}
if state.lowlink_of.get(&v) == state.index_of.get(&v) {
let mut component = HashSet::new();
while let Some(w) = state.stack.pop() {
state.on_stack.remove(&w);
component.insert(w);
if w == v {
break;
}
}
state.components.push(component);
}
}
for v in self.adj_list.keys() {
if !state.index_of.contains_key(v) {
strong_connect(*v, self, &mut state);
}
}
state.components
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_tarjan_scc() {
// Test 1: A graph with multiple strongly connected components
let n_vertices = 11;
let edges = vec![
(0, 1),
(0, 3),
(1, 2),
(1, 4),
(2, 0),
(2, 6),
(3, 2),
(4, 5),
(4, 6),
(5, 6),
(5, 7),
(5, 8),
(5, 9),
(6, 4),
(7, 9),
(8, 9),
(9, 8),
];
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = graph.tarjan_scc();
assert_eq!(
components,
vec![
set![8, 9],
set![7],
set![5, 4, 6],
set![3, 2, 1, 0],
set![10],
]
);
// Test 2: A graph with no edges
let n_vertices = 5;
let edges = vec![];
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = graph.tarjan_scc();
// Each node is its own SCC
assert_eq!(
components,
vec![set![0], set![1], set![2], set![3], set![4]]
);
// Test 3: A graph with single strongly connected component
let n_vertices = 5;
let edges = vec![(0, 1), (1, 2), (2, 3), (2, 4), (3, 0), (4, 2)];
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = graph.tarjan_scc();
assert_eq!(components, vec![set![4, 3, 2, 1, 0]]);
// Test 4: A graph with multiple strongly connected component
let n_vertices = 7;
let edges = vec![
(0, 1),
(1, 2),
(2, 0),
(1, 3),
(1, 4),
(1, 6),
(3, 5),
(4, 5),
];
let mut graph = Graph::new();
(0..n_vertices).for_each(|v| graph.add_vertex(v));
for &(u, v) in &edges {
graph.add_edge(u, v);
}
let components = graph.tarjan_scc();
assert_eq!(
components,
vec![set![5], set![3], set![4], set![6], set![2, 1, 0],]
);
}
}

1
src/main.rs
View file

@ -29,7 +29,6 @@ mod aba;
mod args; mod args;
mod clauses; mod clauses;
mod error; mod error;
mod graph;
mod literal; mod literal;
mod mapper; mod mapper;
mod parser; mod parser;