Skip to content

Commit

Permalink
Misc changes (#29)
Browse files Browse the repository at this point in the history
  • Loading branch information
AurumTheEnd authored May 23, 2024
1 parent 7f9d435 commit 361a59b
Show file tree
Hide file tree
Showing 33 changed files with 1,394 additions and 89 deletions.
7 changes: 4 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
21 changes: 21 additions & 0 deletions LICENSE
Original file line number Diff line number Diff line change
@@ -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.
114 changes: 114 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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<String> = 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<String> = 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())
```

10 changes: 10 additions & 0 deletions scripts/local_dev.sh
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
4 changes: 2 additions & 2 deletions src/bdd/iterators/image.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,14 @@ use biodivine_lib_bdd::Bdd;
use biodivine_lib_bdd::BddValuation;

pub struct ImageIterator {
domain_iterator: Box<dyn Iterator<Item = Vec<bool>>>,
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(),
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/bdd/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down 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
Loading

0 comments on commit 361a59b

Please sign in to comment.