diff --git a/lib/src/adf.rs b/lib/src/adf.rs index 4d812a4..6063bac 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -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)]); } diff --git a/lib/src/adfbiodivine.rs b/lib/src/adfbiodivine.rs index c5d94d1..c5d76df 100644 --- a/lib/src/adfbiodivine.rs +++ b/lib/src/adfbiodivine.rs @@ -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, diff --git a/lib/src/datatypes/adf.rs b/lib/src/datatypes/adf.rs index 2716d4f..c4db79d 100644 --- a/lib/src/datatypes/adf.rs +++ b/lib/src/datatypes/adf.rs @@ -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>>, - mapping: Rc>>, +/// 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>>, + mapping: Arc>>, } 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>>, - mapping: Rc>>, + pub(crate) fn from_parser( + names: Arc>>, + mapping: Arc>>, ) -> 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 { - 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 { - 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>> { - Rc::clone(&self.names) + pub(crate) fn names(&self) -> Arc>> { + Arc::clone(&self.names) + } + + pub(crate) fn mappings(&self) -> Arc>> { + 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 diff --git a/lib/src/lib.rs b/lib/src/lib.rs index f15c7eb..3709699 100644 --- a/lib/src/lib.rs +++ b/lib/src/lib.rs @@ -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 diff --git a/lib/src/parser.rs b/lib/src/parser.rs index acac346..2603e5a 100644 --- a/lib/src/parser.rs +++ b/lib/src/parser.rs @@ -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>>, - dict: Rc>>, + namelist: Arc>>, + dict: Arc>>, formulae: RefCell>>, formulaname: RefCell>, } @@ -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 { - 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>> { - Rc::clone(&self.dict) + pub(crate) fn dict(&self) -> Arc>> { + Arc::clone(&self.dict) } - pub(crate) fn namelist_rc_refcell(&self) -> Rc>> { - Rc::clone(&self.namelist) + pub(crate) fn namelist(&self) -> Arc>> { + 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") })