File tree Expand file tree Collapse file tree 4 files changed +26
-14
lines changed Expand file tree Collapse file tree 4 files changed +26
-14
lines changed Original file line number Diff line number Diff line change 1
- //===- MLIR -c/ExportSMTLIB.h - C API for emitting SMTLIB ------ ---*- C -*-===//
1
+ //===- mlir -c/Target/ ExportSMTLIB.h - C API for emitting SMTLIB ---*- C -*-===//
2
2
//
3
- // This header declares the C interface for emitting SMTLIB from a MLIR MLIR
4
- // module.
3
+ // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4
+ // See https://llvm.org/LICENSE.txt for license information.
5
+ // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6
+ //
7
+ //===----------------------------------------------------------------------===//
8
+ //
9
+ // This header declares the C interface for emitting SMTLIB from an MLIR module.
5
10
//
6
11
//===----------------------------------------------------------------------===//
7
12
Original file line number Diff line number Diff line change 8
8
9
9
#include " mlir-c/Dialect/SMT.h"
10
10
#include " mlir/CAPI/Registration.h"
11
+ #include " mlir/Dialect/SMT/IR/SMTAttributes.h"
11
12
#include " mlir/Dialect/SMT/IR/SMTDialect.h"
12
- #include " mlir/Dialect/SMT/IR/SMTOps .h"
13
+ #include " mlir/Dialect/SMT/IR/SMTTypes .h"
13
14
14
15
using namespace mlir ;
15
16
using namespace smt ;
Original file line number Diff line number Diff line change 1
1
// ===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===//
2
2
//
3
- // Implements a C Interface for export SMTLIB.
3
+ // Part of the LLVM Project, under the Apache License v2.0 with LLVM
4
+ // Exceptions.
5
+ // See https://llvm.org/LICENSE.txt for license information.
6
+ // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
7
+ //
8
+ // ===----------------------------------------------------------------------===//
9
+ //
10
+ // Implements a C Interface for export SMTLIB.
4
11
//
5
12
// ===----------------------------------------------------------------------===//
6
13
Original file line number Diff line number Diff line change 1
-
2
- /*===- smtlib.c - Simple test of SMTLIB C API -----------------------------===*\
3
- |* *|
4
- |* Part of the LLVM Project, under the Apache License v2.0 with LLVM *|
5
- |* Exceptions. *|
6
- |* See https://llvm.org/LICENSE.txt for license information. *|
7
- |* SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception *|
8
- |* *|
9
- \*===----------------------------------------------------------------------===*/
1
+ //===- smt.c - Test of SMT APIs -------------------------------------------===//
2
+ //
3
+ // Part of the LLVM Project, under the Apache License v2.0 with LLVM
4
+ // Exceptions.
5
+ // See https://llvm.org/LICENSE.txt for license information.
6
+ // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
7
+ //
8
+ //===----------------------------------------------------------------------===//
10
9
11
10
/* RUN: mlir-capi-smt-test 2>&1 | FileCheck %s
12
11
*/
You can’t perform that action at this time.
0 commit comments