From 972fef90deffd66a818bc45046356ca4051ccfa1 Mon Sep 17 00:00:00 2001 From: Heshan Padamsiri Date: Thu, 5 Dec 2024 15:19:06 +0530 Subject: [PATCH 1/6] Add optimization to compiler --- .../ballerina/types/typeops/BddCommonOps.java | 112 ++++++++++++++---- 1 file changed, 87 insertions(+), 25 deletions(-) diff --git a/semtypes/src/main/java/io/ballerina/types/typeops/BddCommonOps.java b/semtypes/src/main/java/io/ballerina/types/typeops/BddCommonOps.java index 6de40258eee1..cac04bd1e329 100644 --- a/semtypes/src/main/java/io/ballerina/types/typeops/BddCommonOps.java +++ b/semtypes/src/main/java/io/ballerina/types/typeops/BddCommonOps.java @@ -23,6 +23,9 @@ import io.ballerina.types.subtypedata.BddAllOrNothing; import io.ballerina.types.subtypedata.BddNode; +import java.util.HashMap; +import java.util.Map; + /** * Contain common BDD operations found in bdd.bal file. * @@ -38,6 +41,21 @@ public static BddNode bddAtom(Atom atom) { } public static Bdd bddUnion(Bdd b1, Bdd b2) { + return bddUnionWithMemo(BddOpMemo.create(), b1, b2); + } + + private static Bdd bddUnionWithMemo(BddOpMemo memoTable, Bdd b1, Bdd b2) { + BddOpMemoKey key = new BddOpMemoKey(b1, b2); + Bdd memoized = memoTable.unionMemo.get(key); + if (memoized != null) { + return memoized; + } + memoized = bddUnionInner(memoTable, b1, b2); + memoTable.unionMemo.put(key, memoized); + return memoized; + } + + private static Bdd bddUnionInner(BddOpMemo memo, Bdd b1, Bdd b2) { if (b1 == b2) { return b1; } else if (b1 instanceof BddAllOrNothing) { @@ -51,23 +69,38 @@ public static Bdd bddUnion(Bdd b1, Bdd b2) { if (cmp < 0L) { return bddCreate(b1Bdd.atom(), b1Bdd.left(), - bddUnion(b1Bdd.middle(), b2), + bddUnionWithMemo(memo, b1Bdd.middle(), b2), b1Bdd.right()); } else if (cmp > 0L) { return bddCreate(b2Bdd.atom(), b2Bdd.left(), - bddUnion(b1, b2Bdd.middle()), + bddUnionWithMemo(memo, b1, b2Bdd.middle()), b2Bdd.right()); } else { return bddCreate(b1Bdd.atom(), - bddUnion(b1Bdd.left(), b2Bdd.left()), - bddUnion(b1Bdd.middle(), b2Bdd.middle()), - bddUnion(b1Bdd.right(), b2Bdd.right())); + bddUnionWithMemo(memo, b1Bdd.left(), b2Bdd.left()), + bddUnionWithMemo(memo, b1Bdd.middle(), b2Bdd.middle()), + bddUnionWithMemo(memo, b1Bdd.right(), b2Bdd.right())); } } } public static Bdd bddIntersect(Bdd b1, Bdd b2) { + return bddIntersectWithMemo(BddOpMemo.create(), b1, b2); + } + + private static Bdd bddIntersectWithMemo(BddOpMemo memo, Bdd b1, Bdd b2) { + BddOpMemoKey key = new BddOpMemoKey(b1, b2); + Bdd memoized = memo.intersectionMemo.get(key); + if (memoized != null) { + return memoized; + } + memoized = bddIntersectInner(memo, b1, b2); + memo.intersectionMemo.put(key, memoized); + return memoized; + } + + private static Bdd bddIntersectInner(BddOpMemo memo, Bdd b1, Bdd b2) { if (b1 == b2) { return b1; } else if (b1 instanceof BddAllOrNothing) { @@ -80,28 +113,43 @@ public static Bdd bddIntersect(Bdd b1, Bdd b2) { long cmp = atomCmp(b1Bdd.atom(), b2Bdd.atom()); if (cmp < 0L) { return bddCreate(b1Bdd.atom(), - bddIntersect(b1Bdd.left(), b2), - bddIntersect(b1Bdd.middle(), b2), - bddIntersect(b1Bdd.right(), b2)); + bddIntersectWithMemo(memo, b1Bdd.left(), b2), + bddIntersectWithMemo(memo, b1Bdd.middle(), b2), + bddIntersectWithMemo(memo, b1Bdd.right(), b2)); } else if (cmp > 0L) { return bddCreate(b2Bdd.atom(), - bddIntersect(b1, b2Bdd.left()), - bddIntersect(b1, b2Bdd.middle()), - bddIntersect(b1, b2Bdd.right())); + bddIntersectWithMemo(memo, b1, b2Bdd.left()), + bddIntersectWithMemo(memo, b1, b2Bdd.middle()), + bddIntersectWithMemo(memo, b1, b2Bdd.right())); } else { return bddCreate(b1Bdd.atom(), - bddIntersect( - bddUnion(b1Bdd.left(), b1Bdd.middle()), - bddUnion(b2Bdd.left(), b2Bdd.middle())), + bddIntersectWithMemo(memo, + bddUnionWithMemo(memo, b1Bdd.left(), b1Bdd.middle()), + bddUnionWithMemo(memo, b2Bdd.left(), b2Bdd.middle())), BddAllOrNothing.bddNothing(), - bddIntersect( - bddUnion(b1Bdd.right(), b1Bdd.middle()), - bddUnion(b2Bdd.right(), b2Bdd.middle()))); + bddIntersectWithMemo(memo, + bddUnionWithMemo(memo, b1Bdd.right(), b1Bdd.middle()), + bddUnionWithMemo(memo, b2Bdd.right(), b2Bdd.middle()))); } } } public static Bdd bddDiff(Bdd b1, Bdd b2) { + return bddDiffWithMemo(BddOpMemo.create(), b1, b2); + } + + private static Bdd bddDiffWithMemo(BddOpMemo memo, Bdd b1, Bdd b2) { + BddOpMemoKey key = new BddOpMemoKey(b1, b2); + Bdd memoized = memo.diffMemo.get(key); + if (memoized != null) { + return memoized; + } + memoized = bddDiffInner(memo, b1, b2); + memo.diffMemo.put(key, memoized); + return memoized; + } + + private static Bdd bddDiffInner(BddOpMemo memo, Bdd b1, Bdd b2) { if (b1 == b2) { return BddAllOrNothing.bddNothing(); } else if (b2 instanceof BddAllOrNothing allOrNothing) { @@ -114,25 +162,27 @@ public static Bdd bddDiff(Bdd b1, Bdd b2) { long cmp = atomCmp(b1Bdd.atom(), b2Bdd.atom()); if (cmp < 0L) { return bddCreate(b1Bdd.atom(), - bddDiff(bddUnion(b1Bdd.left(), b1Bdd.middle()), b2), + bddDiffWithMemo(memo, bddUnionWithMemo(memo, b1Bdd.left(), b1Bdd.middle()), b2), BddAllOrNothing.bddNothing(), - bddDiff(bddUnion(b1Bdd.right(), b1Bdd.middle()), b2)); + bddDiffWithMemo(memo, bddUnionWithMemo(memo, b1Bdd.right(), b1Bdd.middle()), b2)); } else if (cmp > 0L) { return bddCreate(b2Bdd.atom(), - bddDiff(b1, bddUnion(b2Bdd.left(), b2Bdd.middle())), + bddDiffWithMemo(memo, b1, bddUnionWithMemo(memo, b2Bdd.left(), b2Bdd.middle())), BddAllOrNothing.bddNothing(), - bddDiff(b1, bddUnion(b2Bdd.right(), b2Bdd.middle()))); + bddDiffWithMemo(memo, b1, bddUnionWithMemo(memo, b2Bdd.right(), b2Bdd.middle()))); } else { // There is an error in the Castagna paper for this formula. // The union needs to be materialized here. // The original formula does not work in a case like (a0|a1) - a0. // Castagna confirms that the following formula is the correct one. return bddCreate(b1Bdd.atom(), - bddDiff(bddUnion(b1Bdd.left(), b1Bdd.middle()), - bddUnion(b2Bdd.left(), b2Bdd.middle())), + bddDiffWithMemo(memo, + bddUnionWithMemo(memo, b1Bdd.left(), b1Bdd.middle()), + bddUnionWithMemo(memo, b2Bdd.left(), b2Bdd.middle())), BddAllOrNothing.bddNothing(), - bddDiff(bddUnion(b1Bdd.right(), b1Bdd.middle()), - bddUnion(b2Bdd.right(), b2Bdd.middle()))); + bddDiffWithMemo(memo, + bddUnionWithMemo(memo, b1Bdd.right(), b1Bdd.middle()), + bddUnionWithMemo(memo, b2Bdd.right(), b2Bdd.middle()))); } } } @@ -222,4 +272,16 @@ public static String bddToString(Bdd b, boolean inner) { return str; } } + + private record BddOpMemoKey(Bdd b1, Bdd b2) { + + } + + private record BddOpMemo(Map unionMemo, Map intersectionMemo, + Map diffMemo) { + + static BddOpMemo create() { + return new BddOpMemo(new HashMap<>(), new HashMap<>(), new HashMap<>()); + } + } } From 1379b4b41d512b351ffe5b264a7ceb4876bef2c7 Mon Sep 17 00:00:00 2001 From: Heshan Padamsiri Date: Thu, 5 Dec 2024 15:44:22 +0530 Subject: [PATCH 2/6] Add optimization to runtime --- .../runtime/api/types/semtype/Bdd.java | 124 ++++++++++++------ 1 file changed, 86 insertions(+), 38 deletions(-) diff --git a/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java b/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java index 2573230f05a8..7341d35a24da 100644 --- a/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java +++ b/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java @@ -20,6 +20,9 @@ import io.ballerina.runtime.internal.types.semtype.SubTypeData; +import java.util.HashMap; +import java.util.Map; + import static io.ballerina.runtime.api.types.semtype.Conjunction.and; /** @@ -38,10 +41,20 @@ public abstract sealed class Bdd extends SubType implements SubTypeData permits @Override public SubType union(SubType other) { - return bddUnion((Bdd) other); + return bddUnion(BddOpMemo.create(), (Bdd) other); + } + + private Bdd bddUnion(BddOpMemo memoTable, Bdd other) { + BddOpMemoKey key = new BddOpMemoKey(this, other); + Bdd memoized = memoTable.unionMemo().get(key); + if (memoized == null) { + memoized = bddUnionInner(memoTable, other); + memoTable.unionMemo().put(key, memoized); + } + return memoized; } - private Bdd bddUnion(Bdd other) { + private Bdd bddUnionInner(BddOpMemo memo, Bdd other) { if (other == this) { return this; } else if (this == BddAllOrNothing.ALL || other == BddAllOrNothing.ALL) { @@ -57,18 +70,18 @@ private Bdd bddUnion(Bdd other) { if (cmp < 0) { return bddCreate(b1Bdd.atom(), b1Bdd.left(), - b1Bdd.middle().bddUnion(other), + b1Bdd.middle().bddUnion(memo, other), b1Bdd.right()); } else if (cmp > 0) { return bddCreate(b2Bdd.atom(), b2Bdd.left(), - this.bddUnion(b2Bdd.middle()), + this.bddUnion(memo, b2Bdd.middle()), b2Bdd.right()); } else { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(b2Bdd.left()), - b1Bdd.middle().bddUnion(b2Bdd.middle()), - b1Bdd.right().bddUnion(b2Bdd.right())); + b1Bdd.left().bddUnion(memo, b2Bdd.left()), + b1Bdd.middle().bddUnion(memo, b2Bdd.middle()), + b1Bdd.right().bddUnion(memo, b2Bdd.right())); } } @@ -88,10 +101,20 @@ private int atomCmp(Atom a1, Atom a2) { @Override public SubType intersect(SubType other) { - return bddIntersect((Bdd) other); + return bddIntersect(BddOpMemo.create(), (Bdd) other); } - private Bdd bddIntersect(Bdd other) { + private Bdd bddIntersect(BddOpMemo memoTable, Bdd other) { + BddOpMemoKey key = new BddOpMemoKey(this, other); + Bdd memoized = memoTable.intersectionMemo().get(key); + if (memoized == null) { + memoized = bddIntersectInner(memoTable, other); + memoTable.intersectionMemo().put(key, memoized); + } + return memoized; + } + + private Bdd bddIntersectInner(BddOpMemo memo, Bdd other) { if (other == this) { return this; } else if (this == BddAllOrNothing.NOTHING || other == BddAllOrNothing.NOTHING) { @@ -106,66 +129,80 @@ private Bdd bddIntersect(Bdd other) { int cmp = atomCmp(b1Bdd.atom(), b2Bdd.atom()); if (cmp < 0) { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddIntersect(other), - b1Bdd.middle().bddIntersect(other), - b1Bdd.right().bddIntersect(other)); + b1Bdd.left().bddIntersect(memo, other), + b1Bdd.middle().bddIntersect(memo, other), + b1Bdd.right().bddIntersect(memo, other)); } else if (cmp > 0) { return bddCreate(b2Bdd.atom(), - this.bddIntersect(b2Bdd.left()), - this.bddIntersect(b2Bdd.middle()), - this.bddIntersect(b2Bdd.right())); + this.bddIntersect(memo, b2Bdd.left()), + this.bddIntersect(memo, b2Bdd.middle()), + this.bddIntersect(memo, b2Bdd.right())); } else { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(b1Bdd.middle()).bddIntersect(b2Bdd.left().bddUnion(b2Bdd.middle())), + b1Bdd.left().bddUnion(memo, b1Bdd.middle()) + .bddIntersect(memo, b2Bdd.left().bddUnion(memo, b2Bdd.middle())), BddAllOrNothing.NOTHING, - b1Bdd.right().bddUnion(b1Bdd.middle()).bddIntersect(b2Bdd.right().bddUnion(b2Bdd.middle()))); + b1Bdd.right().bddUnion(memo, b1Bdd.middle()) + .bddIntersect(memo, b2Bdd.right().bddUnion(memo, b2Bdd.middle()))); } } @Override public SubType diff(SubType other) { - return bddDiff((Bdd) other); + return bddDiff(BddOpMemo.create(), (Bdd) other); + } + + private Bdd bddDiff(BddOpMemo memoTable, Bdd other) { + var key = new BddOpMemoKey(this, other); + var memoized = memoTable.diffMemo.get(key); + if (memoized == null) { + memoized = bddDiffInner(memoTable, other); + memoTable.diffMemo.put(key, memoized); + } + return memoized; } - private Bdd bddDiff(Bdd other) { + private Bdd bddDiffInner(BddOpMemo memo, Bdd other) { if (this == other || other == BddAllOrNothing.ALL || this == BddAllOrNothing.NOTHING) { return BddAllOrNothing.NOTHING; } else if (other == BddAllOrNothing.NOTHING) { return this; } else if (this == BddAllOrNothing.ALL) { - return other.bddComplement(); + return other.bddComplement(memo); } BddNode b1Bdd = (BddNode) this; BddNode b2Bdd = (BddNode) other; int cmp = atomCmp(b1Bdd.atom(), b2Bdd.atom()); if (cmp < 0L) { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(b1Bdd.middle()).bddDiff(other), + b1Bdd.left().bddUnion(memo, b1Bdd.middle()).bddDiff(memo, other), BddAllOrNothing.NOTHING, - b1Bdd.right().bddUnion(b1Bdd.middle()).bddDiff(other)); + b1Bdd.right().bddUnion(memo, b1Bdd.middle()).bddDiff(memo, other)); } else if (cmp > 0L) { return bddCreate(b2Bdd.atom(), - this.bddDiff(b2Bdd.left().bddUnion(b2Bdd.middle())), + this.bddDiff(memo, b2Bdd.left().bddUnion(memo, b2Bdd.middle())), BddAllOrNothing.NOTHING, - this.bddDiff(b2Bdd.right().bddUnion(b2Bdd.middle()))); + this.bddDiff(memo, b2Bdd.right().bddUnion(memo, b2Bdd.middle()))); } else { // There is an error in the Castagna paper for this formula. // The union needs to be materialized here. // The original formula does not work in a case like (a0|a1) - a0. // Castagna confirms that the following formula is the correct one. return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(b1Bdd.middle()).bddDiff(b2Bdd.left().bddUnion(b2Bdd.middle())), + b1Bdd.left().bddUnion(memo, b1Bdd.middle()) + .bddDiff(memo, b2Bdd.left().bddUnion(memo, b2Bdd.middle())), BddAllOrNothing.NOTHING, - b1Bdd.right().bddUnion(b1Bdd.middle()).bddDiff(b2Bdd.right().bddUnion(b2Bdd.middle()))); + b1Bdd.right().bddUnion(memo, b1Bdd.middle()) + .bddDiff(memo, b2Bdd.right().bddUnion(memo, b2Bdd.middle()))); } } @Override public SubType complement() { - return bddComplement(); + return bddComplement(BddOpMemo.create()); } - private Bdd bddComplement() { + private Bdd bddComplement(BddOpMemo memo) { if (this == BddAllOrNothing.ALL) { return BddAllOrNothing.NOTHING; } else if (this == BddAllOrNothing.NOTHING) { @@ -176,26 +213,26 @@ private Bdd bddComplement() { if (b.right() == nothing) { return bddCreate(b.atom(), nothing, - b.left().bddUnion(b.middle()).bddComplement(), - b.middle().bddComplement()); + b.left().bddUnion(memo, b.middle()).bddComplement(memo), + b.middle().bddComplement(memo)); } else if (b.left() == nothing) { return bddCreate(b.atom(), - b.middle().bddComplement(), - b.right().bddUnion(b.middle()).bddComplement(), + b.middle().bddComplement(memo), + b.right().bddUnion(memo, b.middle()).bddComplement(memo), nothing); } else if (b.middle() == nothing) { return bddCreate(b.atom(), - b.left().bddComplement(), - b.left().bddUnion(b.right()).bddComplement(), - b.right().bddComplement()); + b.left().bddComplement(memo), + b.left().bddUnion(memo, b.right()).bddComplement(memo), + b.right().bddComplement(memo)); } else { // There is a typo in the Frisch PhD thesis for this formula. // (It has left and right swapped.) // Castagna (the PhD supervisor) confirms that this is the correct formula. return bddCreate(b.atom(), - b.left().bddUnion(b.middle()).bddComplement(), + b.left().bddUnion(memo, b.middle()).bddComplement(memo), nothing, - b.right().bddUnion(b.middle()).bddComplement()); + b.right().bddUnion(memo, b.middle()).bddComplement(memo)); } } @@ -204,7 +241,7 @@ private Bdd bddCreate(Atom atom, Bdd left, Bdd middle, Bdd right) { return middle; } if (left.equals(right)) { - return left.bddUnion(right); + return left.bddUnion(BddOpMemo.create(), right); } return new BddNodeImpl(atom, left, middle, right); @@ -282,4 +319,15 @@ public static String bddToString(Bdd b, boolean inner) { } } + private record BddOpMemoKey(Bdd b1, Bdd b2) { + + } + + private record BddOpMemo(Map unionMemo, Map intersectionMemo, + Map diffMemo) { + + static BddOpMemo create() { + return new BddOpMemo(new HashMap<>(), new HashMap<>(), new HashMap<>()); + } + } } From 0fab35b5258a4bbc0e6ea6d34a74c1db9efef10d Mon Sep 17 00:00:00 2001 From: Heshan Padamsiri Date: Thu, 5 Dec 2024 18:25:09 +0530 Subject: [PATCH 3/6] Revert "Add optimization to runtime" This reverts commit 1379b4b41d512b351ffe5b264a7ceb4876bef2c7. --- .../runtime/api/types/semtype/Bdd.java | 124 ++++++------------ 1 file changed, 38 insertions(+), 86 deletions(-) diff --git a/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java b/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java index 7341d35a24da..2573230f05a8 100644 --- a/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java +++ b/bvm/ballerina-runtime/src/main/java/io/ballerina/runtime/api/types/semtype/Bdd.java @@ -20,9 +20,6 @@ import io.ballerina.runtime.internal.types.semtype.SubTypeData; -import java.util.HashMap; -import java.util.Map; - import static io.ballerina.runtime.api.types.semtype.Conjunction.and; /** @@ -41,20 +38,10 @@ public abstract sealed class Bdd extends SubType implements SubTypeData permits @Override public SubType union(SubType other) { - return bddUnion(BddOpMemo.create(), (Bdd) other); - } - - private Bdd bddUnion(BddOpMemo memoTable, Bdd other) { - BddOpMemoKey key = new BddOpMemoKey(this, other); - Bdd memoized = memoTable.unionMemo().get(key); - if (memoized == null) { - memoized = bddUnionInner(memoTable, other); - memoTable.unionMemo().put(key, memoized); - } - return memoized; + return bddUnion((Bdd) other); } - private Bdd bddUnionInner(BddOpMemo memo, Bdd other) { + private Bdd bddUnion(Bdd other) { if (other == this) { return this; } else if (this == BddAllOrNothing.ALL || other == BddAllOrNothing.ALL) { @@ -70,18 +57,18 @@ private Bdd bddUnionInner(BddOpMemo memo, Bdd other) { if (cmp < 0) { return bddCreate(b1Bdd.atom(), b1Bdd.left(), - b1Bdd.middle().bddUnion(memo, other), + b1Bdd.middle().bddUnion(other), b1Bdd.right()); } else if (cmp > 0) { return bddCreate(b2Bdd.atom(), b2Bdd.left(), - this.bddUnion(memo, b2Bdd.middle()), + this.bddUnion(b2Bdd.middle()), b2Bdd.right()); } else { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(memo, b2Bdd.left()), - b1Bdd.middle().bddUnion(memo, b2Bdd.middle()), - b1Bdd.right().bddUnion(memo, b2Bdd.right())); + b1Bdd.left().bddUnion(b2Bdd.left()), + b1Bdd.middle().bddUnion(b2Bdd.middle()), + b1Bdd.right().bddUnion(b2Bdd.right())); } } @@ -101,20 +88,10 @@ private int atomCmp(Atom a1, Atom a2) { @Override public SubType intersect(SubType other) { - return bddIntersect(BddOpMemo.create(), (Bdd) other); + return bddIntersect((Bdd) other); } - private Bdd bddIntersect(BddOpMemo memoTable, Bdd other) { - BddOpMemoKey key = new BddOpMemoKey(this, other); - Bdd memoized = memoTable.intersectionMemo().get(key); - if (memoized == null) { - memoized = bddIntersectInner(memoTable, other); - memoTable.intersectionMemo().put(key, memoized); - } - return memoized; - } - - private Bdd bddIntersectInner(BddOpMemo memo, Bdd other) { + private Bdd bddIntersect(Bdd other) { if (other == this) { return this; } else if (this == BddAllOrNothing.NOTHING || other == BddAllOrNothing.NOTHING) { @@ -129,80 +106,66 @@ private Bdd bddIntersectInner(BddOpMemo memo, Bdd other) { int cmp = atomCmp(b1Bdd.atom(), b2Bdd.atom()); if (cmp < 0) { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddIntersect(memo, other), - b1Bdd.middle().bddIntersect(memo, other), - b1Bdd.right().bddIntersect(memo, other)); + b1Bdd.left().bddIntersect(other), + b1Bdd.middle().bddIntersect(other), + b1Bdd.right().bddIntersect(other)); } else if (cmp > 0) { return bddCreate(b2Bdd.atom(), - this.bddIntersect(memo, b2Bdd.left()), - this.bddIntersect(memo, b2Bdd.middle()), - this.bddIntersect(memo, b2Bdd.right())); + this.bddIntersect(b2Bdd.left()), + this.bddIntersect(b2Bdd.middle()), + this.bddIntersect(b2Bdd.right())); } else { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(memo, b1Bdd.middle()) - .bddIntersect(memo, b2Bdd.left().bddUnion(memo, b2Bdd.middle())), + b1Bdd.left().bddUnion(b1Bdd.middle()).bddIntersect(b2Bdd.left().bddUnion(b2Bdd.middle())), BddAllOrNothing.NOTHING, - b1Bdd.right().bddUnion(memo, b1Bdd.middle()) - .bddIntersect(memo, b2Bdd.right().bddUnion(memo, b2Bdd.middle()))); + b1Bdd.right().bddUnion(b1Bdd.middle()).bddIntersect(b2Bdd.right().bddUnion(b2Bdd.middle()))); } } @Override public SubType diff(SubType other) { - return bddDiff(BddOpMemo.create(), (Bdd) other); - } - - private Bdd bddDiff(BddOpMemo memoTable, Bdd other) { - var key = new BddOpMemoKey(this, other); - var memoized = memoTable.diffMemo.get(key); - if (memoized == null) { - memoized = bddDiffInner(memoTable, other); - memoTable.diffMemo.put(key, memoized); - } - return memoized; + return bddDiff((Bdd) other); } - private Bdd bddDiffInner(BddOpMemo memo, Bdd other) { + private Bdd bddDiff(Bdd other) { if (this == other || other == BddAllOrNothing.ALL || this == BddAllOrNothing.NOTHING) { return BddAllOrNothing.NOTHING; } else if (other == BddAllOrNothing.NOTHING) { return this; } else if (this == BddAllOrNothing.ALL) { - return other.bddComplement(memo); + return other.bddComplement(); } BddNode b1Bdd = (BddNode) this; BddNode b2Bdd = (BddNode) other; int cmp = atomCmp(b1Bdd.atom(), b2Bdd.atom()); if (cmp < 0L) { return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(memo, b1Bdd.middle()).bddDiff(memo, other), + b1Bdd.left().bddUnion(b1Bdd.middle()).bddDiff(other), BddAllOrNothing.NOTHING, - b1Bdd.right().bddUnion(memo, b1Bdd.middle()).bddDiff(memo, other)); + b1Bdd.right().bddUnion(b1Bdd.middle()).bddDiff(other)); } else if (cmp > 0L) { return bddCreate(b2Bdd.atom(), - this.bddDiff(memo, b2Bdd.left().bddUnion(memo, b2Bdd.middle())), + this.bddDiff(b2Bdd.left().bddUnion(b2Bdd.middle())), BddAllOrNothing.NOTHING, - this.bddDiff(memo, b2Bdd.right().bddUnion(memo, b2Bdd.middle()))); + this.bddDiff(b2Bdd.right().bddUnion(b2Bdd.middle()))); } else { // There is an error in the Castagna paper for this formula. // The union needs to be materialized here. // The original formula does not work in a case like (a0|a1) - a0. // Castagna confirms that the following formula is the correct one. return bddCreate(b1Bdd.atom(), - b1Bdd.left().bddUnion(memo, b1Bdd.middle()) - .bddDiff(memo, b2Bdd.left().bddUnion(memo, b2Bdd.middle())), + b1Bdd.left().bddUnion(b1Bdd.middle()).bddDiff(b2Bdd.left().bddUnion(b2Bdd.middle())), BddAllOrNothing.NOTHING, - b1Bdd.right().bddUnion(memo, b1Bdd.middle()) - .bddDiff(memo, b2Bdd.right().bddUnion(memo, b2Bdd.middle()))); + b1Bdd.right().bddUnion(b1Bdd.middle()).bddDiff(b2Bdd.right().bddUnion(b2Bdd.middle()))); } } @Override public SubType complement() { - return bddComplement(BddOpMemo.create()); + return bddComplement(); } - private Bdd bddComplement(BddOpMemo memo) { + private Bdd bddComplement() { if (this == BddAllOrNothing.ALL) { return BddAllOrNothing.NOTHING; } else if (this == BddAllOrNothing.NOTHING) { @@ -213,26 +176,26 @@ private Bdd bddComplement(BddOpMemo memo) { if (b.right() == nothing) { return bddCreate(b.atom(), nothing, - b.left().bddUnion(memo, b.middle()).bddComplement(memo), - b.middle().bddComplement(memo)); + b.left().bddUnion(b.middle()).bddComplement(), + b.middle().bddComplement()); } else if (b.left() == nothing) { return bddCreate(b.atom(), - b.middle().bddComplement(memo), - b.right().bddUnion(memo, b.middle()).bddComplement(memo), + b.middle().bddComplement(), + b.right().bddUnion(b.middle()).bddComplement(), nothing); } else if (b.middle() == nothing) { return bddCreate(b.atom(), - b.left().bddComplement(memo), - b.left().bddUnion(memo, b.right()).bddComplement(memo), - b.right().bddComplement(memo)); + b.left().bddComplement(), + b.left().bddUnion(b.right()).bddComplement(), + b.right().bddComplement()); } else { // There is a typo in the Frisch PhD thesis for this formula. // (It has left and right swapped.) // Castagna (the PhD supervisor) confirms that this is the correct formula. return bddCreate(b.atom(), - b.left().bddUnion(memo, b.middle()).bddComplement(memo), + b.left().bddUnion(b.middle()).bddComplement(), nothing, - b.right().bddUnion(memo, b.middle()).bddComplement(memo)); + b.right().bddUnion(b.middle()).bddComplement()); } } @@ -241,7 +204,7 @@ private Bdd bddCreate(Atom atom, Bdd left, Bdd middle, Bdd right) { return middle; } if (left.equals(right)) { - return left.bddUnion(BddOpMemo.create(), right); + return left.bddUnion(right); } return new BddNodeImpl(atom, left, middle, right); @@ -319,15 +282,4 @@ public static String bddToString(Bdd b, boolean inner) { } } - private record BddOpMemoKey(Bdd b1, Bdd b2) { - - } - - private record BddOpMemo(Map unionMemo, Map intersectionMemo, - Map diffMemo) { - - static BddOpMemo create() { - return new BddOpMemo(new HashMap<>(), new HashMap<>(), new HashMap<>()); - } - } } From f0d2dde3a1b277d84492ad27e40df120fa8b122e Mon Sep 17 00:00:00 2001 From: chiranSachintha Date: Thu, 5 Dec 2024 09:59:41 +0530 Subject: [PATCH 4/6] Update full build pipeline of PR build --- .github/workflows/pull_request_full_build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pull_request_full_build.yml b/.github/workflows/pull_request_full_build.yml index 5274b8db061b..30f8e7173ca1 100644 --- a/.github/workflows/pull_request_full_build.yml +++ b/.github/workflows/pull_request_full_build.yml @@ -62,7 +62,7 @@ jobs: strategy: fail-fast: false matrix: - level: [ 1, 2, 3, 4, 5, 6, 7, 8, 9 ] + level: [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 ] steps: - name: Checkout Repository From 6e1e5c1c744215da39b195b3403dd6950b53e5e0 Mon Sep 17 00:00:00 2001 From: chiranSachintha Date: Thu, 5 Dec 2024 16:48:18 +0530 Subject: [PATCH 5/6] Remove level 11 --- .github/workflows/pull_request_full_build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pull_request_full_build.yml b/.github/workflows/pull_request_full_build.yml index 30f8e7173ca1..92b47e58717e 100644 --- a/.github/workflows/pull_request_full_build.yml +++ b/.github/workflows/pull_request_full_build.yml @@ -62,7 +62,7 @@ jobs: strategy: fail-fast: false matrix: - level: [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 ] + level: [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 13 ] steps: - name: Checkout Repository From 5e99d27d768a98a0f4e9c7bd327f5602604ef0eb Mon Sep 17 00:00:00 2001 From: chiranSachintha Date: Fri, 6 Dec 2024 14:55:01 +0530 Subject: [PATCH 6/6] Update levels --- .github/workflows/pull_request_full_build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pull_request_full_build.yml b/.github/workflows/pull_request_full_build.yml index 92b47e58717e..f0e9784258bf 100644 --- a/.github/workflows/pull_request_full_build.yml +++ b/.github/workflows/pull_request_full_build.yml @@ -62,7 +62,7 @@ jobs: strategy: fail-fast: false matrix: - level: [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 13 ] + level: [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ] steps: - name: Checkout Repository