Searched refs:hLearn1 (Results 1 – 3 of 3) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaCSat2.c | 1258 int hClause, hLearn0, hLearn1, iVar, iDecLit; in Cbs2_ManSolve1_rec() local
1294 if ( !(hLearn1 = Cbs2_ManSolve1_rec( p, Level+1 )) ) in Cbs2_ManSolve1_rec()
1296 if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) ) in Cbs2_ManSolve1_rec()
1297 return hLearn1; in Cbs2_ManSolve1_rec()
1298 hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 ); in Cbs2_ManSolve1_rec()
1312 int hClause, hLearn0, hLearn1, iVar, iDecLit, iDecLit2; in Cbs2_ManSolve2_rec() local
1358 if ( !(hLearn1 = Cbs2_ManSolve2_rec( p, Level+1 )) ) in Cbs2_ManSolve2_rec()
1360 if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) ) in Cbs2_ManSolve2_rec()
1361 return hLearn1; in Cbs2_ManSolve2_rec()
1362 hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 ); in Cbs2_ManSolve2_rec()
|
| H A D | giaCSat.c | 879 int hClause, hLearn0, hLearn1; in Cbs_ManSolve_rec() local
922 if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) ) in Cbs_ManSolve_rec()
924 if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) ) in Cbs_ManSolve_rec()
925 return hLearn1; in Cbs_ManSolve_rec()
926 hClause = Cbs_ManResolve( p, Level, hLearn0, hLearn1 ); in Cbs_ManSolve_rec()
|
| H A D | giaCTas.c | 1289 int hClause, hLearn0, hLearn1; in Tas_ManSolve_rec() local
1340 if ( !(hLearn1 = Tas_ManSolve_rec( p, Level+1 )) ) in Tas_ManSolve_rec()
1342 if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) ) in Tas_ManSolve_rec()
1343 return hLearn1; in Tas_ManSolve_rec()
1344 hClause = Tas_ManResolve( p, Level, hLearn0, hLearn1 ); in Tas_ManSolve_rec()
|