LCOV - code coverage report
Current view: top level - buildbot/coverage/build/src/prop/minisat/mtl - Vec.h (source / functions) Hit Total Coverage
Test: coverage.info Lines: 45 47 95.7 %
Date: 2025-02-20 12:45:24 Functions: 142 143 99.3 %
Branches: 33 50 66.0 %

           Branch data     Line data    Source code
       1                 :            : /*******************************************************************************************[Vec.h]
       2                 :            : Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
       3                 :            : Copyright (c) 2007-2010, Niklas Sorensson
       4                 :            : 
       5                 :            : Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
       6                 :            : associated documentation files (the "Software"), to deal in the Software without restriction,
       7                 :            : including without limitation the rights to use, copy, modify, merge, publish, distribute,
       8                 :            : sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
       9                 :            : furnished to do so, subject to the following conditions:
      10                 :            : 
      11                 :            : The above copyright notice and this permission notice shall be included in all copies or
      12                 :            : substantial portions of the Software.
      13                 :            : 
      14                 :            : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
      15                 :            : NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
      16                 :            : NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
      17                 :            : DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
      18                 :            : OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
      19                 :            : **************************************************************************************************/
      20                 :            : 
      21                 :            : #ifndef Minisat_Vec_h
      22                 :            : #define Minisat_Vec_h
      23                 :            : 
      24                 :            : #include <new>
      25                 :            : 
      26                 :            : #include "base/check.h"
      27                 :            : #include "prop/minisat/mtl/IntTypes.h"
      28                 :            : #include "prop/minisat/mtl/XAlloc.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : namespace Minisat {
      32                 :            : 
      33                 :            : //=================================================================================================
      34                 :            : // Automatically resizable arrays
      35                 :            : //
      36                 :            : // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
      37                 :            : 
      38                 :            : template<class T>
      39                 :            : class vec {
      40                 :            :     T*  data;
      41                 :            :     int sz;
      42                 :            :     int cap;
      43                 :            : 
      44                 :            :     // Don't allow copying (error prone):
      45                 :            :     vec<T>& operator=(vec<T>& other)
      46                 :            :     {
      47                 :            :       Assert(0);
      48                 :            :       return *this;
      49                 :            :     }
      50                 :            :     vec(vec<T>& other) { Assert(0); }
      51                 :            : 
      52                 :            :     // Helpers for calculating next capacity:
      53                 :   30843936 :     static inline int  imax   (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
      54                 :            :     //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
      55                 :            :     static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
      56                 :            : 
      57                 :            : public:
      58                 :            :     // Constructors:
      59                 :   34684554 :     vec()                       : data(NULL) , sz(0)   , cap(0)    { }
      60                 :      62356 :     explicit vec(int size)      : data(NULL) , sz(0)   , cap(0)    { growTo(size); }
      61                 :      51576 :     vec(int size, const T& pad) : data(NULL) , sz(0)   , cap(0)    { growTo(size, pad); }
      62                 :   34786501 :    ~vec()                                                          { clear(true); }
      63                 :            : 
      64                 :            :     // Pointer to first element:
      65                 :  166644662 :     operator T*       (void)           { return data; }
      66                 :            : 
      67                 :            :     // Size operations:
      68                 : 7602510193 :     int      size     (void) const     { return sz; }
      69                 :  172468936 :     void shrink(int nelems)
      70                 :            :     {
      71 [ -  + ][ -  + ]:  172468936 :       Assert(nelems <= sz);
                 [ -  - ]
      72         [ +  + ]:  690470276 :       for (int i = 0; i < nelems; i++) sz--, data[sz].~T();
      73                 :  172468936 :     }
      74                 :            :     void shrink_(int nelems)
      75                 :            :     {
      76                 :            :       Assert(nelems <= sz);
      77                 :            :       sz -= nelems;
      78                 :            :     }
      79                 :          0 :     int      capacity (void) const     { return cap; }
      80                 :            :     void     capacity (int min_cap);
      81                 :            :     void     growTo   (int size);
      82                 :            :     void     growTo   (int size, const T& pad);
      83                 :            :     void     clear    (bool dealloc = false);
      84                 :            : 
      85                 :            :     // Stack interface:
      86         [ +  + ]:    7605263 :     void     push  (void)              { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
      87         [ +  + ]:  538234638 :     void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
      88                 :  164805000 :     void push_(const T& elem)
      89                 :            :     {
      90 [ -  + ][ -  + ]:  164805000 :       Assert(sz < cap);
                 [ -  - ]
      91                 :  164805000 :       data[sz++] = elem;
      92                 :  164805000 :     }
      93                 :   47372920 :     void pop(void)
      94                 :            :     {
      95 [ -  + ][ -  + ]:   47372920 :       Assert(sz > 0);
                 [ -  - ]
      96                 :   47372920 :       sz--, data[sz].~T();
      97                 :   47372920 :     }
      98                 :            :     // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
      99                 :            :     // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
     100                 :            :     // happen given the way capacities are calculated (below). Essentially, all capacities are
     101                 :            :     // even, but INT_MAX is odd.
     102                 :            : 
     103                 :            :     const T& last  (void) const        { return data[sz-1]; }
     104                 :   51972420 :     T&       last  (void)              { return data[sz-1]; }
     105                 :            : 
     106                 :            :     // Vector interface:
     107                 : 6154492040 :     const T& operator [] (int index) const { return data[index]; }
     108                 : 4974553340 :     T&       operator [] (int index)       { return data[index]; }
     109                 :            : 
     110                 :            :     // Duplication (preferred instead):
     111         [ +  + ]:   89094100 :     void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
     112                 :      10780 :     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
     113                 :            : };
     114                 :            : 
     115                 :            : 
     116                 :            : template<class T>
     117                 :   52573293 : void vec<T>::capacity(int min_cap) {
     118         [ +  + ]:   52573293 :     if (cap >= min_cap) return;
     119                 :   30843936 :     int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
     120 [ +  - ][ -  + ]:   30843936 :     if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
         [ -  - ][ -  + ]
     121                 :          0 :         throw OutOfMemoryException();
     122                 :            :  }
     123                 :            : 
     124                 :            : 
     125                 :            : template<class T>
     126                 :   19864986 : void vec<T>::growTo(int size, const T& pad) {
     127         [ +  + ]:   19864986 :     if (sz >= size) return;
     128                 :    7677536 :     capacity(size);
     129         [ +  + ]:   15410922 :     for (int i = sz; i < size; i++) data[i] = pad;
     130                 :    7677536 :     sz = size; }
     131                 :            : 
     132                 :            : 
     133                 :            : template<class T>
     134                 :   16984477 : void vec<T>::growTo(int size) {
     135         [ +  + ]:   16984477 :     if (sz >= size) return;
     136                 :   16981477 :     capacity(size);
     137         [ +  + ]:  100952457 :     for (int i = sz; i < size; i++) new (&data[i]) T();
     138                 :   16981477 :     sz = size; }
     139                 :            : 
     140                 :            : 
     141                 :            : template<class T>
     142                 :   79420976 : void vec<T>::clear(bool dealloc) {
     143         [ +  + ]:   79420976 :     if (data != NULL){
     144         [ +  + ]:  290742345 :         for (int i = 0; i < sz; i++) data[i].~T();
     145                 :   53784693 :         sz = 0;
     146         [ +  + ]:   53784693 :         if (dealloc) free(data), data = NULL, cap = 0; } }
     147                 :            : 
     148                 :            : //=================================================================================================
     149                 :            : }
     150                 :            : }  // namespace cvc5::internal
     151                 :            : 
     152                 :            : #endif

Generated by: LCOV version 1.14