Updates. will rebase

Author: mtdowling

smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/logic/bdd/Bdd.java

@@ -56,7 +56,7 @@ public final class Bdd implements ToNode {
     private final Parameters parameters;
     private final List<Condition> conditions;
     private final List<Rule> results;
-    private final List<int[]> nodes;
+    private final int[][] nodes;
     private final int rootRef;
 
     /**
@@ -83,7 +83,7 @@ static Bdd from(Cfg cfg, BddBuilder bddBuilder, ConditionOrderingStrategy orderi
         return new BddCompiler(cfg, orderingStrategy, bddBuilder).compile();
     }
 
-    public Bdd(Parameters params, List<Condition> conditions, List<Rule> results, List<int[]> nodes, int rootRef) {
+    public Bdd(Parameters params, List<Condition> conditions, List<Rule> results, int[][] nodes, int rootRef) {
         this.parameters = Objects.requireNonNull(params, "params is null");
         this.conditions = conditions;
         this.results = results;
@@ -125,9 +125,9 @@ public List<Rule> getResults() {
     /**
      * Gets the BDD nodes.
      *
-     * @return list of node triples
+     * @return array of node triples
      */
-    public List<int[]> getNodes() {
+    public int[][] getNodes() {
         return nodes;
     }
 
@@ -174,24 +174,28 @@ && nodesEqual(nodes, other.nodes)
                 && Objects.equals(parameters, other.parameters);
     }
 
-    private static boolean nodesEqual(List<int[]> a, List<int[]> b) {
-        if (a.size() != b.size()) {
+    private static boolean nodesEqual(int[][] a, int[][] b) {
+        if (a.length != b.length) {
             return false;
-        } else {
-            for (int i = 0; i < a.size(); i++) {
-                if (!Arrays.equals(a.get(i), b.get(i))) {
-                    return false;
-                }
+        }
+        for (int i = 0; i < a.length; i++) {
+            if (!Arrays.equals(a[i], b[i])) {
+                return false;
             }
-            return true;
         }
+        return true;
     }
 
     @Override
     public int hashCode() {
-        int hash = Objects.hash(rootRef, conditions, results, parameters);
-        for (int[] node : nodes) {
-            hash = 31 * hash + Arrays.hashCode(node);
+        int hash = 31 * rootRef + nodes.length;
+        // Sample up to 16 nodes distributed across the BDD
+        int step = Math.max(1, nodes.length / 16);
+        for (int i = 0; i < nodes.length; i += step) {
+            int[] node = nodes[i];
+            hash = 31 * hash + node[0];
+            hash = 31 * hash + node[1];
+            hash = 31 * hash + node[2];
         }
         return hash;
     }
@@ -208,18 +212,27 @@ public String toString() {
      * @return the given string builder.
      */
     public StringBuilder toString(StringBuilder sb) {
+        // Calculate max width needed for first column identifiers
+        int maxConditionIdx = conditions.size() - 1;
+        int maxResultIdx = results.size() - 1;
+
+        // Width needed for "C" + maxConditionIdx or "R" + maxResultIdx
+        int conditionWidth = maxConditionIdx >= 0 ? String.valueOf(maxConditionIdx).length() + 1 : 2;
+        int resultWidth = maxResultIdx >= 0 ? String.valueOf(maxResultIdx).length() + 1 : 2;
+        int varWidth = Math.max(conditionWidth, resultWidth);
+
         sb.append("Bdd{\n");
 
         // Conditions
         sb.append("  conditions (").append(getConditionCount()).append("):\n");
         for (int i = 0; i < conditions.size(); i++) {
-            sb.append("    C").append(i).append(": ").append(conditions.get(i)).append("\n");
+            sb.append(String.format("    %" + varWidth + "s: %s%n", "C" + i, conditions.get(i)));
         }
 
         // Results
         sb.append("  results (").append(results.size()).append("):\n");
         for (int i = 0; i < results.size(); i++) {
-            sb.append("    R").append(i).append(": ");
+            sb.append(String.format("    %" + varWidth + "s: ", "R" + i));
             appendResult(sb, results.get(i));
             sb.append("\n");
         }
@@ -228,24 +241,32 @@ public StringBuilder toString(StringBuilder sb) {
         sb.append("  root: ").append(formatReference(rootRef)).append("\n");
 
         // Nodes
-        sb.append("  nodes (").append(nodes.size()).append("):\n");
-        for (int i = 0; i < nodes.size(); i++) {
-            sb.append("    ").append(i).append(": ");
+        sb.append("  nodes (").append(nodes.length).append("):\n");
+
+        // Calculate width needed for node indices
+        int indexWidth = String.valueOf(nodes.length - 1).length();
+
+        for (int i = 0; i < nodes.length; i++) {
+            sb.append(String.format("    %" + indexWidth + "d: ", i));
             if (i == 0) {
                 sb.append("terminal");
             } else {
-                int[] node = nodes.get(i);
+                int[] node = nodes[i];
                 int varIdx = node[0];
                 sb.append("[");
+
+                // Use the calculated width for variable/result references
                 if (varIdx < conditions.size()) {
-                    sb.append("C").append(varIdx);
+                    sb.append(String.format("%" + varWidth + "s", "C" + varIdx));
                 } else {
-                    sb.append("R").append(varIdx - conditions.size());
+                    sb.append(String.format("%" + varWidth + "s", "R" + (varIdx - conditions.size())));
                 }
+
+                // Format the references with consistent spacing
                 sb.append(", ")
-                        .append(formatReference(node[1]))
+                        .append(String.format("%6s", formatReference(node[1])))
                         .append(", ")
-                        .append(formatReference(node[2]))
+                        .append(String.format("%6s", formatReference(node[2])))
                         .append("]");
             }
             sb.append("\n");

smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/logic/bdd/BddBuilder.java

@@ -550,6 +550,15 @@ public List<int[]> getNodes() {
         return copy;
     }
 
+    /**
+     * Get the array of nodes.
+     *
+     * @return array of nodes.
+     */
+    public int[][] getNodesArray() {
+        return nodes.toArray(new int[0][]);
+    }
+
     private void validateBooleanOperands(int f, int g, String operation) {
         if (isResult(f) || isResult(g)) {
             throw new IllegalArgumentException("Cannot perform " + operation + " on result terminals");

smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/logic/bdd/BddCompiler.java

@@ -64,7 +64,7 @@ Bdd compile() {
         int rootRef = convertCfgToBdd(cfg.getRoot());
         rootRef = bddBuilder.reduce(rootRef);
         Parameters parameters = cfg.getRuleSet().getParameters();
-        Bdd bdd = new Bdd(parameters, orderedConditions, indexedResults, bddBuilder.getNodes(), rootRef);
+        Bdd bdd = new Bdd(parameters, orderedConditions, indexedResults, bddBuilder.getNodesArray(), rootRef);
 
         long elapsed = System.currentTimeMillis() - start;
         LOGGER.fine(String.format(

smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/logic/bdd/BddEquivalenceChecker.java

@@ -1,3 +1,7 @@
+/*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ * SPDX-License-Identifier: Apache-2.0
+ */
 package software.amazon.smithy.rulesengine.logic.bdd;
 
 import java.time.Duration;
@@ -21,8 +25,9 @@
 /**
  * Verifies functional equivalence between a CFG and its BDD representation.
  *
- * <p>This verifier uses structural equivalence checking to ensure that for every possible
- * combination of condition evaluations, both representations produce the same result.
+ * <p>This verifier uses structural equivalence checking to ensure that both representations produce the same result.
+ * When the BDD has fewer than 20 conditions, the checking is exhaustive. When there are more, random samples are
+ * checked up the earlier of max samples being reached, or the max duration being reached.
  */
 public final class BddEquivalenceChecker {
 
@@ -60,7 +65,7 @@ private BddEquivalenceChecker(Cfg cfg, Bdd bdd) {
     /**
      * Sets the maximum number of samples to test for large condition sets.
      *
-     * <p>Defaults to a max of 1M samples. Set to <= 0 to disable the max.
+     * <p>Defaults to a max of 1M samples. Set to {@code <= 0} to disable the max.
      *
      * @param maxSamples the maximum number of samples
      * @return this verifier for method chaining
@@ -97,7 +102,9 @@ public void verify() {
         testsRun = 0;
 
         LOGGER.info(() -> String.format("Verifying BDD with %d conditions (max samples: %d, timeout: %s)",
-                                        bdd.getConditionCount(), maxSamples, timeout));
+                bdd.getConditionCount(),
+                maxSamples,
+                timeout));
 
         if (bdd.getConditionCount() <= EXHAUSTIVE_THRESHOLD) {
             verifyExhaustive();
@@ -129,11 +136,13 @@ private void verifyResults() {
             Set<Rule> inBddOnly = new HashSet<>(bddResults);
             inBddOnly.removeAll(cfgResults);
             throw new IllegalStateException(String.format(
-                    "Result mismatch: CFG has %d results, BDD has %d results (excluding NoMatchRule).\n" +
-                    "In CFG only: %s\n" +
-                    "In BDD only: %s",
-                    cfgResults.size(), bddResults.size(), inCfgOnly, inBddOnly
-            ));
+                    "Result mismatch: CFG has %d results, BDD has %d results (excluding NoMatchRule).%n" +
+                            "In CFG only: %s%n" +
+                            "In BDD only: %s",
+                    cfgResults.size(),
+                    bddResults.size(),
+                    inCfgOnly,
+                    inBddOnly));
         }
     }
 
@@ -147,7 +156,7 @@ private void verifyExhaustive() {
             verifyCase(mask);
             if (hasEitherLimitBeenExceeded()) {
                 LOGGER.info(String.format("Exhaustive verification stopped after %d tests "
-                                          + "(limit: %d samples or %s timeout)", testsRun, maxSamples, timeout));
+                        + "(limit: %d samples or %s timeout)", testsRun, maxSamples, timeout));
                 break;
             }
         }
@@ -159,7 +168,8 @@ private void verifyExhaustive() {
      */
     private void verifyWithLimits() {
         LOGGER.info(() -> String.format("Running limited verification (will stop at %d samples OR %s timeout)",
-                                        maxSamples, timeout));
+                maxSamples,
+                timeout));
         verifyCriticalCases();
 
         while (!hasEitherLimitBeenExceeded()) {
@@ -235,8 +245,13 @@ private void verifyCase(long mask) {
             for (int i = 0; i < bdd.getConditions().size(); i++) {
                 Condition condition = bdd.getConditions().get(i);
                 boolean value = (mask & (1L << i)) != 0;
-                errorMsg.append("  Condition ").append(i).append(" [").append(value).append("]: ")
-                        .append(condition).append("\n");
+                errorMsg.append("  Condition ")
+                        .append(i)
+                        .append(" [")
+                        .append(value)
+                        .append("]: ")
+                        .append(condition)
+                        .append("\n");
             }
             errorMsg.append("\nResults:\n");
             errorMsg.append("  CFG result: ").append(describeResult(cfgResult)).append("\n");
@@ -255,8 +270,11 @@ private Rule evaluateCfgWithMask(ConditionEvaluator maskEvaluator) {
     }
 
     // Recursively evaluates a CFG node.
-    private CfgNode evaluateCfgNode(CfgNode node, Map<Condition, Integer> conditionToIndex,
-            ConditionEvaluator maskEvaluator) {
+    private CfgNode evaluateCfgNode(
+            CfgNode node,
+            Map<Condition, Integer> conditionToIndex,
+            ConditionEvaluator maskEvaluator
+    ) {
         if (node instanceof ResultNode) {
             return node;
         }

smithy-rules-engine/src/main/java/software/amazon/smithy/rulesengine/logic/bdd/BddEvaluator.java

@@ -7,20 +7,40 @@
 import software.amazon.smithy.rulesengine.logic.ConditionEvaluator;
 
 /**
- * Simple BDD evaluator.
+ * Simple BDD evaluator that works directly with BDD nodes.
  */
 public final class BddEvaluator {
 
-    private final Bdd bdd;
+    private final int[][] nodes;
+    private final int rootRef;
     private final int conditionCount;
 
-    private BddEvaluator(Bdd bdd) {
-        this.bdd = bdd;
-        this.conditionCount = bdd.getConditionCount();
+    private BddEvaluator(int[][] nodes, int rootRef, int conditionCount) {
+        this.nodes = nodes;
+        this.rootRef = rootRef;
+        this.conditionCount = conditionCount;
     }
 
+    /**
+     * Create evaluator from a Bdd object.
+     *
+     * @param bdd the BDD
+     * @return the evaluator
+     */
     public static BddEvaluator from(Bdd bdd) {
-        return new BddEvaluator(bdd);
+        return from(bdd.getNodes(), bdd.getRootRef(), bdd.getConditionCount());
+    }
+
+    /**
+     * Create evaluator from BDD data.
+     *
+     * @param nodes BDD nodes array
+     * @param rootRef root reference
+     * @param conditionCount number of conditions
+     * @return the evaluator
+     */
+    public static BddEvaluator from(int[][] nodes, int rootRef, int conditionCount) {
+        return new BddEvaluator(nodes, rootRef, conditionCount);
     }
 
     /**
@@ -30,7 +50,7 @@ public static BddEvaluator from(Bdd bdd) {
      * @return the result index, or -1 for no match
      */
     public int evaluate(ConditionEvaluator evaluator) {
-        int ref = bdd.getRootRef();
+        int ref = rootRef;
 
         while (true) {
             // Handle terminals
@@ -48,7 +68,7 @@ public int evaluate(ConditionEvaluator evaluator) {
             boolean complemented = ref < 0;
             int nodeIdx = (complemented ? -ref : ref) - 1;
 
-            int[] node = bdd.getNodes().get(nodeIdx);
+            int[] node = nodes[nodeIdx];
             int varIdx = node[0];
 
             // Evaluate condition and follow appropriate branch