diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..051d09d --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +eval "$(lorri direnv)" diff --git a/Cargo.toml b/Cargo.toml index 0db0eae..507a040 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,7 +2,7 @@ name = "adf_bdd" version = "0.1.1" authors = ["Stefan Ellmauthaler "] -edition = "2018" +edition = "2021" license = "GPL-3.0-only" description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams" diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..b4c5932 --- /dev/null +++ b/flake.lock @@ -0,0 +1,127 @@ +{ + "nodes": { + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1627913399, + "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-utils": { + "locked": { + "lastModified": 1634851050, + "narHash": "sha256-N83GlSGPJJdcqhUxSCS/WwW5pksYf3VP1M13cDRTSVA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "c91f3de5adaf1de973b797ef7485e441a65b8935", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "locked": { + "lastModified": 1623875721, + "narHash": "sha256-A8BU7bjS5GirpAUv4QA+QnJ4CceLHkcXdRp4xITDB0s=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "f7e004a55b120c02ecb6219596820fcd32ca8772", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "gitignoresrc": { + "flake": false, + "locked": { + "lastModified": 1635165013, + "narHash": "sha256-o/BdVjNwcB6jOmzZjOH703BesSkkS5O7ej3xhyO8hAY=", + "owner": "hercules-ci", + "repo": "gitignore.nix", + "rev": "5b9e0ff9d3b551234b4f3eb3983744fa354b17f1", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "gitignore.nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1636552551, + "narHash": "sha256-k7Hq/bvUnRlAfFjPGuw3FsSqqspQdRHsCHpgadw6UkQ=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "9e86f5f7a19db6da2445f07bafa6694b556f9c6d", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-21.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1628186154, + "narHash": "sha256-r2d0wvywFnL9z4iptztdFMhaUIAaGzrSs7kSok0PgmE=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "06552b72346632b6943c8032e57e702ea12413bf", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-compat": "flake-compat", + "flake-utils": "flake-utils", + "gitignoresrc": "gitignoresrc", + "nixpkgs": "nixpkgs", + "rust-overlay": "rust-overlay" + } + }, + "rust-overlay": { + "inputs": { + "flake-utils": "flake-utils_2", + "nixpkgs": "nixpkgs_2" + }, + "locked": { + "lastModified": 1636683315, + "narHash": "sha256-udsMHw5gzZPvvFIhopoGicLK/LaYyDN3iAa1PEpP7uM=", + "owner": "oxalica", + "repo": "rust-overlay", + "rev": "e87b7ea329fc78c5e5775c983193f630458c317f", + "type": "github" + }, + "original": { + "owner": "oxalica", + "repo": "rust-overlay", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..fd0c704 --- /dev/null +++ b/flake.nix @@ -0,0 +1,40 @@ +{ + description = "basic rust flake"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.05"; + rust-overlay.url = "github:oxalica/rust-overlay"; + flake-utils.url = "github:numtide/flake-utils"; + flake-compat = { + url = "github:edolstra/flake-compat"; + flake = false; + }; + gitignoresrc = { + url = "github:hercules-ci/gitignore.nix"; + flake = false; + }; + }; + + outputs = { self, nixpkgs, flake-utils, flake-compat, gitignoresrc, rust-overlay, ... }@inputs: + { + #overlay = import ./nix { inherit gitignoresrc; }; + } // (flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { + inherit system; + overlays = [ (import rust-overlay)]; + }; + in + rec { + devShell = + pkgs.mkShell { + buildInputs = [ + pkgs.rust-bin.stable.latest.default + pkgs.rust-analyzer + pkgs.cargo-audit + pkgs.cargo-license + ]; + }; + } + )); +} diff --git a/flake.nix~ b/flake.nix~ new file mode 100644 index 0000000..ab4fc53 --- /dev/null +++ b/flake.nix~ @@ -0,0 +1,42 @@ +{ + description = "d2sgraph - a program to show the graphs (based on d2sparql)"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-21.05"; + rust-overlay.url = "github:oxalica/rust-overlay"; + flake-utils.url = "github:numtide/flake-utils"; + flake-compat = { + url = "github:edolstra/flake-compat"; + flake = false; + }; + gitignoresrc = { + url = "github:hercules-ci/gitignore.nix"; + flake = false; + }; + }; + + outputs = { self, nixpkgs, flake-utils, flake-compat, gitignoresrc, rust-overlay, ... }@inputs: + { + #overlay = import ./nix { inherit gitignoresrc; }; + } // (flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { + inherit system; + overlays = [ (import rust-overlay)]; + }; + in + rec { + devShell = + pkgs.mkShell { + buildInputs = [ + pkgs.rust-bin.stable.latest.default + pkgs.rust-analyzer + pkgs.cargo-audit + pkgs.cargo-license + pkgs.graphviz + pkgs.clingo + ]; + }; + } + )); +} diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..8a7465a --- /dev/null +++ b/shell.nix @@ -0,0 +1,13 @@ +(import + ( + let + lock = builtins.fromJSON (builtins.readFile ./flake.lock); + in + fetchTarball { + url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz"; + sha256 = lock.nodes.flake-compat.locked.narHash; + } + ) + { + src = ./.; + }).shellNix.default diff --git a/src/adf.rs b/src/adf.rs index 2fb097a..f58ca69 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -219,7 +219,7 @@ impl Adf { None => None, } } - + #[allow(clippy::ptr_arg)] fn apply_interpretation(&mut self, interpretation: &Vec) -> Vec { let mut new_interpretation = interpretation.clone(); diff --git a/src/lib.rs b/src/lib.rs index 159eb18..3a652a8 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,7 +1,7 @@ //! This library contains an efficient representation of `Abstract Dialectical Frameworks (ADf)` by utilising an implementation of `Ordered Binary Decision Diagrams (OBDD)` //! //! # Abstract Dialectical Frameworks -//! An `abstract dialectical framework` consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration. +//! An `abstract dialectical framework` consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration. //! # Ordered Binary Decision Diagram //! An `ordered binary decision diagram` is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap. //! @@ -25,11 +25,11 @@ //! s(b). //! s(c). //! s(d). -//! +//! //! ac(a,c(v)). //! ac(b,or(a,b)). //! ac(c,neg(b)). //! ac(d,d). //! ``` +pub mod adf; pub mod obdd; -pub mod adf; \ No newline at end of file diff --git a/src/obdd.rs b/src/obdd.rs index 411cd2f..70a4b31 100644 --- a/src/obdd.rs +++ b/src/obdd.rs @@ -12,9 +12,9 @@ type Term = usize; /// Represents a node in the BDD /// -/// +/// #[derive(Eq, PartialEq, Hash, Clone, Copy)] -pub (crate) struct BddNode { +pub(crate) struct BddNode { var: usize, lo: Term, hi: Term, @@ -26,14 +26,14 @@ impl std::fmt::Display for BddNode { } } -impl BddNode{ - pub fn var(self)->usize{ +impl BddNode { + pub fn var(self) -> usize { self.var } } -pub (crate) struct Bdd { - pub (crate) nodes: Vec, +pub(crate) struct Bdd { + pub(crate) nodes: Vec, hash: HashMap, } @@ -59,11 +59,7 @@ impl Bdd { if lo == hi { lo } else { - let node = BddNode { - var, - lo, - hi, - }; + let node = BddNode { var, lo, hi }; match self.hash.get(&node) { Some(n) => *n, None => { @@ -78,7 +74,6 @@ impl Bdd { } } } - pub fn variable(&mut self, var: usize) -> Term { self.create_node(var, BDD_BOT, BDD_TOP) @@ -94,7 +89,8 @@ impl Bdd { pub fn restrict(&mut self, subtree: Term, var: usize, val: bool) -> Term { let treenode = self.nodes[subtree]; - #[allow(clippy::collapsible_else_if)] // Better readabilty of the if/then/else structure of the algorithm + #[allow(clippy::collapsible_else_if)] + // Better readabilty of the if/then/else structure of the algorithm if treenode.var > var || treenode.var == usize::MAX { subtree } else if treenode.var < var {