zchaff64/zchaff_dbase.h

   1 // *********************************************************************
   2 // Copyright 2000-2004, Princeton University.  All rights reserved.
   3 // By using this software the USER indicates that he or she has read,
   4 // understood and will comply with the following:
   5 //
   6 // --- Princeton University hereby grants USER nonexclusive permission
   7 // to use, copy and/or modify this software for internal, noncommercial,
   8 // research purposes only. Any distribution, including commercial sale
   9 // or license, of this software, copies of the software, its associated
  10 // documentation and/or modifications of either is strictly prohibited
  11 // without the prior consent of Princeton University.  Title to copyright
  12 // to this software and its associated documentation shall at all times
  13 // remain with Princeton University.  Appropriate copyright notice shall
  14 // be placed on all software copies, and a complete copy of this notice
  15 // shall be included in all copies of the associated documentation.
  16 // No right is  granted to use in advertising, publicity or otherwise
  17 // any trademark,  service mark, or the name of Princeton University.
  18 //
  19 //
  20 // --- This software and any associated documentation is provided "as is"
  21 //
  22 // PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
  23 // OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
  24 // PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
  25 // ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
  26 // TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
  27 //
  28 // Princeton University shall not be liable under any circumstances for
  29 // any direct, indirect, special, incidental, or consequential damages
  30 // with respect to any claim by USER or any third party on account of
  31 // or arising from the use, or inability to use, this software or its
  32 // associated documentation, even if Princeton University has been advised
  33 // of the possibility of those damages.
  34 // *********************************************************************/
  35 #ifndef __ZCHAFF_DATABASE__
  36 #define __ZCHAFF_DATABASE__
  37
  38 #include "zchaff_base.h"
  39
  40 #define STARTUP_LIT_POOL_SIZE 0x8000
  41
  42 // **Struct********************************************************************
  43 //
  44 // Synopsis    [Definition of the statistics of clause database]
  45 //
  46 //  Description []
  47 //
  48 //  SeeAlso     [CDatabase]
  49 //
  50 // ****************************************************************************
  51
  52 struct CDatabaseStats {
  53   bool             mem_used_up;
  54   unsigned         init_num_clauses;
  55   unsigned         init_num_literals;
  56   unsigned         num_added_clauses;
  57   long64           num_added_literals;
  58   unsigned         num_deleted_clauses;
  59   unsigned         num_del_orig_cls;
  60   long64           num_deleted_literals;
  61   unsigned         num_compact;
  62   unsigned         num_enlarge;
  63 };
  64
  65 // **Struct********************************************************************
  66 //
  67 //  Synopsis    [Definition of the parameters of clause database]
  68 //
  69 //  Description []
  70 //
  71 //  SeeAlso     [CDatabase]
  72 //
  73 // ****************************************************************************
  74
  75 struct CDatabaseParams {
  76   int         mem_limit;
  77 };
  78
  79 // **Class*********************************************************************
  80 //
  81 //  Synopsis    [Definition of clause database ]
  82 //
  83 //  Description [Clause Database is the place where the information of the
  84 //               SAT problem are stored. it is a parent class of CSolver ]
  85 //
  86 //  SeeAlso     [CSolver]
  87 //
  88 // ****************************************************************************
  89
  90 class CDatabase {
  91   protected:
  92     CDatabaseStats      _stats;
  93
  94     CDatabaseParams     _params;
  95
  96     unsigned            _allocated_gid;    // the gids that have already been
  97                                            // allocated
  98
  99     // for efficiency, the memeory management of lit pool is done by the solver
 100     CLitPoolElement * _lit_pool_start;     // the begin of the lit vector
 101     CLitPoolElement * _lit_pool_finish;    // the tail of the used lit vector
 102     CLitPoolElement * _lit_pool_end_storage;  // the storage end of lit vector
 103
 104
 105     vector<CVariable>   _variables;     // note: first element is not used
 106
 107     vector<CClause>     _clauses;
 108
 109     set<ClauseIdx>      _unused_clause_idx;
 110
 111     ClauseIdx           top_unsat_cls;
 112
 113   protected:
 114     // constructors & destructors
 115     CDatabase() ;
 116
 117     ~CDatabase();
 118
 119     void init_stats(void) {
 120       _stats.mem_used_up              = false;
 121       _stats.init_num_clauses         = num_clauses();
 122       _stats.init_num_literals        = num_literals();
 123       _stats.num_deleted_clauses      = 0;
 124       _stats.num_del_orig_cls         = 0;
 125       _stats.num_deleted_literals     = 0;
 126       _stats.num_enlarge              = 0;
 127       _stats.num_compact              = 0;
 128     }
 129
 130     // lit pool naming convention follows STL Vector
 131     CLitPoolElement * lit_pool_begin(void);
 132
 133     CLitPoolElement * lit_pool_end(void);
 134
 135     void lit_pool_incr_size(int size);
 136
 137     void lit_pool_push_back(int value);
 138
 139     int lit_pool_size(void);
 140
 141     int lit_pool_free_space(void);
 142
 143     double lit_pool_utilization(void);
 144
 145     CLitPoolElement & lit_pool(int i);
 146
 147     // functions on lit_pool
 148     void output_lit_pool_stats(void);
 149
 150     // when allocated memeory runs out, do a reallocation
 151     bool enlarge_lit_pool(void);
 152
 153     void compact_lit_pool(void);        // garbage collection
 154
 155     unsigned literal_value(CLitPoolElement l) {
 156     // note: it will return 0 or 1 or other, here "other" may not equal UNKNOWN
 157       return (variable(l.var_index()).value() ^ l.var_sign());
 158     }
 159
 160     unsigned svar_value(int svar) {
 161     // note: it will return 0 or 1 or other, here "other" may not equal UNKNOWN
 162       return (variable(svar >> 1).value() ^ (svar & 0x1));
 163     }
 164
 165     // clause properties
 166     void mark_clause_deleted(CClause & cl);
 167
 168     int find_unit_literal(ClauseIdx cl);  // if not unit clause, return 0.
 169
 170     bool is_conflicting(ClauseIdx cl);    // e.g. all literals assigned value 0
 171
 172     bool is_unit(ClauseIdx cl);
 173
 174     bool is_satisfied(ClauseIdx cl);   // e.g. at least one literal has value 1
 175
 176     // others
 177     ClauseIdx get_free_clause_idx(void);
 178
 179     ClauseIdx add_clause(int * lits, int n_lits, int gflag = 0);
 180
 181   public:
 182
 183     // member access function
 184     inline vector<CVariable>* variables(void) {
 185       return &_variables;
 186     }
 187
 188     inline CVariable & variable(int idx) {
 189       return _variables[idx];
 190     }
 191
 192     inline vector<CClause>* clauses(void) {
 193       return &_clauses;
 194     }
 195
 196     inline CClause & clause(ClauseIdx idx) {
 197       return _clauses[idx];
 198     }
 199
 200     inline CDatabaseStats & stats(void) {
 201       return _stats;
 202     }
 203
 204     inline void set_mem_limit(int n) {
 205       _params.mem_limit = n;
 206     }
 207
 208     // clause group management
 209     int alloc_gid(void);
 210
 211     void free_gid(int gid);
 212
 213     inline int get_volatile_gid(void) {
 214       return -1;
 215     }
 216
 217     inline int get_permanent_gid(void) {
 218       return 0;
 219     }
 220
 221     bool is_gid_allocated(int gid);
 222
 223     int merge_clause_group(int g1, int g2);
 224
 225     // some stats
 226     inline unsigned & init_num_clauses(void) {
 227       return _stats.init_num_clauses;
 228     }
 229
 230     inline unsigned & init_num_literals(void) {
 231       return _stats.init_num_literals;
 232     }
 233
 234     inline unsigned & num_added_clauses(void) {
 235       return _stats.num_added_clauses;
 236     }
 237
 238     inline long64  & num_added_literals(void) {
 239       return _stats.num_added_literals;
 240     }
 241
 242     inline unsigned & num_deleted_clauses(void) {
 243       return _stats.num_deleted_clauses;
 244     }
 245
 246     inline unsigned & num_del_orig_cls(void) {
 247       return _stats.num_del_orig_cls;
 248     }
 249
 250     inline long64 & num_deleted_literals(void) {
 251       return _stats.num_deleted_literals;
 252     }
 253
 254     inline unsigned num_variables(void) {
 255       return variables()->size() - 1;
 256     }
 257
 258     inline unsigned num_clauses(void) {
 259       return _clauses.size() - _unused_clause_idx.size();
 260     }
 261
 262     inline unsigned num_literals(void) {
 263       return _stats.num_added_literals - _stats.num_deleted_literals;
 264     }
 265
 266     inline unsigned num_mem_compacts(void) {
 267       return _stats.num_compact;
 268     }
 269
 270     inline unsigned num_mem_enlarges(void) { return
 271       _stats.num_enlarge;
 272     }
 273
 274     // functions
 275     unsigned estimate_mem_usage(void);
 276
 277     unsigned mem_usage(void);
 278
 279     inline void set_variable_number(int n) {
 280       variables()->resize(n + 1);
 281     }
 282
 283     inline int add_variable(void) {
 284       variables()->resize(variables()->size() + 1);
 285       return variables()->size() - 1;
 286     }
 287
 288     // dump functions
 289     void detail_dump_cl(ClauseIdx cl_idx, ostream & os = cout);
 290
 291     void dump(ostream & os = cout);
 292
 293     friend ostream & operator << (ostream & os, CDatabase & db) {
 294       db.dump(os);
 295       return os;
 296     }
 297 };
 298 #endif