Searched refs:vAssump (Results 1 – 3 of 3) sorted by relevance
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
H A D | giaSatMap.c | 53 Vec_Int_t * vAssump; // assumptions (root nodes) member 414 p->vAssump = Vec_IntAlloc( 100 ); in Sbm_ManAlloc() 438 Vec_IntFree( p->vAssump ); in Sbm_ManStop() 480 Vec_IntClear( p->vAssump ); in Sbm_ManTestSat() 481 Vec_IntPush( p->vAssump, -1 ); in Sbm_ManTestSat() 484 Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); in Sbm_ManTestSat() 487 Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) ); in Sbm_ManTestSat() 497 …Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1)… in Sbm_ManTestSat() 500 …status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0… in Sbm_ManTestSat()
|
H A D | giaSatLut.c | 93 Vec_Int_t * vAssump; // literals member 165 p->vAssump = Vec_IntAlloc( 64 ); in Sbl_ManAlloc() 205 Vec_IntClear( p->vAssump ); in Sbl_ManClean() 244 Vec_IntFree( p->vAssump ); in Sbl_ManStop() 1017 Vec_IntClear( p->vAssump ); in Sbl_ManTestSat() 1018 Vec_IntPush( p->vAssump, -1 ); in Sbl_ManTestSat() 1021 Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); in Sbl_ManTestSat() 1024 Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) ); in Sbl_ManTestSat() 1037 …Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1)… in Sbl_ManTestSat() 1041 …status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), p->nBTLimi… in Sbl_ManTestSat()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
H A D | abcExact.c | 241 Vec_Int_t * vAssump; /* assumptions */ member 924 p->vAssump = Vec_IntAlloc( 10 ); in Ses_ManAlloc() 950 Vec_IntFree( pSes->vAssump ); in Ses_ManCleanLight() 1123 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 1 ) ); in Ses_ManGateCannotHaveChild() 1125 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ) ); in Ses_ManGateCannotHaveChild() 1213 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 ) ); in Ses_ManCreateClauses() 1214 … Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ) ); in Ses_ManCreateClauses() 1359 …Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 1 ) ); in Ses_ManCreateClauses() 1537 Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ) ); in Ses_ManCreateDepthClauses() 1580 …atus = sat_solver_solve( pSes->pSat, Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ),… in Ses_ManSolve() [all …]
|