// 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.axioms;

import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.SeqExpr;
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
import java.util.Optional;

/** Axiomatization for CEL's greaterequals operator. */
@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
final class GreaterEqualsAxiom {

  static final CelZ3FunctionAxiom INSTANCE =
      CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER_EQUALS.functionDecl())
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_INT64.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkGe(typeSystem.getInt(lhs), typeSystem.getInt(rhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_TIMESTAMP.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkGe(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_DURATION.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkGe(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_UINT64.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkGe(typeSystem.getUint(lhs), typeSystem.getUint(rhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_DOUBLE.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkFPGEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_STRING.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.MkStringLe(
                              (SeqExpr) typeSystem.getString(rhs),
                              (SeqExpr) typeSystem.getString(lhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_BYTES.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.MkStringLe(
                              (SeqExpr) typeSystem.getBytes(rhs),
                              (SeqExpr) typeSystem.getBytes(lhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_INT64_DOUBLE.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          AxiomHelpers.mkFpLeReal(
                              ctx,
                              typeSystem.getDouble(rhs),
                              ctx.mkInt2Real(typeSystem.getInt(lhs))))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_UINT64_DOUBLE.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          AxiomHelpers.mkFpLeReal(
                              ctx,
                              typeSystem.getDouble(rhs),
                              ctx.mkInt2Real(typeSystem.getUint(lhs))))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_DOUBLE_INT64.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          AxiomHelpers.mkRealLeFp(
                              ctx,
                              ctx.mkInt2Real(typeSystem.getInt(rhs)),
                              typeSystem.getDouble(lhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_DOUBLE_UINT64.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          AxiomHelpers.mkRealLeFp(
                              ctx,
                              ctx.mkInt2Real(typeSystem.getUint(rhs)),
                              typeSystem.getDouble(lhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_INT64_UINT64.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkGe(
                              (ArithExpr) typeSystem.getInt(lhs),
                              (ArithExpr) typeSystem.getUint(rhs)))))
          .addBinaryOverloadTranslator(
              Comparison.GREATER_EQUALS_UINT64_INT64.celOverloadDecl(),
              (ctx, typeSystem, constraintSink, lhs, rhs) ->
                  Optional.of(
                      typeSystem.wrapBool(
                          ctx.mkGe(
                              (ArithExpr) typeSystem.getUint(lhs),
                              (ArithExpr) typeSystem.getInt(rhs)))))
          .build();

  private GreaterEqualsAxiom() {}
}
