Commit 2af496d0 authored by leberre's avatar leberre

The head literal cannot be set in the PB learnt constraints constructor...

The head literal cannot be set in the PB learnt constraints constructor because at that point, all the literals might be assigned.

That must be done in the assertConstraint method.
 

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@362 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 0f405bad
......@@ -31,6 +31,7 @@ import java.math.BigInteger;
import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.UnitPropagationListener;
import org.sat4j.specs.IVecInt;
public class LearntBinaryClausePB extends LearntBinaryClause implements
......@@ -38,7 +39,6 @@ public class LearntBinaryClausePB extends LearntBinaryClause implements
public LearntBinaryClausePB(IVecInt ps, ILits voc) {
super(ps, voc);
// TODO Auto-generated constructor stub
}
/**
......@@ -65,4 +65,14 @@ public class LearntBinaryClausePB extends LearntBinaryClause implements
return BigInteger.ONE;
}
@Override
public void assertConstraint(UnitPropagationListener s) {
if (getVocabulary().isUnassigned(head)) {
s.enqueue(head, this);
} else {
assert getVocabulary().isUnassigned(tail);
s.enqueue(tail, this);
}
}
}
......@@ -31,6 +31,7 @@ import java.math.BigInteger;
import org.sat4j.minisat.constraints.cnf.LearntHTClause;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.UnitPropagationListener;
import org.sat4j.specs.IVecInt;
public class LearntHTClausePB extends LearntHTClause implements PBConstr {
......@@ -39,17 +40,26 @@ public class LearntHTClausePB extends LearntHTClause implements PBConstr {
public LearntHTClausePB(IVecInt ps, ILits voc) {
super(ps, voc);
// mettre en bonnes positions head et tail
for (int i = 0; i < size(); i++)
if (getVocabulary().isUnassigned(get(i))) {
head = ps.get(i);
break;
}
}
// @Override
// public void assertConstraint(UnitPropagationListener s) {
// }
@Override
public void assertConstraint(UnitPropagationListener s) {
if (getVocabulary().isUnassigned(head)) {
s.enqueue(head, this);
} else if (getVocabulary().isUnassigned(tail)) {
s.enqueue(tail, this);
} else {
for (int i = 0; i < middleLits.length; i++) {
if (getVocabulary().isUnassigned(middleLits[i])) {
int temp = middleLits[i];
middleLits[i] = head;
head = temp;
s.enqueue(temp, this);
break;
}
}
}
}
public IVecInt computeAnImpliedClause() {
return null;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment