1 /******************************************
2 Copyright (c) 2016, Mate Soos
3 
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 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
12 all copies or substantial portions of the Software.
13 
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22 
23 #ifndef __TOUCHLIST_H__
24 #define __TOUCHLIST_H__
25 
26 #include <vector>
27 #include "solvertypes.h"
28 
29 namespace CMSat {
30 
31 class TouchList
32 {
33 public:
touch(const Lit lit)34     void touch(const Lit lit)
35     {
36         touch(lit.var());
37     }
38 
39     template<typename T, typename... Targs>
touch(T value,Targs...Fargs)40     void touch(T value, Targs... Fargs) // recursive variadic function
41     {
42         touch(value);
43         touch(Fargs...);
44     }
45 
touch(const vector<Lit> & lits)46     void touch(const vector<Lit>& lits)
47     {
48         for(const Lit lit: lits)
49             touch(lit.var());
50     }
51 
touch(const uint32_t var)52     void touch(const uint32_t var)
53     {
54         if (touchedBitset.size() <= var)
55             touchedBitset.resize(var+1, 0);
56 
57         if (touchedBitset[var] == 0) {
58             touched.push_back(var);
59             touchedBitset[var] = 1;
60         }
61     }
62 
getTouchedList()63     const vector<uint32_t>& getTouchedList() const
64     {
65         return touched;
66     }
67 
clear()68     void clear()
69     {
70         //Clear touchedBitset
71         for(vector<uint32_t>::const_iterator
72             it = touched.begin(), end = touched.end()
73             ; it != end
74             ; ++it
75         ) {
76             touchedBitset[*it] = 0;
77         }
78 
79         //Clear touched
80         touched.clear();
81     }
82 
mem_used()83     size_t mem_used() const
84     {
85         uint64_t mem = 0;
86         mem += touched.capacity()*sizeof(uint32_t);
87         mem += touchedBitset.capacity()*sizeof(char);
88 
89         return mem;
90     }
91 
shrink_to_fit()92     void shrink_to_fit()
93     {
94         touched.clear();
95         touched.shrink_to_fit();
96         touchedBitset.clear();
97         touchedBitset.shrink_to_fit();
98     }
99 
100 private:
101     vector<uint32_t> touched;
102     vector<char> touchedBitset;
103 };
104 
105 
106 class TouchListLit
107 {
108 public:
touch(const Lit lit)109     void touch(const Lit lit)
110     {
111         touch(lit.toInt());
112     }
113 
114     template<typename T, typename... Targs>
touch(T value,Targs...Fargs)115     void touch(T value, Targs... Fargs) // recursive variadic function
116     {
117         touch(value);
118         touch(Fargs...);
119     }
120 
touch(const vector<Lit> & lits)121     void touch(const vector<Lit>& lits)
122     {
123         for(const Lit lit: lits)
124             touch(lit);
125     }
126 
touch(const uint32_t var)127     void touch(const uint32_t var)
128     {
129         if (touchedBitset.size() <= var)
130             touchedBitset.resize(var+1, 0);
131 
132         if (touchedBitset[var] == 0) {
133             touched.push_back(var);
134             touchedBitset[var] = 1;
135         }
136     }
137 
getTouchedList()138     const vector<uint32_t>& getTouchedList() const
139     {
140         return touched;
141     }
142 
clear()143     void clear()
144     {
145         //Clear touchedBitset
146         for(vector<uint32_t>::const_iterator
147             it = touched.begin(), end = touched.end()
148             ; it != end
149             ; ++it
150         ) {
151             touchedBitset[*it] = 0;
152         }
153 
154         //Clear touched
155         touched.clear();
156     }
157 
mem_used()158     size_t mem_used() const
159     {
160         uint64_t mem = 0;
161         mem += touched.capacity()*sizeof(uint32_t);
162         mem += touchedBitset.capacity()*sizeof(char);
163 
164         return mem;
165     }
166 
shrink_to_fit()167     void shrink_to_fit()
168     {
169         touched.clear();
170         touched.shrink_to_fit();
171         touchedBitset.clear();
172         touchedBitset.shrink_to_fit();
173     }
174 
175 private:
176     vector<uint32_t> touched;
177     vector<char> touchedBitset;
178 };
179 
180 
181 } //end namespace
182 
183 #endif //__TOUCHLIST_H__
184