fix pareto search for lexicographic PVS product

source-code/java/pom.xml

@@ -150,7 +150,7 @@
 					</execution>
 				</executions>
 			</plugin>
-        </plugins>
+		</plugins>
 
 	</build>
 	<dependencies>

source-code/java/src/isse/mbr/tools/execution/MiniBrassRunner.java

@@ -2,14 +2,18 @@
 
 import isse.mbr.parsing.MiniBrassCompiler;
 import isse.mbr.parsing.MiniBrassParseException;
+import org.apache.commons.lang3.stream.Streams;
 
 import java.io.File;
 import java.io.IOException;
-import java.util.Collection;
 import java.util.Collections;
+import java.util.HashSet;
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Random;
+import java.util.Set;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 /**
  * The MiniBrass runner is responsible for executing branch-and-bound or other
@@ -52,21 +56,52 @@ private void initializeBranchAndBound(File miniZincFile) throws IOException {
 		miniBrassCompiler.setMinizincOnly(true);
 	}
 
-	public Collection<MiniZincSolution> executeBranchAndBoundWithParetoOptima(File miniZincFile, File miniBrassFile, List<File> dataFiles)
+	public Set<MiniZincSolution> executeBranchAndBoundWithParetoOptima(File miniZincFile, File miniBrassFile, List<File> dataFiles)
 			throws MiniBrassParseException, IOException {
-		// find single optimal solution
-		MiniZincSolution solution = executeBranchAndBound(miniZincFile, miniBrassFile, dataFiles);
-		if (solution == null) return Collections.emptySet();
+		// initialize
+		initializeBranchAndBound(miniZincFile);
+		MiniBrassPostProcessor postProcessor = new MiniBrassPostProcessor();
 
-		// find the other solutions that are equally good
-		workingModelManager.replaceModel(lastSolvableMiniZincModel);
+		// parse and compile MiniBrass
+		String compiledMiniBrassCode = miniBrassCompiler.compileInMemory(miniBrassFile);
+		// for domination search
+		String getBetterConstraint = miniBrassCompiler.getUnderlyingParser().getLastModel().getDereferencedSolveInstance().getGeneratedBetterPredicate();
+
+		// search for solutions
+		workingModelManager.appendToModel(compiledMiniBrassCode);
 		miniZincRunner.getConfiguration().setUseAllSolutions(true);
-		MiniZincResult result = runMiniZinc(workingModelManager.getFile(), dataFiles);
-		miniZincRunner.getConfiguration().setUseAllSolutions(false);
+		MiniZincResult initialResult = runMiniZinc(workingModelManager.getFile(), dataFiles);
+		Set<MiniZincSolution> solutions;
+		if (initialResult.isSolvedAndValid()) {
+			Set<MiniZincSolution> seenSolutions = new HashSet<>(); // do not inline or a new set is created for each solution
+			String model = workingModelManager.getModel(); // do not inline – result may differ because working model is modified
+			solutions = Streams.stream(initialResult.getSolutions())
+					.map(s -> findParetoOptimaForSolution(model, dataFiles, s, getBetterConstraint, postProcessor, seenSolutions))
+					.stream().flatMap(s -> s)
+					.collect(Collectors.toSet());
+		} else {
+			solutions = Collections.emptySet();
+		}
+
+		// cleanup and finish
 		workingModelManager.cleanup();
+		return solutions;
+	}
 
-		// interpret result and return solutions
-		return result.isSolvedAndValid() ? result.getSolutions() : Collections.emptySet();
+	private Stream<MiniZincSolution> findParetoOptimaForSolution(String parentModel, List<File> dataFiles,
+	                                                             MiniZincSolution parentSolution, String getBetterConstraint,
+	                                                             MiniBrassPostProcessor postProcessor, Set<MiniZincSolution> seenSolutions)
+			throws IOException {
+		String updatedConstraint = "constraint " + postProcessor.processSolution(getBetterConstraint, parentSolution) + ";";
+		workingModelManager.replaceModel(parentModel);
+		workingModelManager.appendToModel(updatedConstraint);
+		String ownModel = workingModelManager.getModel();
+		MiniZincResult result = runMiniZinc(workingModelManager.getFile(), dataFiles);
+		if (!result.isSolvedAndValid()) return Stream.of(parentSolution);
+		return Streams.stream(result.getSolutions())
+				.filter(seenSolutions::add) // ignore all solutions already seen, and ignore new solutions in the future
+				.map(s -> findParetoOptimaForSolution(ownModel, dataFiles, s, getBetterConstraint, postProcessor, seenSolutions))
+				.stream().flatMap(s -> s);
 	}
 
 	public MiniZincSolution executeBranchAndBound(File miniZincFile, File miniBrassFile, List<File> dataFiles)
@@ -84,6 +119,7 @@ public MiniZincSolution executeBranchAndBound(File miniZincFile, File miniBrassF
 
 		// search for solutions
 		workingModelManager.appendToModel(compiledMiniBrassCode);
+		miniZincRunner.getConfiguration().setUseAllSolutions(false);
 		while ((solution = findNextSolution(workingModelManager.getFile(), dataFiles)) != null) {
 			lastSolvableMiniZincModel = workingModelManager.getModel();
 
@@ -130,7 +166,6 @@ public MiniZincConfiguration getMiniZincRunnerConfiguration() {
 	}
 
 	public void setMiniZincConfiguration(MiniZincConfiguration configuration) {
-		configuration.setUseAllSolutions(false);
 		miniZincRunner.setConfiguration(configuration);
 	}
 
@@ -167,5 +202,4 @@ public void setInitialRandomSeed(int initialRandomSeed) {
 	public void setTimeoutInSeconds(Integer timeout) {
 		this.timeoutInSeconds = timeout;
 	}
-
 }

source-code/java/src/isse/mbr/tools/execution/MiniZincSolution.java

@@ -7,6 +7,8 @@
 
 import isse.mbr.parsing.DznParser;
 import isse.mbr.parsing.MiniBrassParseException;
+import org.apache.commons.lang3.builder.EqualsBuilder;
+import org.apache.commons.lang3.builder.HashCodeBuilder;
 
 /**
  * Represents a particular MiniZinc solution
@@ -16,26 +18,26 @@
 public class MiniZincSolution {
 
 	private Map<String, MiniZincVariable> variableStore;
-	
+
 	// internal data structures
 	private String rawDznSolution;
 	private StringBuilder rawDznSolutionBuilder;
 	private DznParser dznParser;
-	
+
 	public MiniZincSolution() {
 		rawDznSolutionBuilder = new StringBuilder();
 		variableStore = new HashMap<>();
 		dznParser = new DznParser();
 	}
-	
+
 	/**
 	 * A line of the current solution in the dzn format
 	 * @param plainSolutionLine
 	 */
 	public void processSolutionLine(String plainSolutionLine) {
 		rawDznSolutionBuilder.append(plainSolutionLine);
 		rawDznSolutionBuilder.append("\n");
-		MiniZincVariable nextVariable = null; 
+		MiniZincVariable nextVariable = null;
 		try {
 			nextVariable = dznParser.parseVariable(plainSolutionLine.trim());
 		} catch (MiniBrassParseException e) {
@@ -47,16 +49,37 @@ public void processSolutionLine(String plainSolutionLine) {
 	public void flush() {
 		rawDznSolution = rawDznSolutionBuilder.toString();
 	}
-	
+
 	public String getRawDznSolution() {
 		return rawDznSolution;
 	}
-	
+
 	public List<MiniZincVariable> getAllVariables() {
 		return new ArrayList<MiniZincVariable>(variableStore.values());
 	}
-	
+
 	public MiniZincVariable getVariable(String key) {
 		return variableStore.get(key);
 	}
+
+	@Override
+	public boolean equals(Object o) {
+		if (this == o) return true;
+
+		if (o == null || getClass() != o.getClass()) return false;
+
+		MiniZincSolution solution = (MiniZincSolution) o;
+
+		return new EqualsBuilder().append(variableStore, solution.variableStore).isEquals();
+	}
+
+	@Override
+	public int hashCode() {
+		return new HashCodeBuilder(17, 37).append(variableStore).toHashCode();
+	}
+
+	@Override
+	public String toString() {
+		return rawDznSolution;
+	}
 }

source-code/java/src/isse/mbr/tools/execution/MiniZincVariable.java

@@ -1,6 +1,8 @@
 package isse.mbr.tools.execution;
 
 import isse.mbr.model.types.MiniZincParType;
+import org.apache.commons.lang3.builder.EqualsBuilder;
+import org.apache.commons.lang3.builder.HashCodeBuilder;
 
 public class MiniZincVariable {
 	private MiniZincParType type;
@@ -49,4 +51,22 @@ public String getMznExpression() {
 	public void setMznExpression(String mznExpression) {
 		this.mznExpression = mznExpression;
 	}
+
+	@Override
+	public boolean equals(Object o) {
+		if (this == o) return true;
+
+		if (o == null || getClass() != o.getClass()) return false;
+
+		MiniZincVariable that = (MiniZincVariable) o;
+
+		return new EqualsBuilder()
+				.append(mznExpression, that.mznExpression)
+				.isEquals();
+	}
+
+	@Override
+	public int hashCode() {
+		return new HashCodeBuilder(17, 37).append(mznExpression).toHashCode();
+	}
 }

source-code/java/src/isse/mbr/tools/execution/WorkingModelManager.java

@@ -3,6 +3,7 @@
 import org.apache.commons.io.FileUtils;
 import org.apache.commons.io.FilenameUtils;
 
+import java.io.Closeable;
 import java.io.File;
 import java.io.FileWriter;
 import java.io.IOException;
@@ -15,7 +16,7 @@
  *
  * @author Elias
  */
-public class WorkingModelManager {
+public class WorkingModelManager implements AutoCloseable {
 	private File file;
 	private String model;
 	private final boolean writeIntermediateFiles;
@@ -101,4 +102,9 @@ public File getFile() {
 	public String getModel() {
 		return model;
 	}
+
+	@Override
+	public void close() throws Exception {
+		cleanup();
+	}
 }