Searched refs:iLitOut (Results 1 – 5 of 5) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/wlc/ |
| H A D | wlcGraft.c | 454 int iLitOut = Vec_IntEntry( vMap, Abc_Lit2Var(iLitGia) ); in Sbc_ManWlcNodes2() local
455 if ( iLitOut == -1 ) in Sbc_ManWlcNodes2()
458 iLitOut = Abc_LitNotCond( iLitOut, Abc_LitIsCompl(iLitGia) ); in Sbc_ManWlcNodes2()
459 … %d with object %d (%s) bit %d (out of %d).\n", Abc_Lit2Var(iLitOut), Abc_LitIsCompl(iLitOut), i, … in Sbc_ManWlcNodes2()
487 int i, k, iLitGia, iLitOut, iFirst, nBits, iObjFound = -1; in Sbc_ManWlcNodes() local
497 iLitOut = Vec_IntEntry( vGia2Out, Abc_Lit2Var(iLitGia) ); in Sbc_ManWlcNodes()
498 if ( iLitOut == -1 ) in Sbc_ManWlcNodes()
500 iLitOut = Abc_LitNotCond( iLitOut, Abc_LitIsCompl(iLitGia) ); in Sbc_ManWlcNodes()
502 …lc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k, nBits, Abc_Lit2Var(iLitOut), Abc_LitIsCompl(iLitOut) ); in Sbc_ManWlcNodes()
503 Vec_IntPushOrder( vMatched, Abc_Lit2Var(iLitOut) ); in Sbc_ManWlcNodes()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/ |
| H A D | absGla.c | 652 static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut, int Pr… in Ga2_ManCnfAddDynamic() argument
664 ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut; in Ga2_ManCnfAddDynamic()
684 …c( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut, int ProofId ) in Ga2_ManCnfAddStatic() argument
694 ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut; in Ga2_ManCnfAddStatic()
796 int k, Lit, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f ); in Ga2_ManAddToAbsOneStatic() local
797 assert( iLitOut > 1 ); in Ga2_ManAddToAbsOneStatic()
801 iLitOut = Abc_LitNot( iLitOut ); in Ga2_ManAddToAbsOneStatic()
802 … sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 ); in Ga2_ManAddToAbsOneStatic()
817 …Sat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, fUseId ? Gia_Obj… in Ga2_ManAddToAbsOneStatic()
821 …Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj… in Ga2_ManAddToAbsOneStatic()
|
| H A D | absRef.c | 81 … sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId );
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcBmc3.c | 993 static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits[], int iLitOut ) in Saig_ManBmcAddClauses() argument
1006 ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut; in Saig_ManBmcAddClauses()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaJf.c | 129 void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vC… in Jf_ManGenCnf() argument
134 Vec_IntPush( vLits, Abc_LitNotCond(iLitOut, (uTruth == 0)) ); in Jf_ManGenCnf()
147 Vec_IntPush( vLits, Abc_LitNotCond(iLitOut, c) ); in Jf_ManGenCnf()
|