Searched refs:unit_lits (Results 1 – 6 of 6) sorted by relevance
751 for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ ) in Saig_BmcSolveTargets()753 Lit = veci_begin(&p->pSat->unit_lits)[k]; in Saig_BmcSolveTargets()757 veci_resize(&p->pSat->unit_lits, 0); in Saig_BmcSolveTargets()
1691 for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ ) in Saig_ManBmcScalable()1693 Lit = veci_begin(&p->pSat->unit_lits)[k]; in Saig_ManBmcScalable()1697 veci_resize(&p->pSat->unit_lits, 0); in Saig_ManBmcScalable()
705 veci_push( &s->unit_lits, *begin ); in sat_solver3_record()1132 veci_new(&s->unit_lits); in sat_solver3_new()1197 veci_new(&s->unit_lits); in zsat_solver3_new_seed()1322 veci_delete(&s->unit_lits); in sat_solver3_delete()1470 Mem += s->unit_lits.cap * sizeof(int); in sat_solver3_memory()1900 veci_resize(&s->unit_lits, 0); in sat_solver3_solve_internal()
722 veci_push( &s->unit_lits, *begin ); in sat_solver_record()1158 veci_new(&s->unit_lits); in sat_solver_new()1223 veci_new(&s->unit_lits); in zsat_solver_new_seed()1353 veci_delete(&s->unit_lits); in sat_solver_delete()1505 Mem += s->unit_lits.cap * sizeof(int); in sat_solver_memory()1944 veci_resize(&s->unit_lits, 0); in sat_solver_solve_internal()
177 veci unit_lits; // variables whose activity has changed member
179 veci unit_lits; // variables whose activity has changed member