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 __BVA_H__
24 #define __BVA_H__
25
26 #include "heap.h"
27 #include "watched.h"
28 #include "clause.h"
29 #include "touchlist.h"
30 #include <vector>
31 using std::vector;
32
33 namespace CMSat {
34
35 class Solver;
36 class OccSimplifier;
37
38 class BVA
39 {
40 public:
41 BVA(Solver* _solver, OccSimplifier* _simplifier);
42 bool bounded_var_addition();
43 size_t mem_used() const;
44
45 struct Stats
46 {
47 double time_used = 0;
48
49 Stats& operator +=(const Stats& other) {
50 time_used += other.time_used;
51 return *this;
52 }
53
resetStats54 void reset()
55 {
56 *this = Stats();
57 }
58 };
59
60 const Stats& get_stats() const;
61
62 private:
63 Solver* solver;
64 OccSimplifier* simplifier;
65 vector<uint16_t>& seen;
66 vector<uint8_t>& seen2;
67
68 Stats runStats;
69 Stats globalStats;
70 bool bva_verbosity = 0;
71 size_t bva_worked;
72 size_t bva_simp_size;
73 struct lit_pair{
74 lit_pair(Lit a, Lit b = lit_Undef)
75 {
76 if (b == lit_Undef) {
77 lit1 = a;
78 } else {
79 assert(false && "lits are supposed to be sorted in occur lists");
80 assert(a != b);
81 if (a > b) {
82 std::swap(a, b);
83 }
84 lit1 = a;
85 lit2 = b;
86 }
87 }
88
89 bool operator==(const lit_pair& other) const
90 {
91 return lit1 == other.lit1 && lit2 == other.lit2;
92 }
93
hashlit_pair94 unsigned hash(const uint32_t N) const
95 {
96 unsigned long h;
97 h = lit1.toInt();
98
99 if (lit2 == lit_Undef)
100 return h % N;
101
102 h = h*31 + lit2.toInt();
103 return h % N;
104 }
105
106 bool operator!=(const lit_pair& other) const
107 {
108 return !(*this == other);
109 }
110
111 Lit lit1;
112 Lit lit2;
113 };
114 struct PotentialClause {
PotentialClausePotentialClause115 PotentialClause(const lit_pair _lits, const OccurClause cl) :
116 lits(_lits)
117 , occur_cl(cl)
118 {}
119
120 bool operator<(const PotentialClause& other) const
121 {
122 if (lits == other.lits)
123 return false;
124
125 if (lits.lit1 != other.lits.lit1)
126 return lits.lit1 < other.lits.lit1;
127
128 return lits.lit2 < other.lits.lit2;
129 }
130
131 lit_pair lits;
132 OccurClause occur_cl;
133 string to_string(const Solver* solver) const;
134 };
135 struct m_cls_lits_and_red
136 {
137 //Used during removal to lower overhead
m_cls_lits_and_redm_cls_lits_and_red138 m_cls_lits_and_red(const vector<Lit>& _lits, bool _red) :
139 lits(_lits)
140 , red(_red)
141 {}
142 vector<Lit> lits;
143 bool red;
144 };
145 size_t calc_watch_irred_size(const Lit lit) const;
146 void calc_watch_irred_sizes();
147 lit_pair most_occurring_lit_in_potential(size_t& num_occur);
148 lit_pair lit_diff_watches(const OccurClause& a, const OccurClause& b);
149 Lit least_occurring_except(const OccurClause& c);
150 bool simplifies_system(const size_t num_occur) const;
151 int simplification_size(
152 const int m_lit_size
153 , const int m_cls_size
154 ) const;
155 void fill_potential(const Lit lit);
156 bool try_bva_on_lit(const Lit lit);
157 bool bva_simplify_system();
158 void update_touched_lits_in_bva();
159 bool add_longer_clause(const Lit lit, const OccurClause& cl);
160 void remove_duplicates_from_m_cls();
161 void remove_matching_clause(
162 const m_cls_lits_and_red& cl_lits
163 , const lit_pair lit_replace
164 );
165 Clause* find_cl_for_bva(
166 const vector<Lit>& torem
167 , const bool red
168 ) const;
169 void fill_m_cls_lits_and_red();
170 vector<Lit> bva_tmp_lits; //To reduce overhead
171 vector<m_cls_lits_and_red> m_cls_lits; //used during removal to lower overhead
172 vector<Lit> to_remove; //to reduce overhead
173 vector<PotentialClause> potential;
174 vector<lit_pair> m_lits;
175 vector<lit_pair> m_lits_this_cl;
176 vector<OccurClause> m_cls;
177 vector<size_t> watch_irred_sizes;
178 struct VarBVAOrder
179 {
VarBVAOrderVarBVAOrder180 explicit VarBVAOrder(vector<size_t>& _watch_irred_sizes) :
181 watch_irred_sizes(_watch_irred_sizes)
182 {}
183
184 bool operator()(const uint32_t lit1_uint, const uint32_t lit2_uint) const;
185 vector<size_t>& watch_irred_sizes;
186 };
187 Heap<VarBVAOrder> var_bva_order;
188 TouchList touched;
189
190 int64_t bounded_var_elim_time_limit;
191 };
192
get_stats()193 inline const BVA::Stats& BVA::get_stats() const
194 {
195 return globalStats;
196 }
197
198 }
199
200 #endif //__BVA_H__
201