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 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 BVMinisat_Alg_h |
22 |
|
#define BVMinisat_Alg_h |
23 |
|
|
24 |
|
#include "base/check.h" |
25 |
|
#include "prop/bvminisat/mtl/Vec.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace BVMinisat { |
29 |
|
|
30 |
|
//================================================================================================= |
31 |
|
// Useful functions on vector-like types: |
32 |
|
|
33 |
|
//================================================================================================= |
34 |
|
// Removing and searching for elements: |
35 |
|
// |
36 |
|
|
37 |
|
template<class V, class T> |
38 |
166105 |
static inline void remove(V& ts, const T& t) |
39 |
|
{ |
40 |
166105 |
int j = 0; |
41 |
11763851 |
for (; j < ts.size() && ts[j] != t; j++); |
42 |
166105 |
Assert(j < ts.size()); |
43 |
10377641 |
for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; |
44 |
166105 |
ts.pop(); |
45 |
166105 |
} |
46 |
|
|
47 |
|
|
48 |
|
template<class V, class T> |
49 |
35448 |
static inline bool find(V& ts, const T& t) |
50 |
|
{ |
51 |
35448 |
int j = 0; |
52 |
150018 |
for (; j < ts.size() && ts[j] != t; j++); |
53 |
35448 |
return j < ts.size(); |
54 |
|
} |
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) |
73 |
|
to.clear(); |
74 |
|
for (int i = 0; i < from.size(); i++){ |
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){ copy(from, to, true); } |
82 |
|
|
83 |
|
//================================================================================================= |
84 |
|
} // namespace BVMinisat |
85 |
|
} // namespace cvc5 |
86 |
|
|
87 |
|
#endif |