Fix bug regarding level-skips in constraint MDDs

ftsrg · Feb 20, 2024 · b09d67f · b09d67f
1 parent f141ec4
commit b09d67f
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/...heta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java b/...heta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java
@@ -147,6 +147,9 @@ public RecursiveIntObjCursor<? extends MddNode> 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());