Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Forgotten misc changes #29

Merged
merged 22 commits into from
May 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
45e3eab
refactor(expression): renamed distribute to distribute_cnf
AurumTheEnd May 8, 2024
a81f0c6
chore: added license
AurumTheEnd May 14, 2024
b3142fa
feat(expression): added and implemented Equality trait for Expression
AurumTheEnd May 20, 2024
a21b532
feat(expression): added semantic test for Implication
AurumTheEnd May 20, 2024
24db97d
feat(expression): added to_dnf and is_dnf
AurumTheEnd May 9, 2024
a352762
chore(build): updated dev script to determine script location
AurumTheEnd May 21, 2024
c681f5b
feat(expressions): added is_nnf
AurumTheEnd May 21, 2024
ffbd4a1
revert(expressions): partially reverted dynamic dispatch changeset fr…
AurumTheEnd May 21, 2024
262b5b5
feat(bindings): added Python iterator wrappers for expressions
AurumTheEnd May 21, 2024
914eecf
feat(bindings): added utility expression constructor functions
AurumTheEnd May 21, 2024
033a7da
feat(bindings): hopefully finalized Python expression API
AurumTheEnd May 21, 2024
0500a37
fix(bindings): removed unused results from Table's pymethods
AurumTheEnd May 21, 2024
fc6b659
build: bumped dependencies version
AurumTheEnd May 21, 2024
acbc142
refactor(table)!: restructured support iterator to not use Box
AurumTheEnd May 21, 2024
ebd4224
feat(bindings): added Python iterator wrappers for tables
AurumTheEnd May 21, 2024
8af43a7
feat(bindings): hopefully finalized Python table API
AurumTheEnd May 21, 2024
e61dd91
refactor(bdd)!: restructured image iterator to not use Box
AurumTheEnd May 21, 2024
24418df
feat(bindings): added Python iterator wrappers for bdds
AurumTheEnd May 21, 2024
bfe12b2
feat(bindings): hopefully finalized Python bdd API
AurumTheEnd May 21, 2024
1bfbb2b
fix(bindings): removed unused results from expression's pymethods
AurumTheEnd May 21, 2024
5d6e112
feat(bindings): finalized bindings
AurumTheEnd May 22, 2024
a408f44
feat(bindings): finalized README
AurumTheEnd May 22, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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