| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/dch/ |
| H A D | dchCnf.c | 47 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; in Dch_AddClausesMux() local
53 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Dch_AddClausesMux()
57 VarT = Dch_ObjSatNum(p,Aig_Regular(pNodeT)); in Dch_AddClausesMux()
60 fCompT = Aig_IsComplement(pNodeT); in Dch_AddClausesMux()
77 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); in Dch_AddClausesMux()
88 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); in Dch_AddClausesMux()
134 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); in Dch_AddClausesMux()
145 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); in Dch_AddClausesMux()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/ssw/ |
| H A D | sswCnf.c | 106 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; in Ssw_AddClausesMux() local
112 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Ssw_AddClausesMux()
116 VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT)); in Ssw_AddClausesMux()
119 fCompT = Aig_IsComplement(pNodeT); in Ssw_AddClausesMux()
136 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); in Ssw_AddClausesMux()
147 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); in Ssw_AddClausesMux()
193 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); in Ssw_AddClausesMux()
204 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); in Ssw_AddClausesMux()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/ |
| H A D | fraCnf.c | 48 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; in Fra_AddClausesMux() local
54 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Fra_AddClausesMux()
58 VarT = Fra_ObjSatNum(Aig_Regular(pNodeT)); in Fra_AddClausesMux()
61 fCompT = Aig_IsComplement(pNodeT); in Fra_AddClausesMux()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abcSat.c | 288 int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT,… in Abc_NtkClauseMux() argument
298 VarT = (int)(ABC_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy; in Abc_NtkClauseMux()
306 fCompT = Abc_ObjIsComplement(pNodeT); in Abc_NtkClauseMux()
471 Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; in Abc_NtkMiterSatCreateInt() local
537 pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); in Abc_NtkMiterSatCreateInt()
540 Vec_PtrPush( vSuper, pNodeT ); in Abc_NtkMiterSatCreateInt()
554 if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) ) in Abc_NtkMiterSatCreateInt()
|
| H A D | abcBalance.c | 456 Abc_Obj_t * pNodeC, * pNodeT, * pNodeE; in Abc_NodeFindCone_rec() local
466 pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); in Abc_NodeFindCone_rec()
468 Vec_PtrPushUnique( vNodes, Abc_ObjRegular(pNodeT) ); in Abc_NodeFindCone_rec()
|
| H A D | abcIf.c | 788 Abc_Obj_t * pNodeC, * pNodeT, * pNodeE; in Abc_NtkMarkMux() local
798 pNodeC = Abc_NodeRecognizeMux( pDriver, &pNodeT, &pNodeE ); in Abc_NtkMarkMux()
820 *ppNode2 = Abc_ObjRegular(pNodeT); in Abc_NtkMarkMux()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaSupp.c | 425 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; in Gia_Min2AddClausesMux() local
431 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Gia_Min2AddClausesMux()
435 VarT = Gia_Min2ObjSatId(p, Gia_Regular(pNodeT)); in Gia_Min2AddClausesMux()
438 fCompT = Gia_IsComplement(pNodeT); in Gia_Min2AddClausesMux()
455 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); in Gia_Min2AddClausesMux()
466 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); in Gia_Min2AddClausesMux()
512 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); in Gia_Min2AddClausesMux()
523 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); in Gia_Min2AddClausesMux()
|
| H A D | giaSweeper.c | 545 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; in Gia_ManAddClausesMux() local
550 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Gia_ManAddClausesMux()
554 LitT = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeT) ); in Gia_ManAddClausesMux()
|
| H A D | giaUtil.c | 1055 Gia_Obj_t * pNodeT, * pNodeE; in Gia_ObjRecognizeMuxLits() local
1056 Gia_Obj_t * pCtrl = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Gia_ObjRecognizeMuxLits()
1058 *iLitT = Gia_Obj2Lit( p, pNodeT ); in Gia_ObjRecognizeMuxLits()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/cec/ |
| H A D | cecSolve.c | 66 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; in Cec_AddClausesMux() local
72 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Cec_AddClausesMux()
76 VarT = Cec_ObjSatNum(p,Gia_Regular(pNodeT)); in Cec_AddClausesMux()
79 fCompT = Gia_IsComplement(pNodeT); in Cec_AddClausesMux()
96 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); in Cec_AddClausesMux()
107 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); in Cec_AddClausesMux()
153 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); in Cec_AddClausesMux()
164 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); in Cec_AddClausesMux()
|
| H A D | cecSatG.c | 125 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; in Cec3_AddClausesMux() local
131 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Cec3_AddClausesMux()
135 VarT = Cec3_ObjSatId(p, Gia_Regular(pNodeT)); in Cec3_AddClausesMux()
138 fCompT = Gia_IsComplement(pNodeT); in Cec3_AddClausesMux()
155 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); in Cec3_AddClausesMux()
166 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); in Cec3_AddClausesMux()
212 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); in Cec3_AddClausesMux()
223 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); in Cec3_AddClausesMux()
|
| H A D | cecSat.c | 122 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; in Cec2_AddClausesMux() local
128 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Cec2_AddClausesMux()
132 VarT = Cec2_ObjSatId(p, Gia_Regular(pNodeT)); in Cec2_AddClausesMux()
135 fCompT = Gia_IsComplement(pNodeT); in Cec2_AddClausesMux()
152 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); in Cec2_AddClausesMux()
163 if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); in Cec2_AddClausesMux()
209 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); in Cec2_AddClausesMux()
220 if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); in Cec2_AddClausesMux()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/aig/ |
| H A D | aigUtil.c | 1498 Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC; in Aig_ManMuxesDeref() local
1502 if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) ) in Aig_ManMuxesDeref()
1504 pNodeT->nRefs--; in Aig_ManMuxesDeref()
1509 pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE ); in Aig_ManMuxesDeref()
1528 Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC; in Aig_ManMuxesRef() local
1532 if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) ) in Aig_ManMuxesRef()
1534 pNodeT->nRefs++; in Aig_ManMuxesRef()
1539 pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE ); in Aig_ManMuxesRef()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/ssc/ |
| H A D | sscSat.c | 51 Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; in Gia_ManAddClausesMux() local
56 pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Gia_ManAddClausesMux()
60 LitT = Ssc_ObjSatLit( p, Gia_Obj2Lit(p->pFraig,pNodeT) ); in Gia_ManAddClausesMux()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fraig/ |
| H A D | fraigSat.c | 1216 Fraig_Node_t * pNodeI, * pNodeT, * pNodeE; in Fraig_SupergateAddClausesMux() local
1222 pNodeI = Fraig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); in Fraig_SupergateAddClausesMux()
1226 VarT = Fraig_Regular(pNodeT)->Num; in Fraig_SupergateAddClausesMux()
1229 fCompT = Fraig_IsComplement(pNodeT); in Fraig_SupergateAddClausesMux()
|
| H A D | fraig.h | 187 … Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_Node_t * pNodeT, Fraig_Node_t * pN…
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/map/fpga/ |
| H A D | fpga.h | 134 extern Fpga_Node_t * Fpga_NodeMux( Fpga_Man_t * p, Fpga_Node_t * pNode, Fpga_Node_t * pNodeT, Fpg…
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/ivy/ |
| H A D | ivyFraig.c | 2354 Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE; in Ivy_FraigAddClausesMux() local
2360 pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); in Ivy_FraigAddClausesMux()
2364 VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT)); in Ivy_FraigAddClausesMux()
2367 fCompT = Ivy_IsComplement(pNodeT); in Ivy_FraigAddClausesMux()
|