From 03559a956ad3660feee69c5ea174273d7a5ac834 Mon Sep 17 00:00:00 2001 From: Samuel Pastva Date: Wed, 20 Dec 2023 10:41:17 +0100 Subject: [PATCH] Resolve breaking changes while updating dependencies. --- Cargo.toml | 8 +- src/bindings/aeon.rs | 18 +-- src/bindings/bn_classifier/mod.rs | 2 +- .../_impl_hctl_tree_node.rs | 7 +- src/bindings/hctl_model_checker/mod.rs | 11 +- .../lib_param_bn/_impl_boolean_network.rs | 15 +- .../lib_param_bn/_impl_fixed_points.rs | 29 ++-- src/bindings/lib_param_bn/_impl_fn_update.rs | 130 +++++------------- .../_impl_graph_colored_vertices.rs | 6 +- .../lib_param_bn/_impl_graph_vertices.rs | 25 +--- .../_impl_symbolic_async_graph.rs | 60 +++++--- .../lib_param_bn/_impl_symbolic_context.rs | 14 +- src/bindings/lib_param_bn/mod.rs | 6 +- .../pbn_control/_impl_perturbation_graph.rs | 4 +- src/internal/classification/classify.rs | 13 +- src/internal/classification/load_inputs.rs | 2 +- src/internal/scc/_impl_classifier.rs | 8 +- .../mod.rs | 4 +- 18 files changed, 162 insertions(+), 200 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index a902005d..0a1e9770 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -17,10 +17,10 @@ static-z3 = ["z3/static-link-z3"] [dependencies] pyo3 = { version = "0.20.0", features = ["abi3-py37", "extension-module"] } -biodivine-lib-param-bn = { version="0.4.7", features=["solver-z3"] } -biodivine-lib-bdd = "0.5.2" -biodivine-pbn-control = "0.2.1" -biodivine-hctl-model-checker = "0.2.0" +biodivine-lib-param-bn = { version="0.5.2", features=["solver-z3"] } +biodivine-lib-bdd = "0.5.7" +biodivine-pbn-control = "0.3.1" +biodivine-hctl-model-checker = "0.2.2" rand = "0.8.5" macros = { path = "macros" } zip = "0.6.6" diff --git a/src/bindings/aeon.rs b/src/bindings/aeon.rs index 6db8b53c..6724acd9 100644 --- a/src/bindings/aeon.rs +++ b/src/bindings/aeon.rs @@ -41,11 +41,7 @@ pub fn xie_beerel_attractors( graph: &PySymbolicAsyncGraph, states: Option<&PyGraphColoredVertices>, ) -> Vec { - let variables = graph - .as_native() - .as_network() - .variables() - .collect::>(); + let variables = Vec::from_iter(graph.as_native().variables()); let states = states .map(|it| it.as_native()) .unwrap_or_else(|| graph.as_native().unit_colored_vertices()); @@ -66,11 +62,7 @@ pub fn reach_fwd( states: &PyGraphColoredVertices, universe: Option<&PyGraphColoredVertices>, ) -> PyGraphColoredVertices { - let variables = graph - .as_native() - .as_network() - .variables() - .collect::>(); + let variables = Vec::from_iter(graph.as_native().variables()); let universe = universe .map(|it| it.as_native()) .unwrap_or_else(|| graph.as_native().unit_colored_vertices()); @@ -93,11 +85,7 @@ pub fn reach_bwd( states: &PyGraphColoredVertices, universe: Option<&PyGraphColoredVertices>, ) -> PyGraphColoredVertices { - let variables = graph - .as_native() - .as_network() - .variables() - .collect::>(); + let variables = Vec::from_iter(graph.as_native().variables()); let universe = universe .map(|it| it.as_native()) .unwrap_or_else(|| graph.as_native().unit_colored_vertices()); diff --git a/src/bindings/bn_classifier/mod.rs b/src/bindings/bn_classifier/mod.rs index e2522dda..5a994ef2 100644 --- a/src/bindings/bn_classifier/mod.rs +++ b/src/bindings/bn_classifier/mod.rs @@ -59,7 +59,7 @@ pub fn run_attractor_classification(model_path: String, output_zip: String) -> P Ok(model) => model, Err(error) => return throw_runtime_error(error), }; - let graph = match SymbolicAsyncGraph::new(model.clone()) { + let graph = match SymbolicAsyncGraph::new(&model) { Ok(graph) => graph, Err(error) => return throw_runtime_error(error), }; diff --git a/src/bindings/hctl_model_checker/_impl_hctl_tree_node.rs b/src/bindings/hctl_model_checker/_impl_hctl_tree_node.rs index ca029dc0..bc79a9e8 100644 --- a/src/bindings/hctl_model_checker/_impl_hctl_tree_node.rs +++ b/src/bindings/hctl_model_checker/_impl_hctl_tree_node.rs @@ -8,6 +8,7 @@ use biodivine_hctl_model_checker::preprocessing::node::NodeType; use biodivine_hctl_model_checker::preprocessing::parser::{ parse_and_minimize_extended_formula, parse_and_minimize_hctl_formula, parse_hctl_formula, }; +use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; use pyo3::basic::CompareOp; use pyo3::prelude::*; @@ -40,7 +41,8 @@ impl PyHctlTreeNode { /// Tree is slightly modified after the parsing (variable renaming, etc.) due to optimizations. /// Validity of the formula is checked during parsing, including proposition names. pub fn new(formula: String, bn: &PyBooleanNetwork) -> PyResult { - match parse_and_minimize_hctl_formula(bn.as_native(), formula.as_str()) { + let ctx = SymbolicContext::new(bn.as_native()).unwrap(); + match parse_and_minimize_hctl_formula(&ctx, formula.as_str()) { Ok(tree) => Ok(PyHctlTreeNode(tree)), Err(error) => throw_runtime_error(error), } @@ -90,7 +92,8 @@ impl PyHctlTreeNode { /// parsing, including proposition names. /// Extended formulae can include `wild-card propositions` in form `%proposition%`. pub fn new_from_extended(formula: String, bn: &PyBooleanNetwork) -> PyResult { - match parse_and_minimize_extended_formula(bn.as_native(), formula.as_str()) { + let ctx = SymbolicContext::new(bn.as_native()).unwrap(); + match parse_and_minimize_extended_formula(&ctx, formula.as_str()) { Ok(tree) => Ok(PyHctlTreeNode(tree)), Err(error) => throw_runtime_error(error), } diff --git a/src/bindings/hctl_model_checker/mod.rs b/src/bindings/hctl_model_checker/mod.rs index 406eeb36..99c14243 100644 --- a/src/bindings/hctl_model_checker/mod.rs +++ b/src/bindings/hctl_model_checker/mod.rs @@ -11,7 +11,8 @@ use biodivine_hctl_model_checker::model_checking::{ use biodivine_hctl_model_checker::preprocessing::node::HctlTreeNode; use biodivine_hctl_model_checker::preprocessing::parser::parse_and_minimize_hctl_formula; use biodivine_hctl_model_checker::result_print::PrintOptions; -use biodivine_lib_param_bn::BooleanNetwork; + +use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; use std::collections::HashMap; use crate::{throw_runtime_error, throw_type_error, AsNative}; @@ -58,11 +59,11 @@ impl PyHctlTreeNode { /// /// - `PyHctlTreeNode` itself; /// - A string that will be parsed as a HCTL formula. - pub(crate) fn from_python(any: &PyAny, network: &BooleanNetwork) -> PyResult { + pub(crate) fn from_python(any: &PyAny, ctx: &SymbolicContext) -> PyResult { if let Ok(val) = any.extract::() { Ok(val) } else if let Ok(string) = any.extract::() { - let parsed = parse_and_minimize_hctl_formula(network, string.as_str()); + let parsed = parse_and_minimize_hctl_formula(ctx, string.as_str()); match parsed { Err(e) => throw_runtime_error(e), Ok(tree) => Ok(PyHctlTreeNode::from(tree)), @@ -89,7 +90,7 @@ pub fn model_check( sanitize: bool, ) -> PyResult { let stg = stg.as_native(); - let formula = PyHctlTreeNode::from_python(formula, stg.as_network())?; + let formula = PyHctlTreeNode::from_python(formula, stg.symbolic_context())?; let result = if sanitize { model_check_tree(formula.into(), stg) @@ -120,7 +121,7 @@ pub fn model_check_multiple( let stg = stg.as_native(); let mut list: Vec = Vec::new(); for formula in formulae { - list.push(PyHctlTreeNode::from_python(formula, stg.as_network())?.into()); + list.push(PyHctlTreeNode::from_python(formula, stg.symbolic_context())?.into()); } let result = if sanitize { diff --git a/src/bindings/lib_param_bn/_impl_boolean_network.rs b/src/bindings/lib_param_bn/_impl_boolean_network.rs index 942067e1..62477d9d 100644 --- a/src/bindings/lib_param_bn/_impl_boolean_network.rs +++ b/src/bindings/lib_param_bn/_impl_boolean_network.rs @@ -331,8 +331,15 @@ impl PyBooleanNetwork { } } - pub fn inline_inputs(&self, py: Python) -> PyResult> { - PyBooleanNetwork::from(self.as_native().inline_inputs()).export_to_python(py) + #[pyo3(signature = (infer_inputs = true, repair_graph = true))] + pub fn inline_inputs( + &self, + py: Python, + infer_inputs: bool, + repair_graph: bool, + ) -> PyResult> { + PyBooleanNetwork::from(self.as_native().inline_inputs(infer_inputs, repair_graph)) + .export_to_python(py) } /// Eliminate a network variable by inlining its update function into its downstream targets. @@ -343,10 +350,12 @@ impl PyBooleanNetwork { /// - The function cannot be safely inlined due to the presence of uninterpreted functions. /// /// Check the Rust documentation for more information about the method. + #[pyo3(signature = (var, repair_graph = true))] pub fn inline_variable( self_: PyRefMut<'_, Self>, py: Python, var: &PyAny, + repair_graph: bool, ) -> PyResult>> { let id = self_ .as_ref() @@ -355,7 +364,7 @@ impl PyBooleanNetwork { self_ .as_native() - .inline_variable(id.into()) + .inline_variable(id.into(), repair_graph) .map(|it| PyBooleanNetwork::from(it).export_to_python(py)) .transpose() } diff --git a/src/bindings/lib_param_bn/_impl_fixed_points.rs b/src/bindings/lib_param_bn/_impl_fixed_points.rs index 9f4a3de9..f610c66f 100644 --- a/src/bindings/lib_param_bn/_impl_fixed_points.rs +++ b/src/bindings/lib_param_bn/_impl_fixed_points.rs @@ -1,5 +1,6 @@ use crate::bindings::lib_param_bn::{ - PyFixedPoints, PyGraphColoredVertices, PyGraphColors, PyGraphVertices, PySymbolicAsyncGraph, + PyBooleanNetwork, PyFixedPoints, PyGraphColoredVertices, PyGraphColors, PyGraphVertices, + PySymbolicAsyncGraph, }; use crate::AsNative; use biodivine_lib_bdd::BddPartialValuation; @@ -127,8 +128,9 @@ impl PyFixedPoints { /// /// WARNING: Due to technical issues, right now this is only a list, not an iterator. #[staticmethod] - #[pyo3(signature = (stg, limit = None, positive_restriction = None, negative_restriction = None))] + #[pyo3(signature = (bn, stg, limit = None, positive_restriction = None, negative_restriction = None))] pub fn solver_list( + bn: &PyBooleanNetwork, stg: &PySymbolicAsyncGraph, limit: Option, positive_restriction: Option>, @@ -141,7 +143,7 @@ impl PyFixedPoints { positive_spaces.push(read_space(stg, space)?); } } else { - positive_spaces.push(Space::new(stg.as_native().as_network())); + positive_spaces.push(Space::new(bn.as_native())); } // A negative restriction is simply empty if not provided. let negative_restriction = negative_restriction.unwrap_or_default(); @@ -152,8 +154,7 @@ impl PyFixedPoints { let z3_config = z3::Config::new(); let z3 = z3::Context::new(&z3_config); - let network_copy = stg.as_native().as_network().clone(); - let context = BnSolverContext::new(&z3, network_copy); + let context = BnSolverContext::new(&z3, bn.as_native().clone()); let iterator = FixedPoints::solver_iterator(&context, &positive_spaces, &negative_spaces); let limit = limit.unwrap_or(usize::MAX); let results: Vec = iterator @@ -178,8 +179,9 @@ impl PyFixedPoints { /// /// WARNING: Due to technical issues, right now this is only a list, not an iterator. #[staticmethod] - #[pyo3(signature = (stg, limit = None, positive_restriction = None, negative_restriction = None))] + #[pyo3(signature = (bn, stg, limit = None, positive_restriction = None, negative_restriction = None))] pub fn solver_vertex_list( + bn: &PyBooleanNetwork, stg: &PySymbolicAsyncGraph, limit: Option, positive_restriction: Option>, @@ -192,7 +194,7 @@ impl PyFixedPoints { positive_spaces.push(read_space(stg, space)?); } } else { - positive_spaces.push(Space::new(stg.as_native().as_network())); + positive_spaces.push(Space::new(bn.as_native())); } // A negative restriction is simply empty if not provided. let negative_restriction = negative_restriction.unwrap_or_default(); @@ -203,8 +205,7 @@ impl PyFixedPoints { let z3_config = z3::Config::new(); let z3 = z3::Context::new(&z3_config); - let network_copy = stg.as_native().as_network().clone(); - let context = BnSolverContext::new(&z3, network_copy); + let context = BnSolverContext::new(&z3, bn.as_native().clone()); let iterator = FixedPoints::solver_vertex_iterator(&context, &positive_spaces, &negative_spaces); let limit = limit.unwrap_or(usize::MAX); @@ -242,8 +243,9 @@ impl PyFixedPoints { /// /// WARNING: Due to technical issues, right now this is only a list, not an iterator. #[staticmethod] - #[pyo3(signature = (stg, limit = None, positive_restriction = None, negative_restriction = None))] + #[pyo3(signature = (bn, stg, limit = None, positive_restriction = None, negative_restriction = None))] pub fn solver_color_list( + bn: &PyBooleanNetwork, stg: &PySymbolicAsyncGraph, limit: Option, positive_restriction: Option>, @@ -256,7 +258,7 @@ impl PyFixedPoints { positive_spaces.push(read_space(stg, space)?); } } else { - positive_spaces.push(Space::new(stg.as_native().as_network())); + positive_spaces.push(Space::new(bn.as_native())); } // A negative restriction is simply empty if not provided. let negative_restriction = negative_restriction.unwrap_or_default(); @@ -267,8 +269,7 @@ impl PyFixedPoints { let z3_config = z3::Config::new(); let z3 = z3::Context::new(&z3_config); - let network_copy = stg.as_native().as_network().clone(); - let context = BnSolverContext::new(&z3, network_copy); + let context = BnSolverContext::new(&z3, bn.as_native().clone()); let iterator = FixedPoints::solver_color_iterator(&context, &positive_spaces, &negative_spaces); let limit = limit.unwrap_or(usize::MAX); @@ -284,7 +285,7 @@ impl PyFixedPoints { } fn read_space(stg: &PySymbolicAsyncGraph, py_space: &PyDict) -> PyResult { - let mut space = Space::new(stg.as_native().as_network()); + let mut space = Space::new_raw(stg.as_native().num_vars()); for (k, v) in py_space { let key: VariableId = stg.resolve_variable(k)?.into(); let value: ExtendedBoolean = v.extract::()?.into(); diff --git a/src/bindings/lib_param_bn/_impl_fn_update.rs b/src/bindings/lib_param_bn/_impl_fn_update.rs index 2977f400..a1bc4470 100644 --- a/src/bindings/lib_param_bn/_impl_fn_update.rs +++ b/src/bindings/lib_param_bn/_impl_fn_update.rs @@ -1,6 +1,6 @@ use crate::bindings::lib_param_bn::{PyBooleanNetwork, PyFnUpdate, PyParameterId, PyVariableId}; use crate::{throw_runtime_error, AsNative}; -use biodivine_lib_param_bn::{BinaryOp, BooleanNetwork, FnUpdate, VariableId}; +use biodivine_lib_param_bn::{BinaryOp, FnUpdate}; use pyo3::basic::CompareOp; use pyo3::{pymethods, PyResult}; use std::collections::hash_map::DefaultHasher; @@ -37,56 +37,11 @@ impl PyFnUpdate { /// variable/parameter names are used. Otherwise, names are substituted for "v_id" (variables) /// and "p_id" (parameters). pub fn to_string(&self, network: Option<&PyBooleanNetwork>) -> String { - fn recursive(update: &FnUpdate, network: Option<&BooleanNetwork>) -> String { - match update { - FnUpdate::Const(value) => { - if *value { - "true".to_string() - } else { - "false".to_string() - } - } - FnUpdate::Var(id) => { - if let Some(network) = network { - network.get_variable_name(*id).clone() - } else { - format!("v_{}", id.to_index()) - } - } - FnUpdate::Param(id, args) => { - if let Some(network) = network { - let name = network.get_parameter(*id).get_name(); - if args.is_empty() { - name.clone() - } else { - let args = args - .iter() - .map(|x| network.get_variable_name(*x).clone()) - .collect::>(); - format!("{}({})", name, args.join(", ")) - } - } else if args.is_empty() { - format!("p_{}", id.to_index()) - } else { - let args = args.iter().map(|x| format!("{:?}", *x)).collect::>(); - format!("p_{}({})", id.to_index(), args.join(", ")) - } - } - FnUpdate::Not(inner) => { - format!("!{}", recursive(inner, network)) - } - FnUpdate::Binary(op, left, right) => { - format!( - "({} {} {})", - recursive(left, network), - op, - recursive(right, network) - ) - } - } + if let Some(network) = network { + self.as_native().to_string(network.as_native()) + } else { + format!("{}", self.as_native()) } - - recursive(self.as_native(), network.map(|it| it.as_native())) } /// Build a new expression which uses the variables and parameters from the given network. @@ -109,8 +64,8 @@ impl PyFnUpdate { } #[staticmethod] - pub fn from_parameter(id: PyParameterId, args: Option>) -> PyFnUpdate { - let mut args_native: Vec = Vec::new(); + pub fn from_parameter(id: PyParameterId, args: Option>) -> PyFnUpdate { + let mut args_native: Vec = Vec::new(); if let Some(args) = args { for a in args { args_native.push(a.into()); @@ -124,52 +79,42 @@ impl PyFnUpdate { match operator.as_str() { "not" => { assert_eq!(1, arguments.len()); - Ok(FnUpdate::Not(Box::new(arguments[0].as_native().clone())).into()) + let f = FnUpdate::mk_not(arguments[0].as_native().clone()); + Ok(f.into()) } "and" => { - assert_eq!(2, arguments.len()); - Ok(FnUpdate::Binary( - BinaryOp::And, - Box::new(arguments[0].as_native().clone()), - Box::new(arguments[1].as_native().clone()), - ) - .into()) + let args = arguments + .into_iter() + .map(|it| it.as_native().clone()) + .collect::>(); + let f = FnUpdate::mk_conjunction(&args); + Ok(f.into()) } "or" => { - assert_eq!(2, arguments.len()); - Ok(FnUpdate::Binary( - BinaryOp::Or, - Box::new(arguments[0].as_native().clone()), - Box::new(arguments[1].as_native().clone()), - ) - .into()) + let args = arguments + .into_iter() + .map(|it| it.as_native().clone()) + .collect::>(); + let f = FnUpdate::mk_disjunction(&args); + Ok(f.into()) } "xor" => { assert_eq!(2, arguments.len()); - Ok(FnUpdate::Binary( - BinaryOp::Xor, - Box::new(arguments[0].as_native().clone()), - Box::new(arguments[1].as_native().clone()), - ) - .into()) + let l = arguments[0].as_native().clone(); + let r = arguments[1].as_native().clone(); + Ok(l.xor(r).into()) } "iff" => { assert_eq!(2, arguments.len()); - Ok(FnUpdate::Binary( - BinaryOp::Iff, - Box::new(arguments[0].as_native().clone()), - Box::new(arguments[1].as_native().clone()), - ) - .into()) + let l = arguments[0].as_native().clone(); + let r = arguments[1].as_native().clone(); + Ok(l.iff(r).into()) } "imp" => { assert_eq!(2, arguments.len()); - Ok(FnUpdate::Binary( - BinaryOp::Imp, - Box::new(arguments[0].as_native().clone()), - Box::new(arguments[1].as_native().clone()), - ) - .into()) + let l = arguments[0].as_native().clone(); + let r = arguments[1].as_native().clone(); + Ok(l.implies(r).into()) } _ => throw_runtime_error(format!("Unknown operator: {operator}.")), } @@ -191,9 +136,12 @@ impl PyFnUpdate { } } - pub fn as_parameter(&self) -> Option<(PyParameterId, Vec)> { + pub fn as_parameter(&self) -> Option<(PyParameterId, Vec)> { if let FnUpdate::Param(id, args) = self.as_native() { - let args = args.iter().map(|it| (*it).into()).collect::>(); + let args = args + .iter() + .map(|it| (*it).clone().into()) + .collect::>(); Some(((*id).into(), args)) } else { None @@ -231,13 +179,9 @@ impl PyFnUpdate { /// is impossible. /// /// A substitution is impossible when `var` appears as argument of an uninterpreted function. - pub fn substitute_variable( - &self, - var: PyVariableId, - function: PyFnUpdate, - ) -> Option { + pub fn substitute_variable(&self, var: PyVariableId, function: PyFnUpdate) -> PyFnUpdate { self.as_native() .substitute_variable(var.into(), function.as_native()) - .map(|it| it.into()) + .into() } } diff --git a/src/bindings/lib_param_bn/_impl_graph_colored_vertices.rs b/src/bindings/lib_param_bn/_impl_graph_colored_vertices.rs index 324a9eae..a7282b6e 100644 --- a/src/bindings/lib_param_bn/_impl_graph_colored_vertices.rs +++ b/src/bindings/lib_param_bn/_impl_graph_colored_vertices.rs @@ -5,6 +5,7 @@ use crate::bindings::lib_param_bn::{ use crate::{throw_runtime_error, AsNative}; use biodivine_lib_bdd::Bdd; use biodivine_lib_param_bn::biodivine_std::traits::Set; +use biodivine_lib_param_bn::symbolic_async_graph::GraphColoredVertices; use pyo3::basic::CompareOp; use pyo3::prelude::*; @@ -30,7 +31,10 @@ impl PyGraphColoredVertices { ctx.bdd_variable_set().num_vars(), bdd.as_native().num_vars() ); - PyGraphColoredVertices(graph.as_native().empty_vertices().copy(bdd.into())) + PyGraphColoredVertices(GraphColoredVertices::new( + bdd.into(), + graph.as_native().symbolic_context(), + )) } pub fn to_bdd(&self) -> PyBdd { diff --git a/src/bindings/lib_param_bn/_impl_graph_vertices.rs b/src/bindings/lib_param_bn/_impl_graph_vertices.rs index 2ed220c6..446da26e 100644 --- a/src/bindings/lib_param_bn/_impl_graph_vertices.rs +++ b/src/bindings/lib_param_bn/_impl_graph_vertices.rs @@ -6,7 +6,7 @@ use crate::{throw_runtime_error, AsNative}; use biodivine_lib_bdd::{Bdd, BddVariable}; use biodivine_lib_param_bn::biodivine_std::bitvector::BitVector; use biodivine_lib_param_bn::biodivine_std::traits::Set; -use biodivine_lib_param_bn::symbolic_async_graph::{GraphVertexIterator, IterableVertices}; +use biodivine_lib_param_bn::symbolic_async_graph::GraphVertices; use pyo3::basic::CompareOp; use pyo3::prelude::*; use std::collections::HashSet; @@ -36,13 +36,10 @@ impl PyGraphVertices { let support = bdd.as_native().support_set(); let expected: HashSet = ctx.state_variables().iter().cloned().collect(); assert!(support.is_subset(&expected)); - PyGraphVertices( - graph - .as_native() - .empty_vertices() - .vertices() - .copy(bdd.into()), - ) + PyGraphVertices(GraphVertices::new( + bdd.into(), + graph.as_native().symbolic_context(), + )) } pub fn to_bdd(&self) -> PyBdd { @@ -118,15 +115,7 @@ impl PyGraphVertices { } pub fn iterator(&self) -> PyGraphVertexIterator { - // See the discussion in `_impl_bdd_iterator.rs` on the safety of this approach. - let iterable = Box::new(self.as_native().materialize()); - let static_iterable = unsafe { - (iterable.as_ref() as *const IterableVertices) - .as_ref() - .unwrap() - }; - let iterator: GraphVertexIterator<'static> = static_iterable.iter(); - PyGraphVertexIterator(iterable, iterator) + PyGraphVertexIterator(self.as_native().iter()) } pub fn __iter__(&self) -> PyGraphVertexIterator { @@ -149,6 +138,6 @@ impl PyGraphVertexIterator { } fn __next__(mut slf: PyRefMut<'_, Self>) -> Option> { - slf.1.next().map(|it| it.values()) + slf.0.next().map(|it| it.values()) } } diff --git a/src/bindings/lib_param_bn/_impl_symbolic_async_graph.rs b/src/bindings/lib_param_bn/_impl_symbolic_async_graph.rs index 271b9930..3dc595e5 100644 --- a/src/bindings/lib_param_bn/_impl_symbolic_async_graph.rs +++ b/src/bindings/lib_param_bn/_impl_symbolic_async_graph.rs @@ -16,18 +16,22 @@ impl PySymbolicAsyncGraph { /// Create a new `SymbolicAsyncGraph` from a `BooleanNetwork`. #[new] pub fn new(network: PyBooleanNetwork) -> PyResult { - let result = SymbolicAsyncGraph::new(network.into()); + let result = SymbolicAsyncGraph::new(network.as_native()); match result { Ok(graph) => Ok(graph.into()), Err(e) => throw_runtime_error(e), } } - /// Obtain a copy of the underlying `BooleanNetwork` used by this `SymbolicAsyncGraph`. - pub fn network(&self, py: Python) -> PyResult> { - let network = self.as_native().as_network(); - let network = PyBooleanNetwork::from(network.clone()); - network.export_to_python(py) + /// Obtain a copy of the underlying `BooleanNetwork` used by this `SymbolicAsyncGraph`, or `None` if there is + /// no network. + pub fn network(&self, py: Python) -> PyResult>> { + if let Some(network) = self.as_native().as_network() { + let network = PyBooleanNetwork::from(network.clone()); + network.export_to_python(py).map(Some) + } else { + Ok(None) + } } /// Obtain a copy of the `SymbolicContext` used by this symbolic encoding. @@ -78,7 +82,7 @@ impl PySymbolicAsyncGraph { pub fn wrap_in_subspace(&self, vertices: &PyGraphVertices) -> HashMap { let space = self.as_native().wrap_in_subspace(vertices.as_native()); let mut result = HashMap::new(); - for k in self.as_native().as_network().variables() { + for k in self.as_native().variables() { if let Some(value) = space[k].try_as_bool() { result.insert(k.into(), value); } @@ -157,11 +161,12 @@ impl PySymbolicAsyncGraph { pub fn fix_parameter(&self, parameter: &PyAny, value: bool) -> PyResult { // Find parameter and validate. let id = self.resolve_parameter(parameter)?; - let param = self.as_native().as_network().get_parameter(id.into()); - if param.get_arity() != 0 { + let ctx = self.as_native().symbolic_context(); + let arity = ctx.get_network_parameter_arity(id.into()); + if arity != 0 { return throw_runtime_error(format!( "Parameter {} has non-zero arity.", - param.get_name() + ctx.get_network_parameter_name(id.into()) )); } @@ -196,11 +201,12 @@ impl PySymbolicAsyncGraph { value: bool, ) -> PyResult { let id = self.resolve_parameter(parameter)?; - let param = self.as_native().as_network().get_parameter(id.into()); - if (param.get_arity() as usize) != inputs.len() { + let ctx = self.as_native().symbolic_context(); + let arity = ctx.get_network_parameter_arity(id.into()); + if usize::from(arity) != inputs.len() { return throw_runtime_error(format!( "Arity mismatch for parameter {}.", - param.get_name() + ctx.get_network_parameter_name(id.into()) )); } let ctx = self.as_native().symbolic_context(); @@ -237,10 +243,16 @@ impl PySymbolicAsyncGraph { value: bool, ) -> PyResult { let id = self.resolve_variable(variable)?; + /* + + TODO: + At some point, we should add the method to symbolic context which would allow this + to be a runtime check again. + if self.as_native().as_network().regulators(id.into()).len() != inputs.len() { let name = self.as_native().as_network().get_variable_name(id.into()); return throw_runtime_error(format!("Artiy mismatch for variable {name}.")); - } + }*/ let ctx = self.as_native().symbolic_context(); let table = ctx.get_implicit_function_table(id.into()); let mut bdd = ctx.mk_constant(false); @@ -276,6 +288,11 @@ impl PySymbolicAsyncGraph { /// Make an empty `ColoredVertexSet`. pub fn empty_colored_vertices(&self) -> PyGraphColoredVertices { + self.as_native().mk_empty_colored_vertices().into() + } + + /// Make an empty `VertexSet`. + pub fn empty_vertices(&self) -> PyGraphVertices { self.as_native().mk_empty_vertices().into() } @@ -287,10 +304,7 @@ impl PySymbolicAsyncGraph { /// Return a `VertexSet` of all vertices valid in this graph. pub fn unit_vertices(&self) -> PyGraphVertices { - self.as_native() - .mk_unit_colored_vertices() - .vertices() - .into() + self.as_native().mk_unit_vertices().into() } /// Return a `ColoredVertexSet` of all color-vertex pairs valid in this graph (i.e. satisfting @@ -574,9 +588,8 @@ impl PySymbolicAsyncGraph { if let Ok(name) = variable.extract::() { let var = self .as_native() - .as_network() - .as_graph() - .find_variable(name.as_str()); + .symbolic_context() + .find_network_variable(name.as_str()); if let Some(var) = var { Ok(var.into()) } else { @@ -590,7 +603,10 @@ impl PySymbolicAsyncGraph { /// Resolve a `ParameterId` for a parameter given either as a string or as a `ParameterId`. pub(crate) fn resolve_parameter(&self, parameter: &PyAny) -> PyResult { if let Ok(name) = parameter.extract::() { - let param = self.as_native().as_network().find_parameter(name.as_str()); + let param = self + .as_native() + .symbolic_context() + .find_network_parameter(name.as_str()); if let Some(param) = param { Ok(param.into()) } else { diff --git a/src/bindings/lib_param_bn/_impl_symbolic_context.rs b/src/bindings/lib_param_bn/_impl_symbolic_context.rs index a960bde4..6cc9eaae 100644 --- a/src/bindings/lib_param_bn/_impl_symbolic_context.rs +++ b/src/bindings/lib_param_bn/_impl_symbolic_context.rs @@ -7,7 +7,7 @@ use crate::bindings::lib_param_bn::{ use crate::{throw_runtime_error, throw_type_error, AsNative}; use biodivine_lib_bdd::{BddPartialValuation, BddValuation, BddVariable, BddVariableSet}; use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; -use biodivine_lib_param_bn::VariableId; +use biodivine_lib_param_bn::{FnUpdate, VariableId}; use pyo3::prelude::*; use std::collections::HashMap; @@ -19,6 +19,10 @@ fn read_arg_list(variables: &[PyVariableId]) -> Vec { variables.iter().map(|it| (*it).into()).collect() } +fn read_fn_arg_list(variables: &[PyFnUpdate]) -> Vec { + variables.iter().map(|it| (*it).clone().into()).collect() +} + /// A helper method that reads a `BddValuation` object from `PyAny`, ensuring that the /// required `variables` are present in the result when the input is only a partial valuation. fn read_valuation( @@ -158,10 +162,10 @@ impl PySymbolicContext { pub fn mk_uninterpreted_function_is_true( &self, parameter: PyParameterId, - arguments: Vec, + arguments: Vec, ) -> PyBdd { self.as_native() - .mk_uninterpreted_function_is_true(parameter.into(), &read_arg_list(&arguments)) + .mk_uninterpreted_function_is_true(parameter.into(), &read_fn_arg_list(&arguments)) .into() } @@ -206,7 +210,7 @@ impl PySymbolicContext { &self, valuation: &PyAny, parameter: PyParameterId, - arguments: Vec, + arguments: Vec, ) -> PyResult { let required_variables = self .as_native() @@ -222,7 +226,7 @@ impl PySymbolicContext { .instantiate_uninterpreted_function( &valuation, parameter.into(), - &read_arg_list(&arguments), + &read_fn_arg_list(&arguments), ) .into()) } diff --git a/src/bindings/lib_param_bn/mod.rs b/src/bindings/lib_param_bn/mod.rs index b5d6e910..cbf6d076 100644 --- a/src/bindings/lib_param_bn/mod.rs +++ b/src/bindings/lib_param_bn/mod.rs @@ -3,8 +3,8 @@ use biodivine_lib_param_bn::symbolic_async_graph::projected_iteration::{ MixedProjection, MixedProjectionIterator, }; use biodivine_lib_param_bn::symbolic_async_graph::{ - GraphColoredVertices, GraphColors, GraphVertexIterator, GraphVertices, IterableVertices, - SymbolicAsyncGraph, SymbolicContext, + GraphColoredVertices, GraphColors, GraphVertexIterator, GraphVertices, SymbolicAsyncGraph, + SymbolicContext, }; use biodivine_lib_param_bn::{ BooleanNetwork, FnUpdate, ModelAnnotation, ParameterId, RegulatoryGraph, VariableId, @@ -84,7 +84,7 @@ pub struct PyModelAnnotation(ModelAnnotation); pub struct PyFixedPoints(); #[pyclass(name = "GraphVertexIterator")] -pub struct PyGraphVertexIterator(Box, GraphVertexIterator<'static>); +pub struct PyGraphVertexIterator(GraphVertexIterator); #[pyclass(name = "SymbolicContext")] #[derive(Clone, Wrapper)] diff --git a/src/bindings/pbn_control/_impl_perturbation_graph.rs b/src/bindings/pbn_control/_impl_perturbation_graph.rs index def41377..5547db1d 100644 --- a/src/bindings/pbn_control/_impl_perturbation_graph.rs +++ b/src/bindings/pbn_control/_impl_perturbation_graph.rs @@ -269,8 +269,8 @@ impl PyPerturbationGraph { /// Resolves a string or `VariableId` to `VariableId`. pub fn find_variable(&self, variable: &PyAny) -> PyResult { if let Ok(name) = variable.extract::() { - let network = self.as_native().as_original().as_network(); - if let Some(var) = network.as_graph().find_variable(name.as_str()) { + let ctx = self.as_native().as_original().symbolic_context(); + if let Some(var) = ctx.find_network_variable(name.as_str()) { Ok(var.into()) } else { throw_runtime_error(format!("Variable {name} not found.")) diff --git a/src/internal/classification/classify.rs b/src/internal/classification/classify.rs index 4418a519..16f32894 100644 --- a/src/internal/classification/classify.rs +++ b/src/internal/classification/classify.rs @@ -15,7 +15,7 @@ use biodivine_hctl_model_checker::preprocessing::parser::parse_and_minimize_hctl use biodivine_lib_param_bn::biodivine_std::traits::Set; use biodivine_lib_param_bn::symbolic_async_graph::{ - GraphColoredVertices, GraphColors, SymbolicAsyncGraph, + GraphColoredVertices, GraphColors, SymbolicAsyncGraph, SymbolicContext, }; use biodivine_lib_param_bn::{BooleanNetwork, ModelAnnotation}; @@ -52,6 +52,7 @@ pub fn classify(model_path: &str, output_zip: &str) -> Result<(), String> { return Err(format!("Input file `{model_path}` is not accessible.")); }; let bn = BooleanNetwork::try_from(aeon_str.as_str())?; + let ctx = SymbolicContext::new(&bn).unwrap(); let annotations = ModelAnnotation::from_model_string(aeon_str.as_str()); let assertions = read_model_assertions(&annotations); let named_properties = read_model_properties(&annotations)?; @@ -73,11 +74,11 @@ pub fn classify(model_path: &str, output_zip: &str) -> Result<(), String> { ); // Parse all formulae and count the max. number of HCTL variables across formulae. - let assertion_tree = parse_and_minimize_hctl_formula(&bn, &assertion)?; + let assertion_tree = parse_and_minimize_hctl_formula(&ctx, &assertion)?; let mut num_hctl_vars = collect_unique_hctl_vars(assertion_tree.clone()).len(); let mut property_trees: Vec = Vec::new(); for (_name, formula) in &named_properties { - let tree = parse_and_minimize_hctl_formula(&bn, formula.as_str())?; + let tree = parse_and_minimize_hctl_formula(&ctx, formula.as_str())?; let tree_vars = collect_unique_hctl_vars(tree.clone()).len(); num_hctl_vars = max(num_hctl_vars, tree_vars); property_trees.push(tree); @@ -114,7 +115,7 @@ pub fn classify(model_path: &str, output_zip: &str) -> Result<(), String> { // restrict the colors on the symbolic graph let graph = SymbolicAsyncGraph::with_custom_context( - bn, + &bn, graph.symbolic_context().clone(), valid_colors.as_bdd().clone(), )?; @@ -162,6 +163,7 @@ mod tests { }; use biodivine_hctl_model_checker::mc_utils::collect_unique_hctl_vars; use biodivine_hctl_model_checker::preprocessing::parser::parse_and_minimize_hctl_formula; + use biodivine_lib_param_bn::symbolic_async_graph::SymbolicContext; use biodivine_lib_param_bn::{BooleanNetwork, ModelAnnotation}; use std::cmp::max; @@ -175,6 +177,7 @@ mod tests { v_3 -> v_3 "; let bn = BooleanNetwork::try_from(aeon_str).unwrap(); + let ctx = SymbolicContext::new(&bn).unwrap(); let formulae = vec![ "!{x}: AX {x}".to_string(), "!{y}: (AG EF {y} & (!{z}: AX {z}))".to_string(), @@ -182,7 +185,7 @@ mod tests { let mut var_count = 0; for f in formulae { - let tree = parse_and_minimize_hctl_formula(&bn, f.as_str()).unwrap(); + let tree = parse_and_minimize_hctl_formula(&ctx, f.as_str()).unwrap(); let c = collect_unique_hctl_vars(tree).len(); var_count = max(c, var_count); } diff --git a/src/internal/classification/load_inputs.rs b/src/internal/classification/load_inputs.rs index 838b0e17..4366fd2a 100644 --- a/src/internal/classification/load_inputs.rs +++ b/src/internal/classification/load_inputs.rs @@ -88,7 +88,7 @@ pub fn load_classification_archive( // Load the BN model (from the archive) and generate the extended STG. let aeon_str = read_zip_file(&mut archive, "model.aeon"); let bn = BooleanNetwork::try_from(aeon_str.as_str())?; - let graph = SymbolicAsyncGraph::new(bn)?; + let graph = SymbolicAsyncGraph::new(&bn)?; // collect the classification outcomes (colored sets) from the individual BDD dumps let mut categories = HashMap::new(); diff --git a/src/internal/scc/_impl_classifier.rs b/src/internal/scc/_impl_classifier.rs index 28c21f87..243160ea 100644 --- a/src/internal/scc/_impl_classifier.rs +++ b/src/internal/scc/_impl_classifier.rs @@ -128,9 +128,9 @@ impl Classifier { } if !not_sink_params.is_empty() { let mut disorder = graph.mk_empty_colors(); - for variable in graph.as_network().variables() { + for variable in graph.variables() { let found_first_successor = &graph.var_can_post(variable, &without_sinks); - for next_variable in graph.as_network().variables() { + for next_variable in graph.variables() { if next_variable == variable { continue; } @@ -198,8 +198,8 @@ impl Classifier { component: GraphColoredVertices, graph: &SymbolicAsyncGraph, ) -> GraphColoredVertices { - let mut is_not_sink = graph.empty_vertices().clone(); - for variable in graph.as_network().variables() { + let mut is_not_sink = graph.empty_colored_vertices().clone(); + for variable in graph.variables() { let has_successor = &graph.var_can_post(variable, &component); if !has_successor.is_empty() { is_not_sink = is_not_sink.union(has_successor); diff --git a/src/internal/scc/algo_interleaved_transition_guided_reduction/mod.rs b/src/internal/scc/algo_interleaved_transition_guided_reduction/mod.rs index 10955770..5318b115 100644 --- a/src/internal/scc/algo_interleaved_transition_guided_reduction/mod.rs +++ b/src/internal/scc/algo_interleaved_transition_guided_reduction/mod.rs @@ -24,9 +24,9 @@ pub fn interleaved_transition_guided_reduction( graph: &SymbolicAsyncGraph, initial: GraphColoredVertices, ) -> (GraphColoredVertices, Vec) { - let variables = graph.as_network().variables().collect::>(); + let variables = graph.variables().collect::>(); let mut scheduler = Scheduler::new(initial, variables); - for variable in graph.as_network().variables() { + for variable in graph.variables() { scheduler.spawn(ReachableProcess::new( variable, graph,