First version of the versioned hashmap

27 files changed, 960 insertions, 0 deletions

diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.classpath b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.classpath
new file mode 100644
index 00000000..0fa31827
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.classpath
@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+        <classpathentry kind="src" path="src"/>
+        <classpathentry kind="src" path="tests"/>
+        <classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/5"/>
+        <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-11">
+                <attributes>
+                        <attribute name="module" value="true"/>
+                </attributes>
+        </classpathentry>
+        <classpathentry kind="output" path="bin"/>
+</classpath>
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.project b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.project
new file mode 100644
index 00000000..464aef51
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.project
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+        <name>org.eclipse.viatra.solver.data</name>
+        <comment></comment>
+        <projects>
+        </projects>
+        <buildSpec>
+                <buildCommand>
+                        <name>org.eclipse.xtext.ui.shared.xtextBuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+                <buildCommand>
+                        <name>org.eclipse.jdt.core.javabuilder</name>
+                        <arguments>
+                        </arguments>
+                </buildCommand>
+        </buildSpec>
+        <natures>
+                <nature>org.eclipse.jdt.core.javanature</nature>
+                <nature>org.eclipse.xtext.ui.shared.xtextNature</nature>
+        </natures>
+</projectDescription>
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.settings/org.eclipse.jdt.core.prefs b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.settings/org.eclipse.jdt.core.prefs
new file mode 100644
index 00000000..f2525a8b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/.settings/org.eclipse.jdt.core.prefs
@@ -0,0 +1,14 @@
+eclipse.preferences.version=1
+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=11
+org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
+org.eclipse.jdt.core.compiler.compliance=11
+org.eclipse.jdt.core.compiler.debug.lineNumber=generate
+org.eclipse.jdt.core.compiler.debug.localVariable=generate
+org.eclipse.jdt.core.compiler.debug.sourceFile=generate
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enablePreviewFeatures=disabled
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
+org.eclipse.jdt.core.compiler.problem.reportPreviewFeatures=warning
+org.eclipse.jdt.core.compiler.release=enabled
+org.eclipse.jdt.core.compiler.source=11
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/bin/.gitignore b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/bin/.gitignore
new file mode 100644
index 00000000..cf1db2ee
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/bin/.gitignore
@@ -0,0 +1 @@
+/org/
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/BooleanValue.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/BooleanValue.java
new file mode 100644
index 00000000..7b0e565b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/BooleanValue.java
@@ -0,0 +1,17 @@
+package org.eclipse.viatra.solver.data;
+
+public class BooleanValue implements TruthValue {
+        private final boolean value;
+        protected BooleanValue(final boolean value) {
+                this.value = value;
+        }
+        public static final BooleanValue trueValue = new BooleanValue(true);
+        public static final BooleanValue falseValue = new BooleanValue(false);
+        
+        @Override
+        public String getName() {
+                // TODO Auto-generated method stub
+                return Boolean.toString(value);
+        }
+        
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/DataSymbol.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/DataSymbol.java
new file mode 100644
index 00000000..74624db6
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/DataSymbol.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data;
+
+public class DataSymbol {
+
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/DefinedSymbol.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/DefinedSymbol.java
new file mode 100644
index 00000000..40d01721
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/DefinedSymbol.java
@@ -0,0 +1,11 @@
+package org.eclipse.viatra.solver.data;
+
+public class DefinedSymbol extends Symbol {
+        private final String name;
+        public DefinedSymbol(String name) {
+                this.name = name;
+        }
+        public String getName() {
+                return name;
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Logic2Valued.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Logic2Valued.java
new file mode 100644
index 00000000..7a807155
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Logic2Valued.java
@@ -0,0 +1,9 @@
+package org.eclipse.viatra.solver.data;
+
+public class Logic2Valued {
+        protected static final String trueName = "true";
+        protected static final String falseName = "false";
+        
+        public static final TruthValue trueValue = new NamedTruthValue(trueName);
+        public static final TruthValue falseValue = new NamedTruthValue(falseName);
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Logic4Valued.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Logic4Valued.java
new file mode 100644
index 00000000..5f1e2bd8
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Logic4Valued.java
@@ -0,0 +1,22 @@
+package org.eclipse.viatra.solver.data;
+
+public class Logic4Valued extends Logic2Valued {
+        protected static final String unknownName = "unknown";
+        protected static final String errorName = "error";
+        
+        public static final TruthValue unknownValue = new NamedTruthValue(unknownName);
+        public static final TruthValue errorValue = new NamedTruthValue(errorName);
+        
+//      public TruthValue getImplMin(TruthValue a, TruthValue b) {
+//              
+//      }
+//      public TruthValue getImplMax(TruthValue a, TruthValue b) {
+//              
+//      }
+//      public TruthValue getInfoMin(TruthValue a, TruthValue b) {
+//              
+//      }
+//      public TruthValue getInfoMax(TruthValue a, TruthValue b) {
+//              
+//      }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Model.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Model.java
new file mode 100644
index 00000000..6f5c58ce
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Model.java
@@ -0,0 +1,10 @@
+package org.eclipse.viatra.solver.data;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+public class Model {
+        Set<ModelObject> objects;
+        Map<String,Map<List<ModelObject>,TruthValue>> interpretation;
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/ModelObject.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/ModelObject.java
new file mode 100644
index 00000000..73607f82
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/ModelObject.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data;
+
+public class ModelObject {
+
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/NamedTruthValue.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/NamedTruthValue.java
new file mode 100644
index 00000000..be3a2351
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/NamedTruthValue.java
@@ -0,0 +1,13 @@
+package org.eclipse.viatra.solver.data;
+
+public class NamedTruthValue implements TruthValue {
+        private final String name;
+        public NamedTruthValue(String name) {
+                this.name = name;
+        }
+        @Override
+        public String getName() {
+                return this.name;
+        }
+
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/PrimitiveSymbol.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/PrimitiveSymbol.java
new file mode 100644
index 00000000..6bf0b195
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/PrimitiveSymbol.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data;
+
+public class PrimitiveSymbol {
+
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Symbol.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Symbol.java
new file mode 100644
index 00000000..d403e181
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/Symbol.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data;
+
+public class Symbol {
+
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/TruthValue.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/TruthValue.java
new file mode 100644
index 00000000..5dbde11c
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/TruthValue.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data;
+
+interface TruthValue {
+        public String getName();
+}
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
new file mode 100644
index 00000000..c4567458
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/ContinousHashProvider.java
@@ -0,0 +1,34 @@
+package org.eclipse.viatra.solver.data.map;
+
+/**
+ * A class representing an equivalence relation for a type {@code KEY} with a continuous hash function.
+ * @author Oszkar Semerath
+ *
+ * @param <KEY> Target java type.
+ */
+public interface ContinousHashProvider<KEY> {
+        /**
+         * 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>
+         * </ul>
+         * Check {@link #equals} for further details.
+         * @param key The target data object.
+         * @param index The depth of the the hash code. Needs to be non-negative.
+         * @return A hash code.
+         */
+        public int getHash(KEY key, int index);
+        /**
+         * Compares the equivalnce of two objects {@code key1} and {@code key2}. It has the contracts of a equivalence relation:
+         * <ul>
+         * <li> Reflexive: {@code equals(key,key) == true}.</li>
+         * <li> Symmetric: {@code equals(key1,key2) == equals(key2,key1)}.</li>
+         * <li> Transitive: {@code equals(key1,key2) == true} and {@code equals(key2,key3) == true} then {@code equals(key1,key3) == true}.</li>
+         * </ul>
+         * @param key1 First data object.
+         * @param key2 Second data object.
+         * @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);
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/Versioned.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/Versioned.java
new file mode 100644
index 00000000..d58c458e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/Versioned.java
@@ -0,0 +1,6 @@
+package org.eclipse.viatra.solver.data.map;
+
+public interface Versioned {
+        public long commit();
+        public void restore(long state);
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMap.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMap.java
new file mode 100644
index 00000000..41fd55b7
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/VersionedMap.java
@@ -0,0 +1,63 @@
+package org.eclipse.viatra.solver.data.map;
+
+import java.util.Iterator;
+import java.util.Map;
+
+import org.eclipse.viatra.solver.data.map.internal.MutableNode;
+import org.eclipse.viatra.solver.data.map.internal.Node;
+import org.eclipse.viatra.solver.data.map.internal.NodeIterator;
+
+public class VersionedMap<KEY,VALUE> implements Versioned{
+
+        protected final ContinousHashProvider<? super KEY> hashProvider;
+        protected final VALUE defaultValue;
+        protected Node<KEY,VALUE> root = null;
+        
+        protected VersionedMap(ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue) {
+                this.hashProvider = hashProvider;
+                this.defaultValue = defaultValue;
+        }
+        
+        public VALUE getDefaultValue() {
+                return defaultValue;
+        }
+        public ContinousHashProvider<? super KEY> getHashProvider() {
+                return hashProvider;
+        }
+        
+        public void put(KEY key, VALUE value) {
+                if(root!=null) {
+                        root = root.putValue(key, value, hashProvider, defaultValue, hashProvider.getHash(key, 0), 0);
+                } else {
+                        root = MutableNode.initialize(key, value, hashProvider, defaultValue);
+                }
+        }
+        public VALUE get(KEY key) {
+                if(root!=null) {
+                        return root.getValue(key, hashProvider, defaultValue, hashProvider.getHash(key, 0), 0);
+                } else {
+                        return defaultValue;
+                }
+        }
+        public int getSize() {
+                if(root == null) {
+                        return 0;
+                } else {
+                        return root.getSize();
+                }
+        }
+        Iterator<Map.Entry<KEY,VALUE>> getIterator() {
+                return new NodeIterator<KEY, VALUE>(this.root);
+        }
+
+        @Override
+        public long commit() {
+                // TODO Auto-generated method stub
+                return 0;
+        }
+
+        @Override
+        public void restore(long state) {
+                // TODO Auto-generated method stub
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/ImmutableNode.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/ImmutableNode.java
new file mode 100644
index 00000000..e2bc06a9
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/ImmutableNode.java
@@ -0,0 +1,215 @@
+package org.eclipse.viatra.solver.data.map.internal;
+
+import org.eclipse.viatra.solver.data.map.ContinousHashProvider;
+
+public class ImmutableNode<KEY, VALUE> extends Node<KEY, VALUE> {
+        /**
+         * Bitmap defining the stored key and values.
+         */
+        int dataMap;
+        /**
+         * Bitmap defining the positions of further nodes.
+         */
+        int nodeMap;
+        /**
+         * Stores Keys, Values, and subnodes. Structure: (KEY,VALUE)*,NODE; NODES are stored backwards. 
+         */
+        Object[] content;
+        
+        /**
+         * Constructor with given content
+         */
+        protected ImmutableNode(int dataMap, int nodeMap, Object[] content) {
+                this.dataMap = dataMap;
+                this.nodeMap = nodeMap;
+                this.content = content;
+        }
+        
+        /**
+         * Constructor that copies a mutable node to an immutable.
+         * @param node
+         */
+        @SuppressWarnings("unchecked")
+        protected ImmutableNode(MutableNode<KEY,VALUE> node) {
+                int size = 0;
+                for(int i = 0; i<factor; i++) {
+                        if(node.content[i]!=null) {
+                                size++;
+                        }
+                }
+                
+                int datas = 0;
+                int nodes = 0;
+                this.dataMap = 0;
+                this.nodeMap = 0;
+                this.content = new Object[size];
+                int bitposition = 1;
+                for(int i = 0; i<factor; i++) {
+                        Object key = node.content[i*2];
+                        if(key != null) {
+                                dataMap |= bitposition;
+                                content[datas*2] = key;
+                                content[datas*2+1] = node.content[i*2+1];
+                                datas++;
+                        } else {
+                                Node<KEY,VALUE> subnode = (Node<KEY, VALUE>) node.content[i*2+1];
+                                if(subnode != null) {
+                                        ImmutableNode<KEY, VALUE> immutableSubnode = subnode.toImmutable();
+                                        nodeMap |=bitposition;
+                                        content[size-1-nodes] = immutableSubnode;
+                                        nodes++;
+                                }
+                        }
+                        bitposition<<=1;
+                }
+        }
+        
+        private int index(int bitmap, int bitpos) {
+                return Integer.bitCount(bitmap & (bitpos-1));
+        }
+        
+        @SuppressWarnings("unchecked")
+        @Override
+        public VALUE getValue(KEY key, ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue, int hash, int depth) {
+                int selectedHashFragment = hashFragment(hash,shiftDepth(depth));
+                int bitposition = 1 << selectedHashFragment;
+                // If the key is stored as a data
+                if((dataMap & bitposition) != 0) {
+                        int keyIndex = 2*index(dataMap, bitposition);
+                        KEY keyCandidate = (KEY) content[keyIndex];
+                        if(hashProvider.equals(keyCandidate, key)) {
+                                return (VALUE) content[keyIndex+1];
+                        } else {
+                                return defaultValue;
+                        }
+                }
+                // the key is stored as a node
+                else if((nodeMap & bitposition) != 0) {
+                        int keyIndex = content.length-1-index(nodeMap, bitposition);
+                        ImmutableNode<KEY,VALUE> subNode = (ImmutableNode<KEY,VALUE>) content[keyIndex];
+                        int newHash = depth%numberOfFactors == 0?
+                                        hashProvider.getHash(key, hashDepth(depth)) :
+                                        hash;
+                        int newDepth = depth+1;
+                        return subNode.getValue(key, hashProvider, defaultValue, newHash, newDepth);
+                }
+                // the key is not stored at all
+                else {
+                        return defaultValue;
+                }
+        }
+        
+        @SuppressWarnings("unchecked")
+        @Override
+        public Node<KEY,VALUE> putValue(KEY key, VALUE value, ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue, int hash, int depth) {
+                int selectedHashFragment = hashFragment(hash,shiftDepth(depth));
+                int bitposition = 1 << selectedHashFragment;
+                if((dataMap & bitposition) != 0) {
+                        int keyIndex = 2*index(dataMap, bitposition);
+                        KEY keyCandidate = (KEY) content[keyIndex];
+                        if(hashProvider.equals(keyCandidate, key)) {
+                                if(value == defaultValue) {
+                                        // delete
+                                        MutableNode<KEY, VALUE> mutable = this.toMutable();
+                                        mutable.removeEntry(selectedHashFragment);
+                                        return mutable;
+                                } else if(value == content[keyIndex+1]) {
+                                        // dont change
+                                        return this;
+                                } else {
+                                        // update existing value
+                                        MutableNode<KEY, VALUE> mutable = this.toMutable();
+                                        mutable.updateValue(value, selectedHashFragment);
+                                        return mutable;
+                                }
+                        } else {
+                                if(value == defaultValue) {
+                                        // dont change
+                                        return this;
+                                } else {
+                                        // add new key + value
+                                        MutableNode<KEY, VALUE> mutable = this.toMutable();
+                                        mutable.putValue(key, value, hashProvider, defaultValue, selectedHashFragment, depth);
+                                        return mutable;
+                                }
+                        }
+                } else if((nodeMap & bitposition)!=0) {
+                        
+                        int keyIndex = content.length-1-index(dataMap, bitposition);
+                        ImmutableNode<KEY,VALUE> subNode = (ImmutableNode<KEY,VALUE>) content[keyIndex];
+                        int newHash = newHash(hashProvider, key, selectedHashFragment, depth);
+                        int newDepth = depth+1;
+                        Node<KEY,VALUE> newsubNode = subNode.putValue(key, value, hashProvider, defaultValue, newHash, newDepth);
+                        
+                        if(subNode == newsubNode) {
+                                // nothing changed
+                                return this;
+                        } else {
+                                MutableNode<KEY, VALUE> result = toMutable();
+                                result.updateSubNode(selectedHashFragment, newsubNode);
+                                return result;
+                        }
+                } else {
+                        // add new key + value
+                        MutableNode<KEY, VALUE> mutable = this.toMutable();
+                        mutable.putValue(key, value, hashProvider, defaultValue, selectedHashFragment, depth);
+                        return mutable;
+                }
+        }
+        
+        
+        @Override
+        public int getSize() {
+                throw new UnsupportedOperationException();
+        }
+        
+        @Override
+        protected MutableNode<KEY,VALUE> toMutable() {
+                return new MutableNode<KEY,VALUE>(this);
+        }
+
+        @Override
+        protected ImmutableNode<KEY,VALUE> toImmutable() {
+                return this;
+        }
+        
+        @Override
+        protected void prettyPrint(StringBuilder builder, int depth, int code) {
+                for(int i = 0; i<depth; i++) {
+                        builder.append("\t");
+                }
+                if(code>=0) {
+                        builder.append(code);
+                        builder.append(":");
+                }
+                builder.append("Immutable(");
+                boolean hadContent = false;
+                int dataMask = 1;
+                for(int i = 0; i<factor; i++) {
+                        if((dataMask & dataMap) != 0) {
+                                if(hadContent) {
+                                        builder.append(",");
+                                }
+                                builder.append(i);
+                                builder.append(":[");
+                                builder.append(content[2*index(dataMap, dataMask)].toString());
+                                builder.append("]->[");
+                                builder.append(content[2*index(dataMap, dataMask)+1].toString());
+                                builder.append("]");
+                                hadContent = true;
+                        }
+                        dataMask<<=1;
+                }
+                builder.append(")");
+                int nodeMask = 1;
+                for(int i = 0; i<factor; i++) {
+                        if((nodeMask & nodeMap)!=0) {
+                                @SuppressWarnings("unchecked")
+                                Node<KEY,VALUE> subNode = (Node<KEY, VALUE>) content[content.length-1-index(nodeMap, nodeMask)];
+                                builder.append("\n");
+                                subNode.prettyPrint(builder, depth+1, i);
+                        }
+                        nodeMask<<=1;
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/ImmutableNodeIterator.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/ImmutableNodeIterator.java
new file mode 100644
index 00000000..7715bc72
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/ImmutableNodeIterator.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data.map.internal;
+
+public class ImmutableNodeIterator {
+
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MutableNode.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MutableNode.java
new file mode 100644
index 00000000..f6d0323e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MutableNode.java
@@ -0,0 +1,241 @@
+package org.eclipse.viatra.solver.data.map.internal;
+
+import org.eclipse.viatra.solver.data.map.ContinousHashProvider;
+
+public class MutableNode<KEY,VALUE> extends Node<KEY,VALUE> {
+        Object[] content;
+        protected MutableNode() {
+                this.content = new Object[2*factor];
+        }
+        public static <KEY,VALUE> MutableNode<KEY,VALUE> initialize(
+                        KEY key, VALUE value,
+                        ContinousHashProvider<? super KEY> hashProvider,
+                        VALUE defaultValue)
+        {
+                if(value == defaultValue) {
+                        return null;
+                } else {
+                        int hash = hashProvider.getHash(key, 0);
+                        int fragment = hashFragment(hash, 0);
+                        MutableNode<KEY, VALUE> res = new MutableNode<KEY, VALUE>();
+                        res.content[2*fragment] = key;
+                        res.content[2*fragment+1] = value;
+                        return res;
+                }
+        }
+        
+        protected MutableNode(ImmutableNode<KEY,VALUE> node) {
+                this.content = new Object[2*factor]; 
+                int dataUsed=0;
+                int nodeUsed=0;
+                for(int i=0; i<factor; i++) {
+                        int bitposition = 1 << i;
+                        if((node.dataMap & bitposition) != 0) {
+                                content[2*i] = this.content[dataUsed*2];
+                                content[2*i+1] = this.content[dataUsed*2+1];
+                                dataUsed++;
+                        } else if((node.nodeMap & bitposition) != 0) {
+                                content[2*i+1] = this.content[this.content.length-1-nodeUsed];
+                                nodeUsed++;
+                        }
+                }
+        }
+        
+        @SuppressWarnings("unchecked")
+        @Override
+        public VALUE getValue(KEY key, ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue, int hash, int depth) {
+                int selectedHashFragment = hashFragment(hash,shiftDepth(depth));
+                KEY keyCandidate = (KEY) content[2*selectedHashFragment];
+                if(keyCandidate != null) {
+                        if(hashProvider.equals(keyCandidate, key)) {
+                                return (VALUE) content[2*selectedHashFragment+1];
+                        } else {
+                                return defaultValue;
+                        }
+                } else {
+                        Node<KEY,VALUE> nodeCandidate = (Node<KEY,VALUE>) content[2*selectedHashFragment+1];
+                        if(nodeCandidate != null) {
+                                int newHash = newHash(hashProvider, key, hash, depth);
+                                int newDepth = depth+1;
+                                return (VALUE) nodeCandidate.getValue(key, hashProvider, defaultValue, newHash, newDepth);
+                        } else {
+                                return defaultValue;
+                        }
+                }
+        }
+        
+        private boolean hasContent() {
+                for(Object element : this.content) {
+                        if(element != null) return true;
+                }
+                return false;
+        }
+
+        private MutableNode<KEY,VALUE> createNewNode(
+                        ContinousHashProvider<? super KEY> hashProvider,
+                        KEY key1, VALUE value1, int oldHash1,
+                        KEY key2, VALUE value2, int oldHash2,
+                        int newdepth)
+        {
+                int newHash1 = newHash(hashProvider, key1, oldHash1, newdepth);
+                int newHash2 = newHash(hashProvider, key2, oldHash2, newdepth);
+                int newFragment1 = hashFragment(newHash1, newdepth);
+                int newFragment2 = hashFragment(newHash2, newdepth);
+                
+                MutableNode<KEY,VALUE> subNode = new MutableNode<KEY,VALUE>();
+                if(newFragment1 != newFragment2) {
+                        subNode.content[newFragment1*2]=key1;
+                        subNode.content[newFragment1*2+1]=value1;
+                        
+                        subNode.content[newFragment2*2]=key2;
+                        subNode.content[newFragment2*2+1]=value2;
+                        return subNode;
+                } else {
+                        MutableNode<KEY,VALUE> subSubNode = createNewNode(
+                                        hashProvider,
+                                        key1, value1, newHash1,
+                                        key2, value2, newHash2,
+                                        newdepth+1);
+                        subNode.content[newFragment1*2+1] = subSubNode;
+                        return subNode;
+                }
+        }
+        
+        @SuppressWarnings("unchecked")
+        @Override
+        public Node<KEY,VALUE> putValue(KEY key, VALUE value, ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue, int hash, int depth) {
+                int selectedHashFragment = hashFragment(hash,shiftDepth(depth));
+                KEY keyCandidate = (KEY) content[2*selectedHashFragment];
+                if(keyCandidate != null) {
+                        if(hashProvider.equals(keyCandidate,key)) {
+                                // Update entry
+                                if(value == defaultValue) {
+                                        return removeEntry(selectedHashFragment);
+                                } else {
+                                        return updateValue(value, selectedHashFragment);
+                                }
+                        } else {
+                                if(value == defaultValue) {
+                                        // dont need to add new node
+                                        return this;
+                                } else {
+                                        // Split entry: data -> node
+                                        return moveDown(key, value, hashProvider, hash, depth, selectedHashFragment, keyCandidate);
+                                }
+                        }
+                } else {
+                        Node<KEY,VALUE> nodeCandidate =  (Node<KEY,VALUE>) content[2*selectedHashFragment+1];
+                        if(nodeCandidate != null) {
+                                Node<KEY, VALUE> newNode = nodeCandidate.putValue(key, value, hashProvider, defaultValue, newHash(hashProvider, key, hash, depth+1), depth+1);
+                                return updateSubNode(selectedHashFragment,newNode);
+                        } else {
+                                content[2*selectedHashFragment] = key;
+                                return updateValue(value, selectedHashFragment);
+                        }
+                }
+        }
+        
+        Node<KEY, VALUE> updateSubNode(int selectedHashFragment, Node<KEY, VALUE> newNode) {
+                content[2*selectedHashFragment+1] = newNode;
+                for(int i = 0; i<this.content.length; i++) {
+                        if(content[i]!=null) return this;
+                }
+                return null;
+        }
+        
+        @SuppressWarnings("unchecked")
+        Node<KEY, VALUE> moveDown(
+                        KEY key, VALUE value,
+                        ContinousHashProvider<? super KEY> hashProvider, int hash,
+                        int depth, int selectedHashFragment, KEY keyCandidate) {
+                KEY previousKey = keyCandidate;
+                VALUE previousValue = (VALUE) content[2*selectedHashFragment+1];
+                
+                MutableNode<KEY,VALUE> subNode = createNewNode(
+                        hashProvider,
+                        previousKey, previousValue, hashProvider.getHash(previousKey, hashDepth(depth)),
+                        key, value, hash,
+                        depth+1);
+                
+                content[2*selectedHashFragment] = null;
+                content[2*selectedHashFragment+1] = subNode;
+                return this;
+        }
+        
+        Node<KEY, VALUE> updateValue(VALUE value, int selectedHashFragment) {
+                content[2*selectedHashFragment+1] = value;
+                return this;
+        }
+        Node<KEY, VALUE> removeEntry(int selectedHashFragment) {
+                content[2*selectedHashFragment] = null;
+                content[2*selectedHashFragment+1] = null;
+                if(hasContent()) {
+                        return this;
+                } else {
+                        return null;
+                }
+        }
+        
+        @SuppressWarnings("unchecked")
+        @Override
+        public int getSize() {
+                int size = 0;
+                for(int i=0; i<factor; i++) {
+                        if(content[i*2]!=null) {
+                                size++;
+                        } else{
+                                 Node<KEY,VALUE> nodeCandidate = (Node<KEY, VALUE>) content[i*2+1];
+                                 if(nodeCandidate!=null) {
+                                         size+=nodeCandidate.getSize();
+                                 }
+                        }
+                }
+                return size;
+        }
+
+        @Override
+        protected MutableNode<KEY,VALUE> toMutable() {
+                return this;
+        }
+        
+        @Override
+        protected ImmutableNode<KEY,VALUE> toImmutable() {
+                return new ImmutableNode<KEY,VALUE>(this);
+        }
+        
+        @Override
+        protected void prettyPrint(StringBuilder builder, int depth, int code) {
+                for(int i = 0; i<depth; i++) {
+                        builder.append("\t");
+                }
+                if(code>=0) {
+                        builder.append(code);
+                        builder.append(":");
+                }
+                builder.append("Mutable(");
+                boolean hadContent = false;
+                for(int i = 0; i<factor; i++) {
+                        if(content[2*i] != null) {
+                                if(hadContent) {
+                                        builder.append(",");
+                                }
+                                builder.append(i);
+                                builder.append(":[");
+                                builder.append(content[2*i].toString());
+                                builder.append("]->[");
+                                builder.append(content[2*i+1].toString());
+                                builder.append("]");
+                                hadContent = true;
+                        }
+                }
+                builder.append(")");
+                for(int i = 0; i<factor; i++) {
+                        if(content[2*i] == null || content[2*i+1]!=null) {
+                                @SuppressWarnings("unchecked")
+                                Node<KEY,VALUE> subNode = (Node<KEY, VALUE>) content[2*i+1];
+                                builder.append("\n");
+                                subNode.prettyPrint(builder, depth+1, i);
+                        }
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MutableNodeIterator.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MutableNodeIterator.java
new file mode 100644
index 00000000..619eb3b2
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/MutableNodeIterator.java
@@ -0,0 +1,29 @@
+package org.eclipse.viatra.solver.data.map.internal;
+
+import java.util.Map.Entry;
+
+public class MutableNodeIterator<KEY,VALUE> extends NodeIterator<MutableNode<KEY,VALUE>,KEY, VALUE>{
+        
+        public MutableNodeIterator(MutableNode<KEY, VALUE> node) {
+                super(node);
+        }
+        
+        /**
+         * Index of the last result value;
+         */
+        int index = -1;
+        NodeIterator<KEY,VALUE> actualSubNode = null;
+        
+        @Override
+        public boolean hasNext() {
+                for(int i = index; i<node.factor; i++) {
+                        
+                }
+                return false;
+        }
+        @Override
+        public Entry<KEY, VALUE> next() {
+                // TODO Auto-generated method stub
+                return null;
+        }
+}
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
new file mode 100644
index 00000000..89c52f7f
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/Node.java
@@ -0,0 +1,69 @@
+package org.eclipse.viatra.solver.data.map.internal;
+
+import org.eclipse.viatra.solver.data.map.ContinousHashProvider;
+
+public abstract class Node<KEY,VALUE>{
+        protected static final int branchingFactorBit = 5;
+        protected static final int factor = 1<<branchingFactorBit;
+        protected static final int numberOfFactors = Integer.SIZE / branchingFactorBit;
+        protected static final int factorMask = factor-1;
+        
+        /**
+         * Calculates the index for the continuous hash.
+         * @param depth The depth of the node in the tree.
+         * @return The index of the continuous hash.
+         */
+        protected static int hashDepth(int depth) {
+                return depth/numberOfFactors;
+        }
+        
+        /**
+         * Calculates the which segment of a single hash should be used.
+         * @param depth The depth of the node in the tree. 
+         * @return The segment of a hash code.
+         */
+        protected static int shiftDepth(int depth) {
+                return depth%numberOfFactors;
+        }
+        /**
+         * Selects a segments from a complete hash for a given depth.
+         * @param hash A complete hash.
+         * @param shiftDepth The index of the segment.
+         * @return The segment as an integer.
+         */
+        protected static int hashFragment(int hash, int 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.
+         * @param hash Hash code for depth-1
+         * @param depth The depth.
+         * @return The new hash code.
+         */
+        protected int newHash(final ContinousHashProvider<? super KEY> hashProvider, KEY key, int hash, int depth) {
+                return depth%numberOfFactors == 0?
+                                hashProvider.getHash(key, hashDepth(depth)) :
+                                hash;
+        }
+        
+        
+        abstract public VALUE getValue(KEY key, ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue,  int hash, int depth);
+        abstract public Node<KEY,VALUE> putValue(KEY key, VALUE value, ContinousHashProvider<? super KEY> hashProvider, VALUE defaultValue, int hash, int depth);
+        abstract public int getSize();
+        
+        abstract protected MutableNode<KEY, VALUE> toMutable();
+        abstract protected ImmutableNode<KEY, VALUE> toImmutable();
+        
+        ///////// For iterators
+        //abstract boolean moveIteratorToNextData(NodeIterator<KEY,VALUE> iterator, int currentIndex);
+        //abstract boolean moveIteratorToNextNode(NodeIterator<KEY,VALUE> iterator, int currentIndex);
+        ///////// FOR printing
+        abstract protected void prettyPrint(StringBuilder builder, int depth, int code);
+        @Override
+        public String toString() {
+                StringBuilder stringBuilder = new StringBuilder();
+                prettyPrint(stringBuilder, 0, -1);
+                return stringBuilder.toString();
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/NodeIterator.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/NodeIterator.java
new file mode 100644
index 00000000..4c426b1e
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/src/org/eclipse/viatra/solver/data/map/internal/NodeIterator.java
@@ -0,0 +1,13 @@
+package org.eclipse.viatra.solver.data.map.internal;
+
+import java.util.Iterator;
+import java.util.Map;
+
+public abstract class NodeIterator<NODETYPE extends Node<KEY,VALUE>,KEY,VALUE>
+        implements Iterator<Map.Entry<KEY,VALUE>>
+{
+        protected NODETYPE node;
+        public NodeIterator(NODETYPE node) {
+                this.node = node;
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapSmokeTest.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapSmokeTest.java
new file mode 100644
index 00000000..e1a7a39b
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapSmokeTest.java
@@ -0,0 +1,82 @@
+package org.eclipse.viatra.solver.data.map;
+
+import java.util.Random;
+
+import org.junit.jupiter.api.Test;
+
+public class MapSmokeTest {
+        
+        private void runTest(int seed, int steps, int maxKey, int maxValue) {
+                String[] values = new String[maxValue];
+                for(int i = 0; i<values.length; i++) {
+                        values[i] = "VALUE-"+i;
+                }
+                ContinousHashProvider<Integer> chp = new ContinousHashProvider<Integer>() {
+                        
+                        @Override
+                        public int getHash(Integer key, int index) {
+                                int result = 1;
+                                final int prime = 31;
+                                result = prime*result + key;
+                                result = prime*result + index;
+                                return result;
+                        }
+                        
+                        @Override
+                        public boolean equals(Integer key1, Integer key2) {
+                                return key1.equals(key2);
+                        }
+                };
+                
+                VersionedMap<Integer, String> sut = new VersionedMap<Integer, String>(chp, values[0]);
+                MapTestEnvironment<Integer, String> e = new MapTestEnvironment<Integer, String>(sut);
+                
+                Random r = new Random(seed);
+                
+                iterativeCall(steps, maxKey, maxValue, values, e, r);
+        }
+
+        void recursiveCall(
+                int steps,
+                int maxKey,
+                int maxValue,
+                String[] values,
+                MapTestEnvironment<Integer, String> e,
+                Random r)
+        {
+                if(steps<=0) {
+                        return;
+                } else {
+                        e.put(r.nextInt(maxKey), values[r.nextInt(maxValue)]);
+                        e.checkEquivalence();
+                        
+                        recursiveCall(steps-1, maxKey, maxValue, values, e, r);
+                }
+        }
+        
+        void iterativeCall(int steps,
+                int maxKey,
+                int maxValue,
+                String[] values,
+                MapTestEnvironment<Integer, String> e,
+                Random r)
+        {
+                for(int i=0; i<steps; i++) {
+                        e.put(r.nextInt(maxKey), values[r.nextInt(maxValue)]);
+                        e.checkEquivalence();
+                }
+        }
+        
+        @Test
+        void runTest1() {
+                runTest(0, 100000, 3, 2);
+        }
+        @Test
+        void runTest2() {
+                runTest(1, 100000, 3, 2);
+        }
+        @Test
+        void runTest3() {
+                runTest(1, 32*32*32*32, 32*32-1, 2);
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapTestEnvironment.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapTestEnvironment.java
new file mode 100644
index 00000000..5e9b2e5f
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapTestEnvironment.java
@@ -0,0 +1,41 @@
+package org.eclipse.viatra.solver.data.map;
+
+import static org.junit.Assert.fail;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Map.Entry;
+
+import junit.framework.AssertionFailedError;
+
+public class MapTestEnvironment<KEY,VALUE> {
+        VersionedMap<KEY, VALUE> sut;
+        Map<KEY,VALUE> oracle = new HashMap<KEY, VALUE>();
+        
+        public MapTestEnvironment(VersionedMap<KEY, VALUE> sut) {
+                this.sut = sut;
+        }
+        
+        public void put(KEY key, VALUE value) {
+                sut.put(key, value);
+                oracle.put(key, value);
+        }
+        
+        public void checkEquivalence() {
+                int nonDefault = 0;
+                for(Entry<KEY, VALUE> entry : oracle.entrySet()) {
+                        VALUE sutAnswer = sut.get(entry.getKey());
+                        VALUE oracleAnswer1 = entry.getValue();
+                        VALUE oracleAnswer2 = (oracleAnswer1 == null)?sut.getDefaultValue():oracleAnswer1;
+                        if(sutAnswer!=oracleAnswer2) {
+                                fail("Non-equivalent gets: " + sutAnswer + " != " + oracleAnswer2 + "<-[oracle]") ;
+                        }
+                        if(entry.getValue() != sut.getDefaultValue()) {
+                                nonDefault++;
+                        }
+                }
+                int sutNonDefault = sut.getSize();
+                assertEquals(sutNonDefault, nonDefault);
+        }
+}
diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapTests.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapTests.java
new file mode 100644
index 00000000..28a49380
--- /dev/null
+++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.solver.data/tests/org/eclipse/viatra/solver/data/map/MapTests.java
@@ -0,0 +1,5 @@
+package org.eclipse.viatra.solver.data.map;
+
+public class MapTests {
+
+}