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 #include "completedetachreattacher.h"
24 #include "solver.h"
25 #include "varreplacer.h"
26 #include "clausecleaner.h"
27 #include "clauseallocator.h"
28
29 using namespace CMSat;
30
CompleteDetachReatacher(Solver * _solver)31 CompleteDetachReatacher::CompleteDetachReatacher(Solver* _solver) :
32 solver(_solver)
33 {
34 }
35
36 /**
37 @brief Completely detach all non-binary clauses
38 */
detach_nonbins_nontris()39 void CompleteDetachReatacher::detach_nonbins_nontris()
40 {
41 assert(!solver->drat->something_delayed());
42 ClausesStay stay;
43
44 for (watch_array::iterator
45 it = solver->watches.begin(), end = solver->watches.end()
46 ; it != end
47 ; ++it
48 ) {
49 stay += clearWatchNotBinNotTri(*it);
50 }
51
52 solver->litStats.redLits = 0;
53 solver->litStats.irredLits = 0;
54
55 assert(stay.redBins % 2 == 0);
56 solver->binTri.redBins = stay.redBins/2;
57
58 assert(stay.irredBins % 2 == 0);
59 solver->binTri.irredBins = stay.irredBins/2;
60 }
61
62 /**
63 @brief Helper function for detachPointerUsingClauses()
64 */
clearWatchNotBinNotTri(watch_subarray ws)65 CompleteDetachReatacher::ClausesStay CompleteDetachReatacher::clearWatchNotBinNotTri(
66 watch_subarray ws
67 ) {
68 ClausesStay stay;
69
70 Watched* i = ws.begin();
71 Watched* j = i;
72 for (Watched* end = ws.end(); i != end; i++) {
73 if (i->isBin()) {
74 if (i->red())
75 stay.redBins++;
76 else
77 stay.irredBins++;
78
79 *j++ = *i;
80 }
81 }
82 ws.shrink_(i-j);
83
84 return stay;
85 }
86
reattachLongs(bool removeStatsFirst)87 bool CompleteDetachReatacher::reattachLongs(bool removeStatsFirst)
88 {
89 if (solver->conf.verbosity >= 6) {
90 cout << "Cleaning and reattaching clauses" << endl;
91 }
92
93 cleanAndAttachClauses(solver->longIrredCls, removeStatsFirst);
94 for(auto& lredcls: solver->longRedCls) {
95 cleanAndAttachClauses(lredcls, removeStatsFirst);
96 }
97 solver->clauseCleaner->clean_implicit_clauses();
98 assert(!solver->drat->something_delayed());
99
100 if (solver->ok) {
101 solver->ok = (solver->propagate<true>().isNULL());
102 }
103
104 return solver->okay();
105 }
106
attachClauses(vector<ClOffset> & cs)107 void CompleteDetachReatacher::attachClauses(
108 vector<ClOffset>& cs
109 ) {
110 for (ClOffset offs: cs) {
111 Clause* cl = solver->cl_alloc.ptr(offs);
112 bool satisfied = false;
113 for(Lit lit: *cl) {
114 if (solver->value(lit) == l_True) {
115 satisfied = true;
116 }
117 }
118 if (!satisfied) {
119 assert(solver->value((*cl)[0]) == l_Undef);
120 assert(solver->value((*cl)[1]) == l_Undef);
121 }
122 solver->attachClause(*cl, false);
123 }
124 }
125
126 /**
127 @brief Cleans clauses from failed literals/removes satisfied clauses from cs
128
129 May change solver->ok to FALSE (!)
130 */
cleanAndAttachClauses(vector<ClOffset> & cs,bool removeStatsFirst)131 void CompleteDetachReatacher::cleanAndAttachClauses(
132 vector<ClOffset>& cs
133 , bool removeStatsFirst
134 ) {
135 vector<ClOffset>::iterator i = cs.begin();
136 vector<ClOffset>::iterator j = i;
137 for (vector<ClOffset>::iterator end = cs.end(); i != end; i++) {
138 assert(!solver->drat->something_delayed());
139 Clause* cl = solver->cl_alloc.ptr(*i);
140
141 //Handle stat removal if need be
142 if (removeStatsFirst) {
143 if (cl->red()) {
144 solver->litStats.redLits -= cl->size();
145 } else {
146 solver->litStats.irredLits -= cl->size();
147 }
148 }
149
150 if (clean_clause(cl)) {
151 solver->attachClause(*cl);
152 *j++ = *i;
153 } else {
154 solver->free_cl(*i);
155 }
156 }
157 cs.resize(cs.size() - (i-j));
158 }
159
160 /**
161 @brief Not only cleans a clause from false literals, but if clause is satisfied, it reports it
162 */
clean_clause(Clause * cl)163 bool CompleteDetachReatacher::clean_clause(Clause* cl)
164 {
165 Clause& ps = *cl;
166 (*solver->drat) << deldelay << ps << fin;
167 if (ps.size() <= 2) {
168 cout
169 << "ERROR, clause is too small, and linked in: "
170 << *cl
171 << endl;
172 }
173 assert(ps.size() > 2);
174
175 Lit *i = ps.begin();
176 Lit *j = i;
177 for (Lit *end = ps.end(); i != end; i++) {
178 if (solver->value(*i) == l_True) {
179 (*solver->drat) << findelay;
180 return false;
181 }
182 if (solver->value(*i) == l_Undef) {
183 *j++ = *i;
184 }
185 }
186 ps.shrink(i-j);
187
188 //Drat
189 if (i != j) {
190 (*solver->drat) << add << *cl
191 #ifdef STATS_NEEDED
192 << solver->sumConflicts
193 #endif
194 << fin << findelay;
195 } else {
196 solver->drat->forget_delay();
197 }
198
199 switch (ps.size()) {
200 case 0:
201 solver->ok = false;
202 return false;
203
204 case 1:
205 solver->enqueue(ps[0]);
206 #ifdef STATS_NEEDED
207 solver->propStats.propsUnit++;
208 #endif
209 return false;
210
211 case 2: {
212 solver->attach_bin_clause(ps[0], ps[1], ps.red());
213 return false;
214 }
215
216 default: {
217 break;
218 }
219 }
220
221 return true;
222 }
223