diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 2b568eb..aae8967 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -7,7 +7,6 @@ This module describes the abstract dialectical framework. pub mod heuristics; use std::cell::RefCell; -use std::collections::{HashMap, HashSet}; use crate::datatypes::BddNode; use crate::{ @@ -42,18 +41,6 @@ pub struct Adf { rng: RefCell, } -#[derive(Clone, Deserialize, Serialize, Debug)] -/// This is a DTO for the graph output -pub struct DoubleLabeledGraph { - // number of nodes equals the number of node labels - // nodes implicitly have their index as their ID - node_labels: HashMap, - // every node gets this label containing multiple entries (it might be empty) - tree_root_labels: HashMap>, - lo_edges: Vec<(String, String)>, - hi_edges: Vec<(String, String)>, -} - impl Default for Adf { fn default() -> Self { Self { @@ -952,111 +939,6 @@ impl Adf { log::info!("{ng_store}"); log::debug!("{:?}", ng_store); } - - /// Turns Adf into solved graph representation - pub fn into_double_labeled_graph(&self, ac: Option<&Vec>) -> DoubleLabeledGraph { - let ac: &Vec = match ac { - Some(ac) => ac, - None => &self.ac, - }; - - let mut node_indices: HashSet = HashSet::new(); - let mut new_node_indices: HashSet = ac.iter().map(|term| term.value()).collect(); - - while !new_node_indices.is_empty() { - node_indices = node_indices.union(&new_node_indices).copied().collect(); - new_node_indices = HashSet::new(); - - for node_index in &node_indices { - let lo_node_index = self.bdd.nodes[*node_index].lo().value(); - if !node_indices.contains(&lo_node_index) { - new_node_indices.insert(lo_node_index); - } - - let hi_node_index = self.bdd.nodes[*node_index].hi().value(); - if !node_indices.contains(&hi_node_index) { - new_node_indices.insert(hi_node_index); - } - } - } - - let node_labels: HashMap = self - .bdd - .nodes - .iter() - .enumerate() - .filter(|(i, _)| node_indices.contains(i)) - .map(|(i, &node)| { - let value_part = match node.var() { - Var::TOP => "TOP".to_string(), - Var::BOT => "BOT".to_string(), - _ => self.ordering.name(node.var()).expect( - "name for each var should exist; special cases are handled separately", - ), - }; - - (i.to_string(), value_part) - }) - .collect(); - - let tree_root_labels_with_usize: HashMap> = ac.iter().enumerate().fold( - self.bdd - .nodes - .iter() - .enumerate() - .filter(|(i, _)| node_indices.contains(i)) - .map(|(i, _)| (i, vec![])) - .collect(), - |mut acc, (root_for, root_node)| { - acc.get_mut(&root_node.value()) - .expect("we know that the index will be in the map") - .push(self.ordering.name(Var(root_for)).expect( - "name for each var should exist; special cases are handled separately", - )); - - acc - }, - ); - - let tree_root_labels: HashMap> = tree_root_labels_with_usize - .into_iter() - .map(|(i, vec)| (i.to_string(), vec)) - .collect(); - - let lo_edges: Vec<(String, String)> = self - .bdd - .nodes - .iter() - .enumerate() - .filter(|(i, _)| node_indices.contains(i)) - .filter(|(_, node)| !vec![Var::TOP, Var::BOT].contains(&node.var())) - .map(|(i, &node)| (i, node.lo().value())) - .map(|(i, v)| (i.to_string(), v.to_string())) - .collect(); - - let hi_edges: Vec<(String, String)> = self - .bdd - .nodes - .iter() - .enumerate() - .filter(|(i, _)| node_indices.contains(i)) - .filter(|(_, node)| !vec![Var::TOP, Var::BOT].contains(&node.var())) - .map(|(i, &node)| (i, node.hi().value())) - .map(|(i, v)| (i.to_string(), v.to_string())) - .collect(); - - log::debug!("{:?}", node_labels); - log::debug!("{:?}", tree_root_labels); - log::debug!("{:?}", lo_edges); - log::debug!("{:?}", hi_edges); - - DoubleLabeledGraph { - node_labels, - tree_root_labels, - lo_edges, - hi_edges, - } - } } #[cfg(test)] diff --git a/server/src/adf.rs b/server/src/adf.rs index d0e0d72..31858b6 100644 --- a/server/src/adf.rs +++ b/server/src/adf.rs @@ -18,13 +18,15 @@ use mongodb::results::DeleteResult; use names::{Generator, Name}; use serde::{Deserialize, Serialize}; -use adf_bdd::adf::{Adf, DoubleLabeledGraph}; +use adf_bdd::adf::Adf; use adf_bdd::adfbiodivine::Adf as BdAdf; use adf_bdd::parser::AdfParser; use crate::config::{AppState, RunningInfo, Task, ADF_COLL, COMPUTE_TIME, DB_NAME, USER_COLL}; use crate::user::{username_exists, User}; +use crate::double_labeled_graph::DoubleLabeledGraph; + type Ac = Vec; type AcDb = Vec; @@ -403,7 +405,7 @@ async fn add_adf_problem( let ac_and_graph = AcAndGraph { ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(), - graph: lib_adf.into_double_labeled_graph(None), + graph: DoubleLabeledGraph::from_adf_and_ac(&lib_adf, None), }; (SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph) @@ -576,7 +578,7 @@ async fn solve_adf_problem( .iter() .map(|ac| AcAndGraph { ac: ac.iter().map(|t| t.0.to_string()).collect(), - graph: adf.into_double_labeled_graph(Some(ac)), + graph: DoubleLabeledGraph::from_adf_and_ac(&adf, Some(ac)), }) .collect(); diff --git a/server/src/double_labeled_graph.rs b/server/src/double_labeled_graph.rs new file mode 100644 index 0000000..9f1034e --- /dev/null +++ b/server/src/double_labeled_graph.rs @@ -0,0 +1,118 @@ +use serde::{Deserialize, Serialize}; +use std::collections::{HashMap, HashSet}; + +use adf_bdd::adf::Adf; +use adf_bdd::datatypes::{Term, Var}; + +#[derive(Clone, Deserialize, Serialize, Debug)] +/// This is a DTO for the graph output +pub struct DoubleLabeledGraph { + // number of nodes equals the number of node labels + // nodes implicitly have their index as their ID + node_labels: HashMap, + // every node gets this label containing multiple entries (it might be empty) + tree_root_labels: HashMap>, + lo_edges: Vec<(String, String)>, + hi_edges: Vec<(String, String)>, +} + +impl DoubleLabeledGraph { + pub fn from_adf_and_ac(adf: &Adf, ac: Option<&Vec>) -> Self { + let ac: &Vec = match ac { + Some(ac) => ac, + None => &adf.ac, + }; + + let mut node_indices: HashSet = HashSet::new(); + let mut new_node_indices: HashSet = ac.iter().map(|term| term.value()).collect(); + + while !new_node_indices.is_empty() { + node_indices = node_indices.union(&new_node_indices).copied().collect(); + new_node_indices = HashSet::new(); + + for node_index in &node_indices { + let lo_node_index = adf.bdd.nodes[*node_index].lo().value(); + if !node_indices.contains(&lo_node_index) { + new_node_indices.insert(lo_node_index); + } + + let hi_node_index = adf.bdd.nodes[*node_index].hi().value(); + if !node_indices.contains(&hi_node_index) { + new_node_indices.insert(hi_node_index); + } + } + } + + let node_labels: HashMap = adf + .bdd + .nodes + .iter() + .enumerate() + .filter(|(i, _)| node_indices.contains(i)) + .map(|(i, &node)| { + let value_part = match node.var() { + Var::TOP => "TOP".to_string(), + Var::BOT => "BOT".to_string(), + _ => adf.ordering.name(node.var()).expect( + "name for each var should exist; special cases are handled separately", + ), + }; + + (i.to_string(), value_part) + }) + .collect(); + + let tree_root_labels_with_usize: HashMap> = ac.iter().enumerate().fold( + adf.bdd + .nodes + .iter() + .enumerate() + .filter(|(i, _)| node_indices.contains(i)) + .map(|(i, _)| (i, vec![])) + .collect(), + |mut acc, (root_for, root_node)| { + acc.get_mut(&root_node.value()) + .expect("we know that the index will be in the map") + .push(adf.ordering.name(Var(root_for)).expect( + "name for each var should exist; special cases are handled separately", + )); + + acc + }, + ); + + let tree_root_labels: HashMap> = tree_root_labels_with_usize + .into_iter() + .map(|(i, vec)| (i.to_string(), vec)) + .collect(); + + let lo_edges: Vec<(String, String)> = adf + .bdd + .nodes + .iter() + .enumerate() + .filter(|(i, _)| node_indices.contains(i)) + .filter(|(_, node)| !vec![Var::TOP, Var::BOT].contains(&node.var())) + .map(|(i, &node)| (i, node.lo().value())) + .map(|(i, v)| (i.to_string(), v.to_string())) + .collect(); + + let hi_edges: Vec<(String, String)> = adf + .bdd + .nodes + .iter() + .enumerate() + .filter(|(i, _)| node_indices.contains(i)) + .filter(|(_, node)| !vec![Var::TOP, Var::BOT].contains(&node.var())) + .map(|(i, &node)| (i, node.hi().value())) + .map(|(i, v)| (i.to_string(), v.to_string())) + .collect(); + + DoubleLabeledGraph { + node_labels, + tree_root_labels, + lo_edges, + hi_edges, + } + } +} diff --git a/server/src/main.rs b/server/src/main.rs index acccfb1..93615b6 100644 --- a/server/src/main.rs +++ b/server/src/main.rs @@ -17,6 +17,7 @@ use actix_cors::Cors; mod adf; mod config; +mod double_labeled_graph; mod user; use adf::{