/*********************************************************************
 Copyright 2000-2004, Princeton University.  All rights reserved. 
 By using this software the USER indicates that he or she has read, 
 understood and will comply with the following:

 --- Princeton University hereby grants USER nonexclusive permission 
 to use, copy and/or modify this software for internal, noncommercial,
 research purposes only. Any distribution, including commercial sale 
 or license, of this software, copies of the software, its associated 
 documentation and/or modifications of either is strictly prohibited 
 without the prior consent of Princeton University.  Title to copyright
 to this software and its associated documentation shall at all times 
 remain with Princeton University.  Appropriate copyright notice shall 
 be placed on all software copies, and a complete copy of this notice 
 shall be included in all copies of the associated documentation.  
 No right is  granted to use in advertising, publicity or otherwise 
 any trademark, service mark, or the name of Princeton University. 


 --- This software and any associated documentation is provided "as is" 

 PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 
 OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 
 PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR 
 ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 
 TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.  

 Princeton University shall not be liable under any circumstances for 
 any direct, indirect, special, incidental, or consequential damages 
 with respect to any claim by USER or any third party on account of 
 or arising from the use, or inability to use, this software or its 
 associated documentation, even if Princeton University has been advised
 of the possibility of those damages.
*********************************************************************/

#include <sys/time.h>
#include <sys/resource.h>
#include <unistd.h>
#include <cstdio>
#include <vector>
#include <set>
#include <algorithm>
#include <iostream>
#include <fstream>
#include <assert.h>

using namespace std;

#define WORD_LEN 64000

#define MEM_LIMIT 800000

#define UNKNOWN 2

int _peak_mem;
bool _dump_core; 

double get_cpu_time()
{
    double res;
    struct rusage usage;

    getrusage(RUSAGE_SELF, &usage);

    res = usage.ru_utime.tv_usec + usage.ru_stime.tv_usec;
    res *= 1e-6;
    res += usage.ru_utime.tv_sec + usage.ru_stime.tv_sec; 
	
    return res;
}

void get_line(ifstream &fs, vector<char> &buf)
{
    buf.clear();
    buf.reserve(4096);
    while(!fs.eof()) {
        char ch = fs.get();
        if(ch == '\n' || ch == '\377')
	    break;
        if(ch == '\r') 
	    continue;
        buf.push_back(ch);
    }
    buf.push_back('\0');
    return;
}

int get_token (char * & lp, char * token)
{
    char * wp = token;
    while (*lp && ((*lp == ' ') || (*lp == '\t'))) {
	lp++;
    }
    while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) {
	*(wp++) = *(lp++);
    }
    *wp = '\0';                                 // terminate string
    return wp - token; 
}

int get_mem_usage(void) 
{
    FILE * fp;
    char buffer[128];
    char token[128];
    char filename[128];

    int pid = getpid();
    sprintf(filename, "/proc/%i/status", pid);
    if ( (fp = fopen (filename, "r")) == NULL) {
	cerr << "Can't open Proc file, are you sure you are using Linux?" << endl;
	exit(1);
    }
    while(!feof(fp)) {
	fgets(buffer, 128, fp);
	char * ptr = buffer;
	get_token(ptr, token);
	if (strcmp(token, "VmSize:")==0) {
	    get_token(ptr, token);
	    fclose(fp);
	    return atoi(token);
	}
    }
    cerr << "Error in get memeory usage" << endl;
    exit(1);
    return 0;
}

int my_a2i(char * str)
{
    int result = 0;
    bool neg = false;
    if (str[0] == '-') {
	neg = true;
	++ str;
    }
    else if (str[0] == '+')
	++ str;
    for (unsigned i=0; i< strlen(str); ++i) {
	int d = str[i] - '0';
	if (d < 0 || d > 9) {
	    cerr << "Abort: Unable to change " << str << " into a number " << endl;
	    exit(1);
	}
	result = result * 10 + d;
    }
    if (neg) 
	result = -result;
    return result;
}

class CClause 
{
public:    
    vector<int> literals;
//      vector<int> my_literals;
    vector<int> resolvents;
//      bool my_is_built;
    bool is_involved	: 1;
    bool is_built	: 1;	
    bool is_needed	: 1;
public:
    CClause(void) {
	is_involved = false;
	is_built = false;
	is_needed = false;
//  	my_is_built = false;
    }
    ~CClause(){}
};

class CVariable
{
public:
    short value;
    short in_clause_phase	:4; 
    bool is_needed		:1;
    int antecedent;
    int num_lits[2];
    int level;
    CVariable(void) { 
	value = UNKNOWN; 
	antecedent = -1; 
	in_clause_phase = UNKNOWN;
	num_lits[0] = num_lits[1] = 0;
	level = -1;
	is_needed = false;
    }
};
struct cmp_var_level 
{
    bool operator () (CVariable * v1, CVariable * v2)
	{
	    if (v1->level > v2->level)
		return true;
	    else if (v1->level < v2->level)
		return false;
	    else if ( (int)v1 > (int)v2)
		return true;
	    return false;
	}
};

class CDatabase {
private:
    int _current_num_clauses;

    int	_num_init_clauses;

    vector<CVariable> _variables;

    vector<CClause> _clauses;

    int _conf_id;

    vector<int> _conf_clause;

public:
    CDatabase() {
	_num_init_clauses = 0;
	_current_num_clauses = 0;
	_conf_id = -1;
    }

    int & num_init_clauses(void) { return _num_init_clauses; }

    vector<CVariable> & variables(void) {return _variables; }

    vector<CClause> & clauses(void)  {return  _clauses; }
    
    void read_cnf(char * filename);

    bool verify(char * filename);

    bool real_verify(void);

    int lit_value(int svar) { 
	assert (_variables[svar>>1].value != UNKNOWN);
	return _variables[svar>>1].value ^ (svar&0x1);
    }

    int add_orig_clause_by_lits(vector<int> lits);
	
    int add_learned_clause_by_resolvents(vector<int> & resolvents);

    void set_var_number(int nvar);

    void set_init_cls_number (int n) {
	_num_init_clauses = n;
    }
    void construct_learned_clauses(void);

    void recursive_construct_clause(int cl_id);

    void recursive_find_involved (int cl_id);

    int recursive_find_level(int vid);
    
    void dump(void);
};

void CDatabase::dump(void) 
{
    cout << "p cnf " << _variables.size() - 1 << " " << _num_init_clauses << endl;
    for (unsigned i=0; i< _clauses.size(); ++i) {
	for (unsigned j=0; j< _clauses[i].literals.size(); ++j ) {
	    int lit = _clauses[i].literals[j];
	    cout << ((lit & 0x1)?"-":"") << (lit>>1) << " ";
	}
	cout << "0" << endl;
    }
}
void CDatabase::set_var_number(int nvar) 
{ 
    _variables.resize(nvar + 1);
    for (unsigned i=0; i < _variables.size(); ++i) {
	_variables[i].value = UNKNOWN;
	_variables[i].in_clause_phase = UNKNOWN;
    }
}

void check_mem_out(void)
{
    int mem = get_mem_usage();
    if (mem > MEM_LIMIT) {
	cerr << "Mem out" << endl;
	exit(1);
    }
    if (mem > _peak_mem)
	_peak_mem = mem;
}

int CDatabase::add_orig_clause_by_lits(vector<int> lits) 
{
    static int line_n = 0;
    ++ line_n;
    if (lits.size() == 0) {
	cerr << "Empty Clause Encountered " << endl;
	exit(1);
    }
    int cls_id = _clauses.size();
    _clauses.resize(_clauses.size() + 1);
    vector<int> temp_cls;
    for (unsigned i=0; i< lits.size(); ++i) {
	int vid = lits[i];
	int phase = 0;
	if (vid < 0) {
	    vid = - vid;
	    phase = 1;
	}
	if (vid == 0 || vid > (int) _variables.size() - 1) {
	    cerr << "Variable index out of range " << endl;
	    exit(1);
	}
	if (_variables[vid].in_clause_phase == UNKNOWN){
	    _variables[vid].in_clause_phase = phase;
	    temp_cls.push_back(vid + vid + phase);
//  	    _clauses[cls_id].my_literals.push_back(vid + vid + phase);
	    ++ _variables[vid].num_lits[phase];
	}
	else if (_variables[vid].in_clause_phase != phase) {
	    cerr << "clause " << line_n << endl;
	    cerr << "A clause contain both literal and its negate " << endl;
	    exit(1);
	}
    }
    _clauses[cls_id].literals.resize(temp_cls.size());
    for (unsigned i=0; i< temp_cls.size(); ++i) {
	_clauses[cls_id].literals[i]= temp_cls[i];
    }
    _clauses[cls_id].is_built = true;
//      _clauses[cls_id].my_is_built = true;
    for (unsigned i=0; i< lits.size(); ++i) {
	int vid = lits[i];
	if (vid < 0) vid = -vid;
	_variables[vid].in_clause_phase = UNKNOWN;
    }
    ++ _current_num_clauses;
    if (_current_num_clauses%10 == 0)
	check_mem_out();
    return cls_id;
}

int CDatabase::add_learned_clause_by_resolvents(vector<int> & resolvents)
{
    int cls_id = _clauses.size();
    _clauses.resize(_clauses.size() + 1);
    _clauses[cls_id].resolvents.resize(resolvents.size());
    for (unsigned i=0; i< resolvents.size();  ++i) 
	_clauses[cls_id].resolvents[i] = resolvents[i];
    _clauses[cls_id].is_built = false;
    return cls_id;
}

void CDatabase::read_cnf (char * filename)
{
    cout << "Read in original clauses ... ";
    ifstream in_file (filename);
    if (!in_file) {
	cerr << "Can't open input CNF file " << filename << endl;
	exit(1);
    }
    vector<char> buffer;
    vector<int> literals;
    bool header_encountered = false;
    char token[WORD_LEN];	
    while (!in_file.eof()) {
	get_line(in_file, buffer);
	char * ptr = &(*buffer.begin());
	if (get_token(ptr, token)) {
	    if (strcmp(token, "c")==0)
		continue;
	    else if (strcmp(token, "p")==0) {
		get_token(ptr, token);
		if (strcmp(token, "cnf") != 0) {
		    cerr << "Format Error, p cnf NumVar NumCls " << endl;
		    exit(1);
		}
		get_token(ptr, token);
		int nvar = my_a2i(token);
		set_var_number(nvar);
		get_token(ptr, token);
		int ncls = my_a2i(token);
		set_init_cls_number(ncls);
		header_encountered = true;
		continue;
	    }
	    else {
		int lit = my_a2i(token);
		if (lit != 0)
		    literals.push_back(lit);
		else {
		    add_orig_clause_by_lits(literals);
		    literals.clear();
		}
	    }
	}
	while (get_token(ptr, token)) {
	    int lit = my_a2i(token);
	    if (lit != 0)
		literals.push_back(lit);
	    else {
		add_orig_clause_by_lits(literals);
		literals.clear();
	    }
	}
    }
    if (!literals.empty()) {
	cerr << "Trailing numbers without termination " << endl;
	exit(1);
    }
    if (clauses().size() != (unsigned)num_init_clauses()) 
	cerr << "WARNING : Clause count inconsistant with the header " << endl;
    cout << num_init_clauses() << " Clauses " << endl;
}

//  void CDatabase::construct_learned_clauses(void)
//  {
//      for (int cl_id=0; cl_id< _clauses.size(); ++cl_id) {
//  	if (_clauses[cl_id].is_built == true)
//  	    continue;

//  	CClause & cl = _clauses[cl_id];

//  	vector<int> literals;
//  	int cl1 = cl.resolvents[0];
//  	assert (_clauses[cl1].my_is_built == true);

//  	for (unsigned i=0; i< _clauses[cl1].my_literals.size(); ++i) {
//  	    int lit = _clauses[cl1].my_literals[i];
//  	    int vid = (lit>>0x1);
//  	    int sign = (lit&0x1);
//  	    assert (_variables[vid].in_clause_phase == UNKNOWN);
//  	    _variables[vid].in_clause_phase = sign;
//  	    literals.push_back(lit);
//  	}

//  	for (unsigned i=1; i< cl.resolvents.size(); ++i) {
//  	    int distance = 0;
//  	    int cl1 = cl.resolvents[i];
//  	    assert (_clauses[cl1].my_is_built == true);
//  	    for (unsigned j=0; j< _clauses[cl1].my_literals.size(); ++j) {
//  		int lit = _clauses[cl1].my_literals[j];
//  		int vid = (lit>>0x1);
//  		int sign = (lit&0x1);
//  		if (_variables[vid].in_clause_phase == UNKNOWN) {
//  		    _variables[vid].in_clause_phase = sign;
//  		    literals.push_back(lit);
//  		}
//  		else if (_variables[vid].in_clause_phase != sign) {
//  		    //distance 1 literal
//  		    ++distance;
//  		    _variables[vid].in_clause_phase = UNKNOWN;
//  		}
//  	    }
//  	    if (distance != 1) {
//  		cerr << "Resolve between two clauses with distance larger than 1" << endl;
//  		cerr << "The resulting clause is " << cl_id << endl;
//  		cerr << "Starting clause is " << cl.resolvents[0] << endl;
//  		cerr << "One of the clause involved is " << cl1 << endl;
//  		exit(1);
//  	    }
//  	}
	    
//  	for (unsigned i=0; i< literals.size(); ++i) {
//  	    int lit = literals[i];
//  	    int vid = (lit>>0x1);
//  	    int sign = (lit&0x1);
//  	    if (_variables[vid].in_clause_phase == UNKNOWN) 
//  		continue;
//  	    assert (_variables[vid].in_clause_phase == sign);
//  	    _variables[vid].in_clause_phase = UNKNOWN;
//  	    cl.my_literals.push_back(lit);
//  	}
//  	::sort(cl.my_literals.begin(), cl.my_literals.end());
//  	cl.my_is_built = true;
//      }
//  }

void CDatabase::recursive_find_involved(int cl_id) 
{
    if (_clauses[cl_id].is_involved == true)
	return;
    _clauses[cl_id].is_involved = true;
    
    recursive_construct_clause(cl_id);
    
    int num_1 = 0;
    for (unsigned i=0; i< _clauses[cl_id].literals.size(); ++i) {
	int lit = _clauses[cl_id].literals[i];
	int vid = (lit>>1);
	int sign = (lit & 0x1);
	assert (_variables[vid].value != UNKNOWN);
	if ((_variables[vid].value == 1 && sign == 0) ||
	    (_variables[vid].value == 0 && sign == 1)) {
	    if (num_1 == 0) 
		++ num_1;
	    else {
		cerr << "Clause " << cl_id << " has more than one value 1 literals " << endl;
		exit(1);
	    }
	}
	else { //literal value 0, so seek its antecedent
	    int ante = _variables[vid].antecedent;
	    recursive_find_involved(ante);
	}
    }
}

void CDatabase::recursive_construct_clause(int cl_id)
{
    CClause & cl = _clauses[cl_id];
    if (cl.is_built == true)
	return;

    assert (cl.resolvents.size() > 1);

    //I have to construct them first because of recursion may
    //mess up with the in_clause_signs. 
    for (unsigned i=0; i< cl.resolvents.size(); ++i) {
	_clauses[cl.resolvents[i]].is_needed = true;
	recursive_construct_clause(cl.resolvents[i]);
    }
    
//      cout << "Constructing clause " << cl_id << endl;
    vector<int> literals;

    //initialize
    int cl1 = cl.resolvents[0];
    assert (_clauses[cl1].is_built);
    for (unsigned i=0; i< _clauses[cl1].literals.size(); ++i) {
	int lit = _clauses[cl1].literals[i];
	int vid = (lit>>0x1);
	int sign = (lit&0x1);
	assert (_variables[vid].in_clause_phase == UNKNOWN);
	_variables[vid].in_clause_phase = sign;
	literals.push_back(lit);
    }
    
    for (unsigned i=1; i< cl.resolvents.size(); ++i) {
	int distance = 0;
	int cl1 = cl.resolvents[i];
	assert (_clauses[cl1].is_built);
	for (unsigned j=0; j< _clauses[cl1].literals.size(); ++j) {
	    int lit = _clauses[cl1].literals[j];
	    int vid = (lit>>0x1);
	    int sign = (lit&0x1);
	    if (_variables[vid].in_clause_phase == UNKNOWN) {
		_variables[vid].in_clause_phase = sign;
		literals.push_back(lit);
	    }
	    else if (_variables[vid].in_clause_phase != sign) {
				//distance 1 literal
		++distance;
		_variables[vid].in_clause_phase = UNKNOWN;
	    }
	}
	if (distance != 1) {
	    cerr << "Resolve between two clauses with distance larger than 1" << endl;
	    cerr << "The resulting clause is " << cl_id << endl;
	    cerr << "Starting clause is " << cl.resolvents[0] << endl;
	    cerr << "One of the clause involved is " << cl1 << endl;
	    exit(1);
	}
    }
    vector<int> temp_cls;
    for (unsigned i=0; i< literals.size(); ++i) {
	int lit = literals[i];
	int vid = (lit>>0x1);
	int sign = (lit&0x1);
	if (_variables[vid].in_clause_phase == UNKNOWN) 
	    continue;
	assert (_variables[vid].in_clause_phase == sign);
	_variables[vid].in_clause_phase = UNKNOWN;
	temp_cls.push_back(lit);
    }
    cl.literals.resize(temp_cls.size());
    for (unsigned i=0; i< temp_cls.size(); ++i)
	cl.literals[i] = temp_cls[i];

//      ::sort(cl.literals.begin(), cl.literals.end());
//      assert (cl.literals.size()== cl.my_literals.size());
//      for (unsigned i=0; i< cl.literals.size(); ++i)
//  	assert (cl.literals[i] == cl.my_literals[i]);
    cl.is_built = true;
    ++ _current_num_clauses;
    if (_current_num_clauses%10 == 0)
	check_mem_out();	
}

int CDatabase::recursive_find_level(int vid)
{
    int ante = _variables[vid].antecedent;
    assert (_variables[vid].value != UNKNOWN);
    assert (_variables[vid].antecedent != -1);
    assert (_clauses[ante].is_involved);
    if (_variables[vid].level != -1) 
	return _variables[vid].level;
    int level = -1;
    for (unsigned i=0; i<_clauses[ante].literals.size(); ++i) {
	int v = (_clauses[ante].literals[i] >> 1);
	int s = (_clauses[ante].literals[i] & 0x1);
	if (v == vid) {
	    assert(_variables[v].value != s);
	    continue;
	}
	else {
	    assert(_variables[v].value == s);
	    int l = recursive_find_level(v);
	    if (level < l )
		level = l;
	}
    }
    _variables[vid].level = level + 1;
    return level + 1;
}

bool CDatabase::real_verify(void)
{
    //1. If a variable is assigned value at dlevel 0, 
    //either it's pure or it has an antecedent
    for (unsigned i=1; i< _variables.size(); ++i) {
	if (_variables[i].value != UNKNOWN && _variables[i].antecedent == -1) {
	    if ((_variables[i].num_lits[0]==0 && _variables[i].value==0) || 
		(_variables[i].num_lits[1]==0 && _variables[i].value==1)) {
//  		cout << "Variable " << i << " is assigned " << _variables[i].value
//  		     << " because it is pure literal. " << endl;
	    }
	    else {
		cerr << "Don't know why variable " << i << " is assigned " << _variables[i].value
		     << " for no reasons" << endl;
		exit(1);
	    }
	}
    }
    //2. Construct the final conflicting clause if needed and find all 
    //the clauses that are involved in making it conflicting
    cout << "Begin constructing all involved clauses " << endl;
    _clauses[_conf_id].is_needed = true;
    recursive_find_involved(_conf_id);
    int count = 0;
    for (unsigned i=num_init_clauses(); i< _clauses.size(); ++i)
	if (_clauses[i].is_built)
	    ++ count;
    cout << "Num. Learned Clause:\t\t\t" << _clauses.size() - num_init_clauses() << endl;
    cout << "Num. Clause Built:\t\t\t" << count << endl;
    cout << "Constructed all involved clauses " << endl;
    
    //2.5. Verify the literals in the CONF clause
    assert(_clauses[_conf_id].is_built);
    assert(_clauses[_conf_id].is_involved);
    bool _found;
    for(unsigned i=0;i<_conf_clause.size();i++){
        _found=false;
        for(unsigned j=0;j<_clauses[_conf_id].literals.size();j++){
            if(_conf_clause[i]==_clauses[_conf_id].literals[j]){
                _found=true;
                break;
            }
        }
        if(!_found){
            cerr << "The conflict clause in trace can't be verified! "<<endl;
            cerr << "Literal "<<_conf_clause[i]<<" is not found."<<endl;
        }
    }
    cout << "Conflict clause verification finished." <<endl;

    //3. Levelize the variables that are decided at dlevel 0
    cout << "Levelize variables...";
    for (unsigned i=1; i< _variables.size(); ++i) {
	int cl_id = _variables[i].antecedent;
	if (_variables[i].value != UNKNOWN &&  cl_id != -1) {
	    if (_clauses[cl_id].is_involved) {
		int level = recursive_find_level(i);
//  		cout << "Var: " << i << " level " << level << endl;
	    }
	}
    }
    cout << "finished"<< endl;
    //4. Can we construct an empty clause? 
    cout << "Begin Resolution..." ;
    set<CVariable *, cmp_var_level> clause_lits;
    for (unsigned i=0; i< _clauses[_conf_id].literals.size(); ++i) {
	assert (lit_value(_clauses[_conf_id].literals[i]) == 0);
	int vid = (_clauses[_conf_id].literals[i] >> 1);
	clause_lits.insert(&_variables[vid]);
    }
    assert (clause_lits.size() == _clauses[_conf_id].literals.size());

    while(!clause_lits.empty()) {
//  	for (set<CVariable *, cmp_var_level>::iterator itr = clause_lits.begin();
//  	     itr != clause_lits.end(); ++itr) {
//  	    int vid = (*itr) - &_variables[0];
//  	    cout << vid << "(" << (*itr)->level << ") ";
//  	}
//  	cout << endl;

	int vid = (*clause_lits.begin() - &_variables[0]);
	int ante = _variables[vid].antecedent;
	if (ante == -1) {
	    cerr << "Variable " << vid << " has an NULL antecedent ";
	    exit(1);
	}
	_clauses[ante].is_needed = true;
	clause_lits.erase(clause_lits.begin());
	_variables[vid].in_clause_phase = 1;
	CClause & cl = _clauses[ante];
	int distance = 0;
	for (unsigned i=0; i< cl.literals.size(); ++i) {
	    int l = cl.literals[i];
	    int v = (l>>1);
	    assert (_variables[v].value != UNKNOWN);
	    if (lit_value(l) == 1) {
		if (vid != v) {
		    cerr << "The antecedent of the variable is not really an antecedent " << endl;
		    exit(1);
		}
		else 
		    ++distance;
	    }
	    else
		clause_lits.insert(&_variables[v]);
	}
	assert (distance == 1);
    }
    cout << " Empty clause generated." << endl;
    cout << "Mem Usage :\t\t\t\t" << get_mem_usage()<< endl;
    int needed_cls_count = 0;
    int needed_var_count = 0;
    for (int i=0; i< num_init_clauses(); ++i) {
	if (_clauses[i].is_needed == true) {
	    ++ needed_cls_count;
	    for (unsigned j=0; j< _clauses[i].literals.size(); ++j) {
		int vid = (_clauses[i].literals[j] >> 1);
		if (_variables[vid].is_needed == false) {
		    ++ needed_var_count;
		    _variables[vid].is_needed = true;
		}
	    }
	}
    }
    cout << "Original Num. Clauses:\t\t\t" << num_init_clauses() << endl;
    cout << "Needed Clauses to Construct Empty:\t"<< needed_cls_count << endl;
    cout << "Total Variable count:\t\t\t" << _variables.size()-1 << endl;
    cout << "Variables involved in Empty:\t\t" << needed_var_count << endl;

    for (unsigned i=0; i< _clauses.size(); ++i) {
	if (_clauses[i].is_built)
	    assert (_clauses[i].is_needed || i < (unsigned)num_init_clauses());
    }
    if (_dump_core == true) {
	cout << "Unsat Core dumped:\t\t\tunsat_core.cnf" << endl;
	ofstream dump("unsat_core.cnf");
	dump << "c Variables Not Involved: ";
	unsigned int k=0;
	for (unsigned i=1; i< _variables.size(); ++i) {
	    if (_variables[i].is_needed == false) {
		if (k%20 == 0) 
		    dump << endl << "c ";
		++k;
		dump << i << " ";
	    }
	}
	dump << endl;
	dump << "p cnf " << _variables.size()-1 << " " << needed_cls_count << endl;
	for (int i=0; i< num_init_clauses(); ++i) {
	    if (_clauses[i].is_needed) {
		dump << "c Original Cls ID: " << i << endl;
		for (unsigned j=0; j< _clauses[i].literals.size(); ++j)
		    dump << ((_clauses[i].literals[j] & 0x1)?" -":" ") << (_clauses[i].literals[j] >> 1);
		dump << " 0" << endl;
	    }
	}
    }
    return true;
}

bool CDatabase::verify(char * filename)
{	
    vector<char> buffer;
    char token [WORD_LEN];

    ifstream in_file (filename);
    if (!in_file) {
	cerr << "Can't open input CNF file " << filename << endl;
	exit(1);
    }
    
    while (!in_file.eof()) {
	get_line(in_file, buffer);
	char * ptr = &(*buffer.begin());
	get_token(ptr, token);
	if (strcmp (token, "CL:") == 0) {
	    vector<int> resolvents;

	    get_token(ptr, token);
	    int cl_id = my_a2i(token);

	    get_token(ptr, token);
	    assert (strcmp(token, "<=") == 0);

	    while (get_token(ptr, token)) {
		int r = my_a2i(token);
		resolvents.push_back(r);
	    }
	    int c = add_learned_clause_by_resolvents(resolvents);
	    assert (c == cl_id);
	}
	else if (strcmp (token, "VAR:") == 0) {
	    get_token(ptr,token);
	    int vid = my_a2i(token);

	    get_token(ptr,token);
	    assert (strcmp(token, "L:") == 0);
	    get_token(ptr, token); //skip the level
		
	    get_token(ptr,token);
	    assert (strcmp(token, "V:") == 0);
	    get_token(ptr,token);
	    int value = my_a2i(token);
	    assert (value == 1 || value == 0);

	    get_token(ptr,token);
	    assert (strcmp(token, "A:") == 0);
	    get_token(ptr,token);
	    int ante = my_a2i(token);

	    get_token(ptr,token);
	    assert (strcmp(token, "Lits:") == 0);

	    _variables[vid].value = value;
	    _variables[vid].antecedent = ante;
	}
	else if (strcmp (token, "CONF:") == 0) {
	    get_token(ptr,token);
	    _conf_id = my_a2i(token);

	    get_token(ptr,token);
	    assert (strcmp(token, "==") == 0);

	    while (get_token(ptr, token)) {
		int lit = my_a2i(token);
		assert (lit > 0);
		assert ((lit>>1) < (int)_variables.size());
		_conf_clause.push_back(lit);
	    }
	}
    }	
    if (_conf_id == -1) {
	cerr << "No final conflicting clause defined " << endl;
	exit (1);
    }
    cout << "Mem Usage After Readin file:\t\t" << get_mem_usage() << endl;
//      construct_learned_clauses();
//      for (unsigned i=num_init_clauses(); i< _clauses.size(); ++i) {
//  	assert (_clauses[i].my_is_built);
//  	for (unsigned j=0; j< _clauses[i].my_literals.size(); ++j) {
//  	    int svar = _clauses[i].my_literals[j];
//  	    int vid = (svar>>1);
//  	    int sign = (svar&0x1);
//  	    cout << (sign?"-":"") << vid << " " ;
//  	}
//  	cout << endl;
//      }
//      return true;
    return real_verify();
}

int main(int argc, char * * argv)
{
    cout << "ZVerify SAT Solver Verifier" << endl;
    cout << "Copyright Princeton University, 2003-2004. All Right Reseverd." << endl;
    if (argc != 3 && argc !=4) {
	cerr << "Usage: " << argv[0] << " CNF_File Dump_File [-core]" << endl
	     << "-core: dump the unsat core " << endl;
	cerr << endl;
	exit(1);
    }
    if (argc == 3) 
	_dump_core = false;
    else {
	assert (argc == 4);
	if (strcmp(argv[3], "-core") != 0) {
	    cerr << "Must use -core as the third parameter" << endl;
	    exit(1);
	}
	_dump_core = true;
    }
    cout << "COMMAND LINE: ";
    for (int i=0; i< argc; ++i) 
	cout << argv[i] << " ";
    cout << endl;

    _peak_mem = get_mem_usage();
    CDatabase dbase;
    double begin_time = get_cpu_time();
    dbase.read_cnf(argv[1]);
    if (dbase.verify(argv[2]) == true) {
	double end_time = get_cpu_time();
	cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl;
	cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl;
	cout << "Verification Successful " << endl;
    }
    else {
	cout << "Failed to verify the result " << endl;
    }
}










