Lines Matching defs:c2c
264 vector<int> c2c;
292 const vec<Lit>& cc = clauses[c2c[resolvents[ii]]];
314 P.beginChain(c2c[resolvents[0]]+1); //+1 because modified Proof.C clause count is base 1
316 P.resolve(c2c[resolvents[ii]]+1, ~Lit(ps[ii-1]>>1,ps[ii-1]&1));
333 vec<Lit>& lits = clauses[c2c[ante]];
335 P.beginChain(c2c[ante]+1);
341 P.resolve(c2c[iter->second]+1, ~lits[i]);
355 vec<Lit>& lits = clauses[c2c[conf_id]];
356 P.beginChain(c2c[conf_id]+1);
361 P.resolve(c2c[iter->second]+1, ~lits[i]);
369 c2c[ci] = P.addRoot(clauses.last(),ci+1)-1;
379 c2c[ci] = addChain(resolvents,ci); // learnt
388 if (clauses[c2c[ante]].size()==1) {
393 clauses[c2c[ante]].copyTo(cc);
403 c2c[ci] = addVChain(lit>>1, (bool)(lit&1), ante, ci);
430 c2c(pclauses_.size(),-1) {}
437 clauses[c2c[conf_id]].copyTo(cc);