Safe Haskell	None
Language	Haskell2010

Cudd.Imperative

Description

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 Source

Constructors

DDManager
Fields unDDManager :: Ptr CDDManager

newtype DDNode s u Source

Constructors

DDNode
Fields unDDNode :: Ptr CDDNode

Instances

Eq (DDNode s u)
Ord (DDNode s u)
Show (DDNode s u)

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

cuddInitDefaults :: ST s (DDManager s u) Source

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

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

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

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

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

bZero :: DDManager s u -> DDNode s u Source

bOne :: DDManager s u -> DDNode s u Source

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

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

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

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

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

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

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

bNot :: DDNode s u -> DDNode s u Source

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

readSize :: DDManager s u -> ST s Int Source

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

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

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

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

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

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

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

debugCheck :: DDManager s u -> ST s Int Source

checkKeys :: DDManager s u -> ST s Int Source

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

toInt :: DDNode s u -> Int Source

checkZeroRef :: DDManager s u -> ST s Int Source

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

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

dagSize :: DDNode s u -> ST s Int Source

readNodeCount :: DDManager s u -> ST s Integer Source

readPeakNodeCount :: DDManager s u -> ST s Integer Source

regular :: DDNode s u -> DDNode s u Source

readMaxCache :: DDManager s u -> ST s Int Source

readMaxCacheHard :: DDManager s u -> ST s Int Source

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

readCacheSlots :: DDManager s u -> ST s Int Source

readCacheUsedSlots :: DDManager s u -> ST s Int Source

cudd_unique_slots :: Int Source

cudd_cache_slots :: Int Source

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

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

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

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

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

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

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

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

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

readIndex :: DDNode s u -> ST s Int Source

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

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

data Cube Source

data Prime Source

data DDGen s u t Source

Constructors

DDGen (Ptr CDDGen)

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

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

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

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

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

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

module Cudd.Common