xchaff_dbase.cpp

Go to the documentation of this file.
00001 /* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */
00002 
00003 /*********************************************************************
00004  Copyright 2000-2001, Princeton University.  All rights reserved. 
00005  By using this software the USER indicates that he or she has read, 
00006  understood and will comply with the following:
00007 
00008  --- Princeton University hereby grants USER nonexclusive permission 
00009  to use, copy and/or modify this software for internal, noncommercial,
00010  research purposes only. Any distribution, including commercial sale 
00011  or license, of this software, copies of the software, its associated 
00012  documentation and/or modifications of either is strictly prohibited 
00013  without the prior consent of Princeton University.  Title to copyright
00014  to this software and its associated documentation shall at all times 
00015  remain with Princeton University.  Appropriate copyright notice shall 
00016  be placed on all software copies, and a complete copy of this notice 
00017  shall be included in all copies of the associated documentation.  
00018  No right is  granted to use in advertising, publicity or otherwise 
00019  any trademark,  service mark, or the name of Princeton University. 
00020 
00021 
00022  --- This software and any associated documentation is provided "as is" 
00023 
00024  PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS 
00025  OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A 
00026  PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR 
00027  ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, 
00028  TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.  
00029 
00030  Princeton University shall not be liable under any circumstances for 
00031  any direct, indirect, special, incidental, or consequential damages 
00032  with respect to any claim by USER or any third party on account of 
00033  or arising from the use, or inability to use, this software or its 
00034  associated documentation, even if Princeton University has been advised
00035  of the possibility of those damages.
00036 *********************************************************************/
00037 
00038 #include "xchaff_utils.h"
00039 #include "xchaff_dbase.h"
00040 
00041 CDatabase::CDatabase() : _variables(1)
00042 { 
00043     _stats.mem_used_up_counts = 0;
00044     _stats.mem_used_up = false;
00045 
00046     _stats.init_num_clauses = 0;
00047     _stats.init_num_literals = 0;
00048     _stats.num_added_clauses = 0;
00049     _stats.num_added_literals = 0;
00050     _stats.num_deleted_clauses = 0;
00051     _stats.num_deleted_literals = 0;
00052 
00053     _lit_pool_start = new CLitPoolElement[STARTUP_LIT_POOL_SIZE]; 
00054     _lit_pool_finish = _lit_pool_start;
00055     _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE;
00056     lit_pool_push_back(0); //set the first element as a spacing element
00057 
00058     _mem_limit = 1024*1024*512; //that's 0.5 G
00059 }
00060 
00061 
00062 void CDatabase::compact_lit_pool(void)
00063 {
00064     CHECK(cout << "Begin Compaction " << endl;);
00065     int new_index = 1;
00066     for (int i=1; i< lit_pool_size(); ++i){ //begin with 1 because 0 position is always 0
00067   if (lit_pool(i).val()<=0 && lit_pool(i-1).val()<=0)
00068       continue;
00069   else {
00070       lit_pool(new_index) = lit_pool(i);
00071       ++new_index;
00072   }
00073     }
00074     _lit_pool_finish = lit_pool_begin() + new_index;
00075     //update all the pointers of the clauses;
00076     //1. clean up the pt pointers from variables
00077     for (unsigned i=1; i<variables().size(); ++i) {
00078   variable(i).ht_ptr(0).clear();
00079   variable(i).ht_ptr(1).clear();
00080     }
00081     //2. reinsert the ht_pointers
00082     for (int i=1; i< lit_pool_size(); ++i) {
00083   if (lit_pool(i).val() > 0 && lit_pool(i).is_ht()) {
00084       int var_idx = lit_pool(i).var_index();
00085       int sign = lit_pool(i).var_sign();
00086       variable(var_idx).ht_ptr(sign).push_back(& lit_pool(i));
00087   }
00088     }
00089     //3. update the clauses' first literal pointer
00090     for (int i=1; i< lit_pool_size(); ++i) {
00091   if (lit_pool(i).val() <= 0) {
00092       int cls_idx = -lit_pool(i).val();
00093       clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits();
00094   }
00095     }
00096     CHECK(output_lit_pool_state(); 
00097     cout << endl << endl;);
00098 }
00099 
00100 bool CDatabase::enlarge_lit_pool(void) //will return true if successful, otherwise false.
00101 {
00102     CHECK (output_lit_pool_state());
00103     if (lit_pool_size() - num_clauses() > num_literals() * 2) {
00104   //memory fragmented. ratio of efficiency < 0.5
00105   //minus num_clauses() is because of spacing for 
00106   //each clause in lit_pool
00107   compact_lit_pool();
00108   return true;
00109     }
00110     CHECK(cout << "Begin Enlarge Lit Pool" << endl;);
00111 
00112     //otherwise we have to enlarge it.
00113     //first, check if memory is running out
00114     int current_mem = estimate_mem_usage();
00115     float grow_ratio;
00116     if (current_mem < _mem_limit /2 ) {
00117   grow_ratio = 2;
00118     }
00119     else if (current_mem < _mem_limit * 0.8) {
00120   grow_ratio = 1.2;
00121     }
00122     else {
00123   _stats.mem_used_up = true;
00124   if (lit_pool_size() - num_clauses() > num_literals() * 1.1) {
00125       compact_lit_pool();
00126       return true;
00127   }
00128   else 
00129       return false;
00130     }
00131     //second, make room for new lit pool.
00132     CLitPoolElement * old_start = _lit_pool_start;
00133     CLitPoolElement * old_finish = _lit_pool_finish;
00134     int old_size = _lit_pool_end_storage - _lit_pool_start;
00135     int new_size = (int)(old_size * grow_ratio);
00136     _lit_pool_start = new CLitPoolElement[new_size];
00137     _lit_pool_finish = _lit_pool_start;
00138     _lit_pool_end_storage = _lit_pool_start + new_size;
00139     //copy the old content into new place
00140     for (CLitPoolElement * ptr = old_start; ptr != old_finish; ++ptr) {
00141   *_lit_pool_finish = *ptr;
00142   _lit_pool_finish ++;
00143     }
00144     //update all the pointers
00145     long displacement = _lit_pool_start - old_start;
00146     for (unsigned i=0; i< clauses().size(); ++i)
00147   if (clause(i).in_use()) 
00148       clause(i).first_lit() += displacement; 
00149 
00150     for (unsigned i=0; i< variables().size(); ++i) {
00151   CVariable & v = variable(i);
00152   for (int j=0; j< 2 ; ++j) {
00153       vector<CLitPoolElement *> & ht_ptr = v.ht_ptr(j);
00154       for (unsigned k=0; k< ht_ptr.size(); ++k) {
00155     ht_ptr[k] += displacement; 
00156       }
00157   }
00158     }
00159     //free old space
00160     delete [] old_start;
00161     CHECK(output_lit_pool_state());
00162     CHECK(cout << endl << endl);
00163     return true;
00164 }
00165 
00166 
00167 void CDatabase::output_lit_pool_state (void) 
00168 {
00169     cout << "Lit_Pool Used " << lit_pool_size() << " Free " << lit_pool_free_space()
00170    << " Total " << lit_pool_size() + lit_pool_free_space()
00171    << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals(); 
00172     cout << " Efficiency " << (float)((float)num_literals()) / (float)((lit_pool_size() - num_clauses())) << endl;
00173 }
00174 
00175 
00176 void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os) {
00177     os << "Clause : " << cl_idx;
00178     CClause & cl = clause(cl_idx);
00179     if (!cl.in_use()) 
00180   os << "\t\t\t======removed=====";
00181     char * value;
00182     int i, sz;
00183     sz = cl.num_lits(); 
00184     if (cl.num_lits() < 0) {
00185   os << ">> " ;
00186   sz = -sz;
00187     }
00188     for (i=0; i<sz; ++i) {
00189   if (literal_value(cl.literals()[i])==0) value = "0";
00190   else if (literal_value(cl.literals()[i])==1) value = "1";
00191   else value = "X";
00192   os << cl.literals()[i] << "(" << value << "@" << variable(cl.literal(i).var_index()).dlevel()<< ")  ";
00193     }
00194     os << endl;
00195 }
00196 
00197 void CDatabase::dump(ostream & os) {
00198     os << "Dump Database: " << endl;
00199     for(unsigned i=0; i<_clauses.size(); ++i) 
00200   detail_dump_cl(i);
00201 //      os << "Cl: " << i << " " << clause(i) << endl;
00202     for(unsigned i=1; i<_variables.size(); ++i)
00203   os << "VID: " << i << "\t" << variable(i);
00204 }
00205 
00206 
00207 
00208 
00209 
00210 
00211 
00212 
00213 
00214 
00215 
00216 
00217 
00218 
00219 
00220 
00221 
00222 
00223 
00224 

Generated on Tue Jul 3 14:33:42 2007 for CVC3 by  doxygen 1.5.1