1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Compare commits

..

No commits in common. "f56a9bea066f1831f503098a1ce2cd518cef8315" and "aa189de7b5481acf6282bf20d169d299c9f12541" have entirely different histories.

11 changed files with 60 additions and 214 deletions

View File

@ -7,11 +7,11 @@ name: DevSkim
on:
push:
branches: [ "main" ]
branches: [ main ]
pull_request:
branches: [ "main" ]
branches: [ main ]
schedule:
- cron: '15 6 * * 4'
- cron: '26 6 * * 5'
jobs:
lint:
@ -23,12 +23,12 @@ jobs:
security-events: write
steps:
- name: Checkout code
uses: actions/checkout@v3
uses: actions/checkout@v2
- name: Run DevSkim scanner
uses: microsoft/DevSkim-Action@v1
- name: Upload DevSkim scan results to GitHub Security tab
uses: github/codeql-action/upload-sarif@v2
uses: github/codeql-action/upload-sarif@v1
with:
sarif_file: devskim-results.sarif

View File

@ -11,15 +11,13 @@
# Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project)
This project is currently split into three parts:
This project is currently split into two parts:
- a [binary (adf-bdd)](bin), which allows one to easily answer semantics questions on abstract dialectical frameworks
- a [library (adf_bdd)](lib), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions
- a [server](server) and a [frontend](frontend) to access the solver as a web-service available at https://adf-bdd.dev
Latest documentation of the API can be found [here](https://docs.rs/adf_bdd/latest/adf_bdd/).
The current version of the binary can be downloaded [here](https://github.com/ellmau/adf-obdd/releases).
Do not hesitate to report bugs or ask about features in the [issues-section](https://github.com/ellmau/adf-obdd/issues) or have a conversation about anything of the project in the [discussion space](https://github.com/ellmau/adf-obdd/discussions)

View File

@ -8,8 +8,8 @@
![Crates.io](https://img.shields.io/crates/l/adf_bdd)
[![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust)
| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Web-Service](https://adf-bdd.dev) | [Repository](https://github.com/ellmau/adf-obdd) |
|--- | --- | --- | --- | --- |
| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Repository](https://github.com/ellmau/adf-obdd) |
|--- | --- | --- | --- |
# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF-BDD)
This is the readme for the executable solver.

View File

@ -8,8 +8,8 @@
![Crates.io](https://img.shields.io/crates/l/adf_bdd)
[![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust)
| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Web-Service](https://adf-bdd.dev) | [Repository](https://github.com/ellmau/adf-obdd) |
|--- | --- | --- | --- | --- |
| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Repository](https://github.com/ellmau/adf-obdd) |
|--- | --- | --- | --- |
# Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden (ADF_BDD)
This library contains an efficient representation of Abstract Dialectical Frameworks (ADf) by utilising an implementation of Ordered Binary Decision Diagrams (OBDD)

View File

@ -8,16 +8,14 @@
![Crates.io](https://img.shields.io/crates/l/adf_bdd)
[![GitHub Discussions](https://img.shields.io/github/discussions/ellmau/adf-obdd)](https://github.com/ellmau/adf-obdd/discussions) ![rust-edition](https://img.shields.io/badge/Rust--edition-2021-blue?logo=rust)
| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Web-Service](https://adf-bdd.dev) | [Repository](https://github.com/ellmau/adf-obdd) |
|--- | --- | --- | --- | --- |
| [Home](index.md) | [Binary](adf-bdd.md) | [Library](adf_bdd.md)| [Repository](https://github.com/ellmau/adf-obdd) |
|--- | --- | --- | --- |
# Abstract Dialectical Frameworks solved by (ordered) Binary Decision Diagrams; developed in Dresden (ADF-oBDD project)
This project is currently split into three parts:
This project is currently split into two parts:
- a [binary (adf-bdd)](adf-bdd.md), which allows one to easily answer semantics questions on abstract dialectical frameworks
- a [library (adf_bdd)](adf_bdd.md), which contains all the necessary algorithms and an open API which compute the answers to the semantics questions
- a server and a frontend, available at https://adf-bdd.dev
Latest documentation of the API can be found [here](https://docs.rs/adf_bdd/latest/adf_bdd/).
The current version of the binary can be downloaded [here](https://github.com/ellmau/adf-obdd/releases).

View File

@ -8,6 +8,7 @@ This module describes the abstract dialectical framework.
pub mod heuristics;
use std::cell::RefCell;
use crate::datatypes::BddNode;
use crate::{
datatypes::{
adf::{
@ -51,18 +52,23 @@ impl Default for Adf {
}
}
impl From<(VarContainer, Bdd, Vec<Term>)> for Adf {
fn from(source: (VarContainer, Bdd, Vec<Term>)) -> Self {
Self {
ordering: source.0,
bdd: source.1,
ac: source.2,
impl Adf {
/// Instntiates an ADF based on the publically available data
pub fn from_ord_nodes_and_ac(
ordering: VarContainer,
bdd_nodes: Vec<BddNode>,
ac: Vec<Term>,
) -> Self {
let bdd = Bdd::from_nodes(bdd_nodes);
Adf {
ordering,
bdd,
ac,
rng: Self::default_rng(),
}
}
}
impl Adf {
/// Instantiates a new ADF, based on the [parser-data][crate::parser::AdfParser].
pub fn from_parser(parser: &AdfParser) -> Self {
log::info!("[Start] instantiating BDD");

View File

@ -26,7 +26,7 @@ impl Default for VarContainer {
}
impl VarContainer {
/// Create [`VarContainer`] from its components
/// Create [VarContainer] from its components
pub fn from_parser(
names: Arc<RwLock<Vec<String>>>,
mapping: Arc<RwLock<HashMap<String, usize>>>,
@ -52,12 +52,12 @@ impl VarContainer {
.and_then(|name| name.get(var.value()).cloned())
}
/// Return ordered names from [`VarContainer`]
/// Return ordered names from [VarContainer]
pub fn names(&self) -> Arc<RwLock<Vec<String>>> {
Arc::clone(&self.names)
}
/// Return map from names to indices in [`VarContainer`]
/// Return map from names to indices in [VarContainer]
pub fn mappings(&self) -> Arc<RwLock<HashMap<String, usize>>> {
Arc::clone(&self.mapping)
}

View File

@ -198,146 +198,6 @@ while let Ok(result) = r.recv() {
solving.join().unwrap();
```
### Serialize and Deserialize custom datastructures representing an [`adf::Adf`]
The Web Application <https://adf-bdd.dev> uses custom datastructures that are stored in a mongodb which inspired this example.
```rust
use std::sync::{Arc, RwLock};
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
use adf_bdd::datatypes::adf::VarContainer;
use adf_bdd::datatypes::{BddNode, Term, Var};
use adf_bdd::obdd::Bdd;
use adf_bdd::parser::AdfParser;
use adf_bdd::adf::Adf;
// Custom Datastructures for (De-)Serialization
# #[derive(PartialEq, Debug)]
#[derive(Deserialize, Serialize)]
struct MyCustomVarContainer {
names: Vec<String>,
mapping: HashMap<String, String>,
}
impl From<VarContainer> for MyCustomVarContainer {
fn from(source: VarContainer) -> Self {
Self {
names: source.names().read().unwrap().clone(),
mapping: source
.mappings()
.read()
.unwrap()
.iter()
.map(|(k, v)| (k.clone(), v.to_string()))
.collect(),
}
}
}
impl From<MyCustomVarContainer> for VarContainer {
fn from(source: MyCustomVarContainer) -> Self {
Self::from_parser(
Arc::new(RwLock::new(source.names)),
Arc::new(RwLock::new(
source
.mapping
.into_iter()
.map(|(k, v)| (k, v.parse().unwrap()))
.collect(),
)),
)
}
}
# #[derive(PartialEq, Debug)]
#[derive(Deserialize, Serialize)]
struct MyCustomBddNode {
var: String,
lo: String,
hi: String,
}
impl From<BddNode> for MyCustomBddNode {
fn from(source: BddNode) -> Self {
Self {
var: source.var().0.to_string(),
lo: source.lo().0.to_string(),
hi: source.hi().0.to_string(),
}
}
}
impl From<MyCustomBddNode> for BddNode {
fn from(source: MyCustomBddNode) -> Self {
Self::new(
Var(source.var.parse().unwrap()),
Term(source.lo.parse().unwrap()),
Term(source.hi.parse().unwrap()),
)
}
}
# #[derive(PartialEq, Debug)]
#[derive(Deserialize, Serialize)]
struct MyCustomAdf {
ordering: MyCustomVarContainer,
bdd: Vec<MyCustomBddNode>,
ac: Vec<String>,
}
impl From<Adf> for MyCustomAdf {
fn from(source: Adf) -> Self {
Self {
ordering: source.ordering.into(),
bdd: source.bdd.nodes.into_iter().map(Into::into).collect(),
ac: source.ac.into_iter().map(|t| t.0.to_string()).collect(),
}
}
}
impl From<MyCustomAdf> for Adf {
fn from(source: MyCustomAdf) -> Self {
let bdd = Bdd::from(source.bdd.into_iter().map(Into::into).collect::<Vec<BddNode>>());
Adf::from((
source.ordering.into(),
bdd,
source
.ac
.into_iter()
.map(|t| Term(t.parse().unwrap()))
.collect(),
))
}
}
// use the above example as input
let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d).";
let parser = AdfParser::default();
parser.parse()(&input).unwrap();
// create Adf
let adf = Adf::from_parser(&parser);
// cast into custom struct
let my_custom_adf: MyCustomAdf = adf.into();
// stringify to json
let json: String = serde_json::to_string(&my_custom_adf).unwrap();
// parse json
let parsed_custom_adf: MyCustomAdf = serde_json::from_str(&json).unwrap();
// cast into lib struct that resembles the original Adf
let parsed_adf: Adf = parsed_custom_adf.into();
# let my_custom_adf2: MyCustomAdf = parsed_adf.into();
# assert_eq!(my_custom_adf, my_custom_adf2);
```
*/
#![deny(
missing_debug_implementations,

View File

@ -82,7 +82,7 @@ impl NoGood {
visit.then_some(result)
}
/// Creates an updated [`Vec<Term>`], based on the given [&[Term]] and the [NoGood].
/// Creates an updated [Vec<Term>], based on the given [&[Term]] and the [NoGood].
/// The parameter _update_ is set to [`true`] if there has been an update and to [`false`] otherwise
pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec<Term> {
*update = false;

View File

@ -13,7 +13,7 @@ use std::{cell::RefCell, cmp::min, collections::HashMap, fmt::Display};
/// Each roBDD is identified by its corresponding [`Term`], which implicitly identifies the root node of a roBDD.
#[derive(Debug, Serialize, Deserialize)]
pub struct Bdd {
/// The nodes of the [`Bdd`] with their edges
/// The nodes of the [Bdd] with their edges
pub nodes: Vec<BddNode>,
#[cfg(feature = "variablelist")]
#[serde(skip)]
@ -50,18 +50,6 @@ impl Default for Bdd {
}
}
impl From<Vec<BddNode>> for Bdd {
fn from(nodes: Vec<BddNode>) -> Self {
let mut bdd = Self::new();
for node in nodes {
bdd.node(node.var(), node.lo(), node.hi());
}
bdd
}
}
impl Bdd {
/// Instantiate a new roBDD structure.
/// Constants for the [``][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too.
@ -113,6 +101,17 @@ impl Bdd {
RefCell::new(HashMap::new())
}
/// Construct [Bdd] from a list of nodes by adding one after the other
pub fn from_nodes(nodes: Vec<BddNode>) -> Self {
let mut bdd = Self::new();
for node in nodes {
bdd.node(node.var(), node.lo(), node.hi());
}
bdd
}
/// Instantiates a [variable][crate::datatypes::Var] and returns the representing roBDD as a [`Term`][crate::datatypes::Term].
pub fn variable(&mut self, var: Var) -> Term {
self.node(var, Term::BOT, Term::TOP)

View File

@ -20,7 +20,6 @@ use serde::{Deserialize, Serialize};
use adf_bdd::adf::Adf;
use adf_bdd::adfbiodivine::Adf as BdAdf;
use adf_bdd::obdd::Bdd;
use adf_bdd::parser::AdfParser;
use crate::config::{AppState, RunningInfo, Task, ADF_COLL, COMPUTE_TIME, DB_NAME, USER_COLL};
@ -165,38 +164,16 @@ pub(crate) struct SimplifiedAdf {
pub(crate) ac: AcDb,
}
impl From<Adf> for SimplifiedAdf {
fn from(source: Adf) -> Self {
Self {
ordering: source.ordering.into(),
bdd: source.bdd.nodes.into_iter().map(Into::into).collect(),
ac: source.ac.into_iter().map(|t| t.0.to_string()).collect(),
impl SimplifiedAdf {
fn from_lib_adf(adf: Adf) -> Self {
SimplifiedAdf {
ordering: adf.ordering.into(),
bdd: adf.bdd.nodes.into_iter().map(Into::into).collect(),
ac: adf.ac.into_iter().map(|t| t.0.to_string()).collect(),
}
}
}
impl From<SimplifiedAdf> for Adf {
fn from(source: SimplifiedAdf) -> Self {
let bdd = Bdd::from(
source
.bdd
.into_iter()
.map(Into::into)
.collect::<Vec<BddNode>>(),
);
Adf::from((
source.ordering.into(),
bdd,
source
.ac
.into_iter()
.map(|t| Term(t.parse().unwrap()))
.collect(),
))
}
}
type SimplifiedAdfOpt = OptionWithError<SimplifiedAdf>;
#[derive(Deserialize, Serialize)]
@ -431,7 +408,7 @@ async fn add_adf_problem(
graph: DoubleLabeledGraph::from_adf_and_ac(&lib_adf, None),
};
(SimplifiedAdf::from(lib_adf), ac_and_graph)
(SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph)
});
app_state
@ -573,7 +550,15 @@ async fn solve_adf_problem(
#[cfg(feature = "mock_long_computations")]
std::thread::sleep(Duration::from_secs(20));
let mut adf: Adf = simp_adf.into();
let mut adf: Adf = Adf::from_ord_nodes_and_ac(
simp_adf.ordering.into(),
simp_adf.bdd.into_iter().map(Into::into).collect(),
simp_adf
.ac
.into_iter()
.map(|t| Term(t.parse().unwrap()))
.collect(),
);
let acs: Vec<Ac> = match adf_problem_input.strategy {
Strategy::Complete => adf.complete().collect(),