Diffcursor fixes & continuous hash provider compare service.

6 files changed, 159 insertions, 54 deletions

diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/ContinousHashProvider.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/ContinousHashProvider.java
index 56c5fefd..a36e2bdb 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/ContinousHashProvider.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/ContinousHashProvider.java
@@ -1,5 +1,7 @@
 package org.eclipse.viatra.solver.data.map;
 
+import org.eclipse.viatra.solver.data.map.internal.Node;
+
 /**
  * A class representing an equivalence relation for a type {@code KEY} with a continuous hash function.
  * @author Oszkar Semerath
@@ -7,11 +9,18 @@ package org.eclipse.viatra.solver.data.map;
  * @param <KEY> Target java type.
  */
 public interface ContinousHashProvider<KEY> {
+        public static final int effectiveBits = Node.effectiveBits;
+        public static final int effectiveBitMask = (1<<(effectiveBits))-1;
+        /**
+         * Maximal practical depth for differentiating keys. If two keys have the same hash code until that depth, the algorithm can stop.
+         */
+        public static final int maxPracticalDepth = 500;
         /**
          * Provides a hash code for a object {@code key} with a given {@code index}. It has the following contracts:
          * <ul>
          * <li>If {@link #equals}{@code (key1,key2)}, then {@code getHash(key1, index) == getHash(key2, index)} for all values of {@code index}.</li>
          * <li>If {@code getHash(key1,index) == getHash(key2, index)} for all values of {@code index}, then {@link #equals}{@code (key1, key2)}</li>
+         * <li>In current implementation, we use only the least significant {@link #effectiveBits}
          * </ul>
          * Check {@link #equals} for further details.
          * @param key The target data object.
@@ -32,4 +41,24 @@ public interface ContinousHashProvider<KEY> {
 //       * @return whether {@code key1} and {@code key2} are equivalent with respect to an equivalence relation represented by the given .
 //       */
 //      public boolean equals(KEY key1, KEY key2);
+
+        public default int getEffectiveHash(KEY key, int index) {
+                return getHash(key, index) & effectiveBitMask;
+        }
+        public default int compare(KEY key1, KEY key2) {
+                if(key1.equals(key2)) {
+                        return 0;
+                } else {
+                        for(int i=0; i<ContinousHashProvider.maxPracticalDepth; i++) {
+                                int hash1 = getEffectiveHash(key1, i);
+                                int hash2 = getEffectiveHash(key2, i);
+                                int result = Integer.compare(hash1, hash2);
+                                if(result != 0) {
+                                        return result;
+                                }
+                        }
+                        throw new IllegalArgumentException(
+                                "Two different keys ("+key1+" and "+key2+") have the same hashcode over the practical depth limitation ("+ContinousHashProvider.maxPracticalDepth+")!");
+                }
+        }
 }
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMapStoreImpl.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMapStoreImpl.java
index d9adc117..09607d4a 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMapStoreImpl.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMapStoreImpl.java
@@ -1,5 +1,7 @@
 package org.eclipse.viatra.solver.data.map;
 
+import java.util.ArrayList;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.Map;
 import java.util.Set;
@@ -37,7 +39,7 @@ public class VersionedMapStoreImpl<KEY,VALUE> implements VersionedMapStore<KEY,
                 }
         }
         
-        public VersionedMapStoreImpl(ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue) {
+        public VersionedMapStoreImpl(ContinousHashProvider<KEY> hashProvider, VALUE defaultValue) {
                 this(hashProvider,defaultValue,new VersionedMapStoreConfiguration());
         }
         
@@ -52,15 +54,18 @@ public class VersionedMapStoreImpl<KEY,VALUE> implements VersionedMapStore<KEY,
         @Override
         public VersionedMap<KEY,VALUE> createMap(long state) {
                 ImmutableNode<KEY, VALUE> data = revert(state);
-                if(data != null) {
-                        return new VersionedMapImpl<KEY,VALUE>(this,hashProvider,defaultValue,data); 
-                } else {
-                        throw new IllegalArgumentException("Store does not contain state " + state + "!");
-                }
+                return new VersionedMapImpl<KEY,VALUE>(this,hashProvider,defaultValue,data); 
         }
         
         synchronized public ImmutableNode<KEY,VALUE> revert(long state) {
-                return states.get(state);
+                if(states.containsKey(state)) {
+                        return states.get(state);
+                } else {
+                        ArrayList<Long> existingKeys = new ArrayList<Long>(states.keySet());
+                        Collections.sort(existingKeys);
+                        throw new IllegalArgumentException(
+                                "Store does not contain state "+state+"! Avaliable states: "+existingKeys.toArray().toString());
+                }
         }
         synchronized public long commit(Node<KEY,VALUE> data, VersionedMapImpl<KEY, VALUE> mapToUpdateRoot) {
                 ImmutableNode<KEY,VALUE> immutable;
@@ -100,6 +105,6 @@ public class VersionedMapStoreImpl<KEY,VALUE> implements VersionedMapStore<KEY,
                 VersionedMap<KEY, VALUE> map2 = createMap(toState);
                 Cursor<KEY, VALUE> cursor1 = map1.getCursor();
                 Cursor<KEY, VALUE> cursor2 = map2.getCursor();
-                return new MapDiffCursor<KEY, VALUE>(this.defaultValue,cursor1,cursor2);
+                return new MapDiffCursor<KEY, VALUE>(this.hashProvider,this.defaultValue,cursor1,cursor2);
         }
 }
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapCursor.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapCursor.java
index 5b9d5c7d..6c177611 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapCursor.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapCursor.java
@@ -30,11 +30,12 @@ public class MapCursor<KEY,VALUE> implements Cursor<KEY,VALUE> {
                 // Initializing tree stack
                 super();
                 this.nodeStack = new ArrayDeque<>();
+                this.nodeIndexStack = new ArrayDeque<>();
                 if(root != null) {
                         this.nodeStack.add(root);
+                        this.nodeIndexStack.push(IndexStart);
                 }
-                this.nodeIndexStack = new ArrayDeque<>();
-                this.nodeIndexStack.push(IndexStart);
+                
                 this.dataIndex = IndexStart;
                 
                 // Initializing cache
@@ -63,7 +64,11 @@ public class MapCursor<KEY,VALUE> implements Cursor<KEY,VALUE> {
                         throw new ConcurrentModificationException();
                 }
                 if(!isTerminated()) {
-                        return this.nodeStack.peek().moveToNext(this);
+                        boolean result = this.nodeStack.peek().moveToNext(this);
+                        if(this.nodeIndexStack.size() != this.nodeStack.size()) {
+                                throw new IllegalArgumentException("Node stack is corrupted by illegal moves!");
+                        }
+                        return result;
                 }
                 return false;
         }
@@ -85,7 +90,11 @@ public class MapCursor<KEY,VALUE> implements Cursor<KEY,VALUE> {
         public static <KEY,VALUE> boolean sameSubnode(MapCursor<KEY,VALUE> cursor1, MapCursor<KEY,VALUE> cursor2) {
                 Node<KEY, VALUE> nodeOfCursor1 = cursor1.nodeStack.peek();
                 Node<KEY, VALUE> nodeOfCursor2 = cursor2.nodeStack.peek();
-                return nodeOfCursor1.equals(nodeOfCursor2);
+                if(nodeOfCursor1 != null && nodeOfCursor2 != null) {
+                        return nodeOfCursor1.equals(nodeOfCursor2);
+                } else {
+                        return false;
+                }
         }
         
         /**
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapDiffCursor.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapDiffCursor.java
index 5c911bb4..8d7cda14 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapDiffCursor.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MapDiffCursor.java
@@ -4,6 +4,7 @@ import java.util.List;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
+import org.eclipse.viatra.solver.data.map.ContinousHashProvider;
 import org.eclipse.viatra.solver.data.map.Cursor;
 import org.eclipse.viatra.solver.data.map.DiffCursor;
 import org.eclipse.viatra.solver.data.map.VersionedMap;
@@ -17,43 +18,52 @@ public class MapDiffCursor<KEY,VALUE> implements DiffCursor<KEY, VALUE>, Cursor<
         /**
          * Default value representing missing elements.
          */
-        VALUE defaultValue;
-        MapCursor<KEY,VALUE> cursor1;
-        MapCursor<KEY,VALUE> cursor2;
+        private VALUE defaultValue;
+        private MapCursor<KEY,VALUE> cursor1;
+        private MapCursor<KEY,VALUE> cursor2;
+        private ContinousHashProvider<? super KEY> hashProvider;
         
         // Values
-        KEY key;
-        VALUE value1;
-        VALUE value2;
+        private KEY key;
+        private VALUE fromValue;
+        private VALUE toValue;
         
         // State
         /**
          * Positive number if cursor 1 is behind, negative number if cursor 2 is behind, and 0 if they are at the same position.
          */
-        int cursorRelation;
+        private int cursorRelation;
+        /**
+         * Denotes a state when two cursors are in the same position, but they contain different keys.
+         * Possible values:
+         * <ul>
+         * <li>0: not stuck</li>
+         * <li>1: hashClash, next it should return the key of cursor 1.</li>
+         * <li>2: hashClash, next it should return the key of cursor 2.</li>
+         * </ul>
+         */
+        private int hashClash=0;
         
-        public MapDiffCursor(VALUE defaultValue, Cursor<KEY, VALUE> cursor1, Cursor<KEY, VALUE> cursor2) {
+        public MapDiffCursor(ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue, Cursor<KEY, VALUE> cursor1, Cursor<KEY, VALUE> cursor2) {
                 super();
+                this.hashProvider = hashProvider;
                 this.defaultValue = defaultValue;
                 this.cursor1 = (MapCursor<KEY, VALUE>) cursor1;
                 this.cursor2 = (MapCursor<KEY, VALUE>) cursor2;
-                
-                this.updateState();
-                this.moveToConsistentState();
         }
 
         public KEY getKey() {
                 return key;
         }
-        public VALUE getValue1() {
-                return value1;
+        public VALUE getFromValue() {
+                return fromValue;
         }
-        public VALUE getValue2() {
-                return value2;
+        public VALUE getToValue() {
+                return toValue;
         }
         @Override
         public VALUE getValue() {
-                return this.value2;
+                return getToValue();
         }
         public boolean isTerminated() {
                 return cursor1.isTerminated() && cursor2.isTerminated();
@@ -71,33 +81,72 @@ public class MapDiffCursor<KEY,VALUE> implements DiffCursor<KEY, VALUE>, Cursor<
         }
         
         protected void updateState() {
-                this.cursorRelation = MapCursor.compare(cursor1, cursor2);
-                if(cursorRelation > 0 || cursor2.isTerminated()) {
-                        this.key = cursor1.getKey();
-                        this.value1 = cursor1.getValue();
-                        this.value2 = defaultValue;
-                } else if(cursorRelation < 0|| cursor1.isTerminated()){
-                        this.key = cursor2.getKey();
-                        this.value1 = defaultValue;
-                        this.value2 = cursor1.getValue();
-                } else {
-                        // cursor1 = cursor2
-                        if(!cursor1.getKey().equals(cursor2.getKey())) {
-                                throw new IllegalStateException(
-                                        "Cursor comarison tells that they are in the same state, but keys are different. " + cursor1.getKey() + " - " + cursor2.getKey());
+                if(!isTerminated()) {
+                        this.cursorRelation = MapCursor.compare(cursor1, cursor2);
+                        if(cursorRelation > 0 || cursor2.isTerminated()) {
+                                this.key = cursor1.getKey();
+                                this.fromValue = cursor1.getValue();
+                                this.toValue = defaultValue;
+                        } else if(cursorRelation < 0 || cursor1.isTerminated()){
+                                this.key = cursor2.getKey();
+                                this.fromValue = defaultValue;
+                                this.toValue = cursor1.getValue();
+                        } else {
+                                // cursor1 = cursor2
+                                if(cursor1.getKey().equals(cursor2.getKey())) {
+                                        this.key = cursor1.getKey();
+                                        this.fromValue = cursor1.getValue();
+                                        this.toValue = defaultValue;
+                                } else {
+                                        resolveHashClash1();
+                                }
                         }
-                        this.key = cursor1.getKey();
-                        this.value1 = cursor1.getValue();
-                        this.value2 = defaultValue;
                 }
         }
+        protected void resolveHashClash1() {
+                int compareResult = this.hashProvider.compare(cursor1.key, cursor2.key);
+                if(compareResult<0) {
+                        this.hashClash = 2;
+                        this.cursorRelation = 0;
+                        this.key = cursor1.key;
+                        this.fromValue = cursor1.value;
+                        this.toValue = defaultValue;
+                } else if(compareResult>0) {
+                        this.hashClash = 1;
+                        this.cursorRelation = 0;
+                        this.key = cursor2.key;
+                        this.fromValue = defaultValue;
+                        this.toValue = cursor2.value;
+                } else {
+                        throw new IllegalArgumentException("Inconsistent compare result for diffcursor");
+                }
+        }
+        protected boolean isInHashClash() {
+                return this.hashClash != 0;
+        }
+        protected void resolveHashClash2() {
+                if(hashClash == 1) {
+                        this.hashClash = 0;
+                        this.cursorRelation = 0;
+                        this.key = cursor1.key;
+                        this.fromValue = cursor1.value;
+                        this.toValue = defaultValue;
+                } else if(hashClash == 2) {
+                        this.hashClash = 0;
+                        this.cursorRelation = 0;
+                        this.key = cursor2.key;
+                        this.fromValue = defaultValue;
+                        this.toValue = cursor2.value;
+                } else throw new IllegalArgumentException("Inconsistent compare result for diffcursor");
+        }
+
         
-        protected boolean differentValues() {
-                return this.value1 != this.value2;
+        protected boolean sameValues() {
+                return this.fromValue == this.toValue;
         }
         protected boolean moveOne() {
                 if(isTerminated()) {
-                        throw new IllegalStateException("DiffCursor tries to move when terminated!");
+                        return false;
                 }
                 if(this.cursorRelation > 0 || cursor2.isTerminated()) {
                         return cursor1.move();
@@ -129,10 +178,11 @@ public class MapDiffCursor<KEY,VALUE> implements DiffCursor<KEY, VALUE>, Cursor<
                                         lastResult = skipNode();
                                         changed = true;
                                 }
-                                if(differentValues()) {
+                                if(sameValues()) {
                                         lastResult = moveOne();
                                         changed = true;
                                 }
+                                updateState();
                         } while(changed && !isTerminated());
                         return lastResult;
                 } else {
@@ -142,11 +192,17 @@ public class MapDiffCursor<KEY,VALUE> implements DiffCursor<KEY, VALUE>, Cursor<
         
         public boolean move() {
                 if(!isTerminated()) {
-                        if(moveOne()) {
-                                return moveToConsistentState();
+                        if(isInHashClash()) {
+                                this.resolveHashClash2();
+                                return true;
                         } else {
-                                return false;
+                                if(moveOne()) {
+                                        return moveToConsistentState();
+                                } else {
+                                        return false;
+                                }
                         }
+                        
                 } else return false;
         }
 }
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/Node.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/Node.java
index c3a50201..1d659779 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/Node.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/Node.java
@@ -9,6 +9,7 @@ public abstract class Node<KEY,VALUE>{
         protected static final int factor = 1<<branchingFactorBit;
         protected static final int numberOfFactors = Integer.SIZE / branchingFactorBit;
         protected static final int factorMask = factor-1;
+        public static final int effectiveBits = branchingFactorBit * numberOfFactors;
         
         /**
          * Calculates the index for the continuous hash.
@@ -37,6 +38,7 @@ public abstract class Node<KEY,VALUE>{
                 if(shiftDepth<0 && 5<shiftDepth) throw new IllegalArgumentException("Invalid shift depth! valid intervall=[0;5], input="+shiftDepth);
                 return (hash >>> shiftDepth*branchingFactorBit) & factorMask;
         }
+        
         /**
          * Returns the hash code for a given depth. It may calculate new hash code, or reuse a hash code calculated for depth-1.
          * @param key The key.
@@ -45,8 +47,12 @@ public abstract class Node<KEY,VALUE>{
          * @return The new hash code.
          */
         protected int newHash(final ContinousHashProvider<? super KEY> hashProvider, KEY key, int hash, int depth) {
+                final int hashDepth = hashDepth(depth);
+                if(hashDepth>=ContinousHashProvider.maxPracticalDepth) {
+                        throw new IllegalArgumentException("Key "+key+" have the clashing hashcode over the practical depth limitation ("+ContinousHashProvider.maxPracticalDepth+")!");
+                }
                 return depth%numberOfFactors == 0?
-                                hashProvider.getHash(key, hashDepth(depth)) :
+                                hashProvider.getHash(key, hashDepth) :
                                 hash;
         }
         
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/VersionedMapImpl.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/VersionedMapImpl.java
index fcee6f46..715a9d74 100644
--- a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/VersionedMapImpl.java
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/VersionedMapImpl.java
@@ -108,7 +108,7 @@ public class VersionedMapImpl<KEY,VALUE> implements VersionedMap<KEY,VALUE>{
                 Cursor<KEY, VALUE> fromCursor = this.getCursor();
                 VersionedMap<KEY, VALUE> toMap = this.store.createMap(toVersion);
                 Cursor<KEY, VALUE> toCursor = toMap.getCursor();
-                return new MapDiffCursor<KEY, VALUE>(defaultValue, fromCursor, toCursor);
+                return new MapDiffCursor<KEY, VALUE>(this.hashProvider,this.defaultValue, fromCursor, toCursor);
                 
         }