Home
last modified time | relevance | path

Searched refs:vAssump (Results 1 – 3 of 3) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/
H A DgiaSatMap.c53 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 DgiaSatLut.c93 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 DabcExact.c241 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 …]