Solver.php 63 KB

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