xchaff_dbase.h

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 
00039 #ifndef __DATABASE__
00040 #define __DATABASE__
00041 
00042 #include "xchaff_base.h"
00043 #include <queue>
00044 
00045 #define STARTUP_LIT_POOL_SIZE 0x1000
00046 
00047 struct pair_int_equal {
00048     bool operator () (pair<int,int> a, pair<int,int> b) {
00049   return (a.first==b.first && a.second == b.second);
00050     }
00051 };
00052 
00053 struct pair_int_hash_fun {
00054     size_t operator () (const pair<int, int> a) const {
00055   return (a.first + (a.second << 16));
00056     }
00057 };
00058 
00059 /**Struct**********************************************************************
00060 
00061   Synopsis    [Definition of the statistics of clause database]
00062 
00063   Description []
00064 
00065   SeeAlso     [CDatabase]
00066 
00067 ******************************************************************************/
00068 
00069 struct CDatabaseStats {
00070     int mem_used_up_counts;
00071     bool mem_used_up;
00072     int init_num_clauses;
00073     int init_num_literals;
00074     int num_added_clauses;
00075     int num_added_literals;
00076     int num_deleted_clauses;
00077     int num_deleted_literals;
00078 };
00079 
00080 /**Class**********************************************************************
00081 
00082   Synopsis    [Definition of clause database ]
00083 
00084   Description [Clause Database is the place where the information of the 
00085                SAT problem are stored. it is a parent class of CSolver ]
00086 
00087   SeeAlso     [CSolver]
00088 
00089 ******************************************************************************/
00090 class CDatabase
00091 {
00092 protected:
00093     CDatabaseStats _stats;
00094     //for efficiency, the memeory management of lit pool is done by the solver
00095 
00096     CLitPoolElement * _lit_pool_start;    //the begin of the lit vector
00097     CLitPoolElement * _lit_pool_finish;   //the tail of the used lit vector
00098     CLitPoolElement * _lit_pool_end_storage;    //the storage end of lit vector
00099 
00100     vector<CVariable> _variables; //note: first element is not used
00101     vector<CClause> _clauses;
00102     queue<ClauseIdx> _unused_clause_idx_queue;
00103 
00104     int _num_var_in_new_cl;
00105     int _mem_limit;
00106 public:
00107 //constructors & destructors
00108     CDatabase() ;
00109     ~CDatabase() { 
00110   delete [] _lit_pool_start; 
00111     }
00112     void init(void) {
00113         init_num_clauses() = num_clauses();
00114   init_num_literals() = num_literals();
00115     }
00116 //member access function
00117     vector<CVariable>& variables(void) { 
00118   return _variables; 
00119     }
00120     vector<CClause>& clauses(void) { 
00121   return _clauses; 
00122     }
00123     CVariable & variable(int idx) { 
00124   return _variables[idx]; 
00125     }
00126     CClause & clause(ClauseIdx idx) { 
00127   return _clauses[idx]; 
00128     }
00129     CDatabaseStats & stats(void) {
00130   return _stats;
00131     }
00132     void set_mem_limit(int n) {
00133   _mem_limit = n;
00134     }
00135 //some stats
00136     int & init_num_clauses() { return _stats.init_num_clauses; }
00137     int & init_num_literals () { return _stats.init_num_literals; }
00138     int & num_added_clauses () { return _stats.num_added_clauses; }
00139     int & num_added_literals() { return _stats.num_added_literals; }
00140     int & num_deleted_clauses() { return _stats.num_deleted_clauses; }
00141     int & num_deleted_literals() { return _stats.num_deleted_literals; }
00142 
00143 //lit pool naming convention is following STL Vector
00144     CLitPoolElement * lit_pool_begin(void) { 
00145   return _lit_pool_start; 
00146     }
00147     CLitPoolElement * lit_pool_end(void) { 
00148   return _lit_pool_finish; 
00149     }
00150     void lit_pool_push_back(int value) { 
00151   assert (_lit_pool_finish <= _lit_pool_end_storage );
00152   _lit_pool_finish->val() = value;
00153   ++ _lit_pool_finish;
00154     }
00155     int lit_pool_size(void) { 
00156   return _lit_pool_finish - _lit_pool_start; 
00157     }
00158     int lit_pool_free_space(void) { 
00159   return _lit_pool_end_storage - _lit_pool_finish; 
00160     }
00161     CLitPoolElement & lit_pool(int i) {
00162   return _lit_pool_start[i];
00163     }
00164 //functions on lit_pool
00165     void output_lit_pool_state(void);
00166 
00167     bool enlarge_lit_pool(void);
00168 
00169     void compact_lit_pool(void);
00170 
00171 //functions 
00172     int estimate_mem_usage (void) 
00173   {
00174   int lit_pool = sizeof(CLitPoolElement) * 
00175                  (lit_pool_size() + lit_pool_free_space());
00176   int mem_vars = sizeof(CVariable) * 
00177                        variables().capacity();
00178   int mem_cls = sizeof(CClause) * 
00179                       clauses().capacity();
00180   int mem_cls_queue = sizeof(int) * 
00181                             _unused_clause_idx_queue.size();
00182   int mem_ht_ptrs =0, mem_lit_clauses = 0;
00183   mem_ht_ptrs = sizeof(CLitPoolElement*) * 
00184                     (clauses().size()-_unused_clause_idx_queue.size()) * 2;
00185   return (lit_pool + mem_vars + mem_cls +
00186     mem_cls_queue + mem_ht_ptrs + mem_lit_clauses);
00187   }
00188     int mem_usage(void) {
00189   int lit_pool = (lit_pool_size() + lit_pool_free_space()) * sizeof(CLitPoolElement);
00190   int mem_vars = sizeof(CVariable) * variables().capacity();
00191   int mem_cls = sizeof(CClause) * clauses().capacity();
00192   int mem_cls_queue = sizeof(int) * _unused_clause_idx_queue.size();
00193   int mem_ht_ptrs = 0, mem_lit_clauses = 0;
00194   for (unsigned i=0; i< variables().size(); ++i) {
00195       CVariable & v = variable(i);
00196       mem_ht_ptrs += v.ht_ptr(0).capacity() + v.ht_ptr(1).capacity(); 
00197   }
00198   mem_ht_ptrs *= sizeof(CLitPoolElement*);
00199   mem_lit_clauses *= sizeof(ClauseIdx);
00200   return (lit_pool + mem_vars + mem_cls + 
00201     mem_cls_queue + mem_ht_ptrs + mem_lit_clauses);
00202     }
00203     void set_variable_number(int n) { 
00204   variables().resize(n + 1) ; 
00205     }
00206     int add_variable(void) {
00207   variables().resize( variables().size() + 1);
00208   return variables().size() - 1;
00209     }
00210     int num_variables(void) {
00211   return variables().size() - 1;
00212     }
00213 
00214     int num_clauses(void) { 
00215   return _clauses.size() - _unused_clause_idx_queue.size(); 
00216     }
00217     int num_literals(void) { 
00218   return _stats.num_added_literals - _stats.num_deleted_literals; 
00219     }
00220 
00221     void mark_clause_deleted(CClause & cl) {
00222   ++_stats.num_deleted_clauses;
00223   _stats.num_deleted_literals += cl.num_lits();
00224   cl.in_use() = false;
00225   for (int i=0; i< cl.num_lits(); ++i) {
00226       CLitPoolElement & l = cl.literal(i);
00227       --variable(l.var_index()).lits_count(l.var_sign());
00228       l.val() = 0;
00229   }
00230     }
00231     void mark_var_in_new_cl(int v_idx, int phase ) { 
00232       if (variable(v_idx).in_new_cl() == -1 && phase != -1)
00233     ++ _num_var_in_new_cl;
00234       else if (variable(v_idx).in_new_cl() != -1 && phase == -1)
00235     -- _num_var_in_new_cl;
00236       else assert (0 && "How can this happen? ");
00237       variable(v_idx).set_in_new_cl( phase ); 
00238     }
00239     int literal_value (CLitPoolElement l) { //note: it will return 0 or 1 or other , 
00240                                            //here "other" may not equal UNKNOWN
00241   return variable(l.var_index()).value() ^ l.var_sign(); 
00242     }
00243 
00244     int find_unit_literal(ClauseIdx cl);  //if not unit clause, return 0.
00245 
00246     bool is_conflict(ClauseIdx cl);     //e.g. all literals assigned value 0
00247 
00248     bool is_satisfied(ClauseIdx cl);    //e.g. at least one literal has value 1
00249 
00250     void detail_dump_cl(ClauseIdx cl_idx, ostream & os = cout);
00251 
00252     void dump(ostream & os = cout);
00253 };
00254 
00255 #endif
00256 
00257 
00258 
00259 
00260 
00261 
00262 
00263 
00264 
00265 
00266 
00267 
00268 
00269 
00270 

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