Cross Reference: /pkg/src/modules/solver/solver.c

Lines Matching refs:lit_neg
305     assert(lit_neg(begin[0]) < s->size*2);
306     assert(lit_neg(begin[1]) < s->size*2);
308     //vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
309     //vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
311     vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
312     vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
320     assert(lit_neg(lits[0]) < s->size*2);
321     assert(lit_neg(lits[1]) < s->size*2);
323     //vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
324     //vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
327     vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
328     vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
628     *veci_begin(learnt) = lit_neg(p);
710                     (clause_begin(confl))[1] = lit_neg(p);
724                 false_lit = lit_neg(p);
745                             vecp_push(solver_read_wlist(s,lit_neg(lits[1])),*i);
877                     veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
885             assume(s,lit_neg(toLit(next)));
1005     vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
1006     vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
1017       vecp_replace(solver_read_wlist(s, lit_neg(old->lits[0])), old, new);
1027       vecp_replace(solver_read_wlist(s, lit_neg(old->lits[0])), old, new);
1102         if (*i == lit_neg(last) || sig == values[lit_var(*i)])