Home
last modified time | relevance | path

Searched refs:nVarsAlloc (Results 1 – 14 of 14) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/msat/
H A DmsatSolverApi.c168 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 DmsatOrderJ.c59 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 DmsatSolverCore.c47 if ( p->nVars == p->nVarsAlloc ) in Msat_SolverAddVar()
48 Msat_SolverResize( p, 2 * p->nVarsAlloc ); in Msat_SolverAddVar()
H A Dmsat.h114 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 DmsatOrderH.c86 Msat_OrderSetBounds( p, pSat->nVarsAlloc ); in Msat_OrderAlloc()
H A DmsatInt.h116 int nVarsAlloc; // the maximum allowed number of variables member
H A DmsatSolverSearch.c388 for ( i = 0; i < p->nVarsAlloc; i++ ) in Msat_SolverRemoveLearned()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/proof/
H A Dpr.c78 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 DsatInter.c49 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 DsatInterA.c49 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 DsatInterP.c48 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 DsatInterB.c49 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 DfraigSat.c750 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 DgiaSatMap.c347 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()