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

Add multithread-safe functionality for the dictionary/ordering

Browse Source 
* Streamline a couple of API calls
* Expose more structs and methods to the public API
* Breaking some API (though nothing which is currently used in the binary)
This commit is contained in:
Stefan Ellmauthaler 2022-07-27 11:50:14 +02:00
parent 00674f7c5e
commit 84aa627159
Failed to extract signature
5 changed files with 134 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
lib/src/adf.rs
View File

@ -47,19 +47,14 @@ impl Adf {
pub fn from_parser(parser: &AdfParser) -> Self {
log::info!("[Start] instantiating BDD");
let mut result = Self {
ordering: VarContainer::from_parser(
parser.namelist_rc_refcell(),
parser.dict_rc_refcell(),
),
ordering: parser.var_container(),
bdd: Bdd::new(),
ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()],
ac: vec![Term(0); parser.dict_size()],
};
(0..parser.namelist_rc_refcell().borrow().len())
.into_iter()
.for_each(|value| {
log::trace!("adding variable {}", Var(value));
result.bdd.variable(Var(value));
});
(0..parser.dict_size()).into_iter().for_each(|value| {
log::trace!("adding variable {}", Var(value));
result.bdd.variable(Var(value));
});
log::debug!("[Start] adding acs");
parser
.formula_order()
@ -87,7 +82,7 @@ impl Adf {
bio_ac: &[biodivine_lib_bdd::Bdd],
) -> Self {
let mut result = Self {
ordering: VarContainer::copy(ordering),
ordering: ordering.clone(),
bdd: Bdd::new(),
ac: vec![Term(0); bio_ac.len()],
};
@ -900,11 +895,16 @@ mod test {
parser.parse()(input).unwrap();
let adf = Adf::from_parser(&parser);
assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a");
assert_eq!(adf.ordering.names().as_ref().borrow()[1], "c");
assert_eq!(adf.ordering.names().as_ref().borrow()[2], "b");
assert_eq!(adf.ordering.names().as_ref().borrow()[3], "e");
assert_eq!(adf.ordering.names().as_ref().borrow()[4], "d");
assert_eq!(adf.ordering.name(Var(0)), Some("a".to_string()));
assert_eq!(adf.ordering.names().read().unwrap()[0], "a");
assert_eq!(adf.ordering.name(Var(1)), Some("c".to_string()));
assert_eq!(adf.ordering.names().read().unwrap()[1], "c");
assert_eq!(adf.ordering.name(Var(2)), Some("b".to_string()));
assert_eq!(adf.ordering.names().read().unwrap()[2], "b");
assert_eq!(adf.ordering.name(Var(3)), Some("e".to_string()));
assert_eq!(adf.ordering.names().read().unwrap()[3], "e");
assert_eq!(adf.ordering.name(Var(4)), Some("d".to_string()));
assert_eq!(adf.ordering.names().read().unwrap()[4], "d");
assert_eq!(adf.ac, vec![Term(4), Term(2), Term(7), Term(15), Term(12)]);
@ -915,11 +915,11 @@ mod test {
parser.varsort_alphanum();
let adf = Adf::from_parser(&parser);
assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a");
assert_eq!(adf.ordering.names().as_ref().borrow()[1], "b");
assert_eq!(adf.ordering.names().as_ref().borrow()[2], "c");
assert_eq!(adf.ordering.names().as_ref().borrow()[3], "d");
assert_eq!(adf.ordering.names().as_ref().borrow()[4], "e");
assert_eq!(adf.ordering.names().read().unwrap()[0], "a");
assert_eq!(adf.ordering.names().read().unwrap()[1], "b");
assert_eq!(adf.ordering.names().read().unwrap()[2], "c");
assert_eq!(adf.ordering.names().read().unwrap()[3], "d");
assert_eq!(adf.ordering.names().read().unwrap()[4], "e");
assert_eq!(adf.ac, vec![Term(3), Term(7), Term(2), Term(11), Term(13)]);
}

16
lib/src/adfbiodivine.rs
View File

@ -40,19 +40,17 @@ impl Adf {
pub fn from_parser(parser: &AdfParser) -> Self {
log::info!("[Start] instantiating BDD");
let mut bdd_var_builder = biodivine_lib_bdd::BddVariableSetBuilder::new();
let namelist = parser.namelist_rc_refcell().as_ref().borrow().clone();
let namelist = parser
.namelist()
.read()
.expect("ReadLock on namelist failed")
.clone();
let slice_vec: Vec<&str> = namelist.iter().map(<_>::as_ref).collect();
bdd_var_builder.make_variables(&slice_vec);
let bdd_variables = bdd_var_builder.build();
let mut result = Self {
ordering: VarContainer::from_parser(
parser.namelist_rc_refcell(),
parser.dict_rc_refcell(),
),
ac: vec![
bdd_variables.mk_false();
parser.namelist_rc_refcell().as_ref().borrow().len()
],
ordering: parser.var_container(),
ac: vec![bdd_variables.mk_false(); parser.dict_size()],
vars: bdd_variables.variables(),
varset: bdd_variables,
rewrite: None,

60
lib/src/datatypes/adf.rs
View File

@ -2,49 +2,63 @@
use super::{Term, Var};
use serde::{Deserialize, Serialize};
use std::{cell::RefCell, collections::HashMap, fmt::Display, rc::Rc};
use std::{collections::HashMap, fmt::Display, sync::Arc, sync::RwLock};
#[derive(Serialize, Deserialize, Debug)]
pub(crate) struct VarContainer {
names: Rc<RefCell<Vec<String>>>,
mapping: Rc<RefCell<HashMap<String, usize>>>,
/// A container which acts as a dictionary as well as an ordering of variables.
/// *names* is a list of variable-names and the sequence of the values is inducing the order of variables.
/// *mapping* allows to search for a variable name and to receive the corresponding position in the variable list (`names`).
#[derive(Serialize, Deserialize, Debug, Clone)]
pub struct VarContainer {
names: Arc<RwLock<Vec<String>>>,
mapping: Arc<RwLock<HashMap<String, usize>>>,
}
impl Default for VarContainer {
fn default() -> Self {
VarContainer {
names: Rc::new(RefCell::new(Vec::new())),
mapping: Rc::new(RefCell::new(HashMap::new())),
names: Arc::new(RwLock::new(Vec::new())),
mapping: Arc::new(RwLock::new(HashMap::new())),
}
}
}
impl VarContainer {
pub fn from_parser(
names: Rc<RefCell<Vec<String>>>,
mapping: Rc<RefCell<HashMap<String, usize>>>,
pub(crate) fn from_parser(
names: Arc<RwLock<Vec<String>>>,
mapping: Arc<RwLock<HashMap<String, usize>>>,
) -> VarContainer {
VarContainer { names, mapping }
}
pub fn copy(from: &Self) -> Self {
VarContainer {
names: from.names.clone(),
mapping: from.mapping.clone(),
}
}
/// Get the [Var] used by the `Bdd` which corresponds to the given [&str].
/// Returns [None] if no matching value is found.
pub fn variable(&self, name: &str) -> Option<Var> {
self.mapping.borrow().get(name).map(|val| Var(*val))
self.mapping
.read()
.ok()
.and_then(|map| map.get(name).map(|val| Var(*val)))
}
/// Get the name which corresponds to the given [Var].
/// Returns [None] if no matching value is found.
pub fn name(&self, var: Var) -> Option<String> {
self.names.borrow().get(var.value()).cloned()
self.names
.read()
.ok()
.and_then(|name| name.get(var.value()).cloned())
}
#[allow(dead_code)]
pub fn names(&self) -> Rc<RefCell<Vec<String>>> {
Rc::clone(&self.names)
pub(crate) fn names(&self) -> Arc<RwLock<Vec<String>>> {
Arc::clone(&self.names)
}
pub(crate) fn mappings(&self) -> Arc<RwLock<HashMap<String, usize>>> {
Arc::clone(&self.mapping)
}
/// Creates a [PrintDictionary] for output purposes.
pub fn print_dictionary(&self) -> PrintDictionary {
PrintDictionary::new(self)
}
}
/// A struct which holds the dictionary to print interpretations and allows to instantiate printable interpretations.
@ -56,7 +70,7 @@ pub struct PrintDictionary {
impl PrintDictionary {
pub(crate) fn new(order: &VarContainer) -> Self {
Self {
ordering: VarContainer::copy(order),
ordering: order.clone(),
}
}
/// creates a [PrintableInterpretation] for output purposes

11
lib/src/lib.rs
View File

@ -169,14 +169,16 @@ The enum [`Heuristic`][crate::adf::heuristics::Heuristic] allows one to choose a
use adf_bdd::parser::AdfParser;
use adf_bdd::adf::Adf;
use adf_bdd::adf::heuristics::Heuristic;
use adf_bdd::datatypes::Term;
use adf_bdd::datatypes::{Term, adf::VarContainer};
// create a channel
let (s, r) = crossbeam_channel::unbounded();
let variables = VarContainer::default();
let variables_worker = variables.clone();
// spawn a solver thread
let solving = std::thread::spawn(move || {
// 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();
let parser = AdfParser::with_var_container(variables_worker);
parser.parse()(&input).expect("parsing worked well");
// use hybrid approach
let mut adf = adf_bdd::adfbiodivine::Adf::from_parser(&parser).hybrid_step();
@ -184,9 +186,12 @@ let solving = std::thread::spawn(move || {
adf.stable_nogood_channel(Heuristic::Simple, s);
});
let printer = variables.print_dictionary();
// print results as they are computed
while let Ok(result) = r.recv() {
println!("stable model: {:?}", result);
print!("stable model: {:?} \n", result);
// use dictionary
print!("stable model with variable names: {}", printer.print_interpretation(&result));
# assert_eq!(result, vec![Term(1),Term(1),Term(0),Term(0)]);
}
// waiting for the other thread to close

81
lib/src/parser.rs
View File

@ -10,7 +10,13 @@ use nom::{
sequence::{delimited, preceded, separated_pair, terminated},
IResult,
};
use std::{cell::RefCell, collections::HashMap, rc::Rc};
use std::collections::HashMap;
use std::{
cell::RefCell,
sync::{Arc, RwLock},
};
use crate::datatypes::adf::VarContainer;
/// A representation of a formula, still using the strings from the input.
#[derive(Clone, PartialEq, Eq)]
@ -127,8 +133,8 @@ impl std::fmt::Debug for Formula<'_> {
/// Note that the parser can be utilised by an [ADF][`crate::adf::Adf`] to initialise it with minimal overhead.
#[derive(Debug)]
pub struct AdfParser<'a> {
namelist: Rc<RefCell<Vec<String>>>,
dict: Rc<RefCell<HashMap<String, usize>>>,
namelist: Arc<RwLock<Vec<String>>>,
dict: Arc<RwLock<HashMap<String, usize>>>,
formulae: RefCell<Vec<Formula<'a>>>,
formulaname: RefCell<Vec<String>>,
}
@ -136,8 +142,8 @@ pub struct AdfParser<'a> {
impl Default for AdfParser<'_> {
fn default() -> Self {
AdfParser {
namelist: Rc::new(RefCell::new(Vec::new())),
dict: Rc::new(RefCell::new(HashMap::new())),
namelist: Arc::new(RwLock::new(Vec::new())),
dict: Arc::new(RwLock::new(HashMap::new())),
formulae: RefCell::new(Vec::new()),
formulaname: RefCell::new(Vec::new()),
}
@ -176,8 +182,14 @@ where
fn parse_statement(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|input| {
let mut dict = self.dict.borrow_mut();
let mut namelist = self.namelist.borrow_mut();
let mut dict = self
.dict
.write()
.expect("RwLock of dict could not get write access");
let mut namelist = self
.namelist
.write()
.expect("RwLock of namelist could not get write access");
let (remain, statement) =
terminated(AdfParser::statement, terminated(tag("."), multispace0))(input)?;
if !dict.contains_key(statement) {
@ -200,16 +212,31 @@ where
}
}
impl<'a> AdfParser<'a> {
/// Creates a new parser, utilising the already existing [VarContainer]
pub fn with_var_container(var_container: VarContainer) -> AdfParser<'a> {
AdfParser {
namelist: var_container.names(),
dict: var_container.mappings(),
formulae: RefCell::new(Vec::new()),
formulaname: RefCell::new(Vec::new()),
}
}
}
impl AdfParser<'_> {
/// after an update to the namelist, all indizes are updated
fn regenerate_indizes(&self) {
self.namelist
.as_ref()
.borrow()
.read()
.expect("ReadLock on namelist failed")
.iter()
.enumerate()
.for_each(|(i, elem)| {
self.dict.as_ref().borrow_mut().insert(elem.clone(), i);
self.dict
.write()
.expect("WriteLock on dict failed")
.insert(elem.clone(), i);
});
}
@ -217,7 +244,10 @@ impl AdfParser<'_> {
/// Results, which got used before might become corrupted.
/// Ensure that all used data is physically copied.
pub fn varsort_lexi(&self) -> &Self {
self.namelist.as_ref().borrow_mut().sort_unstable();
self.namelist
.write()
.expect("WriteLock on namelist failed")
.sort_unstable();
self.regenerate_indizes();
self
}
@ -227,8 +257,8 @@ impl AdfParser<'_> {
/// Ensure that all used data is physically copied.
pub fn varsort_alphanum(&self) -> &Self {
self.namelist
.as_ref()
.borrow_mut()
.write()
.expect("WriteLock on namelist failed")
.string_sort_unstable(natural_lexical_cmp);
self.regenerate_indizes();
self
@ -343,14 +373,18 @@ impl AdfParser<'_> {
/// Allows insight of the number of parsed statements.
pub fn dict_size(&self) -> usize {
//self.dict.borrow().len()
self.dict.as_ref().borrow().len()
self.dict.read().expect("ReadLock on dict failed").len()
}
/// Returns the number-representation and position of a given statement in string-representation.
///
/// Will return [None] if the string does no occur in the dictionary.
pub fn dict_value(&self, value: &str) -> Option<usize> {
self.dict.as_ref().borrow().get(value).copied()
self.dict
.read()
.expect("ReadLock on dict failed")
.get(value)
.copied()
}
/// Returns the acceptance condition of a statement at the given position.
@ -360,12 +394,17 @@ impl AdfParser<'_> {
self.formulae.borrow().get(idx).cloned()
}
pub(crate) fn dict_rc_refcell(&self) -> Rc<RefCell<HashMap<String, usize>>> {
Rc::clone(&self.dict)
pub(crate) fn dict(&self) -> Arc<RwLock<HashMap<String, usize>>> {
Arc::clone(&self.dict)
}
pub(crate) fn namelist_rc_refcell(&self) -> Rc<RefCell<Vec<String>>> {
Rc::clone(&self.namelist)
pub(crate) fn namelist(&self) -> Arc<RwLock<Vec<String>>> {
Arc::clone(&self.namelist)
}
/// Returns a [`VarContainer`][crate::datatypes::adf::VarContainer] which allows to access the variable information gathered by the parser
pub fn var_container(&self) -> VarContainer {
VarContainer::from_parser(self.namelist(), self.dict())
}
pub(crate) fn formula_count(&self) -> usize {
@ -379,8 +418,8 @@ impl AdfParser<'_> {
.map(|name| {
*self
.dict
.as_ref()
.borrow()
.read()
.expect("ReadLock on dict failed")
.get(name)
.expect("Dictionary should contain all the used formulanames")
})