Lines Matching defs:ps
45 | newClause : (ps : const vec<Lit>&) (learnt : bool) (id : ClauseId) -> [void]
52 | ps - The new clause as a vector of literals.
53 | learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the
98 const vec<Lit>& ps = learnt ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals.
100 if (ps.size() == 0){
103 }else if (ps.size() == 1){
107 unit_id[var(ps[0])] = (sign(ps[0])) ? -id : id; //HA: sign info
108 if (!enqueue(ps[0]))
113 Clause* c = Clause_new(learnt, ps, id);
118 int max = level[var(ps[1])];
119 for (int i = 2; i < ps.size(); i++)
120 if (level[var(ps[i])] > max)
121 max = level[var(ps[i])],
123 (*c)[1] = ps[max_i];
124 (*c)[max_i] = ps[1];