Branch data Line data Source code
1 : : /*-
2 : : * Copyright (c) 2013-2017 Vsevolod Stakhov <vsevolod@FreeBSD.org>
3 : : * All rights reserved.
4 : : *
5 : : * Redistribution and use in source and binary forms, with or without
6 : : * modification, are permitted provided that the following conditions
7 : : * are met:
8 : : * 1. Redistributions of source code must retain the above copyright
9 : : * notice, this list of conditions and the following disclaimer
10 : : * in this position and unchanged.
11 : : * 2. Redistributions in binary form must reproduce the above copyright
12 : : * notice, this list of conditions and the following disclaimer in the
13 : : * documentation and/or other materials provided with the distribution.
14 : : *
15 : : * THIS SOFTWARE IS PROVIDED BY THE AUTHOR(S) ``AS IS'' AND ANY EXPRESS OR
16 : : * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
17 : : * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
18 : : * IN NO EVENT SHALL THE AUTHOR(S) BE LIABLE FOR ANY DIRECT, INDIRECT,
19 : : * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
20 : : * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
21 : : * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
22 : : * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
23 : : * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
24 : : * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25 : : */
26 : :
27 : : #include <sys/param.h>
28 : : #include <sys/mount.h>
29 : :
30 : : #include <assert.h>
31 : : #include <errno.h>
32 : : #include <stdbool.h>
33 : : #include <stdlib.h>
34 : : #include <stdio.h>
35 : : #include <string.h>
36 : : #include <ctype.h>
37 : : #include <math.h>
38 : : #include <kvec.h>
39 : :
40 : : #include "pkg.h"
41 : : #include "private/event.h"
42 : : #include "private/pkg.h"
43 : : #include "private/pkgdb.h"
44 : : #include "private/pkg_jobs.h"
45 : : #include "picosat.h"
46 : :
47 : : struct pkg_solve_item;
48 : :
49 : : enum pkg_solve_rule_type {
50 : : PKG_RULE_DEPEND = 0,
51 : : PKG_RULE_UPGRADE_CONFLICT,
52 : : PKG_RULE_EXPLICIT_CONFLICT,
53 : : PKG_RULE_REQUEST_CONFLICT,
54 : : PKG_RULE_REQUEST,
55 : : PKG_RULE_REQUIRE,
56 : : PKG_RULE_MAX
57 : : };
58 : :
59 : : static const char *rule_reasons[] = {
60 : : [PKG_RULE_DEPEND] = "dependency",
61 : : [PKG_RULE_UPGRADE_CONFLICT] = "upgrade",
62 : : [PKG_RULE_REQUEST_CONFLICT] = "candidates",
63 : : [PKG_RULE_EXPLICIT_CONFLICT] = "conflict",
64 : : [PKG_RULE_REQUEST] = "request",
65 : : [PKG_RULE_REQUIRE] = "require",
66 : : [PKG_RULE_MAX] = NULL
67 : : };
68 : :
69 : : enum pkg_solve_variable_flags {
70 : : PKG_VAR_INSTALL = (1 << 0),
71 : : PKG_VAR_TOP = (1 << 1),
72 : : PKG_VAR_FAILED = (1 << 2),
73 : : PKG_VAR_ASSUMED = (1 << 3),
74 : : PKG_VAR_ASSUMED_TRUE = (1 << 4)
75 : : };
76 : : struct pkg_solve_variable {
77 : : struct pkg_job_universe_item *unit;
78 : : unsigned int flags;
79 : : int order;
80 : : const char *digest;
81 : : const char *uid;
82 : : const char *assumed_reponame;
83 : : struct pkg_solve_variable *next, *prev;
84 : : };
85 : :
86 : : struct pkg_solve_item {
87 : : int nitems;
88 : : int nresolved;
89 : : struct pkg_solve_variable *var;
90 : : int inverse;
91 : : struct pkg_solve_item *prev,*next;
92 : : };
93 : :
94 : : struct pkg_solve_rule {
95 : : enum pkg_solve_rule_type reason;
96 : : struct pkg_solve_item *items;
97 : : };
98 : :
99 : : struct pkg_solve_problem {
100 : : struct pkg_jobs *j;
101 : : kvec_t(struct pkg_solve_rule *) rules;
102 : : pkghash *variables_by_uid;
103 : : struct pkg_solve_variable *variables;
104 : : PicoSAT *sat;
105 : : size_t nvars;
106 : : };
107 : :
108 : : struct pkg_solve_impl_graph {
109 : : struct pkg_solve_variable *var;
110 : : struct pkg_solve_impl_graph *prev, *next;
111 : : };
112 : :
113 : : /*
114 : : * Use XOR here to implement the following logic:
115 : : * atom is true if it is installed and not inverted or
116 : : * if it is not installed but inverted
117 : : */
118 : : #define PKG_SOLVE_CHECK_ITEM(item) \
119 : : ((item)->var->to_install ^ (item)->inverse)
120 : :
121 : : /*
122 : : * Utilities to convert jobs to SAT rule
123 : : */
124 : :
125 : : static void
126 : 3134 : pkg_solve_item_new(struct pkg_solve_rule *rule, struct pkg_solve_variable *var,
127 : : int inverse)
128 : : {
129 : : struct pkg_solve_item *it;
130 : :
131 : 3134 : it = xcalloc(1, sizeof(struct pkg_solve_item));
132 : 3134 : it->var = var;
133 : 3134 : it->inverse = inverse;
134 [ + + ]: 3134 : it->nitems = rule->items ? rule->items->nitems + 1 : 1;
135 [ + + ]: 3134 : DL_APPEND(rule->items, it);
136 : 3134 : }
137 : :
138 : : static struct pkg_solve_rule *
139 : 1834 : pkg_solve_rule_new(enum pkg_solve_rule_type reason)
140 : : {
141 : : struct pkg_solve_rule *result;
142 : :
143 : 1834 : result = xcalloc(1, sizeof(struct pkg_solve_rule));
144 : 1834 : result->reason = reason;
145 : :
146 : 1834 : return (result);
147 : : }
148 : :
149 : : static void
150 : 1291 : pkg_solve_variable_set(struct pkg_solve_variable *var,
151 : : struct pkg_job_universe_item *item)
152 : : {
153 : 1291 : var->unit = item;
154 : : /* XXX: Is it safe to save a ptr here ? */
155 : 1291 : var->digest = item->pkg->digest;
156 : 1291 : var->uid = item->pkg->uid;
157 : 1291 : var->prev = var;
158 : 1291 : }
159 : :
160 : : static void
161 : 1834 : pkg_solve_rule_free(struct pkg_solve_rule *rule)
162 : : {
163 : : struct pkg_solve_item *it, *tmp;
164 : :
165 [ + + + + ]: 4968 : LL_FOREACH_SAFE(rule->items, it, tmp) {
166 : 3134 : free(it);
167 : 3134 : }
168 : 1834 : free(rule);
169 : 1834 : }
170 : :
171 : :
172 : : void
173 : 640 : pkg_solve_problem_free(struct pkg_solve_problem *problem)
174 : : {
175 [ + + ]: 1646 : while (kv_size(problem->rules)) {
176 : 1006 : pkg_solve_rule_free(kv_pop(problem->rules));
177 : : }
178 : :
179 : 640 : pkghash_destroy(problem->variables_by_uid);
180 : :
181 : 640 : picosat_reset(problem->sat);
182 : 640 : free(problem->variables);
183 : 640 : free(problem);
184 : 640 : }
185 : :
186 : :
187 : : static void
188 : 0 : pkg_print_rule_buf(struct pkg_solve_rule *rule, xstring *sb)
189 : : {
190 : 0 : struct pkg_solve_item *it = rule->items, *key_elt = NULL;
191 : :
192 : 0 : fprintf(sb->fp, "%s rule: ", rule_reasons[rule->reason]);
193 [ # # # # : 0 : switch(rule->reason) {
# # ]
194 : : case PKG_RULE_DEPEND:
195 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
196 [ # # ]: 0 : if (it->inverse == -1) {
197 : 0 : key_elt = it;
198 : 0 : break;
199 : : }
200 : 0 : }
201 [ # # ]: 0 : if (key_elt) {
202 : 0 : fprintf(sb->fp, "package %s%s depends on: ", key_elt->var->uid,
203 : 0 : (key_elt->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
204 : 0 : }
205 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
206 [ # # ]: 0 : if (it != key_elt) {
207 : 0 : fprintf(sb->fp, "%s%s", it->var->uid,
208 : 0 : (it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
209 : 0 : }
210 : 0 : }
211 : 0 : break;
212 : : case PKG_RULE_UPGRADE_CONFLICT:
213 : 0 : fprintf(sb->fp, "upgrade local %s-%s to remote %s-%s",
214 : 0 : it->var->uid, it->var->unit->pkg->version,
215 : 0 : it->next->var->uid, it->next->var->unit->pkg->version);
216 : 0 : break;
217 : : case PKG_RULE_EXPLICIT_CONFLICT:
218 : 0 : fprintf(sb->fp, "The following packages conflict with each other: ");
219 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
220 : 0 : fprintf(sb->fp, "%s-%s%s%s", it->var->unit->pkg->uid, it->var->unit->pkg->version,
221 : 0 : (it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)",
222 : 0 : it->next ? ", " : "");
223 : 0 : }
224 : 0 : break;
225 : : case PKG_RULE_REQUIRE:
226 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
227 [ # # ]: 0 : if (it->inverse == -1) {
228 : 0 : key_elt = it;
229 : 0 : break;
230 : : }
231 : 0 : }
232 [ # # ]: 0 : if (key_elt) {
233 : 0 : fprintf(sb->fp, "package %s%s depends on a requirement provided by: ",
234 : 0 : key_elt->var->uid,
235 : 0 : (key_elt->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
236 : 0 : }
237 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
238 [ # # ]: 0 : if (it != key_elt) {
239 : 0 : fprintf(sb->fp, "%s%s", it->var->uid,
240 : 0 : (it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
241 : 0 : }
242 : 0 : }
243 : 0 : break;
244 : : case PKG_RULE_REQUEST_CONFLICT:
245 : 0 : fprintf(sb->fp, "The following packages in request are candidates for installation: ");
246 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
247 : 0 : fprintf(sb->fp, "%s-%s%s", it->var->uid, it->var->unit->pkg->version,
248 : 0 : it->next ? ", " : "");
249 : 0 : }
250 : 0 : break;
251 : : default:
252 : 0 : break;
253 : : }
254 : 0 : }
255 : :
256 : : static void
257 : 1006 : pkg_debug_print_rule(struct pkg_solve_rule *rule)
258 : : {
259 : : xstring *sb;
260 : :
261 [ + - ]: 1006 : if (ctx.debug_level < 3)
262 : 1006 : return;
263 : :
264 : 0 : sb = xstring_new();
265 : :
266 : 0 : pkg_print_rule_buf(rule, sb);
267 : :
268 : 0 : fflush(sb->fp);
269 : 0 : pkg_debug(2, "%s", sb->buf);
270 : 0 : xstring_free(sb);
271 : 1006 : }
272 : :
273 : : static int
274 : 56 : pkg_solve_handle_provide (struct pkg_solve_problem *problem,
275 : : struct pkg_job_provide *pr, struct pkg_solve_rule *rule,
276 : : struct pkg *orig, const char *reponame, int *cnt)
277 : : {
278 : : struct pkg_solve_variable *var, *curvar;
279 : : struct pkg_job_universe_item *un;
280 : : struct pkg *pkg;
281 : : bool libfound, providefound;
282 : :
283 : : /* Find the first package in the universe list */
284 : 56 : un = pr->un;
285 [ + + ]: 76 : while (un->prev->next != NULL) {
286 : 20 : un = un->prev;
287 : : }
288 : :
289 : : /* Find the corresponding variables chain */
290 : :
291 : 56 : var = pkghash_get_value(problem->variables_by_uid, un->pkg->uid);
292 [ + + ]: 140 : LL_FOREACH(var, curvar) {
293 : : /*
294 : : * For each provide we need to check whether this package
295 : : * actually provides this require
296 : : */
297 : 84 : libfound = providefound = false;
298 : 84 : pkg = curvar->unit->pkg;
299 : :
300 [ + + ]: 84 : if (pr->is_shlib) {
301 : 16 : libfound = (pkghash_get(pkg->shlibs_provided, pr->provide) != NULL);
302 : : /* Skip incompatible ABI as well */
303 [ + - + - ]: 16 : if (libfound && strcmp(pkg->arch, orig->arch) != 0) {
304 : 0 : pkg_debug(2, "solver: require %s: package %s-%s(%c) provides wrong ABI %s, "
305 : 0 : "wanted %s", pr->provide, pkg->name, pkg->version,
306 : 0 : pkg->type == PKG_INSTALLED ? 'l' : 'r', orig->arch, pkg->arch);
307 : 0 : continue;
308 : : }
309 : 16 : }
310 : : else {
311 : 68 : providefound = (pkghash_get(pkg->provides, pr->provide) != NULL);
312 : : }
313 : :
314 [ + + + + ]: 84 : if (!providefound && !libfound) {
315 : 56 : pkg_debug(4, "solver: %s provide is not satisfied by %s-%s(%c)", pr->provide,
316 : 28 : pkg->name, pkg->version, pkg->type == PKG_INSTALLED ?
317 : : 'l' : 'r');
318 : 28 : continue;
319 : : }
320 : :
321 [ - + ]: 56 : if (curvar->assumed_reponame == NULL) {
322 : 56 : curvar->assumed_reponame = reponame;
323 : 56 : }
324 : :
325 : 112 : pkg_debug(4, "solver: %s provide is satisfied by %s-%s(%c)", pr->provide,
326 : 56 : pkg->name, pkg->version, pkg->type == PKG_INSTALLED ?
327 : : 'l' : 'r');
328 : :
329 : 56 : pkg_solve_item_new(rule, curvar, 1);
330 : 56 : (*cnt)++;
331 : 56 : }
332 : :
333 : 56 : return (EPKG_OK);
334 : : }
335 : :
336 : : static int
337 : 503 : pkg_solve_add_depend_rule(struct pkg_solve_problem *problem,
338 : : struct pkg_solve_variable *var,
339 : : struct pkg_dep *dep,
340 : : const char *reponame)
341 : : {
342 : : const char *uid;
343 : : struct pkg_solve_variable *depvar, *curvar;
344 : 503 : struct pkg_solve_rule *rule = NULL;
345 : 503 : int cnt = 0;
346 : : struct pkg_dep *cur;
347 : :
348 : : /* Dependency rule: (!A | B1 | B2 | B3...) */
349 : 503 : rule = pkg_solve_rule_new(PKG_RULE_DEPEND);
350 : : /* !A */
351 : 503 : pkg_solve_item_new(rule, var, -1);
352 : :
353 [ + + ]: 1006 : LL_FOREACH2(dep, cur, alt_next) {
354 : 503 : uid = cur->uid;
355 : 503 : depvar = NULL;
356 : 503 : depvar = pkghash_get_value(problem->variables_by_uid, uid);
357 [ + + ]: 503 : if (depvar == NULL) {
358 : 59 : pkg_debug(2, "cannot find variable dependency %s", uid);
359 : 59 : continue;
360 : : }
361 : :
362 : : /* B1 | B2 | ... */
363 : 444 : cnt = 1;
364 [ + + ]: 1068 : LL_FOREACH(depvar, curvar) {
365 : : /* Propagate reponame */
366 [ - + ]: 624 : if (curvar->assumed_reponame == NULL) {
367 : 624 : curvar->assumed_reponame = reponame;
368 : 624 : }
369 : :
370 : 624 : pkg_solve_item_new(rule, curvar, 1);
371 : 624 : cnt++;
372 : 624 : }
373 : 444 : }
374 : :
375 [ + + ]: 503 : if (cnt == 0) {
376 : 59 : pkg_debug(2, "cannot find any suitable dependency for %s", var->uid);
377 : 59 : pkg_solve_rule_free(rule);
378 : :
379 : 59 : return (EPKG_FATAL);
380 : : }
381 : :
382 [ + + + + ]: 444 : kv_prepend(typeof(rule), problem->rules, rule);
383 : :
384 : 444 : return (EPKG_OK);
385 : 503 : }
386 : :
387 : : static int
388 : 108 : pkg_solve_add_conflict_rule(struct pkg_solve_problem *problem,
389 : : struct pkg *pkg,
390 : : struct pkg_solve_variable *var,
391 : : struct pkg_conflict *conflict)
392 : : {
393 : : const char *uid;
394 : : struct pkg_solve_variable *confvar, *curvar;
395 : 108 : struct pkg_solve_rule *rule = NULL;
396 : : struct pkg *other;
397 : :
398 : 108 : uid = conflict->uid;
399 : 108 : confvar = pkghash_get_value(problem->variables_by_uid, uid);
400 [ - + ]: 108 : if (confvar == NULL) {
401 : 0 : pkg_debug(2, "cannot find conflict %s", uid);
402 : 0 : return (EPKG_END);
403 : : }
404 : :
405 : : /* Add conflict rule from each of the alternative */
406 [ + + ]: 268 : LL_FOREACH(confvar, curvar) {
407 : 160 : other = curvar->unit->pkg;
408 [ + + ]: 160 : if (conflict->type == PKG_CONFLICT_REMOTE_LOCAL) {
409 : : /* Skip unappropriate packages */
410 [ + + ]: 140 : if (pkg->type == PKG_INSTALLED) {
411 [ + + ]: 68 : if (other->type == PKG_INSTALLED)
412 : 16 : continue;
413 : 52 : }
414 : : else {
415 [ + + ]: 72 : if (other->type != PKG_INSTALLED)
416 : 24 : continue;
417 : : }
418 : 100 : }
419 [ - + ]: 20 : else if (conflict->type == PKG_CONFLICT_REMOTE_REMOTE) {
420 [ - + ]: 20 : if (pkg->type == PKG_INSTALLED)
421 : 0 : continue;
422 : :
423 [ + + ]: 20 : if (other->type == PKG_INSTALLED)
424 : 4 : continue;
425 : 16 : }
426 : : /*
427 : : * Also if a conflict is digest specific then we skip
428 : : * variables with mismatched digests
429 : : */
430 [ - + ]: 116 : if (conflict->digest) {
431 [ + + ]: 116 : if (strcmp (conflict->digest, other->digest) != 0)
432 : 8 : continue;
433 : 108 : }
434 : :
435 : : /* Conflict rule: (!A | !Bx) */
436 : 108 : rule = pkg_solve_rule_new(PKG_RULE_EXPLICIT_CONFLICT);
437 : : /* !A */
438 : 108 : pkg_solve_item_new(rule, var, -1);
439 : : /* !Bx */
440 : 108 : pkg_solve_item_new(rule, curvar, -1);
441 : :
442 [ + + + + ]: 108 : kv_prepend(typeof(rule), problem->rules, rule);
443 : 108 : }
444 : :
445 : 108 : return (EPKG_OK);
446 : 108 : }
447 : :
448 : : static int
449 : 80 : pkg_solve_add_require_rule(struct pkg_solve_problem *problem,
450 : : struct pkg_solve_variable *var,
451 : : const char *requirement,
452 : : const char *reponame)
453 : : {
454 : : struct pkg_solve_rule *rule;
455 : 80 : struct pkg_solve_item *it = NULL;
456 : : struct pkg_job_provide *pr, *prhead;
457 : : struct pkg *pkg;
458 : : int cnt;
459 : :
460 : 80 : pkg = var->unit->pkg;
461 : :
462 : 80 : prhead = pkghash_get_value(problem->j->universe->provides, requirement);
463 [ + + ]: 80 : if (prhead != NULL) {
464 : 56 : pkg_debug(4, "solver: Add require rule: %s-%s(%c) wants %s",
465 : 56 : pkg->name, pkg->version, pkg->type == PKG_INSTALLED ? 'l' : 'r',
466 : 56 : requirement);
467 : : /* Require rule !A | P1 | P2 | P3 ... */
468 : 56 : rule = pkg_solve_rule_new(PKG_RULE_REQUIRE);
469 : : /* !A */
470 : 56 : pkg_solve_item_new(rule, var, -1);
471 : : /* B1 | B2 | ... */
472 : 56 : cnt = 1;
473 [ + + ]: 112 : LL_FOREACH(prhead, pr) {
474 [ + - + - ]: 112 : if (pkg_solve_handle_provide(problem, pr, rule, pkg, reponame, &cnt)
475 : 56 : != EPKG_OK) {
476 : 0 : free(it);
477 : 0 : free(rule);
478 : 0 : return (EPKG_FATAL);
479 : : }
480 : 56 : }
481 : :
482 [ + - ]: 56 : if (cnt > 1) {
483 [ + + + + ]: 56 : kv_prepend(typeof(rule), problem->rules, rule);
484 : 56 : }
485 : : else {
486 : : /* Missing dependencies... */
487 : 0 : free(it);
488 : 0 : free(rule);
489 : : }
490 : 56 : }
491 : : else {
492 : : /*
493 : : * XXX:
494 : : * This is terribly broken now so ignore till provides/requires
495 : : * are really fixed.
496 : : */
497 : 24 : pkg_debug(1, "solver: for package: %s cannot find provide for requirement: %s",
498 : 24 : pkg->name, requirement);
499 : : }
500 : :
501 : 80 : return (EPKG_OK);
502 : 80 : }
503 : :
504 : : static struct pkg_solve_variable *
505 : 1652 : pkg_solve_find_var_in_chain(struct pkg_solve_variable *var,
506 : : struct pkg_job_universe_item *item)
507 : : {
508 : : struct pkg_solve_variable *cur;
509 : :
510 [ + - ]: 1652 : assert(var != NULL);
511 [ + - ]: 1953 : LL_FOREACH(var, cur) {
512 [ + + ]: 1953 : if (cur->unit == item) {
513 : 1652 : return (cur);
514 : : }
515 : 301 : }
516 : :
517 : 0 : return (NULL);
518 : 1652 : }
519 : :
520 : : static int
521 : 769 : pkg_solve_add_request_rule(struct pkg_solve_problem *problem,
522 : : struct pkg_solve_variable *var, struct pkg_job_request *req, int inverse)
523 : : {
524 : 769 : struct pkg_solve_rule *rule = NULL;
525 : : struct pkg_job_request_item *item, *confitem;
526 : : struct pkg_solve_variable *confvar, *curvar;
527 : : int cnt;
528 : :
529 : 769 : pkg_debug(4, "solver: add variable from %s request with uid %s-%s",
530 : 769 : inverse < 0 ? "delete" : "install", var->uid, var->digest);
531 : :
532 : : /*
533 : : * Get the suggested item
534 : : */
535 : 769 : var = pkghash_get_value(problem->variables_by_uid, req->item->pkg->uid);
536 : 769 : var = pkg_solve_find_var_in_chain(var, req->item->unit);
537 [ + - ]: 769 : assert(var != NULL);
538 : : /* Assume the most significant variable */
539 : 769 : picosat_assume(problem->sat, var->order * inverse);
540 : :
541 : : /*
542 : : * Add clause for any of candidates:
543 : : * A1 | A2 | ... | An
544 : : */
545 : 769 : rule = pkg_solve_rule_new(PKG_RULE_REQUEST);
546 : :
547 : 769 : cnt = 0;
548 : :
549 [ + + ]: 1652 : LL_FOREACH(req->item, item) {
550 : 883 : curvar = pkg_solve_find_var_in_chain(var, item->unit);
551 [ + - ]: 883 : assert(curvar != NULL);
552 : 883 : pkg_solve_item_new(rule, curvar, inverse);
553 : : /* All request variables are top level */
554 : 883 : curvar->flags |= PKG_VAR_TOP;
555 : :
556 [ + + ]: 883 : if (inverse > 0) {
557 : 734 : curvar->flags |= PKG_VAR_INSTALL;
558 : 734 : }
559 : :
560 : 883 : cnt++;
561 : 883 : }
562 : :
563 [ + + + - ]: 769 : if (cnt > 1 && var->unit->inhash != 0) {
564 [ # # # # ]: 0 : kv_prepend(typeof(rule), problem->rules, rule);
565 : : /* Also need to add pairs of conflicts */
566 [ # # ]: 0 : LL_FOREACH(req->item, item) {
567 : 0 : curvar = pkg_solve_find_var_in_chain(var, item->unit);
568 [ # # ]: 0 : assert(curvar != NULL);
569 [ # # ]: 0 : if (item->next == NULL)
570 : 0 : continue;
571 [ # # ]: 0 : LL_FOREACH(item->next, confitem) {
572 : 0 : confvar = pkg_solve_find_var_in_chain(var, confitem->unit);
573 [ # # ]: 0 : assert(confvar != NULL && confvar != curvar && confvar != var);
574 : : /* Conflict rule: (!A | !Bx) */
575 : 0 : rule = pkg_solve_rule_new(PKG_RULE_REQUEST_CONFLICT);
576 : : /* !A */
577 : 0 : pkg_solve_item_new(rule, curvar, -1);
578 : : /* !Bx */
579 : 0 : pkg_solve_item_new(rule, confvar, -1);
580 : :
581 [ # # # # ]: 0 : kv_prepend(typeof(rule), problem->rules, rule);
582 : 0 : }
583 : 0 : }
584 : 0 : }
585 : : else {
586 : : /* No need to add unary rules as we added the assumption already */
587 : 769 : pkg_solve_rule_free(rule);
588 : : }
589 : :
590 : 769 : var->flags |= PKG_VAR_TOP;
591 [ + + ]: 769 : if (inverse > 0) {
592 : 620 : var->flags |= PKG_VAR_INSTALL;
593 : 620 : }
594 : :
595 : 769 : return (EPKG_OK);
596 : : }
597 : :
598 : : static int
599 : 276 : pkg_solve_add_chain_rule(struct pkg_solve_problem *problem,
600 : : struct pkg_solve_variable *var)
601 : : {
602 : : struct pkg_solve_variable *curvar, *confvar;
603 : : struct pkg_solve_rule *rule;
604 : :
605 : : /* Rewind to first */
606 [ - + ]: 276 : while (var->prev->next != NULL) {
607 : 0 : var = var->prev;
608 : : }
609 : :
610 [ - + ]: 613 : LL_FOREACH(var, curvar) {
611 : : /* Conflict rule: (!Ax | !Ay) */
612 [ + + ]: 613 : if (curvar->next == NULL) {
613 : 276 : break;
614 : : }
615 : :
616 [ + + ]: 735 : LL_FOREACH(curvar->next, confvar) {
617 : 398 : rule = pkg_solve_rule_new(PKG_RULE_UPGRADE_CONFLICT);
618 : : /* !Ax */
619 : 398 : pkg_solve_item_new(rule, curvar, -1);
620 : : /* !Ay */
621 : 398 : pkg_solve_item_new(rule, confvar, -1);
622 : :
623 [ + + + + ]: 398 : kv_prepend(typeof(rule), problem->rules, rule);
624 : 398 : }
625 : 337 : }
626 : :
627 : 276 : return (EPKG_OK);
628 : : }
629 : :
630 : : static int
631 : 954 : pkg_solve_process_universe_variable(struct pkg_solve_problem *problem,
632 : : struct pkg_solve_variable *var)
633 : : {
634 : : struct pkg_dep *dep;
635 : : struct pkg_conflict *conflict;
636 : : struct pkg *pkg;
637 : : struct pkg_solve_variable *cur_var;
638 : 954 : struct pkg_jobs *j = problem->j;
639 : 954 : struct pkg_job_request *jreq = NULL;
640 : : pkghash_it it;
641 : 954 : bool chain_added = false;
642 : :
643 [ + + ]: 2245 : LL_FOREACH(var, cur_var) {
644 : 1291 : pkg = cur_var->unit->pkg;
645 : :
646 : : /* Request */
647 [ + + ]: 1291 : if (!(cur_var->flags & PKG_VAR_TOP)) {
648 : 1047 : jreq = pkghash_get_value(j->request_add, cur_var->uid);
649 [ + + ]: 1047 : if (jreq != NULL)
650 : 620 : pkg_solve_add_request_rule(problem, cur_var, jreq, 1);
651 : 1047 : jreq = pkghash_get_value(j->request_delete, cur_var->uid);
652 [ + + ]: 1047 : if (jreq != NULL)
653 : 149 : pkg_solve_add_request_rule(problem, cur_var, jreq, -1);
654 : 1047 : }
655 : :
656 [ + + ]: 1291 : if (jreq) {
657 : 149 : cur_var->assumed_reponame = pkg->reponame;
658 : 149 : }
659 : :
660 : : /* Depends */
661 [ + + ]: 1794 : LL_FOREACH(pkg->depends, dep) {
662 [ + + + + : 1509 : if (pkg_solve_add_depend_rule(problem, cur_var, dep,
+ + ]
663 : 1006 : cur_var->assumed_reponame) != EPKG_OK) {
664 : 59 : continue;
665 : : }
666 : 444 : }
667 : :
668 : : /* Conflicts */
669 [ + + ]: 1399 : LL_FOREACH(pkg->conflicts, conflict) {
670 [ - + ]: 108 : if (pkg_solve_add_conflict_rule(problem, pkg, cur_var, conflict) !=
671 : : EPKG_OK)
672 : 0 : continue;
673 : 108 : }
674 : :
675 : : /* Shlibs */
676 : 1291 : it = pkghash_iterator(pkg->shlibs_required);
677 [ + + ]: 1323 : while (pkghash_next(&it)) {
678 [ - + - + : 96 : if (pkg_solve_add_require_rule(problem, cur_var,
- + ]
679 : 64 : it.key, cur_var->assumed_reponame) != EPKG_OK) {
680 : 0 : continue;
681 : : }
682 : : }
683 : 1291 : it = pkghash_iterator(pkg->requires);
684 [ + + ]: 1339 : while (pkghash_next(&it)) {
685 [ - + - + : 144 : if (pkg_solve_add_require_rule(problem, cur_var,
- + ]
686 : 96 : it.key, cur_var->assumed_reponame) != EPKG_OK) {
687 : 0 : continue;
688 : : }
689 : : }
690 : :
691 : :
692 : : /*
693 : : * If this var chain contains mutually conflicting vars
694 : : * we need to register conflicts with all following
695 : : * vars
696 : : */
697 [ + + + + : 1291 : if (!chain_added && (cur_var->next != NULL || cur_var->prev != var)) {
- + ]
698 [ - + ]: 276 : if (pkg_solve_add_chain_rule(problem, cur_var) != EPKG_OK)
699 : 0 : continue;
700 : :
701 : 276 : chain_added = true;
702 : 276 : }
703 : 1291 : }
704 : :
705 : 954 : return (EPKG_OK);
706 : : }
707 : :
708 : : static int
709 : 954 : pkg_solve_add_variable(struct pkg_job_universe_item *un,
710 : : struct pkg_solve_problem *problem, size_t *n)
711 : : {
712 : : struct pkg_job_universe_item *ucur;
713 : 954 : struct pkg_solve_variable *var = NULL, *tvar = NULL;
714 : :
715 [ + + ]: 2245 : LL_FOREACH(un, ucur) {
716 [ + - ]: 1291 : assert(*n < problem->nvars);
717 : :
718 : : /* Add new variable */
719 : 1291 : var = &problem->variables[*n];
720 : 1291 : pkg_solve_variable_set(var, ucur);
721 : :
722 [ + + ]: 1291 : if (tvar == NULL) {
723 : 954 : pkg_debug(4, "solver: add variable from universe with uid %s", var->uid);
724 [ + + - + ]: 1278 : pkghash_safe_add(problem->variables_by_uid, var->uid, var, NULL);
725 : 954 : tvar = var;
726 : 954 : }
727 : : else {
728 : : /* Insert a variable to a chain */
729 [ + - ]: 337 : DL_APPEND(tvar, var);
730 : : }
731 : 1291 : (*n) ++;
732 : 1291 : var->order = *n;
733 : 1291 : }
734 : :
735 : 954 : return (EPKG_OK);
736 : : }
737 : :
738 : : struct pkg_solve_problem *
739 : 640 : pkg_solve_jobs_to_sat(struct pkg_jobs *j)
740 : : {
741 : : struct pkg_solve_problem *problem;
742 : : struct pkg_job_universe_item *un;
743 : 640 : size_t i = 0;
744 : : pkghash_it it;
745 : :
746 : 640 : problem = xcalloc(1, sizeof(struct pkg_solve_problem));
747 : :
748 : 640 : problem->j = j;
749 : 640 : problem->nvars = j->universe->nitems;
750 : 640 : problem->variables = xcalloc(problem->nvars, sizeof(struct pkg_solve_variable));
751 : 640 : problem->sat = picosat_init();
752 : 640 : kv_init(problem->rules);
753 : :
754 [ + - ]: 640 : if (problem->sat == NULL) {
755 : 0 : pkg_emit_errno("picosat_init", "pkg_solve_sat_problem");
756 : 0 : return (NULL);
757 : : }
758 : :
759 : 640 : picosat_adjust(problem->sat, problem->nvars);
760 : :
761 : : /* Parse universe */
762 : 640 : it = pkghash_iterator(j->universe->items);
763 [ + + ]: 1594 : while (pkghash_next(&it)) {
764 : 954 : un = (struct pkg_job_universe_item *)it.value;
765 : : /* Add corresponding variables */
766 [ + - ]: 954 : if (pkg_solve_add_variable(un, problem, &i) == EPKG_FATAL)
767 : 0 : goto err;
768 : : }
769 : :
770 : : /* Add rules for all conflict chains */
771 : 640 : it = pkghash_iterator(j->universe->items);
772 [ + + ]: 1594 : while (pkghash_next(&it)) {
773 : : struct pkg_solve_variable *var;
774 : :
775 : 954 : un = (struct pkg_job_universe_item *)it.value;
776 : 954 : var = pkghash_get_value(problem->variables_by_uid, un->pkg->uid);
777 [ + - ]: 954 : if (var == NULL) {
778 : 0 : pkg_emit_error("internal solver error: variable %s is not found",
779 : 0 : un->pkg->uid);
780 : 0 : goto err;
781 : : }
782 [ + - ]: 954 : if (pkg_solve_process_universe_variable(problem, var) != EPKG_OK)
783 : 0 : goto err;
784 : : }
785 : :
786 [ + + ]: 640 : if (kv_size(problem->rules) == 0)
787 : 424 : pkg_debug(1, "problem has no requests");
788 : :
789 : 640 : return (problem);
790 : :
791 : : err:
792 : 0 : return (NULL);
793 : 640 : }
794 : :
795 : : static int
796 : 672 : pkg_solve_picosat_iter(struct pkg_solve_problem *problem, int iter __unused)
797 : : {
798 : : int res, i;
799 : : struct pkg_solve_variable *var, *cur;
800 : 672 : bool is_installed = false;
801 : :
802 : 672 : picosat_reset_phases(problem->sat);
803 : 672 : picosat_reset_scores(problem->sat);
804 : : /* Set initial guess */
805 [ + + ]: 2151 : for (i = 0; i < problem->nvars; i ++) {
806 : 1479 : var = &problem->variables[i];
807 : 1479 : is_installed = false;
808 : :
809 [ + + ]: 2436 : LL_FOREACH(var, cur) {
810 [ + + ]: 1560 : if (cur->unit->pkg->type == PKG_INSTALLED) {
811 : 603 : is_installed = true;
812 : 603 : break;
813 : : }
814 : 957 : }
815 : :
816 [ + + ]: 1479 : if (var->flags & PKG_VAR_TOP)
817 : 756 : continue;
818 : :
819 [ + + ]: 723 : if (!(var->flags & (PKG_VAR_FAILED|PKG_VAR_ASSUMED))) {
820 [ + + ]: 459 : if (is_installed) {
821 : 334 : picosat_set_default_phase_lit(problem->sat, i + 1, 1);
822 : 334 : picosat_set_more_important_lit(problem->sat, i + 1);
823 : 334 : }
824 [ + + + + ]: 125 : else if (!var->next && var->prev == var) {
825 : : /* Prefer not to install if have no local version */
826 : 28 : picosat_set_default_phase_lit(problem->sat, i + 1, -1);
827 : 28 : picosat_set_less_important_lit(problem->sat, i + 1);
828 : 28 : }
829 : 459 : }
830 [ + + ]: 264 : else if (var->flags & PKG_VAR_FAILED) {
831 [ + + ]: 36 : if (var->unit->pkg->type == PKG_INSTALLED) {
832 : 32 : picosat_set_default_phase_lit(problem->sat, i + 1, -1);
833 : 32 : picosat_set_less_important_lit(problem->sat, i + 1);
834 : 32 : }
835 : : else {
836 : 4 : picosat_set_default_phase_lit(problem->sat, i + 1, 1);
837 : 4 : picosat_set_more_important_lit(problem->sat, i + 1);
838 : : }
839 : :
840 : 36 : var->flags &= ~PKG_VAR_FAILED;
841 : 36 : }
842 : 723 : }
843 : :
844 : 672 : res = picosat_sat(problem->sat, -1);
845 : :
846 : 672 : return (res);
847 : : }
848 : :
849 : : static void
850 : 1006 : pkg_solve_set_initial_assumption(struct pkg_solve_problem *problem,
851 : : struct pkg_solve_rule *rule)
852 : : {
853 : : struct pkg_job_universe_item *selected, *cur, *local, *first;
854 : : struct pkg_solve_item *item;
855 : : struct pkg_solve_variable *var, *cvar;
856 : 1006 : bool conservative = false, prefer_local = false;
857 : 1006 : const char *assumed_reponame = NULL;
858 : :
859 [ + + ]: 1006 : if (problem->j->type == PKG_JOBS_INSTALL) {
860 : : /* Avoid upgrades on INSTALL job */
861 : 229 : conservative = true;
862 : 229 : prefer_local = true;
863 : 229 : }
864 : : else {
865 : 777 : conservative = pkg_object_bool(pkg_config_get("CONSERVATIVE_UPGRADE"));
866 : : }
867 : :
868 [ + + + ]: 1006 : switch (rule->reason) {
869 : : case PKG_RULE_DEPEND:
870 : : /*
871 : : * The first item is dependent item, the next items are
872 : : * dependencies. We assume that all deps belong to a single
873 : : * upgrade chain.
874 : : */
875 [ + - ]: 444 : assert (rule->items != NULL);
876 : 444 : item = rule->items;
877 : 444 : var = item->var;
878 : 444 : assumed_reponame = var->assumed_reponame;
879 : :
880 : : /* Check what we are depending on */
881 [ + + ]: 444 : if (!(var->flags & (PKG_VAR_TOP|PKG_VAR_ASSUMED_TRUE))) {
882 : : /*
883 : : * We are interested merely in dependencies of top variables
884 : : * or of previously assumed dependencies
885 : : */
886 : 188 : pkg_debug(4, "solver: not interested in dependencies for %s-%s",
887 : 188 : var->unit->pkg->name, var->unit->pkg->version);
888 : 188 : return;
889 : : }
890 : : else {
891 : 256 : pkg_debug(4, "solver: examine dependencies for %s-%s",
892 : 256 : var->unit->pkg->name, var->unit->pkg->version);
893 : : }
894 : :
895 : :
896 : 256 : item = rule->items->next;
897 [ - + ]: 256 : assert (item != NULL);
898 : 256 : var = item->var;
899 : 256 : first = var->unit;
900 : :
901 : : /* Rewind chains */
902 [ - + ]: 256 : while (first->prev->next != NULL) {
903 : 0 : first = first->prev;
904 : : }
905 [ - + ]: 256 : while (var->prev->next != NULL) {
906 : 0 : var = var->prev;
907 : : }
908 : :
909 [ + + ]: 480 : LL_FOREACH(var, cvar) {
910 [ + + ]: 300 : if (cvar->flags & PKG_VAR_ASSUMED) {
911 : : /* Do not reassume packages */
912 : 76 : return;
913 : : }
914 : 224 : }
915 : : /* Forward chain to find local package */
916 : 180 : local = NULL;
917 : :
918 [ + + ]: 292 : DL_FOREACH (first, cur) {
919 [ + + ]: 180 : if (cur->pkg->type == PKG_INSTALLED) {
920 : 68 : local = cur;
921 : 68 : break;
922 : : }
923 : 112 : }
924 : :
925 [ + + + + ]: 180 : if (prefer_local && local != NULL) {
926 : 4 : selected = local;
927 : 4 : }
928 : : else {
929 : 352 : selected = pkg_jobs_universe_select_candidate(first, local,
930 : 176 : conservative, assumed_reponame, true);
931 : :
932 [ + + - + : 176 : if (local && (strcmp(selected->pkg->digest, local->pkg->digest) == 0 ||
# # ]
933 : 0 : !pkg_jobs_need_upgrade(selected->pkg, local->pkg))) {
934 : 64 : selected = local;
935 : 64 : }
936 : : }
937 : :
938 : : /* Now we can find the according var */
939 [ - + ]: 180 : if (selected != NULL) {
940 : :
941 [ + + ]: 404 : LL_FOREACH(var, cvar) {
942 [ + + ]: 224 : if (cvar->unit == selected) {
943 : 180 : picosat_set_default_phase_lit(problem->sat, cvar->order, 1);
944 : 180 : pkg_debug(4, "solver: assumed %s-%s(%s) to be installed",
945 : 180 : selected->pkg->name, selected->pkg->version,
946 : 180 : selected->pkg->type == PKG_INSTALLED ? "l" : "r");
947 : 180 : cvar->flags |= PKG_VAR_ASSUMED_TRUE;
948 : 180 : }
949 : : else {
950 : 44 : pkg_debug(4, "solver: assumed %s-%s(%s) to be NOT installed",
951 : 44 : cvar->unit->pkg->name, cvar->unit->pkg->version,
952 : 44 : cvar->unit->pkg->type == PKG_INSTALLED ? "l" : "r");
953 : 44 : picosat_set_default_phase_lit(problem->sat, cvar->order, -1);
954 : : }
955 : :
956 : 224 : cvar->flags |= PKG_VAR_ASSUMED;
957 : 224 : }
958 : :
959 : 180 : }
960 : 180 : break;
961 : : case PKG_RULE_REQUIRE:
962 : : /* XXX: deal with require rules somehow */
963 : 56 : break;
964 : : default:
965 : : /* No nothing */
966 : 506 : return;
967 : : }
968 : 1006 : }
969 : :
970 : : int
971 : 640 : pkg_solve_sat_problem(struct pkg_solve_problem *problem)
972 : : {
973 : : struct pkg_solve_rule *rule;
974 : : struct pkg_solve_item *item;
975 : 640 : int res, iter = 0;
976 : : size_t i;
977 : 640 : bool need_reiterate = false;
978 : 640 : const int *failed = NULL;
979 : 640 : int attempt = 0;
980 : : struct pkg_solve_variable *var;
981 : :
982 [ + + ]: 1646 : for (i = 0; i < kv_size(problem->rules); i++) {
983 : 1006 : rule = kv_A(problem->rules, i);
984 : :
985 [ + + ]: 3198 : LL_FOREACH(rule->items, item) {
986 : 2192 : picosat_add(problem->sat, item->var->order * item->inverse);
987 : 2192 : }
988 : :
989 : 1006 : picosat_add(problem->sat, 0);
990 : 1006 : pkg_debug_print_rule(rule);
991 : 1006 : }
992 : :
993 [ + + ]: 1646 : for (i = 0; i < kv_size(problem->rules); i++) {
994 : 1006 : rule = kv_A(problem->rules, i);
995 : 1006 : pkg_solve_set_initial_assumption(problem, rule);
996 : 1646 : }
997 : :
998 : : reiterate:
999 : :
1000 : 672 : res = pkg_solve_picosat_iter(problem, iter);
1001 : :
1002 [ + + ]: 672 : if (res != PICOSAT_SATISFIABLE) {
1003 : : /*
1004 : : * in case we cannot satisfy the problem it appears by
1005 : : * experience that the culprit seems to always be the latest of
1006 : : * listed in the failed assumptions.
1007 : : * So try to remove them for the given problem.
1008 : : * To avoid endless loop allow a maximum of 10 iterations no
1009 : : * more
1010 : : */
1011 : 8 : failed = picosat_failed_assumptions(problem->sat);
1012 : 8 : attempt++;
1013 : :
1014 : : /* get the last failure */
1015 [ + + ]: 24 : while (*failed) {
1016 : 16 : failed++;
1017 : : }
1018 : 8 : failed--;
1019 : :
1020 [ - + ]: 8 : if (attempt >= 10) {
1021 : 0 : pkg_emit_error("Cannot solve problem using SAT solver");
1022 : 0 : xstring *sb = xstring_new();
1023 : :
1024 [ # # ]: 0 : while (*failed) {
1025 : 0 : var = &problem->variables[abs(*failed) - 1];
1026 [ # # ]: 0 : for (i = 0; i < kv_size(problem->rules); i++) {
1027 : 0 : rule = kv_A(problem->rules, i);
1028 : :
1029 [ # # ]: 0 : if (rule->reason != PKG_RULE_DEPEND) {
1030 [ # # ]: 0 : LL_FOREACH(rule->items, item) {
1031 [ # # ]: 0 : if (item->var == var) {
1032 : 0 : pkg_print_rule_buf(rule, sb);
1033 : 0 : fputc('\n', sb->fp);
1034 : 0 : break;
1035 : : }
1036 : 0 : }
1037 : 0 : }
1038 : 0 : }
1039 : :
1040 : 0 : fprintf(sb->fp, "cannot %s package %s, remove it from request? ",
1041 : 0 : var->flags & PKG_VAR_INSTALL ? "install" : "remove", var->uid);
1042 : :
1043 : 0 : fflush(sb->fp);
1044 [ # # ]: 0 : if (pkg_emit_query_yesno(true, sb->buf)) {
1045 : 0 : var->flags |= PKG_VAR_FAILED;
1046 : 0 : }
1047 : :
1048 : 0 : failed++;
1049 : 0 : need_reiterate = true;
1050 : : }
1051 : 0 : xstring_free(sb);
1052 : 0 : } else {
1053 : 8 : pkg_emit_notice("Cannot solve problem using SAT solver, trying another plan");
1054 : 8 : var = &problem->variables[abs(*failed) - 1];
1055 : :
1056 : 8 : var->flags |= PKG_VAR_FAILED;
1057 : :
1058 : 8 : need_reiterate = true;
1059 : : }
1060 : :
1061 : : #if 0
1062 : : failed = picosat_next_maximal_satisfiable_subset_of_assumptions(problem->sat);
1063 : :
1064 : : while (*failed) {
1065 : : struct pkg_solve_variable *var = &problem->variables[*failed - 1];
1066 : :
1067 : : pkg_emit_notice("var: %s", var->uid);
1068 : :
1069 : : failed ++;
1070 : : }
1071 : :
1072 : : return (EPKG_AGAIN);
1073 : : #endif
1074 : 8 : }
1075 : : else {
1076 : :
1077 : : /* Assign vars */
1078 [ + + ]: 2099 : for (i = 0; i < problem->nvars; i ++) {
1079 : 1435 : int val = picosat_deref(problem->sat, i + 1);
1080 : 1435 : struct pkg_solve_variable *var = &problem->variables[i];
1081 : :
1082 [ + + ]: 1435 : if (val > 0)
1083 : 829 : var->flags |= PKG_VAR_INSTALL;
1084 : : else
1085 : 606 : var->flags &= ~PKG_VAR_INSTALL;
1086 : :
1087 : 1435 : pkg_debug(2, "decided %s %s-%s to %s",
1088 : 1435 : var->unit->pkg->type == PKG_INSTALLED ? "local" : "remote",
1089 : 1435 : var->uid, var->digest,
1090 : 1435 : var->flags & PKG_VAR_INSTALL ? "install" : "delete");
1091 : 1435 : }
1092 : :
1093 : : /* Check for reiterations */
1094 [ + + + + ]: 1000 : if ((problem->j->type == PKG_JOBS_INSTALL ||
1095 : 664 : problem->j->type == PKG_JOBS_UPGRADE) && iter == 0) {
1096 [ + + ]: 1585 : for (i = 0; i < problem->nvars; i ++) {
1097 : 1098 : bool failed_var = false;
1098 : 1098 : struct pkg_solve_variable *var = &problem->variables[i], *cur;
1099 : :
1100 [ + + ]: 1098 : if (!(var->flags & PKG_VAR_INSTALL)) {
1101 [ + + ]: 714 : LL_FOREACH(var, cur) {
1102 [ + + ]: 597 : if (cur->flags & PKG_VAR_INSTALL) {
1103 : 236 : failed_var = false;
1104 : 236 : break;
1105 : : }
1106 [ + + ]: 361 : else if (cur->unit->pkg->type == PKG_INSTALLED) {
1107 : 264 : failed_var = true;
1108 : 264 : }
1109 : 361 : }
1110 : 353 : }
1111 : :
1112 : : /*
1113 : : * If we want to delete local packages on installation, do one more SAT
1114 : : * iteration to ensure that we have no other choices
1115 : : */
1116 [ + + ]: 1098 : if (failed_var) {
1117 : 32 : pkg_debug (1, "trying to delete local package %s-%s on install/upgrade,"
1118 : : " reiterate on SAT",
1119 : 32 : var->unit->pkg->name, var->unit->pkg->version);
1120 : 32 : need_reiterate = true;
1121 : :
1122 [ + + ]: 68 : LL_FOREACH(var, cur) {
1123 : 36 : cur->flags |= PKG_VAR_FAILED;
1124 : 36 : }
1125 : 32 : }
1126 : 1098 : }
1127 : 487 : }
1128 : : }
1129 : :
1130 [ + + ]: 672 : if (need_reiterate) {
1131 : 32 : iter ++;
1132 : :
1133 : : /* Restore top-level assumptions */
1134 [ + + ]: 220 : for (i = 0; i < problem->nvars; i ++) {
1135 : 188 : struct pkg_solve_variable *var = &problem->variables[i];
1136 : :
1137 [ + + ]: 188 : if (var->flags & PKG_VAR_TOP) {
1138 [ + + ]: 60 : if (var->flags & PKG_VAR_FAILED) {
1139 : 8 : var->flags ^= PKG_VAR_INSTALL | PKG_VAR_FAILED;
1140 : 8 : }
1141 : :
1142 : 120 : picosat_assume(problem->sat, var->order *
1143 : 60 : (var->flags & PKG_VAR_INSTALL ? 1 : -1));
1144 : 60 : }
1145 : 188 : }
1146 : :
1147 : 32 : need_reiterate = false;
1148 : :
1149 : 32 : goto reiterate;
1150 : : }
1151 : :
1152 : 640 : return (EPKG_OK);
1153 : : }
1154 : :
1155 : : void
1156 : 0 : pkg_solve_dot_export(struct pkg_solve_problem *problem, FILE *file)
1157 : : {
1158 : : struct pkg_solve_rule *rule;
1159 : : size_t i;
1160 : :
1161 : 0 : fprintf(file, "digraph {\n");
1162 : :
1163 [ # # ]: 0 : for (i = 0; i < problem->nvars; i ++) {
1164 : 0 : struct pkg_solve_variable *var = &problem->variables[i];
1165 : :
1166 : 0 : fprintf(file, "\tp%d [shape=%s label=\"%s-%s\"]\n", var->order,
1167 : 0 : var->unit->pkg->type == PKG_INSTALLED ? "ellipse" : "octagon",
1168 : 0 : var->uid, var->unit->pkg->version);
1169 : 0 : }
1170 : :
1171 : : /* Print all variables as nodes */
1172 : :
1173 [ # # ]: 0 : for (i = 0; i < kv_size(problem->rules); i++) {
1174 : 0 : rule = kv_A(problem->rules, i);
1175 : 0 : struct pkg_solve_item *it = rule->items, *key_elt = NULL;
1176 : :
1177 [ # # # # ]: 0 : switch(rule->reason) {
1178 : : case PKG_RULE_DEPEND:
1179 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1180 [ # # ]: 0 : if (it->inverse == -1) {
1181 : 0 : key_elt = it;
1182 : 0 : break;
1183 : : }
1184 : 0 : }
1185 [ # # ]: 0 : assert (key_elt != NULL);
1186 : :
1187 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1188 [ # # ]: 0 : if (it != key_elt) {
1189 : 0 : fprintf(file, "\tp%d -> p%d;\n", key_elt->var->order,
1190 : 0 : it->var->order);
1191 : 0 : }
1192 : 0 : }
1193 : 0 : break;
1194 : : case PKG_RULE_UPGRADE_CONFLICT:
1195 : : case PKG_RULE_EXPLICIT_CONFLICT:
1196 : : case PKG_RULE_REQUEST_CONFLICT:
1197 : 0 : fprintf(file, "\tp%d -> p%d [arrowhead=none,color=red];\n",
1198 : 0 : it->var->order, it->next->var->order);
1199 : 0 : break;
1200 : : case PKG_RULE_REQUIRE:
1201 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1202 [ # # ]: 0 : if (it->inverse == -1) {
1203 : 0 : key_elt = it;
1204 : 0 : break;
1205 : : }
1206 : 0 : }
1207 [ # # ]: 0 : assert (key_elt != NULL);
1208 : :
1209 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1210 [ # # ]: 0 : if (it != key_elt) {
1211 : 0 : fprintf(file, "\tp%d -> p%d[arrowhead=diamond];\n", key_elt->var->order,
1212 : 0 : it->var->order);
1213 : 0 : }
1214 : 0 : }
1215 : 0 : break;
1216 : : default:
1217 : 0 : break;
1218 : : }
1219 : 0 : }
1220 : :
1221 : 0 : fprintf(file, "}\n");
1222 : 0 : }
1223 : :
1224 : : int
1225 : 0 : pkg_solve_dimacs_export(struct pkg_solve_problem *problem, FILE *f)
1226 : : {
1227 : : struct pkg_solve_rule *rule;
1228 : : struct pkg_solve_item *it;
1229 : :
1230 : 0 : fprintf(f, "p cnf %d %zu\n", (int)problem->nvars, kv_size(problem->rules));
1231 : :
1232 [ # # ]: 0 : for (unsigned int i = 0; i < kv_size(problem->rules); i++) {
1233 : 0 : rule = kv_A(problem->rules, i);
1234 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1235 : 0 : size_t order = it->var - problem->variables;
1236 [ # # ]: 0 : if (order < problem->nvars)
1237 : 0 : fprintf(f, "%ld ", (long)((order + 1) * it->inverse));
1238 : 0 : }
1239 : 0 : fprintf(f, "0\n");
1240 : 0 : }
1241 : 0 : return (EPKG_OK);
1242 : : }
1243 : :
1244 : : static void
1245 : 954 : pkg_solve_insert_res_job (struct pkg_solve_variable *var,
1246 : : struct pkg_solve_problem *problem)
1247 : : {
1248 : : struct pkg_solved *res;
1249 : 954 : struct pkg_solve_variable *cur_var, *del_var = NULL, *add_var = NULL;
1250 : 954 : int seen_add = 0, seen_del = 0;
1251 : 954 : struct pkg_jobs *j = problem->j;
1252 : :
1253 [ + + ]: 2245 : LL_FOREACH(var, cur_var) {
1254 [ + + + + ]: 1291 : if ((cur_var->flags & PKG_VAR_INSTALL) &&
1255 : 765 : cur_var->unit->pkg->type != PKG_INSTALLED) {
1256 : 691 : add_var = cur_var;
1257 : 691 : seen_add ++;
1258 : 691 : }
1259 [ + + ]: 600 : else if (!(cur_var->flags & PKG_VAR_INSTALL)
1260 [ + + ]: 600 : && cur_var->unit->pkg->type == PKG_INSTALLED) {
1261 : 433 : del_var = cur_var;
1262 : 433 : seen_del ++;
1263 : 433 : }
1264 : 1291 : }
1265 : :
1266 [ - + ]: 954 : if (seen_add > 1) {
1267 : 0 : pkg_emit_error("internal solver error: more than two packages to install(%d) "
1268 : 0 : "from the same uid: %s", seen_add, var->uid);
1269 : 0 : return;
1270 : : }
1271 [ + + + + ]: 954 : else if (seen_add != 0 || seen_del != 0) {
1272 [ + + ]: 880 : if (seen_add > 0) {
1273 : 691 : res = xcalloc(1, sizeof(struct pkg_solved));
1274 : : /* Pure install */
1275 [ + + ]: 691 : if (seen_del == 0) {
1276 : 447 : res->items[0] = add_var->unit;
1277 : 447 : res->type = (j->type == PKG_JOBS_FETCH) ?
1278 : : PKG_SOLVED_FETCH : PKG_SOLVED_INSTALL;
1279 [ + + ]: 447 : DL_APPEND(j->jobs, res);
1280 : 447 : pkg_debug(3, "pkg_solve: schedule installation of %s %s",
1281 : 447 : add_var->uid, add_var->digest);
1282 : 447 : }
1283 : : else {
1284 : : /* Upgrade */
1285 : 244 : res->items[0] = add_var->unit;
1286 : 244 : res->items[1] = del_var->unit;
1287 : 244 : res->type = PKG_SOLVED_UPGRADE;
1288 [ + + ]: 244 : DL_APPEND(j->jobs, res);
1289 : 244 : pkg_debug(3, "pkg_solve: schedule upgrade of %s from %s to %s",
1290 : 244 : del_var->uid, del_var->digest, add_var->digest);
1291 : : }
1292 : 691 : j->count ++;
1293 : 691 : }
1294 : :
1295 : : /*
1296 : : * For delete requests there could be multiple delete requests per UID,
1297 : : * so we need to re-process vars and add all delete jobs required.
1298 : : */
1299 [ + + ]: 2089 : LL_FOREACH(var, cur_var) {
1300 [ + + + + ]: 1209 : if (!(cur_var->flags & PKG_VAR_INSTALL) &&
1301 : 518 : cur_var->unit->pkg->type == PKG_INSTALLED) {
1302 : : /* Skip already added items */
1303 [ + + - + ]: 433 : if (seen_add > 0 && cur_var == del_var)
1304 : 244 : continue;
1305 : :
1306 : 189 : res = xcalloc(1, sizeof(struct pkg_solved));
1307 : 189 : res->items[0] = cur_var->unit;
1308 : 189 : res->type = PKG_SOLVED_DELETE;
1309 [ + + ]: 189 : DL_APPEND(j->jobs, res);
1310 : 189 : pkg_debug(3, "pkg_solve: schedule deletion of %s %s",
1311 : 189 : cur_var->uid, cur_var->digest);
1312 : 189 : j->count ++;
1313 : 189 : }
1314 : 965 : }
1315 : 880 : }
1316 : : else {
1317 : 74 : pkg_debug(2, "solver: ignoring package %s(%s) as its state has not been changed",
1318 : 74 : var->uid, var->digest);
1319 : : }
1320 : 954 : }
1321 : :
1322 : : int
1323 : 640 : pkg_solve_sat_to_jobs(struct pkg_solve_problem *problem)
1324 : : {
1325 : : struct pkg_solve_variable *var;
1326 : 640 : pkghash_it it = pkghash_iterator(problem->variables_by_uid);
1327 : :
1328 [ + + ]: 1594 : while (pkghash_next(&it)) {
1329 : 954 : var = (struct pkg_solve_variable *)it.value;
1330 : 954 : pkg_debug(4, "solver: check variable with uid %s", var->uid);
1331 : 954 : pkg_solve_insert_res_job(var, problem);
1332 : : }
1333 : :
1334 : 640 : return (EPKG_OK);
1335 : : }
1336 : :
1337 : : static bool
1338 : 0 : pkg_solve_parse_sat_output_store(struct pkg_solve_problem *problem, const char *var_str)
1339 : : {
1340 : : struct pkg_solve_variable *var;
1341 : : ssize_t order;
1342 : :
1343 : 0 : order = strtol(var_str, NULL, 10);
1344 [ # # ]: 0 : if (order == 0)
1345 : 0 : return (true);
1346 [ # # ]: 0 : if (order < 0) {
1347 : : /* negative value means false */
1348 : 0 : order = - order - 1;
1349 [ # # ]: 0 : if ((size_t)order < problem->nvars) {
1350 : 0 : var = problem->variables + order;
1351 : 0 : var->flags &= ~PKG_VAR_INSTALL;
1352 : 0 : }
1353 : 0 : } else {
1354 : : /* positive value means true */
1355 : 0 : order = order - 1;
1356 [ # # ]: 0 : if ((size_t)order < problem->nvars) {
1357 : 0 : var = problem->variables + order;
1358 : 0 : var->flags |= PKG_VAR_INSTALL;
1359 : 0 : }
1360 : : }
1361 : 0 : return (false);
1362 : 0 : }
1363 : :
1364 : : int
1365 : 0 : pkg_solve_parse_sat_output(FILE *f, struct pkg_solve_problem *problem)
1366 : : {
1367 : 0 : int ret = EPKG_OK;
1368 : 0 : char *line = NULL, *var_str, *begin;
1369 : 0 : size_t linecap = 0;
1370 : 0 : bool got_sat = false, done = false;
1371 : :
1372 [ # # ]: 0 : while (getline(&line, &linecap, f) > 0) {
1373 [ # # ]: 0 : if (strncmp(line, "SAT", 3) == 0) {
1374 : 0 : got_sat = true;
1375 : 0 : }
1376 [ # # ]: 0 : else if (got_sat) {
1377 : 0 : begin = line;
1378 : 0 : do {
1379 : 0 : var_str = strsep(&begin, " \t");
1380 : : /* Skip unexpected lines */
1381 [ # # # # : 0 : if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
# # ]
1382 : 0 : continue;
1383 [ # # ]: 0 : if (pkg_solve_parse_sat_output_store(problem, var_str))
1384 : 0 : done = true;
1385 [ # # ]: 0 : } while (begin != NULL);
1386 : 0 : }
1387 [ # # ]: 0 : else if (strncmp(line, "v ", 2) == 0) {
1388 : 0 : begin = line + 2;
1389 : 0 : do {
1390 : 0 : var_str = strsep(&begin, " \t");
1391 : : /* Skip unexpected lines */
1392 [ # # # # : 0 : if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
# # ]
1393 : 0 : continue;
1394 [ # # ]: 0 : if (pkg_solve_parse_sat_output_store(problem, var_str))
1395 : 0 : done = true;
1396 [ # # ]: 0 : } while (begin != NULL);
1397 : 0 : }
1398 : : else {
1399 : : /* Slightly ignore anything from solver */
1400 : 0 : continue;
1401 : : }
1402 : : }
1403 : :
1404 [ # # ]: 0 : if (done)
1405 : 0 : ret = pkg_solve_sat_to_jobs(problem);
1406 : : else {
1407 : 0 : pkg_emit_error("cannot parse sat solver output");
1408 : 0 : ret = EPKG_FATAL;
1409 : : }
1410 : :
1411 : 0 : free(line);
1412 : :
1413 : 0 : return (ret);
1414 : : }
|
