Skip to content

Commit

Permalink
feat(bindings): finalized bindings
Browse files Browse the repository at this point in the history
  • Loading branch information
AurumTheEnd committed May 23, 2024
1 parent 1bfbb2b commit 5d6e112
Show file tree
Hide file tree
Showing 5 changed files with 125 additions and 22 deletions.
2 changes: 1 addition & 1 deletion src/bdd/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ impl<TLiteral: Debug + Clone + Eq + Ord> Bdd<TLiteral> {
Ok(BddVariableSet::new_anonymous(num_vars))
}

pub(crate) fn inner(&self) -> &InnerBdd {
pub fn inner(&self) -> &InnerBdd {
&self.bdd
}

Expand Down
55 changes: 44 additions & 11 deletions src/bindings/bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,9 @@ use crate::bindings::iterators::{
PythonBddRangeIterator, PythonBddRelationIterator, PythonBddSupportIterator,
PythonDomainIterator,
};
use crate::bindings::table::PythonTruthTable;
use crate::expressions::Expression;
use crate::table::TruthTable;
use crate::traits::{BooleanFunction, BooleanPoint, BooleanValuation, Evaluate};

#[pyclass(frozen, name = "Bdd")]
Expand All @@ -25,19 +27,20 @@ impl From<Bdd<String>> for PythonBdd {
}
}

#[pymethods]
impl PythonBdd {
#[staticmethod]
pub fn from_expression(expression: &PythonExpression) -> PyResult<Self> {
let native: Expression<String> = 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<PythonBdd> for Bdd<String> {
fn from(value: PythonBdd) -> Self {
(&value).into()
}
}

impl From<&PythonBdd> for Bdd<String> {
fn from(value: &PythonBdd) -> Self {
value.root.clone()
}
}

#[pymethods]
impl PythonBdd {
#[staticmethod]
pub fn mk_not(inner: &PythonBdd) -> PythonBdd {
PythonBdd::new(!(&inner.root))
Expand Down Expand Up @@ -293,6 +296,36 @@ impl PythonBdd {
fn is_implied_by(&self, other: &Self) -> bool {
self.root.is_implied_by(&other.root)
}

#[staticmethod]
pub fn from_expression(expression: &PythonExpression) -> PyResult<Self> {
let native: Expression<String> = 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<Self> {
let native: TruthTable<String> = 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 {
Expand Down
40 changes: 40 additions & 0 deletions src/bindings/expression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ use num_bigint::BigUint;
use std::collections::{BTreeMap, BTreeSet};
use std::str::FromStr;

use crate::bdd::Bdd;
use crate::bindings::bdd::PythonBdd;
use pyo3::prelude::{pyclass, pyfunction, pymethods, PyAny, PyAnyMethods, PyResult};
use pyo3::Bound;

Expand All @@ -11,7 +13,9 @@ 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,
};
Expand Down Expand Up @@ -152,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))
Expand Down Expand Up @@ -373,6 +389,30 @@ impl PythonExpression {
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<String> = table.into();
let rust_expression: Expression<String> = rust_table.to_expression_trivial();

Self::new(rust_expression)
}

#[staticmethod]
pub fn from_bdd(bdd: &PythonBdd) -> Self {
let rust_table: Bdd<String> = bdd.into();
let rust_expression: Expression<String> = rust_table.into();

Self::new(rust_expression)
}

fn to_table(&self) -> PythonTruthTable {
PythonTruthTable::from_expression(self)
}

fn to_bdd(&self) -> PyResult<PythonBdd> {
PythonBdd::from_expression(self)
}
}

impl PythonExpression {
Expand Down
4 changes: 4 additions & 0 deletions src/bindings/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ 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
Expand All @@ -18,6 +19,9 @@ fn biodivine_boolean_functions(m: &Bound<'_, PyModule>) -> PyResult<()> {
m.add_class::<PythonTruthTable>()?;
m.add_class::<PythonBdd>()?;

m.add_class::<TableStyle>()?;
m.add_class::<TableBooleanFormatting>()?;

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)?)?;
Expand Down
46 changes: 36 additions & 10 deletions src/bindings/table.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
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;
Expand Down Expand Up @@ -28,20 +30,20 @@ impl From<TruthTable<String>> for PythonTruthTable {
}
}

#[pyo3::pymethods]
impl PythonTruthTable {
#[staticmethod]
pub fn from_expression(expression: &PythonExpression) -> Self {
let rust_expression: RustExpression<String> = expression.into();
let rust_table: TruthTable<String> = rust_expression.into();

Self::new(rust_table)
impl From<PythonTruthTable> for TruthTable<String> {
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<String> {
fn from(value: &PythonTruthTable) -> Self {
value.root.clone()
}
}

#[pyo3::pymethods]
impl PythonTruthTable {
pub fn to_string_formatted(
&self,
style: TableStyle,
Expand Down Expand Up @@ -321,6 +323,30 @@ impl PythonTruthTable {
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<String> = expression.into();
let rust_table: TruthTable<String> = rust_expression.into();

rust_table.into()
}

#[staticmethod]
pub fn from_bdd(expression: &PythonBdd) -> Self {
let rust_expression: Bdd<String> = expression.into();
let rust_table: TruthTable<String> = rust_expression.into();

rust_table.into()
}

pub fn to_expression(&self) -> PythonExpression {
PythonExpression::from_table(self)
}

pub fn to_bdd(&self) -> PyResult<PythonBdd> {
PythonBdd::from_table(self)
}
}

impl PythonTruthTable {
Expand Down

0 comments on commit 5d6e112

Please sign in to comment.