diff --git a/Cargo.toml b/Cargo.toml index 8a57c9e..f5a41d5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,7 +10,7 @@ name = "biodivine_lib_logical_models" path = "src/lib.rs" [dependencies] -biodivine-lib-bdd = "0.5.3" +biodivine-lib-bdd = "0.5.7" debug-ignore = "1.0.5" dyn-clonable = "0.9.0" rayon = "1.8.0" @@ -18,4 +18,4 @@ serde = { version = "1.0", features = ["derive"] } serde-xml-rs = "0.6.0" thiserror = "1.0.40" xml-rs = "0.8.14" -num-bigint = "0.4.4" \ No newline at end of file +num-bigint = "0.4.4" diff --git a/src/update/update_fn.rs b/src/update/update_fn.rs index 34c18c4..795563c 100644 --- a/src/update/update_fn.rs +++ b/src/update/update_fn.rs @@ -343,6 +343,8 @@ where D: SymbolicDomain, { /// ordered by variable name // todo add a method to get the update function by name (hash map or binary search) + /// maps variable name to its index in the `variables_transition_relation_and_domain` vector to allow for fast access while keeping the vector sorted + mapper: HashMap, pub variables_transition_relation_and_domain: Vec<(String, VarInfo)>, // todo do not keep pub; just here for benchmarking pub bdd_variable_set: BddVariableSet, // todo do not keep pub; just here for testing _marker: std::marker::PhantomData, @@ -371,7 +373,6 @@ where DO: SymbolicDomainOrd, { pub fn from_update_fns( - // todo do not forget to add default update functions for those variables that are not updated (in the loader from xml) vars_and_their_update_fns: HashMap>, ) -> Self { vars_and_their_update_fns.iter().for_each(|(name, _)| { @@ -433,15 +434,21 @@ where ) }); - let unit_set = named_symbolic_domains.iter().fold( - bdd_variable_set.mk_true(), - |acc, ((name, domain), _)| { - println!("anded domain name {}", name); + let unit_set = named_symbolic_domains + .iter() + .fold(bdd_variable_set.mk_true(), |acc, ((_name, domain), _)| { acc.and(&domain.unit_collection(&bdd_variable_set)) - // primed ones must not affect unit collection -> ignore - // .and(&primed_domain.unit_collection(&bdd_variable_set)) - }, - ); + }); + + let unprimed_var_names_and_their_primed_unit_collection = named_symbolic_domains + .iter() + .map(|((unprimed_var_name, _), (_, primed_domain))| { + ( + unprimed_var_name, + primed_domain.unit_collection(&bdd_variable_set), + ) + }) + .collect::>(); let relations = update_fns .into_iter() @@ -454,7 +461,8 @@ where .expect("domain always present"); let relation = update_fn.bit_answering_bdds.iter().fold( - bdd_variable_set.mk_true(), + // unit_set -> result of any `and` encodes only valid states + unit_set.clone(), |acc, (bdd_var, bit_answering_bdd)| { // todo this could be called once & zipped to the iterator to make blazingly fast let bdd_var_primed = find_bdd_variables_prime( @@ -463,17 +471,20 @@ where target_symbolic_domain_primed, ); - let bit_answering_bdd = bit_answering_bdd.and(&unit_set); - let primed_target_variable_bdd = bdd_variable_set.mk_var(bdd_var_primed); let primed_bound_to_udpate = - primed_target_variable_bdd.iff(&bit_answering_bdd); + primed_target_variable_bdd.iff(bit_answering_bdd); - acc.and(&primed_bound_to_udpate).and(&unit_set) // todo xd this cant be it + acc.and(&primed_bound_to_udpate) }, ); - relation.and(&unit_set) // todo is this needed? + let specific_primed_unit_set = unprimed_var_names_and_their_primed_unit_collection + .get(target_variable_name) + .expect("always present"); + + // ensure output only valid values + relation.and(specific_primed_unit_set) }) .collect::>(); @@ -494,9 +505,18 @@ where ) }, ) - .collect(); + .collect::>(); + + let mapper = variables_transition_relation_and_domain + .iter() + .enumerate() + .fold(HashMap::new(), |mut acc, (idx, (var_name, _))| { + acc.insert(var_name.to_owned(), idx); + acc + }); Self { + mapper, variables_transition_relation_and_domain, bdd_variable_set, _marker: std::marker::PhantomData, @@ -518,13 +538,6 @@ where let forgor_old_val = source_states_transition_relation.exists(target_domain.raw_bdd_variables().as_slice()); - let unit_set = self - .variables_transition_relation_and_domain - .iter() - .fold(self.bdd_variable_set.mk_true(), |acc, (_, var_info)| { - acc.and(&var_info.domain.unit_collection(&self.bdd_variable_set)) - }); - target_domain .raw_bdd_variables() .into_iter() @@ -533,7 +546,6 @@ where unsafe { acc.rename_variable(primed, unprimed) }; acc }) - .and(&unit_set) } /// Like `successors_async`, but a state that "transitions" to itself under @@ -570,13 +582,6 @@ where .get_transition_relation_and_domain(transition_variable_name) .expect("unknown variable"); - let unit_set = self - .variables_transition_relation_and_domain - .iter() - .fold(self.bdd_variable_set.mk_true(), |acc, (_, var_info)| { - acc.and(&var_info.domain.unit_collection(&self.bdd_variable_set)) - }); - let source_states_primed_set = target_domain .raw_bdd_variables() .into_iter() @@ -589,9 +594,7 @@ where let source_states_transition_relation = source_states_primed_set.and(transition_relation); - source_states_transition_relation - .exists(primed_domain.raw_bdd_variables().as_slice()) - .and(&unit_set) + source_states_transition_relation.exists(primed_domain.raw_bdd_variables().as_slice()) } /// Like `predecessors_async`, but a state that "transitions" to itself under @@ -617,6 +620,9 @@ where .iter() .find(|(maybe_variable_name, _)| maybe_variable_name == variable_name) .map(|(_, update_fn_and_domain)| update_fn_and_domain) + // self.mapper + // .get(variable_name) + // .map(|idx| &self.variables_transition_relation_and_domain[*idx].1) } fn those_states_capable_of_transitioning_under(&self, _variable_name: &str) -> Bdd { diff --git a/tests/some_test.rs b/tests/some_test.rs index 2231c03..05ca98c 100644 --- a/tests/some_test.rs +++ b/tests/some_test.rs @@ -116,7 +116,9 @@ impl TheFourImplsBdd { println!("smart_are_same output: {}", old_smart_dot == new_smart_dot); - old_smart_dot == new_smart_dot + //old_smart_dot == new_smart_dot + //self.old_smart_bdd.iff(&self.new_smart_bdd).is_true() + self.old_smart_bdd == self.new_smart_bdd } fn dumb_are_same(&self, context: &TheFourImpls) -> bool @@ -301,7 +303,7 @@ impl TheFourImpls { // this might be, because the handmade do not target cases where invalid states might come into play // ^ this can be seen by modifying the old impls - if pruning of invalid staes is removed in one of them, // the "basic" tests do not detect any difference, while the "large" tests do -// #[test] +#[test] fn consistency_check() { let mut i = 0usize; loop { @@ -649,7 +651,7 @@ fn check_specific() { } } -#[test] +// #[test] fn predecessors_consistency_check() { let mut i = 0usize; let mut whole_test_count = 0usize; @@ -735,7 +737,19 @@ fn predecessors_consistency_check() { let transitioned = the_four.predecessors_async(variable, initial_state); - assert!(transitioned.are_same(&the_four), "all are same"); + if !transitioned.smart_are_same(&the_four) { + let old_smart_dot = the_four + .old_smart + .bdd_to_dot_string(&transitioned.old_smart_bdd); + println!("old smart: {}", old_smart_dot); + + let new_smart_dot = the_four + .new_smart + .bdd_to_dot_string(&transitioned.new_smart_bdd); + println!("new smart: {}", new_smart_dot); + } + + assert!(transitioned.smart_are_same(&the_four), "all are same"); println!( "predecessors count = {} were the same; whole test {}",