diff --git a/src/_aeon_parser/_from_string_for_boolean_network.rs b/src/_aeon_parser/_from_string_for_boolean_network.rs index 7fccc3a..828bf32 100644 --- a/src/_aeon_parser/_from_string_for_boolean_network.rs +++ b/src/_aeon_parser/_from_string_for_boolean_network.rs @@ -44,6 +44,9 @@ impl TryFrom<&str> for BooleanNetwork { variable_names.insert(reg.regulator.clone()); variable_names.insert(reg.target.clone()); } + for (name, _) in &update_functions { + variable_names.insert(name.clone()); + } let mut variable_names: Vec = variable_names.into_iter().collect(); variable_names.sort(); @@ -113,7 +116,10 @@ mod tests { Box::new(FnUpdate::Var(VariableId(0))), Box::new(FnUpdate::Binary( Imp, - Box::new(FnUpdate::Param(ParameterId(1), vec![VariableId(2)])), + Box::new(FnUpdate::Param( + ParameterId(1), + vec![FnUpdate::Var(VariableId(2))], + )), Box::new(FnUpdate::Binary( Or, Box::new(FnUpdate::Var(VariableId(2))), @@ -124,10 +130,13 @@ mod tests { let f2 = FnUpdate::Binary( Iff, - Box::new(FnUpdate::Param(ParameterId(1), vec![VariableId(0)])), + Box::new(FnUpdate::Param( + ParameterId(1), + vec![FnUpdate::Var(VariableId(0))], + )), Box::new(FnUpdate::Param( ParameterId(2), - vec![VariableId(0), VariableId(0)], + vec![FnUpdate::Var(VariableId(0)), FnUpdate::Var(VariableId(0))], )), ); @@ -135,7 +144,7 @@ mod tests { Imp, Box::new(FnUpdate::Param( ParameterId(2), - vec![VariableId(1), VariableId(1)], + vec![FnUpdate::Var(VariableId(1)), FnUpdate::Var(VariableId(1))], )), Box::new(FnUpdate::Not(Box::new(FnUpdate::Binary( Xor, diff --git a/src/_aeon_parser/_from_string_for_fn_update_temp.rs b/src/_aeon_parser/_from_string_for_fn_update_temp.rs index 3ad1cf4..ca3b7ec 100644 --- a/src/_aeon_parser/_from_string_for_fn_update_temp.rs +++ b/src/_aeon_parser/_from_string_for_fn_update_temp.rs @@ -203,29 +203,24 @@ fn terminal(data: &[Token]) -> Result, String> { } } -/// **(internal)** Parse a list of function arguments. All arguments must be names separated +/// **(internal)** Parse a list of function arguments. All arguments must be expressions separated /// by commas. -fn read_args(data: &[Token]) -> Result, String> { +/// +/// Note that commas *have to* separate individual arguments, because any comma which is a part +/// of a "lower level" function call has to be enclosed in parentheses. +fn read_args(data: &[Token]) -> Result, String> { if data.is_empty() { return Ok(Vec::new()); } let mut result = Vec::new(); - let mut i = 0; - while let Token::Name(name) = &data[i] { - result.push(name.clone()); - i += 1; - if data.len() == i { - return Ok(result); - } - if data[i] != Token::Comma { - return Err(format!("Expected ',', found {:?}.", data[i])); - } - i += 1; - if data.len() == i { - return Err("Unexpected ',' at the end of an argument list.".to_string()); + for arg in data.split(|it| *it == Token::Comma) { + if arg.is_empty() { + return Err("Found empty function argument.".to_string()); } + let arg = parse_update_function(arg)?; + result.push(*arg); } - Err(format!("Unexpected token {:?} in argument list.", data[i])) + Ok(result) } #[cfg(test)] @@ -245,6 +240,8 @@ mod tests { "(a => b)", "(a <=> b)", "(a <=> !(f(a, b) => (c ^ d)))", + "f(a, f(b), c)", + "f((a & c))", ]; for str in inputs { assert_eq!(str, format!("{}", FnUpdateTemp::try_from(str).unwrap())) @@ -292,9 +289,7 @@ mod tests { fn test_malformed_args() { assert!(FnUpdateTemp::try_from("f(a b c)").is_err()); assert!(FnUpdateTemp::try_from("f(a, b, c,)").is_err()); - assert!(FnUpdateTemp::try_from("f(a & c)").is_err()); assert!(FnUpdateTemp::try_from("f(a, & c)").is_err()); - assert!(FnUpdateTemp::try_from("f(a, f(b), c)").is_err()); } #[test] diff --git a/src/_aeon_parser/_impl_fn_update_temp.rs b/src/_aeon_parser/_impl_fn_update_temp.rs index 061ee51..d83bc28 100644 --- a/src/_aeon_parser/_impl_fn_update_temp.rs +++ b/src/_aeon_parser/_impl_fn_update_temp.rs @@ -16,7 +16,14 @@ impl FnUpdateTemp { r.unknown_variables_to_parameters(rg), ), Not(inner) => Not(inner.unknown_variables_to_parameters(rg)), - Param(name, args) => Param(name, args), + Param(name, args) => { + let args: Vec = args + .into_iter() + .map(|it| *it.unknown_variables_to_parameters(rg)) + .collect(); + + Param(name, args) + } Var(name) => { if rg.find_variable(&name).is_some() { Var(name) @@ -43,6 +50,10 @@ impl FnUpdateTemp { Param(name, args) => { let arity = u32::try_from(args.len()).unwrap(); result.insert(Parameter::new(name, arity)); + + for arg in args { + arg.dump_parameters(result); + } } } } @@ -61,7 +72,7 @@ impl FnUpdateTemp { Const(_) => {} Param(_, args) => { for arg in args { - result.insert(arg.clone()); + arg.dump_variables(result); } } } @@ -82,7 +93,7 @@ impl FnUpdateTemp { Self::check_parameter_arity(&bn[parameter_id], &args)?; let mut arguments = Vec::with_capacity(args.len()); for arg in args { - arguments.push(Self::get_variable(bn, &arg)?); + arguments.push(*arg.into_fn_update(bn)?); } FnUpdate::Param(parameter_id, arguments) } @@ -106,7 +117,7 @@ impl FnUpdateTemp { /// **(internal)** Generate an error message if the given `parameter` does not have /// arity matching the given `args` list. - fn check_parameter_arity(parameter: &Parameter, args: &[String]) -> Result<(), String> { + fn check_parameter_arity(parameter: &Parameter, args: &[FnUpdateTemp]) -> Result<(), String> { if parameter.get_arity() != u32::try_from(args.len()).unwrap() { Err(format!( "`{}` has arity {}, but is used with {} arguments.", diff --git a/src/_aeon_parser/mod.rs b/src/_aeon_parser/mod.rs index 1c35229..aee7c45 100644 --- a/src/_aeon_parser/mod.rs +++ b/src/_aeon_parser/mod.rs @@ -31,7 +31,7 @@ pub(crate) struct RegulationTemp { pub(crate) enum FnUpdateTemp { Const(bool), Var(String), - Param(String, Vec), + Param(String, Vec), Not(Box), Binary(BinaryOp, Box, Box), } diff --git a/src/_impl_boolean_network.rs b/src/_impl_boolean_network.rs index a2f6846..6679713 100644 --- a/src/_impl_boolean_network.rs +++ b/src/_impl_boolean_network.rs @@ -2,7 +2,7 @@ use crate::symbolic_async_graph::{RegulationConstraint, SymbolicContext}; use crate::Monotonicity::Inhibition; use crate::{ BooleanNetwork, FnUpdate, Monotonicity, Parameter, ParameterId, ParameterIdIterator, - Regulation, RegulatoryGraph, Variable, VariableId, VariableIdIterator, ID_REGEX, + RegulatoryGraph, Variable, VariableId, VariableIdIterator, ID_REGEX, }; use std::collections::{HashMap, HashSet}; use std::ops::Index; @@ -58,6 +58,14 @@ impl BooleanNetwork { Ok(id) } + /// Set parameter name. This should be relatively safe since we use IDs everythere. + fn rename_parameter(&mut self, parameter: ParameterId, new_name: &str) -> Result<(), String> { + self.assert_no_such_parameter(new_name)?; + let param = self.parameters.get_mut(parameter.to_index()).unwrap(); + param.name = new_name.to_string(); + Ok(()) + } + /// Add a new `UpdateFunction` to the `BooleanNetwork`. /// /// The variable must not already have an update function. We assume all the variables @@ -267,257 +275,403 @@ impl BooleanNetwork { }) .collect() } + + /// Return a copy of this network where all unused parameters (uninterpreted functions) + /// are removed. + /// + /// Note that `VariableId` objects are still valid for the result network, but `ParameterId` + /// objects can now refer to different parameters. + pub fn prune_unused_parameters(&self) -> BooleanNetwork { + let mut used = HashSet::new(); + for var in self.variables() { + if let Some(update) = self.get_update_function(var) { + used.extend(update.collect_parameters().into_iter()); + } + } + + if used.len() == self.num_parameters() { + // Skip analysis if all parameters are used. + return self.clone(); + } + + // Ensure the parameter ordering is as similar as possible. + let mut used = Vec::from_iter(used); + used.sort(); + + let mut new_bn = BooleanNetwork::new(self.graph.clone()); + let mut old_to_new_map = HashMap::new(); + for old_id in used { + let old_param = &self[old_id]; + let new_id = new_bn + .add_parameter(old_param.name.as_str(), old_param.arity) + .unwrap_or_else(|_| { + unreachable!("Parameter was valid in the old BN."); + }); + old_to_new_map.insert(old_id, new_id); + } + + let empty = HashMap::new(); + for var in self.variables() { + if let Some(update) = self.get_update_function(var) { + let update = update.rename_all(&empty, &old_to_new_map); + new_bn + .set_update_function(var, Some(update)) + .unwrap_or_else(|_| unreachable!("Function was valid in the old BN.")); + } + } + + new_bn + } } impl BooleanNetwork { - /// Infer a *sufficient* regulatory graph based on the update functions of + /// Infer a *sufficient local regulatory graph* based on the update functions of /// this `BooleanNetwork`. /// - /// The resulting graph is solely based on the information that can be inferred from the - /// update functions. In particular, if the BN contains uninterpreted functions, - /// the monotonicity of variables appearing within these functions is unknown. Overall, - /// the method is typically only useful for fully specified networks with minor errors - /// in the regulatory graph. + /// ## Notes /// - /// The BN still has to satisfy basic integrity constraints. In particular, every uninterpreted - /// function must be used, and must be used consistently (i.e. correct arity). Also, every - /// update function may only use variables declared as regulators. Otherwise, an error - /// is returned. + /// - The method will simplify the update functions when it detects that a variable + /// is not an essential input of the update function (for any instantiation). + /// - This also removes any unused parameters (uninterpreted functions), or parameters that + /// become unused due to the transformation. + /// - For fully specified update functions, the method simply updates the regulations to + /// match the actual behaviour of the function (i.e. any non-essential regulations are + /// removed, monotonicity is always specified unless the input is truly non-monotonic). + /// - For regulations that interact with uninterpreted functions: + /// - Observability: If there are no instantiations where the regulation is essential, + /// we remove the regulation completely. Otherwise, we preserve the original + /// observability constraint. + /// - Monotonicity: Similarly, if every instantiation of the function has a known + /// monotonicity, then we use this monotonicity. Otherwise, if the original constraint + /// is still satisfied for a subset of all instantiations, we use the original one. + /// + /// ## Limitations + /// + /// The result only guarantees that the constraints are *locally consistent**, meaning they + /// are valid when applied to the singular update function, not necessarily the whole model. + /// In other words, uninterpreted functions that are used by multiple variables can still cause + /// the model to be invalid if they use contradictory constraints, but this usually cannot be + /// resolved deterministically. + /// + /// ## Output + /// + /// The function can fail we, for whatever reason, cannot create [SymbolicContext] for + /// the old network. /// - /// The method can also fail if a non-observable regulator is removed from a partially - /// specified function, because in such case we cannot always transform the function - /// in a way that is valid. pub fn infer_valid_graph(&self) -> Result { - let ctx = SymbolicContext::new(self)?; + let mut old_bn = self.prune_unused_parameters(); + let ctx = SymbolicContext::new(&old_bn)?; - // This should ensure the variable IDs in the old and the new network are compatible, - // so that we can reuse Regulation and FnUpdate objects. - let var_names = self - .variables() - .map(|id| self.get_variable_name(id)) - .cloned() - .collect::>(); + // Copying the old variable names means VariableId objects should be still valid. + let var_names = old_bn.as_graph().variable_names(); + // Now we can recreate the regulatory graph from scratch: let mut new_rg = RegulatoryGraph::new(var_names); - for target_var in self.variables() { - if let Some(function) = self.get_update_function(target_var) { + for target_var in old_bn.variables() { + if let Some(function) = old_bn.get_update_function(target_var) { let fn_is_true = ctx.mk_fn_update_true(function); - for regulator_var in self.as_graph().regulators(target_var) { - let Some(regulation) = RegulationConstraint::infer_sufficient_regulation( - &ctx, - regulator_var, - target_var, - &fn_is_true, - ) else { + + for regulator_var in old_bn.regulators(target_var) { + let old_regulation = old_bn + .as_graph() + .find_regulation(regulator_var, target_var) + .unwrap_or_else(|| { + unreachable!("Regulation must exist."); + }); + + let Some(regulation) = + RegulationConstraint::fix_regulation(&ctx, old_regulation, &fn_is_true) + else { + // The regulator is completely unused. We can replace it with a constant + // and simplify the function. + let function = old_bn + .get_update_function(target_var) + .as_ref() + .unwrap_or_else(|| { + unreachable!("We already know `target_var` has a function."); + }); + let function = function + .substitute_variable(regulator_var, &FnUpdate::Const(false)) + .simplify_constants(); + old_bn + .set_update_function(target_var, Some(function)) + .unwrap_or_else(|_| { + unreachable!("Transformed function should be also valid."); + }); continue; }; - new_rg.add_raw_regulation(regulation).unwrap(); + new_rg.add_raw_regulation(regulation).unwrap_or_else(|_| { + unreachable!("The regulation must be valid."); + }) } } else { - // If the update function is missing, just copy the existing regulators, but - // remove any monotonicity/observability. - for regulator_var in self.as_graph().regulators(target_var) { + // If the update function is missing, just copy the existing regulators. + // Any constraint is satisfiable with an unknown function. + for regulator_var in old_bn.regulators(target_var) { + let old_regulation = old_bn + .as_graph() + .find_regulation(regulator_var, target_var) + .unwrap_or_else(|| { + unreachable!("Regulation must exist."); + }); new_rg - .add_raw_regulation(Regulation { - regulator: regulator_var, - target: target_var, - observable: false, - monotonicity: None, - }) - .unwrap(); + .add_raw_regulation(old_regulation.clone()) + .unwrap_or_else(|_| { + unreachable!("The regulation must be valid."); + }); } } } + // Next, we create a new BN and copy over the (potentially simplified) functions. let mut new_bn = BooleanNetwork::new(new_rg); // Copy over existing parameters - for parameter_id in self.parameters() { - let parameter = &self[parameter_id]; + for parameter_id in old_bn.parameters() { + let parameter = &old_bn[parameter_id]; new_bn .add_parameter(¶meter.name, parameter.arity) - .unwrap(); + .unwrap_or_else(|_| { + unreachable!("Parameter was valid in the old network."); + }); } - for var in self.variables() { - let name = self.get_variable_name(var); - if let Some(update) = self.get_update_function(var) { - // At the moment, there is no way to "fix" the function in a way that - // works with logical parameters if one of the arguments is non-observable. - // As such, we first try to copy the function with no change. then we try to - // run it through a string translation, but this only works on functions without - // parameters. If this fails, the conversion fails. - let Err(_) = new_bn.set_update_function(var, Some(update.clone())) else { - continue; - }; - let fn_bdd = ctx.mk_fn_update_true(update); - let fn_string = fn_bdd - .to_boolean_expression(ctx.bdd_variable_set()) - .to_string(); - let Err(_) = new_bn.add_string_update_function(name, &fn_string) else { - continue; - }; - return Err(format!( - "Cannot translate function for variable {} due to elimianted arguments.", - name - )); + for var in old_bn.variables() { + if let Some(update) = old_bn.get_update_function(var) { + // At this point, all non-essential variables are already removed from the + // function and we can thus safely copy it into the new network. + new_bn + .set_update_function(var, Some(update.clone())) + .unwrap_or_else(|_| { + unreachable!("The transformed function must be valid."); + }); } } - Ok(new_bn) + // In the end, we still have to prune the network in case we just made some uninterpreted + // function irrelevant by eliminating unused inputs. + Ok(new_bn.prune_unused_parameters()) } - /// Try to inline the input nodes (variables) of the network as logical parameters - /// (uninterpreted functions of arity 0). + /// Similar to [BooleanNetwork::inline_inputs], but inlines constant values (i.e. `x=true` or + /// `x=false`). /// - /// The operation also removes all observability requirements, as the transformation between - /// variable and parameter can cause them to be unsatisfiable (in particular, some - /// regulations can become observable only for certain parameter valuations). - /// - /// This often reduces the overall symbolic complexity of working with the network, as - /// fewer symbolic variables are necessary. However, note that at the moment, not all input - /// nodes can be correctly inlined. In particular, in order for a node to be inlined, - /// the following must hold: - /// - /// - Either it has no regulators and its update function is unknown, or it has exactly one - /// regulator and its update function is the identity function (update(x) = x). That is, - /// constant source nodes are not inlined. - /// - Every variable that depends on it has an explicit update function, the source node - /// does appear in this function (syntactically; we do not check for observability), and - /// it does not appear as an argument to any of the nested uninterpreted functions. - /// - /// The second requirement is necessary to ensure that the newly created parameter will still - /// appear in the network, and that we are not losing any information about its effect in the - /// downstream functions. However, note that we are still technically losing the - /// monotonicity/observability requirements. You should thus always check the integrity of - /// both the original and transformed network. - pub fn inline_inputs(&self) -> BooleanNetwork { - let inputs: HashSet = self - .variables() - .filter(|it| { - // Check if the variable is an input. - let has_no_regulators = self.as_graph().regulators(*it).is_empty(); - let has_update_function = self.get_update_function(*it).is_some(); - let is_free_input = has_no_regulators && !has_update_function; - - let has_identity_update = - self.get_update_function(*it) == &Some(FnUpdate::Var(*it)); - let is_only_regulator = self.as_graph().regulators(*it) == vec![*it]; - let is_identity_input = has_identity_update && is_only_regulator; - is_free_input || is_identity_input - }) - .filter(|input| { - // Only retain inputs that are safe to remove. - let mut is_ok = true; - for target in self.targets(*input) { - if let Some(update) = self.get_update_function(target) { - // If the input does not appear in the function at all, we can't remove - // it, because we'd lose information about that input. - is_ok = is_ok && update.contains_variable(*input); - update.walk_postorder(&mut |it: &FnUpdate| { - if let FnUpdate::Param(_, args) = it { - // If the input appears as function argument, we can't remove - // it because we don't have a way of substituting the argument. - is_ok = is_ok && !args.contains(input) - } - }) - } else { - // The target variable does not have an update function - we'd lose - // one implicit argument if we just delete this input variable. - is_ok = false; + /// By default, the constant check is purely syntactic, but we do perform basic constant + /// propagation (e.g. `x | true = true`) in order to catch the most obvious non-trivial cases. + /// However, you can set `infer_constants` to `true`, in which case a symbolic method will + /// be used to check if the variable uses a constant function. Note that this can also + /// eliminate parameters in some cases (e.g. inlining `x=true` into `y=x | f(z)`). + /// + /// Furthermore, similar to [BooleanNetwork::inline_inputs], you can set `repair_graph` to + /// `true` in order to fix any inconsistent regulations that arise due to the inlining + /// (this is highly recommended if you are using `infer_constants`). + /// + /// The inlining is performed iteratively, meaning if the inlining produces a new constant, + /// it is eventually also inlined. + /// + /// ## Panics + /// + /// The method can fail if `infer_constants` or `repair_graph` is specified and the network + /// does not have a valid symbolic representation. + pub fn inline_constants(&self, infer_constants: bool, repair_graph: bool) -> BooleanNetwork { + let mut result = self.clone(); + 'inlining: loop { + // These are two very similar algorithms, but we don't want to create the context + // needlessly if we don't have to. + if infer_constants { + let ctx = SymbolicContext::new(&result).unwrap_or_else(|_| { + panic!("Cannot create symbolic context for a network."); + }); + for var in result.variables() { + if let Some(update) = result.get_update_function(var) { + // Even if the value is not constant, we want to do constant propagation, + // just in case it makes the problem simpler. + let update_simplified = update.simplify_constants(); + let is_constant = update_simplified.as_const(); + result + .set_update_function(var, Some(update_simplified)) + .unwrap_or_else(|_| { + unreachable!( + "A simplified function can always replace the original." + ) + }); + if is_constant.is_some() { + result = result.inline_variable_internal(var, repair_graph); + continue 'inlining; + } + + // If constant propagation failed, we can recompute the + // result symbolically. + let update = result + .get_update_function(var) + .as_ref() + .unwrap_or_else(|| unreachable!("The function is known (see above).")); + let fn_is_true = ctx.mk_fn_update_true(update); + let constant = if fn_is_true.is_true() { + Some(true) + } else if fn_is_true.is_false() { + Some(false) + } else { + None + }; + if let Some(value) = constant { + // "Clean up" the function before inlining it. + result + .set_update_function(var, Some(FnUpdate::Const(value))) + .unwrap_or_else(|_| { + unreachable!("Constant function should be always allowed."); + }); + result = result.inline_variable_internal(var, repair_graph); + // The network has changed, so we need to recreate the symbolic context. + continue 'inlining; + } + } + } + } else { + for var in result.variables() { + if let Some(update) = result.get_update_function(var) { + // This is necessary to enable propagation beyond the first iteration, + // because we need to be able to detect things like `x | true` as `true`. + let update_simplified = update.simplify_constants(); + let is_constant = update_simplified.as_const(); + result + .set_update_function(var, Some(update_simplified)) + .unwrap_or_else(|_| { + unreachable!( + "A simplified function can always repalce the original." + ) + }); + if is_constant.is_some() { + result = result.inline_variable_internal(var, repair_graph); + continue 'inlining; + } } } - is_ok - }) - .collect(); - - let variables: HashSet = - self.variables().filter(|it| !inputs.contains(it)).collect(); - let mut variable_names: Vec = variables - .iter() - .map(|it| self.get_variable_name(*it)) - .cloned() - .collect(); - - variable_names.sort(); - - let mut new_rg = RegulatoryGraph::new(variable_names); - for reg in self.as_graph().regulations() { - if variables.contains(®.get_regulator()) { - let source_name = self.get_variable_name(reg.get_regulator()); - let target_name = self.get_variable_name(reg.get_target()); - new_rg - .add_regulation( - source_name.as_str(), - target_name.as_str(), - false, // necessary for this to work... - reg.get_monotonicity(), - ) - .unwrap(); } + // If nothing was inlined, we can stop. + break; } + result + } - let mut new_bn = BooleanNetwork::new(new_rg); - - // Copy old parameters. - for param in self.parameters() { - let param = self.get_parameter(param); - new_bn - .add_parameter(param.get_name().as_str(), param.get_arity()) - .unwrap(); - } - - // Add new inlined parameters. - // Note that integrity of the original BN ensures that there is no parameter - // with the same name already. - for var in &inputs { - let name = self.get_variable_name(*var); - new_bn.add_parameter(name.as_str(), 0).unwrap(); - } + /// Try to inline the input nodes (variables) of the network as logical parameters + /// (uninterpreted functions of arity 0). + /// + /// Here, an "input" is a variable `x` such that: + /// - `x` has no incoming regulations and a missing update function. + /// - `x` has an identity update function. This is either checked syntactically (default), + /// or semantically using BDDs (if `infer_inputs` is set to `true`). + /// + /// Note that this does not include constant nodes (e.g. `x=true`). These are handled + /// separately by [BooleanNetwork::inline_constants]. Also note that input variables that + /// do not influence any other variable are removed. + /// + /// Variables with update functions `x=f(true, false)` or `x=a` (where `a` is a zero-arity + /// parameter) are currently not considered to be inputs, although their role is conceptually + /// similar. + /// + /// This method is equivalent to calling [BooleanNetwork::inline_variable] on each input, + /// but the current implementation of [BooleanNetwork::inline_variable] does not permit + /// inlining of self-regulating variables, hence we have a special method for inputs only. + /// + /// Finally, just as [BooleanNetwork::inline_variable], the method can generate an + /// inconsistent regulatory graph. If `repair_graph` is set to true, the static properties + /// of relevant regulations are inferred using BDDs. + /// + pub fn inline_inputs(&self, infer_inputs: bool, repair_graph: bool) -> BooleanNetwork { + let inputs: Vec = { + if infer_inputs { + let ctx = SymbolicContext::new(self).unwrap_or_else(|_| { + panic!("Cannot create symbolic context for a network."); + }); + self.variables() + .filter(|it| { + // Check if the variable is an input. + let has_no_regulators = self.as_graph().regulators(*it).is_empty(); + let has_update_function = self.get_update_function(*it).is_some(); + let is_free_input = has_no_regulators && !has_update_function; + + let has_identity_update = + if let Some(update) = self.get_update_function(*it) { + let bdd_var = ctx.get_state_variable(*it); + let bdd_identity = ctx.bdd_variable_set().mk_var(bdd_var); + let bdd_fn = ctx.mk_fn_update_true(update); + + bdd_fn.iff(&bdd_identity).is_true() + } else { + false + }; + is_free_input || has_identity_update + }) + .collect() + } else { + self.variables() + .filter(|it| { + // Check if the variable is an input. + let has_no_regulators = self.as_graph().regulators(*it).is_empty(); + let has_update_function = self.get_update_function(*it).is_some(); + let is_free_input = has_no_regulators && !has_update_function; + + let has_identity_update = + self.get_update_function(*it) == &Some(FnUpdate::Var(*it)); + is_free_input || has_identity_update + }) + .collect() + } + }; - // Copy update functions. Technically, they should still be syntactically correct, so - // we just have to re-parse them in the new context. - for var in &variables { - let update = self.get_update_function(*var); - let name = self.get_variable_name(*var); - if let Some(update) = update { - new_bn - .add_string_update_function(name.as_str(), update.to_string(self).as_str()) - .unwrap(); + /* + This is not super efficient, because we make a new copy of the BN every time, + but we also want to avoid copying the inlining logic here, because it is already + sufficiently complex. + */ + + let mut result = self.clone(); + for input in inputs { + let name = self.get_variable_name(input); + let new_id = result.as_graph().find_variable(name).unwrap(); + // Simplify the function for the purposes of inlining. + if result.get_update_function(new_id).is_some() { + result + .set_update_function(new_id, Some(FnUpdate::Var(new_id))) + .unwrap_or_else(|_| { + println!("Identity update must be allowed for these variables."); + }); } + result = result.inline_variable_internal(new_id, repair_graph); } - new_bn + result } /// Produce a new [BooleanNetwork] where the given [VariableId] `var` has been eliminated /// by inlining its update function into all downstream variables. /// - /// The regulatory graph is updated to reflect this change. However, no further analysis - /// of logical consistency is performed. You can use [BooleanNetwork::infer_valid_graph] - /// to clean up the resulting graph if desired (for example, the method will remove any - /// unused regulations should these be introduced by the reduction process). + /// Note that the inlining operation is purely syntactic. This means that even if we create + /// new regulations when relevant, the resulting regulatory graph may be inconsistent with + /// the update functions. If you set `repair_graph` to `true`, the method will perform + /// semantic analysis on the new functions and repair regulatory graph where relevant. + /// If `repair_graph` is set to `false`, the operation does not perform any post-processing. /// /// > A simple example where "inconsistent" regulatory graph is produced is the inlining /// > of a constant input variable `f_a = true` into the update function `f_c = a | b`. /// > Here, we have regulations `a -> c` and `b -> c`. However, for the inlined function, - /// > we have `f_c = true | b = true`. As such, `b` is no longer observable in `f_c` and + /// > we have `f_c = (true | b) = true`. As such, `b` is no longer observable in `f_c` and /// > the resulting model is thus not "logically consistent". We need to either fix this /// > manually, or using [BooleanNetwork::infer_valid_graph]. /// /// ### Limitations /// - /// **At the moment, the reduced variable cannot have a self-regulation.** If such variable - /// is targeted with reduction, the result is `None`. Also, the variable cannot be inlined - /// into uninterpreted functions (see [FnUpdate::substitute_variable]), in which case we also - /// return `None`. We also cannot inline into *missing* update functions, but this is the - /// same as inlining into uninterpreted functions. + /// **At the moment, the reduced variable cannot have a self-regulation.** If such a variable + /// is targeted with reduction, the result is `None`. If a variable is inlined into a missing + /// function, the function is given a name as a new parameter, and the variable is inlined + /// into this new parameter function. /// /// Note that variables that don't regulate anything (outputs) are simply removed by this - /// reduction (although this is correct behaviour, just not super intuitive). + /// reduction. However, this is correct behaviour, just not super intuitive. /// - /// Finally, note that because the set of variables is different between this and the + /// Also note that because the set of variables is different between this and the /// resulting [BooleanNetwork], any [VariableId] that is valid in this network is not /// valid in the resulting network. /// @@ -532,54 +686,117 @@ impl BooleanNetwork { /// regulation `a -? c` (because `a -> b -> c` and `a -| c` in the original system). /// Then `f` can actually be `false`, `a`, or `!a`. /// - /// This does not mean you cannot use reduction on systems with uninterpreted functions at all, - /// but be careful about the new meaning of the static constraints on these functions. + /// This does not mean you cannot use reduction on systems with uninterpreted functions + /// at all, but be careful about the new meaning of the static constraints on these + /// functions. /// - pub fn inline_variable(&self, var: VariableId) -> Option { - let var_regulators = self.as_graph().regulators(var); - let var_targets = self.as_graph().targets(var); - if var_targets.contains(&var) { + pub fn inline_variable(&self, var: VariableId, repair_graph: bool) -> Option { + if self.as_graph().targets(var).contains(&var) { // Cannot inline variable if it is self-regulated. return None; } - let new_variables = self - .variables() + Some(self.inline_variable_internal(var, repair_graph)) + } + + /// An internal infallible version of [BooleanNetwork::inline_variable] which does not check + /// for self-regulations. The idea is that you can use this function if you are *sure* the + /// inlining is reasonable even if a self-regulation is present. + fn inline_variable_internal(&self, var: VariableId, repair_graph: bool) -> BooleanNetwork { + // TODO: Please break this up into smaller methods. I'm just not sure how... yet. + let mut old_bn = self.clone(); + let old_rg = self.as_graph(); + + // Remove `var` from regulators if it is there. + let var_regulators = old_rg + .regulators(var) + .into_iter() .filter(|it| *it != var) - .map(|it| self[it].name.clone()) .collect::>(); - let mut new_rg = RegulatoryGraph::new(new_variables); - - // First, copy every regulation that does not involve `var` or is not "feed forward". - for reg in self.as_graph().regulations() { - if reg.target == var || reg.regulator == var { - // Skip regulations where `var` is involved. - continue; - } - if var_regulators.contains(®.regulator) && var_targets.contains(®.target) { - // Skip regulations that directly circumvent `var`, because these will be - // recreated in the next step, possibly with different monotonicity/observability. - continue; + let var_targets = old_rg.targets(var); + + // If we have to create an explicit uninterpreted function for the inlined variable, + // we have to give it a unique name at first. But one the variable is inlined, we can + // use the old name. So here, we save whether a parameter needs to be removed, and if + // so, to what. + let mut rename_parameter: Option<(ParameterId, String)> = None; + + // 1. The very first step is to replace anonymous functions with explicit ones if they + // are somehow related to `var`. Hence in the next steps, we can assume the inlined + // function and the target functions are all explicit. + for check_var in var_targets.iter().chain(&[var]) { + let has_missing_function = old_bn.get_update_function(*check_var).is_none(); + let contains_self = old_bn + .get_update_function(*check_var) + .as_ref() + .map(|it| it.contains_variable(var)) + .unwrap_or(false); + let contains_self = *check_var == var && contains_self; + if has_missing_function || contains_self { + // Regulators, but without any self-regulation on the inlined variable. + // That self-regulation will be no longer there, hence we need to ignore it. + let regulators = old_rg + .regulators(*check_var) + .into_iter() + .filter(|it| !(*check_var == var && *it == var)) + .collect::>(); + let mut prefix = "fn".to_string(); // This is used to resolve name collisions. + let arity = u32::try_from(regulators.len()).unwrap(); + let p_id = loop { + let name = format!("{}_{}", prefix, old_bn.get_variable_name(*check_var)); + match old_bn.add_parameter(&name, arity) { + Ok(p_id) => break p_id, + Err(_) => { + // In case of collision, append a _ to prefix. + prefix = format!("{}_", prefix); + } + } + }; + if *check_var == var { + rename_parameter = Some((p_id, old_bn.get_variable_name(*check_var).clone())); + } + if has_missing_function { + // If we are creating the parameter due to a missing function, simply create + // a new update function and place it there. + let update = FnUpdate::mk_basic_param(p_id, ®ulators); + old_bn + .set_update_function(*check_var, Some(update)) + .unwrap(); + } else { + // Otherwise we are here due to `contains_self`, in which case we need to swap + // the variable for the fresh parameter. + let function = old_bn.get_update_function(*check_var).as_ref().unwrap(); + let function = + function.substitute_variable(*check_var, &FnUpdate::mk_param(p_id, &[])); + old_bn + .set_update_function(*check_var, Some(function)) + .unwrap(); + } } - new_rg - .add_regulation( - self.get_variable_name(reg.regulator), - self.get_variable_name(reg.target), - reg.observable, - reg.monotonicity, - ) - .unwrap(); } - // Now, add a new regulation for every combination of the old regulators and targets, - // but also incorporate the old "feed forward" regulations if present. + // 2. Compute variable list without the inlined variable. + let new_variables = { + let mut names = Vec::from_iter( + old_bn + .variables() + .map(|it| old_bn.get_variable_name(it).clone()), + ); + names.remove(var.to_index()); + names + }; + + // 3. Create an initial regulatory graph. We may try to further "fix" this graph later + // if `repair_graph` is set to true. But this should be enough for us to start inlining. + let mut new_rg = RegulatoryGraph::new(new_variables); + + // 3a. First, create new regulations related to regulators/targets of `var`. + // Specifically, add a new regulation for every combination of an + // old regulator and an old target, preserving the monotonicity/observability. for old_regulator in &var_regulators { for old_target in &var_targets { - let old_one = self - .as_graph() - .find_regulation(*old_regulator, var) - .unwrap(); - let old_two = self.as_graph().find_regulation(var, *old_target).unwrap(); - let old_feed_forward = self.as_graph().find_regulation(*old_regulator, *old_target); + let old_one = old_rg.find_regulation(*old_regulator, var).unwrap(); + let old_two = old_rg.find_regulation(var, *old_target).unwrap(); + let old_feed_forward = old_rg.find_regulation(*old_regulator, *old_target); // The new regulation is observable only if both partial regulations are // observable, or if the feed forward regulation exists and is observable. @@ -609,14 +826,14 @@ impl BooleanNetwork { None } } else { - // If there is no feed forward regulation, we juse use the new monotonicity. + // If there is no feed forward regulation, we just use the new monotonicity. combined_monotonicity }; new_rg .add_regulation( - self.get_variable_name(*old_regulator), - self.get_variable_name(*old_target), + old_bn.get_variable_name(*old_regulator), + old_bn.get_variable_name(*old_target), new_observable, new_monotonicity, ) @@ -624,76 +841,184 @@ impl BooleanNetwork { } } - // Finally, we can actually inline the update functions, but as always, this is a bit - // trickier than it sounds, because we have to translate [VariableId] and [ParameterId] - // between the old and the new model. + // 3b. Copy the remaining regulations into the new graph (i.e. those that do not + // involve `var` and are not "feed forward"). + for reg in old_rg.regulations() { + if reg.target == var || reg.regulator == var { + continue; + } + let name_regulator = self.get_variable_name(reg.regulator); + let name_target = self.get_variable_name(reg.target); + let new_regulator = new_rg.find_variable(name_regulator).unwrap(); + let new_target = new_rg.find_variable(name_target).unwrap(); + + if new_rg.find_regulation(new_regulator, new_target).is_some() { + // Skip if the regulation already exists. These are "feed forward" + // regulations that we already created. + continue; + } + + new_rg + .add_regulation( + name_regulator, + name_target, + reg.observable, + reg.monotonicity, + ) + .unwrap(); + } + + // 4. Now we can actually create a new network and all the relevant parameters. + // Here, we have to account for the fact that if a variable is unused and has an unknown + // function, we created an explicit parameter for it, which is now also unused. Such + // parameter should not be copied as it is redundant. let mut new_bn = BooleanNetwork::new(new_rg); + for id in old_bn.parameters() { + if rename_parameter.as_ref().map(|(a, _)| *a) == Some(id) { + // The rename_parameter is the one created *for* the inlined variable. We + // should check that the variable is actually used somewhere before copying it. + let mut is_used = false; + for target in &var_targets { + let update = old_bn.get_update_function(*target).as_ref().unwrap(); + if update.collect_arguments().contains(&var) { + is_used = true; + break; + } + } + if !is_used { + // No need to rename the parameter if it is skipped. + rename_parameter = None; + continue; + } + } + let parameter = old_bn.get_parameter(id); + new_bn + .add_parameter(¶meter.name, parameter.arity) + .unwrap(); + } + + // 5. Next, we build a map which assigns each old variable and parameter its new ID + // (except for `var`). + let new_var_id = old_bn + .variables() + .filter(|it| *it != var) + .map(|it| { + let name = old_bn.get_variable_name(it); + (it, new_bn.as_graph().find_variable(name).unwrap()) + }) + .collect::>(); + // This needs to be a filter-map, because we might have skipped the parameter of the + // inlined variable if it is never used. + let new_param_id = old_bn + .parameters() + .filter_map(|it| { + let name = &old_bn.get_parameter(it).name; + new_bn.find_parameter(name).map(|new_id| (it, new_id)) + }) + .collect::>(); - // First, build a map which assigns each "old" variable a "new" variable id. For the erased - // variable, we use an invalid value. - let mut old_to_new_var = Vec::with_capacity(self.num_vars()); - for v in self.variables() { - if v == var { - old_to_new_var.push(VariableId::from_index(usize::MAX)); + // 6. We can now move the update functions to the new network. If the function involves + // `var`, we substitute it. + let var_function = old_bn.get_update_function(var).clone().unwrap(); + for old_var in old_bn.variables() { + if old_var == var { + continue; + } + let new_id = new_var_id.get(&old_var).unwrap(); + if var_targets.contains(&old_var) { + // This variable is regulated by `var`. We need to inline `var_function`. + let update = old_bn.get_update_function(old_var).as_ref().unwrap(); + let inlined = update.substitute_variable(var, &var_function); + // Then we rename everything to new names... + let inlined = inlined.rename_all(&new_var_id, &new_param_id); + new_bn.set_update_function(*new_id, Some(inlined)).unwrap(); } else { - let name = self.get_variable_name(v); - let new_id = new_bn.as_graph().find_variable(name.as_str()).unwrap(); - old_to_new_var.push(new_id); + // This variable is not regulated by `var`, hence we just copy. + if let Some(update) = old_bn.get_update_function(old_var).as_ref() { + let renamed = update.rename_all(&new_var_id, &new_param_id); + new_bn.set_update_function(*new_id, Some(renamed)).unwrap(); + } } } - // Then we do the same for parameters. However, since we are only doing inlining, the new - // network will actually contain exactly the same parameters. - let mut old_to_new_param = Vec::with_capacity(self.num_parameters()); - for param in self.parameters() { - let param = &self[param]; - let new_id = new_bn - .add_parameter(param.get_name(), param.get_arity()) - .unwrap(); - old_to_new_param.push(new_id); + if let Some((p_id, name)) = rename_parameter { + new_bn.rename_parameter(p_id, name.as_str()).unwrap(); } - // Now we can finally copy all the update functions, possibly inlining them along the way. - let Some(var_function) = self.get_update_function(var).as_ref() else { - // Cannot inline variable with implicit update function. - return None; - }; + // 7. Prune unused parameters. This is necessary because if we are inlining an output + // variable, we might delete the last occurrence of a parameter, in which case we + // ideally want to remove it from the network completely. + new_bn = new_bn.prune_unused_parameters(); - for v in self.variables() { - if v == var { - continue; + // 8. If we don't want to fix the regulatory graph afterwards, we are done. + // However, if we do want to fix it, we will need to create a symbolic context + // and start building the network from scratch. + // This is essentially `infer_valid_graph`, but only for the relevant regulations. + if !repair_graph { + new_bn + } else { + let ctx = SymbolicContext::new(&new_bn).unwrap(); + + let repair_targets = var_targets + .iter() + .filter_map(|it| new_var_id.get(it).cloned()) + .collect::>(); + + let mut new_new_rg = RegulatoryGraph::new(new_bn.as_graph().variable_names()); + + // We need to clone the regulations because we will might be modifying the BN + // in the loop (not the regulations though). + for reg in Vec::from_iter(new_bn.as_graph().regulations().cloned()) { + if !repair_targets.contains(®.target) { + // Regulations that do not involve one of the relevant targets are copied. + new_new_rg.add_raw_regulation(reg).unwrap(); + } else { + // Otherwise, let's try to build the update function (we know that all of + // these exist, since we just inlined into them) and infer its properties. + + let fun = new_bn.get_update_function(reg.target).as_ref().unwrap(); + let fun_bdd = ctx.mk_fn_update_true(fun); + let Some(new_reg) = RegulationConstraint::fix_regulation(&ctx, ®, &fun_bdd) + else { + // This regulation is irrelevant, hence we can substitute the variable + // for a constant, and use that instead. This simplified function will + // be copied into the result instead of the original one. + let eliminated = fun + .substitute_variable(reg.regulator, &FnUpdate::Const(false)) + .simplify_constants(); + new_bn + .set_update_function(reg.target, Some(eliminated)) + .unwrap_or_else(|_| { + unreachable!("Simplified function must be still valid."); + }); + continue; + }; + new_new_rg.add_raw_regulation(new_reg).unwrap(); + } } - let new_id = old_to_new_var[v.to_index()]; - let old_function = self.get_update_function(v).as_ref(); - if !var_targets.contains(&v) { - // This variable is not regulated by `var`, hence we don't need any inlining - // and we can just move the function to the new network. - let new_function = - old_function.map(|it| it.substitute(&old_to_new_var, &old_to_new_param)); - new_bn.set_update_function(new_id, new_function).unwrap(); - } else { - // This variable is regulated by `var`, hence we first need to inline the - // update function and then translate the result into the new network. - let Some(old_function) = old_function else { - // Cannot inline into missing update function. - return None; - }; - let Some(inlined_function) = old_function.substitute_variable(var, var_function) - else { - // We tried to inline the function, but it did not work. Most likely - // because there is an unknown function where - // the variable is used as an argument. - return None; + // Finally, just copy all the functions to the new network. They should still be valid. + let mut new_new_bn = BooleanNetwork::new(new_new_rg); + for param in new_bn.parameters() { + let param = new_bn.get_parameter(param); + new_new_bn + .add_parameter(param.name.as_str(), param.arity) + .unwrap(); + } + for var in new_bn.variables() { + let Some(update) = new_bn.get_update_function(var).as_ref() else { + continue; }; - let new_function = inlined_function.substitute(&old_to_new_var, &old_to_new_param); - new_bn - .set_update_function(new_id, Some(new_function)) + new_new_bn + .set_update_function(var, Some(update.clone())) .unwrap(); } - } - Some(new_bn) + // In very rare instances, we can eliminate a parameter by detecting an unused + // regulation and simplifying the variable away (e.g. `x & !x & f(z)` simplifies + // to `false`). Hence we have to prune parameters again here. + new_new_bn.prune_unused_parameters() + } } } @@ -758,32 +1083,49 @@ mod test { fn test_rg_inference_with_parameters() { let bn = BooleanNetwork::try_from( r" - a -> c - b -| c - $c: f(a, b) + a ->? c + b -? c + d -> c + $d: true + $c: f(a, b, d | !d) ", ) .unwrap(); let expected = BooleanNetwork::try_from( r" - a -?? c - b -?? c - $c: f(a, b) + a ->? c + b -? c + $c: f(a, b, true) + $d: true ", ) .unwrap(); assert_eq!(expected, bn.infer_valid_graph().unwrap()); - let invalid = BooleanNetwork::try_from( + let bn = BooleanNetwork::try_from( r" a -> c + # This monotonicity is intentionally wrong. b -| c - $c: b & x & (a | !a) + $a: true + $b: true + # x is a parameter. + $c: b & ((a | !a) | x) + ", + ) + .unwrap(); + + let expected = BooleanNetwork::try_from( + r" + b -> c + $a: true + $b: true + $c: b ", ) .unwrap(); - assert!(invalid.infer_valid_graph().is_err()); + assert_eq!(expected, bn.infer_valid_graph().unwrap()); } #[test] @@ -807,29 +1149,60 @@ mod test { d ->? y e ->? y - # Both d and e appear in y, but only e can be erased as d appears in an uninterpreted - # function. + # Both d and e appear in y, but d appears in an uninterpreted function. $y: fun(d) | e f ->? z z ->? z - # f cannot be erased because it does not appear in z + # f does not appear in z, hence it will just disappear. + # z is an input based on identity function, hence it will be inlined, but + # it isn't used either, so it will also disappear. $z: z g ->? w - # g cannot be erased because w does not have a function + # g will be inlined into a newly created function for w. ", ) .unwrap(); - let inlined = bn.inline_inputs(); + let inlined = bn.inline_inputs(false, true); + + // Should be a,b,e,d,g,fn_w,fun. + assert_eq!(inlined.num_parameters(), 7); + // Should be c,w,x,y. + assert_eq!(inlined.num_vars(), 4); - assert_eq!(inlined.num_parameters(), 4); - assert_eq!(inlined.num_vars(), 8); assert!(inlined.find_parameter("a").is_some()); assert!(inlined.find_parameter("b").is_some()); assert!(inlined.find_parameter("e").is_some()); + assert!(inlined.find_parameter("d").is_some()); + assert!(inlined.find_parameter("g").is_some()); assert!(inlined.find_parameter("fun").is_some()); + assert!(inlined.find_parameter("fn_w").is_some()); + assert!(inlined.as_graph().find_variable("c").is_some()); + assert!(inlined.as_graph().find_variable("w").is_some()); + assert!(inlined.as_graph().find_variable("x").is_some()); + assert!(inlined.as_graph().find_variable("y").is_some()); + + // This should be only detected using BDDs. + let bn = BooleanNetwork::try_from( + r" + a -? a + a -> b + $a: (!a => a) + $b: _f(a) + ", + ) + .unwrap(); + + let expected = BooleanNetwork::try_from( + r" + $b: _f(a) + ", + ) + .unwrap(); + assert_ne!(expected, bn.inline_inputs(false, true)); + assert_eq!(expected, bn.inline_inputs(true, true)); } #[test] @@ -867,7 +1240,7 @@ mod test { ", ) .unwrap(); - assert_eq!(bn.inline_variable(b), Some(expected)); + assert_eq!(bn.inline_variable(b, false), Some(expected)); // Then remove `d`, which is an output, so does not connect to anything. let expected = BooleanNetwork::try_from( @@ -882,7 +1255,7 @@ mod test { ", ) .unwrap(); - assert_eq!(bn.inline_variable(d), Some(expected)); + assert_eq!(bn.inline_variable(d, false), Some(expected)); // Reducing `a` should correctly propagate the unknown function. let expected = BooleanNetwork::try_from( @@ -897,10 +1270,21 @@ mod test { ", ) .unwrap(); - assert_eq!(bn.inline_variable(a), Some(expected)); + assert_eq!(bn.inline_variable(a, false), Some(expected)); - // Reducing `c` should fail because it is inlining into an unknown function. - assert_eq!(bn.inline_variable(c), None); + let expected = BooleanNetwork::try_from( + r" + a -| b + b -?? a + a -?? a + b -> d + $a: p(!b & a) + $b: !a + $d: b + ", + ) + .unwrap(); + assert_eq!(bn.inline_variable(c, false), Some(expected)); // Finally, a quick test for self-regulations: let bn = BooleanNetwork::try_from( @@ -914,6 +1298,90 @@ mod test { ) .unwrap(); let b = bn.as_graph().find_variable("b").unwrap(); - assert_eq!(bn.inline_variable(b), None); + assert_eq!(bn.inline_variable(b, false), None); + + // Test that a parameter is indeed removed if it is no longer relevant. + let bn = BooleanNetwork::try_from( + r" + a -> b + $a: true + $b: f(a) + ", + ) + .unwrap(); + let expected = BooleanNetwork::try_from( + r" + $a: true + ", + ) + .unwrap(); + let b = bn.as_graph().find_variable("b").unwrap(); + + assert_eq!(expected, bn.inline_variable(b, true).unwrap()); + } + + #[test] + fn test_constant_inlining() { + let bn = BooleanNetwork::try_from( + r" + b -> x + c -> x + + # Only c is a constant, but it is enough to turn x into a constant. + b -> b + $b: b + $c: true + + $x: b | c + + # This will also inline because x is a constant. + x -> y + $y: (x & !x) + + # Here, y will inline, but b should stay. + y -> z + b -| z + $z: !b | y + ", + ) + .unwrap(); + + let expected = BooleanNetwork::try_from( + r" + b -> b + $b: b + b -| z + $z: !b + ", + ) + .unwrap(); + + assert_eq!(bn.inline_constants(false, true), expected); + + // Here, a/b should be only detected as constants through BDDs. + let bn = BooleanNetwork::try_from( + r" + a -? a + $a: (a & !a) + b -? b + $b: (b | !b) + a -> c + b -> c + c -> c + $c: (a & b) | c + ", + ) + .unwrap(); + + let expected = BooleanNetwork::try_from( + r" + c -> c + $c: c + ", + ) + .unwrap(); + + assert_ne!(bn.inline_constants(false, true), expected); + assert_eq!(bn.inline_constants(true, true), expected); } } diff --git a/src/_impl_fn_update.rs b/src/_impl_fn_update.rs index 4b11f8f..02d0213 100644 --- a/src/_impl_fn_update.rs +++ b/src/_impl_fn_update.rs @@ -1,7 +1,8 @@ use crate::symbolic_async_graph::SymbolicContext; +use crate::BinaryOp::{And, Iff, Imp, Or, Xor}; use crate::FnUpdate::*; use crate::_aeon_parser::FnUpdateTemp; -use crate::{BinaryOp, BooleanNetwork, ExtendedBoolean, FnUpdate, ParameterId, Space, VariableId}; +use crate::{BinaryOp, BooleanNetwork, FnUpdate, ParameterId, VariableId}; use biodivine_lib_bdd::{Bdd, BddPartialValuation, BddVariable}; use std::collections::{HashMap, HashSet}; @@ -23,12 +24,21 @@ impl FnUpdate { Var(id) } - /// Create a `p(x_1, ..., x_k)` formula where `p` is a parameter function and `x_1` through - /// `x_k` are its arguments. - pub fn mk_param(id: ParameterId, args: &[VariableId]) -> FnUpdate { + /// Create a `p(e_1, ..., e_k)` formula where `p` is a parameter function and `e_1` through + /// `e_k` are general argument expressions. + pub fn mk_param(id: ParameterId, args: &[FnUpdate]) -> FnUpdate { Param(id, args.to_vec()) } + /// Same as [Self::mk_param], but can take variable IDs as arguments directly. + pub fn mk_basic_param(id: ParameterId, args: &[VariableId]) -> FnUpdate { + let args = args + .iter() + .map(|it| FnUpdate::mk_var(*it)) + .collect::>(); + Param(id, args) + } + /// Create a `!phi` formula, where `phi` is an inner `FnUpdate`. pub fn mk_not(inner: FnUpdate) -> FnUpdate { Not(Box::new(inner)) @@ -46,27 +56,27 @@ impl FnUpdate { /// Create a conjunction. pub fn and(self, other: FnUpdate) -> FnUpdate { - FnUpdate::mk_binary(BinaryOp::And, self, other) + FnUpdate::mk_binary(And, self, other) } /// Create a disjunction. pub fn or(self, other: FnUpdate) -> FnUpdate { - FnUpdate::mk_binary(BinaryOp::Or, self, other) + FnUpdate::mk_binary(Or, self, other) } /// Create an exclusive or. pub fn xor(self, other: FnUpdate) -> FnUpdate { - FnUpdate::mk_binary(BinaryOp::Xor, self, other) + FnUpdate::mk_binary(Xor, self, other) } /// Create an implication. pub fn implies(self, other: FnUpdate) -> FnUpdate { - FnUpdate::mk_binary(BinaryOp::Imp, self, other) + FnUpdate::mk_binary(Imp, self, other) } /// Create an equivalence. pub fn iff(self, other: FnUpdate) -> FnUpdate { - FnUpdate::mk_binary(BinaryOp::Iff, self, other) + FnUpdate::mk_binary(Iff, self, other) } /// If `Const`, return the value, otherwise return `None`. @@ -86,7 +96,7 @@ impl FnUpdate { } /// If `Param`, return the id and args, otherwise return `None`. - pub fn as_param(&self) -> Option<(ParameterId, &[VariableId])> { + pub fn as_param(&self) -> Option<(ParameterId, &[FnUpdate])> { match self { Param(id, args) => Some((*id, args)), _ => None, @@ -174,7 +184,7 @@ impl FnUpdate { let mut clause = build_literal(map, literals.next().unwrap()); for literal in literals { let literal = build_literal(map, literal); - clause = FnUpdate::mk_binary(BinaryOp::And, clause, literal); + clause = FnUpdate::mk_binary(And, clause, literal); } clause } @@ -183,7 +193,7 @@ impl FnUpdate { let mut result = build_clause(&state_variables, clauses.next().unwrap()); for clause in clauses { let clause = build_clause(&state_variables, clause); - result = FnUpdate::mk_binary(BinaryOp::Or, result, clause); + result = FnUpdate::mk_binary(Or, result, clause); } result } @@ -197,8 +207,8 @@ impl FnUpdate { args.insert(*id); } Param(_, p_args) => { - for id in p_args { - args.insert(*id); + for fun in p_args { + r_arguments(fun, args); } } Not(inner) => r_arguments(inner, args), @@ -222,8 +232,11 @@ impl FnUpdate { match function { Const(_) => (), Var(_) => (), - Param(id, _) => { + Param(id, args) => { params.insert(*id); + for fun in args { + r_parameters(fun, params); + } } Not(inner) => r_parameters(inner, params), Binary(_, l, r) => { @@ -252,9 +265,9 @@ impl FnUpdate { if args.is_empty() { context[*id].get_name().to_string() } else { - let mut arg_string = format!("({}", context.get_variable_name(args[0])); + let mut arg_string = format!("({}", args[0].to_string(context)); for arg in args.iter().skip(1) { - arg_string = format!("{}, {}", arg_string, context.get_variable_name(*arg)); + arg_string = format!("{}, {}", arg_string, arg.to_string(context)); } format!("{}{})", context[*id].get_name(), arg_string) } @@ -285,27 +298,27 @@ impl FnUpdate { let left = left.evaluate(values); let right = right.evaluate(values); match op { - BinaryOp::And => match (left, right) { + And => match (left, right) { (Some(false), _) => Some(false), (_, Some(false)) => Some(false), (Some(true), Some(true)) => Some(true), _ => None, }, - BinaryOp::Or => match (left, right) { + Or => match (left, right) { (Some(true), _) => Some(true), (_, Some(true)) => Some(true), (Some(false), Some(false)) => Some(false), _ => None, }, - BinaryOp::Iff => match (left, right) { + Iff => match (left, right) { (Some(left), Some(right)) => Some(left == right), _ => None, }, - BinaryOp::Xor => match (left, right) { + Xor => match (left, right) { (Some(left), Some(right)) => Some(left != right), _ => None, }, - BinaryOp::Imp => match (left, right) { + Imp => match (left, right) { (Some(false), _) => Some(true), (_, Some(true)) => Some(true), (Some(true), Some(false)) => Some(false), @@ -316,43 +329,6 @@ impl FnUpdate { } } - /// Test that this update function is a syntactic specialisation of the provided `FnUpdate`. - /// - /// Syntactic specialisation is a function that has the same abstract syntax tree, except that - /// some occurrences of parameters can be substituted for more concrete Boolean functions. - /// - /// Note that this is not entirely bulletproof, as it does not check for usage of multiple - /// parameters within the same function, which could influence the semantics of the main - /// function, but does not influence the specialisation. - pub fn is_specialisation_of(&self, other: &FnUpdate) -> bool { - match other { - Const(_) => self == other, - Var(_) => self == other, - Not(inner) => { - if let Some(self_inner) = self.as_not() { - self_inner.is_specialisation_of(inner) - } else { - false - } - } - Binary(op, left, right) => { - if let Some((self_left, self_op, self_right)) = self.as_binary() { - self_op == *op - && self_left.is_specialisation_of(left) - && self_right.is_specialisation_of(right) - } else { - false - } - } - Param(_, args) => { - // Every argument in this sub-tree must be declared in the parameter. - self.collect_arguments() - .iter() - .all(|arg| args.contains(arg)) - } - } - } - /// Allows us to iterate through all nodes of the abstract syntax tree of this function /// in post-order. /// @@ -364,7 +340,12 @@ impl FnUpdate { { match self { Const(_) => action(self), - Param(_, _) => action(self), + Param(_, args) => { + for arg in args { + arg.walk_postorder(action); + } + action(self) + } Var(_) => action(self), Not(inner) => { inner.walk_postorder(action); @@ -378,71 +359,66 @@ impl FnUpdate { } } - /// Create a copy of this function which replaces every occurrence of every - /// `VariableId` with a new one supplied by the provided vector (original `VariableId` - /// is the index into the vector). Similarly replaces every `ParameterId`. - /// - /// TODO: - /// The name of this function is very much not great. We should rename it to something - /// more natural, like "substitute_symbols". Also... is anybody actually using this? - pub fn substitute(&self, vars: &[VariableId], params: &[ParameterId]) -> FnUpdate { + /// Create a copy of this [FnUpdate] with every occurrence of [VariableId] `var` substituted + /// for [FnUpdate] `expression`. + pub fn substitute_variable(&self, var: VariableId, expression: &FnUpdate) -> FnUpdate { match self { Const(_) => self.clone(), - Param(id, args) => { - let new_args = args.iter().map(|it| vars[it.0]).collect(); - Param(params[id.0], new_args) + Param(p, args) => { + let new_args = args + .iter() + .map(|it| it.substitute_variable(var, expression)) + .collect::>(); + Param(*p, new_args) + } + Var(id) => { + if id == &var { + expression.clone() + } else { + self.clone() + } } - Var(id) => FnUpdate::mk_var(vars[id.0]), Not(inner) => { - let inner = inner.substitute(vars, params); + let inner = inner.substitute_variable(var, expression); FnUpdate::mk_not(inner) } Binary(op, left, right) => { - let left = left.substitute(vars, params); - let right = right.substitute(vars, params); + let left = left.substitute_variable(var, expression); + let right = right.substitute_variable(var, expression); FnUpdate::mk_binary(*op, left, right) } } } - /// Create a copy of this [FnUpdate] with every occurrence of [VariableId] `var` substituted - /// for [FnUpdate] `expression`. - /// - /// At the moment, the process can fail if there are uninterpreted functions (parameters) - /// in which `var` appears as an argument. This is because we don't have a symbolic translation - /// for such functions (yet). In such case, the function returns `None`. - /// - /// TODO: Once we actually have *full* support for any combination of nested uninterpreted - /// functions, this operation can be declared as infallible. - pub fn substitute_variable(&self, var: VariableId, expression: &FnUpdate) -> Option { - Some(match self { + /// Rename all occurrences of the specified `variables` and `parameters` to new IDs. + pub fn rename_all( + &self, + variables: &HashMap, + parameters: &HashMap, + ) -> FnUpdate { + match self { Const(_) => self.clone(), - Param(_, args) => { - // If the variable is used in an uninterpreted function, - // we cannot perform the substitution. - if args.contains(&var) { - return None; - } else { - self.clone() - } - } - Var(id) => { - if id == &var { - expression.clone() - } else { - self.clone() + Var(id) => match variables.get(id) { + Some(new_id) => Var(*new_id), + None => self.clone(), + }, + Param(id, args) => { + let args = args + .iter() + .map(|it| it.rename_all(variables, parameters)) + .collect::>(); + match parameters.get(id) { + Some(new_id) => Param(*new_id, args), + None => Param(*id, args), } } - Not(inner) => { - let inner = inner.substitute_variable(var, expression)?; - FnUpdate::mk_not(inner) - } + Not(inner) => inner.rename_all(variables, parameters).negation(), Binary(op, left, right) => { - let left = left.substitute_variable(var, expression)?; - let right = right.substitute_variable(var, expression)?; + let left = left.rename_all(variables, parameters); + let right = right.rename_all(variables, parameters); FnUpdate::mk_binary(*op, left, right) } - }) + } } /// Returns true if this update function uses the given parameter. @@ -460,10 +436,10 @@ impl FnUpdate { /// Returns true if this update function uses the given variable. pub fn contains_variable(&self, variable: VariableId) -> bool { let mut result = false; - let mut is_var = |it: &FnUpdate| match it { - Var(id) => result = result || (*id == variable), - Param(_, args) => result = result || args.contains(&variable), - _ => {} + let mut is_var = |it: &FnUpdate| { + if let Var(id) = it { + result = result || (*id == variable); + } }; self.walk_postorder(&mut is_var); result @@ -474,26 +450,36 @@ impl FnUpdate { /// /// Note that the result is neither a conjunction or disjunctive normal form, it just /// eliminates all operators other than conjunction and disjunction. + /// + /// Furthermore, when the function contains parameters with expression arguments, the + /// arguments are normalized as well. pub fn to_and_or_normal_form(&self) -> FnUpdate { match self { - Const(_) | Var(_) | Param(_, _) => self.clone(), + Const(_) | Var(_) => self.clone(), + Param(p, args) => { + let args = args + .iter() + .map(|it| it.to_and_or_normal_form()) + .collect::>(); + Param(*p, args) + } Not(inner) => inner.to_and_or_normal_form().negation(), Binary(op, left, right) => { let left = left.to_and_or_normal_form(); let right = right.to_and_or_normal_form(); match op { - BinaryOp::And | BinaryOp::Or => FnUpdate::mk_binary(*op, left, right), - BinaryOp::Imp => { + And | Or => FnUpdate::mk_binary(*op, left, right), + Imp => { // !left | right left.negation().or(right) } - BinaryOp::Xor => { + Xor => { // (left | right) & !(left & right) let both = left.clone().and(right.clone()); let one = left.and(right); one.and(both.negation()) } - BinaryOp::Iff => { + Iff => { // (left & right) | (!left & !right) let both = left.clone().and(right.clone()); let neither = left.negation().and(right.negation()); @@ -510,6 +496,9 @@ impl FnUpdate { /// Note that constants will be automatically negated (true => false, false => true). Also, /// keep in mind that this will rewrite binary operators (and => or, iff => xor, etc.), so /// don't expect the function to look the same afterwards. + /// + /// Similar to [Self::to_and_or_normal_form], when the function contains parameters with + /// complex arguments, each argument is also normalized. pub fn distribute_negation(&self) -> FnUpdate { fn recursion(update: &FnUpdate, invert: bool) -> FnUpdate { match update { @@ -522,10 +511,15 @@ impl FnUpdate { } } Param(id, args) => { + let args = args + .iter() + .map(|it| it.distribute_negation()) + .collect::>(); + let param = Param(*id, args); if invert { - Param(*id, args.clone()).negation() + param.negation() } else { - update.clone() + param } } Not(inner) => recursion(inner, !invert), @@ -536,31 +530,31 @@ impl FnUpdate { } else { // Otherwise we must do magic. match op { - BinaryOp::And => { + And => { // !(left & right) = (!left | !right) let left = recursion(left, true); let right = recursion(right, true); left.or(right) } - BinaryOp::Or => { + Or => { // !(left | right) = (!left & !right) let left = recursion(left, true); let right = recursion(right, true); left.and(right) } - BinaryOp::Imp => { + Imp => { // !(left => right) = (left & !right) let left = recursion(left, false); let right = recursion(right, true); left.and(right) } - BinaryOp::Xor => { + Xor => { // !(left ^ right) = (left <=> right) let left = recursion(left, false); let right = recursion(right, false); left.iff(right) } - BinaryOp::Iff => { + Iff => { // !(left <=> right) = (left ^ right) let left = recursion(left, false); let right = recursion(right, false); @@ -575,33 +569,69 @@ impl FnUpdate { recursion(self, false) } - /// Perform partial evaluation of this function using extended Boolean values in the given - /// `Space`. - - pub fn eval_in_space(&self, space: &Space) -> ExtendedBoolean { + /// Utility function that eliminates unnecessary constants from this update function + /// using standard syntactic transformations. + pub fn simplify_constants(&self) -> FnUpdate { match self { - Const(value) => { - if *value { - ExtendedBoolean::One + Const(value) => Const(*value), + Var(id) => Var(*id), + Param(id, args) => { + let args = args + .iter() + .map(|it| it.simplify_constants()) + .collect::>(); + Param(*id, args) + } + Not(inner) => { + // !true = false + // !false = true + let inner = inner.simplify_constants(); + if let Some(inner_const) = inner.as_const() { + Const(!inner_const) } else { - ExtendedBoolean::Zero + Not(Box::new(inner)) } } - Var(var) => space[*var], - Param(_, _) => { - // We assume that a parameter can evaluate to anything. - ExtendedBoolean::Any - } - Not(inner) => inner.eval_in_space(space).negate(), Binary(op, left, right) => { - let left = left.eval_in_space(space); - let right = right.eval_in_space(space); + let left = left.simplify_constants(); + let right = right.simplify_constants(); match op { - BinaryOp::Or => left.or(right), - BinaryOp::And => left.and(right), - BinaryOp::Imp => left.implies(right), - BinaryOp::Iff => left.iff(right), - BinaryOp::Xor => left.xor(right), + And => match (left.as_const(), right.as_const()) { + (Some(false), _) | (_, Some(false)) => Const(false), + (Some(true), _) => right, + (_, Some(true)) => left, + _ => left.and(right), + }, + Or => match (left.as_const(), right.as_const()) { + (Some(true), _) | (_, Some(true)) => Const(true), + (Some(false), _) => right, + (_, Some(false)) => left, + _ => left.or(right), + }, + Xor => match (left.as_const(), right.as_const()) { + (Some(true), Some(true)) | (Some(false), Some(false)) => Const(false), + (Some(false), Some(true)) | (Some(true), Some(false)) => Const(true), + (Some(false), _) => right, + (_, Some(false)) => left, + (Some(true), _) => FnUpdate::mk_not(right), + (_, Some(true)) => FnUpdate::mk_not(left), + _ => left.xor(right), + }, + Iff => match (left.as_const(), right.as_const()) { + (Some(true), Some(true)) | (Some(false), Some(false)) => Const(true), + (Some(false), Some(true)) | (Some(true), Some(false)) => Const(false), + (Some(true), _) => right, + (_, Some(true)) => left, + (Some(false), _) => FnUpdate::mk_not(right), + (_, Some(false)) => FnUpdate::mk_not(left), + _ => left.iff(right), + }, + Imp => match (left.as_const(), right.as_const()) { + (Some(false), _) | (_, Some(true)) => Const(true), + (Some(true), _) => right, + (_, Some(false)) => FnUpdate::mk_not(left), + _ => left.implies(right), + }, } } } @@ -616,38 +646,6 @@ mod tests { use std::collections::HashMap; use std::convert::TryFrom; - #[test] - fn fn_update_specialisation_test() { - let bn = BooleanNetwork::try_from( - r" - a -> c1 - b -> c1 - a -> c2 - b -> c2 - a -> c3 - b -> c3 - $c1: !(a => b) | f(a, b) - $c2: !(a => b) | ((a <=> b) & g(b)) - $c3: (a => b) | f(a, b) - ", - ) - .unwrap(); - - let c1 = bn.as_graph().find_variable("c1").unwrap(); - let c2 = bn.as_graph().find_variable("c2").unwrap(); - let c3 = bn.as_graph().find_variable("c3").unwrap(); - - let fn_c1 = bn.get_update_function(c1).as_ref().unwrap(); - let fn_c2 = bn.get_update_function(c2).as_ref().unwrap(); - let fn_c3 = bn.get_update_function(c3).as_ref().unwrap(); - - assert!(fn_c2.is_specialisation_of(fn_c1)); - assert!(!fn_c1.is_specialisation_of(fn_c2)); - assert!(!fn_c3.is_specialisation_of(fn_c1)); - assert!(!fn_c3.is_specialisation_of(fn_c2)); - assert!(fn_c3.is_specialisation_of(fn_c3)); - } - #[test] fn fn_update_eval_test() { let bn = BooleanNetwork::try_from( @@ -746,7 +744,7 @@ mod tests { assert_eq!(fun, bn.get_update_function(c).as_ref().unwrap()); // Construct a FnUpdate - let f_a_b = FnUpdate::mk_param(id_f, &vec![a, b]); + let f_a_b = FnUpdate::mk_param(id_f, &[FnUpdate::mk_var(a), FnUpdate::mk_var(b)]); let f_a = FnUpdate::mk_var(a); let mut fun_2 = f_a_b.or(FnUpdate::mk_true().or(FnUpdate::mk_false())); fun_2 = f_a.clone().iff(fun_2.negation()); @@ -771,7 +769,10 @@ mod tests { assert_eq!(a, l.as_var().unwrap()); let inner = r.as_not().unwrap(); let (l, _, r) = inner.as_binary().unwrap(); - assert_eq!((id_f, vec![a, b].as_slice()), l.as_param().unwrap()); + assert_eq!( + (id_f, vec![FnUpdate::Var(a), FnUpdate::Var(b)].as_slice()), + l.as_param().unwrap() + ); let (l, _, r) = r.as_binary().unwrap(); assert!(l.as_const().unwrap()); assert!(!r.as_const().unwrap()); @@ -830,9 +831,170 @@ mod tests { let fn3 = FnUpdate::try_from_str("((b <=> c) & b) | !(c & !(b <=> c)) & f(b, c)", &bn).unwrap(); let fn4 = FnUpdate::try_from_str("(a & b & f(a, b))", &bn).unwrap(); + let fn5 = FnUpdate::try_from_str("((b <=> c) & b & f((b <=> c), b))", &bn).unwrap(); let a = bn.as_graph().find_variable("a").unwrap(); - assert_eq!(Some(fn3), fn1.substitute_variable(a, &fn2)); - assert_eq!(None, fn4.substitute_variable(a, &fn2)); + assert_eq!(fn3, fn1.substitute_variable(a, &fn2)); + assert_eq!(fn5, fn4.substitute_variable(a, &fn2)); + } + + #[test] + pub fn test_constant_simplification() { + let bn = BooleanNetwork::try_from( + r" + a -> b + b -> c + a -> c + $c: f(a, b) | g(a, b) + ", + ) + .unwrap(); + + assert_eq!( + FnUpdate::try_from_str("true & b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b & true", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("false & b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("false", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b & false", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("false", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b | false", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("false | b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b | true", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("true", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("true | b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("true", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b ^ true", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("!b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("true ^ b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("!b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b ^ false", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("false ^ b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b <=> true", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("true <=> b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b <=> false", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("!b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("false <=> b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("!b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b => false", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("!b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("false => b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("true", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("b => true", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("true", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("true => b", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("b", &bn).unwrap(), + ); + + assert_eq!( + FnUpdate::try_from_str("true & f(b & false, c) => g(a, b) | (a <=> true)", &bn) + .unwrap() + .simplify_constants(), + FnUpdate::try_from_str("f(false, c) => g(a, b) | a", &bn).unwrap(), + ); } } diff --git a/src/_impl_regulatory_graph/_impl_misc.rs b/src/_impl_regulatory_graph/_impl_misc.rs index eb22db6..3209d66 100644 --- a/src/_impl_regulatory_graph/_impl_misc.rs +++ b/src/_impl_regulatory_graph/_impl_misc.rs @@ -102,6 +102,11 @@ impl RegulatoryGraph { )) } } + + /// Copy the variable names from this graph into a separate vector. + pub fn variable_names(&self) -> Vec { + self.variables.iter().map(|it| it.name.clone()).collect() + } } /// Some basic utility methods for inspecting the `RegulatoryGraph`. diff --git a/src/_impl_space.rs b/src/_impl_space.rs index a835ed3..6200f9f 100644 --- a/src/_impl_space.rs +++ b/src/_impl_space.rs @@ -100,33 +100,4 @@ impl Space { pub fn count_any(&self) -> usize { self.0.iter().filter(|it| **it == Any).count() } - - /// Check if this `Space` is a **trap** space within the given `BooleanNetwork`. - /// - /// A trap space is a `Space` in which every asynchronous transition from every state leads - /// to a state within the same `Space`. - pub fn is_trap_space(&self, network: &BooleanNetwork) -> bool { - for var in network.variables() { - let expected_value = self[var]; - if expected_value.is_fixed() { - if let Some(update) = network.get_update_function(var) { - let actual_value = update.eval_in_space(self); - if expected_value != actual_value { - // Since expected value is fixed, either actual value is a different - // constant, or `Any`, in which case this is still not a trap space. - return false; - } - } else { - // If the function is unknown, the whole thing is a giant parameter that we - // know nothing about, hence the value cannot be fixed. - return false; - } - } else { - // If the expected value is `Any`, then there can be no transitions escaping - // using this variable, so we can just skip it. - } - } - - true - } } diff --git a/src/async_graph/_impl_async_graph.rs b/src/async_graph/_impl_async_graph.rs deleted file mode 100644 index 0ae24b6..0000000 --- a/src/async_graph/_impl_async_graph.rs +++ /dev/null @@ -1,98 +0,0 @@ -use crate::async_graph::{AsyncGraph, AsyncGraphEdgeParams, DefaultEdgeParams}; -use crate::BooleanNetwork; - -impl AsyncGraph { - /// Create a new `AsyncGraph` from the given `BooleanNetwork` using default edge parameter implementation. - pub fn new(network: BooleanNetwork) -> Result, String> { - if network.graph.num_vars() > 32 { - Err("Can't create the graph. At most 32 variables supported".to_string()) - } else { - let edge_params = DefaultEdgeParams::new(network)?; - Ok(AsyncGraph { edges: edge_params }) - } - } -} - -impl AsyncGraph { - /// Create a new `AsyncGraph` using given edge parametrisation. - pub fn new_with_edges(edge_params: Params) -> Result, String> { - if edge_params.network().graph.num_vars() > 32 { - Err("Can't create the graph. At most 32 variables supported".to_string()) - } else { - Ok(AsyncGraph { edges: edge_params }) - } - } - - /// Return the total number of states in this graph. - pub fn num_states(&self) -> usize { - 1 << self.network().graph.num_vars() - } - - /// Return a reference to the original Boolean network. - pub fn network(&self) -> &BooleanNetwork { - self.edges.network() - } - - /// Expose the inner edge implementation. - pub fn edges(&self) -> &Params { - &self.edges - } - - /// Make a witness network for one parametrisation in the given set. - pub fn make_witness(&self, params: &Params::ParamSet) -> BooleanNetwork { - self.edges.make_witness(params) - } - - /// Return an empty set of parameters. - pub fn empty_params(&self) -> &Params::ParamSet { - self.edges.empty_params() - } - - /// Return a full set of parameters. - pub fn unit_params(&self) -> &Params::ParamSet { - self.edges.unit_params() - } -} - -#[cfg(test)] -mod tests { - use crate::async_graph::AsyncGraph; - use crate::BooleanNetwork; - use std::convert::TryFrom; - - #[test] - fn test_graph_unit_set_anonymous_params() { - let network = BooleanNetwork::try_from( - " - a ->? b - a -> a - b -| b - b -|? a - ", - ) - .unwrap(); - let graph = AsyncGraph::new(network).unwrap(); - // both functions can have 3 different valuations, so 9 in total - assert_eq!(9.0, graph.unit_params().cardinality()); - } - - #[test] - fn test_graph_unit_set_names_params() { - let network = BooleanNetwork::try_from( - " - a ->? b - a -> a - b -| b - b -|? a - $a: a | p(b) - $b: q(a, b) & a - ", - ) - .unwrap(); - let graph = AsyncGraph::new(network).unwrap(); - // p can have 2 valuations, q can have 4, 8 in total - // actually, for b, there is only one possible function but it is achieved - // regardless of two values of q. - assert_eq!(8.0, graph.unit_params().cardinality()); - } -} diff --git a/src/async_graph/_impl_default_edge_params.rs b/src/async_graph/_impl_default_edge_params.rs deleted file mode 100644 index b91c2a4..0000000 --- a/src/async_graph/_impl_default_edge_params.rs +++ /dev/null @@ -1,72 +0,0 @@ -use crate::async_graph::{AsyncGraphEdgeParams, DefaultEdgeParams}; -use crate::bdd_params::{build_static_constraints, BddParameterEncoder, BddParams}; -use crate::biodivine_std::structs::IdState; -use crate::biodivine_std::traits::Set; -use crate::{BooleanNetwork, VariableId}; - -impl DefaultEdgeParams { - /// New default edge parametrisation for the given network. Warning: computes the unit set, which can be expensive. - pub fn new(network: BooleanNetwork) -> Result { - let encoder = BddParameterEncoder::new(&network); - Self::new_with_custom_encoder(network, encoder) - } - - pub fn new_with_custom_encoder( - network: BooleanNetwork, - encoder: BddParameterEncoder, - ) -> Result { - let unit_set = BddParams::from(build_static_constraints(&network, &encoder)); - if unit_set.is_empty() { - Err("No update functions satisfy given constraints".to_string()) - } else { - Ok(DefaultEdgeParams { - empty_set: BddParams::from(encoder.bdd_variables.mk_false()), - network, - encoder, - unit_set, - }) - } - } -} - -impl AsyncGraphEdgeParams for DefaultEdgeParams { - type ParamSet = BddParams; - - fn network(&self) -> &BooleanNetwork { - &self.network - } - - fn empty_params(&self) -> &Self::ParamSet { - &self.empty_set - } - - fn unit_params(&self) -> &Self::ParamSet { - &self.unit_set - } - - /// Compute the parameter set which enables the value of `variable` to be flipped - /// in the given `state`. - /// - /// Note that this set is not a subset of the `unit_set`! It is really just the flip condition. - fn edge_params(&self, state: IdState, variable: VariableId) -> BddParams { - // First, compute the parameter set that sends value of variable to true in this state - let update_function = &self.network.update_functions[variable.0]; - let edge_params = if let Some(update_function) = update_function { - update_function.symbolic_eval_true(state, &self.encoder) - } else { - let var = self.encoder.get_implicit(state, variable); - BddParams::from(self.encoder.bdd_variables.mk_var(var)) - }; - - // Now if we actually want to go to false, invert the set: - if state.get_bit(variable.0) { - BddParams::from(edge_params.into_bdd().not()) - } else { - edge_params - } - } - - fn make_witness(&self, params: &Self::ParamSet) -> BooleanNetwork { - self.network.make_witness(params, &self.encoder) - } -} diff --git a/src/async_graph/_impl_evolution_operators.rs b/src/async_graph/_impl_evolution_operators.rs deleted file mode 100644 index dae268d..0000000 --- a/src/async_graph/_impl_evolution_operators.rs +++ /dev/null @@ -1,188 +0,0 @@ -use crate::async_graph::{AsyncGraphEdgeParams, Bwd, BwdIterator, Fwd, FwdIterator}; -use crate::biodivine_std::structs::IdState; -use crate::biodivine_std::traits::{EvolutionOperator, InvertibleEvolutionOperator}; - -impl<'a, Params: AsyncGraphEdgeParams> EvolutionOperator for Fwd<'a, Params> { - type State = IdState; - type Params = Params::ParamSet; - type Iterator = FwdIterator<'a, Params>; - - fn step(&self, current: IdState) -> Self::Iterator { - return FwdIterator { - graph: self.graph, - variables: self.graph.network().graph.variables(), - state: current, - }; - } -} - -impl<'a, Params: AsyncGraphEdgeParams> InvertibleEvolutionOperator for Fwd<'a, Params> { - type InvertedOperator = Bwd<'a, Params>; - - fn invert(&self) -> Self::InvertedOperator { - Bwd { graph: self.graph } - } -} - -impl Iterator for FwdIterator<'_, Params> { - type Item = (IdState, Params::ParamSet); - - fn next(&mut self) -> Option { - if let Some(var) = self.variables.next() { - let target = self.state.flip_bit(var.0); - let edge_params = self.graph.edges.edge_params(self.state, var); - Some((target, edge_params)) - } else { - None - } - } -} - -impl<'a, Params: AsyncGraphEdgeParams> EvolutionOperator for Bwd<'a, Params> { - type State = IdState; - type Params = Params::ParamSet; - type Iterator = BwdIterator<'a, Params>; - - fn step(&self, current: IdState) -> Self::Iterator { - BwdIterator { - graph: self.graph, - variables: self.graph.network().graph.variables(), - state: current, - } - } -} - -impl<'a, Params: AsyncGraphEdgeParams> InvertibleEvolutionOperator for Bwd<'a, Params> { - type InvertedOperator = Fwd<'a, Params>; - - fn invert(&self) -> Self::InvertedOperator { - Fwd { graph: self.graph } - } -} - -impl Iterator for BwdIterator<'_, Params> { - type Item = (IdState, Params::ParamSet); - - fn next(&mut self) -> Option { - if let Some(var) = self.variables.next() { - let source = self.state.flip_bit(var.0); - let edge_params = self.graph.edges.edge_params(source, var); - Some((source, edge_params)) - } else { - None - } - } -} - -#[cfg(test)] -mod tests { - use crate::async_graph::AsyncGraph; - use crate::bdd_params::BddParams; - use crate::biodivine_std::structs::IdState; - use crate::biodivine_std::traits::{EvolutionOperator, Graph, Set}; - use crate::BooleanNetwork; - use std::collections::HashSet; - use std::convert::TryFrom; - - #[test] - fn test_no_param_network() { - let network = BooleanNetwork::try_from( - " - a -> b - a -> a - b -| a - b -| b - $a: a & !b - $b: a | !b - ", - ) - .unwrap(); - let graph = &AsyncGraph::new(network).unwrap(); - - let edges: HashSet<(IdState, IdState)> = vec![ - (IdState::from(0b00), IdState::from(0b10)), - (IdState::from(0b10), IdState::from(0b00)), - (IdState::from(0b00), IdState::from(0b10)), - (IdState::from(0b01), IdState::from(0b11)), - (IdState::from(0b11), IdState::from(0b10)), - ] - .into_iter() - .collect(); - - let fwd = graph.fwd(); - let bwd = graph.bwd(); - - for s in graph.states() { - for (t, p) in fwd.step(s) { - assert_eq!( - !p.is_empty(), - edges.contains(&(s, t)), - "Edge ({:?},{:?})", - s, - t - ); - } - for (t, p) in bwd.step(s) { - assert_eq!( - !p.is_empty(), - edges.contains(&(t, s)), - "Edge ({:?},{:?})", - t, - s - ); - } - } - } - - #[test] - fn test_anonymous_param_network() { - let network = BooleanNetwork::try_from( - " - a ->? b - a -> a - b -|? a - b -| b - ", - ) - .unwrap(); - let graph = &AsyncGraph::new(network).unwrap(); - let fwd = graph.fwd(); - let bwd = graph.bwd(); - - let edges: HashSet<(IdState, IdState, i32)> = vec![ - (IdState::from(0b00), IdState::from(0b10), 2 * 3), - (IdState::from(0b10), IdState::from(0b00), 3 * 3), - (IdState::from(0b00), IdState::from(0b01), 1 * 3), - (IdState::from(0b11), IdState::from(0b10), 1 * 3), - (IdState::from(0b01), IdState::from(0b11), 3 * 3), - (IdState::from(0b11), IdState::from(0b01), 2 * 3), - ] - .into_iter() - .collect(); - - assert_eq!(9.0, graph.unit_params().cardinality()); - - let mut fwd_edges: HashSet<(IdState, IdState, BddParams)> = HashSet::new(); - let mut bwd_edges: HashSet<(IdState, IdState, BddParams)> = HashSet::new(); - - for s in graph.states() { - let successors = fwd.step(s); - for (t, p) in successors { - let p = p.intersect(graph.unit_params()); - if p.cardinality() > 0.0 { - assert!(edges.contains(&(s, t, p.cardinality() as i32))); - } - fwd_edges.insert((s, t, p)); - } - for (t, p) in bwd.step(s) { - let p = p.intersect(graph.unit_params()); - if p.cardinality() > 0.0 { - assert!(edges.contains(&(t, s, p.cardinality() as i32))); - } - bwd_edges.insert((t, s, p)); - } - } - - assert_eq!(fwd_edges, bwd_edges) - } -} diff --git a/src/async_graph/mod.rs b/src/async_graph/mod.rs deleted file mode 100644 index 08c0aca..0000000 --- a/src/async_graph/mod.rs +++ /dev/null @@ -1,125 +0,0 @@ -//! *Legacy* semi-symbolic representation of the coloured asynchronous state-transition graph. -//! -//! It represents states explicitly (see `IdState`), but uses symbolic representation (`BddParams`) -//! for sets of parameters. -//! -//! **`AsyncGraph` in its current form and the related structures are deprecated in favour of -//! `SymbolicAsyncGraph`. We may re-implement it later under a new name and a new API, because -//! in some niche use cases it seems to be faster and/or easier to use than a fully symbolic -//! approach. However, try not to rely on this implementation too much.** -//! -#![allow(deprecated)] - -use crate::bdd_params::{BddParameterEncoder, BddParams}; -use crate::biodivine_std::structs::{IdState, IdStateRange}; -use crate::biodivine_std::traits::{Graph, InvertibleGraph, Set}; -use crate::{BooleanNetwork, VariableId, VariableIdIterator}; - -mod _impl_async_graph; -mod _impl_default_edge_params; -mod _impl_evolution_operators; - -/// An asynchronous transition system of a `BooleanNetwork`. The states of the graph -/// are standard `IdState`s. The parameter sets are given by the associated `AsyncGraphEdgeParams`. -/// -/// Async graph implements the standard "asynchronous update", i.e. every variable can be -/// non-deterministically updated at any time, but the actual parameters for which this -/// happens are determined by the `AsyncGraphEdgeParams`. -/// -/// This actually hides a lot of complexity, because implementing `AsyncGraphEdgeParams` is typically -/// much easier than re-implementing the whole async graph structure. -/// -/// **`AsyncGraph` in its current form and the related structures are deprecated in favour of -/// `SymbolicAsyncGraph`. We may re-implement it later under a new name and a new API, because -/// in some niche use cases it seems to be faster than fully symbolic approach. However, -/// try not to rely on this implementation too much.** -#[deprecated] -pub struct AsyncGraph { - edges: P, -} - -/// Default implementation for edge parameters which adheres to the monotonicity and observability -/// constraints of the network, but poses no other restrictions. -pub struct DefaultEdgeParams { - network: BooleanNetwork, - encoder: BddParameterEncoder, - /// The parameter valuations which satisfy the static regulation constraints. - unit_set: BddParams, - empty_set: BddParams, -} - -/// Async graph edges implement the edge colouring (parametrisation) of a graph. Instances of -/// this trait are used together with the `AsyncGraph` to produce a semantic coloured graph -/// of a parametrised Boolean network. -/// -/// See `DefaultEdgeParams` for default implementation of edge colours. -/// -/// This trait is especially useful when constructing things like wrappers of existing graphs, -/// which need to modify the behaviour of the graph. Another option are various custom -/// parameter encoders, where we simply do not want to re-implement the whole graph trait -/// front scratch. -pub trait AsyncGraphEdgeParams { - type ParamSet: Set; - // A reference to the underlying Boolean network. - fn network(&self) -> &BooleanNetwork; - /// Create a new empty set of parameters. - fn empty_params(&self) -> &Self::ParamSet; - /// Create a new full set of parameters. - fn unit_params(&self) -> &Self::ParamSet; - /// Create parameters for the edge starting in the given `state`, - /// flipping the given `variable`. - fn edge_params(&self, state: IdState, variable: VariableId) -> Self::ParamSet; - /// Construct a witness network for the given set of parameters. - /// - /// TODO: It is not really essential in this trait. Think of a way to move it elsewhere. - fn make_witness(&self, params: &Self::ParamSet) -> BooleanNetwork; -} - -/// A forward `EvolutionOperator` of the `AsyncGraph`. -pub struct Fwd<'a, Edges: AsyncGraphEdgeParams> { - graph: &'a AsyncGraph, -} - -/// A backward `EvolutionOperator` of the `AsyncGraph`. -pub struct Bwd<'a, Edges: AsyncGraphEdgeParams> { - graph: &'a AsyncGraph, -} - -/// An iterator over successors of a state in the `AsyncGraph`. -pub struct FwdIterator<'a, Edges: AsyncGraphEdgeParams> { - graph: &'a AsyncGraph, - state: IdState, - variables: VariableIdIterator, -} - -/// An iterator over predecessors of a state in the `AsyncGraph`. -pub struct BwdIterator<'a, Edges: AsyncGraphEdgeParams> { - graph: &'a AsyncGraph, - state: IdState, - variables: VariableIdIterator, -} - -impl<'a, Edges: AsyncGraphEdgeParams> Graph for &'a AsyncGraph { - type State = IdState; - type Params = Edges::ParamSet; - type States = IdStateRange; - type FwdEdges = Fwd<'a, Edges>; - type BwdEdges = Bwd<'a, Edges>; - - fn states(&self) -> Self::States { - IdStateRange::new(self.num_states()) - } - - fn fwd(&self) -> Self::FwdEdges { - Fwd { graph: self } - } - - fn bwd(&self) -> Self::BwdEdges { - Bwd { graph: self } - } -} - -impl<'a, Edges: AsyncGraphEdgeParams> InvertibleGraph for &'a AsyncGraph { - type FwdEdges = Fwd<'a, Edges>; - type BwdEdges = Bwd<'a, Edges>; -} diff --git a/src/bdd_params/_impl_bdd_parameter_encoder.rs b/src/bdd_params/_impl_bdd_parameter_encoder.rs deleted file mode 100644 index e8e2de8..0000000 --- a/src/bdd_params/_impl_bdd_parameter_encoder.rs +++ /dev/null @@ -1,374 +0,0 @@ -use super::BddParameterEncoder; -use crate::bdd_params::{BddParams, FunctionTableEntry}; -use crate::biodivine_std::structs::IdState; -use crate::{BooleanNetwork, ParameterId, VariableId}; -use biodivine_lib_bdd::{BddVariable, BddVariableSetBuilder, ValuationsOfClauseIterator}; - -const MAX_VARIABLES: usize = 8 * std::mem::size_of::(); - -impl BddParameterEncoder { - /// Create a new `BddParameterEncoder` based on information given in a `BooleanNetwork`. - pub fn new(bn: &BooleanNetwork) -> BddParameterEncoder { - if bn.graph.num_vars() > MAX_VARIABLES { - panic!( - "Only up to {} variables supported by this parameter encoder.", - MAX_VARIABLES - ); - } - let bdd = BddVariableSetBuilder::new(); - Self::new_with_custom_variables(bn, bdd) - } - - /// Create a new `BddParameterEncoder` based on information given in a `BooleanNetwork` - /// and with variables already provided via `BddVariableSetBuilder`. - pub fn new_with_custom_variables( - bn: &BooleanNetwork, - mut bdd: BddVariableSetBuilder, - ) -> BddParameterEncoder { - BddParameterEncoder { - regulators: Self::build_regulators_table(bn), - explicit_function_tables: Self::build_explicit_function_table(bn, &mut bdd), - implicit_function_tables: Self::build_implicit_function_table(bn, &mut bdd), - bdd_variables: bdd.build(), - } - } - - /* - These utility functions should probably have some separate module, like static constraint computation, - but right now this is good enough... - */ - - pub(crate) fn build_explicit_function_table( - network: &BooleanNetwork, - bdd: &mut BddVariableSetBuilder, - ) -> Vec> { - let mut table = Vec::new(); - for pid in network.parameters() { - let p = network.get_parameter(pid); - // Here, we abuse BddValuationIterator to go over all possible valuations - // of function inputs. - - let p_vars = ValuationsOfClauseIterator::new_unconstrained(p.arity as u16) - .map(|valuation| { - let bdd_name = format!("{}{}", p.name, valuation); - bdd.make_variable(&bdd_name) - }) - .collect(); - - table.push(p_vars); - } - table - } - - pub(crate) fn build_implicit_function_table( - network: &BooleanNetwork, - bdd: &mut BddVariableSetBuilder, - ) -> Vec> { - let mut table = Vec::new(); - for vid in network.graph.variables() { - let v = network.graph.get_variable(vid); - - if network.get_update_function(vid).is_some() { - table.push(Vec::new()); - } else { - let args = network.graph.regulators(vid); - let cardinality = args.len(); - - // Note that if args are empty, one variable is still created because there is - // an "empty" valuation. - let p_vars = ValuationsOfClauseIterator::new_unconstrained(cardinality as u16) - .map(|valuation| { - let bdd_name = format!("\\{{{}}}{}", v.name, valuation); - bdd.make_variable(&bdd_name) - }) - .collect(); - - table.push(p_vars); - } - } - table - } - - pub(crate) fn build_regulators_table(network: &BooleanNetwork) -> Vec> { - let mut table = Vec::new(); - for vid in network.graph.variables() { - if network.get_update_function(vid).is_some() { - table.push(Vec::new()); - } else { - let args = network.graph.regulators(vid); - table.push(args); - } - } - table - } - - /// A vector of entries in the table of a specific function. - pub fn implicit_function_table(&self, target: VariableId) -> Vec { - let regulators = &self.regulators[target.0]; - let table = &self.implicit_function_tables[target.0]; - (0..table.len()) - .map(|i| FunctionTableEntry { - table: target.0, - entry_index: i, - regulators, - }) - .collect() - } - - /// Get teh parameters which correspond to a specific table entry being one. - pub fn get_implicit_for_table(&self, entry: &FunctionTableEntry) -> BddParams { - let var = self.implicit_function_tables[entry.table][entry.entry_index]; - BddParams(self.bdd_variables.mk_var(var)) - } - - pub fn get_implicit_var_for_table(&self, entry: &FunctionTableEntry) -> BddVariable { - self.implicit_function_tables[entry.table][entry.entry_index] - } - - /// Find the `BddVariable` corresponding to the value of the `parameter` function - /// in the given `state` assuming the specified `arguments`. - pub fn get_explicit( - &self, - state: IdState, - parameter: ParameterId, - arguments: &[VariableId], - ) -> BddVariable { - let table_index = Self::compute_table_index(state, arguments); - self.explicit_function_tables[parameter.0][table_index] - } - - /// Make a `BddParams` set which corresponds to the valuations for which the value of - /// `parameter` function given `arguments` is `true` in the given `state`. - pub fn explicit_true_when( - &self, - state: IdState, - parameter: ParameterId, - arguments: &[VariableId], - ) -> BddParams { - let var = self.get_explicit(state, parameter, arguments); - BddParams(self.bdd_variables.mk_var(var)) - } - - /// Find the `BddVariable` corresponding to the value of the implicit update function - /// of the given `variable` in the given `state`. - pub fn get_implicit(&self, state: IdState, variable: VariableId) -> BddVariable { - let regulators = &self.regulators[variable.0]; - let table = &self.implicit_function_tables[variable.0]; - if regulators.is_empty() && table.is_empty() { - panic!( - "Variable {:?} does not have an implicit update function.", - variable - ); - } - if regulators.is_empty() { - // if regulators are empty but table is not, this is a zero-regulator variable - return table[0]; - } - let table_index = Self::compute_table_index(state, regulators); - self.implicit_function_tables[variable.0][table_index] - } - - /// Make a `BddParams` set which corresponds to the valuations for which the value of - /// an implicit update function of `variable` is true in the given `state`. - pub fn implicit_true_when(&self, state: IdState, variable: VariableId) -> BddParams { - let var = self.get_implicit(state, variable); - BddParams(self.bdd_variables.mk_var(var)) - } - - // Compute which function table entry does the arguments correspond to in the given `state`. - fn compute_table_index(state: IdState, args: &[VariableId]) -> usize { - let mut table_index: usize = 0; - for i in 0..args.len() { - if state.get_bit(args[args.len() - 1 - i].0) { - table_index += 1; - } - if i < args.len() - 1 { - table_index <<= 1; - } - } - table_index - } -} - -#[cfg(test)] -mod tests { - use crate::bdd_params::BddParameterEncoder; - use crate::biodivine_std::structs::IdState; - use crate::BooleanNetwork; - use crate::VariableId; - use std::convert::TryFrom; - - #[test] - fn explicit_parameter_encoder_test() { - let network = BooleanNetwork::try_from( - " - a -> b - a -| a - b -> a - $a: p(a,b) => q(b) - $b: q(a) - ", - ) - .unwrap(); - let encoder = BddParameterEncoder::new(&network); - - let variables = encoder.bdd_variables.variables(); - assert_eq!(6, variables.len()); - - let p = network.find_parameter("p").unwrap(); - let q = network.find_parameter("q").unwrap(); - - // The order of parameters is not fixed, so we can't explicitly test exact BddVariables. - // We can however test that all should appear. - - let mut actual_vars = Vec::new(); - actual_vars.push(encoder.get_explicit( - IdState::from(0b00), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit( - IdState::from(0b01), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit( - IdState::from(0b10), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit( - IdState::from(0b11), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit(IdState::from(0b00), q, &vec![VariableId(0)])); - actual_vars.push(encoder.get_explicit(IdState::from(0b01), q, &vec![VariableId(0)])); - actual_vars.sort(); - - assert_eq!(variables, actual_vars); - - // Also, some basic identities should hold: - - let a = encoder.get_explicit(IdState::from(0b00), p, &vec![VariableId(1), VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b00), p, &vec![VariableId(0), VariableId(1)]); - assert_eq!(a, b); - - let a = encoder.get_explicit(IdState::from(0b10), p, &vec![VariableId(1), VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b01), p, &vec![VariableId(0), VariableId(1)]); - assert_eq!(a, b); - - let a = encoder.get_explicit(IdState::from(0b01), p, &vec![VariableId(1), VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b10), p, &vec![VariableId(0), VariableId(1)]); - assert_eq!(a, b); - - let a = encoder.get_explicit(IdState::from(0b11), p, &vec![VariableId(1), VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b11), p, &vec![VariableId(0), VariableId(1)]); - assert_eq!(a, b); - - let a = encoder.get_explicit(IdState::from(0b01), p, &vec![VariableId(1), VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b01), p, &vec![VariableId(0), VariableId(1)]); - assert_ne!(a, b); - - let a = encoder.get_explicit(IdState::from(0b00), q, &vec![VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b10), q, &vec![VariableId(0)]); - assert_eq!(a, b); - - let a = encoder.get_explicit(IdState::from(0b10), q, &vec![VariableId(1)]); - let b = encoder.get_explicit(IdState::from(0b11), q, &vec![VariableId(1)]); - assert_eq!(a, b); - - let a = encoder.get_explicit(IdState::from(0b00), q, &vec![VariableId(0)]); - let b = encoder.get_explicit(IdState::from(0b01), q, &vec![VariableId(0)]); - assert_ne!(a, b); - } - - #[test] - fn anonymous_parameter_encoder_test() { - let network = BooleanNetwork::try_from( - " - a -> b - a -| a - b -> a - ", - ) - .unwrap(); - let encoder = BddParameterEncoder::new(&network); - - let variables = encoder.bdd_variables.variables(); - assert_eq!(6, variables.len()); - - let a = network.graph.find_variable("a").unwrap(); - let b = network.graph.find_variable("b").unwrap(); - - let mut actual_vars = Vec::new(); - actual_vars.push(encoder.get_implicit(IdState::from(0b00), a)); - actual_vars.push(encoder.get_implicit(IdState::from(0b01), a)); - actual_vars.push(encoder.get_implicit(IdState::from(0b10), a)); - actual_vars.push(encoder.get_implicit(IdState::from(0b11), a)); - actual_vars.push(encoder.get_implicit(IdState::from(0b00), b)); - actual_vars.push(encoder.get_implicit(IdState::from(0b01), b)); - actual_vars.sort(); - - assert_eq!(variables, actual_vars); - - let v1 = encoder.get_implicit(IdState::from(0b10), b); - let v2 = encoder.get_implicit(IdState::from(0b00), b); - assert_eq!(v1, v2); - - let v1 = encoder.get_implicit(IdState::from(0b11), b); - let v2 = encoder.get_implicit(IdState::from(0b01), b); - assert_eq!(v1, v2); - - let v1 = encoder.get_implicit(IdState::from(0b01), b); - let v2 = encoder.get_implicit(IdState::from(0b00), b); - assert_ne!(v1, v2); - } - - #[test] - fn mixed_parameter_encoder_test() { - let network = BooleanNetwork::try_from( - " - a -> b - a -| a - b -> a - $a: b & p(a, b) - ", - ) - .unwrap(); - let encoder = BddParameterEncoder::new(&network); - - let variables = encoder.bdd_variables.variables(); - assert_eq!(6, variables.len()); - - let p = network.find_parameter("p").unwrap(); - let b = network.graph.find_variable("b").unwrap(); - - let mut actual_vars = Vec::new(); - actual_vars.push(encoder.get_explicit( - IdState::from(0b00), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit( - IdState::from(0b01), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit( - IdState::from(0b10), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_explicit( - IdState::from(0b11), - p, - &vec![VariableId(0), VariableId(1)], - )); - actual_vars.push(encoder.get_implicit(IdState::from(0b01), b)); - actual_vars.push(encoder.get_implicit(IdState::from(0b00), b)); - actual_vars.sort(); - - assert_eq!(variables, actual_vars); - } -} diff --git a/src/bdd_params/_impl_bdd_params.rs b/src/bdd_params/_impl_bdd_params.rs deleted file mode 100644 index 3d7ed62..0000000 --- a/src/bdd_params/_impl_bdd_params.rs +++ /dev/null @@ -1,47 +0,0 @@ -use super::BddParams; -use crate::biodivine_std::traits::Set; -use biodivine_lib_bdd::Bdd; - -impl BddParams { - /// Consume these `BddParams` and turn them into a raw `Bdd`. - pub fn into_bdd(self) -> Bdd { - self.0 - } - - pub fn as_bdd(&self) -> &Bdd { - &self.0 - } - - pub fn cardinality(&self) -> f64 { - self.0.cardinality() - } -} - -impl Set for BddParams { - fn union(&self, other: &Self) -> Self { - BddParams(self.0.or(&other.0)) - } - - fn intersect(&self, other: &Self) -> Self { - BddParams(self.0.and(&other.0)) - } - - fn minus(&self, other: &Self) -> Self { - BddParams(self.0.and_not(&other.0)) - } - - fn is_empty(&self) -> bool { - self.0.is_false() - } - - fn is_subset(&self, other: &Self) -> bool { - // TODO: Introduce special function for this in bdd-lib to avoid allocation - self.minus(other).is_empty() - } -} - -impl From for BddParams { - fn from(val: Bdd) -> Self { - BddParams(val) - } -} diff --git a/src/bdd_params/_impl_fn_update.rs b/src/bdd_params/_impl_fn_update.rs deleted file mode 100644 index 799734a..0000000 --- a/src/bdd_params/_impl_fn_update.rs +++ /dev/null @@ -1,51 +0,0 @@ -use crate::bdd_params::{BddParameterEncoder, BddParams}; -use crate::biodivine_std::structs::IdState; -use crate::{BinaryOp, FnUpdate}; -use biodivine_lib_bdd::Bdd; - -impl FnUpdate { - /// **(internal)** Evaluate this `FnUpdate` into symbolic `BddParams` that represent all parameter - /// valuations for which this function evaluates to `true`. - pub(crate) fn symbolic_eval_true( - &self, - state: IdState, - encoder: &BddParameterEncoder, - ) -> BddParams { - BddParams(self._symbolic_eval(state, encoder)) - } - - pub(super) fn _symbolic_eval(&self, state: IdState, encoder: &BddParameterEncoder) -> Bdd { - match self { - FnUpdate::Const(value) => { - if *value { - encoder.bdd_variables.mk_true() - } else { - encoder.bdd_variables.mk_false() - } - } - FnUpdate::Not(inner) => inner._symbolic_eval(state, encoder).not(), - FnUpdate::Var(id) => { - if state.get_bit(id.0) { - encoder.bdd_variables.mk_true() - } else { - encoder.bdd_variables.mk_false() - } - } - FnUpdate::Param(id, args) => { - let var = encoder.get_explicit(state, *id, args); - encoder.bdd_variables.mk_var(var) - } - FnUpdate::Binary(op, l, r) => { - let l = l._symbolic_eval(state, encoder); - let r = r._symbolic_eval(state, encoder); - match op { - BinaryOp::And => l.and(&r), - BinaryOp::Or => l.or(&r), - BinaryOp::Xor => l.xor(&r), - BinaryOp::Imp => l.imp(&r), - BinaryOp::Iff => l.iff(&r), - } - } - } - } -} diff --git a/src/bdd_params/_impl_function_table_entry.rs b/src/bdd_params/_impl_function_table_entry.rs deleted file mode 100644 index a7fe028..0000000 --- a/src/bdd_params/_impl_function_table_entry.rs +++ /dev/null @@ -1,32 +0,0 @@ -use crate::bdd_params::FunctionTableEntry; -use crate::VariableId; - -impl FunctionTableEntry<'_> { - /// Obtain the value of the input variable. Panics if the variable is not an - /// input of this function. - pub fn get_value(&self, variable: VariableId) -> bool { - for i in 0..self.regulators.len() { - if variable == self.regulators[i] { - // first argument is least significant bit, last argument most significant - let mask = 1 << i; - return (self.entry_index & mask) != 0; - } - } - panic!("Variable {:?} is not an input.", variable); - } - - /// Obtain a table entry with the value of `variable` flipped. - pub fn flip_value(&self, variable: VariableId) -> FunctionTableEntry { - for i in 0..self.regulators.len() { - if variable == self.regulators[i] { - let mask = 1 << i; - return FunctionTableEntry { - entry_index: self.entry_index ^ mask, - regulators: self.regulators, - table: self.table, - }; - } - } - panic!("Variable {:?} is not an input.", variable); - } -} diff --git a/src/bdd_params/_impl_static_constraints.rs b/src/bdd_params/_impl_static_constraints.rs deleted file mode 100644 index cc1d931..0000000 --- a/src/bdd_params/_impl_static_constraints.rs +++ /dev/null @@ -1,222 +0,0 @@ -//! **(internal)** This module implements functions for creating `Bdd`s corresponding -//! to the static constraints of the individual regulations of a `BooleanNetwork`. - -use crate::bdd_params::BddParameterEncoder; -use crate::biodivine_std::structs::IdState; -use crate::{BooleanNetwork, FnUpdate, Monotonicity, Regulation, VariableId}; -use biodivine_lib_bdd::{bdd, Bdd}; -use std::ops::Range; - -/// Build a `Bdd` which describes all valuations satisfying the static constraints -/// of the given `BooleanNetwork`. -pub fn build_static_constraints(bn: &BooleanNetwork, encoder: &BddParameterEncoder) -> Bdd { - let mut condition = encoder.bdd_variables.mk_true(); - let ctx = Ctx::new(bn, encoder); - for r in &bn.graph.regulations { - if let Some(fun) = bn.get_update_function(r.target) { - if r.monotonicity.is_some() { - let monotonicity = build_monotonicity_explicit(&ctx, r, fun); - condition = bdd!(condition & monotonicity); - if condition.is_false() { - println!( - "Regulation {} -> {} is not monotonous.", - bn.graph.get_variable(r.regulator).name, - bn.graph.get_variable(r.target).name - ); - break; - } - } - if r.observable { - let observability = build_observability_explicit(&ctx, r, fun); - condition = bdd!(condition & observability); - if condition.is_false() { - println!( - "Regulation {} -> {} is not observable.", - bn.graph.get_variable(r.regulator).name, - bn.graph.get_variable(r.target).name - ); - break; - } - } - } else { - if r.monotonicity.is_some() { - let monotonicity = build_monotonicity_implicit(&ctx, r); - condition = bdd!(condition & monotonicity); - if condition.is_false() { - println!( - "Regulation {} -> {} is not monotonous.", - bn.graph.get_variable(r.regulator).name, - bn.graph.get_variable(r.target).name - ); - break; - } - } - if r.observable { - let observability = build_observability_implicit(&ctx, r); - condition = bdd!(condition & observability); - if condition.is_false() { - println!( - "Regulation {} -> {} is not observable.", - bn.graph.get_variable(r.regulator).name, - bn.graph.get_variable(r.target).name - ); - break; - } - } - } - } - condition -} - -struct Ctx<'a> { - bn: &'a BooleanNetwork, - encoder: &'a BddParameterEncoder, -} - -impl<'a> Ctx<'a> { - pub fn new(bn: &'a BooleanNetwork, encoder: &'a BddParameterEncoder) -> Ctx<'a> { - Ctx { bn, encoder } - } - - /// Transform a table pair into pair of `Bdd`s assuming an update function is known. - pub fn pair_explicit(&self, states: (IdState, IdState), fun: &'a FnUpdate) -> (Bdd, Bdd) { - let (inactive, active) = states; - let inactive = fun._symbolic_eval(inactive, self.encoder); - let active = fun._symbolic_eval(active, self.encoder); - (inactive, active) - } - - /// Transform a table pair into a pair of `Bdd`s assuming an implicit update function. - pub fn pair_implicit(&self, states: (IdState, IdState), variable: VariableId) -> (Bdd, Bdd) { - let (inactive, active) = states; - let inactive = self.encoder.get_implicit(inactive, variable); - let active = self.encoder.get_implicit(active, variable); - let inactive = self.encoder.bdd_variables.mk_var(inactive); - let active = self.encoder.bdd_variables.mk_var(active); - (inactive, active) - } -} - -fn build_monotonicity_implicit<'a>(ctx: &Ctx<'a>, regulation: &'a Regulation) -> Bdd { - let mut condition = ctx.encoder.bdd_variables.mk_true(); - for states in InputStatesPairIterator::new(ctx.bn, regulation) { - let (inactive, active) = ctx.pair_implicit(states, regulation.target); - let monotonous = - build_monotonicity_pair(&inactive, &active, regulation.monotonicity.unwrap()); - condition = bdd!(condition & monotonous); - } - condition -} - -fn build_observability_implicit<'a>(ctx: &Ctx<'a>, regulation: &'a Regulation) -> Bdd { - let mut condition = ctx.encoder.bdd_variables.mk_false(); - for states in InputStatesPairIterator::new(ctx.bn, regulation) { - let (inactive, active) = ctx.pair_implicit(states, regulation.target); - condition = bdd!(condition | (!(inactive <=> active))); - } - condition -} - -fn build_monotonicity_explicit<'a>( - ctx: &Ctx<'a>, - regulation: &'a Regulation, - update_function: &'a FnUpdate, -) -> Bdd { - let mut condition = ctx.encoder.bdd_variables.mk_true(); - for states in InputStatesPairIterator::new(ctx.bn, regulation) { - let (inactive, active) = ctx.pair_explicit(states, update_function); - let monotonous = - build_monotonicity_pair(&inactive, &active, regulation.monotonicity.unwrap()); - condition = bdd!(condition & monotonous); - } - condition -} - -fn build_observability_explicit<'a>( - ctx: &Ctx<'a>, - regulation: &'a Regulation, - update_function: &'a FnUpdate, -) -> Bdd { - let mut condition = ctx.encoder.bdd_variables.mk_false(); - for states in InputStatesPairIterator::new(ctx.bn, regulation) { - let (inactive, active) = ctx.pair_explicit(states, update_function); - condition = bdd!(condition | (!(inactive <=> active))); - } - condition -} - -/// **(internal)** Iterates over pairs of states where the first state has a particular regulator -/// variable set to zero while the second state has it set to one. -/// -/// The pairs cover all possible inputs into an associated update function such that -/// the alternated variable is one of the inputs of the function. -struct InputStatesPairIterator { - range: Range, - mask: usize, - regulators: Vec, - variable: VariableId, -} - -impl Iterator for InputStatesPairIterator { - type Item = (IdState, IdState); - - fn next(&mut self) -> Option { - for next_index in &mut self.range { - if next_index & self.mask != 0 { - continue; - } else { - // this is an inactive index - let state = extend_table_index_to_state(next_index, &self.regulators); - return Some((state, state.flip_bit(self.variable.0))); - } - } - None - } -} - -impl InputStatesPairIterator { - pub fn new(bn: &BooleanNetwork, regulation: &Regulation) -> InputStatesPairIterator { - let regulators = bn.graph.regulators(regulation.target); - let regulator_index = regulators - .iter() - .position(|v| *v == regulation.regulator) - .unwrap(); - let table_size = 1 << regulators.len(); - let mask = 1 << regulator_index; // select the regulator bit of the table index - InputStatesPairIterator { - regulators, - variable: regulation.regulator, - mask, - range: (0..table_size), - } - } -} - -/// **(internal)** Build a state which has the variables set exactly as in the `table_index` and -/// all other variables set to zero. -/// -/// index: 0110, args: (0, 3, 5, 6) -> 0101000 -/// index: abcd, args: (0, 3, 5, 6) -> dc0b00a -fn extend_table_index_to_state(table_index: usize, args: &[VariableId]) -> IdState { - let mut state: usize = 0; - for (i, regulator) in args.iter().enumerate() { - if (table_index >> i) & 1 == 1 { - // If we have one in the table index - // then we also put one in the state, - // but on the correct position. - state |= 1 << regulator.0; - } - } - IdState::from(state) -} - -/// **(internal)** Builds a `Bdd` of parameters corresponding to valuations where the given -/// pair of function entries behaves monotonously. -fn build_monotonicity_pair(inactive: &Bdd, active: &Bdd, monotonicity: Monotonicity) -> Bdd { - match monotonicity { - // increasing: [f(0) = 1] => [f(1) = 1] - Monotonicity::Activation => bdd!(inactive => active), - // decreasing: [f(0) = 0] => [f(1) = 0] which is equivalent to [f(0) = 1] => [f(1) = 1] - Monotonicity::Inhibition => bdd!(active => inactive), - } -} diff --git a/src/bdd_params/_impl_witness_generator.rs b/src/bdd_params/_impl_witness_generator.rs deleted file mode 100644 index 42bc57e..0000000 --- a/src/bdd_params/_impl_witness_generator.rs +++ /dev/null @@ -1,295 +0,0 @@ -#![allow(deprecated)] -use crate::bdd_params::{BddParameterEncoder, BddParams}; -use crate::{BinaryOp, BooleanNetwork, FnUpdate, VariableId}; -use biodivine_lib_bdd::boolean_expression::BooleanExpression; -use biodivine_lib_bdd::{Bdd, BddValuation, BddVariableSet, ValuationsOfClauseIterator}; - -impl BooleanNetwork { - /// *Legacy* function for creating a fully instantiated `BooleanNetwork` using parameters. - /// - /// In later revisions, this should be part of `BddParameterEncoder`. - pub fn make_witness( - &self, - params: &BddParams, - encoder: &BddParameterEncoder, - ) -> BooleanNetwork { - let valuation = params.as_bdd().sat_witness(); - if valuation.is_none() { - panic!("Cannot create witness for empty parameter set."); - } - self.make_witness_for_valuation(valuation.unwrap(), encoder) - } - - /// *Legacy* function for creating a fully instantiated `BooleanNetwork` using parameters. - /// - /// In later revisions, this should be part of `BddParameterEncoder`. - pub fn make_witness_for_valuation( - &self, - valuation: BddValuation, - encoder: &BddParameterEncoder, - ) -> BooleanNetwork { - // First, make functions for explicit parameters: - let mut explicit_parameter_expressions = Vec::with_capacity(self.parameters.len()); - for i_p in 0..self.parameters.len() { - let parameter = &self.parameters[i_p]; - let parameter_input_table = &encoder.explicit_function_tables[i_p]; - let num_inputs = parameter.arity as u16; - if num_inputs == 0 { - assert_eq!(parameter_input_table.len(), 1); - explicit_parameter_expressions.push(BooleanExpression::Const( - valuation.value(parameter_input_table[0]), - )); - } else { - let parameter_function_input_vars = BddVariableSet::new_anonymous(num_inputs); - - let variables_and_valuations = parameter_input_table - .iter() - .zip(ValuationsOfClauseIterator::new_unconstrained(num_inputs)); - - // initially, the function is just false - let mut function_bdd = parameter_function_input_vars.mk_false(); - for (bdd_variable, input_valuation) in variables_and_valuations { - if valuation.value(*bdd_variable) { - // and for each `1` in the function table, we add the input valuation - let input_valuation_bdd = Bdd::from(input_valuation.clone()); - function_bdd = function_bdd.or(&input_valuation_bdd); - } - } - - let parameter_expression = - function_bdd.to_boolean_expression(¶meter_function_input_vars); - explicit_parameter_expressions.push(parameter_expression); - } - } - - let mut result = self.clone(); - for i_var in 0..self.graph.num_vars() { - if let Some(function) = &self.update_functions[i_var] { - // Replace parameters in the explicit function with actual functions - let resolved_function = - *Self::replace_parameters(function, &explicit_parameter_expressions); - result.update_functions[i_var] = Some(resolved_function); - } else { - // Build an anonymous update function - let regulators = &encoder.regulators[i_var]; - let num_inputs = regulators.len() as u16; - let function_input_table = &encoder.implicit_function_tables[i_var]; - let function_input_vars = BddVariableSet::new_anonymous(num_inputs); - - let variables_and_valuations = function_input_table - .iter() - .zip(ValuationsOfClauseIterator::new_unconstrained(num_inputs)); - let mut function_bdd = function_input_vars.mk_false(); - for (bdd_variable, input_valuation) in variables_and_valuations { - if valuation.value(*bdd_variable) { - let input_valuation_bdd = Bdd::from(input_valuation); - function_bdd = function_bdd.or(&input_valuation_bdd); - } - } - - let function_expression = function_bdd.to_boolean_expression(&function_input_vars); - result.update_functions[i_var] = Some(*Self::expression_to_fn_update( - &function_expression, - regulators, - )); - } - } - - result.parameters.clear(); - result.parameter_to_index.clear(); - - result - } - - fn replace_parameters( - update_function: &FnUpdate, - parameter_expressions: &[BooleanExpression], - ) -> Box { - Box::new(match update_function { - FnUpdate::Const(value) => FnUpdate::Const(*value), - FnUpdate::Var(id) => FnUpdate::Var(*id), - FnUpdate::Not(a) => FnUpdate::Not(Self::replace_parameters(a, parameter_expressions)), - FnUpdate::Binary(op, a, b) => FnUpdate::Binary( - *op, - Self::replace_parameters(a, parameter_expressions), - Self::replace_parameters(b, parameter_expressions), - ), - FnUpdate::Param(id, args) => { - let parameter_expression = ¶meter_expressions[id.0]; - *Self::expression_to_fn_update(parameter_expression, args) - } - }) - } - - fn expression_to_fn_update( - expression: &BooleanExpression, - args: &[VariableId], - ) -> Box { - Box::new(match expression { - BooleanExpression::Const(value) => FnUpdate::Const(*value), - BooleanExpression::Iff(a, b) => FnUpdate::Binary( - BinaryOp::Iff, - Self::expression_to_fn_update(a, args), - Self::expression_to_fn_update(b, args), - ), - BooleanExpression::Imp(a, b) => FnUpdate::Binary( - BinaryOp::Imp, - Self::expression_to_fn_update(a, args), - Self::expression_to_fn_update(b, args), - ), - BooleanExpression::Or(a, b) => FnUpdate::Binary( - BinaryOp::Or, - Self::expression_to_fn_update(a, args), - Self::expression_to_fn_update(b, args), - ), - BooleanExpression::And(a, b) => FnUpdate::Binary( - BinaryOp::And, - Self::expression_to_fn_update(a, args), - Self::expression_to_fn_update(b, args), - ), - BooleanExpression::Xor(a, b) => FnUpdate::Binary( - BinaryOp::Xor, - Self::expression_to_fn_update(a, args), - Self::expression_to_fn_update(b, args), - ), - BooleanExpression::Not(a) => FnUpdate::Not(Self::expression_to_fn_update(a, args)), - BooleanExpression::Variable(name) => { - // name is x_i, so we can strip x_ away and parse it - let name = &name[2..]; - let arg_index: usize = name.parse().unwrap(); - FnUpdate::Var(args[arg_index]) - } - }) - } -} - -#[cfg(test)] -mod tests { - use crate::async_graph::AsyncGraph; - use crate::BooleanNetwork; - use std::convert::TryFrom; - - #[test] - pub fn make_witness_0() { - let network = BooleanNetwork::try_from( - " - a -> b - a -?? a - b -|? c - a ->? c - c -? a - c -| d - $a: a & (p(c) => (c | c)) - $b: p(a) <=> q(a, a) - $c: q(b, b) => !(b ^ k) - ", - ) - .unwrap(); - let graph = AsyncGraph::new(network).unwrap(); - let witness = graph.make_witness(graph.unit_params()); - let witness_string = BooleanNetwork::try_from( - " - a -> b - a -?? a - b -|? c - a ->? c - c -? a - c -| d - # validity of the functions has been manually verified - $a: (a & (true => (c | c))) - $b: (true <=> (a & a)) - $c: ((b & b) => !(b ^ false)) - $d: !c - ", - ) - .unwrap(); - assert_eq!(witness, witness_string); - // turn the witness into a graph again - there should be exactly one parametrisation: - let graph = AsyncGraph::new(witness).unwrap(); - assert_eq!(graph.unit_params().cardinality(), 1.0); - } - - #[test] - pub fn make_witness_1() { - let network = BooleanNetwork::try_from( - " - SSF -> SWI5 - - SSF -> ACE2 - - SBF -> SSF - HCM1 -> SSF - - MBF -> YHP1 - SBF -> YHP1 - - MBF -> HCM1 - SBF -> HCM1 - - MBF -> YOX1 - SBF -> YOX1 - - CLN3 -> SBF - MBF -> SBF - YHP1 -| SBF - YOX1 -| SBF - - CLN3 -> MBF - - ACE2 -> CLN3 - YHP1 -| CLN3 - SWI5 -> CLN3 - YOX1 -| CLN3 - ", - ) - .unwrap(); - let graph = AsyncGraph::new(network).unwrap(); - let witness = graph.make_witness(graph.unit_params()); - let witness_string = BooleanNetwork::try_from( - " - SSF -> SWI5 - - SSF -> ACE2 - - SBF -> SSF - HCM1 -> SSF - - MBF -> YHP1 - SBF -> YHP1 - - MBF -> HCM1 - SBF -> HCM1 - - MBF -> YOX1 - SBF -> YOX1 - - CLN3 -> SBF - MBF -> SBF - YHP1 -| SBF - YOX1 -| SBF - - CLN3 -> MBF - - ACE2 -> CLN3 - YHP1 -| CLN3 - SWI5 -> CLN3 - YOX1 -| CLN3 - $ACE2: SSF - $CLN3: ACE2 | SWI5 | !YHP1 | !YOX1 - $HCM1: MBF | SBF - $MBF: CLN3 - $SBF: CLN3 | MBF | !YHP1 | !YOX1 - $SSF: HCM1 | SBF - $SWI5: SSF - $YHP1: MBF | SBF - $YOX1: MBF | SBF - ", - ) - .unwrap(); - - assert_eq!(witness, witness_string); - - let graph = AsyncGraph::new(witness).unwrap(); - assert_eq!(graph.unit_params().cardinality(), 1.0); - } -} diff --git a/src/bdd_params/mod.rs b/src/bdd_params/mod.rs deleted file mode 100644 index 49159b1..0000000 --- a/src/bdd_params/mod.rs +++ /dev/null @@ -1,54 +0,0 @@ -//! *Legacy* symbolic representation of parameter space of a `BooleanNetwork` using `Bdds`. -//! -//! Specifically, there is the `BddParams` struct which represents the set of valuations -//! and the `BddParameterEncoder` struct which allows creating new `Bdd` and `BddParams` that -//! correspond to situations where individual parameters have a specific value. - -use crate::VariableId; -use biodivine_lib_bdd::{Bdd, BddVariable, BddVariableSet}; - -mod _impl_bdd_parameter_encoder; -mod _impl_bdd_params; -mod _impl_fn_update; -mod _impl_function_table_entry; -mod _impl_static_constraints; -mod _impl_witness_generator; - -pub use _impl_static_constraints::build_static_constraints; - -/// A wrapper for the `Bdd` object that implements a basic `Set` trait. -#[derive(Clone, Debug, Hash, PartialEq, Eq)] -pub struct BddParams(Bdd); - -/// Handles the translation between parameters of the `BooleanNetwork` and `BddVariables`. -/// -/// There are two types of parameters in the `BooleanNetwork` - explicit and implicit. -/// -/// Explicit are the named parameters that are specifically declared in the update functions. -/// Implicit are the anonymous parameters representing the missing update functions. -/// -/// Every explicit and implicit `Parameter` maps to a set of `BddVariables` that represent -/// the values in its function table. The responsibility of this struct is to create all -/// `BddVariables` and maintain how they map to individual parameters. -#[derive(Clone)] -pub struct BddParameterEncoder { - /// The actual `BddVariableSet` used to represent the parameters - use this for `.dot` printing etc. - pub bdd_variables: BddVariableSet, - /// The actual regulators of each variable - these are used when evaluating implicit parameters. - regulators: Vec>, - /// A vector of function tables indexed by explicit `ParameterId`s of the `BooleanNetwork`. - explicit_function_tables: Vec>, - /// A vector of implicit function tables indexed by `VariableId`s of the `BooleanNetwork`. - /// If the variable has an explicit update function, the table is empty. - implicit_function_tables: Vec>, -} - -/// **(experimental)** Represents one "line" in a Boolean function table. -/// -/// You can query the state of input variables on this line or make a new line -/// with updated variable values. -pub struct FunctionTableEntry<'a> { - entry_index: usize, // index into the specific table - table: usize, // index into the vector of tables - regulators: &'a Vec, -} diff --git a/src/bin/bench_fixed_points_naive.rs b/src/bin/bench_fixed_points_naive.rs index 25d7d85..1d5ff39 100644 --- a/src/bin/bench_fixed_points_naive.rs +++ b/src/bin/bench_fixed_points_naive.rs @@ -6,7 +6,7 @@ fn main() { let args = Vec::from_iter(std::env::args()); let path = &args[1]; let model = BooleanNetwork::try_from_file(path).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bench_fixed_points_solver.rs b/src/bin/bench_fixed_points_solver.rs index 841a225..1b3e538 100644 --- a/src/bin/bench_fixed_points_solver.rs +++ b/src/bin/bench_fixed_points_solver.rs @@ -8,7 +8,7 @@ fn main() { let args = Vec::from_iter(std::env::args()); let path = &args[1]; let model = BooleanNetwork::try_from_file(path).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bench_fixed_points_symbolic.rs b/src/bin/bench_fixed_points_symbolic.rs index 9efd53e..9796f84 100644 --- a/src/bin/bench_fixed_points_symbolic.rs +++ b/src/bin/bench_fixed_points_symbolic.rs @@ -6,7 +6,7 @@ fn main() { let args = Vec::from_iter(std::env::args()); let path = &args[1]; let model = BooleanNetwork::try_from_file(path).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bench_fixed_points_symbolic_colors.rs b/src/bin/bench_fixed_points_symbolic_colors.rs index c5aa428..253e5bf 100644 --- a/src/bin/bench_fixed_points_symbolic_colors.rs +++ b/src/bin/bench_fixed_points_symbolic_colors.rs @@ -6,7 +6,7 @@ fn main() { let args = Vec::from_iter(std::env::args()); let path = &args[1]; let model = BooleanNetwork::try_from_file(path).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bench_fixed_points_symbolic_iterator.rs b/src/bin/bench_fixed_points_symbolic_iterator.rs index e139a50..635f57d 100644 --- a/src/bin/bench_fixed_points_symbolic_iterator.rs +++ b/src/bin/bench_fixed_points_symbolic_iterator.rs @@ -7,7 +7,7 @@ fn main() { let args = Vec::from_iter(std::env::args()); let path = &args[1]; let model = BooleanNetwork::try_from_file(path).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bench_fixed_points_symbolic_vertices.rs b/src/bin/bench_fixed_points_symbolic_vertices.rs index a996dde..fe19fc3 100644 --- a/src/bin/bench_fixed_points_symbolic_vertices.rs +++ b/src/bin/bench_fixed_points_symbolic_vertices.rs @@ -6,7 +6,7 @@ fn main() { let args = Vec::from_iter(std::env::args()); let path = &args[1]; let model = BooleanNetwork::try_from_file(path).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bench_reach.rs b/src/bin/bench_reach.rs index f4a3b07..5d652e1 100644 --- a/src/bin/bench_reach.rs +++ b/src/bin/bench_reach.rs @@ -7,7 +7,7 @@ use biodivine_lib_param_bn::BooleanNetwork; fn main() { let args = std::env::args().collect::>(); let model = BooleanNetwork::try_from_file(args[1].as_str()).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters.", diff --git a/src/bin/bnet_parametrizer.rs b/src/bin/bnet_parametrizer.rs index d63034f..db411e7 100644 --- a/src/bin/bnet_parametrizer.rs +++ b/src/bin/bnet_parametrizer.rs @@ -46,8 +46,16 @@ fn flatten_fn_update(network: &mut BooleanNetwork, update: &FnUpdate) -> FnUpdat FnUpdate::Var(id) => FnUpdate::Var(*id), FnUpdate::Not(update) => flatten_fn_update(network, update).negation(), FnUpdate::Param(id, args) => { + let mut var_args = Vec::new(); + for arg in args { + if let FnUpdate::Var(id) = arg { + var_args.push(*id); + } else { + panic!("Cannot process models with nested function calls."); + } + } let name = network.get_parameter(*id).get_name().clone(); - explode_function(network, args, format!("{}_", name)) + explode_function(network, &var_args, format!("{}_", name)) } FnUpdate::Binary(op, left, right) => FnUpdate::Binary( *op, diff --git a/src/bin/check_fixed_points.rs b/src/bin/check_fixed_points.rs index e10af6a..01c9272 100644 --- a/src/bin/check_fixed_points.rs +++ b/src/bin/check_fixed_points.rs @@ -20,7 +20,7 @@ fn main() { let args = std::env::args().collect::>(); let model = BooleanNetwork::try_from_file(args[1].as_str()).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters/inputs.", model.num_vars(), diff --git a/src/bin/check_fixed_points_solver.rs b/src/bin/check_fixed_points_solver.rs index 1a02ad4..587c765 100644 --- a/src/bin/check_fixed_points_solver.rs +++ b/src/bin/check_fixed_points_solver.rs @@ -16,7 +16,7 @@ fn main() { let args = std::env::args().collect::>(); let model = BooleanNetwork::try_from_file(args[1].as_str()).unwrap(); - let model = model.inline_inputs(); + let model = model.inline_inputs(true, true); println!( "Loaded model with {} variables and {} parameters/inputs.", model.num_vars(), diff --git a/src/bin/dump_graph.rs b/src/bin/dump_graph.rs index 7924865..8c31815 100644 --- a/src/bin/dump_graph.rs +++ b/src/bin/dump_graph.rs @@ -1,16 +1,10 @@ #![allow(deprecated)] -use biodivine_lib_bdd::{BddValuation, ValuationsOfClauseIterator}; -use biodivine_lib_param_bn::async_graph::AsyncGraph; -use biodivine_lib_param_bn::bdd_params::BddParameterEncoder; -use biodivine_lib_param_bn::biodivine_std::traits::{EvolutionOperator, Graph}; -use biodivine_lib_param_bn::BooleanNetwork; -use std::convert::TryFrom; -use std::io::Read; - /// Dump aeon model from stdin as explicit coloured graph to stdout. /// Provides extra debug info on stderr... fn main() { + panic!("Dump graph feature is disabled. If you need it, please get in touch."); + /* let mut buffer = String::new(); std::io::stdin().read_to_string(&mut buffer).unwrap(); @@ -51,5 +45,5 @@ fn main() { println!(); } } - } + }*/ } diff --git a/src/lib.rs b/src/lib.rs index 3d66676..c2886e9 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -18,8 +18,6 @@ use std::collections::HashMap; use std::iter::Map; use std::ops::Range; -pub mod async_graph; -pub mod bdd_params; pub mod biodivine_std; pub mod fixed_points; pub mod sbml; @@ -212,7 +210,7 @@ pub enum FnUpdate { /// References a network parameter (uninterpreted function). /// /// The variable list are the arguments of the function invocation. - Param(ParameterId, Vec), + Param(ParameterId, Vec), /// Negation. Not(Box), /// Binary boolean operation. diff --git a/src/sbml/export.rs b/src/sbml/export.rs index 3f29078..6dfff7d 100644 --- a/src/sbml/export.rs +++ b/src/sbml/export.rs @@ -128,7 +128,7 @@ impl BooleanNetwork { FnUpdate::Param(id, args) => { write!(out, "{}", self[*id].get_name())?; for arg in args { - write!(out, "{}", self[*arg].get_name())?; + self.write_update_function(out, arg)?; } write!(out, "")?; } diff --git a/src/sbml/import/_convert_mathml_to_fn_update.rs b/src/sbml/import/_convert_mathml_to_fn_update.rs index 15277c5..f4219bf 100644 --- a/src/sbml/import/_convert_mathml_to_fn_update.rs +++ b/src/sbml/import/_convert_mathml_to_fn_update.rs @@ -49,20 +49,16 @@ pub fn sbml_transition_to_update_function( } } MathMl::SymbolApply(p_name, args) => { - let mut variables = Vec::new(); + let mut fn_args = Vec::new(); for arg in args { let update = math_to_update(arg, network, transition, id_to_var)?; - if let FnUpdate::Var(v) = update { - variables.push(v); - } else { - return Err(format!("(Transition `{:?}`) Uninterpreted functions can have only variables as arguments.", transition.id)); - } + fn_args.push(update); } // This should already be created by parent function. let param = network.find_parameter(p_name).unwrap(); - Ok(FnUpdate::Param(param, variables)) + Ok(FnUpdate::Param(param, fn_args)) } MathMl::Apply(op, args) => { match op.as_str() { diff --git a/src/solver_context/_impl_bn_solver_context.rs b/src/solver_context/_impl_bn_solver_context.rs index e28f242..acfff60 100644 --- a/src/solver_context/_impl_bn_solver_context.rs +++ b/src/solver_context/_impl_bn_solver_context.rs @@ -286,10 +286,11 @@ impl<'z3> BnSolverContext<'z3> { let args: Vec = args .iter() .map(|it| { - variable_constructors[it.to_index()] - .apply(&[]) - .as_bool() - .unwrap() + self.translate_update_function( + it, + variable_constructors, + parameter_constructors, + ) }) .collect::>(); let arg_refs: Vec<&dyn Ast<'z3>> = args.iter().map(|it| it as &dyn Ast).collect(); diff --git a/src/symbolic_async_graph/_impl_regulation_constraint.rs b/src/symbolic_async_graph/_impl_regulation_constraint.rs index dcd5bf4..d855cd0 100644 --- a/src/symbolic_async_graph/_impl_regulation_constraint.rs +++ b/src/symbolic_async_graph/_impl_regulation_constraint.rs @@ -134,6 +134,64 @@ impl RegulationConstraint { monotonicity, }) } + + /// Similar to [Self::infer_sufficient_regulation], but it tries to keep the constraints + /// from the given `old_regulation` assuming they are satisfiable and more restrictive + /// than the inferred constraints. + pub fn fix_regulation( + ctx: &SymbolicContext, + old_regulation: &Regulation, + fn_is_true: &Bdd, + ) -> Option { + let obs = Self::mk_observability(ctx, fn_is_true, old_regulation.regulator); + let observable = if obs.is_true() { + // The regulation is used by every possible instantiation, it is always observable. + true + } else if !obs.is_false() { + // The regulation is used by *some* instantiations. It is observable if the old + // regulation is observable. + old_regulation.observable + } else { + // The regulation is *never* used, hence the regulation is irrelevant. + return None; + }; + + let act = Self::mk_activation(ctx, fn_is_true, old_regulation.regulator); + let inh = Self::mk_inhibition(ctx, fn_is_true, old_regulation.regulator); + + let monotonicity = if act.is_true() { + // The function is *always* an activation. + Some(Monotonicity::Activation) + } else if inh.is_true() { + // The function is *always* an inhibition. + Some(Monotonicity::Inhibition) + } else { + // The function can have instantiations with different monotonicity, or possibly + // even dual monotonicity. + if old_regulation.monotonicity == Some(Monotonicity::Activation) && !act.is_false() { + // Old regulation is an activation and there are *some* activating instantiations. + // We can propagate the old constraint. + Some(Monotonicity::Activation) + } else if old_regulation.monotonicity == Some(Monotonicity::Inhibition) + && !inh.is_false() + { + // Old regulation is an inhibition and there are *some* inhibiting instantiations. + // We can propagate the old constraint. + Some(Monotonicity::Inhibition) + } else { + // Either the old activation is also non-monotonic, or the function contradicts + // the old monotonicity requirement. + None + } + }; + + Some(Regulation { + regulator: old_regulation.regulator, + target: old_regulation.target, + observable, + monotonicity, + }) + } } /// Compute a `Bdd` which is a subset of the `initial` valuations that satisfies all diff --git a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs index 9a4beb8..dd8f880 100644 --- a/src/symbolic_async_graph/_impl_symbolic_async_graph.rs +++ b/src/symbolic_async_graph/_impl_symbolic_async_graph.rs @@ -486,6 +486,11 @@ impl SymbolicAsyncGraph { }) .collect::>(); + let sub_to_main_map = sub_network + .variables() + .zip(sub_to_main.clone()) + .collect::>(); + { // 2.1 Verify that the sub-network has the same parameters as the main network. for param in sub_network.parameters() { @@ -510,6 +515,11 @@ impl SymbolicAsyncGraph { }) .collect::>(); + let param_sub_to_main_map = sub_network + .parameters() + .zip(param_sub_to_main.clone()) + .collect::>(); + { // 3.1 Verify that every regulation from main is in sub. for main_reg in main_network.as_graph().regulations() { @@ -559,7 +569,8 @@ impl SymbolicAsyncGraph { let name = main_network.get_variable_name(main_var); if let Some(sub_fun) = sub_network.get_update_function(sub_var) { if let Some(main_fun) = main_network.get_update_function(main_var) { - let sub_fun_in_main = sub_fun.substitute(&sub_to_main, ¶m_sub_to_main); + let sub_fun_in_main = + sub_fun.rename_all(&sub_to_main_map, ¶m_sub_to_main_map); if &sub_fun_in_main != main_fun { return Err(format!("Functions of `{}` are different.", name)); } @@ -607,7 +618,7 @@ impl SymbolicAsyncGraph { .get_implicit_function_table(main_var); let function_args = main_network.regulators(main_var); let specialised_function = - specialised_function.substitute(&sub_to_main, ¶m_sub_to_main); + specialised_function.rename_all(&sub_to_main_map, ¶m_sub_to_main_map); let mut valuation = main_network .variables() @@ -1223,7 +1234,7 @@ mod tests { let g1_b = bn.as_graph().find_variable("b").unwrap(); let g1_c = bn.as_graph().find_variable("c").unwrap(); - let bn_reduced = bn.inline_variable(g1_b).unwrap(); + let bn_reduced = bn.inline_variable(g1_b, false).unwrap(); let g2_a = bn_reduced.as_graph().find_variable("a").unwrap(); let g2_c = bn_reduced.as_graph().find_variable("c").unwrap(); diff --git a/src/symbolic_async_graph/_impl_symbolic_context.rs b/src/symbolic_async_graph/_impl_symbolic_context.rs index bc7fa8d..892402e 100644 --- a/src/symbolic_async_graph/_impl_symbolic_context.rs +++ b/src/symbolic_async_graph/_impl_symbolic_context.rs @@ -244,7 +244,7 @@ impl SymbolicContext { pub fn mk_uninterpreted_function_is_true( &self, parameter: ParameterId, - args: &[VariableId], + args: &[FnUpdate], ) -> Bdd { let table = &self.explicit_function_tables[parameter.0]; self.mk_function_table_true(table, &self.prepare_args(args)) @@ -262,7 +262,8 @@ impl SymbolicContext { variable ); }); - self.mk_function_table_true(table, &self.prepare_args(args)) + let args = args.iter().map(|it| FnUpdate::Var(*it)).collect::>(); + self.mk_function_table_true(table, &self.prepare_args(&args)) } /// Create a `Bdd` that is true when given `FnUpdate` evaluates to true. @@ -346,7 +347,8 @@ impl SymbolicContext { variable ); }); - self.instantiate_function_table(valuation, table, &self.prepare_args(args)) + let args = args.iter().map(|it| FnUpdate::Var(*it)).collect::>(); + self.instantiate_function_table(valuation, table, &self.prepare_args(&args)) } /// Create a `Bdd` which represents the instantiated explicit uninterpreted function. @@ -354,7 +356,7 @@ impl SymbolicContext { &self, valuation: &BddValuation, parameter: ParameterId, - args: &[VariableId], + args: &[FnUpdate], ) -> Bdd { let table = &self.explicit_function_tables[parameter.0]; self.instantiate_function_table(valuation, table, &self.prepare_args(args)) @@ -383,12 +385,9 @@ impl SymbolicContext { } } - /// **(internal)** Utility method for converting `VariableId` arguments to `Bdd` arguments. - fn prepare_args(&self, args: &[VariableId]) -> Vec { - return args - .iter() - .map(|v| self.mk_state_variable_is_true(*v)) - .collect(); + /// **(internal)** Utility method for converting `FnUpdate` arguments to `Bdd` arguments. + fn prepare_args(&self, args: &[FnUpdate]) -> Vec { + return args.iter().map(|v| self.mk_fn_update_true(v)).collect(); } /// This is similar to [BddVariableSet::transfer_from], but applied at the level of