|
|
@ -62,7 +62,7 @@ class Solver
|
|
|
|
continue;
|
|
|
|
continue;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
$literals = $rule->getLiterals();
|
|
|
|
$literals = $rule->literals;
|
|
|
|
$literal = $literals[0];
|
|
|
|
$literal = $literals[0];
|
|
|
|
|
|
|
|
|
|
|
|
if (!$this->decisions->decided(abs($literal))) {
|
|
|
|
if (!$this->decisions->decided(abs($literal))) {
|
|
|
@ -104,7 +104,7 @@ class Solver
|
|
|
|
continue;
|
|
|
|
continue;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
$assertRuleLiterals = $assertRule->getLiterals();
|
|
|
|
$assertRuleLiterals = $assertRule->literals;
|
|
|
|
$assertRuleLiteral = $assertRuleLiterals[0];
|
|
|
|
$assertRuleLiteral = $assertRuleLiterals[0];
|
|
|
|
|
|
|
|
|
|
|
|
if (abs($literal) !== abs($assertRuleLiteral)) {
|
|
|
|
if (abs($literal) !== abs($assertRuleLiteral)) {
|
|
|
@ -356,7 +356,7 @@ class Solver
|
|
|
|
while (true) {
|
|
|
|
while (true) {
|
|
|
|
$this->learnedPool[count($this->learnedPool) - 1][] = $rule;
|
|
|
|
$this->learnedPool[count($this->learnedPool) - 1][] = $rule;
|
|
|
|
|
|
|
|
|
|
|
|
foreach ($rule->getLiterals() as $literal) {
|
|
|
|
foreach ($rule->literals as $literal) {
|
|
|
|
// skip the one true literal
|
|
|
|
// skip the one true literal
|
|
|
|
if ($this->decisions->satisfy($literal)) {
|
|
|
|
if ($this->decisions->satisfy($literal)) {
|
|
|
|
continue;
|
|
|
|
continue;
|
|
|
@ -480,7 +480,7 @@ class Solver
|
|
|
|
$this->problems[] = $problem;
|
|
|
|
$this->problems[] = $problem;
|
|
|
|
|
|
|
|
|
|
|
|
$seen = array();
|
|
|
|
$seen = array();
|
|
|
|
$literals = $conflictRule->getLiterals();
|
|
|
|
$literals = $conflictRule->literals;
|
|
|
|
|
|
|
|
|
|
|
|
foreach ($literals as $literal) {
|
|
|
|
foreach ($literals as $literal) {
|
|
|
|
// skip the one true literal
|
|
|
|
// skip the one true literal
|
|
|
@ -503,7 +503,7 @@ class Solver
|
|
|
|
$problem->addRule($why);
|
|
|
|
$problem->addRule($why);
|
|
|
|
$this->analyzeUnsolvableRule($problem, $why);
|
|
|
|
$this->analyzeUnsolvableRule($problem, $why);
|
|
|
|
|
|
|
|
|
|
|
|
$literals = $why->getLiterals();
|
|
|
|
$literals = $why->literals;
|
|
|
|
|
|
|
|
|
|
|
|
foreach ($literals as $literal) {
|
|
|
|
foreach ($literals as $literal) {
|
|
|
|
// skip the one true literal
|
|
|
|
// skip the one true literal
|
|
|
@ -627,7 +627,7 @@ class Solver
|
|
|
|
$decisionQueue = array();
|
|
|
|
$decisionQueue = array();
|
|
|
|
$noneSatisfied = true;
|
|
|
|
$noneSatisfied = true;
|
|
|
|
|
|
|
|
|
|
|
|
foreach ($rule->getLiterals() as $literal) {
|
|
|
|
foreach ($rule->literals as $literal) {
|
|
|
|
if ($this->decisions->satisfy($literal)) {
|
|
|
|
if ($this->decisions->satisfy($literal)) {
|
|
|
|
$noneSatisfied = false;
|
|
|
|
$noneSatisfied = false;
|
|
|
|
break;
|
|
|
|
break;
|
|
|
@ -688,7 +688,7 @@ class Solver
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
$rule = $this->rules->ruleById($i);
|
|
|
|
$rule = $this->rules->ruleById($i);
|
|
|
|
$literals = $rule->getLiterals();
|
|
|
|
$literals = $rule->literals;
|
|
|
|
|
|
|
|
|
|
|
|
if ($rule->isDisabled()) {
|
|
|
|
if ($rule->isDisabled()) {
|
|
|
|
continue;
|
|
|
|
continue;
|
|
|
|