Commit ae418f13 authored by Daniel Le Berre's avatar Daniel Le Berre

Can now detect learned unit clause.

parent e5676273
Pipeline #9086 failed with stages
in 18 minutes and 55 seconds
......@@ -97,7 +97,7 @@ public class MixedDataStructureDanielHT extends AbstractDataStructureFactory {
public Constr createUnregisteredClause(IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, getVocabulary());
......
......@@ -95,7 +95,7 @@ public class MixedDataStructureDanielWL extends AbstractDataStructureFactory {
public Constr createUnregisteredClause(IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, getVocabulary());
......
......@@ -46,8 +46,8 @@ import org.sat4j.specs.IVecInt;
* @author leberre
* @since 2.1
*/
public class MixedDataStructureDanielWLConciseBinary extends
AbstractDataStructureFactory {
public class MixedDataStructureDanielWLConciseBinary
extends AbstractDataStructureFactory {
private BinaryClauses[] binaryClauses;
......@@ -126,7 +126,7 @@ public class MixedDataStructureDanielWLConciseBinary extends
public Constr createUnregisteredClause(IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, getVocabulary());
......
......@@ -49,8 +49,15 @@ public class UnitClause implements Constr {
protected final int literal;
protected double activity;
private boolean learnt;
public UnitClause(int value) {
this(value, false);
}
public UnitClause(int value, boolean learnt) {
this.literal = value;
this.learnt = learnt;
}
public void assertConstraint(UnitPropagationListener s) {
......@@ -100,7 +107,7 @@ public class UnitClause implements Constr {
}
public void setLearnt() {
throw new UnsupportedOperationException();
learnt = true;
}
public boolean simplify() {
......@@ -119,7 +126,7 @@ public class UnitClause implements Constr {
}
public boolean learnt() {
return false;
return learnt;
}
public int size() {
......
......@@ -189,7 +189,7 @@ public abstract class AbstractPBDataStructureFactory
public Constr createUnregisteredClause(IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, getVocabulary());
......
......@@ -58,7 +58,7 @@ public class UnitBinaryHTClauseConstructor implements IClauseConstructor {
public Constr constructLearntClause(ILits voc, IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, voc);
......
......@@ -58,7 +58,7 @@ public class UnitBinaryHTClausePBConstructor implements IClauseConstructor {
public Constr constructLearntClause(ILits voc, IVecInt literals) {
if (literals.size() == 1) {
return new UnitClausePB(literals.last(), voc);
return new UnitClausePB(literals.last(), true, voc);
}
if (literals.size() == 2) {
return new LearntBinaryClausePB(literals, voc);
......
......@@ -58,7 +58,7 @@ public class UnitBinaryWLClauseConstructor implements IClauseConstructor {
public Constr constructLearntClause(ILits voc, IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, voc);
......
......@@ -39,7 +39,8 @@ import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.UnitPropagationListener;
public class UnitConciseBinaryWLClauseConstructor implements IClauseConstructor {
public class UnitConciseBinaryWLClauseConstructor
implements IClauseConstructor {
private BinaryClauses[] binaryClauses;
......@@ -64,7 +65,8 @@ public class UnitConciseBinaryWLClauseConstructor implements IClauseConstructor
if (binaryClauses == null) {
binaryClauses = new BinaryClauses[voc.nVars() * 2 + 2];
} else if (binaryClauses.length < voc.nVars() * 2 + 1) {
BinaryClauses[] newBinaryClauses = new BinaryClauses[voc.nVars() * 2 + 2];
BinaryClauses[] newBinaryClauses = new BinaryClauses[voc.nVars() * 2
+ 2];
System.arraycopy(binaryClauses, 0, newBinaryClauses, 0,
binaryClauses.length);
binaryClauses = newBinaryClauses;
......@@ -90,7 +92,7 @@ public class UnitConciseBinaryWLClauseConstructor implements IClauseConstructor
public Constr constructLearntClause(ILits voc, IVecInt literals) {
if (literals.size() == 1) {
return new UnitClause(literals.last());
return new UnitClause(literals.last(), true);
}
if (literals.size() == 2) {
return new LearntBinaryClause(literals, voc);
......
......@@ -45,6 +45,11 @@ public final class UnitClausePB extends UnitClause implements PBConstr {
this.voc = voc;
}
public UnitClausePB(int value, boolean learnt, ILits voc) {
super(value, learnt);
this.voc = voc;
}
/**
*
*/
......
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