sat_solvers/minisat/Proof.C

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);