README.md

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

   [dependencies]
   biodivine-boolean-functions = { git = "https://github.com/sybila/biodivine-boolean-functions" }

2. Use from 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.

   $ bash ./scripts/local_dev.sh

3. Use from 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())