From f27502784ac231bbc6384cf3ed9de95a2a21dc64 Mon Sep 17 00:00:00 2001 From: monsterkrampe Date: Thu, 1 Sep 2022 09:31:19 +0200 Subject: [PATCH] Support multiple solving strategies --- frontend/src/components/app.tsx | 21 ++++- frontend/src/components/graph.tsx | 2 +- lib/src/adf.rs | 118 ++++++++++++++++++++++++++- lib/src/obdd.rs | 4 +- server/src/main.rs | 128 +++++------------------------- 5 files changed, 154 insertions(+), 119 deletions(-) diff --git a/frontend/src/components/app.tsx b/frontend/src/components/app.tsx index 84c25ec..9119b6c 100644 --- a/frontend/src/components/app.tsx +++ b/frontend/src/components/app.tsx @@ -35,13 +35,20 @@ ac(10,and(neg(2),6)). ac(1,and(neg(7),2)). ac(6,neg(7)).ac(2,and(neg(9),neg(6))).`; +enum Strategy { + ParseOnly = 'ParseOnly', + Ground = 'Ground', + FirstComplete = 'FirstComplete', + FirstStable = 'FirstStable', +} + function App() { const [loading, setLoading] = useState(false); const [code, setCode] = useState(placeholder); const [graph, setGraph] = useState(); const submitHandler = useCallback( - () => { + (strategy: Strategy) => { setLoading(true); fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, { @@ -49,7 +56,7 @@ function App() { headers: { 'Content-Type': 'application/json', }, - body: JSON.stringify({ code }), + body: JSON.stringify({ code, strategy }), }) .then((res) => res.json()) .then((data) => setGraph(data)) @@ -86,8 +93,14 @@ function App() { onChange={(event) => { setCode(event.target.value); }} /> - - + + + {' '} + + {' '} + + {' '} + {graph diff --git a/frontend/src/components/graph.tsx b/frontend/src/components/graph.tsx index f9085a8..c4f84b6 100644 --- a/frontend/src/components/graph.tsx +++ b/frontend/src/components/graph.tsx @@ -191,7 +191,7 @@ function Graph(props: Props) { label, style: { height: subLabel.length > 0 ? 60 : 30, - width: Math.max(30, 10 * mainLabel.length, 10 * subLabel.length), + width: Math.max(30, 5 * mainLabel.length + 10, 5 * subLabel.length + 10), }, }; }); diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 4d13df6..dc87a6d 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -7,6 +7,7 @@ This module describes the abstract dialectical framework. pub mod heuristics; use std::cell::RefCell; +use std::collections::{HashMap, HashSet}; use crate::{ datatypes::{ @@ -30,14 +31,25 @@ use self::heuristics::Heuristic; /// /// Please note that due to the nature of the underlying reduced and ordered Bdd the concept of a [`Term`][crate::datatypes::Term] represents one (sub) formula as well as truth-values. pub struct Adf { - // TODO: none of this should be public - pub ordering: VarContainer, - pub bdd: Bdd, - pub ac: Vec, + ordering: VarContainer, + bdd: Bdd, + ac: Vec, #[serde(skip, default = "Adf::default_rng")] rng: RefCell, } +#[derive(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<(usize, usize)>, + hi_edges: Vec<(usize, usize)>, +} + impl Default for Adf { fn default() -> Self { Self { @@ -920,6 +932,104 @@ 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, value_part) + }) + .collect(); + + let tree_root_labels: 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 lo_edges: Vec<(usize, usize)> = 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())) + .collect(); + + let hi_edges: Vec<(usize, usize)> = 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())) + .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/lib/src/obdd.rs b/lib/src/obdd.rs index 321a2f3..a54cb70 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -13,9 +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 { - // TODO: use this again - // pub(crate) nodes: Vec, - pub nodes: Vec, + pub(crate) nodes: Vec, #[cfg(feature = "variablelist")] #[serde(skip)] var_deps: Vec>, diff --git a/server/src/main.rs b/server/src/main.rs index 31f4139..0e8ecb1 100644 --- a/server/src/main.rs +++ b/server/src/main.rs @@ -1,32 +1,27 @@ use actix_files as fs; use actix_web::{post, web, App, HttpServer, Responder}; use serde::{Deserialize, Serialize}; -use std::collections::{HashMap, HashSet}; #[cfg(feature = "cors_for_local_development")] use actix_cors::Cors; #[cfg(feature = "cors_for_local_development")] use actix_web::http; -use adf_bdd::adf::Adf; -use adf_bdd::datatypes::Var; +use adf_bdd::adf::{Adf, DoubleLabeledGraph}; use adf_bdd::parser::AdfParser; -#[derive(Serialize)] -// This is a DTO for the graph output -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<(usize, usize)>, - hi_edges: Vec<(usize, usize)>, +#[derive(Deserialize)] +enum Strategy { + ParseOnly, + Ground, + FirstComplete, + FirstStable, } #[derive(Deserialize)] struct SolveReqBody { code: String, + strategy: Strategy, } #[derive(Serialize)] @@ -37,6 +32,7 @@ struct SolveResBody { #[post("/solve")] async fn solve(req_body: web::Json) -> impl Responder { let input = &req_body.code; + let strategy = &req_body.strategy; let parser = AdfParser::default(); match parser.parse()(input) { @@ -52,99 +48,17 @@ async fn solve(req_body: web::Json) -> impl Responder { log::debug!("{:?}", adf); - // TODO: as first test: turn full graph with initial ac into DoubleLabeledGraph DTO and return it - - // get relevant nodes from bdd and ac - let mut node_indices: HashSet = HashSet::new(); - let mut new_node_indices: HashSet = adf.ac.iter().map(|term| term.value()).collect(); - - while !new_node_indices.is_empty() { - node_indices = node_indices.union(&new_node_indices).map(|i| *i).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, value_part) - }) - .collect(); - - let tree_root_labels: HashMap> = adf.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 lo_edges: Vec<(usize, usize)> = 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())) - .collect(); - - let hi_edges: Vec<(usize, usize)> = 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())) - .collect(); - - log::debug!("{:?}", node_labels); - log::debug!("{:?}", tree_root_labels); - log::debug!("{:?}", lo_edges); - log::debug!("{:?}", hi_edges); - - let dto = DoubleLabeledGraph { - node_labels, - tree_root_labels, - lo_edges, - hi_edges, + let ac = match strategy { + Strategy::ParseOnly => None, + Strategy::Ground => Some(adf.grounded()), + // TODO: error handling if no such model exists! + Strategy::FirstComplete => Some(adf.complete().next().unwrap()), + // TODO: error handling if no such model exists! + Strategy::FirstStable => Some(adf.stable().next().unwrap()), }; + let dto = adf.into_double_labeled_graph(ac.as_ref()); + web::Json(dto) } @@ -183,9 +97,9 @@ async fn main() -> std::io::Result<()> { // this mus be last to not override anything .service(fs::Files::new("/", "./assets").index_file("index.html")) }) - .bind(("0.0.0.0", 8080))? - .run() - .await; + .bind(("0.0.0.0", 8080))? + .run() + .await; server }