21 #ifndef ABC__aig__llb__llbInt_h
22 #define ABC__aig__llb__llbInt_h
174 abctime TimeTarget,
int fBackward,
int fReorder,
int fVerbose );
182 DdManager * dd,
DdNode * bCurrent,
int fReorder,
int fVerbose,
int * pOrder );
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
DdNode * Llb_NonlinComputeInitState(Aig_Man_t *pAig, DdManager *dd)
void Llb_ManPrepareGroups(Llb_Man_t *pMan)
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
void Llb_MtrPrint(Llb_Mtr_t *p, int fOrder)
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
void Llb_ManPrepareVarLimits(Llb_Man_t *p)
DdNode * Llb_ImgComputeImage(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
Vec_Int_t * Llb_ManDeriveConstraints(Aig_Man_t *p)
FUNCTION DECLARATIONS ///.
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
void Llb_ManDumpReached(DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_ Gia_ParLlb_t
INCLUDES ///.
void Llb_ManGroupStop(Llb_Grp_t *p)
DdManager * Llb_NonlinImageStart(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, int *pOrder, int fFirst, abctime TimeTarget)
void Llb_NonlinImageQuit()
void Llb_ManStop(Llb_Man_t *p)
Vec_Int_t * Llb_DriverCollectNs(Aig_Man_t *pAig, Vec_Int_t *vDriRefs)
Vec_Int_t * Llb_DriverCountRefs(Aig_Man_t *p)
DECLARATIONS ///.
void Llb_ManPrintEntries(Aig_Man_t *p, Vec_Int_t *vCands)
DdManager * Llb_ImgPartition(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
int Llb_ManTracePaths(Aig_Man_t *p, Aig_Obj_t *pPivot)
DdNode * Llb_NonlinImageCompute(DdNode *bCurrent, int fReorder, int fDrop, int fVerbose, int *pOrder)
DdManager * Llb_DriverLastPartition(Aig_Man_t *p, Vec_Int_t *vVarsNs, abctime TimeTarget)
DdNode * Llb_NonlinImage(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, DdManager *dd, DdNode *bCurrent, int fReorder, int fVerbose, int *pOrder)
int Llb_ManReachabilityWithHints(Llb_Man_t *p)
DdNode * Llb_DriverPhaseCube(Aig_Man_t *pAig, Vec_Int_t *vDriRefs, DdManager *dd)
static int Vec_IntEntry(Vec_Int_t *p, int i)
Llb_Grp_t * Llb_ManGroupAlloc(Llb_Man_t *pMan)
DECLARATIONS ///.
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
void Llb_ImgQuantifyReset(Vec_Ptr_t *vDdMans)
Llb_Grp_t * Llb_ManGroupsCombine(Llb_Grp_t *p1, Llb_Grp_t *p2)
Vec_Ptr_t * Llb_ImgSupports(Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
FUNCTION DEFINITIONS ///.
#define ABC_NAMESPACE_HEADER_END
void Llb4_Nonlin4Sweep(Aig_Man_t *pAig, int nSweepMax, int nClusterMax, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int fVerbose)
Vec_Int_t * Llb_ManMarkPivotNodes(Aig_Man_t *p, int fUseInternal)
void Llb_ImgQuantifyFirst(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
static int Llb_ObjBddVar(Vec_Int_t *vOrder, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
int Llb_ManModelCheckAigWithHints(Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars)
int Llb_CoreExperiment(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
DdNode * Llb_Nonlin4Image(DdManager *dd, Vec_Ptr_t *vParts, DdNode *bCurrent, Vec_Int_t *vVars2Q)
void Llb_MtrVerifyMatrix(Llb_Mtr_t *p)
void Llb_MtrSchedule(Llb_Mtr_t *p)
Llb_Man_t * Llb_ManStart(Aig_Man_t *pAigGlo, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Llb_Grp_t * Llb_ManGroupCreateFromCuts(Llb_Man_t *pMan, Vec_Int_t *vCut1, Vec_Int_t *vCut2)
int Llb_ManReachability(Llb_Man_t *p, Vec_Int_t *vHints, DdManager **pddGlo)
Abc_Cex_t * Llb4_Nonlin4TransformCex(Aig_Man_t *pAig, Vec_Ptr_t *vStates, int iCexPo, int fVerbose)
DECLARATIONS ///.
int Llb_ManModelCheckAig(Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars, Vec_Int_t *vHints, DdManager **pddGlo)
Vec_Ptr_t * Llb_ManFlow(Aig_Man_t *p, Vec_Ptr_t *vSources, int *pnFlow)
static int Aig_ObjId(Aig_Obj_t *pObj)
DdNode * Llb_BddQuantifyPis(Aig_Man_t *pInit, DdManager *dd, DdNode *bFunc)
void Llb_ImgSchedule(Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Vec_Int_t * Llb_DriverCollectCs(Aig_Man_t *pAig)
Llb_Mtr_t * Llb_MtrCreate(Llb_Man_t *p)
typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_ Llb_Man_t
INCLUDES ///.
void Llb_MtrFree(Llb_Mtr_t *p)
void Llb_MtrPrintMatrixStats(Llb_Mtr_t *p)
DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
void Llb_ManPrepareVarMap(Llb_Man_t *p)
DECLARATIONS ///.
void Llb_ManCluster(Llb_Mtr_t *p)