Home
last modified time | relevance | path

Searched refs:pvWatched (Results 1 – 4 of 4) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/msat/
H A DmsatClause.c61 Msat_ClauseVec_t ** pvWatched; in Msat_ClauseCreate() local
205 pvWatched = Msat_SolverReadWatchedArray( p ); in Msat_ClauseCreate()
206 Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC ); in Msat_ClauseCreate()
207 Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC ); in Msat_ClauseCreate()
228 Msat_ClauseVec_t ** pvWatched; in Msat_ClauseFree() local
229 pvWatched = Msat_SolverReadWatchedArray( p ); in Msat_ClauseFree()
231 Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); in Msat_ClauseFree()
233 Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); in Msat_ClauseFree()
H A DmsatSolverApi.c55 …ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; } in Msat_SolverReadWatchedArray()
195 p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc ); in Msat_SolverAlloc()
197 p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); in Msat_SolverAlloc()
265 p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc ); in Msat_SolverResize()
267 p->pvWatched[i] = Msat_ClauseVecAlloc( 16 ); in Msat_SolverResize()
342 Msat_ClauseVecClear( p->pvWatched[i] ); in Msat_SolverClean()
413 Msat_ClauseVecFree( p->pvWatched[i] ); in Msat_SolverFree()
414 ABC_FREE( p->pvWatched ); in Msat_SolverFree()
H A DmsatSolverSearch.c219 Msat_ClauseVec_t ** pvWatched = p->pvWatched; in Msat_SolverPropagate() local
230 nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] ); in Msat_SolverPropagate()
231 pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] ); in Msat_SolverPropagate()
253 Msat_ClauseVecShrink( pvWatched[Lit], j ); in Msat_SolverPropagate()
261 Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] ); in Msat_SolverPropagate()
265 Msat_ClauseVecShrink( pvWatched[Lit], j ); in Msat_SolverPropagate()
H A DmsatInt.h112 …Msat_ClauseVec_t ** pvWatched; // 'pvWatched[lit]' is a list of constraints watching 'lit' (will… member