1/*****************************************************************************************[Proof.C] 2MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson 3 4Permission is hereby granted, free of charge, to any person obtaining a copy of this software and 5associated documentation files (the "Software"), to deal in the Software without restriction, 6including without limitation the rights to use, copy, modify, merge, publish, distribute, 7sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is 8furnished to do so, subject to the following conditions: 9 10The above copyright notice and this permission notice shall be included in all copies or 11substantial portions of the Software. 12 13THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT 14NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 15NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, 16DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT 17OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 18**************************************************************************************************/ 19 20#include "Proof.h" 21#include "Sort.h" 22#include <iostream> 23 24//================================================================================================= 25// Temporary files handling: 26 27 28class TempFiles { 29 vec<cchar*> files; // For clean-up purposed on abnormal exit. 30 31public: 32 ~TempFiles() 33 { 34 for (int i = 0; i < files.size(); i++) 35 remove(files[i]); 36 //printf("Didn't delete:\n %s\n", files[i]); 37 } 38 39 // Returns a read-only string with the filename of the temporary file. 40 // The pointer can be used to 41 // remove the file (which is otherwise done automatically upon program exit). 42 // 43 char* open(File& fp) 44 { 45 char* name; 46 for(;;){ 47 name = tempnam(NULL, NULL); 48 assert(name != NULL); 49 fp.open(name, "wx+"); 50 if (fp.null()) 51 xfree(name); 52 else{ 53 files.push(name); 54 return name; 55 } 56 } 57 } 58}; 59static TempFiles temp_files; // (should be singleton) 60 61 62//================================================================================================= 63// Proof logging: 64 65Proof::Proof() 66{ 67 fp_name = temp_files.open(fp); 68 id_counter = 1; //HA: to save sign info on-the-fly, unit_id uses -ve clause id's to indicate 69 // that the clause literal is negated, so can't use 0 70 root_counter = 1; 71 trav = NULL; 72 c2fp.push(0); // dummy argument (placeholder for clause ID 0 which does not exist) 73} 74 75Proof::Proof(ProofTraverser& t) 76{ 77 id_counter = 1; 78 root_counter = 1; 79 trav = &t; 80 c2fp.push(0); 81} 82 83ClauseId Proof::addRoot(vec<Lit>& cl, ClauseId orig_root_id) 84{ 85 cl.copyTo(clause); 86 87 sortUnique(clause); 88 89 if (trav != NULL) 90 trav->root(clause); 91 92 if (!fp.null()){ 93 94 fp.setMode(READ); 95 c2fp.push(fp.tell()); 96 fp.seek(0, SEEK_END); 97 fp.setMode(WRITE); 98 99 putUInt(fp, -1 == orig_root_id ? root_counter << 1 : orig_root_id << 1); 100 putUInt(fp, index(clause[0])); 101 for (int i = 1; i < clause.size(); i++) 102 putUInt(fp, index(clause[i]) - index(clause[i-1])); 103 putUInt(fp, 0); // (0 is safe terminator since we removed duplicates) 104 } 105 root_counter++; 106 return id_counter++; 107} 108 109void Proof::beginChain(ClauseId start) 110{ 111 assert(start != ClauseId_NULL); 112 chain_id .clear(); 113 chain_var.clear(); 114 chain_id.push(abs(start)); //HA: the abs 115 //std::cout << "B " << abs(start); 116} 117 118void Proof::resolve(ClauseId next, Var x) 119{ 120 assert(next != ClauseId_NULL); 121 chain_id .push(abs(next)); //HA: abs 122 if (next>=0) chain_var.push(x << 1); 123 else chain_var.push((x << 1) | 1); // HA: adding sign info to pivots 124} 125 126void Proof::resolve(ClauseId next, Lit p) 127{ 128 assert(next != ClauseId_NULL); 129 chain_id .push(abs(next)); //HA: abs 130 chain_var.push(index(p)); 131 //std::cout << " (" << index(p) << "," << next << ")"; 132} 133 134ClauseId Proof::endChain() 135{ 136 assert(chain_id.size() == chain_var.size() + 1); 137 //std::cout << std::endl; 138 if (chain_id.size() == 1) 139 return chain_id[0]; 140 else{ 141 if (trav != NULL) 142 trav->chain(chain_id, chain_var); 143 if (!fp.null()){ 144 145 fp.setMode(READ); 146 c2fp.push(fp.tell()); 147 fp.seek(0, SEEK_END); 148 fp.setMode(WRITE); 149 150 putUInt(fp, ((id_counter - chain_id[0]) << 1) | 1); 151 152 for (int i = 0; i < chain_var.size(); i++) 153 putUInt(fp, chain_var[i] + 1), 154 putUInt(fp, id_counter - chain_id[i+1]); 155 putUInt(fp, 0); 156 } 157 158 return id_counter++; 159 } 160} 161 162void Proof::deleted(ClauseId gone) 163{ 164 if (trav != NULL) 165 trav->deleted(abs(gone)); 166 if (!fp.null()){ 167 putUInt(fp, ((id_counter - (abs(gone))) << 1) | 1); 168 putUInt(fp, 0); 169 } 170} 171 172 173//================================================================================================= 174// Read-back methods: 175 176//HA: fill up "clause" as a root clause 177#ifdef DEBUG 178ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp, std::ofstream* fout) { 179#else 180ClauseId Proof::parseRoot(vec<Lit>& clause, File& fp, uint64 tmp) { 181#endif 182 183 int idx,idx0; 184{ 185#ifdef DEBUG 186 if (NULL != fout) (*fout) << "r "; 187#endif 188} 189 clause.clear(); 190 idx0 = tmp >> 1; // the root_counter value 191 idx = getUInt(fp); 192{ 193#ifdef DEBUG 194 if (NULL != fout) (*fout) << idx; 195#endif 196} 197 clause.push(toLit(idx)); 198 for(;;){ 199 tmp = getUInt(fp); 200 if (tmp == 0) break; 201 idx += tmp; 202{ 203#ifdef DEBUG 204 if (NULL != fout) (*fout) << " " << idx; 205#endif 206} 207 clause.push(toLit(idx)); 208 } 209{ 210#ifdef DEBUG 211 if (NULL != fout) (*fout) << "\n"; 212#endif 213} 214 return idx0; 215} 216 217//HA: fill up chain_id and chain_var 218#ifdef DEBUG 219void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, 220 File& fp, uint64 tmp, ClauseId id, std::ofstream* fout) { 221#else 222void Proof::parseChain(vec<ClauseId>& chain_id, vec<Var>& chain_var, 223 File& fp, uint64 tmp, ClauseId id) { 224#endif 225 226 chain_id .clear(); 227 chain_var.clear(); 228 chain_id.push(id - (tmp >> 1)); 229{ 230#ifdef DEBUG 231 if (NULL != fout) (*fout) << "B " << (id - (tmp >> 1)) << " "; 232#endif 233} 234 235 for(;;){ 236 tmp = getUInt(fp); 237 if (tmp == 0) break; 238 chain_var.push(tmp - 1); 239{ 240#ifdef DEBUG 241 if (NULL != fout) (*fout) << " " << (tmp-1); 242#endif 243} 244 245 tmp = getUInt(fp); 246 chain_id.push(id - tmp); 247{ 248#ifdef DEBUG 249 if (NULL != fout) (*fout) << " " << (id-tmp) << " "; 250#endif 251} 252 } 253} 254 255void Proof::compress(Proof& dst, ClauseId goal) 256{ 257 assert(!fp.null()); 258 fp.setMode(READ); 259 vec<ClauseId> dfs_stack; // stack for simulating "backwards" DFS 260 vec<vec<ClauseId> > chain_id_stack; 261 vec<vec<Var> > chain_var_stack; 262 vec<ClauseId> c2c(goal+2,-1); // c2c[old_id] is new id in compressed proof of clause old_id 263 264#ifdef DEBUG 265 std::ofstream fout ("filter.fdb"); // Output for debugging 266#endif 267 268 dfs_stack.push(goal); 269 ClauseId id = dfs_stack.last(); 270 while (dfs_stack.size()>0) { 271 id = dfs_stack.last(); 272 switch (c2c[id]) { 273 case -2 : // a chain that has been visited before. write it out now 274 { 275 //int64 pos = c2fp[id]; 276 //fp.seek(pos); 277 //uint64 tmp = getUInt(fp); 278 //parseChain(chain_id,chain_var,fp,tmp,id); 279 chain_id_stack.last().copyTo(chain_id); chain_id_stack.pop(); 280 chain_var_stack.last().copyTo(chain_var); chain_var_stack.pop(); 281 int sz = chain_id.size(); 282 for (int i=0; i<sz; i++) // redirect chain_id[i]'s to new id's 283 chain_id[i]=c2c[chain_id[i]]; 284 dst.beginChain(chain_id[0]); 285 for (int i=1;i<sz;i++) 286 dst.resolve(chain_var[i-1] & 1 ? -1*chain_id[i] : chain_id[i],chain_var[i-1] >> 1); 287 c2c[id] = dst.endChain(); 288 dfs_stack.pop(); 289{ 290#ifdef DEBUG 291 fout << c2c[id] << " B [" << id << "] : "; 292 for (int i=0;i<chain_var.size();i++) 293 fout << " " << chain_var[i] << " "; 294 fout << "::"; 295 for (int i=0; i<sz; i++) 296 fout << " " << chain_id[i] << " "; 297 fout << "\n"; 298#endif 299} 300 break; 301 } 302 case -1 : // this root/chain has not been visited before 303 { 304 int64 pos = c2fp[id]; 305 fp.seek(pos); 306 uint64 tmp = getUInt(fp); 307 if ((tmp & 1) == 0) { // if root, just write it out 308 ClauseId orig_root_id = parseRoot(clause,fp,tmp); 309 c2c[id] = dst.addRoot(clause,orig_root_id); 310 311{ 312#ifdef DEBUG 313 fout << c2c[id] << " R [" << ((tmp>>1)-1) << "]\n"; //debug 314#endif 315} 316 dfs_stack.pop(); 317 } else { // if chain, process antecedent clauses first 318 parseChain(chain_id,chain_var,fp,tmp,id); 319 chain_id_stack.push(); chain_id.copyTo(chain_id_stack.last()); 320 chain_var_stack.push(); chain_var.copyTo(chain_var_stack.last()); 321 int sz = chain_id.size(); 322 for (int i=0; i<sz; i++) 323 dfs_stack.push(chain_id[i]); 324 c2c[id] = -2; // means a chain that has been visited but not written out yet 325 } 326 break; 327 } 328 default: // this one's already been processed. 329 dfs_stack.pop(); 330 } 331 } 332{ 333#ifdef DEBUG 334 fout.close(); 335#endif 336} 337} 338 339 340bool Proof::save(cchar* filename) 341{ 342 assert(!fp.null()); 343 344 // Switch to read mode: 345 fp.setMode(READ); 346 fp.seek(0); 347 348 // Copy file: 349 File out(filename, "wox"); 350 351 if (out.null()) 352 return false; 353 354 while (!fp.eof()) { 355 out.putChar(fp.getChar()); 356 } 357 358 // Restore write (proof-logging) mode: 359 fp.seek(0, SEEK_END); 360 fp.setMode(WRITE); 361 return true; 362} 363 364void Proof::traverse(ProofTraverser& trav, int& res_count, ClauseId goal) 365{ 366 assert(!fp.null()); 367 368 // Switch to read mode: 369 fp.setMode(READ); 370 fp.seek(0); 371 372 // Traverse proof: 373 if (goal == ClauseId_NULL) 374 goal = last(); 375 376#ifdef DEBUG 377 std::ofstream fout ("proof.trv"); 378 fout << "G " << goal << "\n"; 379#endif 380 381 uint64 tmp; 382 383 for(ClauseId id = 1; id <= goal; id++){ 384 tmp = getUInt(fp); 385 if ((tmp & 1) == 0){ 386 // Root clause: 387#ifdef DEBUG 388 parseRoot(clause,fp,tmp,&fout); 389#else 390 parseRoot(clause,fp,tmp); 391#endif 392 trav.root(clause); 393 } else { 394 // Derivation or Deletion: 395#ifdef DEBUG 396 parseChain(chain_id,chain_var,fp,tmp,id,&fout); 397#else 398 parseChain(chain_id,chain_var,fp,tmp,id); 399#endif 400 res_count+=chain_var.size(); 401 if (chain_var.size() == 0) 402 id--, // (no new clause introduced) 403 trav.deleted(chain_id[0]-1); //HA: -1 to compensate for id_counter base 1 404 else 405 trav.chain(chain_id, chain_var); 406 } 407 } 408 trav.done(); 409#ifdef DEBUG 410 fout.close(); 411#endif 412 // Restore write (proof-logging) mode: 413 fp.seek(0, SEEK_END); 414 fp.setMode(WRITE); 415} 416