Branch data     Line data    Source code

       1                 :            : /*******************************************************************************************[Alg.h]
       2                 :            : Copyright (c) 2003-2006, 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
       6                 :            : this software and associated documentation files (the "Software"), to deal in
       7                 :            : the Software without restriction, including without limitation the rights to
       8                 :            : use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
       9                 :            : the Software, and to permit persons to whom the Software is furnished to do so,
      10                 :            : subject to the following conditions:
      11                 :            : 
      12                 :            : The above copyright notice and this permission notice shall be included in all
      13                 :            : copies or substantial portions of the Software.
      14                 :            : 
      15                 :            : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
      16                 :            : IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
      17                 :            : FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
      18                 :            : COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
      19                 :            : IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
      20                 :            : CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
      21                 :            : **************************************************************************************************/
      22                 :            : 
      23                 :            : #ifndef Minisat_Alg_h
      24                 :            : #define Minisat_Alg_h
      25                 :            : 
      26                 :            : #include "base/check.h"
      27                 :            : #include "prop/minisat/mtl/Vec.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace Minisat {
      31                 :            : 
      32                 :            : //=================================================================================================
      33                 :            : // Useful functions on vector-like types:
      34                 :            : 
      35                 :            : //=================================================================================================
      36                 :            : // Removing and searching for elements:
      37                 :            : //
      38                 :            : 
      39                 :            : template <class V, class T>
      40                 :      63329 : static inline void remove(V& ts, const T& t)
      41                 :            : {
      42                 :      63329 :   int j = 0;
      43 [ +  - ][ +  + ]:     794980 :   for (; j < ts.size() && ts[j] != t; j++);
                 [ +  + ]
      44 [ -  + ][ -  + ]:      63329 :   Assert(j < ts.size());
                 [ -  - ]
      45         [ +  + ]:    1719114 :   for (; j < ts.size() - 1; j++) ts[j] = ts[j + 1];
      46                 :      63329 :   ts.pop();
      47                 :      63329 : }
      48                 :            : 
      49                 :            : template <class V, class T>
      50                 :     196583 : static inline bool find(V& ts, const T& t)
      51                 :            : {
      52                 :     196583 :   int j = 0;
      53 [ +  + ][ +  + ]:     797065 :   for (; j < ts.size() && ts[j] != t; j++);
                 [ +  + ]
      54                 :     196583 :   return j < ts.size();
      55                 :            : }
      56                 :            : 
      57                 :            : //=================================================================================================
      58                 :            : // Copying vectors with support for nested vector types:
      59                 :            : //
      60                 :            : 
      61                 :            : // Base case:
      62                 :            : template <class T>
      63                 :            : static inline void copy(const T& from, T& to)
      64                 :            : {
      65                 :            :   to = from;
      66                 :            : }
      67                 :            : 
      68                 :            : // Recursive case:
      69                 :            : template <class T>
      70                 :            : static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
      71                 :            : {
      72                 :            :   if (!append) to.clear();
      73                 :            :   for (int i = 0; i < from.size(); i++)
      74                 :            :   {
      75                 :            :     to.push();
      76                 :            :     copy(from[i], to.last());
      77                 :            :   }
      78                 :            : }
      79                 :            : 
      80                 :            : template <class T>
      81                 :            : static inline void append(const vec<T>& from, vec<T>& to)
      82                 :            : {
      83                 :            :   copy(from, to, true);
      84                 :            : }
      85                 :            : 
      86                 :            : //=================================================================================================
      87                 :            : }  // namespace Minisat
      88                 :            : }  // namespace cvc5::internal
      89                 :            : 
      90                 :            : #endif