//===- smt.c - Test of SMT APIs -------------------------------------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM
// Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//

/* RUN: mlir-capi-smt-test 2>&1 | FileCheck %s
 */

#include "mlir-c/Dialect/SMT.h"
#include "mlir-c/Dialect/Func.h"
#include "mlir-c/IR.h"
#include "mlir-c/Support.h"
#include "mlir-c/Target/ExportSMTLIB.h"
#include <assert.h>
#include <stdio.h>

void dumpCallback(MlirStringRef message, void *userData) {
  fprintf(stderr, "%.*s", (int)message.length, message.data);
}

void testExportSMTLIB(MlirContext ctx) {
  // clang-format off
  const char *testSMT = 
    "func.func @test() {\n"
    "  smt.solver() : () -> () { }\n"
    "  return\n"
    "}\n";
  // clang-format on

  MlirModule module =
      mlirModuleCreateParse(ctx, mlirStringRefCreateFromCString(testSMT));

  MlirLogicalResult result =
      mlirTranslateModuleToSMTLIB(module, dumpCallback, NULL, false, false);
  (void)result;
  assert(mlirLogicalResultIsSuccess(result));

  // CHECK: ; solver scope 0
  // CHECK-NEXT: (reset)
  mlirModuleDestroy(module);
}

void testSMTType(MlirContext ctx) {
  MlirType boolType = mlirSMTTypeGetBool(ctx);
  MlirType intType = mlirSMTTypeGetInt(ctx);
  MlirType arrayType = mlirSMTTypeGetArray(ctx, intType, boolType);
  MlirType bvType = mlirSMTTypeGetBitVector(ctx, 32);
  MlirType funcType =
      mlirSMTTypeGetSMTFunc(ctx, 2, (MlirType[]){intType, boolType}, boolType);
  MlirType sortType = mlirSMTTypeGetSort(
      ctx, mlirIdentifierGet(ctx, mlirStringRefCreateFromCString("sort")), 0,
      NULL);

  // CHECK: !smt.bool
  mlirTypeDump(boolType);
  // CHECK: !smt.int
  mlirTypeDump(intType);
  // CHECK: !smt.array<[!smt.int -> !smt.bool]>
  mlirTypeDump(arrayType);
  // CHECK: !smt.bv<32>
  mlirTypeDump(bvType);
  // CHECK: !smt.func<(!smt.int, !smt.bool) !smt.bool>
  mlirTypeDump(funcType);
  // CHECK: !smt.sort<"sort">
  mlirTypeDump(sortType);

  // CHECK: bool_is_any_non_func_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(boolType)
                      ? "bool_is_any_non_func_smt_value_type\n"
                      : "bool_is_func_smt_value_type\n");
  // CHECK: int_is_any_non_func_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(intType)
                      ? "int_is_any_non_func_smt_value_type\n"
                      : "int_is_func_smt_value_type\n");
  // CHECK: array_is_any_non_func_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(arrayType)
                      ? "array_is_any_non_func_smt_value_type\n"
                      : "array_is_func_smt_value_type\n");
  // CHECK: bit_vector_is_any_non_func_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(bvType)
                      ? "bit_vector_is_any_non_func_smt_value_type\n"
                      : "bit_vector_is_func_smt_value_type\n");
  // CHECK: sort_is_any_non_func_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(sortType)
                      ? "sort_is_any_non_func_smt_value_type\n"
                      : "sort_is_func_smt_value_type\n");
  // CHECK: smt_func_is_func_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnyNonFuncSMTValueType(funcType)
                      ? "smt_func_is_any_non_func_smt_value_type\n"
                      : "smt_func_is_func_smt_value_type\n");

  // CHECK: bool_is_any_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnySMTValueType(boolType)
                      ? "bool_is_any_smt_value_type\n"
                      : "bool_is_not_any_smt_value_type\n");
  // CHECK: int_is_any_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnySMTValueType(intType)
                      ? "int_is_any_smt_value_type\n"
                      : "int_is_not_any_smt_value_type\n");
  // CHECK: array_is_any_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnySMTValueType(arrayType)
                      ? "array_is_any_smt_value_type\n"
                      : "array_is_not_any_smt_value_type\n");
  // CHECK: array_is_any_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnySMTValueType(bvType)
                      ? "array_is_any_smt_value_type\n"
                      : "array_is_not_any_smt_value_type\n");
  // CHECK: smt_func_is_any_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnySMTValueType(funcType)
                      ? "smt_func_is_any_smt_value_type\n"
                      : "smt_func_is_not_any_smt_value_type\n");
  // CHECK: sort_is_any_smt_value_type
  fprintf(stderr, mlirSMTTypeIsAnySMTValueType(sortType)
                      ? "sort_is_any_smt_value_type\n"
                      : "sort_is_not_any_smt_value_type\n");

  // CHECK: int_type_is_not_a_bool
  fprintf(stderr, mlirSMTTypeIsABool(intType) ? "int_type_is_a_bool\n"
                                              : "int_type_is_not_a_bool\n");
  // CHECK: bool_type_is_not_a_int
  fprintf(stderr, mlirSMTTypeIsAInt(boolType) ? "bool_type_is_a_int\n"
                                              : "bool_type_is_not_a_int\n");
  // CHECK: bv_type_is_not_a_array
  fprintf(stderr, mlirSMTTypeIsAArray(bvType) ? "bv_type_is_a_array\n"
                                              : "bv_type_is_not_a_array\n");
  // CHECK: array_type_is_not_a_bit_vector
  fprintf(stderr, mlirSMTTypeIsABitVector(arrayType)
                      ? "array_type_is_a_bit_vector\n"
                      : "array_type_is_not_a_bit_vector\n");
  // CHECK: sort_type_is_not_a_smt_func
  fprintf(stderr, mlirSMTTypeIsASMTFunc(sortType)
                      ? "sort_type_is_a_smt_func\n"
                      : "sort_type_is_not_a_smt_func\n");
  // CHECK: func_type_is_not_a_sort
  fprintf(stderr, mlirSMTTypeIsASort(funcType) ? "func_type_is_a_sort\n"
                                               : "func_type_is_not_a_sort\n");
}

void testSMTAttribute(MlirContext ctx) {
  // CHECK: slt_is_BVCmpPredicate
  fprintf(stderr, mlirSMTAttrCheckBVCmpPredicate(
                      ctx, mlirStringRefCreateFromCString("slt"))
                      ? "slt_is_BVCmpPredicate\n"
                      : "slt_is_not_BVCmpPredicate\n");
  // CHECK: lt_is_not_BVCmpPredicate
  fprintf(stderr, mlirSMTAttrCheckBVCmpPredicate(
                      ctx, mlirStringRefCreateFromCString("lt"))
                      ? "lt_is_BVCmpPredicate\n"
                      : "lt_is_not_BVCmpPredicate\n");
  // CHECK: slt_is_not_IntPredicate
  fprintf(stderr, mlirSMTAttrCheckIntPredicate(
                      ctx, mlirStringRefCreateFromCString("slt"))
                      ? "slt_is_IntPredicate\n"
                      : "slt_is_not_IntPredicate\n");
  // CHECK: lt_is_IntPredicate
  fprintf(stderr, mlirSMTAttrCheckIntPredicate(
                      ctx, mlirStringRefCreateFromCString("lt"))
                      ? "lt_is_IntPredicate\n"
                      : "lt_is_not_IntPredicate\n");

  // CHECK: #smt.bv<5> : !smt.bv<32>
  mlirAttributeDump(mlirSMTAttrGetBitVector(ctx, 5, 32));
  // CHECK: 0 : i64
  mlirAttributeDump(
      mlirSMTAttrGetBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt")));
  // CHECK: 0 : i64
  mlirAttributeDump(
      mlirSMTAttrGetIntPredicate(ctx, mlirStringRefCreateFromCString("lt")));
}

int main(void) {
  MlirContext ctx = mlirContextCreate();
  mlirDialectHandleLoadDialect(mlirGetDialectHandle__smt__(), ctx);
  mlirDialectHandleLoadDialect(mlirGetDialectHandle__func__(), ctx);
  testExportSMTLIB(ctx);
  testSMTType(ctx);
  testSMTAttribute(ctx);

  mlirContextDestroy(ctx);

  return 0;
}