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 _GATEFINDER_H_
24 #define _GATEFINDER_H_
25
26 #include "solvertypes.h"
27 #include "cset.h"
28 #include <set>
29 #include "watcharray.h"
30 #include <array>
31
32 namespace CMSat {
33
34 class Solver;
35 class OccSimplifier;
36 using std::set;
37
38 class OrGate {
39 public:
OrGate(const Lit & _rhs,Lit _lit1,Lit _lit2,const bool _red)40 OrGate(const Lit& _rhs, Lit _lit1, Lit _lit2, const bool _red) :
41 lit1(_lit1)
42 , lit2(_lit2)
43 , rhs(_rhs)
44 , red(_red)
45 {
46 if (lit1 > lit2)
47 std::swap(lit1, lit2);
48 }
49
50 bool operator==(const OrGate& other) const
51 {
52 return
53 rhs == other.rhs
54 && lit1 == other.lit1
55 && lit2 == other.lit2
56 ;
57 }
getLits()58 std::array<Lit, 2> getLits() const
59 {
60 return std::array<Lit, 2>{{lit1, lit2}};
61 }
62
63 //LHS
64 Lit lit1;
65 Lit lit2;
66
67 //RHS
68 Lit rhs;
69
70 //Data about gate
71 bool red;
72 };
73
74 struct GateCompareForEq
75 {
operatorGateCompareForEq76 bool operator()(const OrGate& a, const OrGate& b) const
77 {
78 if (a.lit1 != b.lit1) {
79 return (a.lit1 < b.lit1);
80 }
81
82 if (a.lit2 != b.lit2) {
83 return (a.lit2 < b.lit2);
84 }
85 return (a.rhs < b.rhs);
86 }
87 };
88
89 inline std::ostream& operator<<(std::ostream& os, const OrGate& gate)
90 {
91 os
92 << " gate "
93 << " lits: " << gate.lit1 << ", " << gate.lit2
94 << " rhs: " << gate.rhs
95 << " learnt " << gate.red
96 ;
97 return os;
98 }
99
100 class GateFinder
101 {
102 public:
103 GateFinder(OccSimplifier *simplifier, Solver *control);
104 bool doAll();
105
106 //Stats
107 struct Stats
108 {
clearStats109 void clear()
110 {
111 Stats tmp;
112 *this = tmp;
113 }
114
total_timeStats115 double total_time() const
116 {
117 return findGateTime + orBasedTime + varReplaceTime
118 + andBasedTime + erTime;
119 }
120 Stats& operator+=(const Stats& other);
121 void print(const size_t nVars) const;
122
123 //Time
124 double findGateTime = 0.0;
125 uint32_t find_gate_timeout = 0;
126 double orBasedTime = 0.0;
127 uint32_t or_based_timeout = 0;
128 double varReplaceTime = 0.0;
129 double andBasedTime = 0.0;
130 uint32_t and_based_timeout = 0;
131 double erTime = 0.0;
132
133 //OR-gate
134 uint64_t orGateUseful = 0;
135 uint64_t numLongCls = 0;
136 uint64_t numLongClsLits = 0;
137 int64_t litsRem = 0;
138
139 //Var-replace
140 uint64_t varReplaced = 0;
141
142 //And-gate
143 uint64_t andGateUseful = 0;
144 uint64_t clauseSizeRem = 0;
145
146 //ER
147 uint64_t numERVars = 0;
148
149 //Gates
150 uint64_t learntGatesSize = 0;
151 uint64_t numRed = 0;
152 uint64_t irredGatesSize = 0;
153 uint64_t numIrred = 0;
154 };
155
156 const Stats& get_stats() const;
157
158 private:
159 void print_graphviz_dot();
160
161 //Setup
162 void link_in_gate(const OrGate& gate);
163 void add_gate_if_not_already_inside(Lit rhs, Lit lit1, Lit lit2);
164 void find_or_gates_in_sweep_mode(Lit lit);
165
166 //High-level functions
167 bool remove_clauses_with_all_or_gates();
168 bool shorten_with_all_or_gates();
169
170 //Finding
171 void find_or_gates_and_update_stats();
172 void find_or_gates();
173 void findOrGate(
174 const Lit rhs
175 , const Lit lit1
176 , const Lit lit2
177 );
178
179 bool all_simplifications_with_gates();
180 vector<ClOffset> subs; //to reduce overhead of allocation
181 bool shortenWithOrGate(const OrGate& gate);
182 size_t findEqOrGates();
183
184 //And gate treatment
185 bool remove_clauses_using_and_gate(
186 const OrGate& gate
187 , const bool reallyRemove
188 , const bool only_irred
189 );
190
191 cl_abst_type calc_sorted_occ_and_set_seen2(
192 const OrGate& gate
193 , uint32_t& maxSize
194 , uint32_t& minSize
195 , const bool only_irred
196 );
197 void set_seen2_and_abstraction(
198 const Clause& cl
199 , cl_abst_type& abstraction
200 );
201 bool check_seen_and_gate_against_cl(
202 const Clause& this_cl
203 , const OrGate& gate
204 );
205
206 void treatAndGateClause(
207 const ClOffset other_cl_offset
208 , const OrGate& gate
209 , const ClOffset this_cl_offset
210 );
211 cl_abst_type calc_abst_and_set_seen(
212 const Clause& cl
213 , const OrGate& gate
214 );
215 ClOffset find_pair_for_and_gate_reduction(
216 const Watched& ws
217 , const size_t minSize
218 , const size_t maxSize
219 , const cl_abst_type abstraction
220 , const OrGate& gate
221 , const bool only_irred
222 );
223
224 ClOffset findAndGateOtherCl(
225 const vector<ClOffset>& this_sizeSortedOcc
226 , const Lit lit
227 , const cl_abst_type abst2
228 , const bool gate_is_red
229 , const bool only_irred
230 );
231 bool findAndGateOtherCl_tri(
232 watch_subarray_const ws_list
233 , const bool gate_is_red
234 , const bool only_irred
235 , Watched& ret
236 );
237 bool find_pair_for_and_gate_reduction_tri(
238 const Watched& ws
239 , const OrGate& gate
240 , const bool only_irred
241 , Watched& found_pair
242 );
243 bool remove_clauses_using_and_gate_tri(
244 const OrGate& gate
245 , const bool really_remove
246 , const bool only_irred
247 );
248 void set_seen2_tri(
249 const OrGate& gate
250 , const bool only_irred
251 );
252 bool check_seen_and_gate_against_lit(
253 const Lit lit
254 , const OrGate& gate
255 );
256
257 ///temporary for and-gate treatment. Cleared at every treatAndGate() call
258 vector<vector<ClOffset> > sizeSortedOcc;
259
260 //Indexes, gate data
261 vector<OrGate> orGates; //List of OR gates
262
263 //For temporaries
264 vector<uint32_t> seen2Set; //Bits that have been set in seen2, and later need to be cleared
265 set<ClOffset> clToUnlink;
266 struct TriToUnlink
267 {
TriToUnlinkTriToUnlink268 TriToUnlink(Lit _lit2, Lit _lit3, bool _red) :
269 lit2(_lit2)
270 , lit3(_lit3)
271 , red(_red)
272 {}
273
274 const Lit lit2;
275 const Lit lit3;
276 const bool red;
277
278 bool operator<(const TriToUnlink& other) const
279 {
280 if (lit2 != other.lit2)
281 return lit2 < other.lit2;
282 if (lit3 != other.lit3)
283 return lit3 < other.lit3;
284 return red < other.red;
285 }
286 };
287 set<TriToUnlink> tri_to_unlink;
288
289 //Graph
290 void print_graphviz_dot2(); ///<Print Graphviz DOT file describing the gates
291
292 //Stats
293 Stats runStats;
294 Stats globalStats;
295
296 //Limits
297 int64_t numMaxGateFinder;
298 int64_t numMaxShortenWithGates;
299 int64_t numMaxClRemWithGates;
300
301 //long-term stats
302 uint64_t numDotPrinted;
303
304 //Main data
305 OccSimplifier *simplifier;
306 Solver *solver;
307 vector<uint16_t>& seen;
308 vector<uint8_t>& seen2;
309 vector<Lit>& toClear;
310 };
311
get_stats()312 inline const GateFinder::Stats& GateFinder::get_stats() const
313 {
314 return globalStats;
315 }
316
317 } //end namespace
318
319 #endif //_GATEFINDER_H_
320