mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Add naive AF support in Web
This commit is contained in:
parent
96ffa42eee
commit
c34e57f3e0
@ -40,6 +40,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
|||||||
const [code, setCode] = useState(PLACEHOLDER);
|
const [code, setCode] = useState(PLACEHOLDER);
|
||||||
const [filename, setFilename] = useState('');
|
const [filename, setFilename] = useState('');
|
||||||
const [parsing, setParsing] = useState<Parsing>('Naive');
|
const [parsing, setParsing] = useState<Parsing>('Naive');
|
||||||
|
const [isAf, setIsAf] = useState(false);
|
||||||
const [name, setName] = useState('');
|
const [name, setName] = useState('');
|
||||||
const fileRef = useRef<HTMLInputElement>(null);
|
const fileRef = useRef<HTMLInputElement>(null);
|
||||||
|
|
||||||
@ -59,6 +60,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
|||||||
}
|
}
|
||||||
|
|
||||||
formData.append('parsing', parsing);
|
formData.append('parsing', parsing);
|
||||||
|
formData.append('is_af', isAf);
|
||||||
formData.append('name', name);
|
formData.append('name', name);
|
||||||
|
|
||||||
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/add`, {
|
fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/add`, {
|
||||||
@ -119,10 +121,13 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
|||||||
label="Put your code here:"
|
label="Put your code here:"
|
||||||
helperText={(
|
helperText={(
|
||||||
<>
|
<>
|
||||||
For more info on the syntax, have a
|
For more info on the ADF syntax, have a
|
||||||
look
|
look
|
||||||
{' '}
|
{' '}
|
||||||
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noopener noreferrer">here</Link>
|
<Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noopener noreferrer">here</Link>
|
||||||
|
. For the AF syntax, we currently only allow the ICCMA competition format, see for example
|
||||||
|
{' '}
|
||||||
|
<Link href="https://argumentationcompetition.org/2025/rules.html" target="_blank" rel="noopener noreferrer">here</Link>
|
||||||
.
|
.
|
||||||
</>
|
</>
|
||||||
)}
|
)}
|
||||||
@ -137,6 +142,20 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
|
|||||||
|
|
||||||
<Container sx={{ marginTop: 2 }}>
|
<Container sx={{ marginTop: 2 }}>
|
||||||
<Stack direction="row" justifyContent="center" spacing={2}>
|
<Stack direction="row" justifyContent="center" spacing={2}>
|
||||||
|
<FormControl>
|
||||||
|
<FormLabel id="isAf-radio-group">ADF or AF?</FormLabel>
|
||||||
|
<RadioGroup
|
||||||
|
row
|
||||||
|
aria-labelledby="isAf-radio-group"
|
||||||
|
name="isAf"
|
||||||
|
value={isAf}
|
||||||
|
onChange={(e) => setIsAf(((e.target as HTMLInputElement).value))}
|
||||||
|
>
|
||||||
|
<FormControlLabel value={false} control={<Radio />} label="ADF" />
|
||||||
|
<FormControlLabel value={true} control={<Radio />} label="AF" />
|
||||||
|
</RadioGroup>
|
||||||
|
<span style={{ fontSize: "0.7em" }}>AFs are converted to ADFs internally.</span>
|
||||||
|
</FormControl>
|
||||||
<FormControl>
|
<FormControl>
|
||||||
<FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
|
<FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
|
||||||
<RadioGroup
|
<RadioGroup
|
||||||
|
|||||||
@ -21,3 +21,17 @@ The `Parsing Strategy` determines the internal implementation used for these. `N
|
|||||||
You will get a view on the BDD in the detail view after you added the problem.
|
You will get a view on the BDD in the detail view after you added the problem.
|
||||||
|
|
||||||
You can optionally set a name for you ADF problem. Otherwise a random name will be chosen. At the moment the name cannot be changed later (but you could remove and re-add the problem).
|
You can optionally set a name for you ADF problem. Otherwise a random name will be chosen. At the moment the name cannot be changed later (but you could remove and re-add the problem).
|
||||||
|
|
||||||
|
We also support adding AFs in the ICCMA competition format. They are converted to ADFs internally in the obvious way.
|
||||||
|
For example you can try the following code and change the option below from ADF to AF.
|
||||||
|
|
||||||
|
```
|
||||||
|
p af 5
|
||||||
|
# this is a comment
|
||||||
|
1 2
|
||||||
|
2 4
|
||||||
|
4 5
|
||||||
|
5 4
|
||||||
|
5 5
|
||||||
|
```
|
||||||
|
|
||||||
|
|||||||
@ -1,3 +1,4 @@
|
|||||||
|
use std::cell::RefCell;
|
||||||
use std::collections::{HashMap, HashSet};
|
use std::collections::{HashMap, HashSet};
|
||||||
use std::sync::{Arc, RwLock};
|
use std::sync::{Arc, RwLock};
|
||||||
#[cfg(feature = "mock_long_computations")]
|
#[cfg(feature = "mock_long_computations")]
|
||||||
@ -11,7 +12,7 @@ use actix_web::rt::time::timeout;
|
|||||||
use actix_web::{delete, get, 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 futures_util::{FutureExt, TryFutureExt, 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 mongodb::results::DeleteResult;
|
||||||
@ -21,7 +22,7 @@ use serde::{Deserialize, Serialize};
|
|||||||
use adf_bdd::adf::Adf;
|
use adf_bdd::adf::Adf;
|
||||||
use adf_bdd::adfbiodivine::Adf as BdAdf;
|
use adf_bdd::adfbiodivine::Adf as BdAdf;
|
||||||
use adf_bdd::obdd::Bdd;
|
use adf_bdd::obdd::Bdd;
|
||||||
use adf_bdd::parser::AdfParser;
|
use adf_bdd::parser::{AdfParser, Formula};
|
||||||
|
|
||||||
use crate::config::{AppState, RunningInfo, Task, ADF_COLL, COMPUTE_TIME, DB_NAME, USER_COLL};
|
use crate::config::{AppState, RunningInfo, Task, ADF_COLL, COMPUTE_TIME, DB_NAME, USER_COLL};
|
||||||
use crate::user::{username_exists, User};
|
use crate::user::{username_exists, User};
|
||||||
@ -205,6 +206,8 @@ pub(crate) struct AdfProblem {
|
|||||||
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,
|
||||||
|
#[serde(default)]
|
||||||
|
pub(crate) is_af: bool,
|
||||||
pub(crate) adf: SimplifiedAdfOpt,
|
pub(crate) adf: SimplifiedAdfOpt,
|
||||||
pub(crate) acs_per_strategy: AcsPerStrategy,
|
pub(crate) acs_per_strategy: AcsPerStrategy,
|
||||||
}
|
}
|
||||||
@ -215,6 +218,7 @@ struct AddAdfProblemBodyMultipart {
|
|||||||
code: Option<Text<String>>, // Either Code or File is set
|
code: Option<Text<String>>, // Either Code or File is set
|
||||||
file: Option<TempFile>, // Either Code or File is set
|
file: Option<TempFile>, // Either Code or File is set
|
||||||
parsing: Text<Parsing>,
|
parsing: Text<Parsing>,
|
||||||
|
is_af: Text<bool>, // if its not an AF then it is an ADF
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Clone)]
|
#[derive(Clone)]
|
||||||
@ -222,6 +226,7 @@ struct AddAdfProblemBodyPlain {
|
|||||||
name: String,
|
name: String,
|
||||||
code: String,
|
code: String,
|
||||||
parsing: Parsing,
|
parsing: Parsing,
|
||||||
|
is_af: bool, // if its not an AF then it is an ADF
|
||||||
}
|
}
|
||||||
|
|
||||||
impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
|
impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
|
||||||
@ -237,6 +242,7 @@ impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
|
|||||||
.and_then(|code| (!code.is_empty()).then_some(code))
|
.and_then(|code| (!code.is_empty()).then_some(code))
|
||||||
.ok_or("Either a file or the code has to be provided.")?,
|
.ok_or("Either a file or the code has to be provided.")?,
|
||||||
parsing: source.parsing.into_inner(),
|
parsing: source.parsing.into_inner(),
|
||||||
|
is_af: source.is_af.into_inner(),
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -259,6 +265,7 @@ struct AdfProblemInfo {
|
|||||||
name: String,
|
name: String,
|
||||||
code: String,
|
code: String,
|
||||||
parsing_used: Parsing,
|
parsing_used: Parsing,
|
||||||
|
is_af: bool,
|
||||||
acs_per_strategy: AcsPerStrategy,
|
acs_per_strategy: AcsPerStrategy,
|
||||||
running_tasks: Vec<Task>,
|
running_tasks: Vec<Task>,
|
||||||
}
|
}
|
||||||
@ -269,6 +276,7 @@ impl AdfProblemInfo {
|
|||||||
name: adf.name.clone(),
|
name: adf.name.clone(),
|
||||||
code: adf.code,
|
code: adf.code,
|
||||||
parsing_used: adf.parsing_used,
|
parsing_used: adf.parsing_used,
|
||||||
|
is_af: adf.is_af,
|
||||||
acs_per_strategy: adf.acs_per_strategy,
|
acs_per_strategy: adf.acs_per_strategy,
|
||||||
running_tasks: tasks
|
running_tasks: tasks
|
||||||
.iter()
|
.iter()
|
||||||
@ -280,6 +288,91 @@ impl AdfProblemInfo {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
struct AF(Vec<Vec<usize>>);
|
||||||
|
|
||||||
|
impl From<AF> for AdfParser {
|
||||||
|
fn from(source: AF) -> Self {
|
||||||
|
let names: Vec<String> = (0..source.0.len())
|
||||||
|
.map(|val| (val + 1).to_string())
|
||||||
|
.collect();
|
||||||
|
let dict: HashMap<String, usize> = names
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.map(|(i, val)| (val.clone(), i))
|
||||||
|
.collect();
|
||||||
|
let formulae: Vec<Formula> = source
|
||||||
|
.0
|
||||||
|
.into_iter()
|
||||||
|
.map(|attackers| {
|
||||||
|
attackers.into_iter().fold(
|
||||||
|
// TODO: is it correct to use Top here? what if something is not attacked at all?
|
||||||
|
Formula::Top,
|
||||||
|
|acc, attacker| {
|
||||||
|
Formula::And(
|
||||||
|
Box::new(acc),
|
||||||
|
Box::new(Formula::Not(Box::new(Formula::Atom(
|
||||||
|
(attacker + 1).to_string(),
|
||||||
|
)))),
|
||||||
|
)
|
||||||
|
},
|
||||||
|
)
|
||||||
|
})
|
||||||
|
.collect();
|
||||||
|
let formulanames = names.clone();
|
||||||
|
|
||||||
|
Self {
|
||||||
|
namelist: Arc::new(RwLock::new(names)),
|
||||||
|
dict: Arc::new(RwLock::new(dict)),
|
||||||
|
formulae: RefCell::new(formulae),
|
||||||
|
formulaname: RefCell::new(formulanames),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn parse_af(code: String) -> Result<AdfParser, &'static str> {
|
||||||
|
let mut lines = code.lines();
|
||||||
|
|
||||||
|
let Some(first_line) = lines.next() else {
|
||||||
|
return Err("There must be at least one line in the AF input.");
|
||||||
|
};
|
||||||
|
|
||||||
|
let first_line: Vec<_> = first_line.split(" ").collect();
|
||||||
|
if first_line[0] != "p" || first_line[1] != "af" {
|
||||||
|
return Err("Expected first line to be of the form: p af <n>");
|
||||||
|
}
|
||||||
|
|
||||||
|
let Ok(num_arguments) = first_line[2].parse::<usize>() else {
|
||||||
|
return Err("Could not convert number of arguments to u32; expected first line to be of the form: p af <n>");
|
||||||
|
};
|
||||||
|
|
||||||
|
let attacks_opt: Option<Vec<(usize, usize)>> = lines
|
||||||
|
.filter(|line| !line.starts_with('#') && !line.is_empty())
|
||||||
|
.map(|line| {
|
||||||
|
let mut line = line.split(" ");
|
||||||
|
let a = line.next()?;
|
||||||
|
let b = line.next()?;
|
||||||
|
if line.next().is_some() {
|
||||||
|
None
|
||||||
|
} else {
|
||||||
|
Some((a.parse::<usize>().ok()?, b.parse::<usize>().ok()?))
|
||||||
|
}
|
||||||
|
})
|
||||||
|
.collect();
|
||||||
|
let Some(attacks) = attacks_opt else {
|
||||||
|
return Err("Line must be of the form: n m");
|
||||||
|
};
|
||||||
|
|
||||||
|
// index in outer vector represents attacked element
|
||||||
|
let mut is_attacked_by: Vec<Vec<usize>> = vec![vec![]; num_arguments];
|
||||||
|
for (a, b) in attacks {
|
||||||
|
is_attacked_by[b - 1].push(a - 1); // we normalize names to be zero-indexed
|
||||||
|
}
|
||||||
|
|
||||||
|
let hacked_adf_parser = AdfParser::from(AF(is_attacked_by));
|
||||||
|
|
||||||
|
Ok(hacked_adf_parser)
|
||||||
|
}
|
||||||
|
|
||||||
#[post("/add")]
|
#[post("/add")]
|
||||||
async fn add_adf_problem(
|
async fn add_adf_problem(
|
||||||
req: HttpRequest,
|
req: HttpRequest,
|
||||||
@ -381,6 +474,7 @@ async fn add_adf_problem(
|
|||||||
username: username.clone(),
|
username: username.clone(),
|
||||||
code: adf_problem_input.code.clone(),
|
code: adf_problem_input.code.clone(),
|
||||||
parsing_used: adf_problem_input.parsing,
|
parsing_used: adf_problem_input.parsing,
|
||||||
|
is_af: adf_problem_input.is_af,
|
||||||
adf: SimplifiedAdfOpt::None,
|
adf: SimplifiedAdfOpt::None,
|
||||||
acs_per_strategy: AcsPerStrategy::default(),
|
acs_per_strategy: AcsPerStrategy::default(),
|
||||||
};
|
};
|
||||||
@ -413,9 +507,20 @@ async fn add_adf_problem(
|
|||||||
#[cfg(feature = "mock_long_computations")]
|
#[cfg(feature = "mock_long_computations")]
|
||||||
std::thread::sleep(Duration::from_secs(20));
|
std::thread::sleep(Duration::from_secs(20));
|
||||||
|
|
||||||
let parser = AdfParser::default();
|
let (parser, parse_result) = {
|
||||||
let parse_result = parser.parse()(&adf_problem_input.code)
|
if adf_problem_input.is_af {
|
||||||
.map_err(|_| "ADF could not be parsed, double check your input!");
|
parse_af(adf_problem_input.code)
|
||||||
|
.map(|p| (p, Ok(())))
|
||||||
|
.unwrap_or_else(|e| (AdfParser::default(), Err(e)))
|
||||||
|
} else {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let parse_result = parser.parse()(&adf_problem_input.code)
|
||||||
|
.map(|_| ())
|
||||||
|
.map_err(|_| "ADF could not be parsed, double check your input!");
|
||||||
|
|
||||||
|
(parser, parse_result)
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
let result = parse_result.map(|_| {
|
let result = parse_result.map(|_| {
|
||||||
let lib_adf = match adf_problem_input.parsing {
|
let lib_adf = match adf_problem_input.parsing {
|
||||||
@ -500,7 +605,7 @@ async fn solve_adf_problem(
|
|||||||
.collection(ADF_COLL);
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
let username = match identity.map(|id| id.id()) {
|
let username = match identity.map(|id| id.id()) {
|
||||||
None => {
|
Option::None => {
|
||||||
return HttpResponse::Unauthorized().body("You need to login to add an ADF problem.")
|
return HttpResponse::Unauthorized().body("You need to login to add an ADF problem.")
|
||||||
}
|
}
|
||||||
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
@ -512,7 +617,7 @@ async fn solve_adf_problem(
|
|||||||
.await
|
.await
|
||||||
{
|
{
|
||||||
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
Ok(None) => {
|
Ok(Option::None) => {
|
||||||
return HttpResponse::NotFound()
|
return HttpResponse::NotFound()
|
||||||
.body(format!("ADF problem with name {problem_name} not found."))
|
.body(format!("ADF problem with name {problem_name} not found."))
|
||||||
}
|
}
|
||||||
@ -644,7 +749,7 @@ async fn get_adf_problem(
|
|||||||
.collection(ADF_COLL);
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
let username = match identity.map(|id| id.id()) {
|
let username = match identity.map(|id| id.id()) {
|
||||||
None => {
|
Option::None => {
|
||||||
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
||||||
}
|
}
|
||||||
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
@ -656,7 +761,7 @@ async fn get_adf_problem(
|
|||||||
.await
|
.await
|
||||||
{
|
{
|
||||||
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
Err(err) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
Ok(None) => {
|
Ok(Option::None) => {
|
||||||
return HttpResponse::NotFound()
|
return HttpResponse::NotFound()
|
||||||
.body(format!("ADF problem with name {problem_name} not found."))
|
.body(format!("ADF problem with name {problem_name} not found."))
|
||||||
}
|
}
|
||||||
@ -682,7 +787,7 @@ async fn delete_adf_problem(
|
|||||||
.collection(ADF_COLL);
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
let username = match identity.map(|id| id.id()) {
|
let username = match identity.map(|id| id.id()) {
|
||||||
None => {
|
Option::None => {
|
||||||
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
||||||
}
|
}
|
||||||
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
@ -717,7 +822,7 @@ async fn get_adf_problems_for_user(
|
|||||||
.collection(ADF_COLL);
|
.collection(ADF_COLL);
|
||||||
|
|
||||||
let username = match identity.map(|id| id.id()) {
|
let username = match identity.map(|id| id.id()) {
|
||||||
None => {
|
Option::None => {
|
||||||
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
return HttpResponse::Unauthorized().body("You need to login to get an ADF problem.")
|
||||||
}
|
}
|
||||||
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
Some(Err(err)) => return HttpResponse::InternalServerError().body(err.to_string()),
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user