ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00
Code Issues Projects Releases Wiki Activity

Support stable model semantics with nogoods

Browse Source
This commit is contained in:
monsterkrampe 2022-09-02 11:45:52 +02:00
parent f27502784a
commit 9ab4ff3de4
No known key found for this signature in database
GPG Key ID: B8ADC1F5A5CE5057
2 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
frontend/src/components/app.tsx
View File

@ -40,6 +40,7 @@ enum Strategy {
Ground = 'Ground',
FirstComplete = 'FirstComplete',
FirstStable = 'FirstStable',
FirstStableNogood = 'FirstStableNogood',
}
function App() {
@ -73,7 +74,7 @@ function App() {
<CssBaseline />
<main>
<Typography variant="h2" component="h1" align="center" gutterBottom>
Solve your ADF Problem with Style!
Solve your ADF Problem with OBDDs!
</Typography>
<Container>
@ -101,6 +102,8 @@ function App() {
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstComplete)}>(First) Complete Model</Button>
{' '}
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStable)}>(First) Stable Model</Button>
{' '}
<Button variant="outlined" onClick={() => submitHandler(Strategy.FirstStableNogood)}>(First) Stable Model using nogoods</Button>
</Container>
{graph

4
server/src/main.rs
View File

@ -16,6 +16,7 @@ enum Strategy {
Ground,
FirstComplete,
FirstStable,
FirstStableNogood,
}
#[derive(Deserialize)]
@ -55,6 +56,9 @@ async fn solve(req_body: web::Json<SolveReqBody>) -> impl Responder {
Strategy::FirstComplete => Some(adf.complete().next().unwrap()),
// TODO: error handling if no such model exists!
Strategy::FirstStable => Some(adf.stable().next().unwrap()),
// TODO: error handling if no such model exists!
// TODO: support more than just default heuristics
Strategy::FirstStableNogood => Some(adf.stable_nogood(adf_bdd::adf::heuristics::Heuristic::default()).next().unwrap()),
};
let dto = adf.into_double_labeled_graph(ac.as_ref());