zchaff64/zverify_df.cpp

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