From b09d67f0957b4194aac194c368d7f8ec94c0d513 Mon Sep 17 00:00:00 2001 From: mondokm Date: Tue, 20 Feb 2024 15:03:01 +0100 Subject: [PATCH] Fix bug regarding level-skips in constraint MDDs --- .../expression/MddExpressionRepresentation.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java index 631afef262..366a946cb3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java @@ -147,6 +147,9 @@ public RecursiveIntObjCursor cursor(RecursiveIntObjMapView MddNode mddNode = mddNodeConstraint.get(mddNodeConstraint.statistics().lowestValue()); while (true) { + // This is needed because the constraint node might contain level-skips: of the domain is bounded, then default values are detected + if(mddNode.isTerminal()) break; + final IntStatistics statistics = mddNode.statistics(); final Decl decl = variable.getTraceInfo(Decl.class); final LitExpr lowerBound = LitExprConverter.toLitExpr(statistics.lowestValue(), decl.getType()); @@ -466,7 +469,8 @@ private static int generateMissingLiteral(MddExpressionRepresentation representa final IntSetView remaining = domain.minus(representation.explicitRepresentation.getCacheView().keySet()); if (remaining.isEmpty()) { representation.explicitRepresentation.setComplete(); - throw new UnsupportedOperationException("Not yet implemented"); + // Return the first element + newValue = representation.explicitRepresentation.getCacheView().keySet().statistics().lowestValue(); } else { final var cur = remaining.cursor(); Preconditions.checkState(cur.moveNext());