Move CEL-agnostic Z3 expression helpers out of CelZ3TypeSystem

verifier/src/main/java/dev/cel/verifier/BUILD.bazel

@@ -112,7 +112,10 @@ java_library(
 
 java_library(
     name = "type_system",
-    srcs = ["CelZ3TypeSystem.java"],
+    srcs = [
+        "CelZ3Exprs.java",
+        "CelZ3TypeSystem.java",
+    ],
     compatible_with = [],
     tags = [
     ],

verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

@@ -112,7 +112,7 @@ Set<BoolExpr> getTypeConstraints() {
   }
 
   BoolExpr hasTruncation() {
-    return CelZ3TypeSystem.mkOrFlattened(ctx, truncationConditions);
+    return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions);
   }
 
   CelZ3TypeSystem getTypeSystem() {
@@ -806,7 +806,7 @@ private FieldAccess getMapAccess(Expr<?> operand, String field, BoolExpr typeGua
     BoolExpr presence =
         (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str);
     Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str);
-    constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value);
+    constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
     return new FieldAccess(presence, value);
   }
 
@@ -816,7 +816,7 @@ private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGua
     BoolExpr presence =
         (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str);
     Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str);
-    constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value);
+    constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
     return new FieldAccess(presence, value);
   }
 
@@ -853,7 +853,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a
       FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
 
       presenceResult =
-          CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+          CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
               .addCase(isMessage, msgAcc.presence)
               .addCase(isMap, mapAcc.presence)
               .build(ctx.mkFalse());
@@ -863,7 +863,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a
       Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
 
       valueResult =
-          CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+          CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
               .addCase(isMessage, msgRead)
               .addCase(isMap, mapRead)
               .build(typeSystem.mkError());
@@ -1060,7 +1060,7 @@ private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSynta
     TranslatedValue resultTv =
         withScope(
             comp.accuVar(),
-            TranslatedValue.create(accu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)),
+            TranslatedValue.create(accu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)),
             () -> translateExpr(comp.result(), ast));
     Expr<?> result = resultTv.z3Expr();
     return TranslatedValue.create(
@@ -1152,7 +1152,7 @@ private BoolExpr getBoundedMapBijection(
                   seqMap);
     }
     constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
-    return CelZ3TypeSystem.mkAndFlattened(ctx, constraints);
+    return CelZ3Exprs.mkAndFlattened(ctx, constraints);
   }
 
   private <T> T withIterationScope(
@@ -1301,8 +1301,7 @@ private TranslatedValue unrollMapAndFilter(
     TranslatedValue resultTv =
         withScope(
             comp.accuVar(),
-            TranslatedValue.create(
-                chainedAccu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)),
+            TranslatedValue.create(chainedAccu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)),
             () -> translateExpr(comp.result(), ast));
 
     Expr<?> iterRangeExpr = iterRangeTv.z3Expr();
@@ -1313,10 +1312,10 @@ private TranslatedValue unrollMapAndFilter(
     // result of any non-true condition, since the unrolled value ignores early exits.
     BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition()));
     BoolExpr isAbstracted =
-        CelZ3TypeSystem.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
+        CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
     // An error is not final when truncated: an unknown from a later iteration overrides it.
     Expr<?> finalResult =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(rangeIsError, typeSystem.mkError())
             .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast))
             .build(resultTv.z3Expr());
@@ -1326,7 +1325,7 @@ private TranslatedValue unrollMapAndFilter(
             ctx.mkITE(
                 ctx.mkOr(rangeIsError, rangeIsUnknown),
                 iterRangeTv.isApproximate(),
-                CelZ3TypeSystem.mkOrFlattened(
+                CelZ3Exprs.mkOrFlattened(
                     ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled));
 
     return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint);
@@ -1379,50 +1378,49 @@ private TranslatedValue reduceAllOrExists(
 
       BoolExpr isActive = iter.inBounds;
 
-      hasMatchList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isMatch));
-      hasErrorList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isE));
-      hasUnknownList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isU));
+      hasMatchList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isMatch));
+      hasErrorList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isE));
+      hasUnknownList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isU));
 
       hasSafeMatchList.add(
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isActive, isMatch, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isActive, isMatch, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
       hasSafeErrorList.add(
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isActive, isE, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isActive, isE, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
       hasSafeUnknownList.add(
-          CelZ3TypeSystem.mkAndFlattened(
-              ctx, isActive, isU, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
-      activeTaints.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, stepTv.isApproximate()));
+          CelZ3Exprs.mkAndFlattened(
+              ctx, isActive, isU, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
+      activeTaints.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, stepTv.isApproximate()));
     }
 
-    BoolExpr hasMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasMatchList);
-    BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, hasErrorList);
-    BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasUnknownList);
+    BoolExpr hasMatch = CelZ3Exprs.mkOrFlattened(ctx, hasMatchList);
+    BoolExpr hasError = CelZ3Exprs.mkOrFlattened(ctx, hasErrorList);
+    BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasUnknownList);
     BoolExpr rangeIsError = typeSystem.isError(iterRangeTv.z3Expr());
     BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeTv.z3Expr());
 
-    BoolExpr hasSafeMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeMatchList);
-    BoolExpr hasSafeError = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeErrorList);
-    BoolExpr hasSafeUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeUnknownList);
-    BoolExpr anyActiveTaint = CelZ3TypeSystem.mkOrFlattened(ctx, activeTaints);
+    BoolExpr hasSafeMatch = CelZ3Exprs.mkOrFlattened(ctx, hasSafeMatchList);
+    BoolExpr hasSafeError = CelZ3Exprs.mkOrFlattened(ctx, hasSafeErrorList);
+    BoolExpr hasSafeUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasSafeUnknownList);
+    BoolExpr anyActiveTaint = CelZ3Exprs.mkOrFlattened(ctx, activeTaints);
 
     Expr<?> comprehensionUnknown = mkParameterizedUnknown(compExpr, ast);
     Expr<?> result =
-        CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
             .addCase(rangeIsError, typeSystem.mkError())
             .addCase(rangeIsUnknown, comprehensionUnknown)
             .addCase(hasMatch, typeSystem.mkBool(!isAll))
             .addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown)
             .addCase(hasError, typeSystem.mkError())
             .build(typeSystem.mkBool(isAll));
 
-    BoolExpr baseTaint =
-        CelZ3TypeSystem.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate());
+    BoolExpr baseTaint = CelZ3Exprs.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate());
 
     // Taint identically shadows the value flow's short-circuit control structure
     BoolExpr resultTaint =
         (BoolExpr)
-            CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+            CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
                 .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate())
                 .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch)))
                 .addCase(
@@ -1562,7 +1560,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
         boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
       }
 
-      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
+      return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type instanceof MapType) {
       // Do NOT emit a for-all quantifier over map keys or values here.
@@ -1614,7 +1612,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
         boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
       }
 
-      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
+      return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type.kind() == CelKind.STRUCT) {
       return ctx.mkAnd(

verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java

@@ -227,7 +227,7 @@ public CelVerificationResult verifyEquivalence(
       // an unknown only by its attributes (e.g. `a && true` and `a` both yield unknown {a}). Two
       // distinct unknowns may thus still be equivalent.
       BoolExpr combinedTaint =
-          CelZ3TypeSystem.mkOrFlattened(
+          CelZ3Exprs.mkOrFlattened(
               ctx,
               tvA.isApproximate(),
               tvB.isApproximate(),
@@ -318,7 +318,7 @@ CelVerificationResult verifyImplication(
       BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition));
 
       BoolExpr combinedTaint =
-          CelZ3TypeSystem.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate());
+          CelZ3Exprs.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate());
       BoolExpr unknownCondition =
           ctx.mkOr(
               translator.getTypeSystem().isUnknown(assumeTv.z3Expr()),

verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java

@@ -0,0 +1,160 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import com.google.common.collect.Lists;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+
+/** Helpers for building Z3 expressions that are independent of the CEL encoding. */
+public final class CelZ3Exprs {
+
+  /**
+   * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
+   *
+   * <p>Returns {@code false} if the list is empty.
+   */
+  public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) {
+    return mkOrFlattened(ctx, Arrays.asList(args));
+  }
+
+  /**
+   * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
+   *
+   * <p>Returns {@code false} if the list is empty.
+   */
+  public static BoolExpr mkOrFlattened(Context ctx, List<BoolExpr> args) {
+    // Pruning true/false constants in Java is significantly faster than building
+    // larger ASTs and letting Z3 process them natively.
+    List<BoolExpr> filteredArgs = new ArrayList<>();
+    for (BoolExpr arg : args) {
+      if (arg.isTrue()) {
+        return ctx.mkTrue();
+      }
+      if (!arg.isFalse()) {
+        filteredArgs.add(arg);
+      }
+    }
+    if (filteredArgs.isEmpty()) {
+      return ctx.mkFalse();
+    }
+    if (filteredArgs.size() == 1) {
+      return filteredArgs.get(0);
+    }
+    return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0]));
+  }
+
+  /**
+   * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs.
+   *
+   * <p>Returns {@code true} if the list is empty.
+   */
+  public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) {
+    return mkAndFlattened(ctx, Arrays.asList(args));
+  }
+
+  public static BoolExpr mkAndFlattened(Context ctx, List<BoolExpr> args) {
+    // Pruning true/false constants in Java is significantly faster than building
+    // larger ASTs and letting Z3 process them natively.
+    List<BoolExpr> filteredArgs = new ArrayList<>();
+    for (BoolExpr arg : args) {
+      if (arg.isFalse()) {
+        return ctx.mkFalse();
+      }
+      if (!arg.isTrue()) {
+        filteredArgs.add(arg);
+      }
+    }
+    if (filteredArgs.isEmpty()) {
+      return ctx.mkTrue();
+    }
+    if (filteredArgs.size() == 1) {
+      return filteredArgs.get(0);
+    }
+    return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0]));
+  }
+
+  /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */
+  public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
+    if (arg.isTrue()) {
+      return ctx.mkFalse();
+    }
+    if (arg.isFalse()) {
+      return ctx.mkTrue();
+    }
+    return ctx.mkNot(arg);
+  }
+
+  /**
+   * Helper to build a chain of nested ITE (If-Then-Else) conditions.
+   *
+   * <p>Conditions are evaluated in the order they are added. Branches with {@code isFalse()}
+   * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to
+   * avoid allocating dead AST paths in Z3.
+   */
+  public static final class SwitchBuilder {
+
+    private static final class SwitchCase {
+      private final BoolExpr condition;
+      private final Expr<?> value;
+
+      private SwitchCase(BoolExpr condition, Expr<?> value) {
+        this.condition = condition;
+        this.value = value;
+      }
+    }
+
+    private final Context ctx;
+    private final List<SwitchCase> cases;
+
+    public static SwitchBuilder newBuilder(Context ctx) {
+      return new SwitchBuilder(ctx);
+    }
+
+    @CanIgnoreReturnValue
+    public SwitchBuilder addCase(BoolExpr condition, Expr<?> value) {
+      // Skip branches that can never be hit (e.g. `isFalse()` probes).
+      if (condition.isFalse()) {
+        return this;
+      }
+      cases.add(new SwitchCase(condition, value));
+      return this;
+    }
+
+    public Expr<?> build(Expr<?> defaultFallback) {
+      Expr<?> result = defaultFallback;
+      for (SwitchCase c : Lists.reverse(cases)) {
+        // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite.
+        if (c.value.equals(result)) {
+          continue;
+        }
+        result = ctx.mkITE(c.condition, c.value, result);
+      }
+      return result;
+    }
+
+    private SwitchBuilder(Context ctx) {
+      this.ctx = ctx;
+      this.cases = new ArrayList<>();
+    }
+  }
+
+  private CelZ3Exprs() {}
+}