1 /*
2 Based on SatELite -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 Copyright (c) 2016, Mate Soos
4 
5 Permission is hereby granted, free of charge, to any person obtaining a copy
6 of this software and associated documentation files (the "Software"), to deal
7 in the Software without restriction, including without limitation the rights
8 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9 copies of the Software, and to permit persons to whom the Software is
10 furnished to do so, subject to the following conditions:
11 
12 The above copyright notice and this permission notice shall be included in
13 all 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,
17 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
21 THE SOFTWARE.
22 ***********************************************/
23 #ifndef CSET_H
24 #define CSET_H
25 
26 #include <limits>
27 #include "constants.h"
28 
29 #include "clause.h"
30 
31 namespace CMSat {
32 using std::vector;
33 
34 /**
35 @brief Used to quicky add, remove and iterate through a clause set
36 
37 Used in OccSimplifier to put into a set all clauses that need to be treated
38 */
39 class CSet {
40     vector<uint32_t>       where;  ///<Map clause ID to position in 'which'.
41     vector<ClOffset>   which;  ///< List of clauses (for fast iteration). May contain 'Clause_NULL'.
42     vector<uint32_t>       free;   ///<List of positions holding 'Clause_NULL'.
43 
44     public:
45         //ClauseSimp& operator [] (uint32_t index) { return which[index]; }
reserve(uint32_t size)46         void reserve(uint32_t size) {
47             where.reserve(size);
48             which.reserve(size);
49         }
50         //uint32_t size(void) const { return which.size(); }
51         ///@brief Number of elements in the set
nElems(void)52         uint32_t nElems(void) const { return which.size() - free.size(); }
53 
54         /**
55         @brief Add a clause to the set
56         */
add(const ClOffset offs)57         bool add(const ClOffset offs) {
58             //Don't check for special value
59             assert(offs != std::numeric_limits< uint32_t >::max());
60 
61             if (where.size() < offs+1)
62                 where.resize(offs+1, std::numeric_limits<uint32_t>::max());
63 
64             if (where[offs] != std::numeric_limits<uint32_t>::max()) {
65                 return false;
66             }
67             if (free.size() > 0){
68                 where[offs] = free.back();
69                 which[free.back()] = offs;
70                 free.pop_back();
71             }else{
72                 where[offs] = which.size();
73                 which.push_back(offs);
74             }
75             return true;
76         }
77 
alreadyIn(const ClOffset offs)78         bool alreadyIn(const ClOffset offs) const
79         {
80             //Don't check for special value
81             assert(offs != std::numeric_limits< uint32_t >::max());
82 
83             if (where.size() < offs+1)
84                 return false;
85 
86             return where[offs] != std::numeric_limits<uint32_t>::max();
87         }
88 
89         /**
90         @brief Fully clear the set
91         */
clear(void)92         void clear(void) {
93             where.clear();
94             which.clear();
95             free.clear();
96         }
97 
98         /**
99         @brief A normal iterator to iterate through the set
100 
101         No other way exists of iterating correctly.
102         */
103         class iterator
104         {
105             public:
iterator(vector<ClOffset>::iterator _it)106                 explicit iterator(vector<ClOffset>::iterator _it) :
107                 it(_it)
108                 {}
109 
110                 void operator++()
111                 {
112                     it++;
113                 }
114 
115                 bool operator!=(const iterator& iter) const
116                 {
117                     return (it != iter.it);
118                 }
119 
120                 ClOffset& operator*() {
121                     return *it;
122                 }
123 
124                 vector<ClOffset>::iterator& operator->() {
125                     return it;
126                 }
127             private:
128                 vector<ClOffset>::iterator it;
129         };
130 
131         /**
132         @brief A constant iterator to iterate through the set
133 
134         No other way exists of iterating correctly.
135         */
136         class const_iterator
137         {
138             public:
const_iterator(vector<ClOffset>::const_iterator _it)139                 explicit const_iterator(vector<ClOffset>::const_iterator _it) :
140                 it(_it)
141                 {}
142 
143                 void operator++()
144                 {
145                     it++;
146                 }
147 
148                 bool operator!=(const const_iterator& iter) const
149                 {
150                     return (it != iter.it);
151                 }
152 
153                 const ClOffset& operator*() {
154                     return *it;
155                 }
156 
157                 vector<ClOffset>::const_iterator& operator->() {
158                     return it;
159                 }
160             private:
161                 vector<ClOffset>::const_iterator it;
162         };
163 
164         ///@brief Get starting iterator
begin()165         iterator begin()
166         {
167             return iterator(which.begin());
168         }
169 
170         ///@brief Get ending iterator
end()171         iterator end()
172         {
173             return iterator(which.begin() + which.size());
174         }
175 
176         ///@brief Get starting iterator (constant version)
begin()177         const_iterator begin() const
178         {
179             return const_iterator(which.begin());
180         }
181 
182         ///@brief Get ending iterator (constant version)
end()183         const_iterator end() const
184         {
185             return const_iterator(which.begin() + which.size());
186         }
187 };
188 
189 } //end namespace
190 
191 #endif //CSET_H
192