mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
2 Commits
a0ad716b28
...
46ad9eb3fa
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
46ad9eb3fa | ||
|
|
7e18b6194f |
23
Cargo.lock
generated
23
Cargo.lock
generated
@ -283,6 +283,7 @@ dependencies = [
|
|||||||
"adf_bdd",
|
"adf_bdd",
|
||||||
"argon2",
|
"argon2",
|
||||||
"env_logger 0.9.3",
|
"env_logger 0.9.3",
|
||||||
|
"futures-util",
|
||||||
"log",
|
"log",
|
||||||
"mongodb",
|
"mongodb",
|
||||||
"names",
|
"names",
|
||||||
@ -1143,9 +1144,9 @@ dependencies = [
|
|||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "futures-core"
|
name = "futures-core"
|
||||||
version = "0.3.27"
|
version = "0.3.28"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "86d7a0c1aa76363dac491de0ee99faf6941128376f1cf96f07db7603b7de69dd"
|
checksum = "4bca583b7e26f571124fe5b7561d49cb2868d79116cfa0eefce955557c6fee8c"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "futures-executor"
|
name = "futures-executor"
|
||||||
@ -1160,19 +1161,19 @@ dependencies = [
|
|||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "futures-io"
|
name = "futures-io"
|
||||||
version = "0.3.27"
|
version = "0.3.28"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "89d422fa3cbe3b40dca574ab087abb5bc98258ea57eea3fd6f1fa7162c778b91"
|
checksum = "4fff74096e71ed47f8e023204cfd0aa1289cd54ae5430a9523be060cdb849964"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "futures-macro"
|
name = "futures-macro"
|
||||||
version = "0.3.27"
|
version = "0.3.28"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "3eb14ed937631bd8b8b8977f2c198443447a8355b6e3ca599f38c975e5a963b6"
|
checksum = "89ca545a94061b6365f2c7355b4b32bd20df3ff95f02da9329b34ccc3bd6ee72"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"proc-macro2",
|
"proc-macro2",
|
||||||
"quote",
|
"quote",
|
||||||
"syn 1.0.109",
|
"syn 2.0.8",
|
||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
@ -1183,15 +1184,15 @@ checksum = "ec93083a4aecafb2a80a885c9de1f0ccae9dbd32c2bb54b0c3a65690e0b8d2f2"
|
|||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "futures-task"
|
name = "futures-task"
|
||||||
version = "0.3.27"
|
version = "0.3.28"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "fd65540d33b37b16542a0438c12e6aeead10d4ac5d05bd3f805b8f35ab592879"
|
checksum = "76d3d132be6c0e6aa1534069c705a74a5997a356c0dc2f86a47765e5617c5b65"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "futures-util"
|
name = "futures-util"
|
||||||
version = "0.3.27"
|
version = "0.3.28"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "3ef6b17e481503ec85211fed8f39d1970f128935ca1f814cd32ac4a6842e84ab"
|
checksum = "26b01e40b772d54cf6c6d721c1d1abd0647a0106a12ecaa1c186273392a69533"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"futures-core",
|
"futures-core",
|
||||||
"futures-io",
|
"futures-io",
|
||||||
|
|||||||
@ -24,7 +24,8 @@ actix-identity = "0.5.2"
|
|||||||
argon2 = "0.5.0"
|
argon2 = "0.5.0"
|
||||||
actix-session = { version="0.7.2", features = ["cookie-session"] }
|
actix-session = { version="0.7.2", features = ["cookie-session"] }
|
||||||
names = "0.14.0"
|
names = "0.14.0"
|
||||||
|
futures-util = "0.3.28"
|
||||||
|
|
||||||
[features]
|
[features]
|
||||||
cors_for_local_development = []
|
cors_for_local_development = []
|
||||||
|
mock_long_computations = []
|
||||||
|
|||||||
@ -1,14 +1,19 @@
|
|||||||
use std::collections::HashMap;
|
use std::collections::{HashMap, HashSet};
|
||||||
use std::sync::{Arc, RwLock};
|
use std::sync::{Arc, RwLock};
|
||||||
|
#[cfg(feature = "mock_long_computations")]
|
||||||
|
use std::time::Duration;
|
||||||
|
|
||||||
use actix_identity::Identity;
|
use actix_identity::Identity;
|
||||||
|
use actix_web::rt::spawn;
|
||||||
use actix_web::rt::task::spawn_blocking;
|
use actix_web::rt::task::spawn_blocking;
|
||||||
use actix_web::rt::time::timeout;
|
use actix_web::rt::time::timeout;
|
||||||
use actix_web::{post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder};
|
use actix_web::{delete, get, post, put, web, HttpMessage, HttpRequest, HttpResponse, Responder};
|
||||||
use adf_bdd::datatypes::adf::VarContainer;
|
use adf_bdd::datatypes::adf::VarContainer;
|
||||||
use adf_bdd::datatypes::{BddNode, Term, Var};
|
use adf_bdd::datatypes::{BddNode, Term, Var};
|
||||||
|
use futures_util::{FutureExt, TryStreamExt};
|
||||||
use mongodb::bson::doc;
|
use mongodb::bson::doc;
|
||||||
use mongodb::bson::{to_bson, Bson};
|
use mongodb::bson::{to_bson, Bson};
|
||||||
|
use mongodb::results::DeleteResult;
|
||||||
use names::{Generator, Name};
|
use names::{Generator, Name};
|
||||||
use serde::{Deserialize, Serialize};
|
use serde::{Deserialize, Serialize};
|
||||||
|
|
||||||
@ -22,13 +27,13 @@ use crate::user::{username_exists, User};
|
|||||||
type Ac = Vec<Term>;
|
type Ac = Vec<Term>;
|
||||||
type AcDb = Vec<String>;
|
type AcDb = Vec<String>;
|
||||||
|
|
||||||
#[derive(Clone, Deserialize, Serialize)]
|
#[derive(Copy, Clone, Deserialize, Serialize)]
|
||||||
pub(crate) enum Parsing {
|
pub(crate) enum Parsing {
|
||||||
Naive,
|
Naive,
|
||||||
Hybrid,
|
Hybrid,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Clone, PartialEq, Eq, Hash, Deserialize, Serialize)]
|
#[derive(Copy, Clone, PartialEq, Eq, Hash, Deserialize, Serialize)]
|
||||||
pub(crate) enum Strategy {
|
pub(crate) enum Strategy {
|
||||||
Ground,
|
Ground,
|
||||||
Complete,
|
Complete,
|
||||||
@ -50,7 +55,27 @@ impl From<AcAndGraph> for Bson {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
type AcsAndGraphsOpt = Option<Vec<AcAndGraph>>;
|
#[derive(Clone, Default, Deserialize, Serialize)]
|
||||||
|
pub(crate) enum OptionWithError<T> {
|
||||||
|
Some(T),
|
||||||
|
Error(String),
|
||||||
|
#[default]
|
||||||
|
None,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T> OptionWithError<T> {
|
||||||
|
fn is_some(&self) -> bool {
|
||||||
|
matches!(self, Self::Some(_))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: Serialize> From<OptionWithError<T>> for Bson {
|
||||||
|
fn from(source: OptionWithError<T>) -> Self {
|
||||||
|
to_bson(&source).expect("Serialization should work")
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
type AcsAndGraphsOpt = OptionWithError<Vec<AcAndGraph>>;
|
||||||
|
|
||||||
#[derive(Default, Deserialize, Serialize)]
|
#[derive(Default, Deserialize, Serialize)]
|
||||||
pub(crate) struct AcsPerStrategy {
|
pub(crate) struct AcsPerStrategy {
|
||||||
@ -63,7 +88,7 @@ pub(crate) struct AcsPerStrategy {
|
|||||||
pub(crate) stable_nogood: AcsAndGraphsOpt,
|
pub(crate) stable_nogood: AcsAndGraphsOpt,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Deserialize, Serialize)]
|
#[derive(Clone, Deserialize, Serialize)]
|
||||||
pub(crate) struct VarContainerDb {
|
pub(crate) struct VarContainerDb {
|
||||||
names: Vec<String>,
|
names: Vec<String>,
|
||||||
mapping: HashMap<String, String>,
|
mapping: HashMap<String, String>,
|
||||||
@ -99,7 +124,7 @@ impl From<VarContainerDb> for VarContainer {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Deserialize, Serialize)]
|
#[derive(Clone, Deserialize, Serialize)]
|
||||||
pub(crate) struct BddNodeDb {
|
pub(crate) struct BddNodeDb {
|
||||||
var: String,
|
var: String,
|
||||||
lo: String,
|
lo: String,
|
||||||
@ -128,7 +153,7 @@ impl From<BddNodeDb> for BddNode {
|
|||||||
|
|
||||||
type SimplifiedBdd = Vec<BddNodeDb>;
|
type SimplifiedBdd = Vec<BddNodeDb>;
|
||||||
|
|
||||||
#[derive(Deserialize, Serialize)]
|
#[derive(Clone, Deserialize, Serialize)]
|
||||||
pub(crate) struct SimplifiedAdf {
|
pub(crate) struct SimplifiedAdf {
|
||||||
pub(crate) ordering: VarContainerDb,
|
pub(crate) ordering: VarContainerDb,
|
||||||
pub(crate) bdd: SimplifiedBdd,
|
pub(crate) bdd: SimplifiedBdd,
|
||||||
@ -145,13 +170,15 @@ impl SimplifiedAdf {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
type SimplifiedAdfOpt = OptionWithError<SimplifiedAdf>;
|
||||||
|
|
||||||
#[derive(Deserialize, Serialize)]
|
#[derive(Deserialize, Serialize)]
|
||||||
pub(crate) struct AdfProblem {
|
pub(crate) struct AdfProblem {
|
||||||
pub(crate) name: String,
|
pub(crate) name: String,
|
||||||
pub(crate) username: String,
|
pub(crate) username: String,
|
||||||
pub(crate) code: String,
|
pub(crate) code: String,
|
||||||
pub(crate) parsing_used: Parsing,
|
pub(crate) parsing_used: Parsing,
|
||||||
pub(crate) adf: SimplifiedAdf,
|
pub(crate) adf: SimplifiedAdfOpt,
|
||||||
pub(crate) acs_per_strategy: AcsPerStrategy,
|
pub(crate) acs_per_strategy: AcsPerStrategy,
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -175,6 +202,32 @@ async fn adf_problem_exists(
|
|||||||
.is_some()
|
.is_some()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[derive(Serialize)]
|
||||||
|
struct AdfProblemInfo {
|
||||||
|
name: String,
|
||||||
|
code: String,
|
||||||
|
parsing_used: Parsing,
|
||||||
|
acs_per_strategy: AcsPerStrategy,
|
||||||
|
running_tasks: Vec<Task>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl AdfProblemInfo {
|
||||||
|
fn from_adf_prob_and_tasks(adf: AdfProblem, tasks: &HashSet<RunningInfo>) -> Self {
|
||||||
|
AdfProblemInfo {
|
||||||
|
name: adf.name.clone(),
|
||||||
|
code: adf.code,
|
||||||
|
parsing_used: adf.parsing_used,
|
||||||
|
acs_per_strategy: adf.acs_per_strategy,
|
||||||
|
running_tasks: tasks
|
||||||
|
.iter()
|
||||||
|
.filter_map(|t| {
|
||||||
|
(t.adf_name == adf.name && t.username == adf.username).then_some(t.task)
|
||||||
|
})
|
||||||
|
.collect(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[post("/add")]
|
#[post("/add")]
|
||||||
async fn add_adf_problem(
|
async fn add_adf_problem(
|
||||||
req: HttpRequest,
|
req: HttpRequest,
|
||||||
@ -271,10 +324,26 @@ async fn add_adf_problem(
|
|||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
let adf_problem_input_clone = adf_problem_input.clone();
|
let adf_problem: AdfProblem = AdfProblem {
|
||||||
|
name: problem_name.clone(),
|
||||||
|
username: username.clone(),
|
||||||
|
code: adf_problem_input.code.clone(),
|
||||||
|
parsing_used: adf_problem_input.parse_strategy,
|
||||||
|
adf: SimplifiedAdfOpt::None,
|
||||||
|
acs_per_strategy: AcsPerStrategy::default(),
|
||||||
|
};
|
||||||
|
|
||||||
|
let result = adf_coll.insert_one(&adf_problem, None).await;
|
||||||
|
|
||||||
|
if let Err(err) = result {
|
||||||
|
return HttpResponse::InternalServerError()
|
||||||
|
.body(format!("Could not create Database entry. Error: {err}"));
|
||||||
|
}
|
||||||
|
|
||||||
let username_clone = username.clone();
|
let username_clone = username.clone();
|
||||||
let problem_name_clone = problem_name.clone();
|
let problem_name_clone = problem_name.clone();
|
||||||
let adf_res = timeout(
|
|
||||||
|
let adf_fut = timeout(
|
||||||
COMPUTE_TIME,
|
COMPUTE_TIME,
|
||||||
spawn_blocking(move || {
|
spawn_blocking(move || {
|
||||||
let running_info = RunningInfo {
|
let running_info = RunningInfo {
|
||||||
@ -289,11 +358,14 @@ async fn add_adf_problem(
|
|||||||
.unwrap()
|
.unwrap()
|
||||||
.insert(running_info.clone());
|
.insert(running_info.clone());
|
||||||
|
|
||||||
|
#[cfg(feature = "mock_long_computations")]
|
||||||
|
std::thread::sleep(Duration::from_secs(20));
|
||||||
|
|
||||||
let parser = AdfParser::default();
|
let parser = AdfParser::default();
|
||||||
parser.parse()(&adf_problem_input_clone.code)
|
parser.parse()(&adf_problem_input.code)
|
||||||
.map_err(|_| "ADF could not be parsed, double check your input!")?;
|
.map_err(|_| "ADF could not be parsed, double check your input!")?;
|
||||||
|
|
||||||
let lib_adf = match adf_problem_input_clone.parse_strategy {
|
let lib_adf = match adf_problem_input.parse_strategy {
|
||||||
Parsing::Naive => Adf::from_parser(&parser),
|
Parsing::Naive => Adf::from_parser(&parser),
|
||||||
Parsing::Hybrid => {
|
Parsing::Hybrid => {
|
||||||
let bd_adf = BdAdf::from_parser(&parser);
|
let bd_adf = BdAdf::from_parser(&parser);
|
||||||
@ -301,46 +373,55 @@ 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),
|
||||||
|
};
|
||||||
|
|
||||||
app_state
|
app_state
|
||||||
.currently_running
|
.currently_running
|
||||||
.lock()
|
.lock()
|
||||||
.unwrap()
|
.unwrap()
|
||||||
.remove(&running_info);
|
.remove(&running_info);
|
||||||
|
|
||||||
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),
|
|
||||||
};
|
|
||||||
|
|
||||||
Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph))
|
Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph))
|
||||||
}),
|
}),
|
||||||
)
|
);
|
||||||
.await;
|
|
||||||
|
|
||||||
match adf_res {
|
spawn(adf_fut.then(move |adf_res| async move {
|
||||||
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
let (adf, ac_and_graph): (SimplifiedAdfOpt, AcsAndGraphsOpt) = match adf_res {
|
||||||
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
|
Err(err) => (
|
||||||
Ok(Ok(Err(err))) => HttpResponse::InternalServerError().body(err.to_string()),
|
SimplifiedAdfOpt::Error(err.to_string()),
|
||||||
Ok(Ok(Ok((adf, ac_and_graph)))) => {
|
AcsAndGraphsOpt::Error(err.to_string()),
|
||||||
let acs = AcsPerStrategy { parse_only: Some(vec![ac_and_graph]), ..Default::default()};
|
),
|
||||||
|
Ok(Err(err)) => (
|
||||||
|
SimplifiedAdfOpt::Error(err.to_string()),
|
||||||
|
AcsAndGraphsOpt::Error(err.to_string()),
|
||||||
|
),
|
||||||
|
Ok(Ok(Err(err))) => (
|
||||||
|
SimplifiedAdfOpt::Error(err.to_string()),
|
||||||
|
AcsAndGraphsOpt::Error(err.to_string()),
|
||||||
|
),
|
||||||
|
Ok(Ok(Ok((adf, ac_and_graph)))) => (
|
||||||
|
SimplifiedAdfOpt::Some(adf),
|
||||||
|
AcsAndGraphsOpt::Some(vec![ac_and_graph]),
|
||||||
|
),
|
||||||
|
};
|
||||||
|
|
||||||
let adf_problem: AdfProblem = AdfProblem {
|
let result = adf_coll
|
||||||
name: problem_name,
|
.update_one(
|
||||||
username,
|
doc! { "name": problem_name, "username": username },
|
||||||
code: adf_problem_input.code,
|
doc! { "$set": { "adf": &adf, "acs_per_strategy.parse_only": &ac_and_graph } },
|
||||||
parsing_used: adf_problem_input.parse_strategy,
|
None,
|
||||||
adf,
|
)
|
||||||
acs_per_strategy: acs,
|
.await;
|
||||||
};
|
|
||||||
|
|
||||||
let result = adf_coll.insert_one(&adf_problem, None).await;
|
if let Err(err) = result {
|
||||||
|
log::error!("{err}");
|
||||||
match result {
|
|
||||||
Ok(_) => HttpResponse::Ok().json(adf_problem), // TODO: return name of problem here (especially since it may be generated)
|
|
||||||
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}));
|
||||||
|
|
||||||
|
HttpResponse::Ok().body("Parsing started...")
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Deserialize)]
|
#[derive(Deserialize)]
|
||||||
@ -382,6 +463,18 @@ async fn solve_adf_problem(
|
|||||||
Ok(Some(prob)) => prob,
|
Ok(Some(prob)) => prob,
|
||||||
};
|
};
|
||||||
|
|
||||||
|
let simp_adf: SimplifiedAdf = match adf_problem.adf {
|
||||||
|
SimplifiedAdfOpt::None => {
|
||||||
|
return HttpResponse::BadRequest().body("The ADF problem has not been parsed yet.")
|
||||||
|
}
|
||||||
|
SimplifiedAdfOpt::Error(err) => {
|
||||||
|
return HttpResponse::BadRequest().body(format!(
|
||||||
|
"The ADF problem could not be parsed. Update it and try again. Error: {err}"
|
||||||
|
))
|
||||||
|
}
|
||||||
|
SimplifiedAdfOpt::Some(adf) => adf,
|
||||||
|
};
|
||||||
|
|
||||||
let has_been_solved = match adf_problem_input.strategy {
|
let has_been_solved = match adf_problem_input.strategy {
|
||||||
Strategy::Complete => adf_problem.acs_per_strategy.complete.is_some(),
|
Strategy::Complete => adf_problem.acs_per_strategy.complete.is_some(),
|
||||||
Strategy::Ground => adf_problem.acs_per_strategy.ground.is_some(),
|
Strategy::Ground => adf_problem.acs_per_strategy.ground.is_some(),
|
||||||
@ -399,14 +492,14 @@ async fn solve_adf_problem(
|
|||||||
|
|
||||||
let username_clone = username.clone();
|
let username_clone = username.clone();
|
||||||
let problem_name_clone = problem_name.clone();
|
let problem_name_clone = problem_name.clone();
|
||||||
let strategy_clone = adf_problem_input.strategy.clone();
|
|
||||||
let acs_and_graphs_res = timeout(
|
let acs_and_graphs_fut = timeout(
|
||||||
COMPUTE_TIME,
|
COMPUTE_TIME,
|
||||||
spawn_blocking(move || {
|
spawn_blocking(move || {
|
||||||
let running_info = RunningInfo {
|
let running_info = RunningInfo {
|
||||||
username: username_clone,
|
username: username_clone,
|
||||||
adf_name: problem_name_clone,
|
adf_name: problem_name_clone,
|
||||||
task: Task::Solve(strategy_clone.clone()),
|
task: Task::Solve(adf_problem_input.strategy),
|
||||||
};
|
};
|
||||||
|
|
||||||
app_state
|
app_state
|
||||||
@ -415,18 +508,20 @@ async fn solve_adf_problem(
|
|||||||
.unwrap()
|
.unwrap()
|
||||||
.insert(running_info.clone());
|
.insert(running_info.clone());
|
||||||
|
|
||||||
|
#[cfg(feature = "mock_long_computations")]
|
||||||
|
std::thread::sleep(Duration::from_secs(20));
|
||||||
|
|
||||||
let mut adf: Adf = Adf::from_ord_nodes_and_ac(
|
let mut adf: Adf = Adf::from_ord_nodes_and_ac(
|
||||||
adf_problem.adf.ordering.into(),
|
simp_adf.ordering.into(),
|
||||||
adf_problem.adf.bdd.into_iter().map(Into::into).collect(),
|
simp_adf.bdd.into_iter().map(Into::into).collect(),
|
||||||
adf_problem
|
simp_adf
|
||||||
.adf
|
|
||||||
.ac
|
.ac
|
||||||
.into_iter()
|
.into_iter()
|
||||||
.map(|t| Term(t.parse().unwrap()))
|
.map(|t| Term(t.parse().unwrap()))
|
||||||
.collect(),
|
.collect(),
|
||||||
);
|
);
|
||||||
|
|
||||||
let acs: Vec<Ac> = match strategy_clone {
|
let acs: Vec<Ac> = match adf_problem_input.strategy {
|
||||||
Strategy::Complete => adf.complete().collect(),
|
Strategy::Complete => adf.complete().collect(),
|
||||||
Strategy::Ground => vec![adf.grounded()],
|
Strategy::Ground => vec![adf.grounded()],
|
||||||
Strategy::Stable => adf.stable().collect(),
|
Strategy::Stable => adf.stable().collect(),
|
||||||
@ -456,26 +551,143 @@ async fn solve_adf_problem(
|
|||||||
|
|
||||||
acs_and_graphs
|
acs_and_graphs
|
||||||
}),
|
}),
|
||||||
)
|
);
|
||||||
.await;
|
|
||||||
|
|
||||||
match acs_and_graphs_res {
|
spawn(acs_and_graphs_fut.then(move |acs_and_graphs_res| async move {
|
||||||
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
let acs_and_graphs_enum: AcsAndGraphsOpt = match acs_and_graphs_res {
|
||||||
Ok(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
|
Err(err) => AcsAndGraphsOpt::Error(err.to_string()),
|
||||||
Ok(Ok(acs_and_graphs)) => {
|
Ok(Err(err)) => AcsAndGraphsOpt::Error(err.to_string()),
|
||||||
let result = adf_coll.update_one(doc! { "name": &problem_name, "username": &username }, match adf_problem_input.strategy {
|
Ok(Ok(acs_and_graphs)) => AcsAndGraphsOpt::Some(acs_and_graphs),
|
||||||
Strategy::Complete => doc! { "$set": { "acs_per_strategy.complete": Some(&acs_and_graphs) } },
|
};
|
||||||
Strategy::Ground => doc! { "$set": { "acs_per_strategy.ground": Some(&acs_and_graphs) } },
|
|
||||||
Strategy::Stable => doc! { "$set": { "acs_per_strategy.stable": Some(&acs_and_graphs) } },
|
|
||||||
Strategy::StableCountingA => doc! { "$set": { "acs_per_strategy.stable_counting_a": Some(&acs_and_graphs) } },
|
|
||||||
Strategy::StableCountingB => doc! { "$set": { "acs_per_strategy.stable_counting_b": Some(&acs_and_graphs) } },
|
|
||||||
Strategy::StableNogood => doc! { "$set": { "acs_per_strategy.stable_nogood": Some(&acs_and_graphs) } },
|
|
||||||
}, None).await;
|
|
||||||
|
|
||||||
match result {
|
let result = adf_coll.update_one(doc! { "name": problem_name, "username": username }, match adf_problem_input.strategy {
|
||||||
Ok(_) => HttpResponse::Ok().json(acs_and_graphs),
|
Strategy::Complete => doc! { "$set": { "acs_per_strategy.complete": &acs_and_graphs_enum } },
|
||||||
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
Strategy::Ground => doc! { "$set": { "acs_per_strategy.ground": &acs_and_graphs_enum } },
|
||||||
}
|
Strategy::Stable => doc! { "$set": { "acs_per_strategy.stable": &acs_and_graphs_enum } },
|
||||||
|
Strategy::StableCountingA => doc! { "$set": { "acs_per_strategy.stable_counting_a": &acs_and_graphs_enum } },
|
||||||
|
Strategy::StableCountingB => doc! { "$set": { "acs_per_strategy.stable_counting_b": &acs_and_graphs_enum } },
|
||||||
|
Strategy::StableNogood => doc! { "$set": { "acs_per_strategy.stable_nogood": &acs_and_graphs_enum } },
|
||||||
|
}, None).await;
|
||||||
|
|
||||||
|
if let Err(err) = result {
|
||||||
|
log::error!("{err}");
|
||||||
}
|
}
|
||||||
|
}));
|
||||||
|
|
||||||
|
HttpResponse::Ok().body("Solving started...")
|
||||||
|
}
|
||||||
|
|
||||||
|
#[get("/{problem_name}")]
|
||||||
|
async fn get_adf_problem(
|
||||||
|
app_state: web::Data<AppState>,
|
||||||
|
identity: Option<Identity>,
|
||||||
|
path: web::Path<String>,
|
||||||
|
) -> impl Responder {
|
||||||
|
let problem_name = path.into_inner();
|
||||||
|
let adf_coll: mongodb::Collection<AdfProblem> = app_state
|
||||||
|
.mongodb_client
|
||||||
|
.database(DB_NAME)
|
||||||
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
|
let username = match identity.map(|id| id.id()) {
|
||||||
|
None => {
|
||||||
|
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
||||||
|
}
|
||||||
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
Some(Ok(username)) => username,
|
||||||
|
};
|
||||||
|
|
||||||
|
let adf_problem = match adf_coll
|
||||||
|
.find_one(doc! { "name": &problem_name, "username": &username }, None)
|
||||||
|
.await
|
||||||
|
{
|
||||||
|
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
Ok(None) => {
|
||||||
|
return HttpResponse::NotFound()
|
||||||
|
.body(format!("ADF problem with name {problem_name} not found."))
|
||||||
|
}
|
||||||
|
Ok(Some(prob)) => prob,
|
||||||
|
};
|
||||||
|
|
||||||
|
HttpResponse::Ok().json(AdfProblemInfo::from_adf_prob_and_tasks(
|
||||||
|
adf_problem,
|
||||||
|
&app_state.currently_running.lock().unwrap(),
|
||||||
|
))
|
||||||
|
}
|
||||||
|
|
||||||
|
#[delete("/{problem_name}")]
|
||||||
|
async fn delete_adf_problem(
|
||||||
|
app_state: web::Data<AppState>,
|
||||||
|
identity: Option<Identity>,
|
||||||
|
path: web::Path<String>,
|
||||||
|
) -> impl Responder {
|
||||||
|
let problem_name = path.into_inner();
|
||||||
|
let adf_coll: mongodb::Collection<AdfProblem> = app_state
|
||||||
|
.mongodb_client
|
||||||
|
.database(DB_NAME)
|
||||||
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
|
let username = match identity.map(|id| id.id()) {
|
||||||
|
None => {
|
||||||
|
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
||||||
|
}
|
||||||
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
Some(Ok(username)) => username,
|
||||||
|
};
|
||||||
|
|
||||||
|
match adf_coll
|
||||||
|
.delete_one(doc! { "name": &problem_name, "username": &username }, None)
|
||||||
|
.await
|
||||||
|
{
|
||||||
|
Ok(DeleteResult {
|
||||||
|
deleted_count: 0, ..
|
||||||
|
}) => HttpResponse::InternalServerError().body("Adf Problem could not be deleted."),
|
||||||
|
Ok(DeleteResult {
|
||||||
|
deleted_count: 1, ..
|
||||||
|
}) => HttpResponse::Ok().body("Adf Problem deleted."),
|
||||||
|
Ok(_) => {
|
||||||
|
unreachable!("delete_one removes at most one entry so all cases are covered already")
|
||||||
|
}
|
||||||
|
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[get("/")]
|
||||||
|
async fn get_adf_problems_for_user(
|
||||||
|
app_state: web::Data<AppState>,
|
||||||
|
identity: Option<Identity>,
|
||||||
|
) -> impl Responder {
|
||||||
|
let adf_coll: mongodb::Collection<AdfProblem> = app_state
|
||||||
|
.mongodb_client
|
||||||
|
.database(DB_NAME)
|
||||||
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
|
let username = match identity.map(|id| id.id()) {
|
||||||
|
None => {
|
||||||
|
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
||||||
|
}
|
||||||
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
Some(Ok(username)) => username,
|
||||||
|
};
|
||||||
|
|
||||||
|
let adf_problem_cursor = match adf_coll.find(doc! { "username": &username }, None).await {
|
||||||
|
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
Ok(cursor) => cursor,
|
||||||
|
};
|
||||||
|
|
||||||
|
let adf_problems: Vec<AdfProblemInfo> = match adf_problem_cursor
|
||||||
|
.map_ok(|adf_problem| {
|
||||||
|
AdfProblemInfo::from_adf_prob_and_tasks(
|
||||||
|
adf_problem,
|
||||||
|
&app_state.currently_running.lock().unwrap(),
|
||||||
|
)
|
||||||
|
})
|
||||||
|
.try_collect()
|
||||||
|
.await
|
||||||
|
{
|
||||||
|
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
Ok(probs) => probs,
|
||||||
|
};
|
||||||
|
|
||||||
|
HttpResponse::Ok().json(adf_problems)
|
||||||
|
}
|
||||||
|
|||||||
@ -3,6 +3,7 @@ use std::sync::Mutex;
|
|||||||
use std::time::Duration;
|
use std::time::Duration;
|
||||||
|
|
||||||
use mongodb::Client;
|
use mongodb::Client;
|
||||||
|
use serde::Serialize;
|
||||||
|
|
||||||
use crate::adf::Strategy;
|
use crate::adf::Strategy;
|
||||||
|
|
||||||
@ -16,7 +17,7 @@ pub(crate) const DB_NAME: &str = "adf-obdd";
|
|||||||
pub(crate) const USER_COLL: &str = "users";
|
pub(crate) const USER_COLL: &str = "users";
|
||||||
pub(crate) const ADF_COLL: &str = "adf-problems";
|
pub(crate) const ADF_COLL: &str = "adf-problems";
|
||||||
|
|
||||||
#[derive(Clone, PartialEq, Eq, Hash)]
|
#[derive(Copy, Clone, PartialEq, Eq, Hash, Serialize)]
|
||||||
pub(crate) enum Task {
|
pub(crate) enum Task {
|
||||||
Parse,
|
Parse,
|
||||||
Solve(Strategy),
|
Solve(Strategy),
|
||||||
|
|||||||
@ -17,7 +17,10 @@ mod adf;
|
|||||||
mod config;
|
mod config;
|
||||||
mod user;
|
mod user;
|
||||||
|
|
||||||
use adf::{add_adf_problem, solve_adf_problem};
|
use adf::{
|
||||||
|
add_adf_problem, delete_adf_problem, get_adf_problem, get_adf_problems_for_user,
|
||||||
|
solve_adf_problem,
|
||||||
|
};
|
||||||
use config::{AppState, ASSET_DIRECTORY, COOKIE_DURATION};
|
use config::{AppState, ASSET_DIRECTORY, COOKIE_DURATION};
|
||||||
use user::{
|
use user::{
|
||||||
create_username_index, delete_account, login, logout, register, update_user, user_info,
|
create_username_index, delete_account, login, logout, register, update_user, user_info,
|
||||||
@ -82,7 +85,10 @@ async fn main() -> std::io::Result<()> {
|
|||||||
.service(
|
.service(
|
||||||
web::scope("/adf")
|
web::scope("/adf")
|
||||||
.service(add_adf_problem)
|
.service(add_adf_problem)
|
||||||
.service(solve_adf_problem),
|
.service(solve_adf_problem)
|
||||||
|
.service(get_adf_problem)
|
||||||
|
.service(delete_adf_problem)
|
||||||
|
.service(get_adf_problems_for_user),
|
||||||
)
|
)
|
||||||
// this mus be last to not override anything
|
// this mus be last to not override anything
|
||||||
.service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
|
.service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
|
||||||
|
|||||||
@ -280,8 +280,7 @@ async fn update_user(
|
|||||||
Some(id) => match id.id() {
|
Some(id) => match id.id() {
|
||||||
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
Ok(username) => {
|
Ok(username) => {
|
||||||
if user.username != username && username_exists(&user_coll, &user.username).await
|
if user.username != username && username_exists(&user_coll, &user.username).await {
|
||||||
{
|
|
||||||
return HttpResponse::Conflict()
|
return HttpResponse::Conflict()
|
||||||
.body("Username is already taken. Please pick another one!");
|
.body("Username is already taken. Please pick another one!");
|
||||||
}
|
}
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user