<commit_before>{-# LANGUAGE RankNTypes #-}

{-| 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
-}

module Cudd.Imperative (
    DDManager(..),
    DDNode(..),
    cuddInit,
    cuddInitDefaults,
    withManager, 
    withManagerDefaults,
    withManagerIO,
    withManagerIODefaults,
    shuffleHeap,
    bZero,
    bOne,
    ithVar,
    bAnd,
    bOr,
    bNand,
    bNor,
    bXor,
    bXnor,
    bNot,
    bIte,
    bExists,
    bForall,
    deref,
    setVarMap,
    varMap,
    lEq,
    swapVariables,
    ref,
    largestCube,
    makePrime,
    support,
    supportIndices,
    indicesToCube,
    computeCube,
    nodesToCube,
    readSize,
    bddToCubeArray,
    compose,
    andAbstract,
    xorExistAbstract,
    leqUnless,
    equivDC,
    xEqY,
    debugCheck,
    checkKeys,
    pickOneMinterm,
    toInt,
    checkZeroRef,
    readInvPerm,
    readPerm,
    dagSize,
    readNodeCount,
    readPeakNodeCount,
    regular,
    readMaxCache,
    readMaxCacheHard,
    setMaxCacheHard,
    readCacheSlots,
    readCacheUsedSlots,
    cudd_unique_slots,
    cudd_cache_slots,
    andLimit,
    readTree,
    newVarAtLevel,
    liCompaction,
    squeeze,
    minimize,
    newVar,
    vectorCompose,
    quit,
    readIndex,
    printMinterm,
    checkCube,
    Cube,
    Prime,
    DDGen(..),
    genFree,
    isGenEmpty,
    firstCube,
    nextCube,
    firstPrime,
    nextPrime,
    module Cudd.Common
    ) where

import Foreign hiding (void)
import Foreign.Ptr
import Foreign.C.Types
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Control.Monad
import Control.Monad.IO.Class
import Data.List
import System.IO.Unsafe

import Cudd.C
import Cudd.MTR
import Cudd.Common

newtype DDManager s u = DDManager {unDDManager :: Ptr CDDManager}
newtype DDNode    s u = DDNode    {unDDNode    :: Ptr CDDNode} deriving (Ord, Eq, Show)

cuddInit :: Int -> Int -> Int -> Int -> Int -> ST s (DDManager s u)
cuddInit numVars numVarsZ numSlots cacheSize maxMemory = unsafeIOToST $ do
    cm <- c_cuddInit (fromIntegral numVars) (fromIntegral numVarsZ) (fromIntegral numSlots) (fromIntegral cacheSize) (fromIntegral maxMemory)
    return $ DDManager cm

cuddInitDefaults :: ST s (DDManager s u)
cuddInitDefaults = cuddInit 0 0 cudd_unique_slots cudd_cache_slots 0

withManager :: Int -> Int -> Int -> Int -> Int -> (forall u. DDManager s u -> ST s a) -> ST s a
withManager numVars numVarsZ numSlots cacheSize maxMemory f = do
    res <- cuddInit numVars numVarsZ numSlots cacheSize maxMemory
    f res 

withManagerDefaults :: (forall u. DDManager s u -> ST s a) -> ST s a
withManagerDefaults f = do
    res <- cuddInitDefaults
    f res 

withManagerIO :: MonadIO m => Int -> Int -> Int -> Int -> Int -> (forall u. DDManager RealWorld u -> m a) -> m a
withManagerIO numVars numVarsZ numSlots cacheSize maxMemory f = do
    res <- liftIO $ stToIO $ cuddInit numVars numVarsZ numSlots cacheSize maxMemory
    f res

withManagerIODefaults :: MonadIO m => (forall u. DDManager RealWorld u -> m a) -> m a
withManagerIODefaults f = do
    res <- liftIO $ stToIO cuddInitDefaults
    f res

shuffleHeap :: DDManager s u -> [Int] -> ST s ()
shuffleHeap (DDManager m) order = unsafeIOToST $ 
    withArrayLen (map fromIntegral order) $ \size ptr -> do
    when (sort order /= [0..size-1]) (error "shuffleHeap: order does not contain each variable once") 
    res1 <- c_cuddBddIthVar m (fromIntegral (size - 1))
    when (res1 == nullPtr) (error "shuffleHeap: Failed to resize table")
    res2 <- c_cuddShuffleHeap m ptr
    when (fromIntegral res2 /= 1) (error "shuffleHeap: Cudd_ShuffleHeap failed")
    return ()

toInt :: DDNode s u -> Int
toInt (DDNode n) = fromIntegral $ ptrToIntPtr n

arg0 :: (Ptr CDDManager -> IO (Ptr CDDNode)) -> DDManager s u -> ST s (DDNode s u)
arg0 f (DDManager m) = liftM DDNode $ unsafeIOToST $ f m

arg1 :: (Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> ST s (DDNode s u)
arg1 f (DDManager m) (DDNode x) = liftM DDNode $ unsafeIOToST $ f m x

arg2 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)
arg2 f (DDManager m) (DDNode x) (DDNode y) = liftM DDNode $ unsafeIOToST $ f m x y
    
arg3 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u  -> ST s (DDNode s u)
arg3 f (DDManager m) (DDNode x) (DDNode y) (DDNode z) = liftM DDNode $ unsafeIOToST $ f m x y z

bZero (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadLogicZero m
bOne  (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadOne m

bAnd    = arg2 c_cuddBddAnd
bOr     = arg2 c_cuddBddOr
bNand   = arg2 c_cuddBddNand
bNor    = arg2 c_cuddBddNor
bXor    = arg2 c_cuddBddXor
bXnor   = arg2 c_cuddBddXnor
bIte    = arg3 c_cuddBddIte
bExists = arg2 c_cuddBddExistAbstract
bForall = arg2 c_cuddBddUnivAbstract

andAbstract      = arg3 c_cuddBddAndAbstract
xorExistAbstract = arg3 c_cuddBddXorExistAbstract

bNot (DDNode x) = DDNode $ unsafePerformIO $ c_cuddNotNoRef x
ithVar (DDManager m) i = liftM DDNode $ unsafeIOToST $ c_cuddBddIthVar m (fromIntegral i)

deref :: DDManager s u -> DDNode s u -> ST s ()
deref (DDManager m) (DDNode x) = unsafeIOToST $ c_cuddIterDerefBdd m x

setVarMap :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s ()
setVarMap (DDManager m) xs ys = unsafeIOToST $ 
    withArrayLen (map unDDNode xs) $ \xl xp -> 
    withArrayLen (map unDDNode ys) $ \yl yp -> do
    when (xl /= yl) (error "setVarMap: lengths not equal")
    void $ c_cuddSetVarMap m xp yp (fromIntegral xl)<commit_msg>add some type sigs<commit_after>{-# LANGUAGE RankNTypes #-}

{-| 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
-}

module Cudd.Imperative (
    DDManager(..),
    DDNode(..),
    cuddInit,
    cuddInitDefaults,
    withManager, 
    withManagerDefaults,
    withManagerIO,
    withManagerIODefaults,
    shuffleHeap,
    bZero,
    bOne,
    ithVar,
    bAnd,
    bOr,
    bNand,
    bNor,
    bXor,
    bXnor,
    bNot,
    bIte,
    bExists,
    bForall,
    deref,
    setVarMap,
    varMap,
    lEq,
    swapVariables,
    ref,
    largestCube,
    makePrime,
    support,
    supportIndices,
    indicesToCube,
    computeCube,
    nodesToCube,
    readSize,
    bddToCubeArray,
    compose,
    andAbstract,
    xorExistAbstract,
    leqUnless,
    equivDC,
    xEqY,
    debugCheck,
    checkKeys,
    pickOneMinterm,
    toInt,
    checkZeroRef,
    readInvPerm,
    readPerm,
    dagSize,
    readNodeCount,
    readPeakNodeCount,
    regular,
    readMaxCache,
    readMaxCacheHard,
    setMaxCacheHard,
    readCacheSlots,
    readCacheUsedSlots,
    cudd_unique_slots,
    cudd_cache_slots,
    andLimit,
    readTree,
    newVarAtLevel,
    liCompaction,
    squeeze,
    minimize,
    newVar,
    vectorCompose,
    quit,
    readIndex,
    printMinterm,
    checkCube,
    Cube,
    Prime,
    DDGen(..),
    genFree,
    isGenEmpty,
    firstCube,
    nextCube,
    firstPrime,
    nextPrime,
    module Cudd.Common
    ) where

import Foreign hiding (void)
import Foreign.Ptr
import Foreign.C.Types
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Control.Monad
import Control.Monad.IO.Class
import Data.List
import System.IO.Unsafe

import Cudd.C
import Cudd.MTR
import Cudd.Common

newtype DDManager s u = DDManager {unDDManager :: Ptr CDDManager}
newtype DDNode    s u = DDNode    {unDDNode    :: Ptr CDDNode} deriving (Ord, Eq, Show)

cuddInit :: Int -> Int -> Int -> Int -> Int -> ST s (DDManager s u)
cuddInit numVars numVarsZ numSlots cacheSize maxMemory = unsafeIOToST $ do
    cm <- c_cuddInit (fromIntegral numVars) (fromIntegral numVarsZ) (fromIntegral numSlots) (fromIntegral cacheSize) (fromIntegral maxMemory)
    return $ DDManager cm

cuddInitDefaults :: ST s (DDManager s u)
cuddInitDefaults = cuddInit 0 0 cudd_unique_slots cudd_cache_slots 0

withManager :: Int -> Int -> Int -> Int -> Int -> (forall u. DDManager s u -> ST s a) -> ST s a
withManager numVars numVarsZ numSlots cacheSize maxMemory f = do
    res <- cuddInit numVars numVarsZ numSlots cacheSize maxMemory
    f res 

withManagerDefaults :: (forall u. DDManager s u -> ST s a) -> ST s a
withManagerDefaults f = do
    res <- cuddInitDefaults
    f res 

withManagerIO :: MonadIO m => Int -> Int -> Int -> Int -> Int -> (forall u. DDManager RealWorld u -> m a) -> m a
withManagerIO numVars numVarsZ numSlots cacheSize maxMemory f = do
    res <- liftIO $ stToIO $ cuddInit numVars numVarsZ numSlots cacheSize maxMemory
    f res

withManagerIODefaults :: MonadIO m => (forall u. DDManager RealWorld u -> m a) -> m a
withManagerIODefaults f = do
    res <- liftIO $ stToIO cuddInitDefaults
    f res

shuffleHeap :: DDManager s u -> [Int] -> ST s ()
shuffleHeap (DDManager m) order = unsafeIOToST $ 
    withArrayLen (map fromIntegral order) $ \size ptr -> do
    when (sort order /= [0..size-1]) (error "shuffleHeap: order does not contain each variable once") 
    res1 <- c_cuddBddIthVar m (fromIntegral (size - 1))
    when (res1 == nullPtr) (error "shuffleHeap: Failed to resize table")
    res2 <- c_cuddShuffleHeap m ptr
    when (fromIntegral res2 /= 1) (error "shuffleHeap: Cudd_ShuffleHeap failed")
    return ()

toInt :: DDNode s u -> Int
toInt (DDNode n) = fromIntegral $ ptrToIntPtr n

arg0 :: (Ptr CDDManager -> IO (Ptr CDDNode)) -> DDManager s u -> ST s (DDNode s u)
arg0 f (DDManager m) = liftM DDNode $ unsafeIOToST $ f m

arg1 :: (Ptr CDDManager -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> ST s (DDNode s u)
arg1 f (DDManager m) (DDNode x) = liftM DDNode $ unsafeIOToST $ f m x

arg2 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> DDNode s u -> ST s (DDNode s u)
arg2 f (DDManager m) (DDNode x) (DDNode y) = liftM DDNode $ unsafeIOToST $ f m x y
    
arg3 :: (Ptr CDDManager -> Ptr CDDNode -> Ptr CDDNode -> Ptr CDDNode -> IO (Ptr CDDNode)) -> DDManager s u -> DDNode s u -> DDNode s u -> DDNode s u  -> ST s (DDNode s u)
arg3 f (DDManager m) (DDNode x) (DDNode y) (DDNode z) = liftM DDNode $ unsafeIOToST $ f m x y z

bZero, bOne :: DDManager s u -> DDNode s u
bZero (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadLogicZero m
bOne  (DDManager m) = DDNode $ unsafePerformIO $ c_cuddReadOne m

bAnd    = arg2 c_cuddBddAnd
bOr     = arg2 c_cuddBddOr
bNand   = arg2 c_cuddBddNand
bNor    = arg2 c_cuddBddNor
bXor    = arg2 c_cuddBddXor
bXnor   = arg2 c_cuddBddXnor
bIte    = arg3 c_cuddBddIte
bExists = arg2 c_cuddBddExistAbstract
bForall = arg2 c_cuddBddUnivAbstract

andAbstract      = arg3 c_cuddBddAndAbstract
xorExistAbstract = arg3 c_cuddBddXorExistAbstract

bNot :: DDNode s u -> DDNode s u
bNot (DDNode x) = DDNode $ unsafePerformIO $ c_cuddNotNoRef x

ithVar :: DDManager s u -> Int -> ST s (DDNode s u)
ithVar (DDManager m) i = liftM DDNode $ unsafeIOToST $ c_cuddBddIthVar m (fromIntegral i)

deref :: DDManager s u -> DDNode s u -> ST s ()
deref (DDManager m) (DDNode x) = unsafeIOToST $ c_cuddIterDerefBdd m x

setVarMap :: DDManager s u -> [DDNode s u] -> [DDNode s u] -> ST s ()
setVarMap (DDManager m) xs ys = unsafeIOToST $ 
    withArrayLen (map unDDNode xs) $ \xl xp -> 
    withArrayLen (map unDDNode ys) $ \yl yp -> do
    when (xl /= yl) (error "setVarMap: lengths not equal")
    void $ c_cuddSetVarMap m xp yp (fromIntegral xl)
{'fraction_non_alphanumeric': 0.0937197287697772, 'fraction_numerical': 0.0059735227639651275, 'mean_word_length': 2.9143759873617694, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 155, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4965842', 'n_tokens_mistral': 4667, 'n_tokens_neox': 4548, 'n_words': 1415}