1 #include "internal.hpp"
2
3 namespace CaDiCaL {
4
External(Internal * i)5 External::External (Internal * i)
6 :
7 internal (i),
8 max_var (0),
9 vsize (0),
10 extended (false),
11 terminator (0),
12 solution (0)
13 {
14 assert (internal);
15 assert (!internal->external);
16 internal->external = this;
17 }
18
~External()19 External::~External () {
20 if (solution) delete [] solution;
21 }
22
enlarge(int new_max_var)23 void External::enlarge (int new_max_var) {
24
25 assert (!extended);
26
27 size_t new_vsize = vsize ? 2*vsize : 1 + (size_t) new_max_var;
28 while (new_vsize <= (size_t) new_max_var) new_vsize *= 2;
29 LOG ("enlarge external size from %zd to new size %zd", vsize, new_vsize);
30 vsize = new_vsize;
31 }
32
init(int new_max_var)33 void External::init (int new_max_var) {
34 assert (!extended);
35 if (new_max_var <= max_var) return;
36 int new_vars = new_max_var - max_var;
37 int old_internal_max_var = internal->max_var;
38 int new_internal_max_var = old_internal_max_var + new_vars;
39 internal->init (new_internal_max_var);
40 if ((size_t) new_max_var >= vsize) enlarge (new_max_var);
41 LOG ("initialized %d external variables", new_vars);
42 if (!max_var) {
43 assert (e2i.empty ());
44 e2i.push_back (0);
45 assert (internal->i2e.empty ());
46 internal->i2e.push_back (0);
47 } else {
48 assert (e2i.size () == (size_t) max_var + 1);
49 assert (internal->i2e.size () == (size_t) old_internal_max_var + 1);
50 }
51 int iidx = old_internal_max_var + 1, eidx;
52 for (eidx = max_var + 1; eidx <= new_max_var; eidx++, iidx++) {
53 LOG ("mapping external %d to internal %d", eidx, iidx);
54 assert (e2i.size () == (size_t) eidx);
55 e2i.push_back (iidx);
56 internal->i2e.push_back (eidx);
57 assert (internal->i2e[iidx] == eidx);
58 assert (e2i[eidx] == iidx);
59 }
60 if (internal->opts.checkfrozen)
61 while (new_max_var >= (int64_t) moltentab.size ())
62 moltentab.push_back (false);
63 assert (iidx == new_internal_max_var + 1);
64 assert (eidx == new_max_var + 1);
65 max_var = new_max_var;
66 }
67
68 /*------------------------------------------------------------------------*/
69
reset_assumptions()70 void External::reset_assumptions () {
71 assumptions.clear ();
72 internal->reset_assumptions ();
73 }
74
reset_extended()75 void External::reset_extended () {
76 if (!extended) return;
77 LOG ("reset extended");
78 extended = false;
79 }
80
reset_limits()81 void External::reset_limits () {
82 internal->reset_limits ();
83 }
84
85 /*------------------------------------------------------------------------*/
86
internalize(int elit)87 int External::internalize (int elit) {
88 int ilit;
89 if (elit) {
90 assert (elit != INT_MIN);
91 const int eidx = abs (elit);
92 if (eidx > max_var) init (eidx);
93 ilit = e2i [eidx];
94 if (elit < 0) ilit = -ilit;
95 if (!ilit) {
96 ilit = internal->max_var + 1;
97 internal->init (ilit);
98 e2i[eidx] = ilit;
99 LOG ("mapping external %d to internal %d", eidx, ilit);
100 e2i[eidx] = ilit;
101 internal->i2e.push_back (eidx);
102 assert (internal->i2e[ilit] == eidx);
103 assert (e2i[eidx] == ilit);
104 if (elit < 0) ilit = -ilit;
105 }
106 if (internal->opts.checkfrozen) {
107 assert (eidx < (int64_t) moltentab.size ());
108 if (moltentab[eidx])
109 FATAL ("can not reuse molten literal %d", eidx);
110 }
111 Flags & f = internal->flags (ilit);
112 if (f.status == Flags::UNUSED) internal->mark_active (ilit);
113 else if (f.status != Flags::ACTIVE &&
114 f.status != Flags::FIXED) internal->reactivate (ilit);
115 if (!marked (tainted, elit) && marked (witness, -elit)) {
116 assert (!internal->opts.checkfrozen);
117 LOG ("marking tainted %d", elit);
118 mark (tainted, elit);
119 }
120 } else ilit = 0;
121 return ilit;
122 }
123
add(int elit)124 void External::add (int elit) {
125 assert (elit != INT_MIN);
126 reset_extended ();
127 if (internal->opts.check &&
128 (internal->opts.checkwitness || internal->opts.checkfailed))
129 original.push_back (elit);
130 const int ilit = internalize (elit);
131 assert (!elit == !ilit);
132 if (elit) LOG ("adding external %d as internal %d", elit, ilit);
133 internal->add_original_lit (ilit);
134 }
135
assume(int elit)136 void External::assume (int elit) {
137 assert (elit);
138 reset_extended ();
139 assumptions.push_back (elit);
140 const int ilit = internalize (elit);
141 assert (ilit);
142 LOG ("assuming external %d as internal %d", elit, ilit);
143 internal->assume (ilit);
144 }
145
failed(int elit)146 bool External::failed (int elit) {
147 assert (elit);
148 assert (elit != INT_MIN);
149 int eidx = abs (elit);
150 if (eidx > max_var) return 0;
151 int ilit = e2i[eidx];
152 if (!ilit) return 0;
153 if (elit < 0) ilit = -ilit;
154 return internal->failed (ilit);
155 }
156
157 /*------------------------------------------------------------------------*/
158
159 // Internal checker if 'solve' claims the formula to be satisfiable.
160
check_satisfiable()161 void External::check_satisfiable () {
162 LOG ("checking satisfiable");
163 if (internal->opts.checkwitness)
164 check_assignment (&External::val);
165 if (internal->opts.checkassumptions && !assumptions.empty ())
166 check_assumptions_satisfied ();
167 }
168
169 // Internal checker if 'solve' claims formula to be unsatisfiable.
170
check_unsatisfiable()171 void External::check_unsatisfiable () {
172 LOG ("checking unsatisfiable");
173 if (internal->opts.checkfailed && !assumptions.empty ())
174 check_assumptions_failing ();
175 }
176
177 // Check result of 'solve' to be correct.
178
check_solve_result(int res)179 void External::check_solve_result (int res) {
180 if (!internal->opts.check) return;
181 if (res == 10) check_satisfiable ();
182 if (res == 20) check_unsatisfiable ();
183 }
184
185 // Prepare checking that completely molten literals are not used as argument
186 // of 'add' or 'assume', which is invalid under freezing semantics. This
187 // case would be caught by our 'restore' implementation so is only needed
188 // for checking the deprecated 'freeze' semantics.
189
update_molten_literals()190 void External::update_molten_literals () {
191 if (!internal->opts.checkfrozen) return;
192 assert (max_var + 1 == (int64_t) moltentab.size ());
193 int registered = 0, molten = 0;
194 for (int lit = 1; lit <= max_var; lit++) {
195 if (moltentab[lit]) {
196 LOG ("skipping already molten literal %d", lit);
197 molten++;
198 } else if (frozen (lit))
199 LOG ("skipping currently frozen literal %d", lit);
200 else {
201 LOG ("new molten literal %d", lit);
202 moltentab[lit] = true;
203 registered++;
204 molten++;
205 }
206 }
207 LOG ("registered %d new molten literals", registered);
208 LOG ("reached in total %d molten literals", molten);
209 }
210
solve()211 int External::solve () {
212 reset_extended ();
213 update_molten_literals ();
214 int res = internal->solve ();
215 if (res == 10) extend ();
216 check_solve_result (res);
217 reset_limits ();
218 return res;
219 }
220
terminate()221 void External::terminate () { internal->terminate (); }
222
223 /*------------------------------------------------------------------------*/
224
freeze(int elit)225 void External::freeze (int elit) {
226 reset_extended ();
227 int ilit = internalize (elit);
228 unsigned eidx = vidx (elit);
229 while (eidx >= frozentab.size ())
230 frozentab.push_back (0);
231 unsigned & ref = frozentab[eidx];
232 if (ref < UINT_MAX) {
233 ref++;
234 LOG ("external variable %d frozen once and now frozen %u times",
235 eidx, ref);
236 } else
237 LOG ("external variable %d frozen but remains frozen forever", eidx);
238 internal->freeze (ilit);
239 }
240
melt(int elit)241 void External::melt (int elit) {
242 reset_extended ();
243 int ilit = internalize (elit);
244 unsigned eidx = vidx (elit);
245 assert (eidx < frozentab.size ());
246 unsigned & ref = frozentab[eidx];
247 assert (ref > 0);
248 if (ref < UINT_MAX) {
249 if (!--ref)
250 LOG ("external variable %d melted once and now completely melted",
251 eidx);
252 else
253 LOG ("external variable %d melted once but remains frozen %u times",
254 eidx, ref);
255 } else
256 LOG ("external variable %d melted but remains frozen forever", eidx);
257 internal->melt (ilit);
258 }
259
260 /*------------------------------------------------------------------------*/
261
check_assignment(int (External::* a)(int)const)262 void External::check_assignment (int (External::*a)(int) const) {
263
264 // First check all assigned and consistent.
265 //
266 for (int idx = 1; idx <= max_var; idx++) {
267 if (!(this->*a) (idx)) FATAL ("unassigned variable: %d", idx);
268 if ((this->*a) (idx) != -(this->*a)(-idx))
269 FATAL ("inconsistently assigned literals %d and %d", idx, -idx);
270 }
271
272 // Then check that all (saved) original clauses are satisfied.
273 //
274 bool satisfied = false;
275 const auto end = original.end ();
276 auto start = original.begin (), i = start;
277 int64_t count = 0;
278 for (; i != end; i++) {
279 int lit = *i;
280 if (!lit) {
281 if (!satisfied) {
282 internal->fatal_message_start ();
283 fputs ("unsatisfied clause:\n", stderr);
284 for (auto j = start; j != i; j++)
285 fprintf (stderr, "%d ", *j);
286 fputc ('0', stderr);
287 internal->fatal_message_end ();
288 }
289 satisfied = false;
290 start = i + 1;
291 count++;
292 } else if (!satisfied && (this->*a) (lit) > 0) satisfied = true;
293 }
294 VERBOSE (1,
295 "satisfying assignment checked on %" PRId64 " clauses",
296 count);
297 }
298
299 /*------------------------------------------------------------------------*/
300
check_assumptions_satisfied()301 void External::check_assumptions_satisfied () {
302 for (const auto & lit : assumptions) {
303 const int tmp = val (lit);
304 if (tmp < 0) FATAL ("assumption %d falsified", lit);
305 if (!tmp) FATAL ("assumption %d unassigned", lit);
306 }
307 VERBOSE (1,
308 "checked that %zd assumptions are satisfied",
309 assumptions.size ());
310 }
311
check_assumptions_failing()312 void External::check_assumptions_failing () {
313 Solver * checker = new Solver ();
314 checker->prefix ("checker ");
315 #ifdef LOGGING
316 if (internal->opts.log) checker->set ("log", true);
317 #endif
318 for (const auto & lit : original)
319 checker->add (lit);
320 for (const auto & lit : assumptions) {
321 if (!failed (lit)) continue;
322 LOG ("checking failed literal %d in core", lit);
323 checker->add (lit);
324 checker->add (0);
325 }
326 int res = checker->solve ();
327 if (res != 20) FATAL ("failed assumptions do not form a core");
328 delete checker;
329 VERBOSE (1,
330 "checked that %zd failing assumptions form a core",
331 assumptions.size ());
332 }
333
334 /*------------------------------------------------------------------------*/
335
traverse_all_frozen_units_as_clauses(ClauseIterator & it)336 bool External::traverse_all_frozen_units_as_clauses (ClauseIterator & it) {
337
338 if (internal->unsat) return true;
339
340 vector<int> clause;
341
342 for (int idx = 1; idx <= max_var; idx++) {
343 const int tmp = fixed (idx);
344 if (!tmp) continue;
345 if (!frozen (idx)) continue;
346 int unit = tmp < 0 ? -idx : idx;
347 clause.push_back (unit);
348 if (!it.clause (clause))
349 return false;
350 clause.clear ();
351 }
352
353 return true;
354 }
355
356 /*------------------------------------------------------------------------*/
357
358 bool
traverse_all_non_frozen_units_as_witnesses(WitnessIterator & it)359 External::traverse_all_non_frozen_units_as_witnesses (WitnessIterator & it)
360 {
361 if (internal->unsat) return true;
362
363 vector<int> clause_and_witness;
364
365 for (int idx = 1; idx <= max_var; idx++) {
366 if (frozen (idx)) continue;
367 const int tmp = fixed (idx);
368 if (!tmp) continue;
369 int unit = tmp < 0 ? -idx : idx;
370 clause_and_witness.push_back (unit);
371 if (!it.witness (clause_and_witness, clause_and_witness))
372 return false;
373 clause_and_witness.clear ();
374 }
375
376 return true;
377 }
378
379 }
380