Data.ABC.Internal.CEC

Comprehensive binding of aig/cec/cec.h for performing combinational equivalence checking of scalable and-inverter graphs (GIA).

Types

Storable types

data Cec_ParCec_t_

Constructors

Cec_ParCec_t_

Fields

nBTLimit'Cec_ParCec :: Int

conflict limit at a node

nTimeLimit'Cec_ParCec :: Int

the runtime limit in seconds (added prefix n)

fUseSmartCnf'Cec_ParCec :: Bool

use smart CNF computation

fRewriting'Cec_ParCec :: Bool

enables AIG rewriting

fVeryVerbose'Cec_ParCec :: Bool

very verbose stats

fVerbose'Cec_ParCec :: Bool

verbose stats

iOutFail'Cec_ParCec :: Int

the number of failed output

Instances

Eq Cec_ParCec_t_

Read Cec_ParCec_t_

Show Cec_ParCec_t_

Storable Cec_ParCec_t_

data Cec_ParSat_t_

Constructors

Cec_ParSat_t_

Fields

nBTLimit'Cec_ParSat :: CInt

nSatVarMax'Cec_ParSat :: CInt

nCallsRecycle'Cec_ParSat :: CInt

fNonChrono'Cec_ParSat :: Bool

fPolarFlip'Cec_ParSat :: Bool

fCheckMiter'Cec_ParSat :: Bool

fLearnCls'Cec_ParSat :: Bool

fVerbose'Cec_ParSat :: Bool

Instances

Eq Cec_ParSat_t_

Read Cec_ParSat_t_

Show Cec_ParSat_t_

Storable Cec_ParSat_t_

Functions

cecCec.c

cecManVerify :: Gia_Man_t -> Cec_ParCec_t_ -> IO CInt

cecCore.c

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 ()