oxidd

oxidd copied to clipboard

Variable Substitution

2

Hi, I'm trying to implement a symbolic solver using `oxidd`, but this requires some variable substitution here and there. For example, if we have the following: ```rust // Create two...

Hirtol

Implement Variable Substitution

1

Closes #10

nhusung

Symbolic `pick_cube`

1

For some model checking algorithms, one needs to be able to obtain a BDD for a single state, i.e. a single satisfying assignment. In BuDDy, these are the two functions:...

SSoelvsten

Set Operator Aliases

3

I might just be unable to find this function, but the binary *diff* operator (including operator overload for the *-* operator) is missing for `oxidd::bdd_function` and `oxidd::bcdd_function`. This operator is...

SSoelvsten

In this pull request I exposed the node level in the bdd, bcdd and zdd. Currently, this has not yet been done with a HasLevel protocol as it is done...

mlaveaux

Iterating over all satisfying assignments for a ZBDD?

2

Thank you for the oxidd package! I'm sorry if I've missed this somewhere, but is it possible to iterate over all satisfying assignments for a ZBDD with oxidd? I'm using...

johnrudge