Correct the parent path in the watch tree, after moving a rule out of the path
parent
509188c112
commit
ff620afe05
|
@ -1266,7 +1266,7 @@ class Solver
|
||||||
}
|
}
|
||||||
|
|
||||||
if ($prevRule) {
|
if ($prevRule) {
|
||||||
if ($prevRule->watch1 === $literal->getId()) {
|
if ($prevRule->next1 == $rule) {
|
||||||
$prevRule->next1 = $nextRule;
|
$prevRule->next1 = $nextRule;
|
||||||
} else {
|
} else {
|
||||||
$prevRule->next2 = $nextRule;
|
$prevRule->next2 = $nextRule;
|
||||||
|
@ -1276,6 +1276,8 @@ class Solver
|
||||||
}
|
}
|
||||||
|
|
||||||
$this->watches[$ruleLiteral->getId()] = $rule;
|
$this->watches[$ruleLiteral->getId()] = $rule;
|
||||||
|
|
||||||
|
$rule = $prevRule;
|
||||||
continue 2;
|
continue 2;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1506,7 +1508,7 @@ class Solver
|
||||||
}
|
}
|
||||||
|
|
||||||
$why = count($this->learnedPool) - 1;
|
$why = count($this->learnedPool) - 1;
|
||||||
|
assert($learnedLiterals[0] !== null);
|
||||||
$newRule = new Rule($learnedLiterals, self::RULE_LEARNED, $why);
|
$newRule = new Rule($learnedLiterals, self::RULE_LEARNED, $why);
|
||||||
|
|
||||||
return array($ruleLevel, $newRule, $why);
|
return array($ruleLevel, $newRule, $why);
|
||||||
|
|
Loading…
Reference in New Issue