mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Support multiple solving strategies
This commit is contained in:
parent
08dbd3d4e7
commit
f27502784a
@ -35,13 +35,20 @@ ac(10,and(neg(2),6)).
|
|||||||
ac(1,and(neg(7),2)).
|
ac(1,and(neg(7),2)).
|
||||||
ac(6,neg(7)).ac(2,and(neg(9),neg(6))).`;
|
ac(6,neg(7)).ac(2,and(neg(9),neg(6))).`;
|
||||||
|
|
||||||
|
enum Strategy {
|
||||||
|
ParseOnly = 'ParseOnly',
|
||||||
|
Ground = 'Ground',
|
||||||
|
FirstComplete = 'FirstComplete',
|
||||||
|
FirstStable = 'FirstStable',
|
||||||
|
}
|
||||||
|
|
||||||
function App() {
|
function App() {
|
||||||
const [loading, setLoading] = useState(false);
|
const [loading, setLoading] = useState(false);
|
||||||
const [code, setCode] = useState(placeholder);
|
const [code, setCode] = useState(placeholder);
|
||||||
const [graph, setGraph] = useState();
|
const [graph, setGraph] = useState();
|
||||||
|
|
||||||
const submitHandler = useCallback(
|
const submitHandler = useCallback(
|
||||||
() => {
|
(strategy: Strategy) => {
|
||||||
setLoading(true);
|
setLoading(true);
|
||||||
|
|
||||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
|
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
|
||||||
@ -49,7 +56,7 @@ function App() {
|
|||||||
headers: {
|
headers: {
|
||||||
'Content-Type': 'application/json',
|
'Content-Type': 'application/json',
|
||||||
},
|
},
|
||||||
body: JSON.stringify({ code }),
|
body: JSON.stringify({ code, strategy }),
|
||||||
})
|
})
|
||||||
.then((res) => res.json())
|
.then((res) => res.json())
|
||||||
.then((data) => setGraph(data))
|
.then((data) => setGraph(data))
|
||||||
@ -86,8 +93,14 @@ function App() {
|
|||||||
onChange={(event) => { setCode(event.target.value); }}
|
onChange={(event) => { setCode(event.target.value); }}
|
||||||
/>
|
/>
|
||||||
</Container>
|
</Container>
|
||||||
<Container maxWidth="xs">
|
<Container>
|
||||||
<Button fullWidth variant="outlined" onClick={submitHandler}>Solve it!</Button>
|
<Button variant="outlined" onClick={() => submitHandler(Strategy.ParseOnly)}>Parse only</Button>
|
||||||
|
{' '}
|
||||||
|
<Button variant="outlined" onClick={() => submitHandler(Strategy.Ground)}>Grounded Model</Button>
|
||||||
|
{' '}
|
||||||
|
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstComplete)}>(First) Complete Model</Button>
|
||||||
|
{' '}
|
||||||
|
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStable)}>(First) Stable Model</Button>
|
||||||
</Container>
|
</Container>
|
||||||
|
|
||||||
{graph
|
{graph
|
||||||
|
|||||||
@ -191,7 +191,7 @@ function Graph(props: Props) {
|
|||||||
label,
|
label,
|
||||||
style: {
|
style: {
|
||||||
height: subLabel.length > 0 ? 60 : 30,
|
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),
|
||||||
},
|
},
|
||||||
};
|
};
|
||||||
});
|
});
|
||||||
|
|||||||
118
lib/src/adf.rs
118
lib/src/adf.rs
@ -7,6 +7,7 @@ This module describes the abstract dialectical framework.
|
|||||||
|
|
||||||
pub mod heuristics;
|
pub mod heuristics;
|
||||||
use std::cell::RefCell;
|
use std::cell::RefCell;
|
||||||
|
use std::collections::{HashMap, HashSet};
|
||||||
|
|
||||||
use crate::{
|
use crate::{
|
||||||
datatypes::{
|
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.
|
/// 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 {
|
pub struct Adf {
|
||||||
// TODO: none of this should be public
|
ordering: VarContainer,
|
||||||
pub ordering: VarContainer,
|
bdd: Bdd,
|
||||||
pub bdd: Bdd,
|
ac: Vec<Term>,
|
||||||
pub ac: Vec<Term>,
|
|
||||||
#[serde(skip, default = "Adf::default_rng")]
|
#[serde(skip, default = "Adf::default_rng")]
|
||||||
rng: RefCell<StdRng>,
|
rng: RefCell<StdRng>,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[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<usize, String>,
|
||||||
|
// every node gets this label containing multiple entries (it might be empty)
|
||||||
|
tree_root_labels: HashMap<usize, Vec<String>>,
|
||||||
|
lo_edges: Vec<(usize, usize)>,
|
||||||
|
hi_edges: Vec<(usize, usize)>,
|
||||||
|
}
|
||||||
|
|
||||||
impl Default for Adf {
|
impl Default for Adf {
|
||||||
fn default() -> Self {
|
fn default() -> Self {
|
||||||
Self {
|
Self {
|
||||||
@ -920,6 +932,104 @@ impl Adf {
|
|||||||
log::info!("{ng_store}");
|
log::info!("{ng_store}");
|
||||||
log::debug!("{:?}", ng_store);
|
log::debug!("{:?}", ng_store);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Turns Adf into solved graph representation
|
||||||
|
pub fn into_double_labeled_graph(&self, ac: Option<&Vec<Term>>) -> DoubleLabeledGraph {
|
||||||
|
let ac: &Vec<Term> = match ac {
|
||||||
|
Some(ac) => ac,
|
||||||
|
None => &self.ac,
|
||||||
|
};
|
||||||
|
|
||||||
|
let mut node_indices: HashSet<usize> = HashSet::new();
|
||||||
|
let mut new_node_indices: HashSet<usize> = 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<usize, String> = 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<usize, Vec<String>> = 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)]
|
#[cfg(test)]
|
||||||
|
|||||||
@ -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.
|
/// Each roBDD is identified by its corresponding [`Term`], which implicitly identifies the root node of a roBDD.
|
||||||
#[derive(Debug, Serialize, Deserialize)]
|
#[derive(Debug, Serialize, Deserialize)]
|
||||||
pub struct Bdd {
|
pub struct Bdd {
|
||||||
// TODO: use this again
|
pub(crate) nodes: Vec<BddNode>,
|
||||||
// pub(crate) nodes: Vec<BddNode>,
|
|
||||||
pub nodes: Vec<BddNode>,
|
|
||||||
#[cfg(feature = "variablelist")]
|
#[cfg(feature = "variablelist")]
|
||||||
#[serde(skip)]
|
#[serde(skip)]
|
||||||
var_deps: Vec<HashSet<Var>>,
|
var_deps: Vec<HashSet<Var>>,
|
||||||
|
|||||||
@ -1,32 +1,27 @@
|
|||||||
use actix_files as fs;
|
use actix_files as fs;
|
||||||
use actix_web::{post, web, App, HttpServer, Responder};
|
use actix_web::{post, web, App, HttpServer, Responder};
|
||||||
use serde::{Deserialize, Serialize};
|
use serde::{Deserialize, Serialize};
|
||||||
use std::collections::{HashMap, HashSet};
|
|
||||||
|
|
||||||
#[cfg(feature = "cors_for_local_development")]
|
#[cfg(feature = "cors_for_local_development")]
|
||||||
use actix_cors::Cors;
|
use actix_cors::Cors;
|
||||||
#[cfg(feature = "cors_for_local_development")]
|
#[cfg(feature = "cors_for_local_development")]
|
||||||
use actix_web::http;
|
use actix_web::http;
|
||||||
|
|
||||||
use adf_bdd::adf::Adf;
|
use adf_bdd::adf::{Adf, DoubleLabeledGraph};
|
||||||
use adf_bdd::datatypes::Var;
|
|
||||||
use adf_bdd::parser::AdfParser;
|
use adf_bdd::parser::AdfParser;
|
||||||
|
|
||||||
#[derive(Serialize)]
|
#[derive(Deserialize)]
|
||||||
// This is a DTO for the graph output
|
enum Strategy {
|
||||||
struct DoubleLabeledGraph {
|
ParseOnly,
|
||||||
// number of nodes equals the number of node labels
|
Ground,
|
||||||
// nodes implicitly have their index as their ID
|
FirstComplete,
|
||||||
node_labels: HashMap<usize, String>,
|
FirstStable,
|
||||||
// every node gets this label containing multiple entries (it might be empty)
|
|
||||||
tree_root_labels: HashMap<usize, Vec<String>>,
|
|
||||||
lo_edges: Vec<(usize, usize)>,
|
|
||||||
hi_edges: Vec<(usize, usize)>,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Deserialize)]
|
#[derive(Deserialize)]
|
||||||
struct SolveReqBody {
|
struct SolveReqBody {
|
||||||
code: String,
|
code: String,
|
||||||
|
strategy: Strategy,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Serialize)]
|
#[derive(Serialize)]
|
||||||
@ -37,6 +32,7 @@ struct SolveResBody {
|
|||||||
#[post("/solve")]
|
#[post("/solve")]
|
||||||
async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
|
async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
|
||||||
let input = &req_body.code;
|
let input = &req_body.code;
|
||||||
|
let strategy = &req_body.strategy;
|
||||||
|
|
||||||
let parser = AdfParser::default();
|
let parser = AdfParser::default();
|
||||||
match parser.parse()(input) {
|
match parser.parse()(input) {
|
||||||
@ -52,98 +48,16 @@ async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
|
|||||||
|
|
||||||
log::debug!("{:?}", adf);
|
log::debug!("{:?}", adf);
|
||||||
|
|
||||||
// TODO: as first test: turn full graph with initial ac into DoubleLabeledGraph DTO and return it
|
let ac = match strategy {
|
||||||
|
Strategy::ParseOnly => None,
|
||||||
// get relevant nodes from bdd and ac
|
Strategy::Ground => Some(adf.grounded()),
|
||||||
let mut node_indices: HashSet<usize> = HashSet::new();
|
// TODO: error handling if no such model exists!
|
||||||
let mut new_node_indices: HashSet<usize> = adf.ac.iter().map(|term| term.value()).collect();
|
Strategy::FirstComplete => Some(adf.complete().next().unwrap()),
|
||||||
|
// TODO: error handling if no such model exists!
|
||||||
while !new_node_indices.is_empty() {
|
Strategy::FirstStable => Some(adf.stable().next().unwrap()),
|
||||||
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<usize, String> =
|
|
||||||
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)
|
let dto = adf.into_double_labeled_graph(ac.as_ref());
|
||||||
})
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
let tree_root_labels: HashMap<usize, Vec<String>> = 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,
|
|
||||||
};
|
|
||||||
|
|
||||||
web::Json(dto)
|
web::Json(dto)
|
||||||
}
|
}
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user