Doxygen Generated Documentation of Ben-Jose Trainable SAT Solver Library
bit_row.h
1 
2 
3 /*************************************************************
4 
5 This file is part of ben-jose.
6 
7 ben-jose is free software: you can redistribute it and/or modify
8 it under the terms of the version 3 of the GNU General Public
9 License as published by the Free Software Foundation.
10 
11 ben-jose is distributed in the hope that it will be useful,
12 but WITHOUT ANY WARRANTY; without even the implied warranty of
13 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
14 GNU General Public License for more details.
15 
16 You should have received a copy of the GNU General Public License
17 along with ben-jose. If not, see <http://www.gnu.org/licenses/>.
18 
19 ------------------------------------------------------------
20 
21 Copyright (C) 2007-2012, 2014-2016. QUIROGA BELTRAN, Jose Luis.
22 Id (cedula): 79523732 de Bogota - Colombia.
23 See https://github.com/joseluisquiroga/ben-jose
24 
25 ben-jose is free software thanks to The Glory of Our Lord
26  Yashua Melej Hamashiaj.
27 Our Resurrected and Living, both in Body and Spirit,
28  Prince of Peace.
29 
30 ------------------------------------------------------------
31 
32 bit_row.h
33 
34 binary rows of bits.
35 
36 --------------------------------------------------------------*/
37 
38 
39 #ifndef BIT_ROW_H
40 #define BIT_ROW_H
41 
42 #include "top_exception.h"
43 #include "bj_mem.h"
44 #include "bj_stream.h"
45 
46 typedef long bit_rw_idx;
47 
48 #ifndef INVALID_IDX
49 #define INVALID_IDX -1
50 #endif
51 
52 #ifndef FILL_FULL_CAP
53 #define FILL_FULL_CAP -100
54 #endif
55 
56 #ifndef START_CAP
57 #define START_CAP 16 // avoid mem problems (due to mem alloc, re-alloc failures)
58 #endif
59 
60 #ifndef k_num_bits_byte
61 #define k_num_bits_byte 8
62 #endif
63 
64 #define BITS_CK(prm) DBG_CK(prm)
65 
66 //======================================================================
67 // bitarray
68 
69 // where 'a' is the byte stream pointer, and b is the bit number.
70 
71 #define div8(b) ((b)>>3)
72 #define mod8(b) ((b)&7)
73 
74 #define get_bit(a, b) ((((t_1byte*)a)[div8(b)] >> mod8(b)) & 1)
75 #define set_bit(a, b) (((t_1byte*)a)[div8(b)] |= (1 << mod8(b)))
76 #define reset_bit(a, b) (((t_1byte*)a)[div8(b)] &= ~(1 << mod8(b)))
77 #define toggle_bit(a, b) (((t_1byte*)a)[div8(b)] ^= (1 << mod8(b)))
78 
79 #define to_bytes(num_bits) (div8(num_bits) + (mod8(num_bits) > 0))
80 #define to_bits(num_bytes) (num_bytes * k_num_bits_byte)
81 
82 //======================================================================
83 // bit_rw_exception
84 
85 typedef enum {
86  brx_bad_eq_op,
87  brx_bad_creat
88 } br_ex_cod_t;
89 
90 class bit_rw_exception : public top_exception {
91 public:
92  bit_rw_exception(long the_id = 0) : top_exception(the_id)
93  {}
94 };
95 
96 //======================================================================
97 // bit_row
98 
99 class bit_row;
100 
101 class bit_ref {
102 public:
103  bit_rw_idx idx;
104  bit_row* brow;
105 
106  bit_ref(){
107  idx = 0;
108  brow = NULL_PT;
109  }
110 
111  bit_ref& operator = (bool val);
112  operator bool();
113 };
114 
115 bit_rw_idx
116 rot_lft_idx(bit_rw_idx pos, bit_rw_idx row_sz, long num_rot);
117 
118 bit_rw_idx
119 rot_rgt_idx(bit_rw_idx pos, bit_rw_idx row_sz, long num_rot);
120 
121 bj_ostream& operator << (bj_ostream& os, bit_row& rr);
122 bit_row& operator << (bit_row& rr, const bool elem);
123 bit_row& operator >> (bit_row& rr, bool& elem);
124 bit_row& operator << (bit_row& rr1, bit_row& rr2);
125 
126 class bit_row {
127 private:
128  bit_row& operator = (bit_row& other){
129  throw bit_rw_exception(brx_bad_eq_op);
130  }
131 
132  bit_row(bit_row& other){
133  throw bit_rw_exception(brx_bad_creat);
134  }
135 
136 
137 public:
138  bit_rw_idx cap; // num bytes of cap
139  bit_rw_idx sz; // num bits in arr
140  t_1byte* data;
141 
142  bit_row(){
143  sz = 0;
144  cap = 0;
145  data = NULL_PT;
146  }
147 
148  ~bit_row(){
149  clear(true, true);
150  }
151 
152  void init_with_copy_of(t_1byte* dat_bytes, long dat_num_bytes){
153  if(size() > 0){
154  clear(true, true);
155  }
156  bit_rw_idx nw_sz = to_bits(dat_num_bytes);
157  set_cap(nw_sz);
158  bj_memcpy(data, dat_bytes, cap);
159  sz = nw_sz;
160  }
161 
162  const t_1byte* get_c_array(){
163  return (t_1byte*)data;
164  }
165 
166  long get_c_array_sz(){
167  return (long)(to_bytes(sz));
168  }
169 
170  bit_rw_idx get_cap(){
171  return to_bits(cap);
172  }
173 
174  bit_rw_idx get_bytes_cap(){
175  return cap;
176  }
177 
178  bool is_valid_idx(bit_rw_idx idx){
179  return ((idx >= 0) && (idx < size()));
180  }
181 
182  bit_rw_idx last_idx(){
183  return (size() - 1);
184  }
185 
186  virtual
187  void grow(bit_rw_idx bits_cap){
188  bit_rw_idx min_cap = to_bytes(bits_cap);
189  if(min_cap <= cap){ return; }
190  bit_rw_idx nxt_cap = cap;
191 
192  if(nxt_cap == 0){
193  nxt_cap = to_bytes(START_CAP);
194  }
195 
196  do{
197  nxt_cap = nxt_cap * 2;
198  } while(nxt_cap < min_cap);
199 
200  BITS_CK(nxt_cap > 1);
201  set_cap(to_bits(nxt_cap));
202  }
203 
204  virtual
205  void set_cap(bit_rw_idx bits_cap){
206  bit_rw_idx min_cap = to_bytes(bits_cap);
207  if(min_cap <= cap){ return; }
208  bit_rw_idx old_cap = cap;
209  BITS_CK(old_cap >= 0);
210  cap = min_cap;
211  t_1byte* n_dat = tpl_realloc(data, old_cap, cap);
212  data = n_dat;
213  }
214 
215  virtual
216  void set_size(bit_rw_idx bits_sz){
217  set_cap(bits_sz);
218  sz = bits_sz;
219  }
220 
221  virtual
222  void clear(bool reset_them = false, bool dealloc = false, bit_rw_idx from = 0){
223  if(data != NULL_PT){
224  if(from != 0){
225  dealloc = false;
226  }
227  if(dealloc){
228  reset_them = false;
229  }
230  if(reset_them){
231  for(bit_rw_idx ii = from; ii < sz; ii++){
232  reset_bit(data, ii);
233  }
234  }
235  sz = from;
236  if(dealloc){
237  tpl_free(data, cap);
238  data = NULL_PT;
239  cap = 0;
240  }
241  }
242  }
243 
244  bit_rw_idx size() const {
245  return sz;
246  }
247 
248  bit_rw_idx num_bytes() const {
249  return to_bytes(sz);
250  }
251 
252  bool is_full() {
253  return (sz == get_cap());
254  }
255 
256  bool is_empty(){
257  return (sz == 0);
258  }
259 
260  bool pos(bit_rw_idx idx){
261  return get_bit(data, idx);
262  }
263 
264  void set(bit_rw_idx idx){
265  set_bit(data, idx);
266  }
267 
268  void reset(bit_rw_idx idx){
269  reset_bit(data, idx);
270  }
271 
272  void set_val(bit_rw_idx idx, bool val = false){
273  if(val){
274  set_bit(data, idx);
275  } else {
276  reset_bit(data, idx);
277  }
278  }
279 
280  virtual
281  void push(const bool elem){
282  if(is_full()){
283  grow(sz + 2);
284  }
285  set_val(sz, elem);
286  sz++;
287  }
288 
289  virtual
290  void inc_sz(){
291  if(is_full()){
292  grow(sz + 2);
293  }
294  reset_bit(data, sz);
295  sz++;
296  }
297 
298  virtual
299  void dec_sz(){
300  sz--;
301  reset_bit(data, sz);
302  }
303 
304  virtual
305  bool pop(){
306  BITS_CK(sz > 0);
307  sz--;
308  bool tmp1 = pos(sz);
309  reset_bit(data, sz);
310  return tmp1;
311  }
312 
313  bool last(){
314  return pos(sz - 1);
315  }
316 
317  void swap(bit_rw_idx idx1, bit_rw_idx idx2){
318  bool tmp1 = pos(idx1);
319  set_val(idx1, pos(idx2));
320  set_val(idx2, tmp1);
321  }
322 
323  virtual
324  bool swap_pop(bit_rw_idx idx){
325  bool tmp1 = pos(idx);
326  sz--;
327  set_val(idx, pos(sz));
328  reset_bit(data, sz);
329  return tmp1;
330  }
331 
332  virtual
333  void swapop(bit_rw_idx idx){
334  sz--;
335  set_val(idx, pos(sz));
336  reset_bit(data, sz);
337  }
338 
339  void fill(const bool elem, bit_rw_idx num_fill = INVALID_IDX,
340  bool only_new = false)
341  {
342  if(num_fill == INVALID_IDX){
343  num_fill = sz;
344  }
345  if(num_fill == FILL_FULL_CAP){
346  num_fill = get_cap();
347  }
348  set_cap(num_fill);
349  bit_rw_idx ii = 0;
350  if(! only_new){
351  for(ii = 0; ((ii < sz) && (ii < num_fill)); ii++){
352  set_val(ii, elem);
353  }
354  }
355  for(ii = sz; ii < num_fill; ii++){
356  push(elem);
357  }
358  }
359 
360  void fill_new(bit_rw_idx num_fill = INVALID_IDX){
361  clear(true);
362  if(num_fill == INVALID_IDX){
363  num_fill = sz;
364  }
365  if(num_fill == FILL_FULL_CAP){
366  num_fill = get_cap();
367  }
368  set_cap(num_fill);
369  for(bit_rw_idx ii = 0; ii < num_fill; ii++){
370  inc_sz();
371  }
372  }
373 
374  bit_ref operator [] (bit_rw_idx idx) {
375  BITS_CK(idx >= 0);
376  BITS_CK(idx < sz);
377  bit_ref the_ref;
378  the_ref.brow = this;
379  the_ref.idx = idx;
380  return the_ref;
381  }
382 
383  void copy_to(bit_row& r_cpy, bit_rw_idx first_ii = 0, bit_rw_idx last_ii = -1){
384  r_cpy.clear(true, false);
385  if((last_ii < 0) || (last_ii > sz)){
386  last_ii = sz;
387  }
388  if((first_ii < 0) || (first_ii > last_ii)){
389  first_ii = 0;
390  }
391  r_cpy.set_cap(last_ii - first_ii);
392  for (bit_rw_idx ii = first_ii; ii < last_ii; ii++){
393  bool ob = pos(ii);
394  r_cpy.push(ob);
395  }
396  }
397 
398  void append_to(bit_row& orig){
399  orig.set_cap(orig.sz + sz);
400  for (bit_rw_idx ii = 0; ii < sz; ii++){
401  orig.push(pos(ii));
402  }
403  }
404 
405  // rotation funcs
406 
407  void rotate_left(bit_row& dest, long num_bits){
408  dest.set_size(size());
409  BITS_CK(size() == dest.size());
410  long d_sz = dest.size();
411  for(bit_rw_idx aa = 0; aa < size(); aa++){
412  bit_rw_idx d_idx = rot_lft_idx(aa, d_sz, num_bits);
413  dest[d_idx] = pos(aa);
414  }
415  }
416 
417  void rotate_right(bit_row& dest, long num_bits){
418  dest.set_size(size());
419  BITS_CK(size() == dest.size());
420  long d_sz = dest.size();
421  for(bit_rw_idx aa = 0; aa < size(); aa++){
422  bit_rw_idx d_idx = rot_rgt_idx(aa, d_sz, num_bits);
423  dest[d_idx] = pos(aa);
424  }
425  }
426 
427  // io funcs
428 
429  bj_ostream& print_bit_row(
430  bj_ostream& os,
431  bool with_lims = true,
432 
433  char* sep = as_pt_char(" "),
434  bit_rw_idx low = INVALID_IDX,
435  bit_rw_idx hi = INVALID_IDX,
436  bit_rw_idx grp_sz = -1,
437  char* grp_sep = as_pt_char("\n")
438  );
439 
440  bool equal_to(bit_row& rw2, bit_rw_idx first_ii = 0, bit_rw_idx last_ii = -1){
441  if((last_ii < 0) || (last_ii > sz)){
442  last_ii = sz;
443  }
444  if((first_ii < 0) || (first_ii > last_ii)){
445  first_ii = 0;
446  }
447  //for(bit_rw_idx ii = 0; ii < sz; ii++){
448  for (bit_rw_idx ii = first_ii; ii < last_ii; ii++){
449  if(pos(ii) != rw2.pos(ii)){
450  return false;
451  }
452  }
453  return true;
454  }
455 
456  void swap_with(bit_row& dest){
457  bit_rw_idx tmp_cap = cap;
458  bit_rw_idx tmp_sz = sz;
459  t_1byte* tmp_data = data;
460 
461  cap = dest.cap;
462  sz = dest.sz;
463  data = dest.data;
464 
465  dest.cap = tmp_cap;
466  dest.sz = tmp_sz;
467  dest.data = tmp_data;
468  }
469 
470  void mem_copy_to(bit_row& r_cpy){
471  r_cpy.set_cap(sz);
472  bj_memcpy(r_cpy.data, data, r_cpy.cap);
473  r_cpy.sz = sz;
474  }
475 };
476 
477 inline
478 bj_ostream&
479 bit_row::print_bit_row(
480  bj_ostream& os,
481  bool with_lims,
482 
483  char* sep,
484  bit_rw_idx low,
485  bit_rw_idx hi,
486  bit_rw_idx grp_sz,
487  char* grp_sep
488  )
489 {
490  bit_rw_idx num_elem = 1;
491  if(with_lims){ os << "["; }
492  for(bit_rw_idx ii = 0; ii < sz; ii++){
493  if(ii == low){ os << ">"; }
494  os << pos(ii);
495  if(ii == hi){ os << "<"; }
496  os << sep;
497  if((grp_sz > 1) && ((num_elem % grp_sz) == 0)){
498  os << grp_sep;
499  }
500  num_elem++;
501  }
502  if(with_lims){ os << "] "; }
503  os.flush();
504  return os;
505 }
506 
507 inline
508 bit_ref& bit_ref::operator = (bool val){
509  BITS_CK(brow != NULL_PT);
510  brow->set_val(idx, val);
511  return (*this);
512 }
513 
514 inline
515 bit_ref::operator bool(){
516  BITS_CK(brow != NULL_PT);
517  return brow->pos(idx);
518 }
519 
520 inline
521 bit_rw_idx
522 rot_lft_idx(bit_rw_idx pos, bit_rw_idx row_sz, long num_rot){
523  //long r_rot = row_sz - (num_rot % row_sz);
524  long r_rot = (num_rot % row_sz);
525  bit_rw_idx n_idx = (pos - r_rot);
526  if(n_idx < 0){
527  n_idx = row_sz + n_idx;
528  }
529  BITS_CK(n_idx >= 0);
530  BITS_CK(n_idx < row_sz);
531  return n_idx;
532 }
533 
534 inline
535 bit_rw_idx
536 rot_rgt_idx(bit_rw_idx pos, bit_rw_idx row_sz, long num_rot){
537  //long r_rot = row_sz - (num_rot % row_sz);
538  long r_rot = (num_rot % row_sz);
539  bit_rw_idx n_idx = (pos + r_rot);
540  if(n_idx >= row_sz){
541  n_idx = n_idx % row_sz;
542  }
543  BITS_CK(n_idx >= 0);
544  BITS_CK(n_idx < row_sz);
545  return n_idx;
546 }
547 
548 inline
549 bj_ostream& operator << (bj_ostream& os, bit_row& rr){
550  rr.print_bit_row(os, true, as_pt_char(" "));
551  return os;
552 }
553 
554 inline
555 bit_row& operator << (bit_row& rr, const bool elem){
556  rr.push(elem);
557  return rr;
558 }
559 
560 inline
561 bit_row& operator >> (bit_row& rr, bool& elem){
562  elem = rr.pop();
563  return rr;
564 }
565 
566 inline
567 bit_row& operator << (bit_row& rr1, bit_row& rr2){
568  rr2.append_to(rr1);
569  return rr1;
570 }
571 
572 //======================================================================
573 // s_bit_row
574 
575 // careful: cannot free the given data while using the
576 // s_bit_row object because it is a pointer to the given data.
577 
578 class s_bit_row : public bit_row {
579 private:
580  virtual
581  void grow(bit_rw_idx bits_cap){ MARK_USED(bits_cap); }
582  virtual
583  void set_cap(bit_rw_idx bits_cap){ MARK_USED(bits_cap); }
584  virtual
585  void set_size(bit_rw_idx bits_sz){ MARK_USED(bits_sz); }
586  virtual
587  void push(const bool elem){ MARK_USED(elem); }
588  virtual
589  void inc_sz(){}
590  virtual
591  void dec_sz(){}
592  virtual
593  bool pop(){ return false; }
594  virtual
595  bool swap_pop(bit_rw_idx idx){ MARK_USED(idx); return false; }
596  virtual
597  void swapop(bit_rw_idx idx){ MARK_USED(idx); }
598 
599 public:
600  virtual
601  void clear(bool reset_them = false, bool dealloc = false, bit_rw_idx from = 0){
602  MARK_USED(reset_them);
603  MARK_USED(dealloc);
604  MARK_USED(from);
605  sz = 0;
606  cap = 0;
607  data = NULL_PT;
608  }
609 
610  s_bit_row(t_1byte* dat = NULL_PT, long dat_num_bytes = 0){
611  init_data(dat, dat_num_bytes);
612  }
613 
614  s_bit_row(double* dat){
615  init_data((t_1byte*)dat, sizeof(double));
616  }
617 
618  s_bit_row(long* dat){
619  init_data((t_1byte*)dat, sizeof(long));
620  }
621 
622  s_bit_row(char* dat){
623  init_data((t_1byte*)dat, sizeof(char));
624  }
625 
626  s_bit_row(s_bit_row& bt_r, long from_byte,
627  long num_bytes)
628  {
629  long max_byte = bt_r.get_bytes_cap();
630  if(from_byte > max_byte){
631  from_byte = max_byte;
632  }
633  if((from_byte + num_bytes) > max_byte){
634  num_bytes = (max_byte - from_byte);
635  }
636  t_1byte* dat = bt_r.data + from_byte;
637  init_data(dat, num_bytes);
638  }
639 
640  ~s_bit_row(){
641  clear();
642  }
643 
644  void init_data(t_1byte* dat, long dat_num_bytes){
645  sz = to_bits(dat_num_bytes);
646  cap = dat_num_bytes;
647  if(cap > 0){
648  data = dat;
649  } else {
650  data = NULL_PT;
651  }
652  }
653 
654 };
655 
656 #endif // BIT_ROW_H
657 
658