Solver.php 64 KB

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