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