Home
last modified time | relevance | path

Searched refs:vRootLits (Results 1 – 8 of 8) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/acec/
H A DacecPo.c530 Vec_IntForEachEntry( vRootLits, iLit, i ) in Gia_PolynBuildNew2()
532 int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra ); in Gia_PolynBuildNew2()
533 … Vec_IntFill( vTempC, 1, (fSigned && i == Vec_IntSize(vRootLits)-1-nExtra) ? -Value : Value ); in Gia_PolynBuildNew2()
660 … %d to %d rank %d.\n", nExtra, Vec_IntSize(vRootLits)-nExtra, Vec_IntSize(vRootLits)-1, Vec_IntSiz… in Gia_PolynBuildNew()
678 OutLit = Vec_IntEntry(vRootLits, Entry); in Gia_PolynBuildNew()
701 Vec_IntForEachEntry( vRootLits, iLit, i ) in Gia_PolynBuildNew()
703 int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra ); in Gia_PolynBuildNew()
705 if ( fSigned && i >= Vec_IntSize(vRootLits)-nExtra-1 ) in Gia_PolynBuildNew()
807 Vec_Int_t * vRootLits = Vec_IntAlloc( Gia_ManCoNum(pGia) ); in Gia_PolynBuild2Test() local
843 Vec_IntPush( vRootLits, Gia_ObjFaninLit0p(pGia, pObj) ); in Gia_PolynBuild2Test()
[all …]
H A DacecNorm.c127 …t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Int_t * vRootLits ) in Acec_BuildTree() argument
133 if ( vRootLits ) in Acec_BuildTree()
134 Vec_IntForEachEntry( vRootLits, iLit, i ) in Acec_BuildTree()
182 Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) in Acec_InsertBox()
H A DacecInt.h46 Vec_Wec_t * vRootLits; // root literals by rank member
77 …Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
H A DacecCl.c356 Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart ) in Acec_RewriteTop()
361 Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart ) in Acec_RewriteTop()
375 if ( i+1 < Vec_WecSize(pBox->vRootLits) ) in Acec_RewriteTop()
376 Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] ); in Acec_RewriteTop()
378 Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] ); in Acec_RewriteTop()
H A DacecXor.c303 pBox->vRootLits = Vec_WecStart( MaxRank + 0 ); in Acec_FindBox()
346 …Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_S… in Acec_FindBox()
361 vLevel = Vec_WecEntry( pBox->vRootLits, Vec_WecSize(pBox->vRootLits)-1 ); in Acec_FindBox()
367 Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) in Acec_FindBox()
H A DacecTree.c49 Vec_WecFreeP( &pBox->vRootLits ); in Acec_BoxFree()
593 Vec_WecPrintLits( pBox->vRootLits ); in Acec_TreePrintBox()
620 pBox->vRootLits = Vec_WecStart( MaxRank + 2 ); in Acec_CreateBox()
671 …Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_S… in Acec_CreateBox()
681 Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) in Acec_CreateBox()
734 Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) ); in Acec_CreateBoxTest()
767 Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) ); in Acec_DeriveBox()
H A DacecMult.c343 Vec_Int_t * Acec_MultDetectInputs1( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits ) in Acec_MultDetectInputs1() argument
431 Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits ) in Acec_MultDetectInputs() argument
H A DacecCore.c404 …Box1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits ); in Acec_MatchBoxes()