mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Give example for custom Adf datastructure in docs
This commit is contained in:
parent
aa189de7b5
commit
1cbd925eb4
@ -8,7 +8,6 @@ This module describes the abstract dialectical framework.
|
||||
pub mod heuristics;
|
||||
use std::cell::RefCell;
|
||||
|
||||
use crate::datatypes::BddNode;
|
||||
use crate::{
|
||||
datatypes::{
|
||||
adf::{
|
||||
@ -52,23 +51,18 @@ impl Default for Adf {
|
||||
}
|
||||
}
|
||||
|
||||
impl Adf {
|
||||
/// Instntiates an ADF based on the publically available data
|
||||
pub fn from_ord_nodes_and_ac(
|
||||
ordering: VarContainer,
|
||||
bdd_nodes: Vec<BddNode>,
|
||||
ac: Vec<Term>,
|
||||
) -> Self {
|
||||
let bdd = Bdd::from_nodes(bdd_nodes);
|
||||
|
||||
Adf {
|
||||
ordering,
|
||||
bdd,
|
||||
ac,
|
||||
impl From<(VarContainer, Bdd, Vec<Term>)> for Adf {
|
||||
fn from(source: (VarContainer, Bdd, Vec<Term>)) -> Self {
|
||||
Self {
|
||||
ordering: source.0,
|
||||
bdd: source.1,
|
||||
ac: source.2,
|
||||
rng: Self::default_rng(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Adf {
|
||||
/// Instantiates a new ADF, based on the [parser-data][crate::parser::AdfParser].
|
||||
pub fn from_parser(parser: &AdfParser) -> Self {
|
||||
log::info!("[Start] instantiating BDD");
|
||||
|
||||
@ -26,7 +26,7 @@ impl Default for VarContainer {
|
||||
}
|
||||
|
||||
impl VarContainer {
|
||||
/// Create [VarContainer] from its components
|
||||
/// Create [`VarContainer`] from its components
|
||||
pub fn from_parser(
|
||||
names: Arc<RwLock<Vec<String>>>,
|
||||
mapping: Arc<RwLock<HashMap<String, usize>>>,
|
||||
@ -52,12 +52,12 @@ impl VarContainer {
|
||||
.and_then(|name| name.get(var.value()).cloned())
|
||||
}
|
||||
|
||||
/// Return ordered names from [VarContainer]
|
||||
/// Return ordered names from [`VarContainer`]
|
||||
pub fn names(&self) -> Arc<RwLock<Vec<String>>> {
|
||||
Arc::clone(&self.names)
|
||||
}
|
||||
|
||||
/// Return map from names to indices in [VarContainer]
|
||||
/// Return map from names to indices in [`VarContainer`]
|
||||
pub fn mappings(&self) -> Arc<RwLock<HashMap<String, usize>>> {
|
||||
Arc::clone(&self.mapping)
|
||||
}
|
||||
|
||||
140
lib/src/lib.rs
140
lib/src/lib.rs
@ -198,6 +198,146 @@ while let Ok(result) = r.recv() {
|
||||
solving.join().unwrap();
|
||||
|
||||
```
|
||||
|
||||
### Serialize and Deserialize custom datastructures representing an [`adf::Adf`]
|
||||
|
||||
The Web Application <https://adf-bdd.dev> uses custom datastructures that are stored in a mongodb which inspired this example.
|
||||
|
||||
```rust
|
||||
use std::sync::{Arc, RwLock};
|
||||
use serde::{Deserialize, Serialize};
|
||||
use std::collections::HashMap;
|
||||
use adf_bdd::datatypes::adf::VarContainer;
|
||||
use adf_bdd::datatypes::{BddNode, Term, Var};
|
||||
use adf_bdd::obdd::Bdd;
|
||||
use adf_bdd::parser::AdfParser;
|
||||
use adf_bdd::adf::Adf;
|
||||
|
||||
// Custom Datastructures for (De-)Serialization
|
||||
|
||||
# #[derive(PartialEq, Debug)]
|
||||
#[derive(Deserialize, Serialize)]
|
||||
struct MyCustomVarContainer {
|
||||
names: Vec<String>,
|
||||
mapping: HashMap<String, String>,
|
||||
}
|
||||
|
||||
impl From<VarContainer> for MyCustomVarContainer {
|
||||
fn from(source: VarContainer) -> Self {
|
||||
Self {
|
||||
names: source.names().read().unwrap().clone(),
|
||||
mapping: source
|
||||
.mappings()
|
||||
.read()
|
||||
.unwrap()
|
||||
.iter()
|
||||
.map(|(k, v)| (k.clone(), v.to_string()))
|
||||
.collect(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl From<MyCustomVarContainer> for VarContainer {
|
||||
fn from(source: MyCustomVarContainer) -> Self {
|
||||
Self::from_parser(
|
||||
Arc::new(RwLock::new(source.names)),
|
||||
Arc::new(RwLock::new(
|
||||
source
|
||||
.mapping
|
||||
.into_iter()
|
||||
.map(|(k, v)| (k, v.parse().unwrap()))
|
||||
.collect(),
|
||||
)),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
# #[derive(PartialEq, Debug)]
|
||||
#[derive(Deserialize, Serialize)]
|
||||
struct MyCustomBddNode {
|
||||
var: String,
|
||||
lo: String,
|
||||
hi: String,
|
||||
}
|
||||
|
||||
impl From<BddNode> for MyCustomBddNode {
|
||||
fn from(source: BddNode) -> Self {
|
||||
Self {
|
||||
var: source.var().0.to_string(),
|
||||
lo: source.lo().0.to_string(),
|
||||
hi: source.hi().0.to_string(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl From<MyCustomBddNode> for BddNode {
|
||||
fn from(source: MyCustomBddNode) -> Self {
|
||||
Self::new(
|
||||
Var(source.var.parse().unwrap()),
|
||||
Term(source.lo.parse().unwrap()),
|
||||
Term(source.hi.parse().unwrap()),
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
# #[derive(PartialEq, Debug)]
|
||||
#[derive(Deserialize, Serialize)]
|
||||
struct MyCustomAdf {
|
||||
ordering: MyCustomVarContainer,
|
||||
bdd: Vec<MyCustomBddNode>,
|
||||
ac: Vec<String>,
|
||||
}
|
||||
|
||||
impl From<Adf> for MyCustomAdf {
|
||||
fn from(source: Adf) -> Self {
|
||||
Self {
|
||||
ordering: source.ordering.into(),
|
||||
bdd: source.bdd.nodes.into_iter().map(Into::into).collect(),
|
||||
ac: source.ac.into_iter().map(|t| t.0.to_string()).collect(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl From<MyCustomAdf> for Adf {
|
||||
fn from(source: MyCustomAdf) -> Self {
|
||||
let bdd = Bdd::from(source.bdd.into_iter().map(Into::into).collect::<Vec<BddNode>>());
|
||||
|
||||
Adf::from((
|
||||
source.ordering.into(),
|
||||
bdd,
|
||||
source
|
||||
.ac
|
||||
.into_iter()
|
||||
.map(|t| Term(t.parse().unwrap()))
|
||||
.collect(),
|
||||
))
|
||||
}
|
||||
}
|
||||
|
||||
// use the above example as input
|
||||
let input = "s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,or(a,b)).ac(c,neg(b)).ac(d,d).";
|
||||
let parser = AdfParser::default();
|
||||
parser.parse()(&input).unwrap();
|
||||
|
||||
// create Adf
|
||||
let adf = Adf::from_parser(&parser);
|
||||
|
||||
// cast into custom struct
|
||||
let my_custom_adf: MyCustomAdf = adf.into();
|
||||
|
||||
// stringify to json
|
||||
let json: String = serde_json::to_string(&my_custom_adf).unwrap();
|
||||
|
||||
// parse json
|
||||
let parsed_custom_adf: MyCustomAdf = serde_json::from_str(&json).unwrap();
|
||||
|
||||
// cast into lib struct that resembles the original Adf
|
||||
let parsed_adf: Adf = parsed_custom_adf.into();
|
||||
|
||||
# let my_custom_adf2: MyCustomAdf = parsed_adf.into();
|
||||
# assert_eq!(my_custom_adf, my_custom_adf2);
|
||||
```
|
||||
|
||||
*/
|
||||
#![deny(
|
||||
missing_debug_implementations,
|
||||
|
||||
@ -82,7 +82,7 @@ impl NoGood {
|
||||
visit.then_some(result)
|
||||
}
|
||||
|
||||
/// Creates an updated [Vec<Term>], based on the given [&[Term]] and the [NoGood].
|
||||
/// Creates an updated [`Vec<Term>`], based on the given [&[Term]] and the [NoGood].
|
||||
/// The parameter _update_ is set to [`true`] if there has been an update and to [`false`] otherwise
|
||||
pub fn update_term_vec(&self, term_vec: &[Term], update: &mut bool) -> Vec<Term> {
|
||||
*update = false;
|
||||
|
||||
@ -13,7 +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.
|
||||
#[derive(Debug, Serialize, Deserialize)]
|
||||
pub struct Bdd {
|
||||
/// The nodes of the [Bdd] with their edges
|
||||
/// The nodes of the [`Bdd`] with their edges
|
||||
pub nodes: Vec<BddNode>,
|
||||
#[cfg(feature = "variablelist")]
|
||||
#[serde(skip)]
|
||||
@ -50,6 +50,18 @@ impl Default for Bdd {
|
||||
}
|
||||
}
|
||||
|
||||
impl From<Vec<BddNode>> for Bdd {
|
||||
fn from(nodes: Vec<BddNode>) -> Self {
|
||||
let mut bdd = Self::new();
|
||||
|
||||
for node in nodes {
|
||||
bdd.node(node.var(), node.lo(), node.hi());
|
||||
}
|
||||
|
||||
bdd
|
||||
}
|
||||
}
|
||||
|
||||
impl Bdd {
|
||||
/// Instantiate a new roBDD structure.
|
||||
/// Constants for the [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are prepared in that step too.
|
||||
@ -101,17 +113,6 @@ impl Bdd {
|
||||
RefCell::new(HashMap::new())
|
||||
}
|
||||
|
||||
/// Construct [Bdd] from a list of nodes by adding one after the other
|
||||
pub fn from_nodes(nodes: Vec<BddNode>) -> Self {
|
||||
let mut bdd = Self::new();
|
||||
|
||||
for node in nodes {
|
||||
bdd.node(node.var(), node.lo(), node.hi());
|
||||
}
|
||||
|
||||
bdd
|
||||
}
|
||||
|
||||
/// Instantiates a [variable][crate::datatypes::Var] and returns the representing roBDD as a [`Term`][crate::datatypes::Term].
|
||||
pub fn variable(&mut self, var: Var) -> Term {
|
||||
self.node(var, Term::BOT, Term::TOP)
|
||||
|
||||
@ -20,6 +20,7 @@ use serde::{Deserialize, Serialize};
|
||||
|
||||
use adf_bdd::adf::Adf;
|
||||
use adf_bdd::adfbiodivine::Adf as BdAdf;
|
||||
use adf_bdd::obdd::Bdd;
|
||||
use adf_bdd::parser::AdfParser;
|
||||
|
||||
use crate::config::{AppState, RunningInfo, Task, ADF_COLL, COMPUTE_TIME, DB_NAME, USER_COLL};
|
||||
@ -164,16 +165,38 @@ pub(crate) struct SimplifiedAdf {
|
||||
pub(crate) ac: AcDb,
|
||||
}
|
||||
|
||||
impl SimplifiedAdf {
|
||||
fn from_lib_adf(adf: Adf) -> Self {
|
||||
SimplifiedAdf {
|
||||
ordering: adf.ordering.into(),
|
||||
bdd: adf.bdd.nodes.into_iter().map(Into::into).collect(),
|
||||
ac: adf.ac.into_iter().map(|t| t.0.to_string()).collect(),
|
||||
impl From<Adf> for SimplifiedAdf {
|
||||
fn from(source: Adf) -> Self {
|
||||
Self {
|
||||
ordering: source.ordering.into(),
|
||||
bdd: source.bdd.nodes.into_iter().map(Into::into).collect(),
|
||||
ac: source.ac.into_iter().map(|t| t.0.to_string()).collect(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl From<SimplifiedAdf> for Adf {
|
||||
fn from(source: SimplifiedAdf) -> Self {
|
||||
let bdd = Bdd::from(
|
||||
source
|
||||
.bdd
|
||||
.into_iter()
|
||||
.map(Into::into)
|
||||
.collect::<Vec<BddNode>>(),
|
||||
);
|
||||
|
||||
Adf::from((
|
||||
source.ordering.into(),
|
||||
bdd,
|
||||
source
|
||||
.ac
|
||||
.into_iter()
|
||||
.map(|t| Term(t.parse().unwrap()))
|
||||
.collect(),
|
||||
))
|
||||
}
|
||||
}
|
||||
|
||||
type SimplifiedAdfOpt = OptionWithError<SimplifiedAdf>;
|
||||
|
||||
#[derive(Deserialize, Serialize)]
|
||||
@ -408,7 +431,7 @@ async fn add_adf_problem(
|
||||
graph: DoubleLabeledGraph::from_adf_and_ac(&lib_adf, None),
|
||||
};
|
||||
|
||||
(SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph)
|
||||
(SimplifiedAdf::from(lib_adf), ac_and_graph)
|
||||
});
|
||||
|
||||
app_state
|
||||
@ -550,15 +573,7 @@ async fn solve_adf_problem(
|
||||
#[cfg(feature = "mock_long_computations")]
|
||||
std::thread::sleep(Duration::from_secs(20));
|
||||
|
||||
let mut adf: Adf = Adf::from_ord_nodes_and_ac(
|
||||
simp_adf.ordering.into(),
|
||||
simp_adf.bdd.into_iter().map(Into::into).collect(),
|
||||
simp_adf
|
||||
.ac
|
||||
.into_iter()
|
||||
.map(|t| Term(t.parse().unwrap()))
|
||||
.collect(),
|
||||
);
|
||||
let mut adf: Adf = simp_adf.into();
|
||||
|
||||
let acs: Vec<Ac> = match adf_problem_input.strategy {
|
||||
Strategy::Complete => adf.complete().collect(),
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user