/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/msat/ |
H A D | msatSolverApi.c | 168 p->nVarsAlloc = nVarsAlloc; in Msat_SolverAlloc() 182 for ( i = 0; i < p->nVarsAlloc; i++ ) in Msat_SolverAlloc() 190 for ( i = 0; i < p->nVarsAlloc; i++ ) in Msat_SolverAlloc() 196 for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) in Msat_SolverAlloc() 205 for ( i = 0; i < p->nVarsAlloc; i++ ) in Msat_SolverAlloc() 215 for ( i = 0; i < p->nVarsAlloc; i++ ) in Msat_SolverAlloc() 246 nVarsAllocOld = p->nVarsAlloc; in Msat_SolverResize() 247 p->nVarsAlloc = nVarsAlloc; in Msat_SolverResize() 314 assert( p->nVarsAlloc >= nVars ); in Msat_SolverClean() 412 for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) in Msat_SolverFree() [all …]
|
H A D | msatOrderJ.c | 59 int nVarsAlloc; // the number of variables allocated member 108 Msat_OrderSetBounds( p, pSat->nVarsAlloc ); in Msat_OrderAlloc() 127 if ( p->nVarsAlloc < nVarsMax ) in Msat_OrderSetBounds() 130 for ( i = p->nVarsAlloc; i < nVarsMax; i++ ) in Msat_OrderSetBounds() 135 p->nVarsAlloc = nVarsMax; in Msat_OrderSetBounds() 311 assert( Var < p->nVarsAlloc ); in Msat_OrderVarAssigned() 349 assert( Var < p->nVarsAlloc ); in Msat_OrderVarUnassigned()
|
H A D | msatSolverCore.c | 47 if ( p->nVars == p->nVarsAlloc ) in Msat_SolverAddVar() 48 Msat_SolverResize( p, 2 * p->nVarsAlloc ); in Msat_SolverAddVar()
|
H A D | msat.h | 114 extern void Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc ); 143 …n void Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc );
|
H A D | msatOrderH.c | 86 Msat_OrderSetBounds( p, pSat->nVarsAlloc ); in Msat_OrderAlloc()
|
H A D | msatInt.h | 116 int nVarsAlloc; // the maximum allowed number of variables member
|
H A D | msatSolverSearch.c | 388 for ( i = 0; i < p->nVarsAlloc; i++ ) in Msat_SolverRemoveLearned()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/proof/ |
H A D | pr.c | 78 int nVarsAlloc; // the allocated size of arrays member 121 extern Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ); 141 Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ) in Pr_ManAlloc() argument 148 Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 ); in Pr_ManAlloc() 176 if ( p->nVarsAlloc < nVarsNew ) in Pr_ManResize() 178 int nVarsAllocOld = p->nVarsAlloc; in Pr_ManResize() 180 if ( p->nVarsAlloc == 0 ) in Pr_ManResize() 181 p->nVarsAlloc = 1; in Pr_ManResize() 182 while ( p->nVarsAlloc < nVarsNew ) in Pr_ManResize() 183 p->nVarsAlloc *= 2; in Pr_ManResize() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | satInter.c | 49 int nVarsAlloc; // the allocated size of var arrays member 212 if ( p->nVarsAlloc < p->pCnf->nVars ) in Int_ManResize() 215 if ( p->nVarsAlloc == 0 ) in Int_ManResize() 216 p->nVarsAlloc = 1; in Int_ManResize() 217 while ( p->nVarsAlloc < p->pCnf->nVars ) in Int_ManResize() 218 p->nVarsAlloc *= 2; in Int_ManResize() 220 p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); in Int_ManResize() 221 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Int_ManResize() 222 p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); in Int_ManResize() 223 p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); in Int_ManResize() [all …]
|
H A D | satInterA.c | 49 int nVarsAlloc; // the allocated size of var arrays member 191 if ( p->nVarsAlloc < p->pCnf->nVars ) in Inta_ManResize() 194 if ( p->nVarsAlloc == 0 ) in Inta_ManResize() 195 p->nVarsAlloc = 1; in Inta_ManResize() 196 while ( p->nVarsAlloc < p->pCnf->nVars ) in Inta_ManResize() 197 p->nVarsAlloc *= 2; in Inta_ManResize() 199 p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); in Inta_ManResize() 200 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Inta_ManResize() 201 p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); in Inta_ManResize() 202 p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); in Inta_ManResize() [all …]
|
H A D | satInterP.c | 48 int nVarsAlloc; // the allocated size of var arrays member 130 if ( p->nVarsAlloc < p->pCnf->nVars ) in Intp_ManResize() 133 if ( p->nVarsAlloc == 0 ) in Intp_ManResize() 134 p->nVarsAlloc = 1; in Intp_ManResize() 135 while ( p->nVarsAlloc < p->pCnf->nVars ) in Intp_ManResize() 136 p->nVarsAlloc *= 2; in Intp_ManResize() 138 p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); in Intp_ManResize() 139 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Intp_ManResize() 140 p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); in Intp_ManResize() 142 p->pReasons = ABC_REALLOC(Sto_Cls_t *, p->pReasons, p->nVarsAlloc ); in Intp_ManResize() [all …]
|
H A D | satInterB.c | 49 int nVarsAlloc; // the allocated size of var arrays member 196 if ( p->nVarsAlloc < p->pCnf->nVars ) in Intb_ManResize() 199 if ( p->nVarsAlloc == 0 ) in Intb_ManResize() 200 p->nVarsAlloc = 1; in Intb_ManResize() 201 while ( p->nVarsAlloc < p->pCnf->nVars ) in Intb_ManResize() 202 p->nVarsAlloc *= 2; in Intb_ManResize() 204 p->pTrail = ABC_REALLOC(lit, p->pTrail, p->nVarsAlloc ); in Intb_ManResize() 205 p->pAssigns = ABC_REALLOC(lit, p->pAssigns, p->nVarsAlloc ); in Intb_ManResize() 206 p->pSeens = ABC_REALLOC(char, p->pSeens, p->nVarsAlloc ); in Intb_ManResize() 207 p->pVarTypes = ABC_REALLOC(int, p->pVarTypes, p->nVarsAlloc ); in Intb_ManResize() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fraig/ |
H A D | fraigSat.c | 750 int nVarsAlloc; in Fraig_PrepareCones() local 756 nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed); in Fraig_PrepareCones() 757 Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 ); in Fraig_PrepareCones() 879 int nVarsAlloc; in Fraig_OrderVariables() local 888 nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed); in Fraig_OrderVariables() 889 Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 ); in Fraig_OrderVariables()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
H A D | giaSatMap.c | 347 int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1), nVarsReal; in Sbm_AddCardinSolver() local 350 sat_solver_setnvars( pSat, nVarsAlloc ); in Sbm_AddCardinSolver() 352 assert( nVarsReal == nVarsAlloc ); in Sbm_AddCardinSolver()
|