Cudd.Cudd

Bindings to the CUDD BDD library

This is a straightforward wrapper around the C library. See http://vlsi.colorado.edu/~fabio/CUDD/ for documentation.

Exampe usage:

import Cudd.Cudd

main = do
    let manager = cuddInit
        v1      = ithVar manager 0
        v2      = ithVar manager 1
        conj    = bAnd manager v1 v2
        implies = lEq manager conj v1
    print implies

Documentation

newtype DDManager

Constructors

DDManager (Ptr CDDManager)

newtype DDNode

Constructors

DDNode

Fields

• unDDNode :: ForeignPtr CDDNode

Instances

Eq DDNode

Methods

(==) :: DDNode -> DDNode -> Bool

(/=) :: DDNode -> DDNode -> Bool

Ord DDNode

Methods

compare :: DDNode -> DDNode -> Ordering

(<) :: DDNode -> DDNode -> Bool

(<=) :: DDNode -> DDNode -> Bool

(>) :: DDNode -> DDNode -> Bool

(>=) :: DDNode -> DDNode -> Bool

max :: DDNode -> DDNode -> DDNode

min :: DDNode -> DDNode -> DDNode

Show DDNode

Methods

showsPrec :: Int -> DDNode -> ShowS

show :: DDNode -> String

showList :: [DDNode] -> ShowS

deref :: FunPtr (Ptr CDDManager -> Ptr CDDNode -> IO ())

cuddInit :: DDManager

cuddInitOrder :: [Int] -> DDManager

readOne :: DDManager -> DDNode

readLogicZero :: DDManager -> DDNode

ithVar :: DDManager -> Int -> DDNode

bAnd :: DDManager -> DDNode -> DDNode -> DDNode

bOr :: DDManager -> DDNode -> DDNode -> DDNode

bNand :: DDManager -> DDNode -> DDNode -> DDNode

bNor :: DDManager -> DDNode -> DDNode -> DDNode

bXor :: DDManager -> DDNode -> DDNode -> DDNode

bXnor :: DDManager -> DDNode -> DDNode -> DDNode

bNot :: DDManager -> DDNode -> DDNode

dumpDot' :: DDManager -> [DDNode] -> Maybe [String] -> Maybe [String] -> Ptr CFile -> IO Int

dumpDot :: DDManager -> DDNode -> String -> IO Int

cudd_cache_slots :: Int

cudd_unique_slots :: Int

eval :: DDManager -> DDNode -> [Int] -> Bool

printMinterm :: DDManager -> DDNode -> IO ()

allSat :: DDManager -> DDNode -> [[SatBit]]

oneSat :: DDManager -> DDNode -> Maybe [SatBit]

onePrime :: DDManager -> DDNode -> DDNode -> Maybe [Int]

supportIndex :: DDManager -> DDNode -> [Bool]

bExists :: DDManager -> DDNode -> DDNode -> DDNode

bForall :: DDManager -> DDNode -> DDNode -> DDNode

bIte :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode

permute :: DDManager -> DDNode -> [Int] -> DDNode

swapVariables :: DDManager -> DDNode -> [DDNode] -> [DDNode] -> DDNode

nodeReadIndex :: DDNode -> Int

dagSize :: DDNode -> Int

indicesToCube :: DDManager -> [Int] -> DDNode

liCompaction :: DDManager -> DDNode -> DDNode -> DDNode

minimize :: DDManager -> DDNode -> DDNode -> DDNode

readSize :: DDManager -> Int

xEqY :: DDManager -> [DDNode] -> [DDNode] -> DDNode

xGtY :: DDManager -> [DDNode] -> [DDNode] -> DDNode

interval :: DDManager -> [DDNode] -> Int -> Int -> DDNode

disequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode

inequality :: DDManager -> Int -> Int -> [DDNode] -> [DDNode] -> DDNode

ddNodeToInt :: Integral i => DDNode -> i

pickOneMinterm :: DDManager -> DDNode -> [DDNode] -> Maybe DDNode

readPerm :: DDManager -> Int -> Int

readInvPerm :: DDManager -> Int -> Int

readPerms :: DDManager -> [Int]

readInvPerms :: DDManager -> [Int]

readTree :: DDManager -> IO (Ptr CMtrNode)

countLeaves :: DDNode -> Int

countMinterm :: DDManager -> DDNode -> Int -> Double

countPath :: DDNode -> Double

countPathsToNonZero :: DDNode -> Double

printDebug :: DDManager -> DDNode -> Int -> Int -> IO Int

andAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode

xorExistAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode

transfer :: DDManager -> DDManager -> DDNode -> DDNode

makePrime :: DDManager -> DDNode -> DDNode -> DDNode

constrain :: DDManager -> DDNode -> DDNode -> DDNode

restrict :: DDManager -> DDNode -> DDNode -> DDNode

squeeze :: DDManager -> DDNode -> DDNode -> DDNode

data SatBit

Constructors

Zero

One

DontCare

Instances

Eq SatBit

Methods

(==) :: SatBit -> SatBit -> Bool

(/=) :: SatBit -> SatBit -> Bool

largestCube :: DDManager -> DDNode -> (Int, DDNode)

lEq :: DDManager -> DDNode -> DDNode -> Bool

printInfo :: DDManager -> Ptr CFile -> IO Int