From 9f6a0da017f389a7253a100ca9063c06447b0ce4 Mon Sep 17 00:00:00 2001 From: Malte Tammena Date: Mon, 25 Mar 2024 17:16:34 +0100 Subject: [PATCH] =?UTF-8?q?no=20=E2=88=9E.=20but=20formatting=20and=20pre-?= =?UTF-8?q?commit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cargo.lock | 119 +++++++++++++++++++ Cargo.toml | 2 + flake.nix | 122 ++++++++----------- nix/packages/aba2sat.nix | 43 ++++--- nix/packages/aspforaba.nix | 53 +++++---- nix/packages/clingo.nix | 18 +-- scripts/validate.sh | 212 ++++++++++++++++----------------- src/aba/prepared.rs | 115 ++++++++++-------- src/graph/mod.rs | 234 ------------------------------------- src/main.rs | 1 - 10 files changed, 398 insertions(+), 521 deletions(-) delete mode 100644 src/graph/mod.rs diff --git a/Cargo.lock b/Cargo.lock index 51bb1d4..33c9ad4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,11 +8,26 @@ version = "0.1.0" dependencies = [ "cadical", "clap", + "graph-cycles", "iter_tools", "nom", + "petgraph", "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]] name = "anstream" version = "0.6.12" @@ -86,6 +101,12 @@ dependencies = [ "libc", ] +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" + [[package]] name = "clap" version = "4.5.1" @@ -139,6 +160,12 @@ version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a" +[[package]] +name = "equivalent" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" + [[package]] name = "errno" version = "0.3.8" @@ -149,12 +176,56 @@ dependencies = [ "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]] name = "heck" version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" 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]] name = "iter_tools" version = "0.10.0" @@ -216,6 +287,22 @@ dependencies = [ "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]] name = "proc-macro2" version = "1.0.78" @@ -306,6 +393,18 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" 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]] name = "windows-sys" version = "0.48.0" @@ -437,3 +536,23 @@ name = "windows_x86_64_msvc" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" 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", +] diff --git a/Cargo.toml b/Cargo.toml index 52eb498..4f858f4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,6 +10,8 @@ license = "GPL3" [dependencies] cadical = "0.1.14" clap = { version = "4.4.8", features = ["wrap_help", "derive"] } +graph-cycles = "0.1.0" iter_tools = "0.10.0" nom = "7.1.3" +petgraph = "0.6.4" thiserror = "1.0.50" diff --git a/flake.nix b/flake.nix index 34052a3..a115ee2 100644 --- a/flake.nix +++ b/flake.nix @@ -6,13 +6,13 @@ inputs.nixpkgs.follows = "nixpkgs"; }; - outputs = - inputs @ { self - , flake-parts - , fenix - , ... - }: - flake-parts.lib.mkFlake { inherit inputs self; } { + outputs = inputs @ { + self, + flake-parts, + fenix, + ... + }: + flake-parts.lib.mkFlake {inherit inputs self;} { imports = [ ]; @@ -24,72 +24,50 @@ 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 - , config - , system - , ... - }: - let - rustToolchain = with fenix.packages.${system}; - combine [ - (complete.withComponents [ - "cargo" - "clippy" - "rust-src" - "rustc" - "rustfmt" - ]) - rust-analyzer - ]; + perSystem = { + self', + pkgs, + config, + system, + ... + }: let + rustToolchain = with fenix.packages.${system}; + combine [ + (complete.withComponents [ + "cargo" + "clippy" + "rust-src" + "rustc" + "rustfmt" + ]) + rust-analyzer + ]; - rustPlatform = pkgs.makeRustPlatform { - cargo = 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"; - }; + rustPlatform = pkgs.makeRustPlatform { + cargo = rustToolchain; + rustc = rustToolchain; }; + 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"; + }; + }; }; } diff --git a/nix/packages/aba2sat.nix b/nix/packages/aba2sat.nix index f6d1099..f6ac860 100644 --- a/nix/packages/aba2sat.nix +++ b/nix/packages/aba2sat.nix @@ -1,28 +1,27 @@ -{ rustPlatform -, lib -, -}: -let +{ + rustPlatform, + lib, +}: let config = lib.trivial.importTOML ../../Cargo.toml; in -rustPlatform.buildRustPackage { - pname = config.package.name; - version = config.package.version; + rustPlatform.buildRustPackage { + pname = config.package.name; + version = config.package.version; - src = lib.sources.cleanSource ../..; + src = lib.sources.cleanSource ../..; - cargoDeps = { - lockFile = "../../Cargo.lock"; - }; + cargoDeps = { + lockFile = "../../Cargo.lock"; + }; - cargoLock = { - lockFile = ../../Cargo.lock; - }; + cargoLock = { + lockFile = ../../Cargo.lock; + }; - meta = { - description = "ABA solver using a SAT backend"; - # homepage = "https://your.new.homepage"; - license = lib.licenses.gpl3; - # maintainers = []; - }; -} + meta = { + description = "ABA solver using a SAT backend"; + # homepage = "https://your.new.homepage"; + license = lib.licenses.gpl3; + # maintainers = []; + }; + } diff --git a/nix/packages/aspforaba.nix b/nix/packages/aspforaba.nix index 76bca06..4154108 100644 --- a/nix/packages/aspforaba.nix +++ b/nix/packages/aspforaba.nix @@ -1,9 +1,8 @@ -{ fetchFromBitbucket -, python3 -, clingo -, -}: -let +{ + fetchFromBitbucket, + python3, + clingo, +}: let name = "ASPforABA"; version = "ICCMA23"; src = fetchFromBitbucket { @@ -13,32 +12,32 @@ let hash = "sha256-QdcisBOsGPOq9/KCQAUpKzQS7E2Olg4Zv+0jmf3/GkU="; }; clingoWithPython = clingo.overrideAttrs (old: { - cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=ON" ]; - nativeBuildInputs = old.nativeBuildInputs ++ [ python3 ]; + cmakeFlags = ["-DCLINGO_BUILD_WITH_PYTHON=ON"]; + nativeBuildInputs = old.nativeBuildInputs ++ [python3]; }); in -python3.pkgs.buildPythonPackage { - inherit src version; - pname = name; + python3.pkgs.buildPythonPackage { + inherit src version; + 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 = '' - rm ./configure - ''; + patchPhase = '' + rm ./configure + ''; - installPhase = '' - mkdir -p $out/bin - cp aspforaba.py $out/bin/ASPforABA - cp -r encodings $out/bin/ + installPhase = '' + mkdir -p $out/bin + cp aspforaba.py $out/bin/ASPforABA + cp -r encodings $out/bin/ - cat << EOF > $out/bin/.config - TEMP_PATH=/tmp/clingo - CLINGO_PATH=${clingoWithPython}/bin/clingo - EOF - ''; -} + cat << EOF > $out/bin/.config + TEMP_PATH=/tmp/clingo + CLINGO_PATH=${clingoWithPython}/bin/clingo + EOF + ''; + } diff --git a/nix/packages/clingo.nix b/nix/packages/clingo.nix index c09d7f0..0dba63f 100644 --- a/nix/packages/clingo.nix +++ b/nix/packages/clingo.nix @@ -1,9 +1,9 @@ -{ lib -, stdenv -, fetchFromGitHub -, cmake -, python3 -, +{ + lib, + stdenv, + fetchFromGitHub, + cmake, + python3, }: stdenv.mkDerivation rec { pname = "clingo"; @@ -16,14 +16,14 @@ stdenv.mkDerivation rec { sha256 = "sha256-2vOscD5jengY3z9gHoY9y9y6RLfdzUj7BNKLyppNRac="; }; - nativeBuildInputs = [ cmake python3 ]; + nativeBuildInputs = [cmake python3]; - cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=ON" ]; + cmakeFlags = ["-DCLINGO_BUILD_WITH_PYTHON=ON"]; meta = { description = "ASP system to ground and solve logic programs"; license = lib.licenses.mit; - maintainers = [ lib.maintainers.raskin ]; + maintainers = [lib.maintainers.raskin]; platforms = lib.platforms.unix; homepage = "https://potassco.org/"; downloadPage = "https://github.com/potassco/clingo/releases/"; diff --git a/scripts/validate.sh b/scripts/validate.sh index 3506f3a..bd81042 100755 --- a/scripts/validate.sh +++ b/scripts/validate.sh @@ -1,46 +1,46 @@ #!/usr/bin/env bash 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\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 " --files-from\n" - printf " Use the following dir to read files, specify a single file with --file instead\n" - exit 1 + if [ -n "$1" ]; then + printf "%s\n\n" "$1" + fi + printf "Usage: validate [OPTIONS] \n" + printf "\n" + printf "Options:\n" + printf " --aspforaba\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 " --files-from\n" + printf " Use the following dir to read files, specify a single file with --file instead\n" + exit 1 } run_dc_co() { - 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 "%40s " "$(basename "$ABA_FILE")" - 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") - 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 - printf "❌\n" - printf "%40s:%s\n" "arg" "$ADDITIONAL_ARG" - printf "%40s:%40s %s\n" "Ours" "$our_result" "$(jq --compact-output --color-output = r#loop.heads.iter().collect(); 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 clauses = body_rules.multi_cartesian_product().map(move |product| { - product - .into_iter() - .map(|elem| I::new(*elem).pos()) - .chain(std::iter::once(I::new(head_sample).neg())) - .collect() - }); - loop_enforcement_clauses.chain(clauses) + let clauses = body_rules + .multi_cartesian_product() + .flat_map(move |product| { + r#loop.heads.iter().map(move |head| { + product + .iter() + .map(|elem| I::new(**elem).pos()) + .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 { - // Construct the graph containing all elements of the universe - // with edges based on the aba's rules - let graph = aba.rules.iter().fold(Graph::new(), |graph, (head, body)| { - body.iter().fold(graph, |mut graph, elem| { - graph.add_edge(*elem, *head); - graph + let mut graph = DiGraph::::new(); + let universe = aba + .universe() + .unique() + .scan(&mut graph, |graph, element| { + let idx = graph.add_node(*element); + Some((*element, idx)) }) + .collect::>(); + 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::>(); + 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 - .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 for PreparedAba { diff --git a/src/graph/mod.rs b/src/graph/mod.rs deleted file mode 100644 index 3ed0845..0000000 --- a/src/graph/mod.rs +++ /dev/null @@ -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>, -} - -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> { - struct TarjanState { - index: i32, - stack: Vec, - on_stack: BTreeSet, - index_of: BTreeMap, - lowlink_of: BTreeMap, - components: Vec>, - } - - 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],] - ); - } -} diff --git a/src/main.rs b/src/main.rs index 3e8b184..1c59c65 100644 --- a/src/main.rs +++ b/src/main.rs @@ -29,7 +29,6 @@ mod aba; mod args; mod clauses; mod error; -mod graph; mod literal; mod mapper; mod parser;