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