zcore_extract.bak

这是一种很好的SAT解析器。通过它

		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 literals without termination in the last clause" << endl;
	exit(1);
    }
    if (clauses().size() != (unsigned) num_init_clauses()) {
	cerr << "WARNING : Clause count inconsistant with the header " << endl;
	cerr << "Header indicates " << num_init_clauses() << " Clauses " << endl;
    }
    cout << "Successfully read " << num_init_clauses() << " Clauses " << endl;
}

void CDatabase::produce_core(char * filename)
{
    parse_trace(filename);
    set<CVariable *, cmp_var_level> clause_lits;
    for (unsigned i=0; i< _conf_clause.size();  ++i) {
	int vid = (_conf_clause[i]>> 1);
	clause_lits.insert(&_variables[vid]);
    }
    assert (clause_lits.size() == _conf_clause.size());	
    _empty_r_source.push_back(_conf_id);
    while(!clause_lits.empty()) {
	int vid = (*clause_lits.begin() - &_variables[0]);
	int ante = _variables[vid].antecedent;
	if (ante == -1) {
	    cerr << "Variable " << vid << " has an NULL antecedent ";
	    exit(1);
	}
	clause_lits.erase(clause_lits.begin());
	_empty_r_source.push_back(ante);
	vector<int> & lits = _variables[vid].claimed_ante_lits;
	for (unsigned i=0; i< lits.size(); ++i) {
	    int l = lits[i];
	    int v = (l>>1);
	    if (v != vid)
		clause_lits.insert(&_variables[v]);
	}
    }
    cout << "Empty clause resolve-sources generated. " << endl;
    cout << "Mem Usage:\t\t\t\t" << get_mem_usage()<< endl;
    calculate_unsat_core();
}

void CDatabase::parse_trace(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 storage[resolvents.size() + 2];
	    storage[0] = - cl_id;
	    storage[1] = - resolvents.size();
	    for (unsigned j=0; j< resolvents.size(); ++j)
		storage[j+2] = resolvents[j];
	    fwrite(storage, sizeof(int), resolvents.size() + 2, _tmp_rsource_fp);
	}
	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);
	    int lev = my_a2i(token);
		
	    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);
	    vector<int> cl_literals;
	    while (get_token(ptr, token)) {
		int r = my_a2i(token);
		cl_literals.push_back(r);
	    }

	    _variables[vid].value = value;
	    _variables[vid].antecedent = ante;
	    _variables[vid].level = lev;
	    for (unsigned j=0; j< cl_literals.size(); ++j) 
		_variables[vid].claimed_ante_lits.push_back(cl_literals[j]);
	}
	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 ( (unsigned)(lit>>1) < _variables.size());
		_conf_clause.push_back(lit);
	    }
	}
    }	
    if (_conf_id == -1) {
	cerr << "No final conflicting clause defined " << endl;
	exit (1);
    }
    cout << "Mem Usage After Read in File:\t\t" << get_mem_usage() << endl;
}

FILE * CDatabase::reverse_file(FILE * fp_in)
{
    //currently fp_in point to the end of the input file
    assert ((unsigned)MAX_BUFF_SIZE > _variables.size() * 2 
	    && "Buffer must be able to contain at least 2 biggest clauses"); 
    int * read_buff;
    read_buff = (int *) malloc((MAX_BUFF_SIZE + _variables.size())*sizeof(int));
    int * write_buff;
    write_buff = (int*) malloc((MAX_BUFF_SIZE + _variables.size()) * sizeof(int));

    long file_size = ftell(fp_in)/sizeof(int);
    assert (ftell(fp_in)%sizeof(int) == 0);
    int num_trunks = file_size/MAX_BUFF_SIZE;

    FILE * fp = tmpfile();
    int last_remain = 0;
    for (int i=0; i< num_trunks; ++i) {
	cout << i << " ";
	cout.flush();
	fseek(fp_in, -MAX_BUFF_SIZE*sizeof(int), SEEK_CUR);
	int r = fread(read_buff, sizeof(int), MAX_BUFF_SIZE, fp_in);
	assert (r == MAX_BUFF_SIZE);
	fseek(fp_in, -MAX_BUFF_SIZE*sizeof(int), SEEK_CUR);
	int write_idx = 0;
	for (int index=MAX_BUFF_SIZE - 1 + last_remain; index>= 1; --index) {
	    if (read_buff[index] < 0) {
		assert (read_buff[index -1] < 0);
		int num_lits = -read_buff[index];
		-- index;
		for (int j=0; j< num_lits + 2; ++j)
		    write_buff[write_idx ++] = read_buff[j + index];
	    }
	}
	fwrite(write_buff, sizeof(int), write_idx, fp);
	last_remain = 0;
	for (int j = 0; j < MAX_BUFF_SIZE; ++j) {
	    if (read_buff[j] < 0 && read_buff[j+1] < 0)
		break;
	    else 
		read_buff[j + MAX_BUFF_SIZE] = read_buff[j];
	    ++ last_remain;
	}
    }
    //the last trunk
    int last_trunk_size = file_size%MAX_BUFF_SIZE;
    int last_trunk_begin = MAX_BUFF_SIZE - last_trunk_size;
    assert (ftell(fp_in) == (long) (last_trunk_size * sizeof(int)));
    fseek(fp_in, -last_trunk_size*sizeof(int), SEEK_CUR);
    fread(read_buff + last_trunk_begin, sizeof(int), last_trunk_size, fp_in);
    int index; 
    int write_idx = 0;

    for (index = MAX_BUFF_SIZE-1 + last_remain; index >= last_trunk_begin + 1; --index) {
	if (read_buff[index] < 0) {
	    assert (read_buff[index -1] < 0);
	    int num_lits = -read_buff[index];
	    -- index;
	    for (int j=0; j< num_lits + 2; ++j)
		write_buff[write_idx ++] = read_buff[j + index];
	}	
    }
    fwrite(write_buff, sizeof(int), write_idx, fp);
    //assert (read_buff[last_trunk_begin] < 0 &&
//	    read_buff[last_trunk_begin+1] < 0);
    check_mem_out();
    free(read_buff);
    free(write_buff);
    return fp;
}

void CDatabase::print_file(FILE * fp)
{
    ofstream out("out_file");
    int inputs[_variables.size()];
    int info[2];
    int pos = ftell(fp);
    rewind(fp);
    fread(info, sizeof(int), 2, fp);
    while (!feof(fp)) {
	assert (info[0] < 0);
	assert (info[1] < 0);
	unsigned num_in = -info[1];
	assert ( num_in < _variables.size());
	fread(inputs, sizeof(int), num_in, fp);
	out << "CL : " << -info[0] << " Num: "<< num_in << " :";
	for (unsigned i=0; i< num_in; ++i)
	    out << inputs[i] << " ";
	out << endl;
	fread(info, sizeof(int), 2, fp);
    }	
    fseek (fp, pos, SEEK_SET);
}

void CDatabase::calculate_unsat_core(void)
{
    int num_edges = 0;
    int num_nodes = 0;
    int max_involved = 0;
    FILE * r_source_fp;
    r_source_fp = reverse_file(_tmp_rsource_fp);
    fclose(_tmp_rsource_fp);
    rewind(r_source_fp);
    hash_set<int> involved;
    for (unsigned i=0; i< _empty_r_source.size(); ++i)
	involved.insert(_empty_r_source[i]);
    max_involved =involved.size();
    
    int r_source[_variables.size()];
    int info[2];
    
    fread(info, sizeof(int), 2, r_source_fp);
    while (!feof(r_source_fp)) {
	assert (info[0] < 0);
	assert (info[1] < 0);
	int cl_id = -info[0];
	unsigned  num_srcs = -info[1];
	num_edges += num_srcs;
	num_nodes ++;
	assert ( num_srcs < _variables.size());
	fread(r_source, sizeof(int), num_srcs, r_source_fp);
	if (involved.find(cl_id) != involved.end()) {
	    involved.erase(cl_id);
	    for (unsigned i=0; i< num_srcs; ++i) {
		int s= r_source[i];
		assert (s < cl_id);
		involved.insert(s);
	    }
	    if (max_involved < (int)involved.size())
		max_involved = involved.size();
	}
	fread(info, sizeof(int), 2, r_source_fp);
    }	
    fclose(r_source_fp);

    int needed_cls_count = 0;
    int needed_var_count = 0;
    for (int i=0; i< num_init_clauses(); ++i) {
	if (involved.find(i) != involved.end()) {
	    ++ needed_cls_count;
	    CClause & cl = _clauses[i];
	    for (unsigned j=0; j< cl.literals.size(); ++j) {
		int vid = (cl.literals[j] >> 1);
		if (_variables[vid].is_needed == false) {
		    ++ needed_var_count;
		    _variables[vid].is_needed = true;
		}
	    }
	}
    }
    cout << "Num. Learned Clauses\t\t\t" << num_nodes << endl;
    cout << "Num. Resolve Sources\t\t\t" << num_edges << endl;
    cout << "Max Hash Size\t\t\t\t" << max_involved << endl;
    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;

    ofstream dump(_core_file_name);

    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 (involved.find(i) != involved.end()) {
	    CClause & cl = _clauses[i];
	    dump << "c Original Cls ID: " << i << endl;
	    for (unsigned j=0; j< cl.literals.size(); ++j)
		dump << ((cl.literals[j] & 0x1)?" -":" ") << (cl.literals[j] >> 1);
	    dump << " 0" << endl;
	}
    }
}

int main(int argc, char * * argv)
{
    cout << "ZExtract: UnSAT Core Extractor" << endl;
    cout << "Copyright Princeton University, 2003-2004. All Right Reserved." << endl;
    if (argc != 3 && argc != 4) {
	cerr << "Usage: " << argv[0] 
	     << " CNF_File  Resolve_Trace  [Core_Filename = unsat_core.cnf]" << endl;
	cerr << endl;
	exit(1);
    }
    cout << "COMMAND LINE: ";
    for (int i=0; i< argc; ++i) 
	cout << argv[i] << " ";
    cout << endl;
    if (argc == 4)
	_core_file_name = argv[3];
	
    _peak_mem = get_mem_usage();

    CDatabase dbase;

    double begin_time = get_cpu_time();
    cout << "Read in original clauses ... " << endl;
    dbase.read_cnf(argv[1]);
    dbase.produce_core(argv[2]);
    double end_time = get_cpu_time();
    cout << "Unsat Core Produced Successfully:\t" << _core_file_name << endl;
    cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl;
    cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl;
}