diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java index 241a369590..85313ef0f2 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java @@ -21,7 +21,6 @@ import hu.bme.mit.theta.common.container.Containers; import java.util.Collection; -import java.util.Objects; import java.util.Optional; import java.util.OptionalInt; import java.util.stream.Stream; @@ -221,18 +220,4 @@ public double getMeanBranchingFactor() { final double mean = nodesToCalculate.mapToDouble(n -> n.getOutEdges().count()).average().orElse(0); return mean; } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - ARG arg = (ARG) o; - return initialized == arg.initialized && - initNodes.equals(arg.initNodes); - } - - @Override - public int hashCode() { - return Objects.hash(initNodes, initialized, partialOrd); - } } diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgEdge.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgEdge.java index e1babcec02..9a41b46f23 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgEdge.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgEdge.java @@ -18,36 +18,10 @@ import hu.bme.mit.theta.analysis.Action; import hu.bme.mit.theta.analysis.State; -import java.util.Objects; - public final class ArgEdge { private static final int HASH_SEED = 3653; private volatile int hashCode = 0; - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - ArgEdge argEdge = (ArgEdge) o; - return Objects.equals(source.getState(), argEdge.source.getState()) - && Objects.equals(target, argEdge.target) - && Objects.equals(action.toString(), argEdge.action.toString()); - } - - @Override - public int hashCode() { - int result = hashCode; - if (result == 0) { - result = HASH_SEED; - result = 31 * result + source.getState().hashCode(); - result = 31 * result + target.getState().hashCode(); - result = 31 * result + action.toString().hashCode(); - hashCode = result; - } - return result; - // return Objects.hash(source.getState(), target.getState(), action.toString()); - } - private final ArgNode source; private final ArgNode target; private final A action; diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java index 81f5a5270a..983817b0f8 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java @@ -20,7 +20,9 @@ import hu.bme.mit.theta.common.Utils; import hu.bme.mit.theta.common.container.Containers; -import java.util.*; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Optional; import java.util.stream.Stream; import static com.google.common.base.Preconditions.checkArgument; @@ -270,29 +272,6 @@ private Stream> unexcludedDescendantsOfNode() { //// - @Override - public int hashCode() { - int result = hashCode; - if (result == 0) { - result = HASH_SEED; - result = 31 * result + id; - hashCode = result; - } - return result; - } - - @Override - public boolean equals(Object o) { - if (this == o) return true; - if (o == null || getClass() != o.getClass()) return false; - ArgNode argNode = (ArgNode) o; - return depth == argNode.depth && - state.equals(argNode.state) && - coveringNode.equals(argNode.coveringNode) && - Set.copyOf(outEdges).equals(Set.copyOf(argNode.outEdges)) && - target == argNode.target; - } - @Override public String toString() { return Utils.lispStringBuilder("ArgNode").add(id).body().add(state).toString(); diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java new file mode 100644 index 0000000000..2631cb362e --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java @@ -0,0 +1,160 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.analysis.algorithm; + +import hu.bme.mit.theta.analysis.Action; +import hu.bme.mit.theta.analysis.State; + +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.stream.Collectors; + +import static com.google.common.base.Objects.equal; + +/** + * Structural comparisons using equal() and hashCode() for ARG-related classes. + * Each node is uniquely identifiable using its incoming edge (or its absence), and wrapped state. + * Each edge is uniquely identifiable using its source node, and wrapped action. + * An ARG is uniquely identifiable using its leaf nodes. + * An ArgTrace is uniquely identifiable using its last node. + *

+ * We perform caching for the hash codes, but equals() checks will always traverse the ancestors of + * a node (and edge). However, this traversal only goes towards the root, rather than in all + * directions. + */ +public final class ArgStructuralEquality { + private static final Map hashCodeCache = new LinkedHashMap<>(); + + private ArgStructuralEquality(){ + } + + public static boolean equals(final ArgNode n1, + final ArgNode n2) { + + // if one node has a parent but the other one does not, nodes are not equal + if(n1.inEdge.isPresent() != n2.inEdge.isPresent()) { + return false; + } + + // if in edge is not same, nodes are not equal + if(n1.inEdge.isPresent() && !equals(n1.inEdge.get(), n2.inEdge.get())) { + return false; + } + + // if wrapped state is not same, nodes are not equal + if(!n1.getState().equals(n2.getState())) { + return false; + } + + return true; + } + + public static boolean equals(final ArgEdge e1, + final ArgEdge e2) { + + // if source node is not same, edges are not equal + if(!equals(e1.getSource(), e2.getSource())) { + return false; + } + + // if wrapped action is not same, edges are not equal + if(!e1.getAction().equals(e2.getAction())) { + return false; + } + + return true; + } + + public static boolean equals(final ARG a1, + final ARG a2) { + + var leaves1 = a1.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet()); + var leaves2 = a2.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet()); + + // if the two ARGs contain a different number of leaf nodes, they are not equal + if(leaves1.size() != leaves2.size()) { + return false; + } + + leaves1loop: + for (ArgNode n1 : leaves1) { + for (ArgNode n2 : leaves2) { + if(equals(n1, n2)) { + continue leaves1loop; + } + } + // a leaf node did not have a corresponding leaf node in the other arg + return false; + } + return true; + } + + public static boolean equals(final ArgTrace t1, + final ArgTrace t2) { + + return equal(t1.node(t1.length()), t2.node(t2.length())); + } + + + public static int hashCode(final ArgNode n) { + if(!hashCodeCache.containsKey(n)) { + int hashcode = 0; + + if(n.inEdge.isPresent()) { + hashcode += hashCode(n.inEdge.get()); + } + + hashcode += n.getState().hashCode(); + hashCodeCache.put(n, hashcode); + } + return hashCodeCache.get(n); + } + + public static int hashCode(final ArgEdge e) { + if(!hashCodeCache.containsKey(e)) { + int hashcode = 0; + + hashcode += hashCode(e.getSource()); + + hashcode += e.getAction().hashCode(); + + hashCodeCache.put(e, hashcode); + } + return hashCodeCache.get(e); + } + + // ARG is not immutable, so we don't cache + public static int hashCode(final ARG a) { + int hashcode = 0; + + var leaves = a.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet()); + for (ArgNode leaf : leaves) { + hashcode += hashCode(leaf); + } + + return hashcode; + } + + public static int hashCode(final ArgTrace t) { + if(!hashCodeCache.containsKey(t)) { + int hashcode = hashCode(t.node(t.length())); + hashCodeCache.put(t, hashcode); + } + return hashCodeCache.get(t); + } + +} diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java index a786f29df8..acc5784bed 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java @@ -116,30 +116,4 @@ public Iterator> iterator() { return nodes.iterator(); } - @Override - public boolean equals(Object o) { - if (this == o) { - return true; - } - if (o == null || getClass() != o.getClass()) { - return false; - } - ArgTrace argTrace = (ArgTrace) o; - return states.equals(argTrace.states); // && edges.equals(argTrace.edges); - } - - @Override - public int hashCode() { - int result = hashCode; - if (result == 0) { - result = HASH_SEED; - result = 31 * result + states.hashCode(); - result = 31 * result + edges.hashCode(); - hashCode = result; - } - return result; - // return Objects.hash(states, edges); - } - //// - } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt index 5cf15eda39..3fd40864b9 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt @@ -300,7 +300,7 @@ data class XcfaProcessState(val locs: LinkedList, val varLookup: L override fun hashCode(): Int { var result = locs.hashCode() - result = 31 * result + paramsInitialized.hashCode() // TODO FRICKIN INNER STATE HASH + result = 31 * result + paramsInitialized.hashCode() return result }