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 SIMPLIFIER_H
24 #define SIMPLIFIER_H
25
26
27 #include <map>
28 #include <vector>
29 #include <list>
30 #include <set>
31 #include <queue>
32 #include <map>
33 #include <iomanip>
34 #include <fstream>
35
36 #include "clause.h"
37 #include "solvertypes.h"
38 #include "heap.h"
39 #include "touchlist.h"
40 #include "varupdatehelper.h"
41 #include "watched.h"
42 #include "watcharray.h"
43 #include "simplefile.h"
44
45 namespace CMSat {
46
47 using std::vector;
48 using std::map;
49 using std::set;
50 using std::pair;
51 using std::priority_queue;
52
53 class ClauseCleaner;
54 class SolutionExtender;
55 class Solver;
56 class TopLevelGaussAbst;
57 class SubsumeStrengthen;
58 class BVA;
59
60 struct BlockedClauses {
BlockedClausesBlockedClauses61 BlockedClauses()
62 {}
63
BlockedClausesBlockedClauses64 explicit BlockedClauses(size_t _start, size_t _end) :
65 start(_start)
66 , end(_end)
67 , toRemove(false)
68 {}
69
save_to_fileBlockedClauses70 void save_to_file(SimpleOutFile& f) const
71 {
72 f.put_uint32_t(toRemove);
73 f.put_uint64_t(start);
74 f.put_uint64_t(end);
75 }
76
load_from_fileBlockedClauses77 void load_from_file(SimpleInFile& f)
78 {
79 toRemove = f.get_uint32_t();
80 start = f.get_uint64_t();
81 end = f.get_uint64_t();
82 }
83
atBlockedClauses84 const Lit& at(const uint64_t at, const vector<Lit>& blkcls) const
85 {
86 return blkcls[start+at];
87 }
88
atBlockedClauses89 Lit& at(const uint64_t at, vector<Lit>& blkcls)
90 {
91 return blkcls[start+at];
92 }
93
sizeBlockedClauses94 uint64_t size() const {
95 return end-start;
96 }
97
98 uint64_t start;
99 uint64_t end;
100 bool toRemove = false;
101 };
102
103 struct BVEStats
104 {
105 uint64_t numCalls = 0;
106 double timeUsed = 0.0;
107
108 int64_t numVarsElimed = 0;
109 uint64_t varElimTimeOut = 0;
110 uint64_t clauses_elimed_long = 0;
111 uint64_t clauses_elimed_bin = 0;
112 uint64_t clauses_elimed_sumsize = 0;
113 uint64_t longRedClRemThroughElim = 0;
114 uint64_t binRedClRemThroughElim = 0;
115 uint64_t numRedBinVarRemAdded = 0;
116 uint64_t testedToElimVars = 0;
117 uint64_t triedToElimVars = 0;
118 uint64_t newClauses = 0;
119 uint64_t subsumedByVE = 0;
120
121 BVEStats& operator+=(const BVEStats& other);
122
printBVEStats123 void print() const
124 {
125 //About elimination
126 cout
127 << "c [occ-bve]"
128 << " elimed: " << numVarsElimed
129 << endl;
130
131 cout
132 << "c [occ-bve]"
133 << " cl-new: " << newClauses
134 << " tried: " << triedToElimVars
135 << " tested: " << testedToElimVars
136 << endl;
137
138 cout
139 << "c [occ-bve]"
140 << " subs: " << subsumedByVE
141 << " red-bin rem: " << binRedClRemThroughElim
142 << " red-long rem: " << longRedClRemThroughElim
143 << endl;
144 }
145
printBVEStats146 void print()
147 {
148 print_stats_line("c timeouted"
149 , stats_line_percent(varElimTimeOut, numCalls)
150 , "% called"
151 );
152 print_stats_line("c v-elimed"
153 , numVarsElimed
154 , "% vars"
155 );
156
157 /*cout << "c"
158 << " v-elimed: " << numVarsElimed
159 << " / " << origNumMaxElimVars
160 << " / " << origNumFreeVars
161 << endl;*/
162
163 print_stats_line("c cl-new"
164 , newClauses
165 );
166
167 print_stats_line("c tried to elim"
168 , triedToElimVars
169 );
170
171 print_stats_line("c elim-bin-lt-cl"
172 , binRedClRemThroughElim);
173
174 print_stats_line("c elim-long-lt-cl"
175 , longRedClRemThroughElim);
176
177 print_stats_line("c lt-bin added due to v-elim"
178 , numRedBinVarRemAdded);
179
180 print_stats_line("c cl-elim-bin"
181 , clauses_elimed_bin);
182
183 print_stats_line("c cl-elim-long"
184 , clauses_elimed_long);
185
186 print_stats_line("c cl-elim-avg-s",
187 ((double)clauses_elimed_sumsize
188 /(double)(clauses_elimed_bin + clauses_elimed_long))
189 );
190
191 print_stats_line("c v-elim-sub"
192 , subsumedByVE
193 );
194 }
clearBVEStats195 void clear() {
196 BVEStats tmp;
197 *this = tmp;
198 }
199 };
200
201 /**
202 @brief Handles subsumption, self-subsuming resolution, variable elimination, and related algorithms
203 */
204 class OccSimplifier
205 {
206 public:
207
208 //Construct-destruct
209 explicit OccSimplifier(Solver* solver);
210 ~OccSimplifier();
211
212 //Called from main
213 bool simplify(const bool _startup, const std::string schedule);
214 void new_var(const uint32_t orig_outer);
215 void new_vars(const size_t n);
216 void save_on_var_memory();
217 bool uneliminate(const uint32_t var);
218 size_t mem_used() const;
219 size_t mem_used_xor() const;
220 size_t mem_used_bva() const;
221 void print_gatefinder_stats() const;
222 uint32_t dump_blocked_clauses(std::ostream* outfile) const;
223
224 //UnElimination
225 void print_blocked_clauses_reverse() const;
226 void extend_model(SolutionExtender* extender);
get_num_elimed_vars()227 uint32_t get_num_elimed_vars() const
228 {
229 return bvestats_global.numVarsElimed;
230 }
231
232 struct Stats
233 {
234 void print(const size_t nVars, OccSimplifier* occs) const;
235 void print_extra_times() const;
236 Stats& operator+=(const Stats& other);
237 void clear();
238 double total_time(OccSimplifier* occs) const;
239
240 uint64_t numCalls = 0;
241 uint64_t ternary_added_tri = 0;
242 uint64_t ternary_added_bin = 0;
243
244 //Time stats
245 double linkInTime = 0;
246 double varElimTime = 0;
247 double xorTime = 0;
248 double triresolveTime = 0;
249 double finalCleanupTime = 0;
250
251 //General stat
252 uint64_t zeroDepthAssings = 0;
253 };
254
255 BVEStats bvestats;
256 BVEStats bvestats_global;
257
258 const Stats& get_stats() const;
259 const SubsumeStrengthen* get_sub_str() const;
260 void check_elimed_vars_are_unassigned() const;
261 bool getAnythingHasBeenBlocked() const;
262
263 /// Used ONLY for XOR, changes occur setup
264 void sort_occurs_and_set_abst();
265 void save_state(SimpleOutFile& f);
266 void load_state(SimpleInFile& f);
267 vector<ClOffset> added_long_cl;
268 TouchListLit added_cl_to_var;
269 vector<uint32_t> n_occurs;
270 TouchListLit removed_cl_with_var;
271 vector<std::pair<Lit, Lit> > added_bin_cl;
272 vector<ClOffset> clauses;
273 void check_elimed_vars_are_unassignedAndStats() const;
274 void unlink_clause(ClOffset cc
275 , bool drat = true
276 , bool allow_empty_watch = false
277 , bool only_set_is_removed = false
278 );
279 void free_clauses_to_free();
280
281 //Setup and teardown. Should be private, but testing needs it to be public
282 bool setup();
283 void finishUp(size_t origTrailSize);
284
285 //Ternary resolution. Should be private but testing needs it to be public
286 bool ternary_res();
287
288 private:
289 friend class SubsumeStrengthen;
290 SubsumeStrengthen* sub_str;
291 friend class BVA;
292 BVA* bva;
293 bool startup = false;
294 bool backward_sub_str();
295 bool execute_simplifier_strategy(const string& strategy);
296
297 //Ternary resolution
298 bool perform_ternary(Clause* cl, ClOffset offs);
299 void check_ternary_cl(Clause* cl, ClOffset offs, watch_subarray ws);
300 struct Tri {
301 Lit lits[3];
302 uint32_t size = 0;
303
TriTri304 Tri () :
305 size(0)
306 {}
307
TriTri308 Tri(const Tri & other)
309 {
310 memcpy(lits, other.lits, sizeof(Lit)*3);
311 size = other.size;
312 }
313 };
314 vector<Tri> cl_to_add_ternary;
315
316 //debug
317 bool subsetReverse(const Clause& B) const;
318
319 //Persistent data
320 Solver* solver; ///<The solver this simplifier is connected to
321 vector<uint16_t>& seen;
322 vector<uint8_t>& seen2;
323 vector<Lit>& toClear;
324 vector<bool> sampling_vars_occsimp;
325
326 //Temporaries
327 vector<Lit> dummy; ///<Used by merge()
328
329 //Time Limits
330 uint64_t clause_lits_added;
331 int64_t strengthening_time_limit; ///<Max. number self-subsuming resolution tries to do this run
332 int64_t subsumption_time_limit; ///<Max. number backward-subsumption tries to do this run
333 int64_t norm_varelim_time_limit;
334 int64_t empty_varelim_time_limit;
335 int64_t varelim_num_limit;
336 int64_t varelim_sub_str_limit;
337 int64_t ternary_res_time_limit;
338 int64_t ternary_res_cls_limit;
339 int64_t* limit_to_decrease;
340
341 //Memory limits
342 int64_t varelim_linkin_limit_bytes;
343
344 //Start-up
345 bool fill_occur();
346 bool fill_occur_and_print_stats();
347 struct LinkInData
348 {
LinkInDataLinkInData349 LinkInData()
350 {}
351
LinkInDataLinkInData352 LinkInData(uint64_t _cl_linked, uint64_t _cl_not_linked) :
353 cl_linked(_cl_linked)
354 , cl_not_linked(_cl_not_linked)
355 {}
356
combineLinkInData357 LinkInData& combine(const LinkInData& other)
358 {
359 cl_linked += other.cl_linked;
360 cl_not_linked += other.cl_not_linked;
361 return *this;
362 }
363
364 uint64_t cl_linked = 0;
365 uint64_t cl_not_linked = 0;
366 };
367 LinkInData link_in_data_irred;
368 LinkInData link_in_data_red;
369 uint64_t calc_mem_usage_of_occur(const vector<ClOffset>& toAdd) const;
370 void print_mem_usage_of_occur(uint64_t memUsage) const;
371 void print_linkin_data(const LinkInData link_in_data) const;
372 OccSimplifier::LinkInData link_in_clauses(
373 const vector<ClOffset>& toAdd
374 , bool alsoOccur
375 , uint32_t max_size
376 , int64_t link_in_lit_limit
377 );
378 void set_limits();
379
380 //Finish-up
381 void remove_by_drat_recently_blocked_clauses(size_t origBlockedSize);
382 void add_back_to_solver();
383 bool check_varelim_when_adding_back_cl(const Clause* cl) const;
384 void remove_all_longs_from_watches();
385 bool complete_clean_clause(Clause& ps);
386
387 //Clause update
388 lbool clean_clause(ClOffset c);
389 void linkInClause(Clause& cl);
390 bool handleUpdatedClause(ClOffset c);
391 uint32_t sum_irred_cls_longs() const;
392 uint32_t sum_irred_cls_longs_lits() const;
393
394 struct watch_sort_smallest_first {
operatorwatch_sort_smallest_first395 bool operator()(const Watched& first, const Watched& second)
396 {
397 //Anything but clause!
398 if (first.isClause())
399 return false;
400 if (second.isClause())
401 return true;
402
403 //Both are bin
404 return false;
405 }
406 };
407
408 /////////////////////
409 //Variable elimination
410 uint32_t grow = 0; /// maximum grow rate for clauses
411 vector<uint64_t> varElimComplexity;
412 ///Order variables according to their complexity of elimination
413 struct VarOrderLt {
414 const vector<uint64_t>& varElimComplexity;
operatorVarOrderLt415 bool operator () (const uint64_t x, const uint64_t y) const
416 {
417 return varElimComplexity[x] < varElimComplexity[y];
418 }
419
VarOrderLtVarOrderLt420 explicit VarOrderLt(
421 const vector<uint64_t>& _varElimComplexity
422 ) :
423 varElimComplexity(_varElimComplexity)
424 {}
425 };
426 void order_vars_for_elim();
427 Heap<VarOrderLt> velim_order;
428 void rem_cls_from_watch_due_to_varelim(watch_subarray todo, const Lit lit);
429 vector<Lit> tmp_rem_lits;
430 vec<Watched> tmp_rem_cls_copy;
431 void add_clause_to_blck(const vector<Lit>& lits);
432 void set_var_as_eliminated(const uint32_t var, const Lit lit);
433 bool can_eliminate_var(const uint32_t var) const;
434 bool clear_vars_from_cls_that_have_been_set(size_t& last_trail);
435 bool deal_with_added_cl_to_var_lit(const Lit lit);
436 bool simulate_frw_sub_str_with_added_cl_to_var();
437
438
439 TouchList elim_calc_need_update;
440 vector<ClOffset> cl_to_free_later;
441 bool maybe_eliminate(const uint32_t x);
442 bool deal_with_added_long_and_bin(const bool main);
443 bool prop_and_clean_long_and_impl_clauses();
444 vector<Lit> tmp_bin_cl;
445 void create_dummy_blocked_clause(const Lit lit);
446 int test_elim_and_fill_resolvents(uint32_t var);
447 void mark_gate_in_poss_negs(Lit elim_lit, watch_subarray_const poss, watch_subarray_const negs);
448 void find_gate(Lit elim_lit, watch_subarray_const a, watch_subarray_const b);
449 void print_var_eliminate_stat(Lit lit) const;
450 bool add_varelim_resolvent(vector<Lit>& finalLits, const ClauseStats& stats, bool is_xor);
451 void update_varelim_complexity_heap();
452 void print_var_elim_complexity_stats(const uint32_t var) const;
453
454 struct ResolventData {
ResolventDataResolventData455 ResolventData()
456 {}
457
ResolventDataResolventData458 ResolventData(const ClauseStats& cls, const bool _is_xor) :
459 stats(cls),
460 is_xor(_is_xor)
461 {}
462
463 ClauseStats stats;
464 bool is_xor;
465 };
466
467 struct Resolvents {
468 uint32_t at = 0;
469 vector<vector<Lit>> resolvents_lits;
470 vector<ResolventData> resolvents_stats;
clearResolvents471 void clear() {
472 at = 0;
473 }
add_resolventResolvents474 void add_resolvent(const vector<Lit>& res, const ClauseStats& stats, bool is_xor) {
475 if (resolvents_lits.size() < at+1) {
476 resolvents_lits.resize(at+1);
477 resolvents_stats.resize(at+1);
478 }
479
480 resolvents_lits[at] = res;
481 resolvents_stats[at] = ResolventData(stats, is_xor);
482 at++;
483 }
back_litsResolvents484 vector<Lit>& back_lits() {
485 assert(at > 0);
486 return resolvents_lits[at-1];
487 }
back_statsResolvents488 const ClauseStats& back_stats() const {
489 assert(at > 0);
490 return resolvents_stats[at-1].stats;
491 }
back_xorResolvents492 bool back_xor() const {
493 assert(at > 0);
494 return resolvents_stats[at-1].is_xor;
495 }
popResolvents496 void pop() {
497 at--;
498 }
emptyResolvents499 bool empty() const {
500 return at == 0;
501 }
sizeResolvents502 uint32_t size() const {
503 return at;
504 }
505 };
506 Resolvents resolvents;
507 Clause* gate_varelim_clause;
508 uint32_t calc_data_for_heuristic(const Lit lit);
509 uint64_t time_spent_on_calc_otf_update;
510 uint64_t num_otf_update_until_now;
511
512 //for n_occur checking only
513 uint32_t calc_occ_data(const Lit lit);
514 void check_n_occur();
515
516 //For empty resolvents
517 enum class ResolvCount{count, set, unset};
518 bool check_empty_resolvent(const Lit lit);
519 int check_empty_resolvent_action(
520 const Lit lit
521 , ResolvCount action
522 , int otherSize
523 );
524
525 uint64_t heuristicCalcVarElimScore(const uint32_t var);
526 bool resolve_clauses(
527 const Watched ps
528 , const Watched qs
529 , const Lit noPosLit
530 );
531 void add_pos_lits_to_dummy_and_seen(
532 const Watched ps
533 , const Lit posLit
534 );
535 bool add_neg_lits_to_dummy_and_seen(
536 const Watched qs
537 , const Lit posLit
538 );
539 bool eliminate_vars();
540 void eliminate_empty_resolvent_vars();
541
542 /////////////////////
543 //Helpers
544 friend class TopLevelGaussAbst;
545 //friend class GateFinder;
546 TopLevelGaussAbst *topLevelGauss;
547 //GateFinder *gateFinder;
548
549 /////////////////////
550 //Blocked clause elimination
551 bool anythingHasBeenBlocked;
552 vector<Lit> blkcls;
553 vector<BlockedClauses> blockedClauses; ///<maps var(outer!!) to postion in blockedClauses
554 vector<uint32_t> blk_var_to_cls;
555 bool blockedMapBuilt;
556 void buildBlockedMap();
557 void cleanBlockedClauses();
558 bool can_remove_blocked_clauses = false;
559
560 //validity checking
561 void sanityCheckElimedVars();
562 void printOccur(const Lit lit) const;
563
564 ///Stats from this run
565 Stats runStats;
566
567 ///Stats globally
568 Stats globalStats;
569 };
570
get_stats()571 inline const OccSimplifier::Stats& OccSimplifier::get_stats() const
572 {
573 return globalStats;
574 }
575
getAnythingHasBeenBlocked()576 inline bool OccSimplifier::getAnythingHasBeenBlocked() const
577 {
578 return anythingHasBeenBlocked;
579 }
580
581 /*inline std::ostream& operator<<(std::ostream& os, const BlockedClauses& bl)
582 {
583 os << bl.lits << " to remove: " << bl.toRemove;
584
585 return os;
586 }*/
587
subsetReverse(const Clause & B)588 inline bool OccSimplifier::subsetReverse(const Clause& B) const
589 {
590 for (uint32_t i = 0; i != B.size(); i++) {
591 if (!seen[B[i].toInt()])
592 return false;
593 }
594 return true;
595 }
596
get_sub_str()597 inline const SubsumeStrengthen* OccSimplifier::get_sub_str() const
598 {
599 return sub_str;
600 }
601
602 } //end namespace
603
604 #endif //SIMPLIFIER_H
605