Lines Matching defs:ps
274 void update(vector<int>& ps, int lit, vector<int>& r1) {
282 ps.push_back(flag); // record pivot in ps
288 vec<Lit>& res, vector<int>& ps) {
295 update(ps,index(cc[jj]),r1);
311 vector<int> ps; // pivots
312 get_res(resolvents,res,ps);
313 assert(ps.size()==resolvents.size()-1);
316 P.resolve(c2c[resolvents[ii]]+1, ~Lit(ps[ii-1]>>1,ps[ii-1]&1));