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 __DISTILLERWITHBIN_H__
24 #define __DISTILLERWITHBIN_H__
25 
26 #include <vector>
27 #include "clause.h"
28 #include "constants.h"
29 #include "solvertypes.h"
30 #include "cloffset.h"
31 #include "watcharray.h"
32 
33 namespace CMSat {
34 
35 using std::vector;
36 
37 class Solver;
38 class Clause;
39 
40 class DistillerLongWithImpl {
41     public:
42         DistillerLongWithImpl(Solver* solver);
43         bool distill_long_with_implicit(bool alsoStrengthen);
44 
45         struct Stats
46         {
clearStats47             void clear()
48             {
49                 Stats tmp;
50                 *this = tmp;
51             }
52 
53             Stats& operator+=(const Stats& other);
54             void print_short(const Solver* solver) const;
55             void print() const;
56 
57             struct WatchBased
58             {
59                 double cpu_time = 0.0;
60                 uint64_t numLitsRem = 0;
61                 uint64_t numClSubsumed = 0;
62                 uint64_t triedCls = 0;
63                 uint64_t shrinked = 0;
64                 uint64_t totalCls = 0;
65                 uint64_t totalLits = 0;
66                 uint64_t ranOutOfTime = 0;
67                 uint64_t numCalled = 0;
68 
clearStats::WatchBased69                 void clear()
70                 {
71                     WatchBased tmp;
72                     *this = tmp;
73                 }
74 
75                 void print_short(const string type, const Solver* solver) const;
76                 void print() const;
77 
78                 WatchBased& operator+=(const WatchBased& other)
79                 {
80                     cpu_time += other.cpu_time;
81                     numLitsRem += other.numLitsRem;
82                     numClSubsumed += other.numClSubsumed;
83                     triedCls += other.triedCls;
84                     shrinked += other.shrinked;
85                     totalCls += other.totalCls;
86                     totalLits += other.totalLits;
87                     ranOutOfTime += other.ranOutOfTime;
88                     numCalled += other.numCalled;
89 
90                     return  *this;
91                 }
92             };
93 
94             WatchBased irredWatchBased;
95             WatchBased redWatchBased;
96         };
97 
98         const Stats& get_stats() const;
99         double mem_used() const;
100 
101     private:
102 
103         bool remove_or_shrink_clause(Clause& cl, ClOffset& offset);
104         void strsub_with_watch(
105             bool alsoStrengthen
106             , Clause& cl
107         );
108         void dump_stats_for_shorten_all_cl_with_watch(
109             bool red
110             , bool alsoStrengthen
111             , double myTime
112             , double orig_time_available
113         );
114 
115         struct WatchBasedData
116         {
117             size_t remLitBin = 0;
118             size_t subBin = 0;
119             void clear();
120             size_t get_cl_subsumed() const;
121             size_t get_lits_rem() const;
122             void print() const;
123         };
124         WatchBasedData watch_based_data;
125         bool isSubsumed;
126         size_t thisremLitBin;
127         void str_and_sub_using_watch(
128             Clause& cl
129             , const Lit lit
130             , const bool alsoStrengthen
131         );
132         void strengthen_clause_with_watch(
133             const Lit lit
134             , const Watched* wit
135         );
136         bool subsume_clause_with_watch(
137            const Lit lit
138             , Watched* wit
139             , const Clause& cl
140         );
141         Stats::WatchBased tmpStats;
142         //bool needToFinish;
143         bool sub_str_cl_with_watch(
144             ClOffset& offset
145             , bool red
146             , const bool alsoStrengthen
147         );
148         void randomise_order_of_clauses(vector<ClOffset>& clauses);
149         uint64_t calc_time_available(
150             const bool alsoStrengthen
151             , const bool red
152         ) const;
153 
154         bool shorten_all_cl_with_watch(
155             vector<ClOffset>& clauses
156             , bool red
157             , bool alsoStrengthen
158         );
159         int64_t timeAvailable;
160 
161         //Working set
162         Solver* solver;
163         vector<Lit> lits;
164         vector<Lit> lits2;
165         vector<uint16_t>& seen;
166         vector<uint8_t>& seen2;
167 
168         //Global status
169         Stats runStats;
170         Stats globalStats;
171         size_t numCalls = 0;
172 
173 };
174 
get_stats()175 inline const DistillerLongWithImpl::Stats& DistillerLongWithImpl::get_stats() const
176 {
177     return globalStats;
178 }
179 
180 } //end namespace
181 
182 #endif //__DISTILLERWITHBIN_H__
183