sat_solvers/minisat/Proof.C

43     char* open(File& fp)
49             fp.open(name, "wx+");
50             if (fp.null())
67     fp_name    = temp_files.open(fp);
92     if (!fp.null()){
94 	fp.setMode(READ);
95 	c2fp.push(fp.tell());
96 	fp.seek(0, SEEK_END);
97 	fp.setMode(WRITE);
99         putUInt(fp, -1 == orig_root_id ? root_counter << 1 : orig_root_id << 1);
100         putUInt(fp, index(clause[0]));
102             putUInt(fp, index(clause[i]) - index(clause[i-1]));
103         putUInt(fp, 0);     // (0 is safe terminator since we removed duplicates)
143         if (!fp.null()){
145 	  fp.setMode(READ);
146 	  c2fp.push(fp.tell());
147 	  fp.seek(0, SEEK_END);
148 	  fp.setMode(WRITE);
150 	  putUInt(fp, ((id_counter - chain_id[0]) << 1) | 1);
153 	      putUInt(fp, chain_var[i] + 1),
154                 putUInt(fp, id_counter - chain_id[i+1]);
155             putUInt(fp, 0);
166     if (!fp.null()){
167         putUInt(fp, ((id_counter - (abs(gone))) << 1) | 1);
168         putUInt(fp, 0);
178 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) {
180 ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp) {
191   idx = getUInt(fp);
199     tmp = getUInt(fp);
220 		       File& fp, uint64 tmp, ClauseId id, std::ofstream* fout) {
223 		       File& fp, uint64 tmp, ClauseId id) {
236     tmp = getUInt(fp);
245     tmp = getUInt(fp);
257     assert(!fp.null());
258     fp.setMode(READ);
276 	  //fp.seek(pos);
277 	  //uint64 tmp = getUInt(fp);
278 	  //parseChain(chain_id,chain_var,fp,tmp,id);
305 	  fp.seek(pos);
306 	  uint64 tmp = getUInt(fp);
308 	    ClauseId orig_root_id = parseRoot(clause,fp,tmp);
318 	    parseChain(chain_id,chain_var,fp,tmp,id);
342     assert(!fp.null());
345     fp.setMode(READ);
346     fp.seek(0);
354     while (!fp.eof()) {
355       out.putChar(fp.getChar());
359     fp.seek(0, SEEK_END);
360     fp.setMode(WRITE);
366     assert(!fp.null());
369     fp.setMode(READ);
370     fp.seek(0);
384       tmp = getUInt(fp);
388 	parseRoot(clause,fp,tmp,&fout);
390 	parseRoot(clause,fp,tmp);
396 	parseChain(chain_id,chain_var,fp,tmp,id,&fout);
398 	parseChain(chain_id,chain_var,fp,tmp,id);
413     fp.seek(0, SEEK_END);
414     fp.setMode(WRITE);