From 361a59bf60d42a58c2292d77bb3c6daca1174b9e Mon Sep 17 00:00:00 2001 From: Prokop Tunel <47597303+AurumTheEnd@users.noreply.github.com> Date: Thu, 23 May 2024 03:17:21 +0200 Subject: [PATCH] Misc changes (#29) --- Cargo.toml | 7 +- LICENSE | 21 ++ README.md | 114 +++++++ scripts/local_dev.sh | 10 + src/bdd/iterators/image.rs | 4 +- src/bdd/mod.rs | 4 +- src/bindings/bdd.rs | 283 ++++++++++++++++- src/bindings/expression.rs | 287 +++++++++++++++++- src/bindings/iterators/domain.rs | 23 ++ src/bindings/iterators/mod.rs | 21 ++ src/bindings/iterators/range_bdd.rs | 23 ++ src/bindings/iterators/range_expression.rs | 23 ++ src/bindings/iterators/range_table.rs | 23 ++ src/bindings/iterators/relation_bdd.rs | 26 ++ src/bindings/iterators/relation_expression.rs | 24 ++ src/bindings/iterators/relation_table.rs | 24 ++ src/bindings/iterators/support_bdd.rs | 24 ++ src/bindings/iterators/support_expression.rs | 24 ++ src/bindings/iterators/support_table.rs | 24 ++ src/bindings/mod.rs | 9 + src/bindings/table.rs | 271 +++++++++++++++-- src/expressions/structs/expression.rs | 105 ++++++- src/expressions/traits/operations/equality.rs | 39 +++ .../traits/operations/implication.rs | 16 +- src/expressions/traits/operations/mod.rs | 1 + src/iterators/image.rs | 7 +- src/iterators/relation.rs | 7 +- src/iterators/support.rs | 7 +- src/table/iterators/support.rs | 20 +- src/table/mod.rs | 2 +- src/traits/mod.rs | 2 +- src/traits/operations/equality.rs | 7 + src/traits/operations/mod.rs | 1 + 33 files changed, 1394 insertions(+), 89 deletions(-) create mode 100644 LICENSE create mode 100644 src/bindings/iterators/domain.rs create mode 100644 src/bindings/iterators/mod.rs create mode 100644 src/bindings/iterators/range_bdd.rs create mode 100644 src/bindings/iterators/range_expression.rs create mode 100644 src/bindings/iterators/range_table.rs create mode 100644 src/bindings/iterators/relation_bdd.rs create mode 100644 src/bindings/iterators/relation_expression.rs create mode 100644 src/bindings/iterators/relation_table.rs create mode 100644 src/bindings/iterators/support_bdd.rs create mode 100644 src/bindings/iterators/support_expression.rs create mode 100644 src/bindings/iterators/support_table.rs create mode 100644 src/expressions/traits/operations/equality.rs create mode 100644 src/traits/operations/equality.rs diff --git a/Cargo.toml b/Cargo.toml index ffc21ec..0a69256 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,13 +10,14 @@ name = "biodivine_boolean_functions" crate-type = ["cdylib", "rlib"] [features] +default = ["python"] python = ["dep:pyo3"] csv = ["dep:csv", "dep:tempfile"] [dependencies] -thiserror = "1.0.50" -itertools = "0.12.0" -regex = "1.10.3" +thiserror = "1.0.61" +itertools = "0.13.0" +regex = "1.10.4" lazy_static = "1.4.0" tabled = "0.15.0" csv = { version = "1.3.0", optional = true } diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..e65294a --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2019-2024 Sybila Systems Biology Laboratory + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README.md b/README.md index 0c6b381..3c2e017 100644 --- a/README.md +++ b/README.md @@ -4,3 +4,117 @@ # Biodivine/Boolean Functions +This is a Rust library with Python PyO3 bindings for Boolean function manipulation. + +You can represent Boolean functions as + +- Expression trees, +- Truth tables, or +- Reduced, Ordered Binary Decision Diagrams. + +## Local usage from Rust + +1. Set up the dependency + ```toml + [dependencies] + biodivine-boolean-functions = { git = "https://github.com/sybila/biodivine-boolean-functions" } + ``` + +2. Use from Rust! + ```rust + use biodivine_boolean_functions::bdd::Bdd; + use biodivine_boolean_functions::expressions::{bool, var, Expression, ExpressionNode}; + use biodivine_boolean_functions::table::display_formatted::{TableBooleanFormatting, TableStyle}; + use biodivine_boolean_functions::table::TruthTable; + use biodivine_boolean_functions::traits::BooleanFunction; + use std::collections::BTreeMap; + use std::str::FromStr; + + // ############### + // # Expressions # + // ############### + + // Create an expression with convenience functions + let expression = var("a") & !var("b") & bool(true); + // Create an expression by nesting nodes + let other_expression = Expression::n_ary_and(&[ + ExpressionNode::Literal("a".to_string()).into(), + Expression::negate(&ExpressionNode::Literal("b".to_string()).into()), + ExpressionNode::Constant(true).into(), + ]); + // Create an expression by parsing it from a string + let parsed_expression = + Expression::from_str("a and not b and true").expect("This input string should be valid."); + + // The three expressions are semantically (and syntactically) equivalent + assert!(expression.is_equivalent(&other_expression)); + assert!(expression.is_equivalent(&parsed_expression)); + + let dnf = expression.to_dnf(); + println!("{}", dnf); // (a & !(b) & true) + + // ################ + // # Truth Tables # + // ################ + + let table: TruthTable = expression.into(); + let table = table.restrict(&BTreeMap::from([("a".to_string(), true)])); + + println!( + "{}", + table.to_string_formatted( + TableStyle::Markdown, + TableBooleanFormatting::Word, + TableBooleanFormatting::Word + ) + ); + // | b | result | + // |-------|--------| + // | false | true | + // | true | false | + + // ############################ + // # Binary Decision Diagrams # + // ############################ + + let bdd: Bdd = table + .try_into() + .expect("Table should not have more than 2^16 variables."); + println!("{:?}", bdd.sat_point()) // Some([false]) + ``` + +## Local usage from Python + +1. Create a Python virtual environment + +2. Run the following to set up PyO3 with `maturin` as per [the docs](https://pyo3.rs/v0.21.2/getting-started). + ```shell + $ bash ./scripts/local_dev.sh + ``` + +3. Use from Python! + ```python + import biodivine_boolean_functions as bbf + + expression = bbf.var("a") & ~bbf.var("b") & bbf.bool(True) + expression_nested = bbf.Expression.mk_and_n_ary([ + bbf.Expression.mk_literal("a"), + bbf.Expression.mk_not(bbf.Expression.mk_literal("b")), + bbf.Expression.mk_constant(True) + ]) + expression_parsed = bbf.Expression("a and not b and true") + + assert expression.semantic_eq(expression_parsed) + assert expression.semantic_eq(expression_nested) + + dnf = expression.to_dnf() + print(dnf) + + table = expression.to_table() + restricted = table.restrict({"a": True}) + print(restricted.to_string_formatted(bbf.TableStyle.Markdown, bbf.TableBooleanFormatting.Word)) + + bdd = expression.to_bdd() + print(bdd.sat_point()) + ``` + diff --git a/scripts/local_dev.sh b/scripts/local_dev.sh index 8125abe..2c38cc7 100755 --- a/scripts/local_dev.sh +++ b/scripts/local_dev.sh @@ -1,5 +1,15 @@ #!/bin/bash +## Resolve folder of this script, following all symlinks, cd to parent +SCRIPT_SOURCE="${BASH_SOURCE[0]}" +while [ -h "$SCRIPT_SOURCE" ]; do # resolve $SOURCE until the file is no longer a symlink + SCRIPT_DIR="$( cd -P "$( dirname "$SCRIPT_SOURCE" )" && pwd )" + SCRIPT_SOURCE="$(readlink "$SCRIPT_SOURCE")" + # if $SOURCE was a relative symlink, we need to resolve it relative to the path where the symlink file was located + [[ $SCRIPT_SOURCE != /* ]] && SCRIPT_SOURCE="$SCRIPT_DIR/$SCRIPT_SOURCE" +done +cd -P "$( dirname "$SCRIPT_SOURCE" )/.." || exit 1 + # If VIRTUAL_ENV is not set, check if either venv, .venv or .env directory # exists and use that as the Python environment. diff --git a/src/bdd/iterators/image.rs b/src/bdd/iterators/image.rs index 2cc6879..b112c14 100644 --- a/src/bdd/iterators/image.rs +++ b/src/bdd/iterators/image.rs @@ -3,14 +3,14 @@ use biodivine_lib_bdd::Bdd; use biodivine_lib_bdd::BddValuation; pub struct ImageIterator { - domain_iterator: Box>>, + domain_iterator: DomainIterator, bdd: Bdd, } impl ImageIterator { pub(crate) fn new(input_count: usize, bdd: &Bdd) -> Self { Self { - domain_iterator: Box::new(DomainIterator::from_count(input_count)), + domain_iterator: DomainIterator::from_count(input_count), bdd: bdd.clone(), } } diff --git a/src/bdd/mod.rs b/src/bdd/mod.rs index b018354..2ea37ba 100644 --- a/src/bdd/mod.rs +++ b/src/bdd/mod.rs @@ -6,7 +6,7 @@ use biodivine_lib_bdd::{Bdd as InnerBdd, BddVariable, BddVariableSet}; use crate::bdd::utils::{extend_bdd_variables, prune_bdd_variables}; -mod iterators; +pub mod iterators; mod traits; mod utils; @@ -102,7 +102,7 @@ impl Bdd { Ok(BddVariableSet::new_anonymous(num_vars)) } - pub(crate) fn inner(&self) -> &InnerBdd { + pub fn inner(&self) -> &InnerBdd { &self.bdd } diff --git a/src/bindings/bdd.rs b/src/bindings/bdd.rs index ca1256c..7ae9f92 100644 --- a/src/bindings/bdd.rs +++ b/src/bindings/bdd.rs @@ -1,11 +1,19 @@ use num_bigint::BigUint; use pyo3::exceptions::PyRuntimeError; use pyo3::{pyclass, pymethods, PyResult}; +use std::collections::{BTreeMap, BTreeSet}; use crate::bdd::Bdd; +use crate::bindings::error::PythonExpressionError::UnknownVariableWhileEvaluating; use crate::bindings::expression::PythonExpression; +use crate::bindings::iterators::{ + PythonBddRangeIterator, PythonBddRelationIterator, PythonBddSupportIterator, + PythonDomainIterator, +}; +use crate::bindings::table::PythonTruthTable; use crate::expressions::Expression; -use crate::traits::BooleanFunction; +use crate::table::TruthTable; +use crate::traits::{BooleanFunction, BooleanPoint, BooleanValuation, Evaluate}; #[pyclass(frozen, name = "Bdd")] #[derive(Clone, Debug, Eq, PartialEq)] @@ -13,19 +21,26 @@ pub struct PythonBdd { root: Bdd, } -#[pymethods] -impl PythonBdd { - #[staticmethod] - pub fn from_expression(expression: &PythonExpression) -> PyResult { - let native: Expression = expression.into(); - match Bdd::try_from(native) { - Ok(bdd) => Ok(Self::new(bdd)), - Err(_e) => Err(PyRuntimeError::new_err( - "Conversion failed. Too many variables.", - )), - } +impl From> for PythonBdd { + fn from(value: Bdd) -> Self { + PythonBdd::new(value) } +} + +impl From for Bdd { + fn from(value: PythonBdd) -> Self { + (&value).into() + } +} + +impl From<&PythonBdd> for Bdd { + fn from(value: &PythonBdd) -> Self { + value.root.clone() + } +} +#[pymethods] +impl PythonBdd { #[staticmethod] pub fn mk_not(inner: &PythonBdd) -> PythonBdd { PythonBdd::new(!(&inner.root)) @@ -56,8 +71,28 @@ impl PythonBdd { PythonBdd::new(Bdd::mk_literal(variable.to_string(), value)) } - pub fn weight(&self) -> BigUint { - self.root.weight() + /// Throws a `KeyError` when a variable is encountered that isn't found among + /// the given `literal_values`. + pub fn evaluate_checked(&self, literal_values: BTreeMap) -> PyResult { + Ok(self + .root + .evaluate_checked(&literal_values) + .map_err(|name| UnknownVariableWhileEvaluating { name })?) + } + + /// Variables not in the dictionary default to false. + pub fn evaluate_safe(&self, literal_values: BTreeMap) -> bool { + self.root.evaluate(&literal_values) + } + + /// Variables not in the dictionary defaults to the passed `default_value` argument. + pub fn evaluate_with_default( + &self, + literal_values: BTreeMap, + default_value: bool, + ) -> bool { + self.root + .evaluate_with_default(&literal_values, default_value) } pub fn node_count(&self) -> usize { @@ -71,6 +106,226 @@ impl PythonBdd { pub fn __repr__(&self) -> String { self.__str__() } + + /// A set of all the variable instances that (syntactically) appear in this Boolean + /// function. + /// + /// See also [BooleanFunction::essential_inputs]. + /// + /// ### Examples + /// + /// The inputs of the expression `(a & b) => (c | !c)` are `{a, b, c}`. + /// + /// ### Implementation notes + /// + /// This operation should be at worst `O(|F|)` for any function representation. + fn inputs(&self) -> BTreeSet { + self.root.inputs() + } + + /// A set of all variable instances that are *essential* in this Boolean function. + /// + /// Intuitively, a variable `v` is essential in function `F` if `v` has some observable + /// impact on the output of `F`. In other words, there is some input vector `X` such that + /// `F(X[v=0]) != F(X[v=1])` (here `X[v=b]` denotes a copy of `X` with the value of `v` + /// fixed to `b`). + /// + /// For a proper formal definition, see for example the introduction in + /// [this paper](https://arxiv.org/pdf/0812.1979.pdf). + /// + /// See also [BooleanFunction::inputs]. + /// + /// ### Examples + /// + /// The essential inputs of the expression `(a & b) => (c | !c)` are `{}`, because + /// this expression is a tautology. + /// + /// ### Implementation notes + /// + /// * BDD: The operation takes `O(|F|)` time by scanning the variables stored in the + /// BDD nodes. + /// * Table: The operation takes `O(n * |F|)` time by scanning the corresponding output + /// pairs for each variable. + /// * Expression: The operation is non-trivial, as we need to determine for each variable + /// whether `F[v = 0]` and `F[v = 1]` are semantically equal. + /// + fn essential_inputs(&self) -> BTreeSet { + self.root.essential_inputs() + } + + /// The number of variables that (syntactically) appear in this Boolean function. + /// + /// This is equivalent to the length of [BooleanFunction::inputs]. + fn degree(&self) -> usize { + self.root.degree() + } + + /// The number of variables that are essential in this Boolean function. + /// + /// This is equivalent to the length of [BooleanFunction::essential_inputs]. + fn essential_degree(&self) -> usize { + self.root.essential_degree() + } + + /// The iterator over Boolean points that are valid as inputs for this Boolean function. + /// + /// This is always the complete space of `2^n` Boolean vectors. + fn domain(&self) -> PythonDomainIterator { + self.root.domain().into() + } + + /// The iterator over all the output values of this Boolean function. + /// + /// The iteration order should correspond to the elements of [BooleanFunction::domain]. + fn image(&self) -> PythonBddRangeIterator { + self.root.image().into() + } + + /// The combined iterator of all input points together with their corresponding outputs. + /// + /// See also [BooleanFunction::domain] and [BooleanFunction::image]. + fn relation(&self) -> PythonBddRelationIterator { + self.root.relation().into() + } + + /// The iterator over all Boolean points for which this function evaluates to `1`. + fn support(&self) -> PythonBddSupportIterator { + self.root.support().into() + } + + /// The number of input points for which this function evaluates to `1`. + /// + /// See also [BooleanFunction::support]. + fn weight(&self) -> BigUint { + self.root.weight() + } + + /// Create a Boolean function that is a restriction of this function for the given variables. + /// + /// A restriction fixes all variables specified by the `valuation` to their respective + /// constant values. That is, the resulting function no longer depends on these variables. + /// + /// ### Examples + /// + /// A Boolean expression `(a | b) & c` restricted to `{ a: 0, c: 1 }` is `(false | b) & true` + /// semantically equal to `b`. + /// + /// ### Implementation notes + /// + /// It is not an error to supply a valuation that also fixes variables that are not the inputs + /// of this function. Such variables are simply ignored. + fn restrict(&self, valuation: BooleanValuation) -> Self { + self.root.restrict(&valuation).into() + } + + /// Create a Boolean function in which the variables specified by `mapping` are substituted + /// for their supplied functions. + /// + /// ### Examples + /// + /// Substituting `a` for `(a | b | c)` in the expression `a & !c` produces `(a | b | c) & !c`. + /// + /// ### Implementation notes + /// + /// Note that the same variable can be substituted and at the same time appear in one of the + /// substituted functions (as in the example). Also note that this operation can increase the + /// degree of a function if the substituted functions contain previously unused variables. + fn substitute(&self, mapping: BTreeMap) -> Self { + self.root + .substitute(&BTreeMap::from_iter( + mapping.into_iter().map(|(k, v)| (k, v.root)), + )) + .into() + } + + /// Produce one [BooleanPoint] for which this function evaluates to `1`, i.e. one of the + /// points in [BooleanFunction::support]. + /// + /// This value should be deterministic, but otherwise can be arbitrary. Returns `None` if + /// the function is not satisfiable. + /// + /// ### Implementation notes + /// + /// This operation is `O(|F|)` for tables, `O(1)` for BDDs, and NP-complete for expressions. + fn sat_point(&self) -> Option { + self.root.sat_point() + } + + /// Eliminate the specified `variables` using *existential* quantification. The resulting + /// function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] | F[v = 1]`. In other words, the resulting + /// function is satisfied for input `x` if there *exists* a value `b` of `v` such that the + /// original function was satisfied for `x[v=b]`. + /// + fn existential_quantification(&self, variables: BTreeSet) -> Self { + self.root.existential_quantification(variables).into() + } + + /// Eliminate the specified `variables` using *universal* quantification. The resulting + /// function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] & F[v = 1]`. In other words, the resulting + /// function is satisfied for `x` if the original function was satisfied for both `x[v=0]` + /// and `x[v=1]`. + /// + fn universal_quantification(&self, variables: BTreeSet) -> Self { + self.root.universal_quantification(variables).into() + } + + /// Computes the derivative of this function with respect to the given `variables`. + /// The resulting function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] ^ F[v = 1]`. In other words, the resulting + /// function is satisfied for `x`, if the values of `F(x[v=0])` and `F(x[v=1])` are different. + /// (Hence the name "derivative": the result is a function that is true for all inputs in + /// which the input function can change its value). + /// + fn derivative(&self, variables: BTreeSet) -> Self { + self.root.derivative(variables).into() + } + + /// Returns `true` if the two functions are *semantically* equivalent. That is, they output + /// the same values for the same inputs. + fn is_equivalent(&self, other: &Self) -> bool { + self.root.is_equivalent(&other.root) + } + + /// Returns `true` if this function is *implied* by the `other` function. That is, it outputs + /// `1` *at least* for those inputs where `other` outputs one. + fn is_implied_by(&self, other: &Self) -> bool { + self.root.is_implied_by(&other.root) + } + + #[staticmethod] + pub fn from_expression(expression: &PythonExpression) -> PyResult { + let native: Expression = expression.into(); + match Bdd::try_from(native) { + Ok(bdd) => Ok(Self::new(bdd)), + Err(_e) => Err(PyRuntimeError::new_err( + "Conversion failed. Too many variables.", + )), + } + } + + #[staticmethod] + pub fn from_table(table: &PythonTruthTable) -> PyResult { + let native: TruthTable = table.into(); + match Bdd::try_from(native) { + Ok(bdd) => Ok(Self::new(bdd)), + Err(_e) => Err(PyRuntimeError::new_err( + "Conversion failed. Too many variables.", + )), + } + } + + pub fn to_expression(&self) -> PythonExpression { + PythonExpression::from_bdd(self) + } + + pub fn to_table(&self) -> PythonTruthTable { + PythonTruthTable::from_bdd(self) + } } impl PythonBdd { diff --git a/src/bindings/expression.rs b/src/bindings/expression.rs index 9f45009..d97c5ef 100644 --- a/src/bindings/expression.rs +++ b/src/bindings/expression.rs @@ -1,13 +1,24 @@ +use num_bigint::BigUint; use std::collections::{BTreeMap, BTreeSet}; use std::str::FromStr; -use pyo3::prelude::{pyclass, pymethods, PyAny, PyAnyMethods, PyResult}; +use crate::bdd::Bdd; +use crate::bindings::bdd::PythonBdd; +use pyo3::prelude::{pyclass, pyfunction, pymethods, PyAny, PyAnyMethods, PyResult}; use pyo3::Bound; use crate::bindings::error::PythonExpressionError; use crate::bindings::error::PythonExpressionError::UnknownVariableWhileEvaluating; -use crate::expressions::{Expression as RustExpression, ExpressionNode}; -use crate::traits::{Evaluate, GatherLiterals, SemanticEq}; +use crate::bindings::iterators::{ + PythonDomainIterator, PythonExpressionRangeIterator, PythonExpressionRelationIterator, + PythonExpressionSupportIterator, +}; +use crate::bindings::table::PythonTruthTable; +use crate::expressions::{Expression as RustExpression, Expression, ExpressionNode}; +use crate::table::TruthTable; +use crate::traits::{ + BooleanFunction, BooleanPoint, BooleanValuation, Evaluate, GatherLiterals, SemanticEq, +}; #[pyclass(frozen, name = "Expression")] #[derive(Clone, Debug, Eq, PartialEq)] @@ -60,10 +71,22 @@ impl PythonExpression { Self::new(self.root.to_cnf()) } + pub fn to_dnf(&self) -> Self { + Self::new(self.root.to_dnf()) + } + + pub fn is_nnf(&self) -> bool { + self.root.is_nnf() + } + pub fn is_cnf(&self) -> bool { self.root.is_cnf() } + pub fn is_dnf(&self) -> bool { + self.root.is_dnf() + } + /// Throws a `KeyError` when a variable is encountered that isn't found among /// the given `literal_values`. pub fn evaluate_checked(&self, literal_values: BTreeMap) -> PyResult { @@ -74,8 +97,8 @@ impl PythonExpression { } /// Variables not in the dictionary default to false. - pub fn evaluate(&self, literal_values: BTreeMap) -> PyResult { - Ok(self.root.evaluate(&literal_values)) + pub fn evaluate_safe(&self, literal_values: BTreeMap) -> bool { + self.root.evaluate(&literal_values) } /// Variables not in the dictionary defaults to the passed `default_value` argument. @@ -83,10 +106,9 @@ impl PythonExpression { &self, literal_values: BTreeMap, default_value: bool, - ) -> PyResult { - Ok(self - .root - .evaluate_with_default(&literal_values, default_value)) + ) -> bool { + self.root + .evaluate_with_default(&literal_values, default_value) } pub fn gather_literals(&self) -> BTreeSet { @@ -134,6 +156,18 @@ impl PythonExpression { Self::new(RustExpression::negate(&expression.root)) } + fn __invert__(&self) -> PythonExpression { + Self::mk_not(self) + } + + fn __and__(&self, other: &PythonExpression) -> PythonExpression { + Self::mk_and_binary(self, other) + } + + fn __or__(&self, other: &PythonExpression) -> PythonExpression { + Self::mk_or_binary(self, other) + } + #[staticmethod] pub fn mk_and_binary(left: &PythonExpression, right: &PythonExpression) -> PythonExpression { Self::new(RustExpression::binary_and(&left.root, &right.root)) @@ -165,6 +199,220 @@ impl PythonExpression { pub fn __repr__(&self) -> String { format!("PythonExpression(\"{}\")", self.__str__()) } + + /// A set of all the variable instances that (syntactically) appear in this Boolean + /// function. + /// + /// See also [BooleanFunction::essential_inputs]. + /// + /// ### Examples + /// + /// The inputs of the expression `(a & b) => (c | !c)` are `{a, b, c}`. + /// + /// ### Implementation notes + /// + /// This operation should be at worst `O(|F|)` for any function representation. + fn inputs(&self) -> BTreeSet { + self.root.inputs() + } + + /// A set of all variable instances that are *essential* in this Boolean function. + /// + /// Intuitively, a variable `v` is essential in function `F` if `v` has some observable + /// impact on the output of `F`. In other words, there is some input vector `X` such that + /// `F(X[v=0]) != F(X[v=1])` (here `X[v=b]` denotes a copy of `X` with the value of `v` + /// fixed to `b`). + /// + /// For a proper formal definition, see for example the introduction in + /// [this paper](https://arxiv.org/pdf/0812.1979.pdf). + /// + /// See also [BooleanFunction::inputs]. + /// + /// ### Examples + /// + /// The essential inputs of the expression `(a & b) => (c | !c)` are `{}`, because + /// this expression is a tautology. + /// + /// ### Implementation notes + /// + /// * BDD: The operation takes `O(|F|)` time by scanning the variables stored in the + /// BDD nodes. + /// * Table: The operation takes `O(n * |F|)` time by scanning the corresponding output + /// pairs for each variable. + /// * Expression: The operation is non-trivial, as we need to determine for each variable + /// whether `F[v = 0]` and `F[v = 1]` are semantically equal. + /// + fn essential_inputs(&self) -> BTreeSet { + self.root.essential_inputs() + } + + /// The number of variables that (syntactically) appear in this Boolean function. + /// + /// This is equivalent to the length of [BooleanFunction::inputs]. + fn degree(&self) -> usize { + self.root.degree() + } + + /// The number of variables that are essential in this Boolean function. + /// + /// This is equivalent to the length of [BooleanFunction::essential_inputs]. + fn essential_degree(&self) -> usize { + self.root.essential_degree() + } + + /// The iterator over Boolean points that are valid as inputs for this Boolean function. + /// + /// This is always the complete space of `2^n` Boolean vectors. + fn domain(&self) -> PythonDomainIterator { + self.root.domain().into() + } + + /// The iterator over all the output values of this Boolean function. + /// + /// The iteration order should correspond to the elements of [BooleanFunction::domain]. + fn image(&self) -> PythonExpressionRangeIterator { + self.root.image().into() + } + + /// The combined iterator of all input points together with their corresponding outputs. + /// + /// See also [BooleanFunction::domain] and [BooleanFunction::image]. + fn relation(&self) -> PythonExpressionRelationIterator { + self.root.relation().into() + } + + /// The iterator over all Boolean points for which this function evaluates to `1`. + fn support(&self) -> PythonExpressionSupportIterator { + self.root.support().into() + } + + /// The number of input points for which this function evaluates to `1`. + /// + /// See also [BooleanFunction::support]. + fn weight(&self) -> BigUint { + self.root.weight() + } + + /// Create a Boolean function that is a restriction of this function for the given variables. + /// + /// A restriction fixes all variables specified by the `valuation` to their respective + /// constant values. That is, the resulting function no longer depends on these variables. + /// + /// ### Examples + /// + /// A Boolean expression `(a | b) & c` restricted to `{ a: 0, c: 1 }` is `(false | b) & true` + /// semantically equal to `b`. + /// + /// ### Implementation notes + /// + /// It is not an error to supply a valuation that also fixes variables that are not the inputs + /// of this function. Such variables are simply ignored. + fn restrict(&self, valuation: BooleanValuation) -> Self { + self.root.restrict(&valuation).into() + } + + /// Create a Boolean function in which the variables specified by `mapping` are substituted + /// for their supplied functions. + /// + /// ### Examples + /// + /// Substituting `a` for `(a | b | c)` in the expression `a & !c` produces `(a | b | c) & !c`. + /// + /// ### Implementation notes + /// + /// Note that the same variable can be substituted and at the same time appear in one of the + /// substituted functions (as in the example). Also note that this operation can increase the + /// degree of a function if the substituted functions contain previously unused variables. + fn substitute(&self, mapping: BTreeMap) -> Self { + self.root + .substitute(&BTreeMap::from_iter( + mapping.into_iter().map(|(k, v)| (k, v.root)), + )) + .into() + } + + /// Produce one [BooleanPoint] for which this function evaluates to `1`, i.e. one of the + /// points in [BooleanFunction::support]. + /// + /// This value should be deterministic, but otherwise can be arbitrary. Returns `None` if + /// the function is not satisfiable. + /// + /// ### Implementation notes + /// + /// This operation is `O(|F|)` for tables, `O(1)` for BDDs, and NP-complete for expressions. + fn sat_point(&self) -> Option { + self.root.sat_point() + } + + /// Eliminate the specified `variables` using *existential* quantification. The resulting + /// function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] | F[v = 1]`. In other words, the resulting + /// function is satisfied for input `x` if there *exists* a value `b` of `v` such that the + /// original function was satisfied for `x[v=b]`. + /// + fn existential_quantification(&self, variables: BTreeSet) -> Self { + self.root.existential_quantification(variables).into() + } + + /// Eliminate the specified `variables` using *universal* quantification. The resulting + /// function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] & F[v = 1]`. In other words, the resulting + /// function is satisfied for `x` if the original function was satisfied for both `x[v=0]` + /// and `x[v=1]`. + /// + fn universal_quantification(&self, variables: BTreeSet) -> Self { + self.root.universal_quantification(variables).into() + } + + /// Computes the derivative of this function with respect to the given `variables`. + /// The resulting function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] ^ F[v = 1]`. In other words, the resulting + /// function is satisfied for `x`, if the values of `F(x[v=0])` and `F(x[v=1])` are different. + /// (Hence the name "derivative": the result is a function that is true for all inputs in + /// which the input function can change its value). + /// + fn derivative(&self, variables: BTreeSet) -> Self { + self.root.derivative(variables).into() + } + + /// Returns `true` if the two functions are *semantically* equivalent. That is, they output + /// the same values for the same inputs. + fn is_equivalent(&self, other: &Self) -> bool { + self.root.is_equivalent(&other.root) + } + + /// Returns `true` if this function is *implied* by the `other` function. That is, it outputs + /// `1` *at least* for those inputs where `other` outputs one. + fn is_implied_by(&self, other: &Self) -> bool { + self.root.is_implied_by(&other.root) + } + + #[staticmethod] + pub fn from_table(table: &PythonTruthTable) -> Self { + let rust_table: TruthTable = table.into(); + let rust_expression: Expression = rust_table.to_expression_trivial(); + + Self::new(rust_expression) + } + + #[staticmethod] + pub fn from_bdd(bdd: &PythonBdd) -> Self { + let rust_table: Bdd = bdd.into(); + let rust_expression: Expression = rust_table.into(); + + Self::new(rust_expression) + } + + fn to_table(&self) -> PythonTruthTable { + PythonTruthTable::from_expression(self) + } + + fn to_bdd(&self) -> PyResult { + PythonBdd::from_expression(self) + } } impl PythonExpression { @@ -172,3 +420,24 @@ impl PythonExpression { PythonExpression { root: expression } } } + +#[pyfunction] +/// A utility function to quickly create a list of literal expressions, useful for constructing n_ary operators. +pub fn vars(names: Vec) -> Vec { + names + .into_iter() + .map(|name| Expression::from(ExpressionNode::Literal(name)).into()) + .collect() +} + +#[pyfunction] +/// A utility function to quickly create a single literal expression. +pub fn var(name: String) -> PythonExpression { + Expression::from(ExpressionNode::Literal(name.to_string())).into() +} + +#[pyfunction] +/// A utility function to quickly create a single constant expression. +pub fn bool(value: bool) -> PythonExpression { + Expression::from(ExpressionNode::Constant(value)).into() +} diff --git a/src/bindings/iterators/domain.rs b/src/bindings/iterators/domain.rs new file mode 100644 index 0000000..de33f77 --- /dev/null +++ b/src/bindings/iterators/domain.rs @@ -0,0 +1,23 @@ +use crate::iterators::DomainIterator; +use pyo3::prelude::*; + +#[pyclass(name = "DomainIterator")] +pub struct PythonDomainIterator { + iter: DomainIterator, +} + +#[pymethods] +impl PythonDomainIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option> { + slf.iter.next() + } +} + +impl From for PythonDomainIterator { + fn from(value: DomainIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/mod.rs b/src/bindings/iterators/mod.rs new file mode 100644 index 0000000..9e04ce9 --- /dev/null +++ b/src/bindings/iterators/mod.rs @@ -0,0 +1,21 @@ +pub use domain::PythonDomainIterator; +pub use range_bdd::PythonBddRangeIterator; +pub use range_expression::PythonExpressionRangeIterator; +pub use range_table::PythonTableRangeIterator; +pub use relation_bdd::PythonBddRelationIterator; +pub use relation_expression::PythonExpressionRelationIterator; +pub use relation_table::PythonTableRelationIterator; +pub use support_bdd::PythonBddSupportIterator; +pub use support_expression::PythonExpressionSupportIterator; +pub use support_table::PythonTableSupportIterator; + +mod domain; +mod range_bdd; +mod range_expression; +mod range_table; +mod relation_bdd; +mod relation_expression; +mod relation_table; +mod support_bdd; +mod support_expression; +mod support_table; diff --git a/src/bindings/iterators/range_bdd.rs b/src/bindings/iterators/range_bdd.rs new file mode 100644 index 0000000..9b801f7 --- /dev/null +++ b/src/bindings/iterators/range_bdd.rs @@ -0,0 +1,23 @@ +use crate::bdd::iterators::ImageIterator; +use pyo3::prelude::*; + +#[pyclass(name = "BddRangeIterator")] +pub struct PythonBddRangeIterator { + iter: ImageIterator, +} + +#[pymethods] +impl PythonBddRangeIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option { + slf.iter.next() + } +} + +impl From for PythonBddRangeIterator { + fn from(value: ImageIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/range_expression.rs b/src/bindings/iterators/range_expression.rs new file mode 100644 index 0000000..6638f15 --- /dev/null +++ b/src/bindings/iterators/range_expression.rs @@ -0,0 +1,23 @@ +use crate::iterators::ImageIterator; +use pyo3::prelude::*; + +#[pyclass(name = "ExpressionRangeIterator")] +pub struct PythonExpressionRangeIterator { + iter: ImageIterator, +} + +#[pymethods] +impl PythonExpressionRangeIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option { + slf.iter.next() + } +} + +impl From> for PythonExpressionRangeIterator { + fn from(value: ImageIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/range_table.rs b/src/bindings/iterators/range_table.rs new file mode 100644 index 0000000..90f5d33 --- /dev/null +++ b/src/bindings/iterators/range_table.rs @@ -0,0 +1,23 @@ +use crate::table::iterators::ImageIterator; +use pyo3::prelude::*; + +#[pyclass(name = "TableRangeIterator")] +pub struct PythonTableRangeIterator { + iter: ImageIterator, +} + +#[pymethods] +impl PythonTableRangeIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option { + slf.iter.next() + } +} + +impl From for PythonTableRangeIterator { + fn from(value: ImageIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/relation_bdd.rs b/src/bindings/iterators/relation_bdd.rs new file mode 100644 index 0000000..ed79d87 --- /dev/null +++ b/src/bindings/iterators/relation_bdd.rs @@ -0,0 +1,26 @@ +use crate::bdd::iterators::ImageIterator; +use crate::iterators::DomainIterator; +use pyo3::prelude::*; +use std::iter::Zip; + +#[pyclass(name = "BddRelationIterator")] +pub struct PythonBddRelationIterator { + iter: Zip, +} + +#[pymethods] +impl PythonBddRelationIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option<(Vec, bool)> { + slf.iter.next() + } +} + +impl From> for PythonBddRelationIterator { + fn from(value: Zip) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/relation_expression.rs b/src/bindings/iterators/relation_expression.rs new file mode 100644 index 0000000..a64a24d --- /dev/null +++ b/src/bindings/iterators/relation_expression.rs @@ -0,0 +1,24 @@ +use crate::iterators::RelationIterator; +use pyo3::prelude::*; + +#[pyclass(name = "ExpressionRelationIterator")] +pub struct PythonExpressionRelationIterator { + iter: RelationIterator, +} + +#[pymethods] +impl PythonExpressionRelationIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option<(Vec, bool)> { + slf.iter.next() + } +} + +impl From> for PythonExpressionRelationIterator { + fn from(value: RelationIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/relation_table.rs b/src/bindings/iterators/relation_table.rs new file mode 100644 index 0000000..bd9a3d9 --- /dev/null +++ b/src/bindings/iterators/relation_table.rs @@ -0,0 +1,24 @@ +use crate::table::iterators::RelationIterator; +use pyo3::prelude::*; + +#[pyclass(name = "TableRelationIterator")] +pub struct PythonTableRelationIterator { + iter: RelationIterator, +} + +#[pymethods] +impl PythonTableRelationIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option<(Vec, bool)> { + slf.iter.next() + } +} + +impl From for PythonTableRelationIterator { + fn from(value: RelationIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/support_bdd.rs b/src/bindings/iterators/support_bdd.rs new file mode 100644 index 0000000..88a1bb9 --- /dev/null +++ b/src/bindings/iterators/support_bdd.rs @@ -0,0 +1,24 @@ +use crate::bdd::iterators::SupportIterator; +use pyo3::prelude::*; + +#[pyclass(name = "BddSupportIterator")] +pub struct PythonBddSupportIterator { + iter: SupportIterator, +} + +#[pymethods] +impl PythonBddSupportIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option> { + slf.iter.next() + } +} + +impl From for PythonBddSupportIterator { + fn from(value: SupportIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/support_expression.rs b/src/bindings/iterators/support_expression.rs new file mode 100644 index 0000000..4c159c3 --- /dev/null +++ b/src/bindings/iterators/support_expression.rs @@ -0,0 +1,24 @@ +use crate::iterators::SupportIterator; +use pyo3::prelude::*; + +#[pyclass(name = "ExpressionSupportIterator")] +pub struct PythonExpressionSupportIterator { + iter: SupportIterator, +} + +#[pymethods] +impl PythonExpressionSupportIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option> { + slf.iter.next() + } +} + +impl From> for PythonExpressionSupportIterator { + fn from(value: SupportIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/iterators/support_table.rs b/src/bindings/iterators/support_table.rs new file mode 100644 index 0000000..eb77edd --- /dev/null +++ b/src/bindings/iterators/support_table.rs @@ -0,0 +1,24 @@ +use crate::table::iterators::SupportIterator; +use pyo3::prelude::*; + +#[pyclass(name = "TableSupportIterator")] +pub struct PythonTableSupportIterator { + iter: SupportIterator, +} + +#[pymethods] +impl PythonTableSupportIterator { + fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> { + slf + } + + fn __next__(mut slf: PyRefMut<'_, Self>) -> Option> { + slf.iter.next() + } +} + +impl From for PythonTableSupportIterator { + fn from(value: SupportIterator) -> Self { + Self { iter: value } + } +} diff --git a/src/bindings/mod.rs b/src/bindings/mod.rs index f869a10..631602f 100644 --- a/src/bindings/mod.rs +++ b/src/bindings/mod.rs @@ -1,11 +1,13 @@ mod bdd; mod error; mod expression; +mod iterators; mod table; use crate::bindings::bdd::PythonBdd; use crate::bindings::expression::PythonExpression; use crate::bindings::table::PythonTruthTable; +use crate::table::display_formatted::{TableBooleanFormatting, TableStyle}; use pyo3::prelude::*; /// A Python module implemented in Rust. The name of this function must match @@ -16,5 +18,12 @@ fn biodivine_boolean_functions(m: &Bound<'_, PyModule>) -> PyResult<()> { m.add_class::()?; m.add_class::()?; m.add_class::()?; + + m.add_class::()?; + m.add_class::()?; + + m.add_function(wrap_pyfunction!(crate::bindings::expression::var, m)?)?; + m.add_function(wrap_pyfunction!(crate::bindings::expression::vars, m)?)?; + m.add_function(wrap_pyfunction!(crate::bindings::expression::bool, m)?)?; Ok(()) } diff --git a/src/bindings/table.rs b/src/bindings/table.rs index 4be740b..0d5cb3b 100644 --- a/src/bindings/table.rs +++ b/src/bindings/table.rs @@ -1,13 +1,22 @@ -use std::collections::{BTreeMap, BTreeSet, HashMap}; +use num_bigint::BigUint; +use std::collections::{BTreeMap, BTreeSet}; +use crate::bdd::Bdd; +use crate::bindings::bdd::PythonBdd; use pyo3::PyResult; use crate::bindings::error::PythonExpressionError::UnknownVariableWhileEvaluating; use crate::bindings::expression::PythonExpression; +use crate::bindings::iterators::{ + PythonDomainIterator, PythonTableRangeIterator, PythonTableRelationIterator, + PythonTableSupportIterator, +}; use crate::expressions::Expression as RustExpression; use crate::table::display_formatted::{TableBooleanFormatting, TableStyle}; use crate::table::TruthTable; -use crate::traits::{BooleanFunction, Evaluate, GatherLiterals, SemanticEq}; +use crate::traits::{ + BooleanFunction, BooleanPoint, BooleanValuation, Evaluate, GatherLiterals, SemanticEq, +}; #[pyo3::pyclass(frozen, name = "Table")] #[derive(Clone, Debug, Eq, PartialEq)] @@ -15,20 +24,26 @@ pub struct PythonTruthTable { root: TruthTable, } -#[pyo3::pymethods] -impl PythonTruthTable { - #[staticmethod] - pub fn from_expression(expression: &PythonExpression) -> Self { - let rust_expression: RustExpression = expression.into(); - let rust_table: TruthTable = rust_expression.into(); +impl From> for PythonTruthTable { + fn from(value: TruthTable) -> Self { + PythonTruthTable::new(value) + } +} - Self::new(rust_table) +impl From for TruthTable { + fn from(value: PythonTruthTable) -> Self { + (&value).into() } +} - pub fn to_expression_trivial(&self) -> PythonExpression { - self.root.to_expression_trivial().into() +impl From<&PythonTruthTable> for TruthTable { + fn from(value: &PythonTruthTable) -> Self { + value.root.clone() } +} +#[pyo3::pymethods] +impl PythonTruthTable { pub fn to_string_formatted( &self, style: TableStyle, @@ -52,8 +67,8 @@ impl PythonTruthTable { } /// Variables not in the dictionary default to false. - pub fn evaluate_safe(&self, literal_values: BTreeMap) -> PyResult { - Ok(self.root.evaluate(&literal_values)) + pub fn evaluate_safe(&self, literal_values: BTreeMap) -> bool { + self.root.evaluate(&literal_values) } /// Variables not in the dictionary defaults to the passed `default_value` argument. @@ -61,10 +76,9 @@ impl PythonTruthTable { &self, literal_values: BTreeMap, default_value: bool, - ) -> PyResult { - Ok(self - .root - .evaluate_with_default(&literal_values, default_value)) + ) -> bool { + self.root + .evaluate_with_default(&literal_values, default_value) } pub fn semantic_eq(&self, other: &Self) -> bool { @@ -115,12 +129,223 @@ impl PythonTruthTable { PythonTruthTable::new(&left.root ^ &right.root) } - fn substitute(&self, mapping: HashMap) -> Self { - let mapping = mapping - .iter() - .map(|(a, b)| (a.clone(), b.root.clone())) - .collect::>(); - PythonTruthTable::new(self.root.substitute(&mapping)) + #[staticmethod] + pub fn mk_not(left: &Self) -> Self { + PythonTruthTable::new(!&left.root) + } + + /// A set of all the variable instances that (syntactically) appear in this Boolean + /// function. + /// + /// See also [BooleanFunction::essential_inputs]. + /// + /// ### Examples + /// + /// The inputs of the expression `(a & b) => (c | !c)` are `{a, b, c}`. + /// + /// ### Implementation notes + /// + /// This operation should be at worst `O(|F|)` for any function representation. + fn inputs(&self) -> BTreeSet { + self.root.inputs() + } + + /// A set of all variable instances that are *essential* in this Boolean function. + /// + /// Intuitively, a variable `v` is essential in function `F` if `v` has some observable + /// impact on the output of `F`. In other words, there is some input vector `X` such that + /// `F(X[v=0]) != F(X[v=1])` (here `X[v=b]` denotes a copy of `X` with the value of `v` + /// fixed to `b`). + /// + /// For a proper formal definition, see for example the introduction in + /// [this paper](https://arxiv.org/pdf/0812.1979.pdf). + /// + /// See also [BooleanFunction::inputs]. + /// + /// ### Examples + /// + /// The essential inputs of the expression `(a & b) => (c | !c)` are `{}`, because + /// this expression is a tautology. + /// + /// ### Implementation notes + /// + /// * BDD: The operation takes `O(|F|)` time by scanning the variables stored in the + /// BDD nodes. + /// * Table: The operation takes `O(n * |F|)` time by scanning the corresponding output + /// pairs for each variable. + /// * Expression: The operation is non-trivial, as we need to determine for each variable + /// whether `F[v = 0]` and `F[v = 1]` are semantically equal. + /// + fn essential_inputs(&self) -> BTreeSet { + self.root.essential_inputs() + } + + /// The number of variables that (syntactically) appear in this Boolean function. + /// + /// This is equivalent to the length of [BooleanFunction::inputs]. + fn degree(&self) -> usize { + self.root.degree() + } + + /// The number of variables that are essential in this Boolean function. + /// + /// This is equivalent to the length of [BooleanFunction::essential_inputs]. + fn essential_degree(&self) -> usize { + self.root.essential_degree() + } + + /// The iterator over Boolean points that are valid as inputs for this Boolean function. + /// + /// This is always the complete space of `2^n` Boolean vectors. + fn domain(&self) -> PythonDomainIterator { + self.root.domain().into() + } + + /// The iterator over all the output values of this Boolean function. + /// + /// The iteration order should correspond to the elements of [BooleanFunction::domain]. + fn image(&self) -> PythonTableRangeIterator { + self.root.image().into() + } + + /// The combined iterator of all input points together with their corresponding outputs. + /// + /// See also [BooleanFunction::domain] and [BooleanFunction::image]. + fn relation(&self) -> PythonTableRelationIterator { + self.root.relation().into() + } + + /// The iterator over all Boolean points for which this function evaluates to `1`. + fn support(&self) -> PythonTableSupportIterator { + self.root.support().into() + } + + /// The number of input points for which this function evaluates to `1`. + /// + /// See also [BooleanFunction::support]. + fn weight(&self) -> BigUint { + self.root.weight() + } + + /// Create a Boolean function that is a restriction of this function for the given variables. + /// + /// A restriction fixes all variables specified by the `valuation` to their respective + /// constant values. That is, the resulting function no longer depends on these variables. + /// + /// ### Examples + /// + /// A Boolean expression `(a | b) & c` restricted to `{ a: 0, c: 1 }` is `(false | b) & true` + /// semantically equal to `b`. + /// + /// ### Implementation notes + /// + /// It is not an error to supply a valuation that also fixes variables that are not the inputs + /// of this function. Such variables are simply ignored. + fn restrict(&self, valuation: BooleanValuation) -> Self { + self.root.restrict(&valuation).into() + } + + /// Create a Boolean function in which the variables specified by `mapping` are substituted + /// for their supplied functions. + /// + /// ### Examples + /// + /// Substituting `a` for `(a | b | c)` in the expression `a & !c` produces `(a | b | c) & !c`. + /// + /// ### Implementation notes + /// + /// Note that the same variable can be substituted and at the same time appear in one of the + /// substituted functions (as in the example). Also note that this operation can increase the + /// degree of a function if the substituted functions contain previously unused variables. + fn substitute(&self, mapping: BTreeMap) -> Self { + self.root + .substitute(&BTreeMap::from_iter( + mapping.into_iter().map(|(k, v)| (k, v.root)), + )) + .into() + } + + /// Produce one [BooleanPoint] for which this function evaluates to `1`, i.e. one of the + /// points in [BooleanFunction::support]. + /// + /// This value should be deterministic, but otherwise can be arbitrary. Returns `None` if + /// the function is not satisfiable. + /// + /// ### Implementation notes + /// + /// This operation is `O(|F|)` for tables, `O(1)` for BDDs, and NP-complete for expressions. + fn sat_point(&self) -> Option { + self.root.sat_point() + } + + /// Eliminate the specified `variables` using *existential* quantification. The resulting + /// function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] | F[v = 1]`. In other words, the resulting + /// function is satisfied for input `x` if there *exists* a value `b` of `v` such that the + /// original function was satisfied for `x[v=b]`. + /// + fn existential_quantification(&self, variables: BTreeSet) -> Self { + self.root.existential_quantification(variables).into() + } + + /// Eliminate the specified `variables` using *universal* quantification. The resulting + /// function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] & F[v = 1]`. In other words, the resulting + /// function is satisfied for `x` if the original function was satisfied for both `x[v=0]` + /// and `x[v=1]`. + /// + fn universal_quantification(&self, variables: BTreeSet) -> Self { + self.root.universal_quantification(variables).into() + } + + /// Computes the derivative of this function with respect to the given `variables`. + /// The resulting function does not depend on any of the eliminated variables. + /// + /// For each variable, this computes `F = F[v = 0] ^ F[v = 1]`. In other words, the resulting + /// function is satisfied for `x`, if the values of `F(x[v=0])` and `F(x[v=1])` are different. + /// (Hence the name "derivative": the result is a function that is true for all inputs in + /// which the input function can change its value). + /// + fn derivative(&self, variables: BTreeSet) -> Self { + self.root.derivative(variables).into() + } + + /// Returns `true` if the two functions are *semantically* equivalent. That is, they output + /// the same values for the same inputs. + fn is_equivalent(&self, other: &Self) -> bool { + self.root.is_equivalent(&other.root) + } + + /// Returns `true` if this function is *implied* by the `other` function. That is, it outputs + /// `1` *at least* for those inputs where `other` outputs one. + fn is_implied_by(&self, other: &Self) -> bool { + self.root.is_implied_by(&other.root) + } + + #[staticmethod] + pub fn from_expression(expression: &PythonExpression) -> Self { + let rust_expression: RustExpression = expression.into(); + let rust_table: TruthTable = rust_expression.into(); + + rust_table.into() + } + + #[staticmethod] + pub fn from_bdd(expression: &PythonBdd) -> Self { + let rust_expression: Bdd = expression.into(); + let rust_table: TruthTable = rust_expression.into(); + + rust_table.into() + } + + pub fn to_expression(&self) -> PythonExpression { + PythonExpression::from_table(self) + } + + pub fn to_bdd(&self) -> PyResult { + PythonBdd::from_table(self) } } diff --git a/src/expressions/structs/expression.rs b/src/expressions/structs/expression.rs index 5b04ca2..fde07d5 100644 --- a/src/expressions/structs/expression.rs +++ b/src/expressions/structs/expression.rs @@ -87,6 +87,15 @@ impl Expression { } } + pub fn is_nnf(&self) -> bool { + match self.node() { + Literal(_) => true, + Constant(_) => false, + Not(e) => matches!(e.node(), Literal(..)), + And(es) | Or(es) => es.iter().all(|e| e.is_nnf()), + } + } + // let rec cnfc (phi: formula_wi) : formula_wi // = match phi with // | FOr_wi phi1 phi2 → distr (cnfc phi1) (cnfc phi2) @@ -100,32 +109,26 @@ impl Expression { Or(es) => es .iter() .map(|e| e.to_cnf()) - .reduce(|acc, e| Expression::distribute(&acc, &e)) + .reduce(|acc, e| Expression::distribute_cnf(&acc, &e)) .unwrap(), And(es) => And(es.iter().map(|e| e.to_cnf()).collect()).into(), _other => nnf, } } - // let rec distr (phi1 phi2: formula_wi) : formula_wi - // = match phi1, phi2 with - // | FAnd_wi and1 and2, phi2 → FAnd_wi (distr and1 phi2) (distr and2 phi2) - // | phi1, FAnd_wi and1 and2 → FAnd_wi (distr phi1 and1) (distr phi1 and2) - // | phi1,phi2 → FOr_wi phi1 phi2 - // end - fn distribute(first: &Self, second: &Self) -> Self { + fn distribute_cnf(first: &Self, second: &Self) -> Self { match (first.node(), second.node()) { (And(es), _) => { let es = es .iter() - .map(|e| Expression::distribute(e, second)) + .map(|e| Expression::distribute_cnf(e, second)) .collect(); And(es).into() } (_, And(es)) => { let es = es .iter() - .map(|e| Expression::distribute(first, e)) + .map(|e| Expression::distribute_cnf(first, e)) .collect(); And(es).into() } @@ -143,6 +146,50 @@ impl Expression { } } + pub fn to_dnf(&self) -> Self { + let nnf = self.to_nnf(); + + match nnf.node() { + And(es) => es + .iter() + .map(|e| e.to_dnf()) + .reduce(|acc, e| Expression::distribute_dnf(&acc, &e)) + .unwrap(), + Or(es) => Or(es.iter().map(|e| e.to_dnf()).collect()).into(), + _other => nnf, + } + } + + fn distribute_dnf(first: &Self, second: &Self) -> Self { + match (first.node(), second.node()) { + (Or(es), _) => { + let es = es + .iter() + .map(|e| Expression::distribute_dnf(e, second)) + .collect(); + Or(es).into() + } + (_, Or(es)) => { + let es = es + .iter() + .map(|e| Expression::distribute_dnf(first, e)) + .collect(); + Or(es).into() + } + (_e1, _e2) => Expression::binary_and(first, second), + } + } + + pub fn is_dnf(&self) -> bool { + match self.node() { + Literal(_) => true, + Constant(_) => false, + Not(inner) => matches!(inner.node(), Literal(_)), + Or(es) => es.iter().all(|e| e.is_dnf()), + And(es) => !es.iter().any(|e| e.is_or()) && es.iter().all(|e| e.is_dnf()), + } + } + pub fn rename_literals(&self, mapping: &BTreeMap) -> Self { match self.node() { Literal(name) => Literal(mapping.get(name).unwrap_or(name).clone()), @@ -190,6 +237,7 @@ pub mod tests { let actual = input.to_nnf(); assert!(expected.semantic_eq(&actual)); + assert!(actual.is_nnf()); } #[test] @@ -200,16 +248,18 @@ pub mod tests { let actual = input.to_nnf(); assert!(expected.semantic_eq(&actual)); + assert!(actual.is_nnf()); } #[test] - fn test_to_nnn_3() { + fn test_to_nnf_3() { // Not (notA ∨ vB) ∨ Not (vB ∧ notC), (vA ∧ notB) ∨ (notB ∨ vC) let input = !(!var("a") | var("b")) | !(var("b") & !var("c")); let expected = (var("a") & !var("b")) | !var("b") | var("c"); let actual = input.to_nnf(); assert!(expected.semantic_eq(&actual)); + assert!(actual.is_nnf()); } #[test] @@ -218,7 +268,7 @@ pub mod tests { let input_right = var("b") & var("c"); let expected = (var("a") | var("b")) & (var("a") | var("c")); - let actual = Expression::distribute(&input_left, &input_right); + let actual = Expression::distribute_cnf(&input_left, &input_right); assert!(expected.semantic_eq(&actual)); } @@ -229,7 +279,7 @@ pub mod tests { let input_right = var("a"); let expected = (var("b") | var("a")) & (var("c") | var("a")); - let actual = Expression::distribute(&input_left, &input_right); + let actual = Expression::distribute_cnf(&input_left, &input_right); assert!(expected.semantic_eq(&actual)); } @@ -272,6 +322,35 @@ pub mod tests { assert!(actual.is_cnf()); } + #[test] + fn to_dnf_basic() { + let input = (var("a") | var("b")) & (var("b") | var("c")) & (var("a") | var("c")); + + let actual = input.to_dnf(); + let expected = (var("a") & var("b")) | (var("b") & var("c")) | (var("a") & var("c")); + + assert!(expected.semantic_eq(&actual)); + assert!(actual.is_dnf()); + println!("{actual}") + } + + #[test] + fn to_dnf_advanced() { + let input = + (var("A") | (var("B") & (var("C") | var("D")))) & (var("E") | (var("F") & !var("G"))); + + let actual = input.to_dnf(); + let expected = (var("E") & var("A")) + | (var("E") & var("B") & var("C")) + | (var("E") & var("B") & var("D")) + | (var("F") & !var("G") & var("A")) + | (var("F") & !var("G") & var("B") & var("C")) + | (var("F") & !var("G") & var("B") & var("D")); + + assert!(expected.semantic_eq(&actual)); + assert!(actual.is_dnf()); + } + #[test] fn is_cnf_levels() { // We intentionally don't use the built-in operators because they would "level" the expression. diff --git a/src/expressions/traits/operations/equality.rs b/src/expressions/traits/operations/equality.rs new file mode 100644 index 0000000..4be99ba --- /dev/null +++ b/src/expressions/traits/operations/equality.rs @@ -0,0 +1,39 @@ +use crate::expressions::Expression; +use crate::traits::Equality; +use std::fmt::Debug; + +impl Equality for Expression { + type Output = Expression; + + fn iff(self, rhs: Self) -> >::Output { + (self.clone() & rhs.clone()) | (!self & !rhs) + } +} + +#[cfg(test)] +mod tests { + use crate::expressions::{bool, var}; + use crate::traits::{Equality, SemanticEq}; + + #[test] + fn test_iff_syntactic_ok() { + let actual = var("a").iff(var("b")); + let expected_alternative_implication = (!var("a") | var("b")) & (var("a") | !var("b")); + let expected_actual_implication = (var("a") & var("b")) | (!var("a") & !var("b")); + + assert!(actual.semantic_eq(&expected_alternative_implication)); + assert_eq!(actual, expected_actual_implication); + } + + #[test] + fn test_iff_semantic_ok() { + assert!(bool(false).iff(bool(false)).semantic_eq(&bool(true))); + assert!(bool(false).iff(bool(true)).semantic_eq(&bool(false))); + assert!(bool(true).iff(bool(false)).semantic_eq(&bool(false))); + assert!(bool(true).iff(bool(true)).semantic_eq(&bool(true))); + + assert!(var("x").iff(bool(false)).semantic_eq(&!var("x"))); + assert!(bool(true).iff(var("x")).semantic_eq(&var("x"))); + assert!(var("x").iff(!var("x")).semantic_eq(&bool(false))); + } +} diff --git a/src/expressions/traits/operations/implication.rs b/src/expressions/traits/operations/implication.rs index ff8c2f8..91f4d10 100644 --- a/src/expressions/traits/operations/implication.rs +++ b/src/expressions/traits/operations/implication.rs @@ -12,11 +12,11 @@ impl Implication> for Expression { #[cfg(test)] mod tests { - use crate::expressions::var; + use crate::expressions::{bool, var}; use crate::traits::{Implication, SemanticEq}; #[test] - fn test_imply_ok() { + fn test_imply_syntactic_ok() { let actual = var("a").imply(var("b")); let expected_alternative_implication = !(var("a") & !var("b")); let expected_actual_implication = !var("a") | var("b"); @@ -24,4 +24,16 @@ mod tests { assert!(actual.semantic_eq(&expected_alternative_implication)); assert_eq!(actual, expected_actual_implication); } + + #[test] + fn test_imply_semantic_ok() { + assert!(bool(false).imply(bool(false)).semantic_eq(&bool(true))); + assert!(bool(false).imply(bool(true)).semantic_eq(&bool(true))); + assert!(bool(true).imply(bool(false)).semantic_eq(&bool(false))); + assert!(bool(true).imply(bool(true)).semantic_eq(&bool(true))); + + assert!(var("x").imply(bool(false)).semantic_eq(&!var("x"))); + assert!(bool(true).imply(var("x")).semantic_eq(&var("x"))); + assert!(!var("x").imply(var("x")).semantic_eq(&var("x"))); + } } diff --git a/src/expressions/traits/operations/mod.rs b/src/expressions/traits/operations/mod.rs index 1dd97fd..baa74b9 100644 --- a/src/expressions/traits/operations/mod.rs +++ b/src/expressions/traits/operations/mod.rs @@ -1 +1,2 @@ +mod equality; mod implication; diff --git a/src/iterators/image.rs b/src/iterators/image.rs index bdc0de7..e9feae4 100644 --- a/src/iterators/image.rs +++ b/src/iterators/image.rs @@ -1,3 +1,4 @@ +use crate::expressions::Expression; use crate::traits::{Evaluate, GatherLiterals}; use crate::utils::{boolean_point_to_valuation, row_index_to_bool_point}; use std::collections::BTreeSet; @@ -5,15 +6,15 @@ use std::fmt::Debug; pub struct ImageIterator { variables: BTreeSet, - evaluatable: Box>, + evaluatable: Expression, index: usize, } impl ImageIterator { - pub(crate) fn new(value: &(impl Evaluate + GatherLiterals + Clone + 'static)) -> Self { + pub(crate) fn new(value: &Expression) -> Self { Self { variables: value.gather_literals(), - evaluatable: Box::from(value.clone()), + evaluatable: value.clone(), index: 0, } } diff --git a/src/iterators/relation.rs b/src/iterators/relation.rs index b715ac9..656e858 100644 --- a/src/iterators/relation.rs +++ b/src/iterators/relation.rs @@ -1,3 +1,4 @@ +use crate::expressions::Expression; use crate::traits::{BooleanPoint, Evaluate, GatherLiterals}; use crate::utils::{boolean_point_to_valuation, row_index_to_bool_point}; use std::collections::BTreeSet; @@ -5,15 +6,15 @@ use std::fmt::Debug; pub struct RelationIterator { variables: BTreeSet, - evaluatable: Box>, + evaluatable: Expression, index: usize, } impl RelationIterator { - pub(crate) fn new(value: &(impl Evaluate + GatherLiterals + Clone + 'static)) -> Self { + pub(crate) fn new(value: &Expression) -> Self { Self { variables: value.gather_literals(), - evaluatable: Box::from(value.clone()), + evaluatable: value.clone(), index: 0, } } diff --git a/src/iterators/support.rs b/src/iterators/support.rs index 19e4709..2cbf191 100644 --- a/src/iterators/support.rs +++ b/src/iterators/support.rs @@ -1,3 +1,4 @@ +use crate::expressions::Expression; use crate::traits::{BooleanPoint, Evaluate, GatherLiterals}; use crate::utils::{boolean_point_to_valuation, row_index_to_bool_point}; use std::collections::BTreeSet; @@ -5,15 +6,15 @@ use std::fmt::Debug; pub struct SupportIterator { variables: BTreeSet, - evaluatable: Box>, + evaluatable: Expression, index: usize, } impl SupportIterator { - pub(crate) fn new(value: &(impl Evaluate + GatherLiterals + Clone + 'static)) -> Self { + pub(crate) fn new(value: &Expression) -> Self { Self { variables: value.gather_literals(), - evaluatable: Box::from(value.clone()), + evaluatable: value.clone(), index: 0, } } diff --git a/src/table/iterators/support.rs b/src/table/iterators/support.rs index 97b6bf0..74bad2f 100644 --- a/src/table/iterators/support.rs +++ b/src/table/iterators/support.rs @@ -4,22 +4,22 @@ use crate::utils::row_index_to_bool_point; use std::fmt::Debug; pub struct SupportIterator { - outputs: Box>, + outputs: std::vec::IntoIter, variable_count: usize, } impl From<&TruthTable> for SupportIterator { fn from(value: &TruthTable) -> Self { Self { - outputs: Box::new( - value - .outputs - .clone() - .into_iter() - .enumerate() - .filter(|(_row_index, output_is_true)| *output_is_true) - .map(|(row_index, _output_is_true)| row_index), - ), + outputs: value + .outputs + .clone() + .into_iter() + .enumerate() + .filter(|(_row_index, output_is_true)| *output_is_true) + .map(|(row_index, _output_is_true)| row_index) + .collect::>() + .into_iter(), variable_count: value.variable_count(), } } diff --git a/src/table/mod.rs b/src/table/mod.rs index 84e1179..dbdf17e 100644 --- a/src/table/mod.rs +++ b/src/table/mod.rs @@ -9,7 +9,7 @@ use crate::utils::row_index_to_bool_point; #[cfg(feature = "csv")] pub mod csv; pub mod display_formatted; -mod iterators; +pub mod iterators; pub mod traits; mod utils; diff --git a/src/traits/mod.rs b/src/traits/mod.rs index abec8db..62d18b8 100644 --- a/src/traits/mod.rs +++ b/src/traits/mod.rs @@ -1,7 +1,7 @@ pub use boolean_function::{BooleanFunction, BooleanPoint, BooleanValuation}; pub use evaluate::Evaluate; pub use gather_literals::GatherLiterals; -pub use operations::implication::Implication; +pub use operations::{equality::Equality, implication::Implication}; pub use power_set::PowerSet; pub use semantic_eq::SemanticEq; diff --git a/src/traits/operations/equality.rs b/src/traits/operations/equality.rs new file mode 100644 index 0000000..181c731 --- /dev/null +++ b/src/traits/operations/equality.rs @@ -0,0 +1,7 @@ +use std::ops::{BitOr, Not}; + +pub trait Equality: BitOr + Not { + type Output; + + fn iff(self, rhs: Rhs) -> >::Output; +} diff --git a/src/traits/operations/mod.rs b/src/traits/operations/mod.rs index b093a05..c42c44a 100644 --- a/src/traits/operations/mod.rs +++ b/src/traits/operations/mod.rs @@ -1 +1,2 @@ +pub mod equality; pub mod implication;