Merge branch 'main' into phenotype-control

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "biodivine-aeon-py"
-version = "0.0.9-alpha1"
+version = "0.0.9-alpha2"
 edition = "2021"
 
 [lib]
@@ -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-lib-param-bn = { version="0.5.2", features=["solver-z3"] }
+biodivine-lib-bdd = "0.5.7"
 biodivine-pbn-control = { git = "https://github.com/sybila/biodivine-pbn-control", rev = "70d4e0d" }
-biodivine-hctl-model-checker = "0.2.0"
+biodivine-hctl-model-checker = "0.2.2"
 rand = "0.8.5"
 macros = { path = "macros" }
 zip = "0.6.6"

src/bindings/aeon.rs

@@ -41,11 +41,7 @@ pub fn xie_beerel_attractors(
     graph: &PySymbolicAsyncGraph,
     states: Option<&PyGraphColoredVertices>,
 ) -> Vec<PyGraphColoredVertices> {
-    let variables = graph
-        .as_native()
-        .as_network()
-        .variables()
-        .collect::<Vec<_>>();
+    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::<Vec<_>>();
+    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::<Vec<_>>();
+    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());

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),
     };

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<PyHctlTreeNode> {
-        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<PyHctlTreeNode> {
-        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),
         }

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<PyHctlTreeNode> {
+    pub(crate) fn from_python(any: &PyAny, ctx: &SymbolicContext) -> PyResult<PyHctlTreeNode> {
         if let Ok(val) = any.extract::<PyHctlTreeNode>() {
             Ok(val)
         } else if let Ok(string) = any.extract::<String>() {
-            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<PyGraphColoredVertices> {
     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<HctlTreeNode> = 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 {

src/bindings/lib_param_bn/_impl_boolean_network.rs

@@ -331,8 +331,15 @@ impl PyBooleanNetwork {
         }
     }
 
-    pub fn inline_inputs(&self, py: Python) -> PyResult<Py<PyBooleanNetwork>> {
-        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<Py<PyBooleanNetwork>> {
+        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<Option<Py<PyBooleanNetwork>>> {
         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()
     }

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<usize>,
         positive_restriction: Option<Vec<&PyDict>>,
@@ -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<PyGraphColoredVertices> = 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<usize>,
         positive_restriction: Option<Vec<&PyDict>>,
@@ -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<usize>,
         positive_restriction: Option<Vec<&PyDict>>,
@@ -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<Space> {
-    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::<bool>()?.into();