mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Continue implementing basic solving endpoint
This commit is contained in:
parent
f796337839
commit
cdd21f7e4f
16
Cargo.lock
generated
16
Cargo.lock
generated
@ -19,6 +19,21 @@ dependencies = [
|
|||||||
"tokio-util",
|
"tokio-util",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "actix-cors"
|
||||||
|
version = "0.6.2"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "02a0adcaabb68f1dfe8880cb3c5f049261c68f5d69ce06b6f3a930f31710838e"
|
||||||
|
dependencies = [
|
||||||
|
"actix-utils",
|
||||||
|
"actix-web",
|
||||||
|
"derive_more",
|
||||||
|
"futures-util",
|
||||||
|
"log",
|
||||||
|
"once_cell",
|
||||||
|
"smallvec",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "actix-http"
|
name = "actix-http"
|
||||||
version = "3.3.1"
|
version = "3.3.1"
|
||||||
@ -204,6 +219,7 @@ dependencies = [
|
|||||||
name = "adf-bdd-server"
|
name = "adf-bdd-server"
|
||||||
version = "0.3.0"
|
version = "0.3.0"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
|
"actix-cors",
|
||||||
"actix-web",
|
"actix-web",
|
||||||
"adf_bdd",
|
"adf_bdd",
|
||||||
"env_logger 0.9.3",
|
"env_logger 0.9.3",
|
||||||
|
|||||||
@ -30,9 +30,10 @@ 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 {
|
||||||
ordering: VarContainer,
|
// TODO: none of this should be public
|
||||||
bdd: Bdd,
|
pub ordering: VarContainer,
|
||||||
ac: Vec<Term>,
|
pub bdd: Bdd,
|
||||||
|
pub ac: Vec<Term>,
|
||||||
#[serde(skip, default = "Adf::default_rng")]
|
#[serde(skip, default = "Adf::default_rng")]
|
||||||
rng: RefCell<StdRng>,
|
rng: RefCell<StdRng>,
|
||||||
}
|
}
|
||||||
|
|||||||
@ -13,7 +13,9 @@ 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 {
|
||||||
pub(crate) nodes: Vec<BddNode>,
|
// TODO: use this again
|
||||||
|
// 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>>,
|
||||||
|
|||||||
@ -14,6 +14,7 @@ description = "Offer Solving ADFs as a service"
|
|||||||
[dependencies]
|
[dependencies]
|
||||||
adf_bdd = { version="0.3.1", path="../lib", features = ["frontend"] }
|
adf_bdd = { version="0.3.1", path="../lib", features = ["frontend"] }
|
||||||
actix-web = "4"
|
actix-web = "4"
|
||||||
|
actix-cors = "0.6"
|
||||||
env_logger = "0.9"
|
env_logger = "0.9"
|
||||||
log = "0.4"
|
log = "0.4"
|
||||||
serde = "1"
|
serde = "1"
|
||||||
|
|||||||
@ -1,7 +1,11 @@
|
|||||||
use actix_web::{get, post, web, App, HttpResponse, HttpServer, Responder};
|
use actix_cors::Cors;
|
||||||
|
use actix_web::{get, http, post, web, App, HttpResponse, HttpServer, Responder};
|
||||||
use serde::{Deserialize, Serialize};
|
use serde::{Deserialize, Serialize};
|
||||||
|
use std::collections::{HashMap, HashSet};
|
||||||
|
|
||||||
use adf_bdd::adf::Adf;
|
use adf_bdd::adf::Adf;
|
||||||
|
use adf_bdd::datatypes::BddNode;
|
||||||
|
use adf_bdd::datatypes::Var;
|
||||||
use adf_bdd::parser::AdfParser;
|
use adf_bdd::parser::AdfParser;
|
||||||
|
|
||||||
#[get("/")]
|
#[get("/")]
|
||||||
@ -15,15 +19,16 @@ async fn root() -> impl Responder {
|
|||||||
struct DoubleLabeledGraph {
|
struct DoubleLabeledGraph {
|
||||||
// number of nodes equals the number of node labels
|
// number of nodes equals the number of node labels
|
||||||
// nodes implicitly have their index as their ID
|
// nodes implicitly have their index as their ID
|
||||||
node_labels: Vec<String>,
|
node_labels: HashMap<usize, String>,
|
||||||
// every node gets this label containing multiple entries (it might be empty)
|
// every node gets this label containing multiple entries (it might be empty)
|
||||||
tree_root_labels: Vec<Vec<String>>,
|
tree_root_labels: HashMap<usize, Vec<String>>,
|
||||||
edges: Vec<(usize, usize)>,
|
lo_edges: Vec<(usize, usize)>,
|
||||||
|
hi_edges: Vec<(usize, usize)>,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Deserialize)]
|
#[derive(Deserialize)]
|
||||||
struct SolveReqBody {
|
struct SolveReqBody {
|
||||||
adf_input: String,
|
code: String,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Serialize)]
|
#[derive(Serialize)]
|
||||||
@ -33,7 +38,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.adf_input;
|
let input = &req_body.code;
|
||||||
|
|
||||||
let parser = AdfParser::default();
|
let parser = AdfParser::default();
|
||||||
match parser.parse()(input) {
|
match parser.parse()(input) {
|
||||||
@ -51,7 +56,98 @@ async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
|
|||||||
|
|
||||||
// TODO: as first test: turn full graph with initial ac into DoubleLabeledGraph DTO and return it
|
// TODO: as first test: turn full graph with initial ac into DoubleLabeledGraph DTO and return it
|
||||||
|
|
||||||
"Hello World"
|
// get relevant nodes from bdd and ac
|
||||||
|
let mut node_indices: HashSet<usize> = HashSet::new();
|
||||||
|
let mut new_node_indices: HashSet<usize> = 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<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)
|
||||||
|
})
|
||||||
|
.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)
|
||||||
}
|
}
|
||||||
|
|
||||||
#[actix_web::main]
|
#[actix_web::main]
|
||||||
@ -59,8 +155,21 @@ async fn main() -> std::io::Result<()> {
|
|||||||
env_logger::builder()
|
env_logger::builder()
|
||||||
.filter_level(log::LevelFilter::Debug)
|
.filter_level(log::LevelFilter::Debug)
|
||||||
.init();
|
.init();
|
||||||
HttpServer::new(|| App::new().service(root).service(solve))
|
|
||||||
.bind(("127.0.0.1", 8080))?
|
HttpServer::new(|| {
|
||||||
.run()
|
let cors = Cors::default()
|
||||||
.await
|
.allowed_origin("http://localhost:1234")
|
||||||
|
.allowed_methods(vec!["GET", "POST"])
|
||||||
|
.allowed_headers(vec![
|
||||||
|
http::header::AUTHORIZATION,
|
||||||
|
http::header::ACCEPT,
|
||||||
|
http::header::CONTENT_TYPE,
|
||||||
|
])
|
||||||
|
.max_age(3600);
|
||||||
|
|
||||||
|
App::new().wrap(cors).service(root).service(solve)
|
||||||
|
})
|
||||||
|
.bind(("127.0.0.1", 8080))?
|
||||||
|
.run()
|
||||||
|
.await
|
||||||
}
|
}
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user