ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-18 09:19:38 +01:00
Code Issues Projects Releases Wiki Activity

Edition 2021, fmt applied

Browse Source 
Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
This commit is contained in:
Stefan Ellmauthaler 2021-11-12 14:14:12 +01:00
parent e0855f9e22
commit 611501588a
9 changed files with 237 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.envrc Normal file
View File

@ -0,0 +1 @@
eval "$(lorri direnv)"

2
Cargo.toml
View File

@ -2,7 +2,7 @@
name = "adf_bdd"
version = "0.1.1"
authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
edition = "2018"
edition = "2021"
license = "GPL-3.0-only"
description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams"

127
flake.lock generated Normal file
View File

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

40
flake.nix Normal file
View File

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

42
flake.nix~ Normal file
View File

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

13
shell.nix Normal file
View File

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

2
src/adf.rs
View File

@ -219,7 +219,7 @@ impl Adf {
None => None,
}
}
#[allow(clippy::ptr_arg)]
fn apply_interpretation(&mut self, interpretation: &Vec<usize>) -> Vec<usize> {
let mut new_interpretation = interpretation.clone();

6
src/lib.rs
View File

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

22
src/obdd.rs
View File

@ -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<BddNode>,
pub(crate) struct Bdd {
pub(crate) nodes: Vec<BddNode>,
hash: HashMap<BddNode, Term>,
}
@ -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 {