Searched refs:Sat_MemHand (Results 1 – 4 of 4) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
| H A D | satClause.h | 101 static inline cla Sat_MemHand( Sat_Mem_t * p, int i, int k ) { return (i << p->nPageSize) |… in Sat_MemHand() function
371 if ( hLimit == Sat_MemHand(p, 1, 2) ) in Sat_MemCompactLearned()
376 assert( p->BookMarkH[1] >= Sat_MemHand(p, 1, 2) && p->BookMarkH[1] <= hLimit ); in Sat_MemCompactLearned()
424 assert( c->lits[c->size] == Sat_MemHand(p, iNew, kNew) ); in Sat_MemCompactLearned()
437 c->lits[c->size] = Sat_MemHand(p, iNew, kNew); in Sat_MemCompactLearned()
|
| H A D | satSolver2.c | 1465 …alues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) in sat_solver2_reducedb()
1485 …alues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) in sat_solver2_reducedb()
|
| H A D | satSolver3.c | 1538 …Values[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) in sat_solver3_reducedb()
|
| H A D | satSolver.c | 1573 …Values[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) in sat_solver_reducedb()
|