Skip to main content

Library for folding (or reducing) over a Reduced Ordered Binary Decision Diagram.

Project description

Fold-BDD

Library for folding (or reducing) over a Reduced Ordered Binary Decision Diagram.

Build Status codecov PyPI version License: MIT

Table of Contents

Installation

If you just need to use fold_bdd, you can just run:

$ pip install fold-bdd

For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:

$ poetry install

Usage

The fold-bdd library supports two types of folds:

  1. Folding over the DAG of a BDD starting at the root and then recursively merging the low and high branches until the True/False leaves. This is simply a compressed variant of a post-order traversal.

  2. Folding over a path in the DAG, starting at the root and moving the the corresponding leaf (left fold).

In both cases, local context such as the levels of the parent and child nodes are passed in.

As input, each of these take in a bdd, from the dd library and function for accumulating or merging.

The following example illustrates how to use fold_bdd to count the number of solutions to a predicate using post_order and evaluate a path using fold_path.

Create ROBDD

# Create BDD.
from dd.cudd import BDD

manager = BDD()
manager.declare('x', 'y')
manager.reorder({'x': 1, 'y': 0})
manger.configure(reordering=False)

bexpr = manager.add_expr('x | y')

Post-Order Examples

from fold_bdd import post_order

Count Number of Nodes in BDD

def merge1(ctx, low=None, high=None):
    return 1 if low is None else low + high

def dag_size(bexpr):
    return post_order(bexpr, merge1)

assert bexpr.dag_size == dag_size(bexpr)

Fold Path Examples

Count nodes along path.

def merge(ctx, val, acc):
    return acc + 1

def count_nodes(bexpr, vals):
    return fold_path(merge, bexpr, vals, initial=0)

assert count_nodes(bexpr, (False, False)) == 3
assert count_nodes(bexpr, (True, False)) == 2

Context Object Attributes

The Context object contains exposes attributes

  • node: Hashable # Reference to Node in ROBDD.
  • node_val: Union[str, bool] # Node name or leaf value.
  • negated: bool # Is the edge to prev node negated.
  • first_lvl: int # Level of first decision in ROBDD.
  • max_lvl: int # How many decision variables are there.
  • curr_lvl: int # Which decision is this.
  • low_lvl: Optional[int] # Which decision does the False edge point to. None if leaf.
  • high_lvl: Optional[int] # Which decision does the True edge point to. None if leaf.
  • is_leaf: bool # Is the current node a leaf.
  • skipped: int # How many decisions were skipped on edge to this node.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

fold-bdd-0.6.0.tar.gz (5.7 kB view hashes)

Uploaded Source

Built Distribution

fold_bdd-0.6.0-py3-none-any.whl (5.9 kB view hashes)

Uploaded Python 3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page