Skip to content

Commit

Permalink
Removed caching
Browse files Browse the repository at this point in the history
  • Loading branch information
leventeBajczi committed Nov 9, 2023
1 parent 0a6b932 commit 05a5d44
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 32 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,6 @@
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.Set;
import java.util.stream.Collectors;

Expand All @@ -33,13 +31,11 @@
* An ARG is uniquely identifiable using its leaf nodes.
* An ArgTrace is uniquely identifiable using its last node.
* <p>
* 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.
* We don't perform caching for the hash codes, and 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<Object, Integer> hashCodeCache = new LinkedHashMap<>();

private ArgStructuralEquality() {
}

Expand Down Expand Up @@ -112,33 +108,26 @@ public static boolean equals(final ArgTrace<? extends State, ? extends Action> t


public static int hashCode(final ArgNode<? extends State, ? extends Action> n) {
if (!hashCodeCache.containsKey(n)) {
int hashcode = 0;

if (n.inEdge.isPresent()) {
hashcode += hashCode(n.inEdge.get());
}
int hashcode = 0;

hashcode += n.getState().hashCode();
hashCodeCache.put(n, hashcode);
if (n.inEdge.isPresent()) {
hashcode += hashCode(n.inEdge.get());
}
return hashCodeCache.get(n);

hashcode += n.getState().hashCode();
return hashcode;
}

public static int hashCode(final ArgEdge<? extends State, ? extends Action> e) {
if (!hashCodeCache.containsKey(e)) {
int hashcode = 0;
int hashcode = 0;

hashcode += hashCode(e.getSource());
hashcode += hashCode(e.getSource());

hashcode += e.getAction().hashCode();
hashcode += e.getAction().hashCode();

hashCodeCache.put(e, hashcode);
}
return hashCodeCache.get(e);
return hashcode;
}

// ARG is not immutable, so we don't cache
public static int hashCode(final ARG<? extends State, ? extends Action> a) {
int hashcode = 0;

Expand All @@ -151,11 +140,7 @@ public static int hashCode(final ARG<? extends State, ? extends Action> a) {
}

public static int hashCode(final ArgTrace<? extends State, ? extends Action> t) {
if (!hashCodeCache.containsKey(t)) {
int hashcode = hashCode(t.node(t.length()));
hashCodeCache.put(t, hashcode);
}
return hashCodeCache.get(t);
return hashCode(t.node(t.length()));
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ import org.junit.jupiter.api.Assertions
import org.junit.jupiter.params.ParameterizedTest
import org.junit.jupiter.params.provider.Arguments
import org.junit.jupiter.params.provider.MethodSource
import java.util.*
import java.util.stream.Stream
import kotlin.io.path.absolutePathString
import kotlin.io.path.createTempDirectory
Expand Down Expand Up @@ -78,8 +77,8 @@ class XcfaCliVerifyTest {
fun chcFiles(): Stream<Arguments> {
return Stream.of(
Arguments.of("/chc/chc-LIA-Lin_000.smt2", ChcFrontend.ChcTransformation.FORWARD, "--domain PRED_CART"),
Arguments.of("/chc/chc-LIA-Arrays_000.smt2", ChcFrontend.ChcTransformation.BACKWARD,
"--domain PRED_CART"),
// Arguments.of("/chc/chc-LIA-Arrays_000.smt2", ChcFrontend.ChcTransformation.BACKWARD,
// "--domain PRED_CART"),
)
}
}
Expand Down

0 comments on commit 05a5d44

Please sign in to comment.