Solver.php 68 KB

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366136713681369137013711372137313741375137613771378137913801381138213831384138513861387138813891390139113921393139413951396139713981399140014011402140314041405140614071408140914101411141214131414141514161417141814191420142114221423142414251426142714281429143014311432143314341435143614371438143914401441144214431444144514461447144814491450145114521453145414551456145714581459146014611462146314641465146614671468146914701471147214731474147514761477147814791480148114821483148414851486148714881489149014911492149314941495149614971498149915001501150215031504150515061507150815091510151115121513151415151516151715181519152015211522152315241525152615271528152915301531153215331534153515361537153815391540154115421543154415451546154715481549155015511552155315541555155615571558155915601561156215631564156515661567156815691570157115721573157415751576157715781579158015811582158315841585158615871588158915901591159215931594159515961597159815991600160116021603160416051606160716081609161016111612161316141615161616171618161916201621162216231624162516261627162816291630163116321633163416351636163716381639164016411642164316441645164616471648164916501651165216531654165516561657165816591660166116621663166416651666166716681669167016711672167316741675167616771678167916801681168216831684168516861687168816891690169116921693169416951696169716981699170017011702170317041705170617071708170917101711171217131714171517161717171817191720172117221723172417251726172717281729173017311732173317341735173617371738173917401741174217431744174517461747174817491750175117521753175417551756175717581759176017611762176317641765176617671768176917701771177217731774177517761777177817791780178117821783178417851786178717881789179017911792179317941795179617971798179918001801180218031804180518061807180818091810181118121813181418151816181718181819182018211822182318241825182618271828182918301831183218331834183518361837183818391840184118421843184418451846184718481849185018511852185318541855185618571858185918601861186218631864186518661867186818691870187118721873187418751876187718781879188018811882188318841885188618871888188918901891189218931894189518961897189818991900190119021903190419051906190719081909191019111912191319141915191619171918191919201921192219231924192519261927192819291930193119321933193419351936193719381939194019411942194319441945194619471948194919501951195219531954195519561957195819591960196119621963196419651966196719681969197019711972197319741975197619771978197919801981198219831984198519861987198819891990199119921993199419951996199719981999200020012002200320042005200620072008200920102011201220132014201520162017201820192020
  1. <?php
  2. /*
  3. * This file is part of Composer.
  4. *
  5. * (c) Nils Adermann <naderman@naderman.de>
  6. * Jordi Boggiano <j.boggiano@seld.be>
  7. *
  8. * For the full copyright and license information, please view the LICENSE
  9. * file that was distributed with this source code.
  10. */
  11. namespace Composer\DependencyResolver;
  12. use Composer\Repository\RepositoryInterface;
  13. use Composer\Package\PackageInterface;
  14. use Composer\DependencyResolver\Operation;
  15. /**
  16. * @author Nils Adermann <naderman@naderman.de>
  17. */
  18. class Solver
  19. {
  20. protected $policy;
  21. protected $pool;
  22. protected $installed;
  23. protected $rules;
  24. protected $updateAll;
  25. protected $ruleToJob = array();
  26. protected $addedMap = array();
  27. protected $updateMap = array();
  28. protected $noObsoletes = array();
  29. protected $watches = array();
  30. protected $removeWatches = array();
  31. protected $decisionMap;
  32. protected $installedMap;
  33. protected $packageToFeatureRule = array();
  34. public function __construct(PolicyInterface $policy, Pool $pool, RepositoryInterface $installed)
  35. {
  36. $this->policy = $policy;
  37. $this->pool = $pool;
  38. $this->installed = $installed;
  39. $this->rules = new RuleSet;
  40. }
  41. /**
  42. * Creates a new rule for the requirements of a package
  43. *
  44. * This rule is of the form (-A|B|C), where B and C are the providers of
  45. * one requirement of the package A.
  46. *
  47. * @param PackageInterface $package The package with a requirement
  48. * @param array $providers The providers of the requirement
  49. * @param int $reason A RULE_* constant describing the
  50. * reason for generating this rule
  51. * @param mixed $reasonData Any data, e.g. the requirement name,
  52. * that goes with the reason
  53. * @return Rule The generated rule or null if tautological
  54. */
  55. protected function createRequireRule(PackageInterface $package, array $providers, $reason, $reasonData = null)
  56. {
  57. $literals = array(new Literal($package, false));
  58. foreach ($providers as $provider) {
  59. // self fulfilling rule?
  60. if ($provider === $package) {
  61. return null;
  62. }
  63. $literals[] = new Literal($provider, true);
  64. }
  65. return new Rule($literals, $reason, $reasonData);
  66. }
  67. /**
  68. * Create a new rule for updating a package
  69. *
  70. * If package A1 can be updated to A2 or A3 the rule is (A1|A2|A3).
  71. *
  72. * @param PackageInterface $package The package to be updated
  73. * @param array $updates An array of update candidate packages
  74. * @param int $reason A RULE_* constant describing the
  75. * reason for generating this rule
  76. * @param mixed $reasonData Any data, e.g. the package name, that
  77. * goes with the reason
  78. * @return Rule The generated rule or null if tautology
  79. */
  80. protected function createUpdateRule(PackageInterface $package, array $updates, $reason, $reasonData = null)
  81. {
  82. $literals = array(new Literal($package, true));
  83. foreach ($updates as $update) {
  84. $literals[] = new Literal($update, true);
  85. }
  86. return new Rule($literals, $reason, $reasonData);
  87. }
  88. /**
  89. * Creates a new rule for installing a package
  90. *
  91. * The rule is simply (A) for a package A to be installed.
  92. *
  93. * @param PackageInterface $package The package to be installed
  94. * @param int $reason A RULE_* constant describing the
  95. * reason for generating this rule
  96. * @param mixed $reasonData Any data, e.g. the package name, that
  97. * goes with the reason
  98. * @return Rule The generated rule
  99. */
  100. protected function createInstallRule(PackageInterface $package, $reason, $reasonData = null)
  101. {
  102. return new Rule(new Literal($package, true));
  103. }
  104. /**
  105. * Creates a rule to install at least one of a set of packages
  106. *
  107. * The rule is (A|B|C) with A, B and C different packages. If the given
  108. * set of packages is empty an impossible rule is generated.
  109. *
  110. * @param array $packages The set of packages to choose from
  111. * @param int $reason A RULE_* constant describing the reason for
  112. * generating this rule
  113. * @param mixed $reasonData Any data, e.g. the package name, that goes with
  114. * the reason
  115. * @return Rule The generated rule
  116. */
  117. protected function createInstallOneOfRule(array $packages, $reason, $reasonData = null)
  118. {
  119. $literals = array();
  120. foreach ($packages as $package) {
  121. $literals[] = new Literal($package, true);
  122. }
  123. return new Rule($literals, $reason, $reasonData);
  124. }
  125. /**
  126. * Creates a rule to remove a package
  127. *
  128. * The rule for a package A is (-A).
  129. *
  130. * @param PackageInterface $package The package to be removed
  131. * @param int $reason A RULE_* constant describing the
  132. * reason for generating this rule
  133. * @param mixed $reasonData Any data, e.g. the package name, that
  134. * goes with the reason
  135. * @return Rule The generated rule
  136. */
  137. protected function createRemoveRule(PackageInterface $package, $reason, $reasonData = null)
  138. {
  139. return new Rule(array(new Literal($package, false)), $reason, $reasonData);
  140. }
  141. /**
  142. * Creates a rule for two conflicting packages
  143. *
  144. * The rule for conflicting packages A and B is (-A|-B). A is called the issuer
  145. * and B the provider.
  146. *
  147. * @param PackageInterface $issuer The package declaring the conflict
  148. * @param Package $provider The package causing the conflict
  149. * @param int $reason A RULE_* constant describing the
  150. * reason for generating this rule
  151. * @param mixed $reasonData Any data, e.g. the package name, that
  152. * goes with the reason
  153. * @return Rule The generated rule
  154. */
  155. protected function createConflictRule(PackageInterface $issuer, PackageInterface $provider, $reason, $reasonData = null)
  156. {
  157. // ignore self conflict
  158. if ($issuer === $provider) {
  159. return null;
  160. }
  161. return new Rule(array(new Literal($issuer, false), new Literal($provider, false)), $reason, $reasonData);
  162. }
  163. /**
  164. * Adds a rule unless it duplicates an existing one of any type
  165. *
  166. * To be able to directly pass in the result of one of the rule creation
  167. * methods the rule may also be null to indicate that no rule should be
  168. * added.
  169. *
  170. * @param int $type A TYPE_* constant defining the rule type
  171. * @param Rule $newRule The rule about to be added
  172. */
  173. private function addRule($type, Rule $newRule = null) {
  174. if ($newRule) {
  175. if ($this->rules->containsEqual($newRule)) {
  176. return;
  177. }
  178. $this->rules->add($newRule, $type);
  179. }
  180. }
  181. protected function addRulesForPackage(PackageInterface $package)
  182. {
  183. $workQueue = new \SplQueue;
  184. $workQueue->enqueue($package);
  185. while (!$workQueue->isEmpty()) {
  186. $package = $workQueue->dequeue();
  187. if (isset($this->addedMap[$package->getId()])) {
  188. continue;
  189. }
  190. $this->addedMap[$package->getId()] = true;
  191. if (!$this->policy->installable($this, $this->pool, $this->installedMap, $package)) {
  192. $this->addRule(RuleSet::TYPE_PACKAGE, $this->createRemoveRule($package, Rule::RULE_NOT_INSTALLABLE, (string) $package));
  193. continue;
  194. }
  195. foreach ($package->getRequires() as $link) {
  196. $possibleRequires = $this->pool->whatProvides($link->getTarget(), $link->getConstraint());
  197. $this->addRule(RuleSet::TYPE_PACKAGE, $rule = $this->createRequireRule($package, $possibleRequires, Rule::RULE_PACKAGE_REQUIRES, (string) $link));
  198. foreach ($possibleRequires as $require) {
  199. $workQueue->enqueue($require);
  200. }
  201. }
  202. foreach ($package->getConflicts() as $link) {
  203. $possibleConflicts = $this->pool->whatProvides($link->getTarget(), $link->getConstraint());
  204. foreach ($possibleConflicts as $conflict) {
  205. $this->addRule(RuleSet::TYPE_PACKAGE, $this->createConflictRule($package, $conflict, Rule::RULE_PACKAGE_CONFLICT, (string) $link));
  206. }
  207. }
  208. // check obsoletes and implicit obsoletes of a package
  209. // if ignoreinstalledsobsoletes is not set, we're also checking
  210. // obsoletes of installed packages (like newer rpm versions)
  211. //
  212. /** TODO if ($this->noInstalledObsoletes) */
  213. if (true) {
  214. $noObsoletes = isset($this->noObsoletes[$package->getId()]);
  215. $isInstalled = (isset($this->installedMap[$package->getId()]));
  216. foreach ($package->getReplaces() as $link) {
  217. $obsoleteProviders = $this->pool->whatProvides($link->getTarget(), $link->getConstraint());
  218. foreach ($obsoleteProviders as $provider) {
  219. if ($provider === $package) {
  220. continue;
  221. }
  222. $reason = ($isInstalled) ? Rule::RULE_INSTALLED_PACKAGE_OBSOLETES : Rule::RULE_PACKAGE_OBSOLETES;
  223. $this->addRule(RuleSet::TYPE_PACKAGE, $this->createConflictRule($package, $provider, $reason, (string) $link));
  224. }
  225. }
  226. // check implicit obsoletes
  227. // for installed packages we only need to check installed/installed problems,
  228. // as the others are picked up when looking at the uninstalled package.
  229. if (!$isInstalled) {
  230. $obsoleteProviders = $this->pool->whatProvides($package->getName(), null);
  231. foreach ($obsoleteProviders as $provider) {
  232. if ($provider === $package) {
  233. continue;
  234. }
  235. if ($isInstalled && !isset($this->installedMap[$provider->getId()])) {
  236. continue;
  237. }
  238. // obsolete same packages even when noObsoletes
  239. if ($noObsoletes && (!$package->equals($provider))) {
  240. continue;
  241. }
  242. $reason = ($package->getName() == $provider->getName()) ? Rule::RULE_PACKAGE_SAME_NAME : Rule::RULE_PACKAGE_IMPLICIT_OBSOLETES;
  243. $this->addRule(RuleSet::TYPE_PACKAGE, $rule = $this->createConflictRule($package, $provider, $reason, (string) $package));
  244. }
  245. }
  246. }
  247. }
  248. }
  249. /**
  250. * Adds all rules for all update packages of a given package
  251. *
  252. * @param PackageInterface $package Rules for this package's updates are to
  253. * be added
  254. * @param bool $allowAll Whether downgrades are allowed
  255. */
  256. private function addRulesForUpdatePackages(PackageInterface $package)
  257. {
  258. $updates = $this->policy->findUpdatePackages($this, $this->pool, $this->installedMap, $package);
  259. $this->addRulesForPackage($package);
  260. foreach ($updates as $update) {
  261. $this->addRulesForPackage($update);
  262. }
  263. }
  264. /**
  265. * Alters watch chains for a rule.
  266. *
  267. * Next1/2 always points to the next rule that is watching the same package.
  268. * The watches array contains rules to start from for each package
  269. *
  270. */
  271. private function addWatchesToRule(Rule $rule)
  272. {
  273. // skip simple assertions of the form (A) or (-A)
  274. if ($rule->isAssertion()) {
  275. return;
  276. }
  277. if (!isset($this->watches[$rule->watch1])) {
  278. $this->watches[$rule->watch1] = null;
  279. }
  280. $rule->next1 = $this->watches[$rule->watch1];
  281. $this->watches[$rule->watch1] = $rule;
  282. if (!isset($this->watches[$rule->watch2])) {
  283. $this->watches[$rule->watch2] = null;
  284. }
  285. $rule->next2 = $this->watches[$rule->watch2];
  286. $this->watches[$rule->watch2] = $rule;
  287. }
  288. /**
  289. * Put watch2 on rule's literal with highest level
  290. */
  291. private function watch2OnHighest(Rule $rule)
  292. {
  293. $literals = $rule->getLiterals();
  294. // if there are only 2 elements, both are being watched anyway
  295. if ($literals < 3) {
  296. return;
  297. }
  298. $watchLevel = 0;
  299. foreach ($literals as $literal) {
  300. $level = abs($this->decisionMap[$literal->getPackageId()]);
  301. if ($level > $watchLevel) {
  302. $rule->watch2 = $literal->getId();
  303. $watchLevel = $level;
  304. }
  305. }
  306. }
  307. private function findDecisionRule(PackageInterface $package)
  308. {
  309. foreach ($this->decisionQueue as $i => $literal) {
  310. if ($package === $literal->getPackage()) {
  311. return $this->decisionQueueWhy[$i];
  312. }
  313. }
  314. return null;
  315. }
  316. // aka solver_makeruledecisions
  317. private function makeAssertionRuleDecisions()
  318. {
  319. // do we need to decide a SYSTEMSOLVABLE at level 1?
  320. $decisionStart = count($this->decisionQueue);
  321. for ($ruleIndex = 0; $ruleIndex < count($this->rules); $ruleIndex++) {
  322. $rule = $this->rules->ruleById($ruleIndex);
  323. if ($rule->isWeak() || !$rule->isAssertion() || $rule->isDisabled()) {
  324. continue;
  325. }
  326. $literals = $rule->getLiterals();
  327. $literal = $literals[0];
  328. if (!$this->decided($literal->getPackage())) {
  329. $this->decisionQueue[] = $literal;
  330. $this->decisionQueueWhy[] = $rule;
  331. $this->addDecision($literal, 1);
  332. continue;
  333. }
  334. if ($this->decisionsSatisfy($literal)) {
  335. continue;
  336. }
  337. // found a conflict
  338. if (RuleSet::TYPE_LEARNED === $rule->getType()) {
  339. $rule->disable();
  340. continue;
  341. }
  342. $conflict = $this->findDecisionRule($literal->getPackage());
  343. /** TODO: handle conflict with systemsolvable? */
  344. if ($conflict && RuleSet::TYPE_PACKAGE === $conflict->getType()) {
  345. $problem = new Problem;
  346. if ($rule->getType() == RuleSet::TYPE_JOB) {
  347. $job = $this->ruleToJob[$rule->getId()];
  348. $problem->addJobRule($job, $rule);
  349. $problem->addRule($conflict);
  350. $this->disableProblem($job);
  351. } else {
  352. $problem->addRule($rule);
  353. $problem->addRule($conflict);
  354. $this->disableProblem($rule);
  355. }
  356. $this->problems[] = $problem;
  357. continue;
  358. }
  359. // conflict with another job or update/feature rule
  360. $problem = new Problem;
  361. $problem->addRule($rule);
  362. $problem->addRule($conflict);
  363. // push all of our rules (can only be feature or job rules)
  364. // asserting this literal on the problem stack
  365. foreach ($this->rules->getIteratorFor(array(RuleSet::TYPE_JOB, RuleSet::TYPE_FEATURE)) as $assertRule) {
  366. if ($assertRule->isDisabled() || !$assertRule->isAssertion() || $assertRule->isWeak()) {
  367. continue;
  368. }
  369. $assertRuleLiterals = $assertRule->getLiterals();
  370. $assertRuleLiteral = $assertRuleLiterals[0];
  371. if ($literal->getPackageId() !== $assertRuleLiteral->getPackageId()) {
  372. continue;
  373. }
  374. if ($assertRule->getType() === RuleSet::TYPE_JOB) {
  375. $job = $this->ruleToJob[$assertRule->getId()];
  376. $problem->addJobRule($job, $assertRule);
  377. $this->disableProblem($job);
  378. } else {
  379. $problem->addRule($assertRule);
  380. $this->disableProblem($assertRule);
  381. }
  382. }
  383. $this->problems[] = $problem;
  384. // start over
  385. while (count($this->decisionQueue) > $decisionStart) {
  386. $decisionLiteral = array_pop($this->decisionQueue);
  387. array_pop($this->decisionQueueWhy);
  388. unset($this->decisionQueueFree[count($this->decisionQueue)]);
  389. $this->decisionMap[$decisionLiteral->getPackageId()] = 0;
  390. }
  391. $ruleIndex = -1;
  392. }
  393. foreach ($this->rules as $rule) {
  394. if (!$rule->isWeak() || !$rule->isAssertion() || $rule->isDisabled()) {
  395. continue;
  396. }
  397. $literals = $rule->getLiterals();
  398. $literal = $literals[0];
  399. if ($this->decisionMap[$literal->getPackageId()] == 0) {
  400. $this->decisionQueue[] = $literal;
  401. $this->decisionQueueWhy[] = $rule;
  402. $this->addDecision($literal, 1);
  403. continue;
  404. }
  405. if ($this->decisionsSatisfy($literals[0])) {
  406. continue;
  407. }
  408. // conflict, but this is a weak rule => disable
  409. if ($rule->getType() == RuleSet::TYPE_JOB) {
  410. $why = $this->ruleToJob[$rule->getId()];
  411. } else {
  412. $why = $rule;
  413. }
  414. $this->disableProblem($why);
  415. /** TODO solver_reenablepolicyrules(solv, -(v + 1)); */
  416. }
  417. }
  418. protected function addChoiceRules()
  419. {
  420. // void
  421. // solver_addchoicerules(Solver *solv)
  422. // {
  423. // Pool *pool = solv->pool;
  424. // Map m, mneg;
  425. // Rule *r;
  426. // Queue q, qi;
  427. // int i, j, rid, havechoice;
  428. // Id p, d, *pp;
  429. // Id p2, pp2;
  430. // Solvable *s, *s2;
  431. //
  432. // solv->choicerules = solv->nrules;
  433. // if (!pool->installed)
  434. // {
  435. // solv->choicerules_end = solv->nrules;
  436. // return;
  437. // }
  438. // solv->choicerules_ref = sat_calloc(solv->rpmrules_end, sizeof(Id));
  439. // queue_init(&q);
  440. // queue_init(&qi);
  441. // map_init(&m, pool->nsolvables);
  442. // map_init(&mneg, pool->nsolvables);
  443. // /* set up negative assertion map from infarch and dup rules */
  444. // for (rid = solv->infarchrules, r = solv->rules + rid; rid < solv->infarchrules_end; rid++, r++)
  445. // if (r->p < 0 && !r->w2 && (r->d == 0 || r->d == -1))
  446. // MAPSET(&mneg, -r->p);
  447. // for (rid = solv->duprules, r = solv->rules + rid; rid < solv->duprules_end; rid++, r++)
  448. // if (r->p < 0 && !r->w2 && (r->d == 0 || r->d == -1))
  449. // MAPSET(&mneg, -r->p);
  450. // for (rid = 1; rid < solv->rpmrules_end ; rid++)
  451. // {
  452. // r = solv->rules + rid;
  453. // if (r->p >= 0 || ((r->d == 0 || r->d == -1) && r->w2 < 0))
  454. // continue; /* only look at requires rules */
  455. // // solver_printrule(solv, SAT_DEBUG_RESULT, r);
  456. // queue_empty(&q);
  457. // queue_empty(&qi);
  458. // havechoice = 0;
  459. // FOR_RULELITERALS(p, pp, r)
  460. // {
  461. // if (p < 0)
  462. // continue;
  463. // s = pool->solvables + p;
  464. // if (!s->repo)
  465. // continue;
  466. // if (s->repo == pool->installed)
  467. // {
  468. // queue_push(&q, p);
  469. // continue;
  470. // }
  471. // /* check if this package is "blocked" by a installed package */
  472. // s2 = 0;
  473. // FOR_PROVIDES(p2, pp2, s->name)
  474. // {
  475. // s2 = pool->solvables + p2;
  476. // if (s2->repo != pool->installed)
  477. // continue;
  478. // if (!pool->implicitobsoleteusesprovides && s->name != s2->name)
  479. // continue;
  480. // if (pool->obsoleteusescolors && !pool_colormatch(pool, s, s2))
  481. // continue;
  482. // break;
  483. // }
  484. // if (p2)
  485. // {
  486. // /* found installed package p2 that we can update to p */
  487. // if (MAPTST(&mneg, p))
  488. // continue;
  489. // if (policy_is_illegal(solv, s2, s, 0))
  490. // continue;
  491. // queue_push(&qi, p2);
  492. // queue_push(&q, p);
  493. // continue;
  494. // }
  495. // if (s->obsoletes)
  496. // {
  497. // Id obs, *obsp = s->repo->idarraydata + s->obsoletes;
  498. // s2 = 0;
  499. // while ((obs = *obsp++) != 0)
  500. // {
  501. // FOR_PROVIDES(p2, pp2, obs)
  502. // {
  503. // s2 = pool->solvables + p2;
  504. // if (s2->repo != pool->installed)
  505. // continue;
  506. // if (!pool->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p2, obs))
  507. // continue;
  508. // if (pool->obsoleteusescolors && !pool_colormatch(pool, s, s2))
  509. // continue;
  510. // break;
  511. // }
  512. // if (p2)
  513. // break;
  514. // }
  515. // if (obs)
  516. // {
  517. // /* found installed package p2 that we can update to p */
  518. // if (MAPTST(&mneg, p))
  519. // continue;
  520. // if (policy_is_illegal(solv, s2, s, 0))
  521. // continue;
  522. // queue_push(&qi, p2);
  523. // queue_push(&q, p);
  524. // continue;
  525. // }
  526. // }
  527. // /* package p is independent of the installed ones */
  528. // havechoice = 1;
  529. // }
  530. // if (!havechoice || !q.count)
  531. // continue; /* no choice */
  532. //
  533. // /* now check the update rules of the installed package.
  534. // * if all packages of the update rules are contained in
  535. // * the dependency rules, there's no need to set up the choice rule */
  536. // map_empty(&m);
  537. // FOR_RULELITERALS(p, pp, r)
  538. // if (p > 0)
  539. // MAPSET(&m, p);
  540. // for (i = 0; i < qi.count; i++)
  541. // {
  542. // if (!qi.elements[i])
  543. // continue;
  544. // Rule *ur = solv->rules + solv->updaterules + (qi.elements[i] - pool->installed->start);
  545. // if (!ur->p)
  546. // ur = solv->rules + solv->featurerules + (qi.elements[i] - pool->installed->start);
  547. // if (!ur->p)
  548. // continue;
  549. // FOR_RULELITERALS(p, pp, ur)
  550. // if (!MAPTST(&m, p))
  551. // break;
  552. // if (p)
  553. // break;
  554. // for (j = i + 1; j < qi.count; j++)
  555. // if (qi.elements[i] == qi.elements[j])
  556. // qi.elements[j] = 0;
  557. // }
  558. // if (i == qi.count)
  559. // {
  560. // #if 0
  561. // printf("skipping choice ");
  562. // solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + rid);
  563. // #endif
  564. // continue;
  565. // }
  566. // d = q.count ? pool_queuetowhatprovides(pool, &q) : 0;
  567. // solver_addrule(solv, r->p, d);
  568. // queue_push(&solv->weakruleq, solv->nrules - 1);
  569. // solv->choicerules_ref[solv->nrules - 1 - solv->choicerules] = rid;
  570. // #if 0
  571. // printf("OLD ");
  572. // solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + rid);
  573. // printf("WEAK CHOICE ");
  574. // solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + solv->nrules - 1);
  575. // #endif
  576. // }
  577. // queue_free(&q);
  578. // queue_free(&qi);
  579. // map_free(&m);
  580. // map_free(&mneg);
  581. // solv->choicerules_end = solv->nrules;
  582. // }
  583. }
  584. /***********************************************************************
  585. ***
  586. *** Policy rule disabling/reenabling
  587. ***
  588. *** Disable all policy rules that conflict with our jobs. If a job
  589. *** gets disabled later on, reenable the involved policy rules again.
  590. ***
  591. *** /
  592. #define DISABLE_UPDATE 1
  593. #define DISABLE_INFARCH 2
  594. #define DISABLE_DUP 3
  595. */
  596. protected function jobToDisableQueue(array $job, array $disableQueue)
  597. {
  598. switch ($job['cmd']) {
  599. case 'install':
  600. foreach ($job['packages'] as $package) {
  601. if (isset($this->installedMap[$package->getId()])) {
  602. $disableQueue[] = array('type' => 'update', 'package' => $package);
  603. }
  604. /* all job packages obsolete * /
  605. qstart = q->count;
  606. pass = 0;
  607. memset(&omap, 0, sizeof(omap));
  608. FOR_JOB_SELECT(p, pp, select, what)
  609. {
  610. Id p2, pp2;
  611. if (pass == 1)
  612. map_grow(&omap, installed->end - installed->start);
  613. s = pool->solvables + p;
  614. if (s->obsoletes)
  615. {
  616. Id obs, *obsp;
  617. obsp = s->repo->idarraydata + s->obsoletes;
  618. while ((obs = *obsp++) != 0)
  619. FOR_PROVIDES(p2, pp2, obs)
  620. {
  621. Solvable *ps = pool->solvables + p2;
  622. if (ps->repo != installed)
  623. continue;
  624. if (!pool->obsoleteusesprovides && !pool_match_nevr(pool, ps, obs))
  625. continue;
  626. if (pool->obsoleteusescolors && !pool_colormatch(pool, s, ps))
  627. continue;
  628. if (pass)
  629. MAPSET(&omap, p2 - installed->start);
  630. else
  631. queue_push2(q, DISABLE_UPDATE, p2);
  632. }
  633. }
  634. FOR_PROVIDES(p2, pp2, s->name)
  635. {
  636. Solvable *ps = pool->solvables + p2;
  637. if (ps->repo != installed)
  638. continue;
  639. if (!pool->implicitobsoleteusesprovides && ps->name != s->name)
  640. continue;
  641. if (pool->obsoleteusescolors && !pool_colormatch(pool, s, ps))
  642. continue;
  643. if (pass)
  644. MAPSET(&omap, p2 - installed->start);
  645. else
  646. queue_push2(q, DISABLE_UPDATE, p2);
  647. }
  648. if (pass)
  649. {
  650. for (i = j = qstart; i < q->count; i += 2)
  651. {
  652. if (MAPTST(&omap, q->elements[i + 1] - installed->start))
  653. {
  654. MAPCLR(&omap, q->elements[i + 1] - installed->start);
  655. q->elements[j + 1] = q->elements[i + 1];
  656. j += 2;
  657. }
  658. }
  659. queue_truncate(q, j);
  660. }
  661. if (q->count == qstart)
  662. break;
  663. pass++;
  664. }
  665. if (omap.size)
  666. map_free(&omap);
  667. if (qstart == q->count)
  668. return; /* nothing to prune * /
  669. if ((set & (SOLVER_SETEVR | SOLVER_SETARCH | SOLVER_SETVENDOR)) == (SOLVER_SETEVR | SOLVER_SETARCH | SOLVER_SETVENDOR))
  670. return; /* all is set */
  671. /* now that we know which installed packages are obsoleted check each of them * /
  672. for (i = j = qstart; i < q->count; i += 2)
  673. {
  674. Solvable *is = pool->solvables + q->elements[i + 1];
  675. FOR_JOB_SELECT(p, pp, select, what)
  676. {
  677. int illegal = 0;
  678. s = pool->solvables + p;
  679. if ((set & SOLVER_SETEVR) != 0)
  680. illegal |= POLICY_ILLEGAL_DOWNGRADE; /* ignore * /
  681. if ((set & SOLVER_SETARCH) != 0)
  682. illegal |= POLICY_ILLEGAL_ARCHCHANGE; /* ignore * /
  683. if ((set & SOLVER_SETVENDOR) != 0)
  684. illegal |= POLICY_ILLEGAL_VENDORCHANGE; /* ignore * /
  685. illegal = policy_is_illegal(solv, is, s, illegal);
  686. if (illegal && illegal == POLICY_ILLEGAL_DOWNGRADE && (set & SOLVER_SETEV) != 0)
  687. {
  688. /* it's ok if the EV is different * /
  689. if (evrcmp(pool, is->evr, s->evr, EVRCMP_COMPARE_EVONLY) != 0)
  690. illegal = 0;
  691. }
  692. if (illegal)
  693. break;
  694. }
  695. if (!p)
  696. {
  697. /* no package conflicts with the update rule * /
  698. /* thus keep the DISABLE_UPDATE * /
  699. q->elements[j + 1] = q->elements[i + 1];
  700. j += 2;
  701. }
  702. }
  703. queue_truncate(q, j);
  704. return;*/
  705. }
  706. break;
  707. case 'remove':
  708. foreach ($job['packages'] as $package) {
  709. if (isset($this->installedMap[$package->getId()])) {
  710. $disableQueue[] = array('type' => 'update', 'package' => $package);
  711. }
  712. }
  713. break;
  714. }
  715. return $disableQueue;
  716. }
  717. protected function disableUpdateRule($package)
  718. {
  719. if (isset($this->packageToFeatureRule[$package->getId()])) {
  720. $this->packageToFeatureRule[$package->getId()]->disable();
  721. }
  722. }
  723. /**
  724. * Disables all policy rules that conflict with jobs
  725. */
  726. protected function disablePolicyRules()
  727. {
  728. $lastJob = null;
  729. $allQueue = array();
  730. $iterator = $this->rules->getIteratorFor(RuleSet::TYPE_JOB);
  731. foreach ($iterator as $rule) {
  732. if ($rule->isDisabled()) {
  733. continue;
  734. }
  735. $job = $this->ruleToJob[$rule->getId()];
  736. if ($job === $lastJob) {
  737. continue;
  738. }
  739. $lastJob = $job;
  740. $allQueue = $this->jobToDisableQueue($job, $allQueue);
  741. }
  742. foreach ($allQueue as $disable) {
  743. switch ($disable['type']) {
  744. case 'update':
  745. $this->disableUpdateRule($disable['package']);
  746. break;
  747. default:
  748. throw new \RuntimeException("Unsupported disable type: " . $disable['type']);
  749. }
  750. }
  751. }
  752. public function solve(Request $request)
  753. {
  754. $this->jobs = $request->getJobs();
  755. $installedPackages = $this->installed->getPackages();
  756. $this->installedMap = array();
  757. foreach ($installedPackages as $package) {
  758. $this->installedMap[$package->getId()] = $package;
  759. }
  760. if (version_compare(PHP_VERSION, '5.3.4', '>=')) {
  761. $this->decisionMap = new \SplFixedArray($this->pool->getMaxId() + 1);
  762. } else {
  763. $this->decisionMap = array_fill(0, $this->pool->getMaxId() + 1, 0);
  764. }
  765. foreach ($this->jobs as $job) {
  766. foreach ($job['packages'] as $package) {
  767. switch ($job['cmd']) {
  768. case 'update':
  769. if (isset($this->installedMap[$package->getId()])) {
  770. $this->updateMap[$package->getId()] = true;
  771. }
  772. break;
  773. }
  774. }
  775. switch ($job['cmd']) {
  776. case 'update-all':
  777. foreach ($installedPackages as $package) {
  778. $this->updateMap[$package->getId()] = true;
  779. }
  780. break;
  781. }
  782. }
  783. foreach ($installedPackages as $package) {
  784. $this->addRulesForPackage($package);
  785. }
  786. foreach ($installedPackages as $package) {
  787. $this->addRulesForUpdatePackages($package);
  788. }
  789. foreach ($this->jobs as $job) {
  790. foreach ($job['packages'] as $package) {
  791. switch ($job['cmd']) {
  792. case 'install':
  793. $this->installCandidateMap[$package->getId()] = true;
  794. $this->addRulesForPackage($package);
  795. break;
  796. }
  797. }
  798. }
  799. // solver_addrpmrulesforweak(solv, &addedmap);
  800. foreach ($installedPackages as $package) {
  801. $updates = $this->policy->findUpdatePackages($this, $this->pool, $this->installedMap, $package);
  802. $rule = $this->createUpdateRule($package, $updates, Rule::RULE_INTERNAL_ALLOW_UPDATE, (string) $package);
  803. $rule->setWeak(true);
  804. $this->addRule(RuleSet::TYPE_FEATURE, $rule);
  805. $this->packageToFeatureRule[$package->getId()] = $rule;
  806. }
  807. foreach ($this->jobs as $job) {
  808. switch ($job['cmd']) {
  809. case 'install':
  810. if (empty($job['packages'])) {
  811. $problem = new Problem();
  812. $problem->addJobRule($job);
  813. $this->problems[] = $problem;
  814. } else {
  815. $rule = $this->createInstallOneOfRule($job['packages'], Rule::RULE_JOB_INSTALL, $job['packageName']);
  816. $this->addRule(RuleSet::TYPE_JOB, $rule);
  817. $this->ruleToJob[$rule->getId()] = $job;
  818. }
  819. break;
  820. case 'remove':
  821. // remove all packages with this name including uninstalled
  822. // ones to make sure none of them are picked as replacements
  823. // todo: cleandeps
  824. foreach ($job['packages'] as $package) {
  825. $rule = $this->createRemoveRule($package, Rule::RULE_JOB_REMOVE);
  826. $this->addRule(RuleSet::TYPE_JOB, $rule);
  827. $this->ruleToJob[$rule->getId()] = $job;
  828. }
  829. break;
  830. case 'lock':
  831. foreach ($job['packages'] as $package) {
  832. if (isset($this->installedMap[$package->getId()])) {
  833. $rule = $this->createInstallRule($package, Rule::RULE_JOB_LOCK);
  834. } else {
  835. $rule = $this->createRemoveRule($package, Rule::RULE_JOB_LOCK);
  836. }
  837. $this->addRule(RuleSet::TYPE_JOB, $rule);
  838. $this->ruleToJob[$rule->getId()] = $job;
  839. }
  840. break;
  841. }
  842. }
  843. $this->addChoiceRules();
  844. foreach ($this->rules as $rule) {
  845. $this->addWatchesToRule($rule);
  846. }
  847. /* disable update rules that conflict with our job */
  848. $this->disablePolicyRules();
  849. /* make decisions based on job/update assertions */
  850. $this->makeAssertionRuleDecisions();
  851. $installRecommended = 0;
  852. $this->runSat(true, $installRecommended);
  853. //$this->printDecisionMap();
  854. //findrecommendedsuggested(solv);
  855. //solver_prepare_solutions(solv);
  856. if ($this->problems) {
  857. throw new SolverProblemsException($this->problems);
  858. }
  859. return $this->createTransaction();
  860. }
  861. protected function createTransaction()
  862. {
  863. $transaction = array();
  864. $installMeansUpdateMap = array();
  865. foreach ($this->decisionQueue as $i => $literal) {
  866. $package = $literal->getPackage();
  867. // !wanted & installed
  868. if (!$literal->isWanted() && isset($this->installedMap[$package->getId()])) {
  869. $literals = array();
  870. if (isset($this->packageToFeatureRule[$package->getId()])) {
  871. $literals = array_merge($literals, $this->packageToFeatureRule[$package->getId()]->getLiterals());
  872. }
  873. foreach ($literals as $updateLiteral) {
  874. if (!$updateLiteral->equals($literal)) {
  875. $installMeansUpdateMap[$updateLiteral->getPackageId()] = $package;
  876. }
  877. }
  878. }
  879. }
  880. foreach ($this->decisionQueue as $i => $literal) {
  881. $package = $literal->getPackage();
  882. // wanted & installed || !wanted & !installed
  883. if ($literal->isWanted() == (isset($this->installedMap[$package->getId()]))) {
  884. continue;
  885. }
  886. if ($literal->isWanted()) {
  887. if (isset($installMeansUpdateMap[$literal->getPackageId()])) {
  888. $source = $installMeansUpdateMap[$literal->getPackageId()];
  889. $transaction[] = new Operation\UpdateOperation(
  890. $source, $package, $this->decisionQueueWhy[$i]
  891. );
  892. // avoid updates to one package from multiple origins
  893. unset($installMeansUpdateMap[$literal->getPackageId()]);
  894. $ignoreRemove[$source->getId()] = true;
  895. } else {
  896. $transaction[] = new Operation\InstallOperation(
  897. $package, $this->decisionQueueWhy[$i]
  898. );
  899. }
  900. } else if (!isset($ignoreRemove[$package->getId()])) {
  901. $transaction[] = new Operation\UninstallOperation(
  902. $package, $this->decisionQueueWhy[$i]
  903. );
  904. }
  905. }
  906. return array_reverse($transaction);
  907. }
  908. protected $decisionQueue = array();
  909. protected $decisionQueueWhy = array();
  910. protected $decisionQueueFree = array();
  911. protected $propagateIndex;
  912. protected $branches = array();
  913. protected $problems = array();
  914. protected $learnedPool = array();
  915. protected $recommendsIndex;
  916. protected function literalFromId($id)
  917. {
  918. $package = $this->pool->packageById(abs($id));
  919. return new Literal($package, $id > 0);
  920. }
  921. protected function addDecision(Literal $l, $level)
  922. {
  923. assert($this->decisionMap[$l->getPackageId()] == 0);
  924. if ($l->isWanted()) {
  925. $this->decisionMap[$l->getPackageId()] = $level;
  926. } else {
  927. $this->decisionMap[$l->getPackageId()] = -$level;
  928. }
  929. }
  930. protected function addDecisionId($literalId, $level)
  931. {
  932. $packageId = abs($literalId);
  933. assert($this->decisionMap[$packageId] == 0);
  934. if ($literalId > 0) {
  935. $this->decisionMap[$packageId] = $level;
  936. } else {
  937. $this->decisionMap[$packageId] = -$level;
  938. }
  939. }
  940. protected function decisionsContain(Literal $l)
  941. {
  942. return (
  943. $this->decisionMap[$l->getPackageId()] > 0 && $l->isWanted() ||
  944. $this->decisionMap[$l->getPackageId()] < 0 && !$l->isWanted()
  945. );
  946. }
  947. protected function decisionsContainId($literalId)
  948. {
  949. $packageId = abs($literalId);
  950. return (
  951. $this->decisionMap[$packageId] > 0 && $literalId > 0 ||
  952. $this->decisionMap[$packageId] < 0 && $literalId < 0
  953. );
  954. }
  955. protected function decisionsSatisfy(Literal $l)
  956. {
  957. return ($l->isWanted() && $this->decisionMap[$l->getPackageId()] > 0) ||
  958. (!$l->isWanted() && $this->decisionMap[$l->getPackageId()] <= 0);
  959. }
  960. protected function decisionsConflict(Literal $l)
  961. {
  962. return (
  963. $this->decisionMap[$l->getPackageId()] > 0 && !$l->isWanted() ||
  964. $this->decisionMap[$l->getPackageId()] < 0 && $l->isWanted()
  965. );
  966. }
  967. protected function decisionsConflictId($literalId)
  968. {
  969. $packageId = abs($literalId);
  970. return (
  971. ($this->decisionMap[$packageId] > 0 && $literalId < 0) ||
  972. ($this->decisionMap[$packageId] < 0 && $literalId > 0)
  973. );
  974. }
  975. protected function decided(PackageInterface $p)
  976. {
  977. return $this->decisionMap[$p->getId()] != 0;
  978. }
  979. protected function undecided(PackageInterface $p)
  980. {
  981. return $this->decisionMap[$p->getId()] == 0;
  982. }
  983. protected function decidedInstall(PackageInterface $p) {
  984. return $this->decisionMap[$p->getId()] > 0;
  985. }
  986. protected function decidedRemove(PackageInterface $p) {
  987. return $this->decisionMap[$p->getId()] < 0;
  988. }
  989. /**
  990. * Makes a decision and propagates it to all rules.
  991. *
  992. * Evaluates each term affected by the decision (linked through watches)
  993. * If we find unit rules we make new decisions based on them
  994. *
  995. * @return Rule|null A rule on conflict, otherwise null.
  996. */
  997. protected function propagate($level)
  998. {
  999. while ($this->propagateIndex < count($this->decisionQueue)) {
  1000. // we invert the decided literal here, example:
  1001. // A was decided => (-A|B) now requires B to be true, so we look for
  1002. // rules which are fulfilled by -A, rather than A.
  1003. $literal = $this->decisionQueue[$this->propagateIndex]->inverted();
  1004. $this->propagateIndex++;
  1005. // /* foreach rule where 'pkg' is now FALSE */
  1006. //for (rp = watches + pkg; *rp; rp = next_rp)
  1007. if (!isset($this->watches[$literal->getId()])) {
  1008. continue;
  1009. }
  1010. $prevRule = null;
  1011. for ($rule = $this->watches[$literal->getId()]; $rule !== null; $prevRule = $rule, $rule = $nextRule) {
  1012. $nextRule = $rule->getNext($literal);
  1013. if ($rule->isDisabled()) {
  1014. continue;
  1015. }
  1016. $otherWatch = $rule->getOtherWatch($literal);
  1017. if ($this->decisionsContainId($otherWatch)) {
  1018. continue;
  1019. }
  1020. $ruleLiterals = $rule->getLiterals();
  1021. if (sizeof($ruleLiterals) > 2) {
  1022. foreach ($ruleLiterals as $ruleLiteral) {
  1023. if ($otherWatch !== $ruleLiteral->getId() &&
  1024. !$this->decisionsConflict($ruleLiteral)) {
  1025. if ($literal->getId() === $rule->watch1) {
  1026. $rule->watch1 = $ruleLiteral->getId();
  1027. $rule->next1 = (isset($this->watches[$ruleLiteral->getId()])) ? $this->watches[$ruleLiteral->getId()] : null;
  1028. } else {
  1029. $rule->watch2 = $ruleLiteral->getId();
  1030. $rule->next2 = (isset($this->watches[$ruleLiteral->getId()])) ? $this->watches[$ruleLiteral->getId()] : null;
  1031. }
  1032. if ($prevRule) {
  1033. if ($prevRule->next1 == $rule) {
  1034. $prevRule->next1 = $nextRule;
  1035. } else {
  1036. $prevRule->next2 = $nextRule;
  1037. }
  1038. } else {
  1039. $this->watches[$literal->getId()] = $nextRule;
  1040. }
  1041. $this->watches[$ruleLiteral->getId()] = $rule;
  1042. $rule = $prevRule;
  1043. continue 2;
  1044. }
  1045. }
  1046. }
  1047. // yay, we found a unit clause! try setting it to true
  1048. if ($this->decisionsConflictId($otherWatch)) {
  1049. return $rule;
  1050. }
  1051. $this->addDecisionId($otherWatch, $level);
  1052. $this->decisionQueue[] = $this->literalFromId($otherWatch);
  1053. $this->decisionQueueWhy[] = $rule;
  1054. }
  1055. }
  1056. return null;
  1057. }
  1058. /**
  1059. * Reverts a decision at the given level.
  1060. */
  1061. private function revert($level)
  1062. {
  1063. while (!empty($this->decisionQueue)) {
  1064. $literal = $this->decisionQueue[count($this->decisionQueue) - 1];
  1065. if (!$this->decisionMap[$literal->getPackageId()]) {
  1066. break;
  1067. }
  1068. $decisionLevel = abs($this->decisionMap[$literal->getPackageId()]);
  1069. if ($decisionLevel <= $level) {
  1070. break;
  1071. }
  1072. /** TODO: implement recommendations
  1073. *if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
  1074. * solv->recommendations.count--;
  1075. */
  1076. $this->decisionMap[$literal->getPackageId()] = 0;
  1077. array_pop($this->decisionQueue);
  1078. array_pop($this->decisionQueueWhy);
  1079. $this->propagateIndex = count($this->decisionQueue);
  1080. }
  1081. while (!empty($this->branches)) {
  1082. list($literals, $branchLevel) = $this->branches[count($this->branches) - 1];
  1083. if ($branchLevel >= $level) {
  1084. break;
  1085. }
  1086. array_pop($this->branches);
  1087. }
  1088. $this->recommendsIndex = -1;
  1089. }
  1090. /**-------------------------------------------------------------------
  1091. *
  1092. * setpropagatelearn
  1093. *
  1094. * add free decision (solvable to install) to decisionq
  1095. * increase level and propagate decision
  1096. * return if no conflict.
  1097. *
  1098. * in conflict case, analyze conflict rule, add resulting
  1099. * rule to learnt rule set, make decision from learnt
  1100. * rule (always unit) and re-propagate.
  1101. *
  1102. * returns the new solver level or 0 if unsolvable
  1103. *
  1104. */
  1105. private function setPropagateLearn($level, Literal $literal, $disableRules, Rule $rule)
  1106. {
  1107. assert($rule != null);
  1108. assert($literal != null);
  1109. $level++;
  1110. $this->addDecision($literal, $level);
  1111. $this->decisionQueue[] = $literal;
  1112. $this->decisionQueueWhy[] = $rule;
  1113. $this->decisionQueueFree[count($this->decisionQueueWhy) - 1] = true;
  1114. while (true) {
  1115. $rule = $this->propagate($level);
  1116. if (!$rule) {
  1117. break;
  1118. }
  1119. if ($level == 1) {
  1120. return $this->analyzeUnsolvable($rule, $disableRules);
  1121. }
  1122. // conflict
  1123. list($learnLiteral, $newLevel, $newRule, $why) = $this->analyze($level, $rule);
  1124. assert($newLevel > 0);
  1125. assert($newLevel < $level);
  1126. $level = $newLevel;
  1127. $this->revert($level);
  1128. assert($newRule != null);
  1129. $this->addRule(RuleSet::TYPE_LEARNED, $newRule);
  1130. $this->learnedWhy[$newRule->getId()] = $why;
  1131. $this->watch2OnHighest($newRule);
  1132. $this->addWatchesToRule($newRule);
  1133. $this->addDecision($learnLiteral, $level);
  1134. $this->decisionQueue[] = $learnLiteral;
  1135. $this->decisionQueueWhy[] = $newRule;
  1136. }
  1137. return $level;
  1138. }
  1139. private function selectAndInstall($level, array $decisionQueue, $disableRules, Rule $rule)
  1140. {
  1141. // choose best package to install from decisionQueue
  1142. $literals = $this->policy->selectPreferedPackages($this->pool, $this->installedMap, $decisionQueue);
  1143. $selectedLiteral = array_shift($literals);
  1144. // if there are multiple candidates, then branch
  1145. if (count($literals)) {
  1146. $this->branches[] = array($literals, $level);
  1147. }
  1148. return $this->setPropagateLearn($level, $selectedLiteral, $disableRules, $rule);
  1149. }
  1150. protected function analyze($level, $rule)
  1151. {
  1152. $ruleLevel = 1;
  1153. $num = 0;
  1154. $l1num = 0;
  1155. $seen = array();
  1156. $learnedLiterals = array(null);
  1157. $decisionId = count($this->decisionQueue);
  1158. $this->learnedPool[] = array();
  1159. while(true) {
  1160. $this->learnedPool[count($this->learnedPool) - 1][] = $rule;
  1161. foreach ($rule->getLiterals() as $literal) {
  1162. // skip the one true literal
  1163. if ($this->decisionsSatisfy($literal)) {
  1164. continue;
  1165. }
  1166. if (isset($seen[$literal->getPackageId()])) {
  1167. continue;
  1168. }
  1169. $seen[$literal->getPackageId()] = true;
  1170. $l = abs($this->decisionMap[$literal->getPackageId()]);
  1171. if (1 === $l) {
  1172. $l1num++;
  1173. } else if ($level === $l) {
  1174. $num++;
  1175. } else {
  1176. // not level1 or conflict level, add to new rule
  1177. $learnedLiterals[] = $literal;
  1178. if ($l > $ruleLevel) {
  1179. $ruleLevel = $l;
  1180. }
  1181. }
  1182. }
  1183. $l1retry = true;
  1184. while ($l1retry) {
  1185. $l1retry = false;
  1186. if (!$num && !--$l1num) {
  1187. // all level 1 literals done
  1188. break 2;
  1189. }
  1190. while (true) {
  1191. assert($decisionId > 0);
  1192. $decisionId--;
  1193. $literal = $this->decisionQueue[$decisionId];
  1194. if (isset($seen[$literal->getPackageId()])) {
  1195. break;
  1196. }
  1197. }
  1198. unset($seen[$literal->getPackageId()]);
  1199. if ($num && 0 === --$num) {
  1200. $learnedLiterals[0] = $this->literalFromId(-$literal->getPackageId());
  1201. if (!$l1num) {
  1202. break 2;
  1203. }
  1204. foreach ($learnedLiterals as $i => $learnedLiteral) {
  1205. if ($i !== 0) {
  1206. unset($seen[$literal->getPackageId()]);
  1207. }
  1208. }
  1209. // only level 1 marks left
  1210. $l1num++;
  1211. $l1retry = true;
  1212. }
  1213. $rule = $this->decisionQueueWhy[$decisionId];
  1214. }
  1215. }
  1216. $why = count($this->learnedPool) - 1;
  1217. assert($learnedLiterals[0] !== null);
  1218. $newRule = new Rule($learnedLiterals, Rule::RULE_LEARNED, $why);
  1219. return array($learnedLiterals[0], $ruleLevel, $newRule, $why);
  1220. }
  1221. private function analyzeUnsolvableRule($problem, $conflictRule, &$lastWeakWhy)
  1222. {
  1223. $why = $conflictRule->getId();
  1224. if ($conflictRule->getType() == RuleSet::TYPE_LEARNED) {
  1225. $learnedWhy = $this->learnedWhy[$why];
  1226. $problemRules = $this->learnedPool[$learnedWhy];
  1227. foreach ($problemRules as $problemRule) {
  1228. $this->analyzeUnsolvableRule($problem, $problemRule, $lastWeakWhy);
  1229. }
  1230. return;
  1231. }
  1232. if ($conflictRule->getType() == RuleSet::TYPE_PACKAGE) {
  1233. // package rules cannot be part of a problem
  1234. return;
  1235. }
  1236. if ($conflictRule->isWeak()) {
  1237. /** TODO why > or < lastWeakWhy? */
  1238. if (!$lastWeakWhy || $why > $lastWeakWhy->getId()) {
  1239. $lastWeakWhy = $conflictRule;
  1240. }
  1241. }
  1242. if ($conflictRule->getType() == RuleSet::TYPE_JOB) {
  1243. $job = $this->ruleToJob[$conflictRule->getId()];
  1244. $problem->addJobRule($job, $conflictRule);
  1245. } else {
  1246. $problem->addRule($conflictRule);
  1247. }
  1248. }
  1249. private function analyzeUnsolvable($conflictRule, $disableRules)
  1250. {
  1251. $lastWeakWhy = null;
  1252. $problem = new Problem;
  1253. $problem->addRule($conflictRule);
  1254. $this->analyzeUnsolvableRule($problem, $conflictRule, $lastWeakWhy);
  1255. $this->problems[] = $problem;
  1256. $seen = array();
  1257. $literals = $conflictRule->getLiterals();
  1258. /* unnecessary because unlike rule.d, watch2 == 2nd literal, unless watch2 changed
  1259. if (sizeof($literals) == 2) {
  1260. $literals[1] = $this->literalFromId($conflictRule->watch2);
  1261. }
  1262. */
  1263. foreach ($literals as $literal) {
  1264. // skip the one true literal
  1265. if ($this->decisionsSatisfy($literal)) {
  1266. continue;
  1267. }
  1268. $seen[$literal->getPackageId()] = true;
  1269. }
  1270. $decisionId = count($this->decisionQueue);
  1271. while ($decisionId > 0) {
  1272. $decisionId--;
  1273. $literal = $this->decisionQueue[$decisionId];
  1274. // skip literals that are not in this rule
  1275. if (!isset($seen[$literal->getPackageId()])) {
  1276. continue;
  1277. }
  1278. $why = $this->decisionQueueWhy[$decisionId];
  1279. $problem->addRule($why);
  1280. $this->analyzeUnsolvableRule($problem, $why, $lastWeakWhy);
  1281. $literals = $why->getLiterals();
  1282. /* unnecessary because unlike rule.d, watch2 == 2nd literal, unless watch2 changed
  1283. if (sizeof($literals) == 2) {
  1284. $literals[1] = $this->literalFromId($why->watch2);
  1285. }
  1286. */
  1287. foreach ($literals as $literal) {
  1288. // skip the one true literal
  1289. if ($this->decisionsSatisfy($literal)) {
  1290. continue;
  1291. }
  1292. $seen[$literal->getPackageId()] = true;
  1293. }
  1294. }
  1295. if ($lastWeakWhy) {
  1296. array_pop($this->problems);
  1297. if ($lastWeakWhy->getType() === RuleSet::TYPE_JOB) {
  1298. $why = $this->ruleToJob[$lastWeakWhy];
  1299. } else {
  1300. $why = $lastWeakWhy;
  1301. }
  1302. if ($lastWeakWhy->getType() == RuleSet::TYPE_CHOICE) {
  1303. $this->disableChoiceRules($lastWeakWhy);
  1304. }
  1305. $this->disableProblem($why);
  1306. /**
  1307. @TODO what does v < 0 mean here? ($why == v)
  1308. if (v < 0)
  1309. solver_reenablepolicyrules(solv, -(v + 1));
  1310. */
  1311. $this->resetSolver();
  1312. return true;
  1313. }
  1314. if ($disableRules) {
  1315. foreach ($this->problems[count($this->problems) - 1] as $reason) {
  1316. if ($reason['job']) {
  1317. $this->disableProblem($reason['job']);
  1318. } else {
  1319. $this->disableProblem($reason['rule']);
  1320. }
  1321. }
  1322. $this->resetSolver();
  1323. return true;
  1324. }
  1325. return false;
  1326. }
  1327. private function disableProblem($why)
  1328. {
  1329. if ($why instanceof Rule) {
  1330. $why->disable();
  1331. } else if (is_array($why)) {
  1332. // disable all rules of this job
  1333. foreach ($this->ruleToJob as $ruleId => $job) {
  1334. if ($why === $job) {
  1335. $this->rules->ruleById($ruleId)->disable();
  1336. }
  1337. }
  1338. }
  1339. }
  1340. private function resetSolver()
  1341. {
  1342. while ($literal = array_pop($this->decisionQueue)) {
  1343. $this->decisionMap[$literal->getPackageId()] = 0;
  1344. }
  1345. $this->decisionQueueWhy = array();
  1346. $this->decisionQueueFree = array();
  1347. $this->recommendsIndex = -1;
  1348. $this->propagateIndex = 0;
  1349. $this->recommendations = array();
  1350. $this->branches = array();
  1351. $this->enableDisableLearnedRules();
  1352. $this->makeAssertionRuleDecisions();
  1353. }
  1354. /*-------------------------------------------------------------------
  1355. * enable/disable learnt rules
  1356. *
  1357. * we have enabled or disabled some of our rules. We now reenable all
  1358. * of our learnt rules except the ones that were learnt from rules that
  1359. * are now disabled.
  1360. */
  1361. private function enableDisableLearnedRules()
  1362. {
  1363. foreach ($this->rules->getIteratorFor(RuleSet::TYPE_LEARNED) as $rule) {
  1364. $why = $this->learnedWhy[$rule->getId()];
  1365. $problemRules = $this->learnedPool[$why];
  1366. $foundDisabled = false;
  1367. foreach ($problemRules as $problemRule) {
  1368. if ($problemRule->isDisabled()) {
  1369. $foundDisabled = true;
  1370. break;
  1371. }
  1372. }
  1373. if ($foundDisabled && $rule->isEnabled()) {
  1374. $rule->disable();
  1375. } else if (!$foundDisabled && $rule->isDisabled()) {
  1376. $rule->enable();
  1377. }
  1378. }
  1379. }
  1380. private function runSat($disableRules = true, $installRecommended = false)
  1381. {
  1382. $this->propagateIndex = 0;
  1383. // /*
  1384. // * here's the main loop:
  1385. // * 1) propagate new decisions (only needed once)
  1386. // * 2) fulfill jobs
  1387. // * 3) try to keep installed packages
  1388. // * 4) fulfill all unresolved rules
  1389. // * 5) install recommended packages
  1390. // * 6) minimalize solution if we had choices
  1391. // * if we encounter a problem, we rewind to a safe level and restart
  1392. // * with step 1
  1393. // */
  1394. $decisionQueue = array();
  1395. $decisionSupplementQueue = array();
  1396. $disableRules = array();
  1397. $level = 1;
  1398. $systemLevel = $level + 1;
  1399. $minimizationSteps = 0;
  1400. $installedPos = 0;
  1401. $this->installedPackages = $this->installed->getPackages();
  1402. while (true) {
  1403. if (1 === $level) {
  1404. $conflictRule = $this->propagate($level);
  1405. if ($conflictRule !== null) {
  1406. if ($this->analyzeUnsolvable($conflictRule, $disableRules)) {
  1407. continue;
  1408. } else {
  1409. return;
  1410. }
  1411. }
  1412. }
  1413. // handle job rules
  1414. if ($level < $systemLevel) {
  1415. $iterator = $this->rules->getIteratorFor(RuleSet::TYPE_JOB);
  1416. foreach ($iterator as $rule) {
  1417. if ($rule->isEnabled()) {
  1418. $decisionQueue = array();
  1419. $noneSatisfied = true;
  1420. foreach ($rule->getLiterals() as $literal) {
  1421. if ($this->decisionsSatisfy($literal)) {
  1422. $noneSatisfied = false;
  1423. break;
  1424. }
  1425. $decisionQueue[] = $literal;
  1426. }
  1427. if ($noneSatisfied && count($decisionQueue)) {
  1428. // prune all update packages until installed version
  1429. // except for requested updates
  1430. if (count($this->installed) != count($this->updateMap)) {
  1431. $prunedQueue = array();
  1432. foreach ($decisionQueue as $literal) {
  1433. if (isset($this->installedMap[$literal->getPackageId()])) {
  1434. $prunedQueue[] = $literal;
  1435. if (isset($this->updateMap[$literal->getPackageId()])) {
  1436. $prunedQueue = $decisionQueue;
  1437. break;
  1438. }
  1439. }
  1440. }
  1441. $decisionQueue = $prunedQueue;
  1442. }
  1443. }
  1444. if ($noneSatisfied && count($decisionQueue)) {
  1445. $oLevel = $level;
  1446. $level = $this->selectAndInstall($level, $decisionQueue, $disableRules, $rule);
  1447. if (0 === $level) {
  1448. return;
  1449. }
  1450. if ($level <= $oLevel) {
  1451. break;
  1452. }
  1453. }
  1454. }
  1455. }
  1456. $systemLevel = $level + 1;
  1457. // jobs left
  1458. $iterator->next();
  1459. if ($iterator->valid()) {
  1460. continue;
  1461. }
  1462. }
  1463. // handle installed packages
  1464. if ($level < $systemLevel) {
  1465. // use two passes if any packages are being updated
  1466. // -> better user experience
  1467. for ($pass = (count($this->updateMap)) ? 0 : 1; $pass < 2; $pass++) {
  1468. $passLevel = $level;
  1469. for ($i = $installedPos, $n = 0; $n < count($this->installedPackages); $i++, $n++) {
  1470. $repeat = false;
  1471. if ($i == count($this->installedPackages)) {
  1472. $i = 0;
  1473. }
  1474. $literal = new Literal($this->installedPackages[$i], true);
  1475. if ($this->decisionsContain($literal)) {
  1476. continue;
  1477. }
  1478. // only process updates in first pass
  1479. /** TODO: && or || ? **/
  1480. if (0 === $pass && !isset($this->updateMap[$literal->getPackageId()])) {
  1481. continue;
  1482. }
  1483. $rule = null;
  1484. if (isset($this->packageToFeatureRule[$literal->getPackageId()])) {
  1485. $rule = $this->packageToFeatureRule[$literal->getPackageId()];
  1486. }
  1487. if (!$rule || $rule->isDisabled()) {
  1488. continue;
  1489. }
  1490. $updateRuleLiterals = $rule->getLiterals();
  1491. $decisionQueue = array();
  1492. if (!isset($this->noUpdate[$literal->getPackageId()]) && (
  1493. $this->decidedRemove($literal->getPackage()) ||
  1494. isset($this->updateMap[$literal->getPackageId()]) ||
  1495. !$literal->equals($updateRuleLiterals[0])
  1496. )) {
  1497. foreach ($updateRuleLiterals as $ruleLiteral) {
  1498. if ($this->decidedInstall($ruleLiteral->getPackage())) {
  1499. // already fulfilled
  1500. $decisionQueue = array();
  1501. break;
  1502. }
  1503. if ($this->undecided($ruleLiteral->getPackage())) {
  1504. $decisionQueue[] = $ruleLiteral;
  1505. }
  1506. }
  1507. }
  1508. if (sizeof($decisionQueue)) {
  1509. $oLevel = $level;
  1510. $level = $this->selectAndInstall($level, $decisionQueue, $disableRules, $rule);
  1511. if (0 === $level) {
  1512. return;
  1513. }
  1514. if ($level <= $oLevel) {
  1515. $repeat = true;
  1516. }
  1517. } else if (!$repeat && $this->undecided($literal->getPackage())) {
  1518. // still undecided? keep package.
  1519. $oLevel = $level;
  1520. if (isset($this->cleanDepsMap[$literal->getPackageId()])) {
  1521. // clean deps removes package
  1522. $level = $this->setPropagateLearn($level, $literal->invert(), $disableRules, null);
  1523. } else {
  1524. // ckeeping package
  1525. $level = $this->setPropagateLearn($level, $literal, $disableRules, $rule);
  1526. }
  1527. if (0 === $level) {
  1528. return;
  1529. }
  1530. if ($level <= $oLevel) {
  1531. $repeat = true;
  1532. }
  1533. }
  1534. if ($repeat) {
  1535. if (1 === $level || $level < $passLevel) {
  1536. // trouble
  1537. break;
  1538. }
  1539. if ($level < $oLevel) {
  1540. // redo all
  1541. $n = 0;
  1542. }
  1543. // repeat
  1544. $i--;
  1545. $n--;
  1546. continue;
  1547. }
  1548. }
  1549. if ($n < count($this->installedPackages)) {
  1550. $installedPos = $i; // retry this problem next time
  1551. break;
  1552. }
  1553. $installedPos = 0;
  1554. }
  1555. $systemLevel = $level + 1;
  1556. if ($pass < 2) {
  1557. // had trouble => retry
  1558. continue;
  1559. }
  1560. }
  1561. if ($level < $systemLevel) {
  1562. $systemLevel = $level;
  1563. }
  1564. for ($i = 0, $n = 0; $n < count($this->rules); $i++, $n++) {
  1565. if ($i == count($this->rules)) {
  1566. $i = 0;
  1567. }
  1568. $rule = $this->rules->ruleById($i);
  1569. $literals = $rule->getLiterals();
  1570. if ($rule->isDisabled()) {
  1571. continue;
  1572. }
  1573. $decisionQueue = array();
  1574. // make sure that
  1575. // * all negative literals are installed
  1576. // * no positive literal is installed
  1577. // i.e. the rule is not fulfilled and we
  1578. // just need to decide on the positive literals
  1579. //
  1580. foreach ($literals as $literal) {
  1581. if (!$literal->isWanted()) {
  1582. if (!$this->decidedInstall($literal->getPackage())) {
  1583. continue 2; // next rule
  1584. }
  1585. } else {
  1586. if ($this->decidedInstall($literal->getPackage())) {
  1587. continue 2; // next rule
  1588. }
  1589. if ($this->undecided($literal->getPackage())) {
  1590. $decisionQueue[] = $literal;
  1591. }
  1592. }
  1593. }
  1594. // need to have at least 2 item to pick from
  1595. if (count($decisionQueue) < 2) {
  1596. continue;
  1597. }
  1598. $oLevel = $level;
  1599. $level = $this->selectAndInstall($level, $decisionQueue, $disableRules, $rule);
  1600. if (0 === $level) {
  1601. return;
  1602. }
  1603. // open suse sat-solver uses this, but why is $level == 1 trouble?
  1604. // SYSTEMSOLVABLE related? we don't have that, so should work
  1605. //if ($level < $systemLevel || $level == 1) {
  1606. if ($level < $systemLevel) {
  1607. break; // trouble
  1608. }
  1609. // something changed, so look at all rules again
  1610. $n = -1;
  1611. }
  1612. // minimization step
  1613. if (count($this->branches)) {
  1614. $lastLiteral = null;
  1615. $lastLevel = null;
  1616. $lastBranchIndex = 0;
  1617. $lastBranchOffset = 0;
  1618. for ($i = count($this->branches) - 1; $i >= 0; $i--) {
  1619. list($literals, $level) = $this->branches[$i];
  1620. foreach ($literals as $offset => $literal) {
  1621. if ($literal && $literal->isWanted() && $this->decisionMap[$literal->getPackageId()] > $level + 1) {
  1622. $lastLiteral = $literal;
  1623. $lastBranchIndex = $i;
  1624. $lastBranchOffset = $offset;
  1625. $lastLevel = $level;
  1626. }
  1627. }
  1628. }
  1629. if ($lastLiteral) {
  1630. $this->branches[$lastBranchIndex][$lastBranchOffset] = null;
  1631. $minimizationSteps++;
  1632. $level = $lastLevel;
  1633. $this->revert($level);
  1634. $why = $this->decisionQueueWhy[count($this->decisionQueueWhy) - 1];
  1635. $oLevel = $level;
  1636. $level = $this->setPropagateLearn($level, $lastLiteral, $disableRules, $why);
  1637. if ($level == 0) {
  1638. return;
  1639. }
  1640. continue;
  1641. }
  1642. }
  1643. break;
  1644. }
  1645. }
  1646. private function printDecisionMap()
  1647. {
  1648. echo "\nDecisionMap: \n";
  1649. foreach ($this->decisionMap as $packageId => $level) {
  1650. if ($packageId === 0) {
  1651. continue;
  1652. }
  1653. if ($level > 0) {
  1654. echo ' +' . $this->pool->packageById($packageId)."\n";
  1655. } elseif ($level < 0) {
  1656. echo ' -' . $this->pool->packageById($packageId)."\n";
  1657. } else {
  1658. echo ' ?' . $this->pool->packageById($packageId)."\n";
  1659. }
  1660. }
  1661. echo "\n";
  1662. }
  1663. private function printDecisionQueue()
  1664. {
  1665. echo "DecisionQueue: \n";
  1666. foreach ($this->decisionQueue as $i => $literal) {
  1667. echo ' ' . $literal . ' ' . $this->decisionQueueWhy[$i]." level ".$this->decisionMap[$literal->getPackageId()]."\n";
  1668. }
  1669. echo "\n";
  1670. }
  1671. private function printWatches()
  1672. {
  1673. echo "\nWatches:\n";
  1674. foreach ($this->watches as $literalId => $watch) {
  1675. echo ' '.$this->literalFromId($literalId)."\n";
  1676. $queue = array(array(' ', $watch));
  1677. while (!empty($queue)) {
  1678. list($indent, $watch) = array_pop($queue);
  1679. echo $indent.$watch;
  1680. if ($watch) {
  1681. echo ' [id='.$watch->getId().',watch1='.$this->literalFromId($watch->watch1).',watch2='.$this->literalFromId($watch->watch2)."]";
  1682. }
  1683. echo "\n";
  1684. if ($watch && ($watch->next1 == $watch || $watch->next2 == $watch)) {
  1685. if ($watch->next1 == $watch) {
  1686. echo $indent." 1 *RECURSION*";
  1687. }
  1688. if ($watch->next2 == $watch) {
  1689. echo $indent." 2 *RECURSION*";
  1690. }
  1691. } elseif ($watch && ($watch->next1 || $watch->next2)) {
  1692. $indent = str_replace(array('1', '2'), ' ', $indent);
  1693. array_push($queue, array($indent.' 2 ', $watch->next2));
  1694. array_push($queue, array($indent.' 1 ', $watch->next1));
  1695. }
  1696. }
  1697. echo "\n";
  1698. }
  1699. }
  1700. }