Cudd.Imperative

An ST Monad based interface 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 Control.Monad.ST
import Cudd.Imperative

main = do
    res <- stToIO $ withManagerDefaults $ \manager -> do
        v1      <- ithVar manager 0
        v2      <- ithVar manager 1
        conj    <- bAnd manager v1 v2
        implies <- lEq manager conj v1
        deref manager conj
        return implies
    print res

Documentation

newtype DDManager s u

Constructors

DDManager

Fields

• unDDManager :: Ptr CDDManager

newtype DDNode s u

Constructors

DDNode

Fields

• unDDNode :: Ptr CDDNode

Instances

Eq (DDNode s u)

Methods

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

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

Ord (DDNode s u)

Methods

compare :: DDNode s u -> DDNode s u -> Ordering

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

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

(>) :: DDNode s u -> DDNode s u -> Bool

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

max :: DDNode s u -> DDNode s u -> DDNode s u

min :: DDNode s u -> DDNode s u -> DDNode s u

Show (DDNode s u)

Methods

showsPrec :: Int -> DDNode s u -> ShowS

show :: DDNode s u -> String

showList :: [DDNode s u] -> ShowS

cuddInit :: Int -> Int -> Int -> Int -> Int -> ST s (DDManager s u)

cuddInitDefaults :: ST s (DDManager s u)

withManager :: Int -> Int -> Int -> Int -> Int -> (forall u. DDManager s u -> ST s a) -> ST s a

withManagerDefaults :: (forall u. DDManager s u -> ST s a) -> ST s a

withManagerIO :: MonadIO m => Int -> Int -> Int -> Int -> Int -> (forall u. DDManager RealWorld u -> m a) -> m a

withManagerIODefaults :: MonadIO m => (forall u. DDManager RealWorld u -> m a) -> m a

shuffleHeap :: DDManager s u -> [Int] -> ST s ()

bZero :: DDManager s u -> DDNode s u

bOne :: DDManager s u -> DDNode s u

ithVar :: DDManager s u -> Int -> ST s (DDNode s u)

bAnd :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bOr :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bNand :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bNor :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bXor :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bXnor :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bNot :: DDNode s u -> DDNode s u

bIte :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bExists :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

bForall :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

deref :: DDManager s u -> DDNode s u -> ST s ()

setVarMap :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s ()

varMap :: DDManager s u -> DDNode s u -> ST s (DDNode s u)

lEq :: DDManager s u -> DDNode s u -> DDNode s u -> ST s Bool

swapVariables :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> DDNode s u -> ST s (DDNode s u)

ref :: DDNode s u -> ST s ()

largestCube :: DDManager s u -> DDNode s u -> ST s (DDNode s u, Int)

makePrime :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

support :: DDManager s u -> DDNode s u -> ST s (DDNode s u)

supportIndices :: DDManager s u -> DDNode s u -> ST s [Int]

indicesToCube :: DDManager s u -> [Int] -> ST s (DDNode s u)

computeCube :: DDManager s u -> [DDNode s u] -> [Bool] -> ST s (DDNode s u)

nodesToCube :: DDManager s u -> [DDNode s u] -> ST s (DDNode s u)

readSize :: DDManager s u -> ST s Int

bddToCubeArray :: DDManager s u -> DDNode s u -> ST s [SatBit]

compose :: DDManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (DDNode s u)

andAbstract :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

xorExistAbstract :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

leqUnless :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s Bool

equivDC :: DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u -> ST s Bool

xEqY :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s (DDNode s u)

debugCheck :: DDManager s u -> ST s Int

checkKeys :: DDManager s u -> ST s Int

pickOneMinterm :: DDManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u)

toInt :: DDNode s u -> Int

checkZeroRef :: DDManager s u -> ST s Int

readInvPerm :: DDManager s u -> Int -> ST s Int

readPerm :: DDManager s u -> Int -> ST s Int

dagSize :: DDNode s u -> ST s Int

readNodeCount :: DDManager s u -> ST s Integer

readPeakNodeCount :: DDManager s u -> ST s Integer

regular :: DDNode s u -> DDNode s u

readMaxCache :: DDManager s u -> ST s Int

readMaxCacheHard :: DDManager s u -> ST s Int

setMaxCacheHard :: DDManager s u -> Int -> ST s ()

readCacheSlots :: DDManager s u -> ST s Int

readCacheUsedSlots :: DDManager s u -> ST s Int

cudd_unique_slots :: Int

cudd_cache_slots :: Int

andLimit :: DDManager s u -> DDNode s u -> DDNode s u -> Int -> ST s (Maybe (DDNode s u))

readTree :: DDManager s u -> ST s (MtrNode s)

newVarAtLevel :: DDManager s u -> Int -> ST s (DDNode s u)

liCompaction :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

squeeze :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

minimize :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)

newVar :: DDManager s u -> ST s (DDNode s u)

vectorCompose :: DDManager s u -> DDNode s u -> [DDNode s u] -> ST s (DDNode s u)

quit :: DDManager s u -> ST s ()

readIndex :: DDNode s u -> ST s Int

printMinterm :: DDManager s u -> DDNode s u -> ST s ()

countMintermExact :: DDManager s u -> DDNode s u -> Int -> ST s Integer

checkCube :: DDManager s u -> DDNode s u -> ST s Bool

data Cube

data Prime

data DDGen s u t

Constructors

DDGen (Ptr CDDGen)

genFree :: DDGen s u t -> ST s ()

isGenEmpty :: DDGen s u t -> ST s Bool

firstCube :: DDManager s u -> DDNode s u -> ST s (Maybe ([SatBit], DDGen s u Cube))

nextCube :: DDManager s u -> DDGen s u Cube -> ST s (Maybe [SatBit])

firstPrime :: DDManager s u -> DDNode s u -> DDNode s u -> ST s (Maybe ([SatBit], DDGen s u Prime))

nextPrime :: DDManager s u -> DDGen s u Prime -> ST s (Maybe [SatBit])

firstNode :: DDManager s u -> DDNode s u -> ST s (Maybe (DDNode s u, DDGen s u Node))

nextNode :: DDManager s u -> DDGen s u Node -> ST s (Maybe (DDNode s u))

module Cudd.Common