Commit 4f81cb7a authored by Lonca Emmanuel's avatar Lonca Emmanuel

Added some constraints.

Added another kind of "channel" constraint, and a first "circuit"
constraint.
parent f7f7db28
......@@ -433,7 +433,9 @@ public abstract class AbstractLauncher implements Serializable, ILogAble {
}
protected void flushLog() {
this.out.print(logBuffer.toString());
if (logBuffer != null) {
this.out.print(logBuffer.toString());
}
logBuffer = null;
}
......
......@@ -41,6 +41,22 @@ public class ConnectionCtrBuilder {
this.intensionCtrEncoder = intensionEnc;
}
public boolean buildCtrChannel(String id, XVarInteger[] list, int startIndex, XVarInteger value) {
for(int i=0; i<list.length; ++i) {
final String[] andParts = new String[list.length];
for(int j=0; j<list.length; ++j) {
final String normJ = CtrBuilderUtils.normalizeCspVarName(list[j].id);
andParts[j] = "eq("+normJ+","+(i==j ? 1 : 0)+")";
}
final String andExpr = CtrBuilderUtils.chainExpressionsForAssociativeOp(andParts, "and");
final String expr = "imp(eq("+CtrBuilderUtils.normalizeCspVarName(value.id)+","+(i+startIndex)+"),"+andExpr+")";
if(this.intensionCtrEncoder.encode(expr)) {
return true;
}
}
return false;
}
public boolean buildCtrChannel(String id, XVarInteger[] list1, int startIndex1, XVarInteger[] list2, int startIndex2) {
if(list1.length != list2.length) {
throw new IllegalArgumentException("lists of different sizes provided as arguments of channel constraint");
......
......@@ -19,7 +19,10 @@
package org.sat4j.csp.constraints3;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import org.sat4j.csp.intension.IIntensionCtrEncoder;
import org.sat4j.reader.XMLCSP3Reader;
......@@ -39,8 +42,11 @@ public class SchedulingCtrBuilder {
private final IIntensionCtrEncoder intensionEnc;
public SchedulingCtrBuilder(IIntensionCtrEncoder intensionEnc) {
private final ComparisonCtrBuilder comparisonCtrBuilder;
public SchedulingCtrBuilder(IIntensionCtrEncoder intensionEnc, ComparisonCtrBuilder comparisonCtrBuilder) {
this.intensionEnc = intensionEnc;
this.comparisonCtrBuilder = comparisonCtrBuilder;
}
public boolean buildCtrStretch(String id, XVarInteger[] list, int[] values, int[] widthsMin, int[] widthsMax) {
......@@ -472,4 +478,80 @@ public class SchedulingCtrBuilder {
return false;
}
public boolean buildCtrCircuit(String id, XVarInteger[] list, int startIndex) {
final List<List<Integer>> circuits = buildCircuits(new int[list.length], 0);
final String circuitsExprs[] = new String[circuits.size()];
for(int i=0; i<circuits.size(); ++i) {
final List<Integer> circuit = circuits.get(i);
final String eqExprs[] = new String[circuit.size()];
for(int j=0; j<circuit.size(); ++j) {
final String norm = CtrBuilderUtils.normalizeCspVarName(list[j].id);
eqExprs[j] = "eq("+norm+","+(circuit.get(j)+startIndex)+")";
}
circuitsExprs[i] = CtrBuilderUtils.chainExpressionsForAssociativeOp(eqExprs, "and");
}
final String expr = CtrBuilderUtils.chainExpressionsForAssociativeOp(circuitsExprs, "or");
return this.intensionEnc.encode(expr);
}
private List<List<Integer>> buildCircuits(int[] circuit, int length) {
if(length == circuit.length) {
return returnIfCircuit(circuit);
}
List<List<Integer>> circuits = new ArrayList<>();
for(int i=0; i<circuit.length; ++i) {
boolean mustContinue = false;
for(int j=0; j<length; ++j) {
if(circuit[j] == i) {
mustContinue = true;
break;
}
}
if(mustContinue) {
continue;
}
circuit[length] = i;
circuits.addAll(buildCircuits(circuit, length+1));
}
return circuits;
}
private List<List<Integer>> returnIfCircuit(int[] circuit) {
Set<Integer> visited = new HashSet<>();
int i=0;
for(; i < circuit.length && circuit[i] == i; ++i) {
visited.add(circuit[i]);
}
if(i < circuit.length) {
final int start = i;
visited.add(i);
for(i=circuit[i]; i!=start; i=circuit[i]) {
visited.add(i);
}
i = start;
}
for(; i<circuit.length; ++i) {
if(circuit[i] == i) {
visited.add(i);
}
}
List<List<Integer>> circuits = new ArrayList<>();
if(visited.size() == circuit.length) {
List<Integer> circuitAsList = new ArrayList<>();
Arrays.stream(circuit).forEach(x -> circuitAsList.add(x));
circuits.add(circuitAsList);
}
return circuits;
}
public boolean buildCtrCircuit(String id, XVarInteger[] list, int startIndex, XVarInteger size) {
// TODO Auto-generated method stub
return false;
}
public boolean buildCtrCircuit(String id, XVarInteger[] list, int startIndex, int size) {
// TODO Auto-generated method stub
return false;
}
}
......@@ -138,7 +138,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
this.elementaryCtrBuilder = new ElementaryCtrBuilder(this.intensionEnc);
this.comparisonCtrBuilder = new ComparisonCtrBuilder(this.intensionEnc);
this.connectionCtrBuilder = new ConnectionCtrBuilder(this.intensionEnc);
this.schedulingCtrBuilder = new SchedulingCtrBuilder(this.intensionEnc);
this.schedulingCtrBuilder = new SchedulingCtrBuilder(this.intensionEnc, this.comparisonCtrBuilder);
this.genericCtrBuilder = new GenericCtrBuilder(this.intensionEnc);
this.countingCtrBuilder = new CountingCtrBuilder(this.intensionEnc);
this.languageCtrBuilder = new LanguageCtrBuilder(this.cspToSatEncoder);
......@@ -620,7 +620,7 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
*/
@Override
public void buildCtrChannel(String id, XVarInteger[] list, int startIndex, XVarInteger value) {
unimplementedCase(id); // TODO: check (again) set variables are not supported yet
this.contradictionFound |= this.connectionCtrBuilder.buildCtrChannel(id, list, startIndex, value);
}
/**
......@@ -943,6 +943,23 @@ public class XMLCSP3Reader extends Reader implements XCallbacks2 {
this.contradictionFound |= this.elementaryCtrBuilder.buildCtrClause(id, pos, neg);
}
@Override
public void buildCtrCircuit(String id, XVarInteger[] list, int startIndex, int size) {
unimplementedCase(id); // TODO
// this.contradictionFound |= this.packingCtrBuilder.buildCtrCircuit(id, list, startIndex, size);
}
@Override
public void buildCtrCircuit(String id, XVarInteger[] list, int startIndex, XVarInteger size) {
unimplementedCase(id); // TODO
// this.contradictionFound |= this.packingCtrBuilder.buildCtrCircuit(id, list, startIndex, size);
}
@Override
public void buildCtrCircuit(String id, XVarInteger[] list, int startIndex) {
this.contradictionFound |= this.schedulingCtrBuilder.buildCtrCircuit(id, list, startIndex);
}
public void buildVarSymbolic(XVarSymbolic x, String[] values) {
unimplementedCase(x.id); // TODO
}
......
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