| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.HasCacBDD
Description
Haskell bindings for CacBDD, a BDD Package with Dynamic Cache Management.
Synopsis
- data Bdd
- type Assignment = [(Int, Bool)]
- top :: Bdd
- bot :: Bdd
- var :: Int -> Bdd
- neg :: Bdd -> Bdd
- con :: Bdd -> Bdd -> Bdd
- dis :: Bdd -> Bdd -> Bdd
- imp :: Bdd -> Bdd -> Bdd
- equ :: Bdd -> Bdd -> Bdd
- xor :: Bdd -> Bdd -> Bdd
- conSet :: [Bdd] -> Bdd
- disSet :: [Bdd] -> Bdd
- xorSet :: [Bdd] -> Bdd
- exists :: Int -> Bdd -> Bdd
- forall :: Int -> Bdd -> Bdd
- forallSet :: [Int] -> Bdd -> Bdd
- existsSet :: [Int] -> Bdd -> Bdd
- restrict :: Bdd -> (Int, Bool) -> Bdd
- restrictSet :: Bdd -> Assignment -> Bdd
- restrictLaw :: Bdd -> Bdd -> Bdd
- ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
- gfp :: (Bdd -> Bdd) -> Bdd
- relabel :: [(Int, Int)] -> Bdd -> Bdd
- relabelFun :: (Int -> Int) -> Bdd -> Bdd
- substit :: Int -> Bdd -> Bdd -> Bdd
- substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd
- evaluate :: Bdd -> Assignment -> Maybe Bool
- evaluateFun :: Bdd -> (Int -> Bool) -> Bool
- allSats :: Bdd -> [Assignment]
- allSatsWith :: [Int] -> Bdd -> [Assignment]
- satCountWith :: [Int] -> Bdd -> Int
- anySat :: Bdd -> Maybe Assignment
- anySatWith :: [Int] -> Bdd -> Maybe Assignment
- firstVarOf :: Bdd -> Maybe Int
- maxVarOf :: Bdd -> Maybe Int
- allVarsOf :: Bdd -> [Int]
- allVarsOfSorted :: Bdd -> [Int]
- thenOf :: Bdd -> Bdd
- elseOf :: Bdd -> Bdd
- subsOf :: Bdd -> [Bdd]
- sizeOf :: Bdd -> Int
- data BddTree
- unravel :: Bdd -> BddTree
- ravel :: BddTree -> Bdd
- maximumvar :: Int
- showInfo :: IO ()
Types
The CacBDD datatype has no structure because from our perspective BDDs are just pointers.
type Assignment = [(Int, Bool)] Source #
An assignment of boolean values to variables/integers.
Creation of new BDDs
Variable, indexed by any integer from 0 to 1.000.000 FIXME: Segfaults if n is negative or out of range. Can we add a safety check without affecting performance?
Combination and Manipulation of BDDs
imp :: Bdd -> Bdd -> Bdd Source #
Implication, via disjunction and negation. Somehow this is faster than calling LessEqual?
restrictSet :: Bdd -> Assignment -> Bdd Source #
Restrict with a (partial) assignment
restrictLaw :: Bdd -> Bdd -> Bdd Source #
Restrict with a law. Note that the law is the second parameter!
relabel :: [(Int, Int)] -> Bdd -> Bdd Source #
Relabel variables according to the given mapping. Note that the mapping list must be sorted!
substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd Source #
Simultaneous substitution of BDDs for variables.
Note that this is not the same as folding substit.
Evaluation
evaluate :: Bdd -> Assignment -> Maybe Bool Source #
Evaluate a BDD given an assignment. Returns Nothing if the assignment does not cover allVarsOf b.
evaluateFun :: Bdd -> (Int -> Bool) -> Bool Source #
Evaluate a BDD given a total assignment function.
Get satisfying assignments
allSats :: Bdd -> [Assignment] Source #
Get all satisfying assignments. These will be partial, i.e. only contain (a subset of) the variables that actually occur in the BDD.
allSatsWith :: [Int] -> Bdd -> [Assignment] Source #
Get all complete assignments, given a set of all variables. In particular this will include variables not in the BDD.
satCountWith :: [Int] -> Bdd -> Int Source #
Given a set of all variables, get the number of satisfying assignments. Note that allvars must be nub'd and sorted.
anySat :: Bdd -> Maybe Assignment Source #
Get the lexicographically smallest satisfying assignment, if there is any.
anySatWith :: [Int] -> Bdd -> Maybe Assignment Source #
Given a set of all variables, get the lexicographically smallest complete satisfying assignment, if there is any.
Variables
allVarsOfSorted :: Bdd -> [Int] Source #
All variables in a given BDD, sorted, *not* lazy.
Sub-BDDs and length
Show and convert to trees
A simple tree definition to show BDDs as text.
Print some debugging information
maximumvar :: Int Source #
The maximum number of variables