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