Merge a5de052 into ba5b113

src/main/java/proof/data/CrossingIndex.java

@@ -1,5 +1,7 @@
 package proof.data;
 
+import java.util.Arrays;
+
 /**
  * Represents a single crossing by two edge segments.
  * 
@@ -44,4 +46,9 @@ public boolean equals(Object other) {
   public int hashCode() {
     return segments[0].hashCode() + segments[1].hashCode();
   }
+
+  @Override
+  public String toString() {
+    return Arrays.toString(segments);
+  }
 }

src/main/java/proof/data/Graph.java

@@ -0,0 +1,165 @@
+package proof.data;
+
+import java.util.Map;
+
+import proof.exception.InvalidGraphException;
+
+/**
+ * Maintains a graph.
+ *
+ * Represents a graph by an adjacency matrix. Requires nodes to be indexed continuously.
+ *
+ * @author Tilo Wiedera
+ *
+ */
+public class Graph {
+
+  private final int[][] edgeIndices;
+  private final double[] costs;
+  private boolean immutable;
+
+  public final static int NO_EDGE = -1;
+  public final static double NO_EDGE_COST = Double.MAX_VALUE;
+
+  /**
+   * Creates a new graph with the exact number of nodes and edges.
+   *
+   * @param numberOfNodes The number of nodes
+   *
+   * @param numberOfEdges The number of edges
+   */
+  public Graph(int numberOfNodes, int numberOfEdges) {
+    immutable = false;
+
+    costs = new double[numberOfEdges];
+    edgeIndices = new int[numberOfNodes][numberOfNodes];
+
+    for (int i = 0; i < numberOfEdges; i++) {
+      costs[i] = NO_EDGE_COST;
+    }
+
+    for (int i = 0; i < numberOfNodes; i++) {
+      for (int ii = 0; ii < numberOfNodes; ii++) {
+        edgeIndices[i][ii] = NO_EDGE;
+      }
+    }
+  }
+
+  /**
+   * Checks whether a single edge exists (or its directed counterpart).
+   *
+   * @param source The index of the first node
+   * @param target The index of the second node
+   *
+   * @return {@code true} iff the edge exist
+   */
+  public boolean edgeExists(int source, int target) {
+    return source >= 0 && source < edgeIndices.length && target >= 0 && target < edgeIndices.length
+        && edgeIndices[source][target] != NO_EDGE;
+  }
+
+  /**
+   * Returns the id of any single edge.
+   *
+   * @param source The index of the first node
+   * @param target The index of the second node
+   *
+   * @return The index of the edge
+   */
+  public int getEdgeId(int source, int target) {
+    if (!edgeExists(source, target)) {
+      throw new IllegalArgumentException("Edge does not exist!");
+    }
+
+    return edgeIndices[source][target];
+  }
+
+  /**
+   * Returns the cost of a single edge
+   *
+   * @param source The index of the first node
+   * @param target The index of the second node
+   *
+   * @return The cost
+   */
+  public double getEdgeCost(int source, int target) {
+    return costs[getEdgeId(source, target)];
+  }
+
+  /**
+   * Creates a new edge.
+   *
+   * Will fail if the index is already in use or the edge already exists.
+   *
+   * @param edgeId The edge index to be used
+   * @param source The index of the first node
+   * @param target The index of the second node
+   * @param cost The cost of the edge
+   */
+  public void addEdge(int edgeId, int source, int target, double cost) {
+    if (immutable) {
+      throw new UnsupportedOperationException("Can not modify immutable graph");
+    }
+
+    if (edgeExists(source, target)) {
+      throw new IllegalArgumentException("Can not override existing edge!");
+    }
+
+    if (edgeId < 0 || edgeId >= costs.length) {
+      throw new IllegalArgumentException("Edge index out of bounds: " + edgeId);
+    }
+
+    if (source < 0 || source >= edgeIndices.length) {
+      throw new IllegalArgumentException("Source index out of bounds: " + source);
+    }
+
+    if (target < 0 || target >= edgeIndices.length) {
+      throw new IllegalArgumentException("Target index out of bounds: " + target);
+    }
+
+    if (costs[edgeId] != NO_EDGE_COST) {
+      throw new IllegalArgumentException("Edge ID already exists!");
+    }
+
+    costs[edgeId] = cost;
+    edgeIndices[source][target] = edgeIndices[target][source] = edgeId;
+  }
+
+  /**
+   * Makes this graph immutable.
+   *
+   * Future calls of {@code addEdge} will throw an {@link UnsupportedOperationException}.
+   *
+   * @throws InvalidGraphException Iff not all edges have been set
+   */
+  public void makeImmutable() throws InvalidGraphException {
+    immutable = true;
+
+    // validate all edges have been inserted
+    int counter = 0;
+    for (int i = 0; i < edgeIndices.length; i++) {
+      for (int ii = 0; ii < edgeIndices.length; ii++) {
+        if (edgeIndices[i][ii] != NO_EDGE) {
+          counter++;
+        }
+      }
+    }
+
+    if (counter != 2 * costs.length) {
+      throw new InvalidGraphException("Can not make incomplete graph immutable");
+    }
+  }
+
+  /**
+   * Validates a variable assignment.
+   *
+   * Checks there are no crossings that require more than {@numberOfSegments}
+   * crossings per edge.
+   *
+   * @param vars The variable assigment
+   * @param numberOfSegments The maximum number of crossings per edge
+   */
+  public void validateVariables(Map<CrossingIndex, Boolean> vars, int numberOfSegments) {
+    // TODO
+  }
+}

src/main/java/proof/data/SegmentIndex.java

@@ -42,4 +42,9 @@ public boolean equals(Object other) {
   public int hashCode() {
     return edge + segment;
   }
+
+  @Override
+  public String toString() {
+    return "(" + edge + "," + segment + ")";
+  }
 }

src/main/java/proof/data/reader/ArrayReader.java

@@ -0,0 +1,8 @@
+package proof.data.reader;
+
+import org.json.JSONArray;
+
+public interface ArrayReader {
+
+  public Object read(JSONArray input);
+}

src/main/java/proof/data/reader/CrossingReader.java

@@ -0,0 +1,15 @@
+package proof.data.reader;
+
+import org.json.JSONArray;
+
+import proof.data.CrossingIndex;
+
+public class CrossingReader implements ArrayReader {
+  private final static SegmentReader SEGMENT_READER = new SegmentReader();
+
+  @Override
+  public CrossingIndex read(JSONArray input) {
+    return new CrossingIndex(SEGMENT_READER.read(input.getJSONObject(0)), SEGMENT_READER.read(input
+        .getJSONObject(1)));
+  }
+}

src/main/java/proof/data/reader/GraphReader.java

@@ -0,0 +1,38 @@
+package proof.data.reader;
+
+import org.json.JSONArray;
+import org.json.JSONException;
+import org.json.JSONObject;
+
+import proof.data.Graph;
+import proof.exception.InvalidGraphException;
+
+public class GraphReader implements ObjectReader {
+
+  @Override
+  public Graph read(JSONObject input) {
+    try {
+      int numberOfNodes = input.getInt("numberOfNodes");
+
+      JSONArray edges = input.getJSONArray("edges");
+
+      Graph result = new Graph(numberOfNodes, edges.length());
+
+      for (int i = 0; i < edges.length(); i++) {
+        JSONObject edge = edges.getJSONObject(i);
+
+        result.addEdge(edge.getInt("id"), edge.getInt("source"), edge.getInt("target"),
+            edge.getDouble("cost"));
+      }
+
+      result.makeImmutable();
+
+      return result;
+
+    } catch (IllegalArgumentException | JSONException e) {
+      InvalidGraphException exception = new InvalidGraphException("Could not parse JSON");
+      exception.initCause(e);
+      throw exception;
+    }
+  }
+}

src/main/java/proof/data/reader/ObjectReader.java

@@ -0,0 +1,8 @@
+package proof.data.reader;
+
+import org.json.JSONObject;
+
+public interface ObjectReader {
+
+  public Object read(JSONObject input);
+}

src/main/java/proof/data/reader/SegmentReader.java

@@ -0,0 +1,13 @@
+package proof.data.reader;
+
+import org.json.JSONObject;
+
+import proof.data.SegmentIndex;
+
+public class SegmentReader implements ObjectReader {
+
+  @Override
+  public SegmentIndex read(JSONObject input) {
+    return new SegmentIndex(input.getInt("edge"), input.getInt("segment"));
+  }
+}

src/main/java/proof/exception/InvalidConstraintException.java

@@ -0,0 +1,8 @@
+package proof.exception;
+
+public class InvalidConstraintException extends InvalidProofException {
+
+  public InvalidConstraintException(String description) {
+    super(description);
+  }
+}

src/main/java/proof/exception/InvalidGraphException.java

@@ -0,0 +1,9 @@
+package proof.exception;
+
+public class InvalidGraphException extends RuntimeException {
+
+  public InvalidGraphException(String description) {
+    super(description);
+  }
+
+}

src/main/java/proof/exception/InvalidPathException.java

@@ -0,0 +1,9 @@
+package proof.exception;
+
+public class InvalidPathException extends InvalidProofException {
+
+  public InvalidPathException(String description) {
+    super(description);
+  }
+
+}

src/main/java/proof/validator/BranchCoverage.java → src/main/java/proof/validator/BranchCoverageValidator.java

@@ -12,32 +12,35 @@
 import org.json.JSONObject;
 
 import proof.data.CrossingIndex;
-import proof.data.SegmentIndex;
+import proof.data.reader.CrossingReader;
 import proof.exception.InvalidCoverageException;
+import proof.validator.base.ObjectValidator;
 
 /**
  * Validates the fixed variables of all leaves.
- * 
+ *
  * The set of all leaves must completely cover the problem at hand. This means, every possible
  * configuration of variables must be met. The {@code BranchCoverage}-Validator will ensure that no
  * variable configuration is missing and that there are no ambiguities caused by multiple leaves
  * reporting the same or overlapping configurations.
- * 
+ *
  * @author Tilo Wiedera
  *
  */
-public class BranchCoverage implements Validator {
+public class BranchCoverageValidator implements ObjectValidator {
+
+  private final static CrossingReader CROSSING_READER = new CrossingReader();
 
   /**
    * Used to sort the leaves in descending number of branching variables.
    */
   final static Comparator<Map<CrossingIndex, Boolean>> LEAF_COMPARATOR =
       new Comparator<Map<CrossingIndex, Boolean>>() {
-        @Override
-        public int compare(Map<CrossingIndex, Boolean> vars1, Map<CrossingIndex, Boolean> vars2) {
-          return vars2.size() - vars1.size();
-        }
-      };
+    @Override
+    public int compare(Map<CrossingIndex, Boolean> vars1, Map<CrossingIndex, Boolean> vars2) {
+      return vars2.size() - vars1.size();
+    }
+  };
 
   @Override
   public void validate(JSONObject object) throws InvalidCoverageException {
@@ -55,15 +58,9 @@ public void validate(JSONObject object) throws InvalidCoverageException {
       for (int j = 0; j < fixedVariables.length(); j++) {
         JSONObject variable = fixedVariables.getJSONObject(j);
 
-        JSONArray segments = variable.getJSONArray("segments");
-        JSONObject s1 = segments.getJSONObject(0);
-        JSONObject s2 = segments.getJSONObject(1);
-
         try {
-          variablesOfLeaf.put(
-              new CrossingIndex(new SegmentIndex(s1.getInt("edge"), s1.getInt("segment")),
-                  new SegmentIndex(s2.getInt("edge"), s2.getInt("segment"))), variable
-                  .getInt("value") == 1);
+          variablesOfLeaf.put(CROSSING_READER.read(variable.getJSONArray("segments")),
+              variable.getInt("value") == 1);
         } catch (IllegalArgumentException e) {
           throw new InvalidCoverageException("Encountered invalid variable indices.");
         }
@@ -102,7 +99,7 @@ public void validate(JSONObject object) throws InvalidCoverageException {
   /**
    * Tries to merge the leaves contained at {@code i} and {@code j}. The leaves will be merged if
    * they differ by the assignment of a single variable.
-   * 
+   *
    * @param leaves The list of all leaves
    * @param i The first leaf index
    * @param j The second leaf index