DecisionQueueFree is no longer needed
parent
2fbc04b950
commit
5b1a48663e
|
@ -25,7 +25,6 @@ class Decisions implements \Iterator, \Countable
|
||||||
protected $pool;
|
protected $pool;
|
||||||
protected $decisionMap;
|
protected $decisionMap;
|
||||||
protected $decisionQueue = array();
|
protected $decisionQueue = array();
|
||||||
protected $decisionQueueFree = array();
|
|
||||||
|
|
||||||
public function __construct($pool)
|
public function __construct($pool)
|
||||||
{
|
{
|
||||||
|
@ -38,37 +37,13 @@ class Decisions implements \Iterator, \Countable
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
protected function addDecision($literal, $level)
|
public function decide($literal, $level, $why)
|
||||||
{
|
|
||||||
$packageId = abs($literal);
|
|
||||||
|
|
||||||
$previousDecision = $this->decisionMap[$packageId];
|
|
||||||
if ($previousDecision != 0) {
|
|
||||||
$literalString = $this->pool->literalToString($literal);
|
|
||||||
$package = $this->pool->literalToPackage($literal);
|
|
||||||
throw new SolverBugException(
|
|
||||||
"Trying to decide $literalString on level $level, even though $package was previously decided as ".(int) $previousDecision."."
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
if ($literal > 0) {
|
|
||||||
$this->decisionMap[$packageId] = $level;
|
|
||||||
} else {
|
|
||||||
$this->decisionMap[$packageId] = -$level;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
public function decide($literal, $level, $why, $addToFreeQueue = false)
|
|
||||||
{
|
{
|
||||||
$this->addDecision($literal, $level);
|
$this->addDecision($literal, $level);
|
||||||
$this->decisionQueue[] = array(
|
$this->decisionQueue[] = array(
|
||||||
self::DECISION_LITERAL => $literal,
|
self::DECISION_LITERAL => $literal,
|
||||||
self::DECISION_REASON => $why,
|
self::DECISION_REASON => $why,
|
||||||
);
|
);
|
||||||
|
|
||||||
if ($addToFreeQueue) {
|
|
||||||
$this->decisionQueueFree[count($this->decisionQueue) - 1] = true;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
public function contain($literal)
|
public function contain($literal)
|
||||||
|
@ -159,15 +134,12 @@ class Decisions implements \Iterator, \Countable
|
||||||
while ($decision = array_pop($this->decisionQueue)) {
|
while ($decision = array_pop($this->decisionQueue)) {
|
||||||
$this->decisionMap[abs($decision[self::DECISION_LITERAL])] = 0;
|
$this->decisionMap[abs($decision[self::DECISION_LITERAL])] = 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
$this->decisionQueueFree = array();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
public function resetToOffset($offset)
|
public function resetToOffset($offset)
|
||||||
{
|
{
|
||||||
while (count($this->decisionQueue) > $offset + 1) {
|
while (count($this->decisionQueue) > $offset + 1) {
|
||||||
$decision = array_pop($this->decisionQueue);
|
$decision = array_pop($this->decisionQueue);
|
||||||
unset($this->decisionQueueFree[count($this->decisionQueue)]);
|
|
||||||
$this->decisionMap[abs($decision[self::DECISION_LITERAL])] = 0;
|
$this->decisionMap[abs($decision[self::DECISION_LITERAL])] = 0;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -212,4 +184,24 @@ class Decisions implements \Iterator, \Countable
|
||||||
{
|
{
|
||||||
return count($this->decisionQueue) === 0;
|
return count($this->decisionQueue) === 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
protected function addDecision($literal, $level)
|
||||||
|
{
|
||||||
|
$packageId = abs($literal);
|
||||||
|
|
||||||
|
$previousDecision = $this->decisionMap[$packageId];
|
||||||
|
if ($previousDecision != 0) {
|
||||||
|
$literalString = $this->pool->literalToString($literal);
|
||||||
|
$package = $this->pool->literalToPackage($literal);
|
||||||
|
throw new SolverBugException(
|
||||||
|
"Trying to decide $literalString on level $level, even though $package was previously decided as ".(int) $previousDecision."."
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
if ($literal > 0) {
|
||||||
|
$this->decisionMap[$packageId] = $level;
|
||||||
|
} else {
|
||||||
|
$this->decisionMap[$packageId] = -$level;
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -275,7 +275,7 @@ class Solver
|
||||||
{
|
{
|
||||||
$level++;
|
$level++;
|
||||||
|
|
||||||
$this->decisions->decide($literal, $level, $rule, true);
|
$this->decisions->decide($literal, $level, $rule);
|
||||||
|
|
||||||
while (true) {
|
while (true) {
|
||||||
$rule = $this->propagate($level);
|
$rule = $this->propagate($level);
|
||||||
|
|
Loading…
Reference in New Issue