Lines Matching defs:id
68 id_counter = 1; //HA: to save sign info on-the-fly, unit_id uses -ve clause id's to indicate
220 File& fp, uint64 tmp, ClauseId id, std::ofstream* fout) {
223 File& fp, uint64 tmp, ClauseId id) {
228 chain_id.push(id - (tmp >> 1));
231 if (NULL != fout) (*fout) << "B " << (id - (tmp >> 1)) << " ";
246 chain_id.push(id - tmp);
249 if (NULL != fout) (*fout) << " " << (id-tmp) << " ";
262 vec<ClauseId> c2c(goal+2,-1); // c2c[old_id] is new id in compressed proof of clause old_id
269 ClauseId id = dfs_stack.last();
271 id = dfs_stack.last();
272 switch (c2c[id]) {
275 //int64 pos = c2fp[id];
278 //parseChain(chain_id,chain_var,fp,tmp,id);
282 for (int i=0; i<sz; i++) // redirect chain_id[i]'s to new id's
287 c2c[id] = dst.endChain();
291 fout << c2c[id] << " B [" << id << "] : ";
304 int64 pos = c2fp[id];
309 c2c[id] = dst.addRoot(clause,orig_root_id);
313 fout << c2c[id] << " R [" << ((tmp>>1)-1) << "]\n"; //debug
318 parseChain(chain_id,chain_var,fp,tmp,id);
324 c2c[id] = -2; // means a chain that has been visited but not written out yet
383 for(ClauseId id = 1; id <= goal; id++){
396 parseChain(chain_id,chain_var,fp,tmp,id,&fout);
398 parseChain(chain_id,chain_var,fp,tmp,id);
402 id--, // (no new clause introduced)