LCOV - code coverage report
Current view: top level - libpkg - pkg_solve.c (source / functions) Hit Total Coverage
Test: cov.info Lines: 414 655 63.2 %
Date: 2015-08-15 Functions: 21 24 87.5 %

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

Generated by: LCOV version 1.10