|
|
|
@ -22,30 +22,20 @@ class RuleWatchGraph
|
|
|
|
|
/**
|
|
|
|
|
* Alters watch chains for a rule.
|
|
|
|
|
*
|
|
|
|
|
* Next1/2 always points to the next rule that is watching the same package.
|
|
|
|
|
* The watches array contains rules to start from for each package
|
|
|
|
|
*
|
|
|
|
|
*/
|
|
|
|
|
public function insert(RuleWatchNode $node)
|
|
|
|
|
{
|
|
|
|
|
// skip simple assertions of the form (A) or (-A)
|
|
|
|
|
if ($node->getRule()->isAssertion()) {
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (!isset($this->watches[$node->watch1])) {
|
|
|
|
|
$this->watches[$node->watch1] = null;
|
|
|
|
|
foreach (array($node->watch1, $node->watch2) as $literal) {
|
|
|
|
|
if (!isset($this->watches[$literal])) {
|
|
|
|
|
$this->watches[$literal] = new RuleWatchChain;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
$node->next1 = $this->watches[$node->watch1];
|
|
|
|
|
$this->watches[$node->watch1] = $node;
|
|
|
|
|
|
|
|
|
|
if (!isset($this->watches[$node->watch2])) {
|
|
|
|
|
$this->watches[$node->watch2] = null;
|
|
|
|
|
$this->watches[$literal]->unshift($node);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
$node->next2 = $this->watches[$node->watch2];
|
|
|
|
|
$this->watches[$node->watch2] = $node;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
public function contains($literalId)
|
|
|
|
@ -56,23 +46,15 @@ class RuleWatchGraph
|
|
|
|
|
public function walkLiteral($literalId, $level, $skipCallback, $conflictCallback, $decideCallback)
|
|
|
|
|
{
|
|
|
|
|
if (!isset($this->watches[$literalId])) {
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
$prevNode = null;
|
|
|
|
|
for ($node = $this->watches[$literalId]; $node !== null; $prevNode = $node, $node = $nextNode) {
|
|
|
|
|
$nextNode = $node->getNext($literalId);
|
|
|
|
|
|
|
|
|
|
if ($node->getRule()->isDisabled()) {
|
|
|
|
|
continue;
|
|
|
|
|
return null;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
$this->watches[$literalId]->rewind();
|
|
|
|
|
while ($this->watches[$literalId]->valid()) {
|
|
|
|
|
$node = $this->watches[$literalId]->current();
|
|
|
|
|
$otherWatch = $node->getOtherWatch($literalId);
|
|
|
|
|
|
|
|
|
|
if (call_user_func($skipCallback, $otherWatch)) {
|
|
|
|
|
continue;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (!$node->getRule()->isDisabled() && !call_user_func($skipCallback, $otherWatch)) {
|
|
|
|
|
$ruleLiterals = $node->getRule()->getLiterals();
|
|
|
|
|
|
|
|
|
|
if (sizeof($ruleLiterals) > 2) {
|
|
|
|
@ -80,14 +62,13 @@ class RuleWatchGraph
|
|
|
|
|
if ($otherWatch !== $ruleLiteral->getId() &&
|
|
|
|
|
!call_user_func($conflictCallback, $ruleLiteral->getId())) {
|
|
|
|
|
|
|
|
|
|
$node = $this->moveWatch($literalId, $ruleLiteral->getId(), $prevNode, $node, $nextNode);
|
|
|
|
|
$this->moveWatch($literalId, $ruleLiteral->getId(), $node);
|
|
|
|
|
|
|
|
|
|
continue 2;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// yay, we found a unit clause! try setting it to true
|
|
|
|
|
if (call_user_func($conflictCallback, $otherWatch)) {
|
|
|
|
|
return $node->getRule();
|
|
|
|
|
}
|
|
|
|
@ -95,40 +76,20 @@ class RuleWatchGraph
|
|
|
|
|
call_user_func($decideCallback, $otherWatch, $level, $node->getRule());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
return null;
|
|
|
|
|
$this->watches[$literalId]->next();
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
public function moveWatch($fromLiteral, $toLiteral, $prevNode, $node, $nextNode) {
|
|
|
|
|
if ($fromLiteral == $node->watch1) {
|
|
|
|
|
$node->watch1 = $toLiteral;
|
|
|
|
|
$node->next1 = (isset($this->watches[$toLiteral])) ? $this->watches[$toLiteral] : null;
|
|
|
|
|
} else {
|
|
|
|
|
$node->watch2 = $toLiteral;
|
|
|
|
|
$node->next2 = (isset($this->watches[$toLiteral])) ? $this->watches[$toLiteral] : null;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if ($prevNode) {
|
|
|
|
|
if ($prevNode->next1 === $node) {
|
|
|
|
|
$prevNode->next1 = $nextNode;
|
|
|
|
|
} else {
|
|
|
|
|
$prevNode->next2 = $nextNode;
|
|
|
|
|
}
|
|
|
|
|
} else {
|
|
|
|
|
$this->watches[$fromLiteral] = $nextNode;
|
|
|
|
|
return null;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
$this->watches[$toLiteral] = $node;
|
|
|
|
|
|
|
|
|
|
if ($prevNode) {
|
|
|
|
|
return $prevNode;
|
|
|
|
|
protected function moveWatch($fromLiteral, $toLiteral, $node)
|
|
|
|
|
{
|
|
|
|
|
if (!isset($this->watches[$toLiteral])) {
|
|
|
|
|
$this->watches[$toLiteral] = new RuleWatchChain;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
$tmpNode = new RuleWatchNode(new Rule(array(), null, null));
|
|
|
|
|
$tmpNode->watch1 = $fromLiteral;
|
|
|
|
|
$tmpNode->next1 = $nextNode;
|
|
|
|
|
$tmpNode->watch2 = $fromLiteral;
|
|
|
|
|
$tmpNode->next2 = $nextNode;
|
|
|
|
|
|
|
|
|
|
return $tmpNode;
|
|
|
|
|
$node->moveWatch($fromLiteral, $toLiteral);
|
|
|
|
|
$this->watches[$fromLiteral]->remove();
|
|
|
|
|
$this->watches[$toLiteral]->unshift($node);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|