Data.ABC.Internal.CNF

Documentation

type Cnf_Dat_t = Ptr Cnf_Dat_t_

cnfVarNums :: Cnf_Dat_t -> IO (Ptr CInt)

withCnfDerive :: Aig_Man_t -> CInt -> (Cnf_Dat_t -> IO a) -> IO a

Use results on cnfDerive in a comptuation, then free them.

cnfDataWriteIntoFile :: Cnf_Dat_t -> String -> Int -> Ptr () -> Ptr () -> IO ()

type Cnf_Man_t = ForeignPtr Cnf_Man_t_

data Cnf_Man_t_

cnfManStart :: IO Cnf_Man_t

Create a new CNF manager.

cnfDeriveWithMan :: Cnf_Man_t -> Aig_Man_t -> CInt -> IO Cnf_Dat_t

cnfDataFree :: Cnf_Dat_t -> IO ()

cnfDataWriteIntoFileWithHeader :: Cnf_Dat_t -> String -> String -> Int -> IO ()