-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Bindings for ABC, A System for Sequential -- Synthesis and Verification -- -- Bindings for ABC focused on creating And-Inverter Graphs (AIG) and -- then performing synthesis and equivalence checking. @package abcBridge @version 0.15 -- | Incomplete. Binding of misc/util/abc_global.h which -- contains miscellaneous functions for ABC, including a counterexample -- datastructure and error handling mechanisms. module Data.ABC.Internal.ABCGlobal data Abc_Cex_t_ Abc_Cex_t_ :: Int -> Int -> Int -> Int -> Int -> [Bool] -> [[Bool]] -> Abc_Cex_t_ -- | the zero-based number of PO, for which verification failed [iPo'Abc_Cex] :: Abc_Cex_t_ -> Int -- | the zero-based number of the time-frame, for which verificaiton failed [iFrame'Abc_Cex] :: Abc_Cex_t_ -> Int -- | the number of registers in the miter [nRegs'Abc_Cex] :: Abc_Cex_t_ -> Int -- | the number of primary inputs in the miter [nPis'Abc_Cex] :: Abc_Cex_t_ -> Int -- | the number of words of bit data used (ezyang: where by words they -- actually mean bits) [nBits'Abc_Cex] :: Abc_Cex_t_ -> Int -- | The cex bit data (the number of bits: nRegs + (iFrame+1) * -- nPis) The format of the data is as such: -- -- [pData'regs'Abc_Cex] :: Abc_Cex_t_ -> [Bool] -- | outer length: iFrame+1; inner length: nPis [pData'inputs'Abc_Cex] :: Abc_Cex_t_ -> [[Bool]] type Abc_Cex_t = Ptr (Abc_Cex_t_) -- | Peek into the value of a Abc_Cex_t. peekAbcCex :: Abc_Cex_t -> IO Abc_Cex_t_ instance GHC.Classes.Eq Data.ABC.Internal.ABCGlobal.Abc_Cex_t_ instance GHC.Show.Show Data.ABC.Internal.ABCGlobal.Abc_Cex_t_ instance GHC.Read.Read Data.ABC.Internal.ABCGlobal.Abc_Cex_t_ -- | module Data.ABC.Internal.FRAIG data Prove_Params_t_ Prove_Params_t_ :: Bool -> Bool -> Bool -> Bool -> Int -> Int -> Float -> Int -> Float -> Int -> Float -> Int -> Bool -> Int -> Int64 -> Int64 -> Int64 -> Int64 -> Prove_Params_t_ -- | enables fraiging [fUseFraiging'Prove_Params] :: Prove_Params_t_ -> Bool -- | enables rewriting [fUseRewriting'Prove_Params] :: Prove_Params_t_ -> Bool -- | enables BDD construction when other methods fail [fUseBdds'Prove_Params] :: Prove_Params_t_ -> Bool -- | prints verbose stats [fVerbose'Prove_Params] :: Prove_Params_t_ -> Bool -- | the number of iterations [nItersMax'Prove_Params] :: Prove_Params_t_ -> Int -- | starting mitering limit [nMiteringLimitStart'Prove_Params] :: Prove_Params_t_ -> Int -- | multiplicative coefficient to increase the limit in each iteration [nMiteringLimitMulti'Prove_Params] :: Prove_Params_t_ -> Float -- | the number of rewriting iterations [nRewritingLimitStart'Prove_Params] :: Prove_Params_t_ -> Int -- | multiplicative coefficient to increase the limit in each iteration [nRewritingLimitMulti'Prove_Params] :: Prove_Params_t_ -> Float -- | starting backtrack(conflict) limit [nFraigingLimitStart'Prove_Params] :: Prove_Params_t_ -> Int -- | multiplicative coefficient to increase the limit in each iteration [nFraigingLimitMulti'Prove_Params] :: Prove_Params_t_ -> Float -- | the number of BDD nodes when construction is aborted [nBddSizeLimit'Prove_Params] :: Prove_Params_t_ -> Int -- | enables dynamic BDD variable reordering [fBddReorder'Prove_Params] :: Prove_Params_t_ -> Bool -- | final mitering limit [nMiteringLimitLast'Prove_Params] :: Prove_Params_t_ -> Int -- | global limit on the number of backtracks [nTotalBacktrackLimit'Prove_Params] :: Prove_Params_t_ -> Int64 -- | global limit on the number of clause inspects [nTotalInspectLimit'Prove_Params] :: Prove_Params_t_ -> Int64 -- | the total number of backtracks made [nTotalBacktracksMade'Prove_Params] :: Prove_Params_t_ -> Int64 -- | the total number of inspects made [nTotalInspectsMade'Prove_Params] :: Prove_Params_t_ -> Int64 proveParamsDefault :: Prove_Params_t_ instance GHC.Classes.Eq Data.ABC.Internal.FRAIG.Prove_Params_t_ instance GHC.Show.Show Data.ABC.Internal.FRAIG.Prove_Params_t_ instance GHC.Read.Read Data.ABC.Internal.FRAIG.Prove_Params_t_ instance Foreign.Storable.Storable Data.ABC.Internal.FRAIG.Prove_Params_t_ module Data.ABC.Internal.Field data Field a b Field :: (a -> IO b) -> (a -> b -> IO ()) -> Field a b [readAt] :: Field a b -> a -> IO b [writeAt] :: Field a b -> a -> b -> IO () fieldFromOffset :: Storable b => Int -> Field (Ptr a) b isoFieldTarget :: Field a b -> Iso b c -> Field a c -- | An isomorphism view. data Iso a b -- | Create an isomorphism iso :: (a -> b) -> (b -> a) -> Iso a b -- | Incomplete. Binding of misc/vec/vecInt.h for -- manipulating vectors of integers. module Data.ABC.Internal.VecInt data Vec_Int_t_ type Vec_Int_t = Ptr (Vec_Int_t_) clearVecInt :: Vec_Int_t -> IO () vecIntSize :: Vec_Int_t -> IO CInt setVecIntSize :: Vec_Int_t -> CInt -> IO () vecIntCap :: Vec_Int_t -> IO CInt setVecIntCap :: Vec_Int_t -> CInt -> IO () vecIntArray :: Vec_Int_t -> IO (Ptr CInt) setVecIntArray :: Vec_Int_t -> Ptr CInt -> IO () -- | Get entry in vector at given index. vecIntEntry :: Vec_Int_t -> CInt -> IO CInt -- | Write entry in vector at given index. vecIntWriteEntry :: Vec_Int_t -> CInt -> CInt -> IO () withVecInt :: CInt -> Ptr CInt -> (Vec_Int_t -> IO a) -> IO a -- | Incomplete. Binding of misc/vec/vecPtr.h for -- manipulating vectors of pointers. module Data.ABC.Internal.VecPtr data Vec_Ptr_t_ type Vec_Ptr_t = Ptr (Vec_Ptr_t_) clearVec :: Vec_Ptr_t -> IO () vecPtrSize :: Vec_Ptr_t -> IO Int vecPtrArray :: Vec_Ptr_t -> IO (Ptr (Ptr a)) vecPtrEntry :: Vec_Ptr_t -> Int -> IO (Ptr a) clearVecPtr :: Vec_Ptr_t -> IO () -- | Bindings to aig/gia/gia.h for manipulating and running -- algorithms on scalable and-inverter graphs (GIA), a representation -- that is optimized for memory-efficiency. These functions power the -- next-generation of ABC algorithms that have not been officially -- released yet, and can be identified by the prefix of an ampersand, as -- in &cec, in the interactive ABC interface. module Data.ABC.Internal.GIA type Gia_Man_t = Ptr (Gia_Man_t_) data Gia_Man_t_ giaManNObjs :: Field Gia_Man_t CInt giaManFanData :: Gia_Man_t -> IO (Ptr CInt) -- | A pointer to a GIA object. GIA objects are pointers to structs in ABC, -- and represent literals in the AIG. The low-order bit of the pointer is -- set to 1 if the literal has been complemented, and so care must be -- taken to only dereference positive pointers. The object is also a -- bitfield, so care must be taken when accessing fields. -- -- Pointers to GIA objects may be invalidated when adding a new object. type Gia_Obj_t = Ptr (Gia_Obj_t_) getGiaObjValue :: Gia_Obj_t -> IO CUInt setGiaObjValue :: Gia_Obj_t -> CUInt -> IO () -- | Also known as the node's id. No complement info. newtype GiaVar GiaVar :: CInt -> GiaVar [unGiaVar] :: GiaVar -> CInt -- | Literals store complement information. newtype GiaLit GiaLit :: CInt -> GiaLit [unGiaLit] :: GiaLit -> CInt giaManConst0Lit :: GiaLit giaManConst1Lit :: GiaLit giaLitIsCompl :: GiaLit -> Bool giaLitVar :: GiaLit -> GiaVar -- | Returns positive literal associated to var. giaVarLit :: GiaVar -> GiaLit giaLitNotCond :: GiaLit -> Bool -> GiaLit giaManCexComb :: Gia_Man_t -> IO Abc_Cex_t giaManConst0 :: Gia_Man_t -> IO Gia_Obj_t giaManCis :: Gia_Man_t -> IO Vec_Int_t giaManCos :: Gia_Man_t -> IO Vec_Int_t giaManCiNum :: Gia_Man_t -> IO CInt giaManCoNum :: Gia_Man_t -> IO CInt giaManPiNum :: Gia_Man_t -> IO CInt giaManPoNum :: Gia_Man_t -> IO CInt giaManAndNum :: Gia_Man_t -> IO CInt getGiaManRegNum :: Gia_Man_t -> IO CInt setGiaManRegNum :: Gia_Man_t -> CInt -> IO () -- | Get var index of combinational input at given index. giaManCiVar :: Gia_Man_t -> CInt -> IO GiaVar -- | Get combinational output at given index. giaManCoVar :: Gia_Man_t -> CInt -> IO GiaVar -- | Get combinational input at given index. giaManCi :: Gia_Man_t -> CInt -> IO Gia_Obj_t -- | Get combinational output at given index. giaManCo :: Gia_Man_t -> CInt -> IO Gia_Obj_t -- | Return object associated with gia var. giaManObj :: Gia_Man_t -> GiaVar -> IO Gia_Obj_t gia_none :: CUInt -- | Returns true if this is a combinational output (latch or primary -- output). giaObjIsCo :: Gia_Obj_t -> IO Bool -- | Returns iDiff0 field of object Note: iDiff0 is a bitfield, so this may -- be more likely to break on unexpected compilers. giaObjDiff0 :: Gia_Obj_t -> IO CUInt -- | Returns iDiff1 field of object Note: iDiff1 is a bitfield, so this may -- be more likely to break on unexpected compilers. giaObjDiff1 :: Gia_Obj_t -> IO CUInt -- | Get the complement attribute of first fanin giaObjFaninC0 :: Gia_Obj_t -> IO Bool giaObjFaninC1 :: Gia_Obj_t -> IO Bool -- | Get first user defined mark giaObjMark0 :: Gia_Obj_t -> IO Bool -- | Get second user defined mark giaObjMark1 :: Gia_Obj_t -> IO Bool giaObjChild0 :: Gia_Obj_t -> IO Gia_Obj_t giaObjChild1 :: Gia_Obj_t -> IO Gia_Obj_t giaObjFaninId0 :: Gia_Obj_t -> GiaVar -> IO GiaVar giaObjFaninId1 :: Gia_Obj_t -> GiaVar -> IO GiaVar giaObjIsTerm :: Gia_Obj_t -> IO Bool giaObjIsAndOrConst0 :: Gia_Obj_t -> IO Bool -- | Returns the variable index associated with the object. giaObjId :: Gia_Man_t -> Gia_Obj_t -> IO GiaVar giaManObjNum :: Gia_Man_t -> IO CInt giaLitNot :: GiaLit -> GiaLit -- | Remove negation. giaRegular :: Gia_Obj_t -> Gia_Obj_t giaIsComplement :: Gia_Obj_t -> Bool giaObjToLit :: (Gia_Man_t) -> (Gia_Obj_t) -> IO ((GiaLit)) giaObjFromLit :: (Gia_Man_t) -> (GiaLit) -> IO ((Gia_Obj_t)) giaManForEachObj1_ :: Gia_Man_t -> (Gia_Obj_t -> GiaVar -> IO b) -> IO () giaManForEachCo :: Gia_Man_t -> (Gia_Obj_t -> Int -> IO b) -> IO [b] giaManAppendCi :: Gia_Man_t -> IO GiaLit giaManAppendCo :: Gia_Man_t -> GiaLit -> IO GiaLit -- | This directly appends the literal to the GIA bypassing any -- hash-consing. giaManAppendAnd :: Gia_Man_t -> GiaLit -> GiaLit -> IO GiaLit giaAigerRead :: (String) -> (Bool) -> (Bool) -> IO ((Gia_Man_t)) giaAigerWrite :: (Gia_Man_t) -> (String) -> (Bool) -> (Bool) -> IO () giaManMiter :: (Gia_Man_t) -> (Gia_Man_t) -> (Int) -> (Bool) -> (Bool) -> (Bool) -> (Bool) -> IO ((Gia_Man_t)) -- | giaManDupDfsLazyLit pNew p l copies a lit l in -- p to pNew and returns the lit in pNew. giaDupLit :: Gia_Man_t -> Gia_Man_t -> GiaLit -> IO GiaLit giaManDupNormalize :: Gia_Man_t -> IO Gia_Man_t giaManHashAlloc :: Gia_Man_t -> IO () giaManHashStart :: Gia_Man_t -> IO () giaManHashStop :: Gia_Man_t -> IO () giaManHashAnd :: (Gia_Man_t) -> (GiaLit) -> (GiaLit) -> IO ((GiaLit)) giaManHashXor :: (Gia_Man_t) -> (GiaLit) -> (GiaLit) -> IO ((GiaLit)) giaManHashMux :: (Gia_Man_t) -> (GiaLit) -> (GiaLit) -> (GiaLit) -> IO ((GiaLit)) giaManStart :: (CInt) -> IO ((Gia_Man_t)) giaManStop :: Gia_Man_t -> IO () p_giaManStop :: FunPtr (Gia_Man_t -> IO ()) giaManCleanup :: (Gia_Man_t) -> IO ((Gia_Man_t)) giaManFillValue :: (Gia_Man_t) -> IO () clearGiaObj :: Gia_Obj_t -> IO () instance Foreign.Storable.Storable Data.ABC.Internal.GIA.GiaLit instance GHC.Classes.Ord Data.ABC.Internal.GIA.GiaLit instance GHC.Classes.Eq Data.ABC.Internal.GIA.GiaLit instance Foreign.Storable.Storable Data.ABC.Internal.GIA.GiaVar instance GHC.Classes.Ord Data.ABC.Internal.GIA.GiaVar instance GHC.Classes.Eq Data.ABC.Internal.GIA.GiaVar -- | Comprehensive binding of aig/cec/cec.h for performing -- combinational equivalence checking of scalable and-inverter graphs -- (GIA). module Data.ABC.Internal.CEC data Cec_ParCec_t_ Cec_ParCec_t_ :: Int -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Cec_ParCec_t_ -- | conflict limit at a node [nBTLimit'Cec_ParCec] :: Cec_ParCec_t_ -> Int -- | the runtime limit in seconds (added prefix n) [nTimeLimit'Cec_ParCec] :: Cec_ParCec_t_ -> Int -- | use smart CNF computation [fUseSmartCnf'Cec_ParCec] :: Cec_ParCec_t_ -> Bool -- | enables AIG rewriting [fRewriting'Cec_ParCec] :: Cec_ParCec_t_ -> Bool -- | perform naive SAT-based checking [fNaive'Cec_ParCec] :: Cec_ParCec_t_ -> Bool -- | very verbose stats [fVeryVerbose'Cec_ParCec] :: Cec_ParCec_t_ -> Bool -- | verbose stats [fVerbose'Cec_ParCec] :: Cec_ParCec_t_ -> Bool -- | the number of failed output [iOutFail'Cec_ParCec] :: Cec_ParCec_t_ -> Int data Cec_ParSat_t_ Cec_ParSat_t_ :: CInt -> CInt -> CInt -> Bool -> Bool -> Bool -> Bool -> Bool -> Cec_ParSat_t_ [nBTLimit'Cec_ParSat] :: Cec_ParSat_t_ -> CInt [nSatVarMax'Cec_ParSat] :: Cec_ParSat_t_ -> CInt [nCallsRecycle'Cec_ParSat] :: Cec_ParSat_t_ -> CInt [fNonChrono'Cec_ParSat] :: Cec_ParSat_t_ -> Bool [fPolarFlip'Cec_ParSat] :: Cec_ParSat_t_ -> Bool [fCheckMiter'Cec_ParSat] :: Cec_ParSat_t_ -> Bool [fLearnCls'Cec_ParSat] :: Cec_ParSat_t_ -> Bool [fVerbose'Cec_ParSat] :: Cec_ParSat_t_ -> Bool cecManVerify :: Gia_Man_t -> Cec_ParCec_t_ -> IO CInt cecManSatDefaultParams :: Cec_ParSat_t_ cecManCecDefaultParams :: Cec_ParCec_t_ cecManSatSolving :: Gia_Man_t -> Cec_ParSat_t_ -> IO Gia_Man_t data Cec_ManPat_t_ type Cec_ManPat_t = Ptr (Cec_ManPat_t_) cecManPatStart :: IO ((Cec_ManPat_t)) cecManPatStop :: (Cec_ManPat_t) -> IO () cecManPatPatCount :: Cec_ManPat_t -> IO CInt cecManPatPrintStats :: (Cec_ManPat_t) -> IO () cecManSatSolve :: (Cec_ManPat_t) -> (Gia_Man_t) -> (Cec_ParSat_t) -> IO () instance GHC.Classes.Eq Data.ABC.Internal.CEC.Cec_ParCec_t_ instance GHC.Read.Read Data.ABC.Internal.CEC.Cec_ParCec_t_ instance GHC.Show.Show Data.ABC.Internal.CEC.Cec_ParCec_t_ instance GHC.Classes.Eq Data.ABC.Internal.CEC.Cec_ParSat_t_ instance GHC.Read.Read Data.ABC.Internal.CEC.Cec_ParSat_t_ instance GHC.Show.Show Data.ABC.Internal.CEC.Cec_ParSat_t_ instance Foreign.Storable.Storable Data.ABC.Internal.CEC.Cec_ParSat_t_ instance Foreign.Storable.Storable Data.ABC.Internal.CEC.Cec_ParCec_t_ -- | Incomplete. Binding of aig/aig/aig.h. This defines the -- next-generation heavy-weight AIG representation (similar to the -- original Data.ABC.Internal.ABC) which is used in internal -- versions (base/abci/abc.c) 8D, 8 and occasionally for 9 -- (during which the GIA is temporarily converted into an AIG for some -- processing.) module Data.ABC.Internal.AIG data Aig_Type_t AigObjNone :: Aig_Type_t AigObjConst1 :: Aig_Type_t AigObjCi :: Aig_Type_t AigObjCo :: Aig_Type_t AigObjBuf :: Aig_Type_t AigObjAnd :: Aig_Type_t AigObjExor :: Aig_Type_t AigObjVoid :: Aig_Type_t data Aig_Man_t_ data Aig_Obj_t_ type Aig_Man_t = Ptr (Aig_Man_t_) type Aig_Obj_t = Ptr (Aig_Obj_t_) aigRegular :: Aig_Obj_t -> Aig_Obj_t aigNot :: Aig_Obj_t -> Aig_Obj_t aigNotCond :: Aig_Obj_t -> Bool -> Aig_Obj_t aigIsComplement :: Aig_Obj_t -> Bool aigManCiNum :: Aig_Man_t -> IO CInt aigManCoNum :: Aig_Man_t -> IO CInt aigManObjNumMax :: Aig_Man_t -> IO Int aigManConst0 :: Aig_Man_t -> IO Aig_Obj_t aigManConst1 :: Aig_Man_t -> IO Aig_Obj_t aigManCi :: (Aig_Man_t) -> (CInt) -> IO ((Aig_Obj_t)) aigManCo :: (Aig_Man_t) -> (CInt) -> IO ((Aig_Obj_t)) aigObjId :: (Aig_Obj_t) -> IO ((CInt)) aigManStart :: (CInt) -> IO ((Aig_Man_t)) aigManStop :: Aig_Man_t -> IO () p_aigManStop :: FunPtr (Aig_Man_t -> IO ()) aigObjCreateCi :: (Aig_Man_t) -> IO ((Aig_Obj_t)) aigObjCreateCo :: (Aig_Man_t) -> (Aig_Obj_t) -> IO ((Aig_Obj_t)) -- | Haskell type representing the C int type. data CInt :: * instance GHC.Classes.Eq Data.ABC.Internal.AIG.Aig_Type_t instance GHC.Show.Show Data.ABC.Internal.AIG.Aig_Type_t instance GHC.Enum.Enum Data.ABC.Internal.AIG.Aig_Type_t module Data.ABC.Internal.CNF type Cnf_Dat_t = Ptr (Cnf_Dat_t_) cnfVarNums :: Cnf_Dat_t -> IO (Ptr CInt) -- | Use results on cnfDerive in a comptuation, then free them. withCnfDerive :: Aig_Man_t -> CInt -> (Cnf_Dat_t -> IO a) -> IO a cnfDataWriteIntoFile :: (Cnf_Dat_t) -> (String) -> (Int) -> (Ptr ()) -> (Ptr ()) -> IO () type Cnf_Man_t = ForeignPtr (Cnf_Man_t_) data Cnf_Man_t_ -- | Create a new CNF manager. cnfManStart :: IO ((Cnf_Man_t)) 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 () -- | Comprehensive binding of aig/gia/giaAig.h for converting -- between AIGs (new-style, not ABC) and GIAs. module Data.ABC.Internal.GiaAig type Gia_AigMap_t = Ptr Aig_Obj_t withGiaAigMap :: Gia_Man_t -> (Gia_AigMap_t -> IO a) -> IO a aigDupGiaLit :: Aig_Man_t -> Gia_AigMap_t -> Gia_Man_t -> GiaLit -> IO Aig_Obj_t giaManToAig :: (Gia_Man_t) -> (CInt) -> IO ((Aig_Man_t)) -- | Incomplete. Binding of base/base/abc.h for -- manipulating and running algorithms on the original ABC datatypes. -- -- This current incomplete binding focuses on functions for manipulating -- and-inverter graphs (AIGs). module Data.ABC.Internal.ABC data Abc_NtkType_t AbcNtkNone :: Abc_NtkType_t AbcNtkNetlist :: Abc_NtkType_t AbcNtkLogic :: Abc_NtkType_t AbcNtkStrash :: Abc_NtkType_t AbcNtkOther :: Abc_NtkType_t data Abc_NtkFunc_t AbcFuncNone :: Abc_NtkFunc_t AbcFuncSop :: Abc_NtkFunc_t AbcFuncBdd :: Abc_NtkFunc_t AbcFuncAig :: Abc_NtkFunc_t AbcFuncMap :: Abc_NtkFunc_t AbcFuncBlifmv :: Abc_NtkFunc_t AbcFuncBlackbox :: Abc_NtkFunc_t AbcFuncOther :: Abc_NtkFunc_t data Abc_ObjType_t AbcObjNone :: Abc_ObjType_t AbcObjConst1 :: Abc_ObjType_t AbcObjPi :: Abc_ObjType_t AbcObjPo :: Abc_ObjType_t AbcObjBi :: Abc_ObjType_t AbcObjBo :: Abc_ObjType_t AbcObjNet :: Abc_ObjType_t AbcObjNode :: Abc_ObjType_t AbcObjLatch :: Abc_ObjType_t AbcObjWhitebox :: Abc_ObjType_t AbcObjBlackbox :: Abc_ObjType_t AbcObjNumber :: Abc_ObjType_t data Abc_Ntk_t_ data Abc_Obj_t_ type Abc_Ntk_t = Ptr (Abc_Ntk_t_) type Abc_Obj_t = Ptr (Abc_Obj_t_) abcNtkFunc :: Abc_Ntk_t -> IO Abc_NtkFunc_t -- | Network name manager. abcNtkManName :: Field Abc_Ntk_t Nm_Man_t -- | Return array of all objects. abcNtkObjs :: Abc_Ntk_t -> IO Vec_Ptr_t -- | Return primary inputs. abcNtkPis :: Abc_Ntk_t -> IO Vec_Ptr_t -- | Return primary outputs. abcNtkPos :: Abc_Ntk_t -> IO Vec_Ptr_t -- | Return combinational outputs (POs, asserts, latches). abcNtkCos :: Abc_Ntk_t -> IO Vec_Ptr_t -- | Return combinational inputs (PIs, latches) abcNtkCis :: Abc_Ntk_t -> IO Vec_Ptr_t abcNtkObj :: Abc_Ntk_t -> Int -> IO Abc_Obj_t -- | The functionality manager varies between AbcNtkFunc. In the -- case of AbcFuncAig, this pointer is guaranteed to be an -- Abc_Aig_t. abcNtkManFunc :: Abc_Ntk_t -> IO (Ptr ()) -- | Return pointer to model associated with network. abcNtkModel :: Abc_Ntk_t -> IO (Ptr CInt) -- | The EXDC network. abcNtkExdc :: Field Abc_Ntk_t Abc_Ntk_t abcNtkPiNum :: Abc_Ntk_t -> IO Int abcNtkPoNum :: Abc_Ntk_t -> IO Int abcNtkCiNum :: Abc_Ntk_t -> IO Int abcNtkCoNum :: Abc_Ntk_t -> IO Int abcNtkLatchNum :: Abc_Ntk_t -> IO CInt abcNtkCreateObj :: Abc_Ntk_t -> Abc_ObjType_t -> IO Abc_Obj_t -- | Negate object. abcObjNot :: Abc_Obj_t -> Abc_Obj_t data Nm_Man_t_ type Nm_Man_t = Ptr (Nm_Man_t_) nmManCreate :: (CInt) -> IO ((Nm_Man_t)) nmManFree :: (Nm_Man_t) -> IO () -- | Return true if object is complemented. abcObjIsComplement :: Abc_Obj_t -> Bool -- | Return normalized object. abcObjRegular :: Abc_Obj_t -> Abc_Obj_t -- | Object identifier. abcObjId :: Abc_Obj_t -> IO CInt -- | Object type. abcObjType :: Abc_Obj_t -> IO Abc_ObjType_t -- | Get object fanins. abcObjFanins :: Abc_Obj_t -> Vec_Int_t -- | Return true if this an and gate. abcObjIsAnd :: Abc_Obj_t -> IO Bool abcObjLit0 :: Abc_Obj_t -> IO Abc_Obj_t abcObjLit1 :: Abc_Obj_t -> IO Abc_Obj_t abcAigAnd :: Abc_Aig_t -> Abc_Obj_t -> Abc_Obj_t -> IO Abc_Obj_t abcAigXor :: Abc_Aig_t -> Abc_Obj_t -> Abc_Obj_t -> IO Abc_Obj_t abcAigMux :: Abc_Aig_t -> Abc_Obj_t -> Abc_Obj_t -> Abc_Obj_t -> IO Abc_Obj_t abcAigConst1 :: (Abc_Ntk_t) -> IO ((Abc_Obj_t)) abcAigCleanup :: Abc_Aig_t -> IO CInt abcObjAddFanin :: (Abc_Obj_t) -> (Abc_Obj_t) -> IO () abcNtkMiter :: (Abc_Ntk_t) -> (Abc_Ntk_t) -> (Bool) -> (Int) -> (Bool) -> (Bool) -> IO ((Abc_Ntk_t)) abcNtkMiterIsConstant :: (Abc_Ntk_t) -> IO ((Int)) abcNtkShortNames :: (Abc_Ntk_t) -> IO () abcNtkAlloc :: (Abc_NtkType_t) -> (Abc_NtkFunc_t) -> (Bool) -> IO ((Abc_Ntk_t)) -- | Duplicate a network, allocating memory for the new network. This -- procedure does not preserve the Id of objects. abcNtkDup :: (Abc_Ntk_t) -> IO ((Abc_Ntk_t)) abcNtkDelete :: (Abc_Ntk_t) -> IO () p_abcNtkDelete :: FunPtr (Abc_Ntk_t -> IO ()) abcNtkDeleteObj :: (Abc_Obj_t) -> IO () abcNtkDeleteObjPo :: (Abc_Obj_t) -> IO () abcNtkIvyProve :: (Ptr Abc_Ntk_t) -> (Ptr ()) -> IO ((Int)) abcNtkVerifySimulatePattern :: (Abc_Ntk_t) -> (Ptr CInt) -> IO ((ForeignPtr CInt)) abcNtkQbf :: (Abc_Ntk_t) -> (Int) -> (CInt) -> (Vec_Int_t) -> IO ((Int)) instance GHC.Classes.Eq Data.ABC.Internal.ABC.Abc_InitType_t instance GHC.Show.Show Data.ABC.Internal.ABC.Abc_InitType_t instance GHC.Classes.Eq Data.ABC.Internal.ABC.Abc_ObjType_t instance GHC.Show.Show Data.ABC.Internal.ABC.Abc_ObjType_t instance GHC.Classes.Eq Data.ABC.Internal.ABC.Abc_NtkFunc_t instance GHC.Show.Show Data.ABC.Internal.ABC.Abc_NtkFunc_t instance GHC.Classes.Eq Data.ABC.Internal.ABC.Abc_NtkType_t instance GHC.Show.Show Data.ABC.Internal.ABC.Abc_NtkType_t instance GHC.Enum.Enum Data.ABC.Internal.ABC.Abc_NtkType_t instance GHC.Enum.Enum Data.ABC.Internal.ABC.Abc_NtkFunc_t instance GHC.Enum.Enum Data.ABC.Internal.ABC.Abc_ObjType_t instance GHC.Enum.Enum Data.ABC.Internal.ABC.Abc_InitType_t -- | Binding of base/io/io.h for reading and writing networks to -- the file system. ABC natively supports a variety of different file -- formats. module Data.ABC.Internal.IO ioReadAiger :: (String) -> (Bool) -> IO ((Abc_Ntk_t)) ioWriteAiger :: (Abc_Ntk_t) -> (String) -> (Bool) -> (Bool) -> (Bool) -> IO () -- | Incomplete. Binding of various orphan functions in ABC: -- functions that are frequently extern'ed into scope but are not defined -- in any header; we've created a new header file orphan.h to -- accomodate these. module Data.ABC.Internal.Orphan abcNtkFromAigPhase :: (Aig_Man_t) -> IO ((Abc_Ntk_t)) abcNtkToDar :: Abc_Ntk_t -> Bool -> Bool -> IO Aig_Man_t -- | Incomplete. Binding of base/main/main.h for managing -- the global state of the ABC library. module Data.ABC.Internal.Main abcStart :: IO () abcStop :: IO () -- | Data.ABC.AIG defines a set of higher level functions for -- manipulating and-inverter graph networks (AIG) directly from -- ABC. This module should be imported qualified, e.g. -- -- 
--   import Data.ABC.AIG (AIG)
--   import qualified Data.ABC.AIG as AIG
--
-- | Warning: The Data.ABC.AIG module has known bugs -- (http:/github.comGaloisIncabcBridgeissues/4) for which -- solutions do not currently exist. Consider using Data.ABC.GIA -- instead. module Data.ABC.AIG data AIG s -- | Build a new, empty AIG graph newAIG :: IO (SomeGraph AIG) -- | Read an AIGER file as an AIG network readAiger :: FilePath -> IO (Network Lit AIG) -- | Proxy for building AIG networks proxy :: Proxy Lit AIG data Lit s true :: AIG s -> Lit s false :: AIG s -> Lit s -- | Convert the network referred to by an AIG manager into CNF format and -- write to a file, returning a mapping from ABC object IDs to CNF -- variable numbers. writeAIGManToCNFWithMapping :: Aig_Man_t -> FilePath -> IO (Vector Int) -- | Returns true is the literal is satisfiabile. checkSat' :: Ptr Abc_Ntk_t -> IO SatResult -- | A network is an and-invertor graph paired with it's outputs, thus -- representing a complete combinational circuit. data Network (l :: * -> *) (g :: * -> *) :: (* -> *) -> (* -> *) -> * [Network] :: Network l g -- | Get number of inputs associated with current network. networkInputCount :: Network l g -> IO Int -- | An And-Inverter-Graph is a data structure storing bit-level nodes. -- -- Graphs are and-inverter graphs, which contain a number of input -- literals and Boolean operations for creating new literals. Every -- literal is part of a specific graph, and literals from different -- networks may not be mixed. -- -- Both the types for literals and graphs must take a single phantom type -- for an arugment that is used to ensure that literals from different -- networks cannot be used in the same operation. class IsLit l => IsAIG (l :: * -> *) (g :: * -> *) | g -> l -- | Create a temporary graph, and use it to compute a result value. withNewGraph :: Proxy l g -> (forall s. g s -> IO a) -> IO a -- | Build a new graph instance, and packge it into the SomeGraph -- type that remembers the IsAIG implementation. newGraph :: Proxy l g -> IO (SomeGraph g) -- | Read an AIG from a file, assumed to be in Aiger format aigerNetwork :: Proxy l g -> FilePath -> IO (Network l g) -- | Get unique literal in graph representing constant true. trueLit :: g s -> l s -- | Get unique literal in graph representing constant false. falseLit :: g s -> l s -- | Generate a constant literal value constant :: g s -> Bool -> l s -- | Return if the literal is a fixed constant. If the literal is symbolic, -- return Nothing. asConstant :: g s -> l s -> Maybe Bool -- | Generate a fresh input literal newInput :: g s -> IO (l s) -- | Compute the logical and of two literals and :: g s -> l s -> l s -> IO (l s) -- | Build the conjunction of a list of literals ands :: g s -> [l s] -> IO (l s) -- | Compute the logical or of two literals or :: g s -> l s -> l s -> IO (l s) -- | Compute the logical equality of two literals eq :: g s -> l s -> l s -> IO (l s) -- | Compute the logical implication of two literals implies :: g s -> l s -> l s -> IO (l s) -- | Compute the exclusive or of two literals xor :: g s -> l s -> l s -> IO (l s) -- | Perform a mux (if-then-else on the bits). mux :: g s -> l s -> l s -> l s -> IO (l s) -- | Return number of inputs in the graph. inputCount :: g s -> IO Int -- | Get input at given index in the graph. getInput :: g s -> Int -> IO (l s) -- | Write network out to AIGER file. writeAiger :: FilePath -> Network l g -> IO () -- | Write network out to DIMACS CNF file. Returns vector mapping -- combinational inputs to CNF Variable numbers. writeCNF :: g s -> l s -> FilePath -> IO [Int] -- | Check if literal is satisfiable in network. checkSat :: g s -> l s -> IO SatResult -- | Perform combinational equivalence checking. cec :: Network l g -> Network l g -> IO VerifyResult -- | Evaluate the network on a set of concrete inputs. evaluator :: g s -> [Bool] -> IO (l s -> Bool) -- | Evaluate the network on a set of concrete inputs. evaluate :: Network l g -> [Bool] -> IO [Bool] -- | Examine the outermost structure of a literal to see how it was -- constructed litView :: g s -> l s -> IO (LitView (l s)) -- | Build an evaluation function over an AIG using the provided view -- function abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a) class IsLit (l :: * -> *) -- | Negate a literal. not :: l s -> l s -- | Tests whether two lits are identical. This is only a syntactic check, -- and may return false even if the two literals represent the same -- predicate. (===) :: l s -> l s -> Bool -- | Satisfiability check result. data SatResult :: * Unsat :: SatResult Sat :: ~[Bool] -> SatResult SatUnknown :: SatResult -- | Result of a verification check. data VerifyResult :: * Valid :: VerifyResult Invalid :: [Bool] -> VerifyResult VerifyUnknown :: VerifyResult -- | Some graph quantifies over the state phantom variable for a graph. data SomeGraph (g :: * -> *) :: (* -> *) -> * [SomeGraph] :: SomeGraph g instance GHC.Classes.Ord (Data.ABC.AIG.Lit s) instance Foreign.Storable.Storable (Data.ABC.AIG.Lit s) instance GHC.Classes.Eq (Data.ABC.AIG.Lit s) instance Data.AIG.Interface.IsLit Data.ABC.AIG.Lit instance Data.AIG.Trace.Traceable Data.ABC.AIG.Lit instance Data.AIG.Interface.IsAIG Data.ABC.AIG.Lit Data.ABC.AIG.AIG -- | GIA defines a set of functions for manipulating scalable -- and-inverter graph networks directly from ABC. This module should be -- imported qualified, e.g. -- -- 
--   import Data.ABC.GIA (GIA)
--   import qualified Data.ABC.GIA as GIA
--
-- -- Scalable and-inverter graphs are briefly described at the Berkeley -- Verification and Synthesis Research Center's website. -- http://bvsrc.org/research.html#AIG%20Package It is a more -- memory efficient method of storing AIG graphs. module Data.ABC.GIA -- | An and-invertor graph network in GIA form. data GIA s -- | Build a new empty GIA graph newGIA :: IO (SomeGraph GIA) -- | Represent a literal. data Lit s -- | Constant true node. true :: Lit s -- | Constant false node false :: Lit s proxy :: Proxy Lit GIA -- | Concrete datatype representing the ways an AIG can be constructed. data LitView a :: * -> * And :: ~a -> ~a -> LitView a NotAnd :: ~a -> ~a -> LitView a Input :: ~Int -> LitView a NotInput :: ~Int -> LitView a TrueLit :: LitView a FalseLit :: LitView a -- | Read an AIGER file into a GIA graph readAiger :: FilePath -> IO (Network Lit GIA) -- | Write an AIGER file with the given number of latches. If the number of -- latches is denoted by "n", then the last n inputs and last n outputs -- are treated as the latch input and outputs respectively. The other -- inputs and outputs represent primary inputs and outputs. writeAigerWithLatches :: FilePath -> Network Lit GIA -> Int -> IO () -- | Check a formula of the form Ex.Ay p(x,y). This function takes a -- network where input variables are used to represent both the -- existentially and the universally quantified variables. The -- existentially quantified variables must precede the universally -- quantified variables, and the number of extential variables is defined -- by an extra Int@ paramter. check_exists_forall :: GIA s -> Int -> Lit s -> [Bool] -> CInt -> IO (Either String SatResult) -- | A proxy is used to identify a specific AIG instance when calling -- methods that create new AIGs. data Proxy (l :: * -> *) (g :: * -> *) :: (* -> *) -> (* -> *) -> * -- | Some graph quantifies over the state phantom variable for a graph. data SomeGraph (g :: * -> *) :: (* -> *) -> * [SomeGraph] :: SomeGraph g class IsLit (l :: * -> *) -- | Negate a literal. not :: l s -> l s -- | Tests whether two lits are identical. This is only a syntactic check, -- and may return false even if the two literals represent the same -- predicate. (===) :: l s -> l s -> Bool -- | An And-Inverter-Graph is a data structure storing bit-level nodes. -- -- Graphs are and-inverter graphs, which contain a number of input -- literals and Boolean operations for creating new literals. Every -- literal is part of a specific graph, and literals from different -- networks may not be mixed. -- -- Both the types for literals and graphs must take a single phantom type -- for an arugment that is used to ensure that literals from different -- networks cannot be used in the same operation. class IsLit l => IsAIG (l :: * -> *) (g :: * -> *) | g -> l -- | Create a temporary graph, and use it to compute a result value. withNewGraph :: Proxy l g -> (forall s. g s -> IO a) -> IO a -- | Build a new graph instance, and packge it into the SomeGraph -- type that remembers the IsAIG implementation. newGraph :: Proxy l g -> IO (SomeGraph g) -- | Read an AIG from a file, assumed to be in Aiger format aigerNetwork :: Proxy l g -> FilePath -> IO (Network l g) -- | Get unique literal in graph representing constant true. trueLit :: g s -> l s -- | Get unique literal in graph representing constant false. falseLit :: g s -> l s -- | Generate a constant literal value constant :: g s -> Bool -> l s -- | Return if the literal is a fixed constant. If the literal is symbolic, -- return Nothing. asConstant :: g s -> l s -> Maybe Bool -- | Generate a fresh input literal newInput :: g s -> IO (l s) -- | Compute the logical and of two literals and :: g s -> l s -> l s -> IO (l s) -- | Build the conjunction of a list of literals ands :: g s -> [l s] -> IO (l s) -- | Compute the logical or of two literals or :: g s -> l s -> l s -> IO (l s) -- | Compute the logical equality of two literals eq :: g s -> l s -> l s -> IO (l s) -- | Compute the logical implication of two literals implies :: g s -> l s -> l s -> IO (l s) -- | Compute the exclusive or of two literals xor :: g s -> l s -> l s -> IO (l s) -- | Perform a mux (if-then-else on the bits). mux :: g s -> l s -> l s -> l s -> IO (l s) -- | Return number of inputs in the graph. inputCount :: g s -> IO Int -- | Get input at given index in the graph. getInput :: g s -> Int -> IO (l s) -- | Write network out to AIGER file. writeAiger :: FilePath -> Network l g -> IO () -- | Write network out to DIMACS CNF file. Returns vector mapping -- combinational inputs to CNF Variable numbers. writeCNF :: g s -> l s -> FilePath -> IO [Int] -- | Check if literal is satisfiable in network. checkSat :: g s -> l s -> IO SatResult -- | Perform combinational equivalence checking. cec :: Network l g -> Network l g -> IO VerifyResult -- | Evaluate the network on a set of concrete inputs. evaluator :: g s -> [Bool] -> IO (l s -> Bool) -- | Evaluate the network on a set of concrete inputs. evaluate :: Network l g -> [Bool] -> IO [Bool] -- | Examine the outermost structure of a literal to see how it was -- constructed litView :: g s -> l s -> IO (LitView (l s)) -- | Build an evaluation function over an AIG using the provided view -- function abstractEvaluateAIG :: g s -> (LitView a -> IO a) -> IO (l s -> IO a) -- | A network is an and-invertor graph paired with it's outputs, thus -- representing a complete combinational circuit. data Network (l :: * -> *) (g :: * -> *) :: (* -> *) -> (* -> *) -> * [Network] :: Network l g -- | Satisfiability check result. data SatResult :: * Unsat :: SatResult Sat :: ~[Bool] -> SatResult SatUnknown :: SatResult -- | Result of a verification check. data VerifyResult :: * Valid :: VerifyResult Invalid :: [Bool] -> VerifyResult VerifyUnknown :: VerifyResult instance GHC.Classes.Ord (Data.ABC.GIA.Lit s) instance Foreign.Storable.Storable (Data.ABC.GIA.Lit s) instance GHC.Classes.Eq (Data.ABC.GIA.Lit s) instance Data.AIG.Interface.IsLit Data.ABC.GIA.Lit instance Data.AIG.Trace.Traceable Data.ABC.GIA.Lit instance Data.AIG.Interface.IsAIG Data.ABC.GIA.Lit Data.ABC.GIA.GIA -- | Contains main interface to ABC, a system for sequential synthesis and -- verification. -- -- ABC provides many functions for manipulating Boolean networks. -- Internally, ABC provides two different ways of representing them: the -- older AIG interface, and a newer GIA interface. This -- library exposes both interfaces, along with a handful of functions for -- manipulating them. module Data.ABC -- | Initializes the ABC engine. This function may be safely called -- multiple times. Higher-level functions will automatically call this -- function, so it is only needed if using the FFI interfaces directly. initialize :: IO () -- | Deinitializes the ABC engine. ABC operations may not be run after this -- function is called. Use with care; this may cause ABC datatypes to -- stop working. unsafeCleanup :: IO () data AIG s type AIGLit = Lit -- | Proxy for AIG interface. -- | Warning: The Data.ABC.AIG module has known bugs -- (http:/github.comGaloisIncabcBridgeissues/4) for which -- solutions do not currently exist. Consider using Data.ABC.GIA -- instead. aigNetwork :: Proxy AIGLit AIG -- | Build a new, empty AIG graph newAIG :: IO (SomeGraph AIG) -- | Read an AIGER file as an AIG network. -- | Warning: The Data.ABC.AIG module has known bugs -- (http:/github.comGaloisIncabcBridgeissues/4) for which -- solutions do not currently exist. Consider using Data.ABC.GIA -- instead. readAigerAsAIG :: FilePath -> IO (Network AIGLit AIG) -- | An and-invertor graph network in GIA form. data GIA s type GIALit = Lit -- | Proxy for GIA interface. giaNetwork :: Proxy GIALit GIA -- | Build a new empty GIA graph newGIA :: IO (SomeGraph GIA) -- | Read an AIGER file as a GIA network. readAigerAsGIA :: FilePath -> IO (Network GIALit GIA)