Lines Matching refs:solver_dlevel
35 #define L_ind solver_dlevel(s)*3+3,solver_dlevel(s)
104 static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); }
348 assert(solver_dlevel(s) == 0);
421 levels [v] = solver_dlevel(s);
449 if (solver_dlevel(s) <= level)
593 if (levels[lit_var(q)] == solver_dlevel(s))
612 if (levels[lit_var(q)] == solver_dlevel(s))
811 assert(s->root_level == solver_dlevel(s));
829 if (solver_dlevel(s) == s->root_level){
854 if (solver_dlevel(s) == 0)
1131 assert(solver_dlevel(s) == 0);
1187 s->root_level = solver_dlevel(s);