cudd-0.1.0.4: Bindings to the CUDD binary decision diagrams library

Safe HaskellNone
LanguageHaskell2010

Cudd.Cudd

Description

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 Source #

Constructors

DDManager (Ptr CDDManager) 

newtype DDNode Source #

Constructors

DDNode 

Fields

Instances

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

cuddInit :: DDManager Source #

cuddInitOrder :: [Int] -> DDManager Source #

readOne :: DDManager -> DDNode Source #

readLogicZero :: DDManager -> DDNode Source #

ithVar :: DDManager -> Int -> DDNode Source #

bAnd :: DDManager -> DDNode -> DDNode -> DDNode Source #

bOr :: DDManager -> DDNode -> DDNode -> DDNode Source #

bNand :: DDManager -> DDNode -> DDNode -> DDNode Source #

bNor :: DDManager -> DDNode -> DDNode -> DDNode Source #

bXor :: DDManager -> DDNode -> DDNode -> DDNode Source #

bXnor :: DDManager -> DDNode -> DDNode -> DDNode Source #

bNot :: DDManager -> DDNode -> DDNode Source #

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

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

cudd_cache_slots :: Int Source #

cudd_unique_slots :: Int Source #

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

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

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

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

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

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

bExists :: DDManager -> DDNode -> DDNode -> DDNode Source #

bForall :: DDManager -> DDNode -> DDNode -> DDNode Source #

bIte :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode Source #

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

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

nodeReadIndex :: DDNode -> Int Source #

dagSize :: DDNode -> Int Source #

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

liCompaction :: DDManager -> DDNode -> DDNode -> DDNode Source #

minimize :: DDManager -> DDNode -> DDNode -> DDNode Source #

readSize :: DDManager -> Int Source #

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

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

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

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

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

ddNodeToInt :: Integral i => DDNode -> i Source #

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

readPerm :: DDManager -> Int -> Int Source #

readInvPerm :: DDManager -> Int -> Int Source #

readPerms :: DDManager -> [Int] Source #

readInvPerms :: DDManager -> [Int] Source #

readTree :: DDManager -> IO (Ptr CMtrNode) Source #

countLeaves :: DDNode -> Int Source #

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

countPath :: DDNode -> Double Source #

countPathsToNonZero :: DDNode -> Double Source #

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

andAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode Source #

xorExistAbstract :: DDManager -> DDNode -> DDNode -> DDNode -> DDNode Source #

transfer :: DDManager -> DDManager -> DDNode -> DDNode Source #

makePrime :: DDManager -> DDNode -> DDNode -> DDNode Source #

constrain :: DDManager -> DDNode -> DDNode -> DDNode Source #

restrict :: DDManager -> DDNode -> DDNode -> DDNode Source #

squeeze :: DDManager -> DDNode -> DDNode -> DDNode Source #

data SatBit Source #

Constructors

Zero 
One 
DontCare 

Instances

Eq SatBit Source # 

Methods

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

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

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

lEq :: DDManager -> DDNode -> DDNode -> Bool Source #

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