diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index a7d620d1d..a51b1660f 100644 --- a/verifier/BUILD.bazel +++ b/verifier/BUILD.bazel @@ -43,6 +43,8 @@ java_library( java_library( name = "z3_impl", compatible_with = [], - visibility = ["//:internal"], + visibility = [ + "//:internal", + ], exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"], ) diff --git a/verifier/axioms/BUILD.bazel b/verifier/axioms/BUILD.bazel index 537cfd2ce..281f40a05 100644 --- a/verifier/axioms/BUILD.bazel +++ b/verifier/axioms/BUILD.bazel @@ -1,6 +1,10 @@ load("@rules_java//java:defs.bzl", "java_library") -package(default_visibility = ["//verifier:__subpackages__"]) +package( + default_visibility = [ + "//verifier:__subpackages__", + ], +) java_library( name = "axioms", diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java index da48ec484..42a09914e 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java @@ -23,5 +23,10 @@ public static CelVerifierBuilder newVerifier() { return CelVerifierZ3Impl.newBuilder(); } + /** Create a builder for configuring a Z3-based {@link CelVerifier} with Z3-specific settings. */ + public static CelVerifierZ3Impl.Builder newZ3Verifier() { + return CelVerifierZ3Impl.newBuilder(); + } + private CelVerifierFactory() {} } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index ce2705b56..6c19c440d 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -42,7 +42,7 @@ /** Z3 implementation of the CelVerifier. */ @Immutable -final class CelVerifierZ3Impl implements CelVerifier { +public final class CelVerifierZ3Impl implements CelVerifier { @VisibleForTesting static final CelTypeProvider EMPTY_TYPE_PROVIDER = @@ -68,7 +68,7 @@ static Builder newBuilder() { return new Builder(); } - static final class Builder implements CelVerifierBuilder { + public static final class Builder implements CelVerifierBuilder { private Duration timeout; private int comprehensionUnrollLimit; private final ImmutableSet.Builder unknownIdentifiers; @@ -116,12 +116,12 @@ public CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit) { } @CanIgnoreReturnValue - Builder addFunctionAxioms(CelZ3FunctionAxiom... axioms) { + public Builder addFunctionAxioms(CelZ3FunctionAxiom... axioms) { return addFunctionAxioms(Arrays.asList(axioms)); } @CanIgnoreReturnValue - Builder addFunctionAxioms(Iterable axioms) { + public Builder addFunctionAxioms(Iterable axioms) { functionAxioms.addAll(axioms); return this; }