zchaff_dbase.cpp

/*********************************************************************
 Copyright 2000-2003, 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 <stdlib.h>
#include "zchaff_dbase.h"

CDatabase::CDatabase()  
{ 	
    _stats.mem_used_up_counts 	= 0;
    _stats.mem_used_up 		= false;

    _stats.init_num_clauses 	= 0;
    _stats.init_num_literals 	= 0;
    _stats.num_added_clauses 	= 0;
    _stats.num_added_literals 	= 0;
    _stats.num_deleted_clauses 	= 0;
    _stats.num_deleted_literals = 0;
    _stats.num_enlarge		= 0;
    _stats.num_compact		= 0;
    _lit_pool_start = (CLitPoolElement *) malloc (sizeof(CLitPoolElement) * STARTUP_LIT_POOL_SIZE); 
    _lit_pool_finish = _lit_pool_start;
    _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE;
    lit_pool_push_back(0); //set the first element as a spacing element

    _params.mem_limit = 1024*1024*1024; //that's 1 G

    variables().resize(1);	//var_id == 0 is never used.
    _allocated_gid    		= 0;
}

CDatabase::~CDatabase()
{ 
    free (_lit_pool_start); 
}

unsigned CDatabase::estimate_mem_usage (void)
{
    unsigned mem_lit_pool = sizeof(CLitPoolElement) * (lit_pool_size() + lit_pool_free_space());

    unsigned mem_vars = sizeof(CVariable) * variables().capacity();

    unsigned mem_cls = sizeof(CClause) * clauses().capacity();

    unsigned mem_cls_queue = sizeof(int) * _unused_clause_idx.size();

    unsigned mem_watched = 2 * num_clauses() *	sizeof(CLitPoolElement *);

    unsigned mem_lit_clauses = 0;
#ifdef KEEP_LIT_CLAUSES
    //mem_lit_clauses = num_literals() * sizeof(ClauseIdx);
	mem_lit_clauses = init_num_literals () * sizeof(ClauseIdx); // changed by sang
#endif

    return (mem_lit_pool + mem_vars + mem_cls +
	    mem_cls_queue + mem_watched + mem_lit_clauses);	//commented out by sang

	//return (mem_vars + mem_cls +
	//    mem_cls_queue + mem_watched + mem_lit_clauses); // added by sang
}

unsigned CDatabase::mem_usage(void) {
    int mem_lit_pool = (lit_pool_size() + lit_pool_free_space()) * sizeof(CLitPoolElement);

    int mem_vars = sizeof(CVariable) * variables().capacity();

    int mem_cls = sizeof(CClause) * clauses().capacity();

    int mem_cls_queue = sizeof(int) * _unused_clause_idx.size();

    int mem_watched = 0, mem_lit_clauses = 0;

    for (unsigned i=0, sz = variables().size(); i < sz ;  ++i) {
	CVariable & v = variable(i);
	mem_watched	+= v.watched(0).capacity() + v.watched(1).capacity(); 
#ifdef KEEP_LIT_CLAUSES
	mem_lit_clauses += v.lit_clause(0).capacity() + v.lit_clause(1).capacity();	
#endif
    }
    mem_watched *= sizeof(CLitPoolElement*);
    mem_lit_clauses *= sizeof(ClauseIdx);
    return (mem_lit_pool + mem_vars + mem_cls + 
	    mem_cls_queue + mem_watched + mem_lit_clauses);
}

int CDatabase::alloc_gid (void)
{
    for (unsigned i=1; i<= WORD_WIDTH; ++i)
	if (is_gid_allocated(i) == false) {
	    _allocated_gid |= (1 << (i-1));
	    return i;
	}
    warning(_POSITION_, "Not enough GID");
    return VOLATILE_GID;
}

void CDatabase::free_gid (int gid) 
{
    assert (gid > 0 && "Can't free volatile or permanent group");
    assert (gid <= WORD_WIDTH && "gid > WORD_WIDTH?" );
    if (is_gid_allocated(gid)==false) {
	fatal(_POSITION_,"Can't free unallocated GID");
    }
    _allocated_gid &= (~(1<< (gid-1)));
}

bool CDatabase::is_gid_allocated(int gid) 
{
    if (gid==VOLATILE_GID || gid==PERMANENT_GID) 
	return true;
    assert (gid<= WORD_WIDTH && gid > 0);	
    if (_allocated_gid & (1 << (gid -1))) 
	return true;
    return false;
}

int CDatabase::merge_clause_group(int g2, int g1) 
{
    assert (g1 >0 && g2> 0 && "Can't merge with permanent or volatile group");
    assert (g1 != g2);
    assert (is_gid_allocated(g1) && is_gid_allocated(g2));
    for (unsigned i=0, sz=clauses().size(); i<sz; ++i) 
	if (clause(i).status() != DELETED_CL)
	    if (clause(i).gid(g1) == true) {
		clause(i).clear_gid(g1);
		clause(i).set_gid(g2);	
	    }
    free_gid (g1);
    return g2;
}


// old version
/*void CDatabase::mark_clause_deleted(CClause & cl) {
    ++_stats.num_deleted_clauses;
    _stats.num_deleted_literals += cl.num_lits();
    cl.set_status(DELETED_CL);
    for (unsigned i=0; i< cl.num_lits(); ++i) {
	CLitPoolElement & l = cl.literal(i);
	//--variable(l.var_index()).lits_count(l.var_sign()); //commented out by sang
	//--variable(l.var_index()).score(l.var_sign());	//commented out by sang
	l.val() = 0;
    }
    _unused_clause_idx.push( &cl - &(*clauses().begin()));
}*/

// new version
void CDatabase::mark_clause_deleted(CClause & cl) {
    ++_stats.num_deleted_clauses;
    _stats.num_deleted_literals += cl.num_lits();

    CLAUSE_STATUS status=cl.status();
    if(status==ORIGINAL_CL) 
        _stats.num_del_orig_cls++;
    cl.set_status(DELETED_CL);
    for (unsigned i=0; i< cl.num_lits(); ++i) {
	CLitPoolElement & l = cl.literal(i);
	--variable(l.var_index()).lits_count(l.var_sign());
	l.val() = 0;
    }
	_unused_clause_idx.push( &cl - &(*clauses().begin()));
    //_unused_clause_idx.insert( &cl - &(*clauses().begin()));
}



bool CDatabase::is_conflicting(ClauseIdx cl)
{
    CLitPoolElement * lits = clause(cl).literals();
    for (int i=0, sz= clause(cl).num_lits(); i<sz;  ++i)
	if (literal_value(lits[i]) != 0)
	    return false;
    return true;
}

bool CDatabase::is_satisfied(ClauseIdx cl)
{
    CLitPoolElement * lits = clause(cl).literals();
    for (int i=0, sz= clause(cl).num_lits(); i<sz; ++i) 
	if (literal_value(lits[i]) == 1) 
	    return true;
    return false;
}

bool CDatabase::is_unit (ClauseIdx cl)
{
    int num_unassigned = 0;
    CLitPoolElement * lits = clause(cl).literals();
    for (int i=0, sz= clause(cl).num_lits(); i<sz;  ++i) {
	int value = literal_value(lits[i]);
	if (value == 1)
	    return false;
	else if (value != 0)
	    ++ num_unassigned; 
    }
    return ( num_unassigned == 1);
}

int CDatabase::find_unit_literal(ClauseIdx cl) 
//will return 0 if not unit
{
    int unit_lit = 0;
    for (int i=0, sz= clause(cl).num_lits(); i<sz;  ++i) {
	int value =literal_value(clause(cl).literal(i));
	if ( value == 1)
	    return 0;
	else if (value != 0) {
	    if (unit_lit == 0)
		unit_lit = clause(cl).literals()[i].s_var();
	    else 
		return 0;
	}
    }
    return unit_lit;
}

CLitPoolElement * CDatabase::lit_pool_begin(void) 
{ 
    return _lit_pool_start; 
}

CLitPoolElement * CDatabase::lit_pool_end(void) 
{ 
    return _lit_pool_finish; 
}

void CDatabase::lit_pool_incr_size( int size) 
{
    _lit_pool_finish += size; 
    assert (_lit_pool_finish <= _lit_pool_end_storage);
}

void CDatabase::lit_pool_push_back(int value) 
{ 
    assert (_lit_pool_finish <= _lit_pool_end_storage );
    _lit_pool_finish->val() = value;
    ++ _lit_pool_finish;
}

int CDatabase::lit_pool_size(void) 
{ 
    return _lit_pool_finish - _lit_pool_start; 
}

int CDatabase::lit_pool_free_space(void) 
{ 
    return _lit_pool_end_storage - _lit_pool_finish; 
}

double CDatabase::lit_pool_utilization(void) 
{
    //minus num_clauses() is because of spacing (i.e. clause indices)
    return (double)num_literals()/((double) (lit_pool_size() - num_clauses())) ; 
}

CLitPoolElement & CDatabase::lit_pool(int i) 
{
    return _lit_pool_start[i];
}

void CDatabase::compact_lit_pool(void)
{
    unsigned i, sz;
    DBG1(cout << "Begin Compaction...... " << 
	 endl << "***Before Compaction "<< endl;  
	 output_lit_pool_stats(););
    int new_index = 1;
    //first do the compaction for the lit pool
    for (i=1, sz= lit_pool_size(); i<sz;  ++i){ //begin with 1 because 0 position is always 0
	if (!lit_pool(i).is_literal() && !lit_pool(i-1).is_literal())
	    continue;
	else {
	    lit_pool(new_index) = lit_pool(i);
	    ++new_index;
	}
    }
    _lit_pool_finish = lit_pool_begin() + new_index;
    //update all the pointers to the literals;
    //1. clean up the watched pointers from variables
    for (i=1, sz = variables().size(); i< sz;  ++i) {
	variable(i).watched(0).clear();
	variable(i).watched(1).clear();
    }
    for (i=1, sz = lit_pool_size(); i<sz;  ++i) {
	CLitPoolElement & lit = lit_pool(i);
        //2. reinsert the watched pointers
	if (lit.is_literal()) {
	    if (lit.is_watched()) {
		int var_idx = lit.var_index();
		int sign = lit.var_sign();
		variable(var_idx).watched(sign).push_back(& lit_pool(i));
	    }
	}
	//3. update the clauses' first literal pointer
	else { //lit is not literal
	    int cls_idx = lit.get_clause_index();
	    clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits();
	}
    }
    DBG1(cout << "***After Compaction " << endl; 
	 output_lit_pool_stats(); 
	 cout << endl << endl;);
    ++_stats.num_compact;
}

bool CDatabase::enlarge_lit_pool(void) //will return true if successful, otherwise false.
{
    unsigned i, sz;
    //if memory efficiency < 2/3, we do a compaction
    if ( lit_pool_utilization() < 0.67) {
	compact_lit_pool();
	return true;
    }
    //otherwise we have to enlarge it.
    DBG1(cout << "Begin Enlarge Lit Pool" << endl;);
    //first, check if memory is running out
    int current_mem = estimate_mem_usage();
    float grow_ratio = 1;
    if (current_mem < _params.mem_limit /4 ) 
	grow_ratio = 2;
    else if (current_mem < _params.mem_limit /2 ) 
	grow_ratio = 1.5;
    else if (current_mem < _params.mem_limit * 0.8) 
	grow_ratio = 1.2;
    if (grow_ratio < 1.2) {
	if ( lit_pool_utilization() < 0.9) {  //still has some garbage
	    cout << "compaction needed, lit_pool_utilization() = " 
	    << lit_pool_utilization() << endl;
	    compact_lit_pool();
	    return true;
	}
	else {
	// return false;	// commented out by sang
		cout << "compaction needed, lit_pool_utilization() = "
            	<< lit_pool_utilization() << endl; // added by sang
	   compact_lit_pool();  // added by sang
	   return true;		// added by sang
	}
    }
    //second, make room for new lit pool.
    CLitPoolElement * old_start = _lit_pool_start;
    CLitPoolElement * old_finish = _lit_pool_finish;
    int old_size = _lit_pool_end_storage - _lit_pool_start;
    int new_size = (int)(old_size * grow_ratio);
    _lit_pool_start = (CLitPoolElement *) realloc( _lit_pool_start, sizeof(CLitPoolElement) * new_size);
    _lit_pool_finish = _lit_pool_start + (old_finish - old_start);
    _lit_pool_end_storage = _lit_pool_start + new_size;

    //update all the pointers
    int displacement = _lit_pool_start - old_start;
    for (i=0; i< clauses().size(); ++i)
	if (clause(i).status()!=DELETED_CL) 
	    clause(i).first_lit() += displacement; 

    for (i=0, sz = variables().size(); i < sz ;  ++i) {
	CVariable & v = variable(i);
	for (int j=0; j< 2 ; ++j) {
	    int k, sz1;
	    vector<CLitPoolElement *> & watched = v.watched(j);
	    for (k=0, sz1 = watched.size(); k< sz1 ; ++k) {
		watched[k] += displacement; 
	    }
	}
    }
    DBG1(output_lit_pool_stats();
	 cout << endl << endl;);
    ++_stats.num_enlarge;
    return true;
}

ClauseIdx CDatabase::get_free_clause_idx(void)
{
    ClauseIdx new_cl;
    if (_unused_clause_idx.empty()) {
	new_cl = _clauses.size();
	_clauses.resize(new_cl + 1);
    }
    else {
	new_cl = _unused_clause_idx.front();
	_unused_clause_idx.pop();
    }
    clause(new_cl).set_id(_stats.num_added_clauses);
    return new_cl;
}

ClauseIdx CDatabase::add_clause(int * lits, int n_lits, int gflag , bool original)  { 
    int new_cl;
    //a. do we need to enlarge lits pool?
    while (lit_pool_free_space() <= n_lits + 1) { 
	if (enlarge_lit_pool()==false) 
	    return -1; //mem out, can't enlarge lit pool, because 
	//ClauseIdx can't be -1, so it shows error.
    }	
    //b. get a free cl index;
	//if (_stats.num_added_clauses < ADDED_CL_MAX)	// added by sang
	new_cl = get_free_clause_idx();
	/*else // no space for more added clauses, so clear and reuse clause(ADDED_CL_MAX)
	{
		cout << "no space for more added clauses, "
			 << "so clear and reuse clause(" << ADDED_CL_MAX << ")" << endl;
		new_cl = ADDED_CL_MAX;
		//clause(new_cl)._status = UNKNOWN_CL;
		//clause(new_cl)._counter_one = 0;	// added by sang		
	}*/

    //c. add the clause lits to lits pool
    CClause & cl = clause(new_cl);
    cl.init(lit_pool_end(), n_lits, gflag);
    lit_pool_incr_size(n_lits + 1);
    for (int i=0; i< n_lits; ++i){
	int var_idx = lits[i]>>1;
	assert((unsigned)var_idx < variables().size());
	int var_sign = lits[i]&0x1;
	cl.literal(i).set(var_idx, var_sign);
	++variable(var_idx).lits_count(var_sign);
#ifdef KEEP_LIT_CLAUSES	// need to determine if it is a conflict clause to add
	//if (new_cl < _stats.init_num_clauses) // only keep track of original clauses
	// variable(var_idx).lits_clauses(var_sign).push_back(new_cl);
#ifndef DISABLE_CLASUES
	if (original)	// only keep track of original clauses
#endif
		variable(var_idx).lit_clause(var_sign).push_back(new_cl); // corrected by sang
#endif
    }
    //the element after the last one is the spacing element
    cl.literal(n_lits).set_clause_index(new_cl); 
    //d. set the watched pointers
    if (cl.num_lits() > 1) {
	//add the watched literal. note: watched literal must be the last free var
	int max_idx = -1, max_dl = -1;
	int i, sz = cl.num_lits();
	//set the first watched literal
	for (i=0; i< sz; ++i) {
	    int v_idx = cl.literal(i).var_index();
	    int v_sign = cl.literal(i).var_sign();
	    CVariable & v = variable(v_idx);
	    if (literal_value(cl.literal(i)) != 0 ){
		v.watched(v_sign).push_back( & cl.literal(i));
		cl.literal(i).set_watch(1);
		break;
	    }
	    else {
		if (v.dlevel() > max_dl) {
		    max_dl = v.dlevel();
		    max_idx = i;
		}
	    }
	}
	if (i >= sz) { //no unassigned literal. so watch literal with max dlevel
	    int v_idx = cl.literal(max_idx).var_index();
	    int v_sign = cl.literal(max_idx).var_sign();
	    variable(v_idx).watched(v_sign).push_back( & cl.literal(max_idx));
	    cl.literal(max_idx).set_watch(1);
	}
	//set the second watched literal
	max_idx = -1; max_dl = -1;
	for (i=sz-1; i>=0; --i) {
	    if (cl.literal(i).is_watched())
		continue; // need to watch two different literals
	    int v_idx = cl.literal(i).var_index();
	    int v_sign = cl.literal(i).var_sign();
	    CVariable & v = variable(v_idx);
	    if (literal_value(cl.literal(i)) != 0) {
		v.watched(v_sign).push_back( & cl.literal(i));
		cl.literal(i).set_watch(-1);
		break;
	    }
	    else {
		if (v.dlevel() > max_dl) {
		    max_dl = v.dlevel();
		    max_idx = i;
		}
	    }
	}
	if (i < 0) {
	    int v_idx = cl.literal(max_idx).var_index();
	    int v_sign = cl.literal(max_idx).var_sign();
	    variable(v_idx).watched(v_sign).push_back( & cl.literal(max_idx));
	    cl.literal(max_idx).set_watch(-1);
	}
    }
    //update some statistics
    ++_stats.num_added_clauses; 
    _stats.num_added_literals += n_lits;
    if (new_cl < 0)
    	cout << " new_cl < 0 in CDatabase::add_clause()! " << endl; // added by sang
    return new_cl;
}


void CDatabase::output_lit_pool_stats (void) 
{
    cout << "Lit_Pool Used " << lit_pool_size() << " Free " << lit_pool_free_space()
	 << " Total " << lit_pool_size() + lit_pool_free_space()
	 << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals(); 
    cout << " Efficiency " <<  lit_pool_utilization() << endl;
}


void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os ) 
{
    os << "CL : " << cl_idx;
    CClause & cl = clause(cl_idx);
    if (cl.status()==DELETED_CL) 
	os << "\t\t\t======removed=====";
    char value;
    for (unsigned i=0; i< cl.num_lits(); ++i) {
	if (literal_value(cl.literal(i))==0) value = '0';
	else if (literal_value(cl.literal(i))==1) value = '1';
	else value = 'X';
	os << cl.literal(i) << "(" << value << "@" << variable(cl.literal(i).var_index()).dlevel()<< ")  ";
    }
    os << endl;
}

void CDatabase::dump(ostream & os) {
    unsigned i;
    os << "Dump Database: " << endl;
    for( i=0; i<_clauses.size(); ++i) 
	detail_dump_cl(i);
    for( i=1; i<_variables.size(); ++i)
	os << "VID " << i << ":\t" << variable(i);
}