Lines Matching refs:chain_var
113 chain_var.clear();
122 if (next>=0) chain_var.push(x << 1);
123 else chain_var.push((x << 1) | 1); // HA: adding sign info to pivots
130 chain_var.push(index(p));
136 assert(chain_id.size() == chain_var.size() + 1);
142 trav->chain(chain_id, chain_var);
152 for (int i = 0; i < chain_var.size(); i++)
153 putUInt(fp, chain_var[i] + 1),
217 //HA: fill up chain_id and chain_var
219 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var,
222 void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var,
227 chain_var.clear();
238 chain_var.push(tmp - 1);
278 //parseChain(chain_id,chain_var,fp,tmp,id);
280 chain_var_stack.last().copyTo(chain_var); chain_var_stack.pop();
286 dst.resolve(chain_var[i-1] & 1 ? -1*chain_id[i] : chain_id[i],chain_var[i-1] >> 1);
292 for (int i=0;i<chain_var.size();i++)
293 fout << " " << chain_var[i] << " ";
318 parseChain(chain_id,chain_var,fp,tmp,id);
320 chain_var_stack.push(); chain_var.copyTo(chain_var_stack.last());
396 parseChain(chain_id,chain_var,fp,tmp,id,&fout);
398 parseChain(chain_id,chain_var,fp,tmp,id);
400 res_count+=chain_var.size();
401 if (chain_var.size() == 0)
405 trav.chain(chain_id, chain_var);