|
@@ -69,7 +69,7 @@ class Solver
|
|
for ($ruleIndex = 0; $ruleIndex < count($this->rules); $ruleIndex++) {
|
|
for ($ruleIndex = 0; $ruleIndex < count($this->rules); $ruleIndex++) {
|
|
$rule = $this->rules->ruleById($ruleIndex);
|
|
$rule = $this->rules->ruleById($ruleIndex);
|
|
|
|
|
|
- if ($rule->isWeak() || !$rule->isAssertion() || $rule->isDisabled()) {
|
|
|
|
|
|
+ if (!$rule->isAssertion() || $rule->isDisabled()) {
|
|
continue;
|
|
continue;
|
|
}
|
|
}
|
|
|
|
|
|
@@ -104,15 +104,15 @@ class Solver
|
|
continue;
|
|
continue;
|
|
}
|
|
}
|
|
|
|
|
|
- // conflict with another job or update/feature rule
|
|
|
|
|
|
+ // conflict with another job
|
|
$problem = new Problem;
|
|
$problem = new Problem;
|
|
$problem->addRule($rule);
|
|
$problem->addRule($rule);
|
|
$problem->addRule($conflict);
|
|
$problem->addRule($conflict);
|
|
|
|
|
|
- // push all of our rules (can only be feature or job rules)
|
|
|
|
|
|
+ // push all of our rules (can only be job rules)
|
|
// asserting this literal on the problem stack
|
|
// asserting this literal on the problem stack
|
|
foreach ($this->rules->getIteratorFor(RuleSet::TYPE_JOB) as $assertRule) {
|
|
foreach ($this->rules->getIteratorFor(RuleSet::TYPE_JOB) as $assertRule) {
|
|
- if ($assertRule->isDisabled() || !$assertRule->isAssertion() || $assertRule->isWeak()) {
|
|
|
|
|
|
+ if ($assertRule->isDisabled() || !$assertRule->isAssertion()) {
|
|
continue;
|
|
continue;
|
|
}
|
|
}
|
|
|
|
|
|
@@ -137,27 +137,6 @@ class Solver
|
|
}
|
|
}
|
|
$ruleIndex = -1;
|
|
$ruleIndex = -1;
|
|
}
|
|
}
|
|
-
|
|
|
|
- foreach ($this->rules as $rule) {
|
|
|
|
- if (!$rule->isWeak() || !$rule->isAssertion() || $rule->isDisabled()) {
|
|
|
|
- continue;
|
|
|
|
- }
|
|
|
|
-
|
|
|
|
- $literals = $rule->getLiterals();
|
|
|
|
- $literal = $literals[0];
|
|
|
|
-
|
|
|
|
- if ($this->decisionMap[abs($literal)] == 0) {
|
|
|
|
- $this->decide($literal, 1, $rule);
|
|
|
|
- continue;
|
|
|
|
- }
|
|
|
|
-
|
|
|
|
- if ($this->decisionsSatisfy($literals[0])) {
|
|
|
|
- continue;
|
|
|
|
- }
|
|
|
|
-
|
|
|
|
- // conflict, but this is a weak rule => disable
|
|
|
|
- $this->disableProblem($rule);
|
|
|
|
- }
|
|
|
|
}
|
|
}
|
|
|
|
|
|
protected function setupInstalledMap()
|
|
protected function setupInstalledMap()
|
|
@@ -553,7 +532,7 @@ class Solver
|
|
return array($learnedLiterals[0], $ruleLevel, $newRule, $why);
|
|
return array($learnedLiterals[0], $ruleLevel, $newRule, $why);
|
|
}
|
|
}
|
|
|
|
|
|
- private function analyzeUnsolvableRule($problem, $conflictRule, &$lastWeakWhy)
|
|
|
|
|
|
+ private function analyzeUnsolvableRule($problem, $conflictRule)
|
|
{
|
|
{
|
|
$why = $conflictRule->getId();
|
|
$why = $conflictRule->getId();
|
|
|
|
|
|
@@ -562,7 +541,7 @@ class Solver
|
|
$problemRules = $this->learnedPool[$learnedWhy];
|
|
$problemRules = $this->learnedPool[$learnedWhy];
|
|
|
|
|
|
foreach ($problemRules as $problemRule) {
|
|
foreach ($problemRules as $problemRule) {
|
|
- $this->analyzeUnsolvableRule($problem, $problemRule, $lastWeakWhy);
|
|
|
|
|
|
+ $this->analyzeUnsolvableRule($problem, $problemRule);
|
|
}
|
|
}
|
|
return;
|
|
return;
|
|
}
|
|
}
|
|
@@ -572,23 +551,15 @@ class Solver
|
|
return;
|
|
return;
|
|
}
|
|
}
|
|
|
|
|
|
- if ($conflictRule->isWeak()) {
|
|
|
|
- /** TODO why > or < lastWeakWhy? */
|
|
|
|
- if (!$lastWeakWhy || $why > $lastWeakWhy->getId()) {
|
|
|
|
- $lastWeakWhy = $conflictRule;
|
|
|
|
- }
|
|
|
|
- }
|
|
|
|
-
|
|
|
|
$problem->addRule($conflictRule);
|
|
$problem->addRule($conflictRule);
|
|
}
|
|
}
|
|
|
|
|
|
private function analyzeUnsolvable($conflictRule, $disableRules)
|
|
private function analyzeUnsolvable($conflictRule, $disableRules)
|
|
{
|
|
{
|
|
- $lastWeakWhy = null;
|
|
|
|
$problem = new Problem;
|
|
$problem = new Problem;
|
|
$problem->addRule($conflictRule);
|
|
$problem->addRule($conflictRule);
|
|
|
|
|
|
- $this->analyzeUnsolvableRule($problem, $conflictRule, $lastWeakWhy);
|
|
|
|
|
|
+ $this->analyzeUnsolvableRule($problem, $conflictRule);
|
|
|
|
|
|
$this->problems[] = $problem;
|
|
$this->problems[] = $problem;
|
|
|
|
|
|
@@ -618,7 +589,7 @@ class Solver
|
|
$why = $this->decisionQueueWhy[$decisionId];
|
|
$why = $this->decisionQueueWhy[$decisionId];
|
|
$problem->addRule($why);
|
|
$problem->addRule($why);
|
|
|
|
|
|
- $this->analyzeUnsolvableRule($problem, $why, $lastWeakWhy);
|
|
|
|
|
|
+ $this->analyzeUnsolvableRule($problem, $why);
|
|
|
|
|
|
$literals = $why->getLiterals();
|
|
$literals = $why->getLiterals();
|
|
|
|
|
|
@@ -631,15 +602,6 @@ class Solver
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
- if ($lastWeakWhy) {
|
|
|
|
- array_pop($this->problems);
|
|
|
|
-
|
|
|
|
- $this->disableProblem($lastWeakWhy);
|
|
|
|
- $this->resetSolver();
|
|
|
|
-
|
|
|
|
- return 1;
|
|
|
|
- }
|
|
|
|
-
|
|
|
|
if ($disableRules) {
|
|
if ($disableRules) {
|
|
foreach ($this->problems[count($this->problems) - 1] as $reason) {
|
|
foreach ($this->problems[count($this->problems) - 1] as $reason) {
|
|
$this->disableProblem($reason['rule']);
|
|
$this->disableProblem($reason['rule']);
|