1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 sat_cutset.cpp 7 8 Author: 9 10 Nikolaj Bjorner 2020-01-02 11 12 --*/ 13 14 15 #include "util/hashtable.h" 16 #include "sat/sat_cutset.h" 17 #include "sat/sat_cutset_compute_shift.h" 18 #include <memory> 19 #include <sstream> 20 21 22 namespace sat { 23 24 /** 25 \brief 26 if c is subsumed by a member in cut_set, then c is not inserted. 27 otherwise, remove members that c subsumes. 28 Note that the cut_set maintains invariant that elements don't subsume each-other. 29 30 TBD: this is a bottleneck. 31 Ideas: 32 - add Bloom filter to is_subset_of operation. 33 - pre-allocate fixed array instead of vector for cut_set to avoid overhead for memory allocation. 34 */ 35 insert(on_update_t & on_add,on_update_t & on_del,cut const & c)36 bool cut_set::insert(on_update_t& on_add, on_update_t& on_del, cut const& c) { 37 unsigned i = 0, k = m_size; 38 for (; i < k; ++i) { 39 cut const& a = (*this)[i]; 40 if (a.subset_of(c)) { 41 return false; 42 } 43 if (c.subset_of(a)) { 44 std::swap(m_cuts[i--], m_cuts[--k]); 45 } 46 } 47 // for DRAT make sure to add new element before removing old cuts 48 // the new cut may need to be justified relative to the old cut 49 push_back(on_add, c); 50 std::swap(m_cuts[i++], m_cuts[m_size-1]); 51 shrink(on_del, i); 52 return true; 53 } 54 no_duplicates() const55 bool cut_set::no_duplicates() const { 56 hashtable<cut const*, cut::hash_proc, cut::eq_proc> table; 57 for (auto const& cut : *this) { 58 VERIFY(!table.contains(&cut)); 59 table.insert(&cut); 60 } 61 return true; 62 } 63 display(std::ostream & out) const64 std::ostream& cut_set::display(std::ostream& out) const { 65 for (auto const& cut : *this) { 66 cut.display(out) << "\n"; 67 } 68 return out; 69 } 70 71 shrink(on_update_t & on_del,unsigned j)72 void cut_set::shrink(on_update_t& on_del, unsigned j) { 73 if (m_var != UINT_MAX && on_del) { 74 for (unsigned i = j; i < m_size; ++i) { 75 on_del(m_var, m_cuts[i]); 76 } 77 } 78 m_size = j; 79 } 80 push_back(on_update_t & on_add,cut const & c)81 void cut_set::push_back(on_update_t& on_add, cut const& c) { 82 SASSERT(m_max_size > 0); 83 if (!m_cuts) { 84 m_cuts = new (*m_region) cut[m_max_size]; 85 } 86 if (m_size == m_max_size) { 87 m_max_size *= 2; 88 cut* new_cuts = new (*m_region) cut[m_max_size]; 89 std::uninitialized_copy(m_cuts, m_cuts + m_size, new_cuts); 90 m_cuts = new_cuts; 91 } 92 if (m_var != UINT_MAX && on_add) on_add(m_var, c); 93 m_cuts[m_size++] = c; 94 } 95 evict(on_update_t & on_del,cut const & c)96 void cut_set::evict(on_update_t& on_del, cut const& c) { 97 for (unsigned i = 0; i < m_size; ++i) { 98 if (m_cuts[i] == c) { 99 evict(on_del, i); 100 break; 101 } 102 } 103 } 104 evict(on_update_t & on_del,unsigned idx)105 void cut_set::evict(on_update_t& on_del, unsigned idx) { 106 if (m_var != UINT_MAX && on_del) on_del(m_var, m_cuts[idx]); 107 m_cuts[idx] = m_cuts[--m_size]; 108 } 109 init(region & r,unsigned max_sz,unsigned v)110 void cut_set::init(region& r, unsigned max_sz, unsigned v) { 111 m_var = v; 112 m_size = 0; 113 SASSERT(!m_region || m_cuts); 114 VERIFY(!m_region || m_max_size > 0); 115 if (!m_region) { 116 m_max_size = 2; // max_sz; 117 m_region = &r; 118 m_cuts = nullptr; 119 } 120 } 121 122 /** 123 \brief shift table 'a' by adding elements from 'c'. 124 a.shift_table(c) 125 126 \pre 'a' is a subset of 'c'. 127 128 Let 't' be the table for 'a'. 129 130 i'th bit in t is function of indices x0*2^0 + x2*2^1 = i 131 i'th bit in t' is function of indices x0*2^0 + x1*2^1 + x2*2^2 = i 132 133 i -> assignment to coefficients in c, 134 -> assignment to coefficients in a 135 -> compute j, 136 -> t'[i] <- t[j] 137 138 This is still time consuming: 139 Ideas: 140 - pre-compute some shift operations. 141 - use strides on some common cases. 142 - what ABC does? 143 */ shift_table(cut const & c) const144 uint64_t cut::shift_table(cut const& c) const { 145 SASSERT(subset_of(c)); 146 unsigned index = 0; 147 for (unsigned i = 0, j = 0, x = (*this)[i], y = c[j]; x != UINT_MAX; ) { 148 if (x == y) { 149 index |= (1 << j); 150 x = (*this)[++i]; 151 } 152 y = c[++j]; 153 } 154 index |= (1 << c.m_size); 155 return compute_shift(table(), index); 156 } 157 operator ==(cut const & other) const158 bool cut::operator==(cut const& other) const { 159 return table() == other.table() && dom_eq(other); 160 } 161 hash() const162 unsigned cut::hash() const { 163 return get_composite_hash(*this, m_size, 164 [](cut const& c) { return (unsigned)c.table(); }, 165 [](cut const& c, unsigned i) { return c[i]; }); 166 } 167 dom_hash() const168 unsigned cut::dom_hash() const { 169 return get_composite_hash(*this, m_size, 170 [](cut const& c) { return 3; }, 171 [](cut const& c, unsigned i) { return c[i]; }); 172 } 173 dom_eq(cut const & other) const174 bool cut::dom_eq(cut const& other) const { 175 if (m_size != other.m_size) return false; 176 for (unsigned i = 0; i < m_size; ++i) { 177 if ((*this)[i] != other[i]) return false; 178 } 179 return true; 180 } 181 182 /** 183 * \brief create the masks 184 * i = 0: 101010101010101 185 * i = 1: 1100110011001100 186 * i = 2: 1111000011110000 187 * i = 3: 111111110000000011111111 188 */ 189 effect_mask(unsigned i)190 uint64_t cut::effect_mask(unsigned i) { 191 SASSERT(i <= 6); 192 uint64_t m = 0; 193 if (i == 6) { 194 m = ~((uint64_t)0); 195 } 196 else { 197 m = (1ull << (1u << i)) - 1; // i = 0: m = 1 198 unsigned w = 1u << (i + 1); // i = 0: w = 2 199 while (w < 64) { 200 m |= (m << w); // i = 0: m = 1 + 4 201 w *= 2; 202 } 203 } 204 return m; 205 } 206 207 /** 208 remove element from cut as it is deemed a don't care 209 */ remove_elem(unsigned i)210 void cut::remove_elem(unsigned i) { 211 for (unsigned j = i + 1; j < m_size; ++j) { 212 m_elems[j-1] = m_elems[j]; 213 } 214 --m_size; 215 uint64_t m = effect_mask(i); 216 uint64_t t = 0; 217 for (unsigned j = 0, offset = 0; j < 64; ++j) { 218 if (0 != (m & (1ull << j))) { 219 t |= ((m_table >> j) & 1u) << offset; 220 ++offset; 221 } 222 } 223 m_table = t; 224 m_dont_care = 0; 225 unsigned f = 0; 226 for (unsigned e : *this) { 227 f |= (1u << (e & 0x1F)); 228 } 229 m_filter = f; 230 } 231 232 /** 233 sat-sweep evaluation. Given 64 bits worth of possible values per variable, 234 find possible values for function table encoded by cut. 235 */ eval(cut_eval const & env) const236 cut_val cut::eval(cut_eval const& env) const { 237 cut_val v; 238 uint64_t t = table(); 239 uint64_t n = table(); 240 unsigned sz = size(); 241 if (sz == 1 && t == 2) { 242 return env[m_elems[0]]; 243 } 244 for (unsigned i = 0; i < 64; ++i) { 245 unsigned offset = 0; 246 for (unsigned j = 0; j < sz; ++j) { 247 offset |= (((env[m_elems[j]].m_t >> i) & 0x1) << j); 248 } 249 v.m_t |= ((t >> offset) & 0x1) << i; 250 v.m_f |= ((n >> offset) & 0x1) << i; 251 } 252 return v; 253 } 254 display(std::ostream & out) const255 std::ostream& cut::display(std::ostream& out) const { 256 out << "{"; 257 for (unsigned i = 0; i < m_size; ++i) { 258 out << (*this)[i]; 259 if (i + 1 < m_size) out << " "; 260 } 261 out << "} "; 262 display_table(out, m_size, table()); 263 return out; 264 } 265 display_table(std::ostream & out,unsigned num_input,uint64_t table)266 std::ostream& cut::display_table(std::ostream& out, unsigned num_input, uint64_t table) { 267 for (unsigned i = 0; i < (1u << num_input); ++i) { 268 if (0 != (table & (1ull << i))) out << "1"; else out << "0"; 269 } 270 return out; 271 } 272 table2string(unsigned num_input,uint64_t table)273 std::string cut::table2string(unsigned num_input, uint64_t table) { 274 std::ostringstream strm; 275 display_table(strm, num_input, table); 276 return strm.str(); 277 } 278 279 280 } 281