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