source: vis_dev/zchaff/zverify_df.cpp @ 23

Last change on this file since 23 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 23.6 KB
Line 
1// *********************************************************************
2// Copyright 2000-2004, Princeton University.  All rights reserved.
3// By using this software the USER indicates that he or she has read,
4// understood and will comply with the following:
5//
6// --- Princeton University hereby grants USER nonexclusive permission
7// to use, copy and/or modify this software for internal, noncommercial,
8// research purposes only. Any distribution, including commercial sale
9// or license, of this software, copies of the software, its associated
10// documentation and/or modifications of either is strictly prohibited
11// without the prior consent of Princeton University.  Title to copyright
12// to this software and its associated documentation shall at all times
13// remain with Princeton University.  Appropriate copyright notice shall
14// be placed on all software copies, and a complete copy of this notice
15// shall be included in all copies of the associated documentation.
16// No right is  granted to use in advertising, publicity or otherwise
17// any trademark, service mark, or the name of Princeton University.
18//
19//
20// --- This software and any associated documentation is provided "as is"
21//
22// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24// PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
25// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
27//
28// Princeton University shall not be liable under any circumstances for
29// any direct, indirect, special, incidental, or consequential damages
30// with respect to any claim by USER or any third party on account of
31// or arising from the use, or inability to use, this software or its
32// associated documentation, even if Princeton University has been advised
33// of the possibility of those damages.
34// *********************************************************************
35
36#include <cstdlib>
37#include <cstring>
38#include <sys/time.h>
39#include <sys/resource.h>
40#include <vector>
41#include <set>
42#include <iostream>
43#include <fstream>
44#include <assert.h>
45
46using namespace std;
47
48const int WORD_LEN      = 64000;
49
50const int MEM_LIMIT     = 800000;
51
52const int UNKNOWN       = 2;
53
54int _peak_mem;
55bool _dump_core;
56
57double get_cpu_time(void) {
58  double res;
59  struct rusage usage;
60  getrusage(RUSAGE_SELF, &usage);
61  res = usage.ru_utime.tv_usec + usage.ru_stime.tv_usec;
62  res *= 1e-6;
63  res += usage.ru_utime.tv_sec + usage.ru_stime.tv_sec;
64  return res;
65}
66
67void get_line(ifstream* fs, vector<char>* buf) {
68  buf->clear();
69  buf->reserve(4096);
70  while (!fs->eof()) {
71    char ch = fs->get();
72    if (ch == '\n' || ch == '\377')
73      break;
74    if (ch == '\r')
75      continue;
76    buf->push_back(ch);
77  }
78  buf->push_back('\0');
79  return;
80}
81
82int get_token(char * & lp, char * token) {
83  char * wp = token;
84  while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
85    lp++;
86  }
87  while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
88    *(wp++) = *(lp++);
89  }
90  *wp = '\0';                                 // terminate string
91  return wp - token;
92}
93
94int get_mem_usage(void) {
95  FILE * fp;
96  char buffer[128];
97  char token[128];
98  char filename[128];
99
100  int pid = getpid();
101  snprintf(filename, sizeof(filename), "/proc/%i/status", pid);
102  if ((fp = fopen(filename, "r")) == NULL) {
103    cerr << "Can't open Proc file, are you sure you are using Linux?" << endl;
104    exit(1);
105  }
106  while (!feof(fp)) {
107    fgets(buffer, 128, fp);
108    char * ptr = buffer;
109    get_token(ptr, token);
110    if (strcmp(token, "VmSize:") == 0) {
111      get_token(ptr, token);
112      fclose(fp);
113      return atoi(token);
114    }
115  }
116  cerr << "Error in get memeory usage" << endl;
117  exit(1);
118  return 0;
119}
120
121int my_a2i(char * str) {
122  int result = 0;
123  bool neg = false;
124  if (str[0] == '-') {
125    neg = true;
126    ++str;
127  }
128  else if (str[0] == '+')
129    ++str;
130  for (unsigned i = 0; i < strlen(str); ++i) {
131    int d = str[i] - '0';
132    if (d < 0 || d > 9) {
133      cerr << "Abort: Unable to change " << str << " into a number " << endl;
134      exit(1);
135    }
136    result = result * 10 + d;
137  }
138  if (neg)
139    result = -result;
140  return result;
141}
142
143class CClause {
144  public:
145    vector<int> literals;
146    vector<int> resolvents;
147    bool is_involved    : 1;
148    bool is_built       : 1;
149    bool is_needed      : 1;
150
151    CClause(void) {
152      is_involved = false;
153      is_built = false;
154      is_needed = false;
155    }
156    ~CClause(void) {}
157};
158
159class CVariable {
160  public:
161    short       value;
162    short       in_clause_phase         :4;
163    bool        is_needed               :1;
164    int         antecedent;
165    int         num_lits[2];
166    int         level;
167    CVariable(void) {
168      value = UNKNOWN;
169      antecedent = -1;
170      in_clause_phase = UNKNOWN;
171      num_lits[0] = num_lits[1] = 0;
172      level = -1;
173      is_needed = false;
174    }
175};
176
177struct cmp_var_level {
178  bool operator() (CVariable * v1, CVariable * v2) {
179    if (v1->level > v2->level)
180      return true;
181    else if (v1->level < v2->level)
182      return false;
183    else if ( (int)v1 > (int)v2)
184      return true;
185    return false;
186  }
187};
188
189class CDatabase {
190  private:
191    int                 _current_num_clauses;
192    int                 _num_init_clauses;
193    vector<CVariable>   _variables;
194    vector<CClause>     _clauses;
195    int                 _conf_id;
196    vector<int>         _conf_clause;
197
198  public:
199    CDatabase(void) {
200      _num_init_clauses = 0;
201      _current_num_clauses = 0;
202      _conf_id = -1;
203    }
204
205    int & num_init_clauses(void) {
206      return _num_init_clauses;
207    }
208
209    vector<CVariable> & variables(void) {
210      return _variables;
211    }
212
213    vector<CClause> & clauses(void) {
214      return  _clauses;
215    }
216
217    void read_cnf(char * filename);
218    bool verify(char * filename);
219    bool real_verify(void);
220    int lit_value(int svar) {
221      assert(_variables[svar>>1].value != UNKNOWN);
222      return _variables[svar>>1].value ^ (svar & 0x1);
223    }
224    int add_orig_clause_by_lits(vector<int> lits);
225    int add_learned_clause_by_resolvents(vector<int> & resolvents);
226    void set_var_number(int nvar);
227    void set_init_cls_number(int n) {
228      _num_init_clauses = n;
229    }
230    void construct_learned_clauses(void);
231    void recursive_construct_clause(int cl_id);
232    void recursive_find_involved(int cl_id);
233    int recursive_find_level(int vid);
234    void dump(void);
235};
236
237void CDatabase::dump(void) {
238  cout << "p cnf " << _variables.size() - 1 << " " << _num_init_clauses << endl;
239  for (unsigned i = 0; i < _clauses.size(); ++i) {
240    for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
241      int lit = _clauses[i].literals[j];
242      cout << ((lit & 0x1) ? "-" : "") << (lit >> 1) << " ";
243    }
244    cout << "0" << endl;
245  }
246}
247
248void CDatabase::set_var_number(int nvar) {
249  _variables.resize(nvar + 1);
250  for (unsigned i = 0; i < _variables.size(); ++i) {
251    _variables[i].value = UNKNOWN;
252    _variables[i].in_clause_phase = UNKNOWN;
253  }
254}
255
256void check_mem_out(void) {
257  int mem = get_mem_usage();
258  if (mem > MEM_LIMIT) {
259    cerr << "Mem out" << endl;
260    exit(1);
261  }
262  if (mem > _peak_mem)
263    _peak_mem = mem;
264}
265
266int CDatabase::add_orig_clause_by_lits(vector<int> lits) {
267  static int line_n = 0;
268  ++line_n;
269  if (lits.size() == 0) {
270    cerr << "Empty Clause Encountered " << endl;
271    exit(1);
272  }
273  int cls_id = _clauses.size();
274  _clauses.resize(_clauses.size() + 1);
275  vector<int> temp_cls;
276  for (unsigned i = 0; i < lits.size(); ++i) {
277    int vid = lits[i];
278    int phase = 0;
279    if (vid < 0) {
280      vid = - vid;
281      phase = 1;
282    }
283    if (vid == 0 || vid > (int) _variables.size() - 1) {
284      cerr << "Variable index out of range " << endl;
285      exit(1);
286    }
287    if (_variables[vid].in_clause_phase == UNKNOWN) {
288      _variables[vid].in_clause_phase = phase;
289      temp_cls.push_back(vid + vid + phase);
290//    _clauses[cls_id].my_literals.push_back(vid + vid + phase);
291      ++_variables[vid].num_lits[phase];
292    }
293    else if (_variables[vid].in_clause_phase != phase) {
294      cerr << "clause " << line_n << endl;
295      cerr << "A clause contain both literal and its negate " << endl;
296      exit(1);
297    }
298  }
299  _clauses[cls_id].literals.resize(temp_cls.size());
300  for (unsigned i = 0; i< temp_cls.size(); ++i) {
301    _clauses[cls_id].literals[i]= temp_cls[i];
302  }
303  _clauses[cls_id].is_built = true;
304//      _clauses[cls_id].my_is_built = true;
305  for (unsigned i = 0; i< lits.size(); ++i) {
306    int vid = lits[i];
307    if (vid < 0) vid = -vid;
308    _variables[vid].in_clause_phase = UNKNOWN;
309  }
310  ++_current_num_clauses;
311  if (_current_num_clauses%10 == 0)
312    check_mem_out();
313  return cls_id;
314}
315
316int CDatabase::add_learned_clause_by_resolvents(vector<int> & resolvents) {
317  int cls_id = _clauses.size();
318  _clauses.resize(_clauses.size() + 1);
319  _clauses[cls_id].resolvents.resize(resolvents.size());
320  for (unsigned i = 0; i< resolvents.size(); ++i)
321    _clauses[cls_id].resolvents[i] = resolvents[i];
322  _clauses[cls_id].is_built = false;
323  return cls_id;
324}
325
326void CDatabase::read_cnf(char * filename) {
327  cout << "Read in original clauses ... ";
328  ifstream in_file(filename);
329  if (!in_file) {
330    cerr << "Can't open input CNF file " << filename << endl;
331    exit(1);
332  }
333  vector<char> buffer;
334  vector<int> literals;
335  bool header_encountered = false;
336  char token[WORD_LEN];
337  while (!in_file.eof()) {
338    get_line(&in_file, &buffer);
339    char * ptr = &(*buffer.begin());
340    if (get_token(ptr, token)) {
341      if (strcmp(token, "c") == 0)
342        continue;
343      else if (strcmp(token, "p") == 0) {
344        get_token(ptr, token);
345        if (strcmp(token, "cnf") != 0) {
346          cerr << "Format Error, p cnf NumVar NumCls " << endl;
347          exit(1);
348        }
349        get_token(ptr, token);
350        int nvar = my_a2i(token);
351        set_var_number(nvar);
352        get_token(ptr, token);
353        int ncls = my_a2i(token);
354        set_init_cls_number(ncls);
355        header_encountered = true;
356        continue;
357      } else {
358        int lit = my_a2i(token);
359        if (lit != 0) {
360          literals.push_back(lit);
361        } else {
362          add_orig_clause_by_lits(literals);
363          literals.clear();
364        }
365      }
366    }
367    while (get_token(ptr, token)) {
368      int lit = my_a2i(token);
369      if (lit != 0) {
370        literals.push_back(lit);
371      } else {
372        add_orig_clause_by_lits(literals);
373        literals.clear();
374      }
375    }
376  }
377  if (!literals.empty()) {
378    cerr << "Trailing numbers without termination " << endl;
379    exit(1);
380  }
381  if (clauses().size() != (unsigned)num_init_clauses())
382    cerr << "WARNING : Clause count inconsistant with the header " << endl;
383  cout << num_init_clauses() << " Clauses " << endl;
384}
385
386void CDatabase::recursive_find_involved(int cl_id) {
387  if (_clauses[cl_id].is_involved == true)
388    return;
389  _clauses[cl_id].is_involved = true;
390
391  recursive_construct_clause(cl_id);
392
393  int num_1 = 0;
394  for (unsigned i = 0; i < _clauses[cl_id].literals.size(); ++i) {
395    int lit = _clauses[cl_id].literals[i];
396    int vid = (lit>>1);
397    int sign = (lit & 0x1);
398    assert(_variables[vid].value != UNKNOWN);
399    if ((_variables[vid].value == 1 && sign == 0) ||
400      (_variables[vid].value == 0 && sign == 1)) {
401      if (num_1 == 0) {
402        ++num_1;
403      } else {
404        cerr << "Clause " << cl_id << " has more than one value 1 literals "
405             << endl;
406        exit(1);
407      }
408    } else {  // literal value 0, so seek its antecedent
409      int ante = _variables[vid].antecedent;
410      recursive_find_involved(ante);
411    }
412  }
413}
414
415void CDatabase::recursive_construct_clause(int cl_id) {
416  CClause & cl = _clauses[cl_id];
417  if (cl.is_built == true)
418    return;
419
420  assert(cl.resolvents.size() > 1);
421
422  // I have to construct them first because of recursion may
423  // mess up with the in_clause_signs.
424  for (unsigned i = 0; i < cl.resolvents.size(); ++i) {
425    _clauses[cl.resolvents[i]].is_needed = true;
426    recursive_construct_clause(cl.resolvents[i]);
427  }
428
429//      cout << "Constructing clause " << cl_id << endl;
430  vector<int> literals;
431
432  // initialize
433  int cl1 = cl.resolvents[0];
434  assert(_clauses[cl1].is_built);
435  for (unsigned i = 0; i < _clauses[cl1].literals.size(); ++i) {
436    int lit = _clauses[cl1].literals[i];
437    int vid = (lit >> 0x1);
438    int sign = (lit & 0x1);
439    assert(_variables[vid].in_clause_phase == UNKNOWN);
440    _variables[vid].in_clause_phase = sign;
441    literals.push_back(lit);
442  }
443
444  for (unsigned i = 1; i < cl.resolvents.size(); ++i) {
445    int distance = 0;
446    int cl1 = cl.resolvents[i];
447    assert(_clauses[cl1].is_built);
448    for (unsigned j = 0; j < _clauses[cl1].literals.size(); ++j) {
449      int lit = _clauses[cl1].literals[j];
450      int vid = (lit >> 0x1);
451      int sign = (lit & 0x1);
452      if (_variables[vid].in_clause_phase == UNKNOWN) {
453        _variables[vid].in_clause_phase = sign;
454        literals.push_back(lit);
455      }
456      else if (_variables[vid].in_clause_phase != sign) {
457        // distance 1 literal
458        ++distance;
459        _variables[vid].in_clause_phase = UNKNOWN;
460      }
461    }
462    if (distance != 1) {
463      cerr << "Resolve between two clauses with distance larger than 1" << endl;
464      cerr << "The resulting clause is " << cl_id << endl;
465      cerr << "Starting clause is " << cl.resolvents[0] << endl;
466      cerr << "One of the clause involved is " << cl1 << endl;
467      exit(1);
468    }
469  }
470  vector<int> temp_cls;
471  for (unsigned i = 0; i < literals.size(); ++i) {
472    int lit = literals[i];
473    int vid = (lit >> 0x1);
474    int sign = (lit & 0x1);
475    if (_variables[vid].in_clause_phase == UNKNOWN)
476      continue;
477    assert(_variables[vid].in_clause_phase == sign);
478    _variables[vid].in_clause_phase = UNKNOWN;
479    temp_cls.push_back(lit);
480  }
481  cl.literals.resize(temp_cls.size());
482  for (unsigned i = 0; i < temp_cls.size(); ++i)
483    cl.literals[i] = temp_cls[i];
484
485//      ::sort(cl.literals.begin(), cl.literals.end());
486//      assert(cl.literals.size()== cl.my_literals.size());
487//      for (unsigned i=0; i< cl.literals.size(); ++i)
488//        assert(cl.literals[i] == cl.my_literals[i]);
489  cl.is_built = true;
490  ++_current_num_clauses;
491  if (_current_num_clauses%10 == 0)
492    check_mem_out();
493}
494
495int CDatabase::recursive_find_level(int vid) {
496  int ante = _variables[vid].antecedent;
497  assert(_variables[vid].value != UNKNOWN);
498  assert(_variables[vid].antecedent != -1);
499  assert(_clauses[ante].is_involved);
500  if (_variables[vid].level != -1)
501    return _variables[vid].level;
502  int level = -1;
503  for (unsigned i = 0; i <_clauses[ante].literals.size(); ++i) {
504    int v = (_clauses[ante].literals[i] >> 1);
505    int s = (_clauses[ante].literals[i] & 0x1);
506    if (v == vid) {
507      assert(_variables[v].value != s);
508      continue;
509    } else {
510      assert(_variables[v].value == s);
511      int l = recursive_find_level(v);
512      if (level < l )
513        level = l;
514    }
515  }
516  _variables[vid].level = level + 1;
517  return level + 1;
518}
519
520bool CDatabase::real_verify(void) {
521  // 1. If a variable is assigned value at dlevel 0,
522  // either it's pure or it has an antecedent
523  for (unsigned i = 1; i < _variables.size(); ++i) {
524    if (_variables[i].value != UNKNOWN && _variables[i].antecedent == -1) {
525      if ((_variables[i].num_lits[0] == 0 && _variables[i].value == 0) ||
526        (_variables[i].num_lits[1] == 0 && _variables[i].value == 1)) {
527//      cout << "Variable " << i << " is assigned " << _variables[i].value
528//      << " because it is pure literal. " << endl;
529      } else {
530        cerr << "Don't know why variable " << i << " is assigned "
531             << _variables[i].value << " for no reasons" << endl;
532        exit(1);
533      }
534    }
535  }
536  // 2. Construct the final conflicting clause if needed and find all
537  // the clauses that are involved in making it conflicting
538  cout << "Begin constructing all involved clauses " << endl;
539  _clauses[_conf_id].is_needed = true;
540  recursive_find_involved(_conf_id);
541  int count = 0;
542  for (unsigned i = num_init_clauses(); i< _clauses.size(); ++i)
543    if (_clauses[i].is_built)
544      ++count;
545  cout << "Num. Learned Clause:\t\t\t" << _clauses.size() - num_init_clauses()
546       << endl
547       << "Num. Clause Built:\t\t\t" << count << endl
548       << "Constructed all involved clauses " << endl;
549
550  // 2.5. Verify the literals in the CONF clause
551  // comments this out if it gives error because you give the wrong
552  // CONF clause literals.
553  assert(_clauses[_conf_id].is_built);
554  assert(_clauses[_conf_id].is_involved);
555  bool _found;
556  for (unsigned i = 0; i <_conf_clause.size(); ++i) {
557    _found = false;
558    for (unsigned j = 0; j <_clauses[_conf_id].literals.size(); ++j) {
559      if (_conf_clause[i] == _clauses[_conf_id].literals[j]) {
560        _found = true;
561        break;
562      }
563    }
564    if (!_found) {
565      cerr << "The conflict clause in trace can't be verified! " << endl;
566      cerr << "Literal " << _conf_clause[i] << " is not found." << endl;
567    }
568  }
569  cout << "Conflict clause verification finished." << endl;
570
571  // 3. Levelize the variables that are decided at dlevel 0
572  cout << "Levelize variables...";
573  for (unsigned i = 1; i < _variables.size(); ++i) {
574    int cl_id = _variables[i].antecedent;
575    if (_variables[i].value != UNKNOWN &&  cl_id != -1) {
576      if (_clauses[cl_id].is_involved) {
577           recursive_find_level(i);
578//         int level = recursive_find_level(i);
579//         cout << "Var: " << i << " level " << level << endl;
580      }
581    }
582  }
583  cout << "finished"<< endl;
584  // 4. Can we construct an empty clause?
585  cout << "Begin Resolution..." ;
586  set<CVariable *, cmp_var_level> clause_lits;
587  for (unsigned i = 0; i< _clauses[_conf_id].literals.size(); ++i) {
588    assert(lit_value(_clauses[_conf_id].literals[i]) == 0);
589    int vid = (_clauses[_conf_id].literals[i] >> 1);
590    clause_lits.insert(&_variables[vid]);
591  }
592  assert(clause_lits.size() == _clauses[_conf_id].literals.size());
593
594  while (!clause_lits.empty()) {
595//    for (set<CVariable *, cmp_var_level>::iterator itr = clause_lits.begin();
596//         itr != clause_lits.end(); ++itr) {
597//      int vid = (*itr) - &_variables[0];
598//      cout << vid << "(" << (*itr)->level << ") ";
599//    }
600//    cout << endl;
601
602    int vid = (*clause_lits.begin() - &_variables[0]);
603    int ante = _variables[vid].antecedent;
604    if (ante == -1) {
605      cerr << "Variable " << vid << " has an NULL antecedent ";
606      exit(1);
607    }
608    _clauses[ante].is_needed = true;
609    clause_lits.erase(clause_lits.begin());
610    _variables[vid].in_clause_phase = 1;
611    CClause & cl = _clauses[ante];
612    int distance = 0;
613    for (unsigned i = 0; i< cl.literals.size(); ++i) {
614      int l = cl.literals[i];
615      int v = (l>>1);
616      assert(_variables[v].value != UNKNOWN);
617      if (lit_value(l) == 1) {
618        if (vid != v) {
619          cerr << "The antecedent of the variable is not really an antecedent "
620               << endl;
621          exit(1);
622        }
623        else
624          ++distance;
625      }
626      else
627        clause_lits.insert(&_variables[v]);
628    }
629    assert(distance == 1);
630  }
631  cout << " Empty clause generated." << endl;
632  cout << "Mem Usage :\t\t\t\t" << get_mem_usage()<< endl;
633  int needed_cls_count = 0;
634  int needed_var_count = 0;
635  for (int i = 0; i < num_init_clauses(); ++i) {
636    if (_clauses[i].is_needed == true) {
637      ++needed_cls_count;
638      for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
639        int vid = (_clauses[i].literals[j] >> 1);
640        if (_variables[vid].is_needed == false) {
641          ++needed_var_count;
642          _variables[vid].is_needed = true;
643        }
644      }
645    }
646  }
647  cout << "Original Num. Clauses:\t\t\t" << num_init_clauses() << endl;
648  cout << "Needed Clauses to Construct Empty:\t"<< needed_cls_count << endl;
649  cout << "Total Variable count:\t\t\t" << _variables.size()-1 << endl;
650  cout << "Variables involved in Empty:\t\t" << needed_var_count << endl;
651
652  for (unsigned i = 0; i< _clauses.size(); ++i) {
653    if (_clauses[i].is_built)
654      assert(_clauses[i].is_needed || i < (unsigned)num_init_clauses());
655  }
656  if (_dump_core == true) {
657    cout << "Unsat Core dumped:\t\t\tunsat_core.cnf" << endl;
658    ofstream dump("unsat_core.cnf");
659    dump << "c Variables Not Involved: ";
660    unsigned int k = 0;
661    for (unsigned i = 1; i < _variables.size(); ++i) {
662      if (_variables[i].is_needed == false) {
663        if (k%20 == 0)
664          dump << endl << "c ";
665        ++k;
666        dump << i << " ";
667      }
668    }
669    dump << endl;
670    dump << "p cnf " << _variables.size()-1 << " " << needed_cls_count << endl;
671    for (int i = 0; i < num_init_clauses(); ++i) {
672      if (_clauses[i].is_needed) {
673        dump << "c Original Cls ID: " << i << endl;
674        for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) {
675          dump << ((_clauses[i].literals[j] & 0x1)?" -":" ")
676               << (_clauses[i].literals[j] >> 1);
677        }
678        dump << " 0" << endl;
679      }
680    }
681  }
682  return true;
683}
684
685bool CDatabase::verify(char * filename) {
686  vector<char> buffer;
687  char token[WORD_LEN];
688
689  ifstream in_file(filename);
690  if (!in_file) {
691    cerr << "Can't open input CNF file " << filename << endl;
692    exit(1);
693  }
694
695  while (!in_file.eof()) {
696    get_line(&in_file, &buffer);
697    char * ptr = &(*buffer.begin());
698    get_token(ptr, token);
699    if (strcmp(token, "CL:") == 0) {
700      vector<int> resolvents;
701
702      get_token(ptr, token);
703      int cl_id = my_a2i(token);
704
705      get_token(ptr, token);
706      assert(strcmp(token, "<=") == 0);
707
708      while (get_token(ptr, token)) {
709        int r = my_a2i(token);
710        resolvents.push_back(r);
711      }
712      int c = add_learned_clause_by_resolvents(resolvents);
713      assert(c == cl_id);
714    }
715    else if (strcmp(token, "VAR:") == 0) {
716      get_token(ptr, token);
717      int vid = my_a2i(token);
718
719      get_token(ptr, token);
720      assert(strcmp(token, "L:") == 0);
721      get_token(ptr, token);  // skip the level
722
723      get_token(ptr, token);
724      assert(strcmp(token, "V:") == 0);
725      get_token(ptr, token);
726      int value = my_a2i(token);
727      assert(value == 1 || value == 0);
728
729      get_token(ptr, token);
730      assert(strcmp(token, "A:") == 0);
731      get_token(ptr, token);
732      int ante = my_a2i(token);
733
734      get_token(ptr, token);
735      assert(strcmp(token, "Lits:") == 0);
736
737      _variables[vid].value = value;
738      _variables[vid].antecedent = ante;
739    }
740    else if (strcmp(token, "CONF:") == 0) {
741      get_token(ptr, token);
742      _conf_id = my_a2i(token);
743
744      get_token(ptr, token);
745      assert(strcmp(token, "==") == 0);
746
747      while (get_token(ptr, token)) {
748        int lit = my_a2i(token);
749        assert(lit > 0);
750        assert((lit>>1) < (int)_variables.size());
751        _conf_clause.push_back(lit);
752      }
753    }
754  }
755  if (_conf_id == -1) {
756    cerr << "No final conflicting clause defined " << endl;
757    exit(1);
758  }
759  cout << "Mem Usage After Readin file:\t\t" << get_mem_usage() << endl;
760  return real_verify();
761}
762
763int main(int argc, char** argv) {
764  cout << "ZVerify SAT Solver Verifier" << endl;
765  cout << "Copyright Princeton University, 2003-2004. All Right Reseverd."
766       << endl;
767  if (argc != 3 && argc !=4) {
768    cerr << "Usage: " << argv[0] << " CNF_File Dump_File [-core]" << endl
769       << "-core: dump the unsat core " << endl;
770    cerr << endl;
771    exit(1);
772  }
773  if (argc == 3) {
774    _dump_core = false;
775  } else {
776    assert(argc == 4);
777    if (strcmp(argv[3], "-core") != 0) {
778      cerr << "Must use -core as the third parameter" << endl;
779      exit(1);
780    }
781    _dump_core = true;
782  }
783  cout << "COMMAND LINE: ";
784  for (int i = 0; i < argc; ++i)
785    cout << argv[i] << " ";
786  cout << endl;
787
788  _peak_mem = get_mem_usage();
789  CDatabase dbase;
790  double begin_time = get_cpu_time();
791  dbase.read_cnf(argv[1]);
792  if (dbase.verify(argv[2]) == true) {
793    double end_time = get_cpu_time();
794    cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl;
795    cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl;
796    cout << "Verification Successful " << endl;
797  } else {
798    cout << "Failed to verify the result " << endl;
799  }
800  return 0;
801}
Note: See TracBrowser for help on using the repository browser.