terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[LLVM] bump to 9deb08a and integrate upstream SMT C APIs (#8424)

This commit is contained in:
Maksim Levental 2025-04-17 15:26:22 -04:00 committed by GitHub
parent d9ed306fcb
commit d07c799f60
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
38 changed files with 6 additions and 3322 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
CODEOWNERS
View File

@ -45,7 +45,6 @@ tools/arcilator @fabianschuiki @maerhart
# SMT
**/Dialect/SMT @maerhart
lib/Conversion/SMTToZ3LLVM @maerhart
lib/Target/ExportSMTLIB @maerhart
# SV
**/Dialect/SV @darthscsi

110
include/circt-c/Dialect/SMT.h
View File

@ -1,110 +0,0 @@
//===- SMT.h - C interface for the SMT dialect --------------------*- C -*-===//
//
// 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
//
//===----------------------------------------------------------------------===//
#ifndef CIRCT_C_DIALECT_SMT_H
#define CIRCT_C_DIALECT_SMT_H
#include "mlir-c/IR.h"
#ifdef __cplusplus
extern "C" {
#endif
//===----------------------------------------------------------------------===//
// Dialect API.
//===----------------------------------------------------------------------===//
MLIR_DECLARE_CAPI_DIALECT_REGISTRATION(SMT, smt);
//===----------------------------------------------------------------------===//
// Type API.
//===----------------------------------------------------------------------===//
/// Checks if the given type is any non-func SMT value type.
MLIR_CAPI_EXPORTED bool smtTypeIsAnyNonFuncSMTValueType(MlirType type);
/// Checks if the given type is any SMT value type.
MLIR_CAPI_EXPORTED bool smtTypeIsAnySMTValueType(MlirType type);
/// Checks if the given type is a smt::ArrayType.
MLIR_CAPI_EXPORTED bool smtTypeIsAArray(MlirType type);
/// Creates an array type with the given domain and range types.
MLIR_CAPI_EXPORTED MlirType smtTypeGetArray(MlirContext ctx,
MlirType domainType,
MlirType rangeType);
/// Checks if the given type is a smt::BitVectorType.
MLIR_CAPI_EXPORTED bool smtTypeIsABitVector(MlirType type);
/// Creates a smt::BitVectorType with the given width.
MLIR_CAPI_EXPORTED MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width);
/// Checks if the given type is a smt::BoolType.
MLIR_CAPI_EXPORTED bool smtTypeIsABool(MlirType type);
/// Creates a smt::BoolType.
MLIR_CAPI_EXPORTED MlirType smtTypeGetBool(MlirContext ctx);
/// Checks if the given type is a smt::IntType.
MLIR_CAPI_EXPORTED bool smtTypeIsAInt(MlirType type);
/// Creates a smt::IntType.
MLIR_CAPI_EXPORTED MlirType smtTypeGetInt(MlirContext ctx);
/// Checks if the given type is a smt::FuncType.
MLIR_CAPI_EXPORTED bool smtTypeIsASMTFunc(MlirType type);
/// Creates a smt::FuncType with the given domain and range types.
MLIR_CAPI_EXPORTED MlirType smtTypeGetSMTFunc(MlirContext ctx,
size_t numberOfDomainTypes,
const MlirType *domainTypes,
MlirType rangeType);
/// Checks if the given type is a smt::SortType.
MLIR_CAPI_EXPORTED bool smtTypeIsASort(MlirType type);
/// Creates a smt::SortType with the given identifier and sort parameters.
MLIR_CAPI_EXPORTED MlirType smtTypeGetSort(MlirContext ctx,
MlirIdentifier identifier,
size_t numberOfSortParams,
const MlirType *sortParams);
//===----------------------------------------------------------------------===//
// Attribute API.
//===----------------------------------------------------------------------===//
/// Checks if the given string is a valid smt::BVCmpPredicate.
MLIR_CAPI_EXPORTED bool smtAttrCheckBVCmpPredicate(MlirContext ctx,
MlirStringRef str);
/// Checks if the given string is a valid smt::IntPredicate.
MLIR_CAPI_EXPORTED bool smtAttrCheckIntPredicate(MlirContext ctx,
MlirStringRef str);
/// Checks if the given attribute is a smt::SMTAttribute.
MLIR_CAPI_EXPORTED bool smtAttrIsASMTAttribute(MlirAttribute attr);
/// Creates a smt::BitVectorAttr with the given value and width.
MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetBitVector(MlirContext ctx,
uint64_t value,
unsigned width);
/// Creates a smt::BVCmpPredicateAttr with the given string.
MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetBVCmpPredicate(MlirContext ctx,
MlirStringRef str);
/// Creates a smt::IntPredicateAttr with the given string.
MLIR_CAPI_EXPORTED MlirAttribute smtAttrGetIntPredicate(MlirContext ctx,
MlirStringRef str);
#ifdef __cplusplus
}
#endif
#endif // CIRCT_C_DIALECT_SMT_H

27
include/circt-c/ExportSMTLIB.h
View File

@ -1,27 +0,0 @@
//===- circt-c/ExportSMTLIB.h - C API for emitting SMTLIB ---------*- C -*-===//
//
// This header declares the C interface for emitting SMTLIB from a CIRCT MLIR
// module.
//
//===----------------------------------------------------------------------===//
#ifndef CIRCT_C_EXPORTSMTLIB_H
#define CIRCT_C_EXPORTSMTLIB_H
#include "mlir-c/IR.h"
#ifdef __cplusplus
extern "C" {
#endif
/// Emits SMTLIB for the specified module using the provided callback and user
/// data
MLIR_CAPI_EXPORTED MlirLogicalResult mlirExportSMTLIB(MlirModule,
MlirStringCallback,
void *userData);
#ifdef __cplusplus
}
#endif
#endif // CIRCT_C_EXPORTSMTLIB_H

4
include/circt/InitAllTranslations.h
View File

@ -18,8 +18,8 @@
#include "circt/Dialect/FIRRTL/FIRParser.h"
#include "circt/Dialect/MSFT/ExportTcl.h"
#include "circt/Target/DebugInfo.h"
#include "circt/Target/ExportSMTLIB.h"
#include "circt/Target/ExportSystemC.h"
#include "mlir/Target/SMTLIB/ExportSMTLIB.h"
#ifndef CIRCT_INITALLTRANSLATIONS_H
#define CIRCT_INITALLTRANSLATIONS_H
@ -35,7 +35,7 @@ inline void registerAllTranslations() {
calyx::registerToCalyxTranslation();
firrtl::registerFromFIRFileTranslation();
firrtl::registerToFIRFileTranslation();
ExportSMTLIB::registerExportSMTLIBTranslation();
mlir::smt::registerExportSMTLIBTranslation();
ExportSystemC::registerExportSystemCTranslation();
debug::registerTranslations();
return true;

42
include/circt/Target/ExportSMTLIB.h
View File

@ -1,42 +0,0 @@
//===- ExportSMTLIB.h - SMT-LIB Exporter ------------------------*- C++ -*-===//
//
// 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
//
//===----------------------------------------------------------------------===//
//
// Defines the interface to the SMT-LIB emitter.
//
//===----------------------------------------------------------------------===//
#ifndef CIRCT_TARGET_EXPORTSMTLIB_H
#define CIRCT_TARGET_EXPORTSMTLIB_H
#include "circt/Support/LLVM.h"
namespace circt {
namespace ExportSMTLIB {
/// Emission options for the ExportSMTLIB pass. Allows controlling the emitted
/// format and overall behavior.
struct SMTEmissionOptions {
// Don't produce 'let' expressions to bind expressions that are only used
// once, but inline them directly at the use-site.
bool inlineSingleUseValues = false;
// Increase indentation for each 'let' expression body.
bool indentLetBody = false;
};
/// Run the ExportSMTLIB pass.
LogicalResult
exportSMTLIB(Operation *module, llvm::raw_ostream &os,
const SMTEmissionOptions &options = SMTEmissionOptions());
/// Register the ExportSMTLIB pass.
void registerExportSMTLIBTranslation();
} // namespace ExportSMTLIB
} // namespace circt
#endif // CIRCT_TARGET_EXPORTSMTLIB_H

143
integration_test/Target/ExportSMTLIB/attributes.mlir
View File

@ -1,143 +0,0 @@
// RUN: circt-translate --export-smtlib %s > %t && z3 %t 2>&1 | FileCheck %s
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s > %t && z3 %t 2>&1 | FileCheck %s
// REQUIRES: z3
// Quantifiers Attributes
smt.solver () : () -> () {
%true = smt.constant true
%7 = smt.exists weight 2 {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
%5 = smt.implies %4, %true
smt.yield %5 : !smt.bool
}
smt.assert %7
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Quantifiers Attributes
smt.solver () : () -> () {
%true = smt.constant true
%7 = smt.exists weight 2 {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
%5 = smt.implies %4, %true
smt.yield %5 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %4: !smt.bool
}
smt.assert %7
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Quantifiers Attributes
smt.solver () : () -> () {
%true = smt.constant true
%7 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
%5 = smt.implies %4, %true
smt.yield %5 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %4: !smt.bool
}
smt.assert %7
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
smt.solver () : () -> () {
%true = smt.constant true
%three = smt.int.constant 3
%four = smt.int.constant 4
%7 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
%5 = smt.eq %arg3, %four: !smt.int
%6 = smt.eq %4, %5: !smt.bool
smt.yield %6 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
smt.yield %4: !smt.bool}, {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%5 = smt.eq %arg3, %four: !smt.int
smt.yield %5: !smt.bool
}
smt.assert %7
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
smt.solver () : () -> () {
%true = smt.constant true
%three = smt.int.constant 3
%four = smt.int.constant 4
%10 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
%5 = smt.eq %arg3, %four: !smt.int
%9 = smt.eq %4, %5: !smt.bool
smt.yield %9 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
%5 = smt.eq %arg3, %four: !smt.int
smt.yield %4, %5: !smt.bool, !smt.bool
}
smt.assert %10
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat

191
integration_test/Target/ExportSMTLIB/basic.mlir
View File

@ -1,191 +0,0 @@
// RUN: circt-translate --export-smtlib %s > %t && z3 %t 2>&1 | FileCheck %s
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s > %t && z3 %t 2>&1 | FileCheck %s
// REQUIRES: z3
// Function and constant symbol declarations, uninterpreted sorts
smt.solver () : () -> () {
%0 = smt.declare_fun "b" : !smt.bv<32>
%1 = smt.declare_fun : !smt.int
%2 = smt.declare_fun : !smt.func<(!smt.int, !smt.bv<32>) !smt.bool>
%3 = smt.apply_func %2(%1, %0) : !smt.func<(!smt.int, !smt.bv<32>) !smt.bool>
smt.assert %3
%4 = smt.declare_fun : !smt.sort<"uninterpreted">
%5 = smt.declare_fun : !smt.sort<"other"[!smt.sort<"uninterpreted">]>
%6 = smt.declare_fun : !smt.func<(!smt.sort<"other"[!smt.sort<"uninterpreted">]>, !smt.sort<"uninterpreted">) !smt.bool>
%7 = smt.apply_func %6(%5, %4) : !smt.func<(!smt.sort<"other"[!smt.sort<"uninterpreted">]>, !smt.sort<"uninterpreted">) !smt.bool>
smt.assert %7
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Big expression
smt.solver () : () -> () {
%true = smt.constant true
%false = smt.constant false
%0 = smt.not %true
%1 = smt.and %0, %true, %false
%2 = smt.or %1, %0, %true
%3 = smt.xor %0, %2
%4 = smt.implies %3, %false
%5 = smt.implies %4, %true
smt.assert %5
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Constant array
smt.solver () : () -> () {
%true = smt.constant true
%false = smt.constant false
%c = smt.int.constant 0
%0 = smt.array.broadcast %true : !smt.array<[!smt.int -> !smt.bool]>
%1 = smt.array.store %0[%c], %false : !smt.array<[!smt.int -> !smt.bool]>
%2 = smt.array.select %1[%c] : !smt.array<[!smt.int -> !smt.bool]>
smt.assert %2
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK: unsat
// BitVector extract and concat, and constants
smt.solver () : () -> () {
%xf = smt.bv.constant #smt.bv<0xf> : !smt.bv<4>
%x0 = smt.bv.constant #smt.bv<0> : !smt.bv<4>
%xff = smt.bv.constant #smt.bv<0xff> : !smt.bv<8>
%0 = smt.bv.concat %xf, %x0 : !smt.bv<4>, !smt.bv<4>
%1 = smt.bv.extract %0 from 4 : (!smt.bv<8>) -> !smt.bv<4>
%2 = smt.bv.repeat 2 times %1 : !smt.bv<4>
%3 = smt.eq %2, %xff : !smt.bv<8>
smt.assert %3
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Quantifiers
smt.solver () : () -> () {
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.int):
%c2_1 = smt.int.constant 2
%2 = smt.int.mul %arg2, %c2_1
%3 = smt.exists {
^bb0(%arg1: !smt.int):
%c2 = smt.int.constant 2
%4 = smt.int.mul %c2, %arg1
%5 = smt.eq %4, %2 : !smt.int
smt.yield %5 : !smt.bool
}
smt.yield %3 : !smt.bool
}
smt.assert %1
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Push and pop
smt.solver () : () -> () {
%three = smt.int.constant 3
%four = smt.int.constant 4
%unsat_eq = smt.eq %three, %four : !smt.int
%sat_eq = smt.eq %three, %three : !smt.int
smt.push 1
smt.assert %unsat_eq
smt.check sat {} unknown {} unsat {}
smt.pop 1
smt.assert %sat_eq
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: sat
// CHECK: unsat
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
// Reset
smt.solver () : () -> () {
%three = smt.int.constant 3
%four = smt.int.constant 4
%unsat_eq = smt.eq %three, %four : !smt.int
%sat_eq = smt.eq %three, %three : !smt.int
smt.assert %unsat_eq
smt.check sat {} unknown {} unsat {}
smt.reset
smt.assert %sat_eq
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: sat
// CHECK: unsat
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK: sat
smt.solver () : () -> () {
smt.set_logic "HORN"
%c = smt.declare_fun : !smt.int
%c4 = smt.int.constant 4
%eq = smt.eq %c, %c4 : !smt.int
smt.assert %eq
smt.check sat {} unknown {} unsat {}
}
// CHECK-NOT: WARNING
// CHECK-NOT: warning
// CHECK-NOT: ERROR
// CHECK-NOT: error
// CHECK-NOT: unsat
// CHECK-NOT: sat
// CHECK: unknown

2
lib/Bindings/Python/CIRCTModule.cpp
View File

@ -27,13 +27,13 @@
#ifdef CIRCT_INCLUDE_TESTS
#include "circt-c/Dialect/RTGTest.h"
#endif
#include "circt-c/Dialect/SMT.h"
#include "circt-c/Dialect/SV.h"
#include "circt-c/Dialect/Seq.h"
#include "circt-c/Dialect/Verif.h"
#include "circt-c/ExportVerilog.h"
#include "mlir-c/Bindings/Python/Interop.h"
#include "mlir-c/Dialect/Index.h"
#include "mlir-c/Dialect/SMT.h"
#include "mlir-c/IR.h"
#include "mlir-c/Transforms.h"
#include "mlir/Bindings/Python/NanobindAdaptors.h"

2
lib/Bindings/Python/CMakeLists.txt
View File

@ -48,11 +48,11 @@ set(PYTHON_BINDINGS_LINK_LIBS
CIRCTCAPIRTG
CIRCTCAPIRtgTool
CIRCTCAPISeq
CIRCTCAPISMT
CIRCTCAPISV
CIRCTCAPIVerif
CIRCTCAPITransforms
MLIRCAPIIndex
MLIRCAPISMT
# needed for mlirFrozenRewritePatternSetDestroy
# but not the actual passes
MLIRCAPITransforms

1
lib/CAPI/CMakeLists.txt
View File

@ -1,6 +1,5 @@
add_subdirectory(Conversion)
add_subdirectory(ExportFIRRTL)
add_subdirectory(ExportSMTLIB)
add_subdirectory(ExportVerilog)
add_subdirectory(Dialect)
add_subdirectory(Firtool)

9
lib/CAPI/Dialect/CMakeLists.txt
View File

@ -21,7 +21,6 @@ set(LLVM_OPTIONAL_SOURCES
RTGTest.cpp
SV.cpp
Seq.cpp
SMT.cpp
Verif.cpp
)
@ -225,11 +224,3 @@ add_circt_public_c_api_library(CIRCTCAPIEmit
MLIRCAPIIR
CIRCTEmit
)
add_circt_public_c_api_library(CIRCTCAPISMT
SMT.cpp
LINK_LIBS PUBLIC
MLIRCAPIIR
MLIRSMT
)

123
lib/CAPI/Dialect/SMT.cpp
View File

@ -1,123 +0,0 @@
//===- SMT.cpp - C interface for the SMT dialect --------------------------===//
//
// 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
//
//===----------------------------------------------------------------------===//
#include "circt-c/Dialect/SMT.h"
#include "mlir/Dialect/SMT/IR/SMTDialect.h"
#include "mlir/Dialect/SMT/IR/SMTOps.h"
#include "mlir/CAPI/Registration.h"
using namespace mlir;
using namespace smt;
//===----------------------------------------------------------------------===//
// Dialect API.
//===----------------------------------------------------------------------===//
MLIR_DEFINE_CAPI_DIALECT_REGISTRATION(SMT, smt, mlir::smt::SMTDialect)
//===----------------------------------------------------------------------===//
// Type API.
//===----------------------------------------------------------------------===//
bool smtTypeIsAnyNonFuncSMTValueType(MlirType type) {
return isAnyNonFuncSMTValueType(unwrap(type));
}
bool smtTypeIsAnySMTValueType(MlirType type) {
return isAnySMTValueType(unwrap(type));
}
bool smtTypeIsAArray(MlirType type) { return isa<ArrayType>(unwrap(type)); }
MlirType smtTypeGetArray(MlirContext ctx, MlirType domainType,
MlirType rangeType) {
return wrap(
ArrayType::get(unwrap(ctx), unwrap(domainType), unwrap(rangeType)));
}
bool smtTypeIsABitVector(MlirType type) {
return isa<BitVectorType>(unwrap(type));
}
MlirType smtTypeGetBitVector(MlirContext ctx, int32_t width) {
return wrap(BitVectorType::get(unwrap(ctx), width));
}
bool smtTypeIsABool(MlirType type) { return isa<BoolType>(unwrap(type)); }
MlirType smtTypeGetBool(MlirContext ctx) {
return wrap(BoolType::get(unwrap(ctx)));
}
bool smtTypeIsAInt(MlirType type) { return isa<IntType>(unwrap(type)); }
MlirType smtTypeGetInt(MlirContext ctx) {
return wrap(IntType::get(unwrap(ctx)));
}
bool smtTypeIsASMTFunc(MlirType type) { return isa<SMTFuncType>(unwrap(type)); }
MlirType smtTypeGetSMTFunc(MlirContext ctx, size_t numberOfDomainTypes,
const MlirType *domainTypes, MlirType rangeType) {
SmallVector<Type> domainTypesVec;
domainTypesVec.reserve(numberOfDomainTypes);
for (size_t i = 0; i < numberOfDomainTypes; i++)
domainTypesVec.push_back(unwrap(domainTypes[i]));
return wrap(SMTFuncType::get(unwrap(ctx), domainTypesVec, unwrap(rangeType)));
}
bool smtTypeIsASort(MlirType type) { return isa<SortType>(unwrap(type)); }
MlirType smtTypeGetSort(MlirContext ctx, MlirIdentifier identifier,
size_t numberOfSortParams, const MlirType *sortParams) {
SmallVector<Type> sortParamsVec;
sortParamsVec.reserve(numberOfSortParams);
for (size_t i = 0; i < numberOfSortParams; i++)
sortParamsVec.push_back(unwrap(sortParams[i]));
return wrap(SortType::get(unwrap(ctx), unwrap(identifier), sortParamsVec));
}
//===----------------------------------------------------------------------===//
// Attribute API.
//===----------------------------------------------------------------------===//
bool smtAttrCheckBVCmpPredicate(MlirContext ctx, MlirStringRef str) {
return symbolizeBVCmpPredicate(unwrap(str)).has_value();
}
bool smtAttrCheckIntPredicate(MlirContext ctx, MlirStringRef str) {
return symbolizeIntPredicate(unwrap(str)).has_value();
}
bool smtAttrIsASMTAttribute(MlirAttribute attr) {
return isa<BitVectorAttr, BVCmpPredicateAttr, IntPredicateAttr>(unwrap(attr));
}
MlirAttribute smtAttrGetBitVector(MlirContext ctx, uint64_t value,
unsigned width) {
return wrap(BitVectorAttr::get(unwrap(ctx), value, width));
}
MlirAttribute smtAttrGetBVCmpPredicate(MlirContext ctx, MlirStringRef str) {
auto predicate = symbolizeBVCmpPredicate(unwrap(str));
assert(predicate.has_value() && "invalid predicate");
return wrap(BVCmpPredicateAttr::get(unwrap(ctx), predicate.value()));
}
MlirAttribute smtAttrGetIntPredicate(MlirContext ctx, MlirStringRef str) {
auto predicate = symbolizeIntPredicate(unwrap(str));
assert(predicate.has_value() && "invalid predicate");
return wrap(IntPredicateAttr::get(unwrap(ctx), predicate.value()));
}

7
lib/CAPI/ExportSMTLIB/CMakeLists.txt
View File

@ -1,7 +0,0 @@
add_circt_public_c_api_library(CIRCTCAPIExportSMTLIB
ExportSMTLIB.cpp
LINK_LIBS PUBLIC
MLIRCAPIIR
CIRCTExportSMTLIB
)

22
lib/CAPI/ExportSMTLIB/ExportSMTLIB.cpp
View File

@ -1,22 +0,0 @@
//===- ExportSMTLIB.cpp - C Interface to ExportSMTLIB ---------------------===//
//
// Implements a C Interface for export SMTLIB.
//
//===----------------------------------------------------------------------===//
#include "circt-c/ExportSMTLIB.h"
#include "circt/Target/ExportSMTLIB.h"
#include "mlir/CAPI/IR.h"
#include "mlir/CAPI/Support.h"
#include "mlir/CAPI/Utils.h"
#include "llvm/Support/raw_ostream.h"
using namespace circt;
MlirLogicalResult mlirExportSMTLIB(MlirModule module,
MlirStringCallback callback,
void *userData) {
mlir::detail::CallbackOstream stream(callback, userData);
return wrap(ExportSMTLIB::exportSMTLIB(unwrap(module), stream));
}

1
lib/Target/CMakeLists.txt
View File

@ -1,3 +1,2 @@
add_subdirectory(DebugInfo)
add_subdirectory(ExportSMTLIB)
add_subdirectory(ExportSystemC)

16
lib/Target/ExportSMTLIB/CMakeLists.txt
View File

@ -1,16 +0,0 @@
add_circt_translation_library(CIRCTExportSMTLIB
ExportSMTLIB.cpp
ADDITIONAL_HEADER_DIRS
LINK_COMPONENTS
Core
LINK_LIBS PUBLIC
CIRCTHW
CIRCTSupport
MLIRFuncDialect
MLIRIR
MLIRSMT
MLIRTranslateLib
)

733
lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
View File

@ -1,733 +0,0 @@
//===- ExportSMTLIB.cpp - SMT-LIB Emitter -----=---------------------------===//
//
// 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
//
//===----------------------------------------------------------------------===//
//
// This is the main SMT-LIB emitter implementation.
//
//===----------------------------------------------------------------------===//
#include "circt/Target/ExportSMTLIB.h"
#include "circt/Dialect/HW/HWDialect.h"
#include "circt/Support/Namespace.h"
#include "mlir/Dialect/Func/IR/FuncOps.h"
#include "mlir/Dialect/SMT/IR/SMTOps.h"
#include "mlir/Dialect/SMT/IR/SMTVisitors.h"
#include "mlir/IR/BuiltinOps.h"
#include "mlir/Support/IndentedOstream.h"
#include "mlir/Tools/mlir-translate/Translation.h"
#include "llvm/ADT/ScopedHashTable.h"
#include "llvm/ADT/StringRef.h"
#include "llvm/Support/Format.h"
#include "llvm/Support/raw_ostream.h"
using namespace circt;
using namespace mlir;
using namespace smt;
using namespace ExportSMTLIB;
using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>;
#define DEBUG_TYPE "export-smtlib"
namespace {
/// A visitor to print the SMT dialect types as SMT-LIB formatted sorts.
/// Printing nested types use recursive calls since nestings of a depth that
/// could lead to problems should not occur in practice.
struct TypeVisitor : public smt::SMTTypeVisitor<TypeVisitor, void,
mlir::raw_indented_ostream &> {
TypeVisitor(const SMTEmissionOptions &options) : options(options) {}
void visitSMTType(BoolType type, mlir::raw_indented_ostream &stream) {
stream << "Bool";
}
void visitSMTType(IntType type, mlir::raw_indented_ostream &stream) {
stream << "Int";
}
void visitSMTType(BitVectorType type, mlir::raw_indented_ostream &stream) {
stream << "(_ BitVec " << type.getWidth() << ")";
}
void visitSMTType(ArrayType type, mlir::raw_indented_ostream &stream) {
stream << "(Array ";
dispatchSMTTypeVisitor(type.getDomainType(), stream);
stream << " ";
dispatchSMTTypeVisitor(type.getRangeType(), stream);
stream << ")";
}
void visitSMTType(SMTFuncType type, mlir::raw_indented_ostream &stream) {
stream << "(";
StringLiteral nextToken = "";
for (Type domainTy : type.getDomainTypes()) {
stream << nextToken;
dispatchSMTTypeVisitor(domainTy, stream);
nextToken = " ";
}
stream << ") ";
dispatchSMTTypeVisitor(type.getRangeType(), stream);
}
void visitSMTType(SortType type, mlir::raw_indented_ostream &stream) {
if (!type.getSortParams().empty())
stream << "(";
stream << type.getIdentifier().getValue();
for (Type paramTy : type.getSortParams()) {
stream << " ";
dispatchSMTTypeVisitor(paramTy, stream);
}
if (!type.getSortParams().empty())
stream << ")";
}
private:
// A reference to the emission options for easy use in the visitor methods.
[[maybe_unused]] const SMTEmissionOptions &options;
};
/// Contains the informations passed to the ExpressionVisitor methods. Makes it
/// easier to add more information.
struct VisitorInfo {
VisitorInfo(mlir::raw_indented_ostream &stream, ValueMap &valueMap)
: stream(stream), valueMap(valueMap) {}
VisitorInfo(mlir::raw_indented_ostream &stream, ValueMap &valueMap,
unsigned indentLevel, unsigned openParens)
: stream(stream), valueMap(valueMap), indentLevel(indentLevel),
openParens(openParens) {}
// Stream to print to.
mlir::raw_indented_ostream &stream;
// Mapping from SSA values to SMT-LIB expressions.
ValueMap &valueMap;
// Total number of spaces currently indented.
unsigned indentLevel = 0;
// Number of parentheses that have been opened but not closed yet.
unsigned openParens = 0;
};
/// A visitor to print SMT dialect operations with exactly one result value as
/// the equivalent operator in SMT-LIB.
struct ExpressionVisitor
: public smt::SMTOpVisitor<ExpressionVisitor, LogicalResult,
VisitorInfo &> {
using Base =
smt::SMTOpVisitor<ExpressionVisitor, LogicalResult, VisitorInfo &>;
using Base::visitSMTOp;
ExpressionVisitor(const SMTEmissionOptions &options, Namespace &names)
: options(options), typeVisitor(options), names(names) {}
LogicalResult dispatchSMTOpVisitor(Operation *op, VisitorInfo &info) {
assert(op->getNumResults() == 1 &&
"expression op must have exactly one result value");
// Print the expression inlined if it is only used once and the
// corresponding emission option is enabled. This can lead to bad
// performance for big inputs since the inlined expression is stored as a
// string in the value mapping where otherwise only the symbol names of free
// and bound variables are stored, and due to a lot of string concatenation
// (thus it's off by default and just intended to print small examples in a
// more human-readable format).
Value res = op->getResult(0);
if (res.hasOneUse() && options.inlineSingleUseValues) {
std::string str;
llvm::raw_string_ostream sstream(str);
mlir::raw_indented_ostream indentedStream(sstream);
VisitorInfo newInfo(indentedStream, info.valueMap, info.indentLevel,
info.openParens);
if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
return failure();
info.valueMap.insert(res, str);
return success();
}
// Generate a let binding for the current expression being processed and
// store the sybmol in the value map. Indent the expressions for easier
// readability.
auto name = names.newName("tmp");
info.valueMap.insert(res, name.str());
info.stream << "(let ((" << name << " ";
VisitorInfo newInfo(info.stream, info.valueMap,
info.indentLevel + 8 + name.size(), 0);
if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
return failure();
info.stream << "))\n";
if (options.indentLetBody) {
// Five spaces to align with the opening parenthesis
info.indentLevel += 5;
}
++info.openParens;
info.stream.indent(info.indentLevel);
return success();
}
//===--------------------------------------------------------------------===//
// Bit-vector theory operation visitors
//===--------------------------------------------------------------------===//
template <typename Op>
LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) {
info.stream << "(" << name << " " << info.valueMap.lookup(op.getLhs())
<< " " << info.valueMap.lookup(op.getRhs()) << ")";
return success();
}
template <typename Op>
LogicalResult printVariadicOp(Op op, StringRef name, VisitorInfo &info) {
info.stream << "(" << name;
for (Value val : op.getOperands())
info.stream << " " << info.valueMap.lookup(val);
info.stream << ")";
return success();
}
LogicalResult visitSMTOp(BVNegOp op, VisitorInfo &info) {
info.stream << "(bvneg " << info.valueMap.lookup(op.getInput()) << ")";
return success();
}
LogicalResult visitSMTOp(BVNotOp op, VisitorInfo &info) {
info.stream << "(bvnot " << info.valueMap.lookup(op.getInput()) << ")";
return success();
}
#define HANDLE_OP(OPTYPE, NAME, KIND) \
LogicalResult visitSMTOp(OPTYPE op, VisitorInfo &info) { \
return print##KIND##Op(op, NAME, info); \
}
HANDLE_OP(BVAddOp, "bvadd", Binary);
HANDLE_OP(BVMulOp, "bvmul", Binary);
HANDLE_OP(BVURemOp, "bvurem", Binary);
HANDLE_OP(BVSRemOp, "bvsrem", Binary);
HANDLE_OP(BVSModOp, "bvsmod", Binary);
HANDLE_OP(BVShlOp, "bvshl", Binary);
HANDLE_OP(BVLShrOp, "bvlshr", Binary);
HANDLE_OP(BVAShrOp, "bvashr", Binary);
HANDLE_OP(BVUDivOp, "bvudiv", Binary);
HANDLE_OP(BVSDivOp, "bvsdiv", Binary);
HANDLE_OP(BVAndOp, "bvand", Binary);
HANDLE_OP(BVOrOp, "bvor", Binary);
HANDLE_OP(BVXOrOp, "bvxor", Binary);
HANDLE_OP(ConcatOp, "concat", Binary);
LogicalResult visitSMTOp(ExtractOp op, VisitorInfo &info) {
info.stream << "((_ extract "
<< (op.getLowBit() + op.getType().getWidth() - 1) << " "
<< op.getLowBit() << ") " << info.valueMap.lookup(op.getInput())
<< ")";
return success();
}
LogicalResult visitSMTOp(RepeatOp op, VisitorInfo &info) {
info.stream << "((_ repeat " << op.getCount() << ") "
<< info.valueMap.lookup(op.getInput()) << ")";
return success();
}
LogicalResult visitSMTOp(BVCmpOp op, VisitorInfo &info) {
return printBinaryOp(op, "bv" + stringifyBVCmpPredicate(op.getPred()).str(),
info);
}
//===--------------------------------------------------------------------===//
// Int theory operation visitors
//===--------------------------------------------------------------------===//
HANDLE_OP(IntAddOp, "+", Variadic);
HANDLE_OP(IntMulOp, "*", Variadic);
HANDLE_OP(IntSubOp, "-", Binary);
HANDLE_OP(IntDivOp, "div", Binary);
HANDLE_OP(IntModOp, "mod", Binary);
LogicalResult visitSMTOp(IntCmpOp op, VisitorInfo &info) {
switch (op.getPred()) {
case IntPredicate::ge:
return printBinaryOp(op, ">=", info);
case IntPredicate::le:
return printBinaryOp(op, "<=", info);
case IntPredicate::gt:
return printBinaryOp(op, ">", info);
case IntPredicate::lt:
return printBinaryOp(op, "<", info);
}
return failure();
}
//===--------------------------------------------------------------------===//
// Core theory operation visitors
//===--------------------------------------------------------------------===//
HANDLE_OP(EqOp, "=", Variadic);
HANDLE_OP(DistinctOp, "distinct", Variadic);
LogicalResult visitSMTOp(IteOp op, VisitorInfo &info) {
info.stream << "(ite " << info.valueMap.lookup(op.getCond()) << " "
<< info.valueMap.lookup(op.getThenValue()) << " "
<< info.valueMap.lookup(op.getElseValue()) << ")";
return success();
}
LogicalResult visitSMTOp(ApplyFuncOp op, VisitorInfo &info) {
info.stream << "(" << info.valueMap.lookup(op.getFunc());
for (Value arg : op.getArgs())
info.stream << " " << info.valueMap.lookup(arg);
info.stream << ")";
return success();
}
template <typename OpTy>
LogicalResult quantifierHelper(OpTy op, StringRef operatorString,
VisitorInfo &info) {
auto weight = op.getWeight();
auto patterns = op.getPatterns();
// TODO: add support
if (op.getNoPattern())
return op.emitError() << "no-pattern attribute not supported yet";
llvm::ScopedHashTableScope<Value, std::string> scope(info.valueMap);
info.stream << "(" << operatorString << " (";
StringLiteral delimiter = "";
SmallVector<StringRef> argNames;
for (auto [i, arg] : llvm::enumerate(op.getBody().getArguments())) {
// Generate and register a new unique name.
StringRef prefix =
op.getBoundVarNames()
? cast<StringAttr>(op.getBoundVarNames()->getValue()[i])
.getValue()
: "tmp";
StringRef name = names.newName(prefix);
argNames.push_back(name);
info.valueMap.insert(arg, name.str());
// Print the bound variable declaration.
info.stream << delimiter << "(" << name << " ";
typeVisitor.dispatchSMTTypeVisitor(arg.getType(), info.stream);
info.stream << ")";
delimiter = " ";
}
info.stream << ")\n";
// Print the quantifier body. This assumes that quantifiers are not deeply
// nested (at least not enough that recursive calls could become a problem).
SmallVector<Value> worklist;
Value yieldedValue = op.getBody().front().getTerminator()->getOperand(0);
worklist.push_back(yieldedValue);
unsigned indentExt = operatorString.size() + 2;
VisitorInfo newInfo(info.stream, info.valueMap,
info.indentLevel + indentExt, 0);
if (weight != 0 || !patterns.empty())
newInfo.stream.indent(newInfo.indentLevel);
else
newInfo.stream.indent(info.indentLevel);
if (weight != 0 || !patterns.empty())
info.stream << "( ! ";
if (failed(printExpression(worklist, newInfo)))
return failure();
info.stream << info.valueMap.lookup(yieldedValue);
for (unsigned j = 0; j < newInfo.openParens; ++j)
info.stream << ")";
if (weight != 0)
info.stream << " :weight " << weight;
if (!patterns.empty()) {
bool first = true;
info.stream << "\n:pattern (";
for (auto &p : patterns) {
if (!first)
info.stream << " ";
// retrieve argument name from the body region
for (auto [i, arg] : llvm::enumerate(p.getArguments()))
info.valueMap.insert(arg, argNames[i].str());
SmallVector<Value> worklist;
// retrieve all yielded operands in pattern region
for (auto yieldedValue : p.front().getTerminator()->getOperands()) {
worklist.push_back(yieldedValue);
unsigned indentExt = operatorString.size() + 2;
VisitorInfo newInfo2(info.stream, info.valueMap,
info.indentLevel + indentExt, 0);
info.stream.indent(0);
if (failed(printExpression(worklist, newInfo2)))
return failure();
info.stream << info.valueMap.lookup(yieldedValue);
for (unsigned j = 0; j < newInfo2.openParens; ++j)
info.stream << ")";
}
first = false;
}
info.stream << ")";
}
if (weight != 0 || !patterns.empty())
info.stream << ")";
info.stream << ")";
return success();
}
LogicalResult visitSMTOp(ForallOp op, VisitorInfo &info) {
return quantifierHelper(op, "forall", info);
}
LogicalResult visitSMTOp(ExistsOp op, VisitorInfo &info) {
return quantifierHelper(op, "exists", info);
}
LogicalResult visitSMTOp(NotOp op, VisitorInfo &info) {
info.stream << "(not " << info.valueMap.lookup(op.getInput()) << ")";
return success();
}
HANDLE_OP(AndOp, "and", Variadic);
HANDLE_OP(OrOp, "or", Variadic);
HANDLE_OP(XOrOp, "xor", Variadic);
HANDLE_OP(ImpliesOp, "=>", Binary);
//===--------------------------------------------------------------------===//
// Array theory operation visitors
//===--------------------------------------------------------------------===//
LogicalResult visitSMTOp(ArrayStoreOp op, VisitorInfo &info) {
info.stream << "(store " << info.valueMap.lookup(op.getArray()) << " "
<< info.valueMap.lookup(op.getIndex()) << " "
<< info.valueMap.lookup(op.getValue()) << ")";
return success();
}
LogicalResult visitSMTOp(ArraySelectOp op, VisitorInfo &info) {
info.stream << "(select " << info.valueMap.lookup(op.getArray()) << " "
<< info.valueMap.lookup(op.getIndex()) << ")";
return success();
}
LogicalResult visitSMTOp(ArrayBroadcastOp op, VisitorInfo &info) {
info.stream << "((as const ";
typeVisitor.dispatchSMTTypeVisitor(op.getType(), info.stream);
info.stream << ") " << info.valueMap.lookup(op.getValue()) << ")";
return success();
}
LogicalResult visitUnhandledSMTOp(Operation *op, VisitorInfo &info) {
return success();
}
#undef HANDLE_OP
/// Print an expression transitively. The root node should be added to the
/// 'worklist' before calling.
LogicalResult printExpression(SmallVector<Value> &worklist,
VisitorInfo &info) {
while (!worklist.empty()) {
Value curr = worklist.back();
// If we already have a let-binding for the value, just print it.
if (info.valueMap.count(curr)) {
worklist.pop_back();
continue;
}
// Traverse until we reach a value/operation that has all operands
// available and can thus be printed.
bool allAvailable = true;
Operation *defOp = curr.getDefiningOp();
assert(defOp != nullptr &&
"block arguments must already be in the valueMap");
for (Value val : defOp->getOperands()) {
if (!info.valueMap.count(val)) {
worklist.push_back(val);
allAvailable = false;
}
}
if (!allAvailable)
continue;
if (failed(dispatchSMTOpVisitor(curr.getDefiningOp(), info)))
return failure();
worklist.pop_back();
}
return success();
}
private:
// A reference to the emission options for easy use in the visitor methods.
[[maybe_unused]] const SMTEmissionOptions &options;
TypeVisitor typeVisitor;
Namespace &names;
};
/// A visitor to print SMT dialect operations with zero result values or
/// ones that have to initialize some global state.
struct StatementVisitor
: public smt::SMTOpVisitor<StatementVisitor, LogicalResult,
mlir::raw_indented_ostream &, ValueMap &> {
using smt::SMTOpVisitor<StatementVisitor, LogicalResult,
mlir::raw_indented_ostream &, ValueMap &>::visitSMTOp;
StatementVisitor(const SMTEmissionOptions &options, Namespace &names)
: options(options), typeVisitor(options), names(names),
exprVisitor(options, names) {}
LogicalResult visitSMTOp(BVConstantOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
valueMap.insert(op.getResult(), op.getValue().getValueAsString());
return success();
}
LogicalResult visitSMTOp(BoolConstantOp op,
mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
valueMap.insert(op.getResult(), op.getValue() ? "true" : "false");
return success();
}
LogicalResult visitSMTOp(IntConstantOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
SmallString<16> str;
op.getValue().toStringSigned(str);
valueMap.insert(op.getResult(), str.str().str());
return success();
}
LogicalResult visitSMTOp(DeclareFunOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
StringRef name =
names.newName(op.getNamePrefix() ? *op.getNamePrefix() : "tmp");
valueMap.insert(op.getResult(), name.str());
stream << "("
<< (isa<SMTFuncType>(op.getType()) ? "declare-fun "
: "declare-const ")
<< name << " ";
typeVisitor.dispatchSMTTypeVisitor(op.getType(), stream);
stream << ")\n";
return success();
}
LogicalResult visitSMTOp(AssertOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
llvm::ScopedHashTableScope<Value, std::string> scope1(valueMap);
SmallVector<Value> worklist;
worklist.push_back(op.getInput());
stream << "(assert ";
VisitorInfo info(stream, valueMap, 8, 0);
if (failed(exprVisitor.printExpression(worklist, info)))
return failure();
stream << valueMap.lookup(op.getInput());
for (unsigned i = 0; i < info.openParens + 1; ++i)
stream << ")";
stream << "\n";
stream.indent(0);
return success();
}
LogicalResult visitSMTOp(ResetOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
stream << "(reset)\n";
return success();
}
LogicalResult visitSMTOp(PushOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
stream << "(push " << op.getCount() << ")\n";
return success();
}
LogicalResult visitSMTOp(PopOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
stream << "(pop " << op.getCount() << ")\n";
return success();
}
LogicalResult visitSMTOp(CheckOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
if (op->getNumResults() != 0)
return op.emitError() << "must not have any result values";
if (op.getSatRegion().front().getOperations().size() != 1)
return op->emitError() << "'sat' region must be empty";
if (op.getUnknownRegion().front().getOperations().size() != 1)
return op->emitError() << "'unknown' region must be empty";
if (op.getUnsatRegion().front().getOperations().size() != 1)
return op->emitError() << "'unsat' region must be empty";
stream << "(check-sat)\n";
return success();
}
LogicalResult visitSMTOp(SetLogicOp op, mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
stream << "(set-logic " << op.getLogic() << ")\n";
return success();
}
LogicalResult visitUnhandledSMTOp(Operation *op,
mlir::raw_indented_ostream &stream,
ValueMap &valueMap) {
// Ignore operations which are handled in the Expression Visitor.
if (isa<smt::Int2BVOp, BV2IntOp>(op))
return op->emitError("operation not supported for SMTLIB emission");
return success();
}
private:
// A reference to the emission options for easy use in the visitor methods.
[[maybe_unused]] const SMTEmissionOptions &options;
TypeVisitor typeVisitor;
Namespace &names;
ExpressionVisitor exprVisitor;
};
} // namespace
//===----------------------------------------------------------------------===//
// Unified Emitter implementation
//===----------------------------------------------------------------------===//
/// Emit the SMT operations in the given 'solver' to the 'stream'.
static LogicalResult emit(SolverOp solver, const SMTEmissionOptions &options,
mlir::raw_indented_ostream &stream) {
if (!solver.getInputs().empty() || solver->getNumResults() != 0)
return solver->emitError()
<< "solver scopes with inputs or results are not supported";
Block *block = solver.getBody();
// Declare uninterpreted sorts.
DenseMap<StringAttr, unsigned> declaredSorts;
auto result = block->walk([&](Operation *op) -> WalkResult {
if (!isa<SMTDialect>(op->getDialect()))
return op->emitError()
<< "solver must not contain any non-SMT operations";
for (Type resTy : op->getResultTypes()) {
auto sortTy = dyn_cast<SortType>(resTy);
if (!sortTy)
continue;
unsigned arity = sortTy.getSortParams().size();
if (declaredSorts.contains(sortTy.getIdentifier())) {
if (declaredSorts[sortTy.getIdentifier()] != arity)
return op->emitError("uninterpreted sorts with same identifier but "
"different arity found");
continue;
}
declaredSorts[sortTy.getIdentifier()] = arity;
stream << "(declare-sort " << sortTy.getIdentifier().getValue() << " "
<< arity << ")\n";
}
return WalkResult::advance();
});
if (result.wasInterrupted())
return failure();
ValueMap valueMap;
llvm::ScopedHashTableScope<Value, std::string> scope0(valueMap);
Namespace names;
StatementVisitor visitor(options, names);
// Collect all statement operations (ops with no result value).
// Declare constants and then only refer to them by identifier later on.
result = block->walk([&](Operation *op) {
if (failed(visitor.dispatchSMTOpVisitor(op, stream, valueMap)))
return WalkResult::interrupt();
return WalkResult::advance();
});
if (result.wasInterrupted())
return failure();
stream << "(reset)\n";
return success();
}
LogicalResult ExportSMTLIB::exportSMTLIB(Operation *module,
llvm::raw_ostream &os,
const SMTEmissionOptions &options) {
if (module->getNumRegions() != 1)
return module->emitError("must have exactly one region");
if (!module->getRegion(0).hasOneBlock())
return module->emitError("op region must have exactly one block");
mlir::raw_indented_ostream ios(os);
unsigned solverIdx = 0;
auto result = module->walk([&](SolverOp solver) {
ios << "; solver scope " << solverIdx << "\n";
if (failed(emit(solver, options, ios)))
return WalkResult::interrupt();
++solverIdx;
return WalkResult::advance();
});
return failure(result.wasInterrupted());
}
//===----------------------------------------------------------------------===//
// circt-translate registration
//===----------------------------------------------------------------------===//
void ExportSMTLIB::registerExportSMTLIBTranslation() {
static llvm::cl::opt<bool> inlineSingleUseValues(
"smtlibexport-inline-single-use-values",
llvm::cl::desc("Inline expressions that are used only once rather than "
"generating a let-binding"),
llvm::cl::init(false));
auto getOptions = [] {
SMTEmissionOptions opts;
opts.inlineSingleUseValues = inlineSingleUseValues;
return opts;
};
static mlir::TranslateFromMLIRRegistration toSMTLIB(
"export-smtlib", "export SMT-LIB",
[=](Operation *module, raw_ostream &output) {
return ExportSMTLIB::exportSMTLIB(module, output, getOptions());
},
[](mlir::DialectRegistry &registry) {
// Register the 'func' and 'HW' dialects to support printing solver
// scopes nested in functions and modules.
registry
.insert<mlir::func::FuncDialect, hw::HWDialect, smt::SMTDialect>();
});
}

2
llvm

@ -1 +1 @@
Subproject commit c6a892e0ed82a378ad1a69905f70700bf57c68cf
Subproject commit 9deb08a30196b5b3b3883b5c7be8c4251039bde7

16
test/CAPI/CMakeLists.txt
View File

@ -13,7 +13,6 @@ target_link_libraries(circt-capi-ir-test
CIRCTCAPISV
CIRCTCAPIFSM
CIRCTCAPIExportFIRRTL
CIRCTCAPIExportSMTLIB
CIRCTCAPIExportVerilog
)
@ -64,21 +63,6 @@ add_llvm_executable(circt-capi-arc-test
)
llvm_update_compile_flags(circt-capi-arc-test)
add_llvm_executable(circt-capi-smtlib-test
PARTIAL_SOURCES_INTENDED
smtlib.c
)
llvm_update_compile_flags(circt-capi-smtlib-test)
target_link_libraries(circt-capi-smtlib-test
PRIVATE
MLIRCAPIIR
MLIRCAPIFunc
CIRCTCAPISMT
CIRCTCAPIExportSMTLIB
)
target_link_libraries(circt-capi-arc-test
PRIVATE

182
test/CAPI/smtlib.c
View File

@ -1,182 +0,0 @@
/*===- smtlib.c - Simple test of SMTLIB C API -----------------------------===*\
|* *|
|* 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: circt-capi-smtlib-test 2>&1 | FileCheck %s
*/
#include "circt-c/Dialect/SMT.h"
#include "circt-c/ExportSMTLIB.h"
#include "mlir-c/Dialect/Func.h"
#include "mlir-c/IR.h"
#include "mlir-c/Support.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 = mlirExportSMTLIB(module, dumpCallback, NULL);
(void)result;
assert(mlirLogicalResultIsSuccess(result));
// CHECK: ; solver scope 0
// CHECK-NEXT: (reset)
}
void testSMTType(MlirContext ctx) {
MlirType boolType = smtTypeGetBool(ctx);
MlirType intType = smtTypeGetInt(ctx);
MlirType arrayType = smtTypeGetArray(ctx, intType, boolType);
MlirType bvType = smtTypeGetBitVector(ctx, 32);
MlirType funcType =
smtTypeGetSMTFunc(ctx, 2, (MlirType[]){intType, boolType}, boolType);
MlirType sortType = smtTypeGetSort(
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, smtTypeIsAnyNonFuncSMTValueType(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, smtTypeIsAnyNonFuncSMTValueType(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, smtTypeIsAnyNonFuncSMTValueType(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, smtTypeIsAnyNonFuncSMTValueType(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, smtTypeIsAnyNonFuncSMTValueType(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, smtTypeIsAnyNonFuncSMTValueType(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, smtTypeIsAnySMTValueType(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, smtTypeIsAnySMTValueType(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, smtTypeIsAnySMTValueType(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, smtTypeIsAnySMTValueType(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, smtTypeIsAnySMTValueType(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, smtTypeIsAnySMTValueType(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, smtTypeIsABool(intType) ? "int_type_is_a_bool\n"
: "int_type_is_not_a_bool\n");
// CHECK: bool_type_is_not_a_int
fprintf(stderr, smtTypeIsAInt(boolType) ? "bool_type_is_a_int\n"
: "bool_type_is_not_a_int\n");
// CHECK: bv_type_is_not_a_array
fprintf(stderr, smtTypeIsAArray(bvType) ? "bv_type_is_a_array\n"
: "bv_type_is_not_a_array\n");
// CHECK: array_type_is_not_a_bit_vector
fprintf(stderr, smtTypeIsABitVector(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, smtTypeIsASMTFunc(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, smtTypeIsASort(funcType) ? "func_type_is_a_sort\n"
: "func_type_is_not_a_sort\n");
}
void testSMTAttribute(MlirContext ctx) {
// CHECK: slt_is_BVCmpPredicate
fprintf(stderr,
smtAttrCheckBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt"))
? "slt_is_BVCmpPredicate\n"
: "slt_is_not_BVCmpPredicate\n");
// CHECK: lt_is_not_BVCmpPredicate
fprintf(stderr,
smtAttrCheckBVCmpPredicate(ctx, mlirStringRefCreateFromCString("lt"))
? "lt_is_BVCmpPredicate\n"
: "lt_is_not_BVCmpPredicate\n");
// CHECK: slt_is_not_IntPredicate
fprintf(stderr,
smtAttrCheckIntPredicate(ctx, mlirStringRefCreateFromCString("slt"))
? "slt_is_IntPredicate\n"
: "slt_is_not_IntPredicate\n");
// CHECK: lt_is_IntPredicate
fprintf(stderr,
smtAttrCheckIntPredicate(ctx, mlirStringRefCreateFromCString("lt"))
? "lt_is_IntPredicate\n"
: "lt_is_not_IntPredicate\n");
// CHECK: #smt.bv<5> : !smt.bv<32>
mlirAttributeDump(smtAttrGetBitVector(ctx, 5, 32));
// CHECK: 0 : i64
mlirAttributeDump(
smtAttrGetBVCmpPredicate(ctx, mlirStringRefCreateFromCString("slt")));
// CHECK: 0 : i64
mlirAttributeDump(
smtAttrGetIntPredicate(ctx, mlirStringRefCreateFromCString("lt")));
}
int main(void) {
MlirContext ctx = mlirContextCreate();
mlirDialectHandleLoadDialect(mlirGetDialectHandle__smt__(), ctx);
mlirDialectHandleLoadDialect(mlirGetDialectHandle__func__(), ctx);
testExportSMTLIB(ctx);
testSMTType(ctx);
testSMTAttribute(ctx);
return 0;
}

1
test/CMakeLists.txt
View File

@ -25,7 +25,6 @@ set(CIRCT_TEST_DEPENDS
circt-capi-rtg-pipelines-test
circt-capi-rtg-test
circt-capi-rtgtest-test
circt-capi-smtlib-test
circt-as
circt-bmc
circt-dis

13
test/Dialect/SMT/array-errors.mlir
View File

@ -1,13 +0,0 @@
// RUN: circt-opt %s --split-input-file --verify-diagnostics
// expected-error @below {{domain must be any SMT value type}}
func.func @array_domain_no_smt_type(%arg0: !smt.array<[i32 -> !smt.bool]>) {
return
}
// -----
// expected-error @below {{range must be any SMT value type}}
func.func @array_range_no_smt_type(%arg0: !smt.array<[!smt.bool -> i32]>) {
return
}

14
test/Dialect/SMT/array.mlir
View File

@ -1,14 +0,0 @@
// RUN: circt-opt %s | circt-opt | FileCheck %s
// CHECK-LABEL: func @arrayOperations
// CHECK-SAME: ([[A0:%.+]]: !smt.bool)
func.func @arrayOperations(%arg0: !smt.bool) {
// CHECK-NEXT: [[V0:%.+]] = smt.array.broadcast [[A0]] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
%0 = smt.array.broadcast %arg0 {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
// CHECK-NEXT: [[V1:%.+]] = smt.array.select [[V0]][[[A0]]] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
%1 = smt.array.select %0[%arg0] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
// CHECK-NEXT: [[V2:%.+]] = smt.array.store [[V0]][[[A0]]], [[A0]] {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
%2 = smt.array.store %0[%arg0], %arg0 {smt.some_attr} : !smt.array<[!smt.bool -> !smt.bool]>
return
}

200
test/Dialect/SMT/basic.mlir
View File

@ -1,200 +0,0 @@
// RUN: circt-opt %s | circt-opt | FileCheck %s
// CHECK-LABEL: func @types
// CHECK-SAME: (%{{.*}}: !smt.bool, %{{.*}}: !smt.bv<32>, %{{.*}}: !smt.int, %{{.*}}: !smt.sort<"uninterpreted_sort">, %{{.*}}: !smt.sort<"uninterpreted_sort"[!smt.bool, !smt.int]>, %{{.*}}: !smt.func<(!smt.bool, !smt.bool) !smt.bool>)
func.func @types(%arg0: !smt.bool, %arg1: !smt.bv<32>, %arg2: !smt.int, %arg3: !smt.sort<"uninterpreted_sort">, %arg4: !smt.sort<"uninterpreted_sort"[!smt.bool, !smt.int]>, %arg5: !smt.func<(!smt.bool, !smt.bool) !smt.bool>) {
return
}
func.func @core(%in: i8) {
// CHECK: %a = smt.declare_fun "a" {smt.some_attr} : !smt.bool
%a = smt.declare_fun "a" {smt.some_attr} : !smt.bool
// CHECK: smt.declare_fun {smt.some_attr} : !smt.bv<32>
%b = smt.declare_fun {smt.some_attr} : !smt.bv<32>
// CHECK: smt.declare_fun {smt.some_attr} : !smt.int
%c = smt.declare_fun {smt.some_attr} : !smt.int
// CHECK: smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">
%d = smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">
// CHECK: smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
%e = smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
// CHECK: smt.constant true {smt.some_attr}
%true = smt.constant true {smt.some_attr}
// CHECK: smt.constant false {smt.some_attr}
%false = smt.constant false {smt.some_attr}
// CHECK: smt.assert %a {smt.some_attr}
smt.assert %a {smt.some_attr}
// CHECK: smt.reset {smt.some_attr}
smt.reset {smt.some_attr}
// CHECK: smt.push 1 {smt.some_attr}
smt.push 1 {smt.some_attr}
// CHECK: smt.pop 1 {smt.some_attr}
smt.pop 1 {smt.some_attr}
// CHECK: %{{.*}} = smt.solver(%{{.*}}) {smt.some_attr} : (i8) -> (i8, i32) {
// CHECK: ^bb0(%{{.*}}: i8)
// CHECK: %{{.*}} = smt.check {smt.some_attr} sat {
// CHECK: smt.yield %{{.*}} : i32
// CHECK: } unknown {
// CHECK: smt.yield %{{.*}} : i32
// CHECK: } unsat {
// CHECK: smt.yield %{{.*}} : i32
// CHECK: } -> i32
// CHECK: smt.yield %{{.*}}, %{{.*}} : i8, i32
// CHECK: }
%0:2 = smt.solver(%in) {smt.some_attr} : (i8) -> (i8, i32) {
^bb0(%arg0: i8):
%1 = smt.check {smt.some_attr} sat {
%c1_i32 = arith.constant 1 : i32
smt.yield %c1_i32 : i32
} unknown {
%c0_i32 = arith.constant 0 : i32
smt.yield %c0_i32 : i32
} unsat {
%c-1_i32 = arith.constant -1 : i32
smt.yield %c-1_i32 : i32
} -> i32
smt.yield %arg0, %1 : i8, i32
}
// CHECK: smt.solver() : () -> () {
// CHECK-NEXT: }
smt.solver() : () -> () { }
// CHECK: smt.solver() : () -> () {
// CHECK-NEXT: smt.set_logic "AUFLIA"
// CHECK-NEXT: }
smt.solver() : () -> () {
smt.set_logic "AUFLIA"
}
// CHECK: smt.check sat {
// CHECK-NEXT: } unknown {
// CHECK-NEXT: } unsat {
// CHECK-NEXT: }
smt.check sat { } unknown { } unsat { }
// CHECK: %{{.*}} = smt.eq %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>
%1 = smt.eq %b, %b {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.distinct %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>
%2 = smt.distinct %b, %b {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.eq %{{.*}}, %{{.*}}, %{{.*}} : !smt.bool
%3 = smt.eq %a, %a, %a : !smt.bool
// CHECK: %{{.*}} = smt.distinct %{{.*}}, %{{.*}}, %{{.*}} : !smt.bool
%4 = smt.distinct %a, %a, %a : !smt.bool
// CHECK: %{{.*}} = smt.ite %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>
%5 = smt.ite %a, %b, %b {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.not %{{.*}} {smt.some_attr}
%6 = smt.not %a {smt.some_attr}
// CHECK: %{{.*}} = smt.and %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}
%7 = smt.and %a, %a, %a {smt.some_attr}
// CHECK: %{{.*}} = smt.or %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}
%8 = smt.or %a, %a, %a {smt.some_attr}
// CHECK: %{{.*}} = smt.xor %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}
%9 = smt.xor %a, %a, %a {smt.some_attr}
// CHECK: %{{.*}} = smt.implies %{{.*}}, %{{.*}} {smt.some_attr}
%10 = smt.implies %a, %a {smt.some_attr}
// CHECK: smt.apply_func %{{.*}}(%{{.*}}, %{{.*}}) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
%11 = smt.apply_func %e(%c, %a) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>
return
}
// CHECK-LABEL: func @quantifiers
func.func @quantifiers() {
// CHECK-NEXT: smt.forall ["a", "b"] weight 2 attributes {smt.some_attr} {
// CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
// CHECK-NEXT: smt.eq
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: } patterns {
// CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool, %{{.*}}: !smt.bool):
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }, {
// CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool):
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }
%0 = smt.forall ["a", "b"] weight 2 attributes {smt.some_attr} {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
%1 = smt.eq %arg2, %arg3 : !smt.bool
smt.yield %1 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
}, {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
}
// CHECK-NEXT: smt.forall ["a", "b"] no_pattern attributes {smt.some_attr} {
// CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
// CHECK-NEXT: smt.eq
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }
%1 = smt.forall ["a", "b"] no_pattern attributes {smt.some_attr} {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
%2 = smt.eq %arg2, %arg3 : !smt.bool
smt.yield %2 : !smt.bool
}
// CHECK-NEXT: smt.forall {
// CHECK-NEXT: smt.constant
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }
%2 = smt.forall {
%3 = smt.constant true
smt.yield %3 : !smt.bool
}
// CHECK-NEXT: smt.exists ["a", "b"] weight 2 attributes {smt.some_attr} {
// CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
// CHECK-NEXT: smt.eq
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: } patterns {
// CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool, %{{.*}}: !smt.bool):
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }, {
// CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool):
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }
%3 = smt.exists ["a", "b"] weight 2 attributes {smt.some_attr} {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
%4 = smt.eq %arg2, %arg3 : !smt.bool
smt.yield %4 : !smt.bool {smt.some_attr}
} patterns {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
}, {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
}
// CHECK-NEXT: smt.exists no_pattern attributes {smt.some_attr} {
// CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):
// CHECK-NEXT: smt.eq
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }
%4 = smt.exists no_pattern attributes {smt.some_attr} {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
%5 = smt.eq %arg2, %arg3 : !smt.bool
smt.yield %5 : !smt.bool {smt.some_attr}
}
// CHECK-NEXT: smt.exists [] {
// CHECK-NEXT: smt.constant
// CHECK-NEXT: smt.yield %{{.*}}
// CHECK-NEXT: }
%5 = smt.exists [] {
%6 = smt.constant true
smt.yield %6 : !smt.bool
}
return
}

112
test/Dialect/SMT/bitvector-errors.mlir
View File

@ -1,112 +0,0 @@
// RUN: circt-opt %s --split-input-file --verify-diagnostics
// expected-error @below {{bit-vector must have at least a width of one}}
func.func @at_least_size_one(%arg0: !smt.bv<0>) {
return
}
// -----
// expected-error @below {{bit-vector must have at least a width of one}}
func.func @positive_width(%arg0: !smt.bv<-1>) {
return
}
// -----
func.func @attr_type_and_return_type_match() {
// expected-error @below {{inferred type(s) '!smt.bv<1>' are incompatible with return type(s) of operation '!smt.bv<32>'}}
// expected-error @below {{failed to infer returned types}}
%c0_bv32 = "smt.bv.constant"() <{value = #smt.bv<0> : !smt.bv<1>}> : () -> !smt.bv<32>
return
}
// -----
func.func @invalid_bitvector_attr() {
// expected-error @below {{explicit bit-vector type required}}
smt.bv.constant #smt.bv<5>
}
// -----
func.func @invalid_bitvector_attr() {
// expected-error @below {{integer value out of range for given bit-vector type}}
smt.bv.constant #smt.bv<32> : !smt.bv<2>
}
// -----
func.func @invalid_bitvector_attr() {
// expected-error @below {{integer value out of range for given bit-vector type}}
smt.bv.constant #smt.bv<-4> : !smt.bv<2>
}
// -----
func.func @extraction(%arg0: !smt.bv<32>) {
// expected-error @below {{range to be extracted is too big, expected range starting at index 20 of length 16 requires input width of at least 36, but the input width is only 32}}
smt.bv.extract %arg0 from 20 : (!smt.bv<32>) -> !smt.bv<16>
return
}
// -----
func.func @concat(%arg0: !smt.bv<32>) {
// expected-error @below {{inferred type(s) '!smt.bv<64>' are incompatible with return type(s) of operation '!smt.bv<33>'}}
// expected-error @below {{failed to infer returned types}}
"smt.bv.concat"(%arg0, %arg0) {} : (!smt.bv<32>, !smt.bv<32>) -> !smt.bv<33>
return
}
// -----
func.func @repeat_result_type_no_multiple_of_input_type(%arg0: !smt.bv<32>) {
// expected-error @below {{result bit-vector width must be a multiple of the input bit-vector width}}
"smt.bv.repeat"(%arg0) : (!smt.bv<32>) -> !smt.bv<65>
return
}
// -----
func.func @repeat_negative_count(%arg0: !smt.bv<32>) {
// expected-error @below {{integer must be positive}}
smt.bv.repeat -2 times %arg0 : !smt.bv<32>
return
}
// -----
// The parser has to extract the bit-width of the input and thus we need to
// test that this is handled correctly in the parser, we cannot just rely on the
// verifier.
func.func @repeat_wrong_input_type(%arg0: !smt.bool) {
// expected-error @below {{input must have bit-vector type}}
smt.bv.repeat 2 times %arg0 : !smt.bool
return
}
// -----
func.func @repeat_count_too_large(%arg0: !smt.bv<32>) {
// expected-error @below {{integer must fit into 63 bits}}
smt.bv.repeat 18446744073709551617 times %arg0 : !smt.bv<32>
return
}
// -----
func.func @repeat_result_type_bitwidth_too_large(%arg0: !smt.bv<9223372036854775807>) {
// expected-error @below {{result bit-width (provided integer times bit-width of the input type) must fit into 63 bits}}
smt.bv.repeat 2 times %arg0 : !smt.bv<9223372036854775807>
return
}
// -----
func.func @invalid_bv2int_signedness() {
%c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32>
// expected-error @below {{expected ':'}}
%bv2int = smt.bv2int %c5_bv32 unsigned : !smt.bv<32>
return
}

81
test/Dialect/SMT/bitvectors.mlir
View File

@ -1,81 +0,0 @@
// RUN: circt-opt %s | circt-opt | FileCheck %s
// CHECK-LABEL: func @bitvectors
func.func @bitvectors() {
// CHECK: %c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr}
%c5_bv32 = smt.bv.constant #smt.bv<5> : !smt.bv<32> {smt.some_attr}
// CHECK: %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8> {smt.some_attr}
%c92_bv8 = smt.bv.constant #smt.bv<0x5c> : !smt.bv<8> {smt.some_attr}
// CHECK: %c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>
%c-1_bv8 = smt.bv.constant #smt.bv<-1> : !smt.bv<8>
// CHECK: %c-1_bv1{{(_[0-9]+)?}} = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
%c-1_bv1_neg = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
// CHECK: %c-1_bv1{{(_[0-9]+)?}} = smt.bv.constant #smt.bv<-1> : !smt.bv<1>
%c-1_bv1_pos = smt.bv.constant #smt.bv<1> : !smt.bv<1>
// CHECK: [[C0:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
%c = smt.bv.constant #smt.bv<0> : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.neg [[C0]] {smt.some_attr} : !smt.bv<32>
%0 = smt.bv.neg %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.add [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%1 = smt.bv.add %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.mul [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%3 = smt.bv.mul %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.urem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%4 = smt.bv.urem %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.srem [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%5 = smt.bv.srem %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.smod [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%7 = smt.bv.smod %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.shl [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%8 = smt.bv.shl %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.lshr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%9 = smt.bv.lshr %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.ashr [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%10 = smt.bv.ashr %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.udiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%11 = smt.bv.udiv %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.sdiv [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%12 = smt.bv.sdiv %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.not [[C0]] {smt.some_attr} : !smt.bv<32>
%13 = smt.bv.not %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.and [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%14 = smt.bv.and %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.or [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%15 = smt.bv.or %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.xor [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%16 = smt.bv.xor %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp slt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%17 = smt.bv.cmp slt %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp sle [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%18 = smt.bv.cmp sle %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp sgt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%19 = smt.bv.cmp sgt %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp sge [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%20 = smt.bv.cmp sge %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp ult [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%21 = smt.bv.cmp ult %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp ule [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%22 = smt.bv.cmp ule %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp ugt [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%23 = smt.bv.cmp ugt %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.cmp uge [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>
%24 = smt.bv.cmp uge %c, %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.concat [[C0]], [[C0]] {smt.some_attr} : !smt.bv<32>, !smt.bv<32>
%25 = smt.bv.concat %c, %c {smt.some_attr} : !smt.bv<32>, !smt.bv<32>
// CHECK: %{{.*}} = smt.bv.extract [[C0]] from 8 {smt.some_attr} : (!smt.bv<32>) -> !smt.bv<16>
%26 = smt.bv.extract %c from 8 {smt.some_attr} : (!smt.bv<32>) -> !smt.bv<16>
// CHECK: %{{.*}} = smt.bv.repeat 2 times [[C0]] {smt.some_attr} : !smt.bv<32>
%27 = smt.bv.repeat 2 times %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv2int [[C0]] {smt.some_attr} : !smt.bv<32>
%29 = smt.bv2int %c {smt.some_attr} : !smt.bv<32>
// CHECK: %{{.*}} = smt.bv2int [[C0]] signed {smt.some_attr} : !smt.bv<32>
%28 = smt.bv2int %c signed {smt.some_attr} : !smt.bv<32>
return
}

497
test/Dialect/SMT/core-errors.mlir
View File

@ -1,497 +0,0 @@
// RUN: circt-opt %s --split-input-file --verify-diagnostics
func.func @solver_isolated_from_above(%arg0: !smt.bool) {
// expected-note @below {{required by region isolation constraints}}
smt.solver() : () -> () {
// expected-error @below {{using value defined outside the region}}
smt.assert %arg0
}
return
}
// -----
func.func @no_smt_value_enters_solver(%arg0: !smt.bool) {
// expected-error @below {{operand #0 must be variadic of any non-smt type, but got '!smt.bool'}}
smt.solver(%arg0) : (!smt.bool) -> () {
^bb0(%arg1: !smt.bool):
smt.assert %arg1
}
return
}
// -----
func.func @no_smt_value_exits_solver() {
// expected-error @below {{result #0 must be variadic of any non-smt type, but got '!smt.bool'}}
%0 = smt.solver() : () -> !smt.bool {
%a = smt.declare_fun "a" : !smt.bool
smt.yield %a : !smt.bool
}
return
}
// -----
func.func @block_args_and_inputs_match() {
// expected-error @below {{block argument types must match the types of the 'inputs'}}
smt.solver() : () -> () {
^bb0(%arg0: i32):
}
return
}
// -----
func.func @solver_yield_operands_and_results_match() {
// expected-error @below {{types of yielded values must match return values}}
smt.solver() : () -> () {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
}
return
}
// -----
func.func @check_yield_operands_and_results_match() {
// expected-error @below {{types of yielded values in 'unsat' region must match return values}}
%0 = smt.check sat {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
} unknown {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
} unsat { } -> i32
return
}
// -----
func.func @check_yield_operands_and_results_match() {
// expected-error @below {{types of yielded values in 'unknown' region must match return values}}
%0 = smt.check sat {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
} unknown {
} unsat {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
} -> i32
return
}
// -----
func.func @check_yield_operands_and_results_match() {
// expected-error @below {{types of yielded values in 'sat' region must match return values}}
%0 = smt.check sat {
} unknown {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
} unsat {
%1 = hw.constant 0 : i32
smt.yield %1 : i32
} -> i32
return
}
// -----
func.func @check_no_block_arguments() {
// expected-error @below {{region #0 should have no arguments}}
smt.check sat {
^bb0(%arg0: i32):
} unknown {
} unsat {
}
return
}
// -----
func.func @check_no_block_arguments() {
// expected-error @below {{region #1 should have no arguments}}
smt.check sat {
} unknown {
^bb0(%arg0: i32):
} unsat {
}
return
}
// -----
func.func @check_no_block_arguments() {
// expected-error @below {{region #2 should have no arguments}}
smt.check sat {
} unknown {
} unsat {
^bb0(%arg0: i32):
}
return
}
// -----
func.func @too_few_operands() {
// expected-error @below {{'inputs' must have at least size 2, but got 0}}
smt.eq : !smt.bool
return
}
// -----
func.func @too_few_operands(%a: !smt.bool) {
// expected-error @below {{'inputs' must have at least size 2, but got 1}}
smt.distinct %a : !smt.bool
return
}
// -----
func.func @ite_type_mismatch(%a: !smt.bool, %b: !smt.bv<32>) {
// expected-error @below {{failed to verify that all of {thenValue, elseValue, result} have same type}}
"smt.ite"(%a, %a, %b) {} : (!smt.bool, !smt.bool, !smt.bv<32>) -> !smt.bool
return
}
// -----
func.func @forall_number_of_decl_names_must_match_num_args() {
// expected-error @below {{number of bound variable names must match number of block arguments}}
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%2 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %2 : !smt.bool
}
return
}
// -----
func.func @exists_number_of_decl_names_must_match_num_args() {
// expected-error @below {{number of bound variable names must match number of block arguments}}
%1 = smt.exists ["a"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%2 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %2 : !smt.bool
}
return
}
// -----
func.func @forall_yield_must_have_exactly_one_bool_value() {
// expected-error @below {{yielded value must be of '!smt.bool' type}}
%1 = smt.forall ["a", "b"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%2 = smt.int.add %arg2, %arg3
smt.yield %2 : !smt.int
}
return
}
// -----
func.func @forall_yield_must_have_exactly_one_bool_value() {
// expected-error @below {{must have exactly one yielded value}}
%1 = smt.forall ["a", "b"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
smt.yield
}
return
}
// -----
func.func @exists_yield_must_have_exactly_one_bool_value() {
// expected-error @below {{yielded value must be of '!smt.bool' type}}
%1 = smt.exists ["a", "b"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%2 = smt.int.add %arg2, %arg3
smt.yield %2 : !smt.int
}
return
}
// -----
func.func @exists_yield_must_have_exactly_one_bool_value() {
// expected-error @below {{must have exactly one yielded value}}
%1 = smt.exists ["a", "b"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
smt.yield
}
return
}
// -----
func.func @exists_patterns_region_and_no_patterns_attr_are_mutually_exclusive() {
// expected-error @below {{patterns and the no_pattern attribute must not be specified at the same time}}
%1 = smt.exists ["a"] no_pattern {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
}
return
}
// -----
func.func @forall_patterns_region_and_no_patterns_attr_are_mutually_exclusive() {
// expected-error @below {{patterns and the no_pattern attribute must not be specified at the same time}}
%1 = smt.forall ["a"] no_pattern {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
}
return
}
// -----
func.func @exists_patterns_region_num_args() {
// expected-error @below {{block argument number and types of the 'body' and 'patterns' region #0 must match}}
%1 = smt.exists ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
}
return
}
// -----
func.func @forall_patterns_region_num_args() {
// expected-error @below {{block argument number and types of the 'body' and 'patterns' region #0 must match}}
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool, %arg3: !smt.bool):
smt.yield %arg2, %arg3 : !smt.bool, !smt.bool
}
return
}
// -----
func.func @exists_patterns_region_at_least_one_yielded_value() {
// expected-error @below {{'patterns' region #0 must have at least one yielded value}}
%1 = smt.exists ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
smt.yield
}
return
}
// -----
func.func @forall_patterns_region_at_least_one_yielded_value() {
// expected-error @below {{'patterns' region #0 must have at least one yielded value}}
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
smt.yield
}
return
}
// -----
func.func @exists_all_pattern_regions_tested() {
// expected-error @below {{'patterns' region #1 must have at least one yielded value}}
%1 = smt.exists ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
}, {
^bb0(%arg2: !smt.bool):
smt.yield
}
return
}
// -----
func.func @forall_all_pattern_regions_tested() {
// expected-error @below {{'patterns' region #1 must have at least one yielded value}}
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
}, {
^bb0(%arg2: !smt.bool):
smt.yield
}
return
}
// -----
func.func @exists_patterns_region_no_non_smt_operations() {
// expected-error @below {{'patterns' region #0 may only contain SMT dialect operations}}
%1 = smt.exists ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
// expected-note @below {{first non-SMT operation here}}
hw.constant 0 : i32
smt.yield %arg2 : !smt.bool
}
return
}
// -----
func.func @forall_patterns_region_no_non_smt_operations() {
// expected-error @below {{'patterns' region #0 may only contain SMT dialect operations}}
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
// expected-note @below {{first non-SMT operation here}}
hw.constant 0 : i32
smt.yield %arg2 : !smt.bool
}
return
}
// -----
func.func @exists_patterns_region_no_var_binding_operations() {
// expected-error @below {{'patterns' region #0 must not contain any variable binding operations}}
%1 = smt.exists ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
// expected-note @below {{first violating operation here}}
smt.exists ["b"] {
^bb0(%arg3: !smt.bool):
smt.yield %arg3 : !smt.bool
}
smt.yield %arg2 : !smt.bool
}
return
}
// -----
func.func @forall_patterns_region_no_var_binding_operations() {
// expected-error @below {{'patterns' region #0 must not contain any variable binding operations}}
%1 = smt.forall ["a"] {
^bb0(%arg2: !smt.bool):
smt.yield %arg2 : !smt.bool
} patterns {
^bb0(%arg2: !smt.bool):
// expected-note @below {{first violating operation here}}
smt.forall ["b"] {
^bb0(%arg3: !smt.bool):
smt.yield %arg3 : !smt.bool
}
smt.yield %arg2 : !smt.bool
}
return
}
// -----
func.func @exists_bound_variable_type_invalid() {
// expected-error @below {{bound variables must by any non-function SMT value}}
%1 = smt.exists ["a", "b"] {
^bb0(%arg2: !smt.func<(!smt.int) !smt.int>, %arg3: !smt.bool):
smt.yield %arg3 : !smt.bool
}
return
}
// -----
func.func @forall_bound_variable_type_invalid() {
// expected-error @below {{bound variables must by any non-function SMT value}}
%1 = smt.forall ["a", "b"] {
^bb0(%arg2: !smt.func<(!smt.int) !smt.int>, %arg3: !smt.bool):
smt.yield %arg3 : !smt.bool
}
return
}
// -----
// expected-error @below {{domain types must be any non-function SMT type}}
func.func @func_domain_no_smt_type(%arg0: !smt.func<(i32) !smt.bool>) {
return
}
// -----
// expected-error @below {{range type must be any non-function SMT type}}
func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) i32>) {
return
}
// -----
// expected-error @below {{range type must be any non-function SMT type}}
func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) !smt.func<(!smt.bool) !smt.bool>>) {
return
}
// -----
func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) !smt.bool>) {
// expected-error @below {{got 0 operands and 1 types}}
smt.apply_func %arg0() : !smt.func<(!smt.bool) !smt.bool>
return
}
// -----
// expected-error @below {{sort parameter types must be any non-function SMT type}}
func.func @sort_type_no_smt_type(%arg0: !smt.sort<"sortname"[i32]>) {
return
}
// -----
func.func @negative_push() {
// expected-error @below {{smt.push' op attribute 'count' failed to satisfy constraint: 32-bit signless integer attribute whose value is non-negative}}
smt.push -1
return
}
// -----
func.func @negative_pop() {
// expected-error @below {{smt.pop' op attribute 'count' failed to satisfy constraint: 32-bit signless integer attribute whose value is non-negative}}
smt.pop -1
return
}
// -----
func.func @set_logic_outside_solver() {
// expected-error @below {{'smt.set_logic' op expects parent op 'smt.solver'}}
smt.set_logic "AUFLIA"
return
}

12
test/Dialect/SMT/cse-test.mlir
View File

@ -1,12 +0,0 @@
// RUN: circt-opt %s --cse | FileCheck %s
func.func @declare_const_cse(%in: i8) -> (!smt.bool, !smt.bool){
// CHECK: smt.declare_fun "a" : !smt.bool
%a = smt.declare_fun "a" : !smt.bool
// CHECK-NEXT: smt.declare_fun "a" : !smt.bool
%b = smt.declare_fun "a" : !smt.bool
// CHECK-NEXT: return
%c = smt.declare_fun "a" : !smt.bool
return %a, %b : !smt.bool, !smt.bool
}

36
test/Dialect/SMT/integers.mlir
View File

@ -1,36 +0,0 @@
// RUN: circt-opt %s | circt-opt | FileCheck %s
// CHECK-LABEL: func @integer_operations
func.func @integer_operations() {
// CHECK-NEXT: [[V0:%.+]] = smt.int.constant -123 {smt.some_attr}
%0 = smt.int.constant -123 {smt.some_attr}
// CHECK-NEXT: %c184467440737095516152 = smt.int.constant 184467440737095516152 {smt.some_attr}
%1 = smt.int.constant 184467440737095516152 {smt.some_attr}
// CHECK-NEXT: smt.int.add [[V0]], [[V0]], [[V0]] {smt.some_attr}
%2 = smt.int.add %0, %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.mul [[V0]], [[V0]], [[V0]] {smt.some_attr}
%3 = smt.int.mul %0, %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.sub [[V0]], [[V0]] {smt.some_attr}
%4 = smt.int.sub %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.div [[V0]], [[V0]] {smt.some_attr}
%5 = smt.int.div %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.mod [[V0]], [[V0]] {smt.some_attr}
%6 = smt.int.mod %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.abs [[V0]] {smt.some_attr}
%7 = smt.int.abs %0 {smt.some_attr}
// CHECK-NEXT: smt.int.cmp le [[V0]], [[V0]] {smt.some_attr}
%9 = smt.int.cmp le %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.cmp lt [[V0]], [[V0]] {smt.some_attr}
%10 = smt.int.cmp lt %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.cmp ge [[V0]], [[V0]] {smt.some_attr}
%11 = smt.int.cmp ge %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int.cmp gt [[V0]], [[V0]] {smt.some_attr}
%12 = smt.int.cmp gt %0, %0 {smt.some_attr}
// CHECK-NEXT: smt.int2bv [[V0]] {smt.some_attr} : !smt.bv<4>
%13 = smt.int2bv %0 {smt.some_attr} : !smt.bv<4>
return
}

21
test/Target/ExportSMTLIB/array.mlir
View File

@ -1,21 +0,0 @@
// RUN: circt-translate --export-smtlib %s | FileCheck %s
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
smt.solver () : () -> () {
%c = smt.int.constant 0
%true = smt.constant true
// CHECK: (assert (let (([[V0:.+]] ((as const (Array Int Bool)) true)))
// CHECK: (let (([[V1:.+]] (store [[V0]] 0 true)))
// CHECK: (let (([[V2:.+]] (select [[V1]] 0)))
// CHECK: [[V2]]))))
// CHECK-INLINED: (assert (select (store ((as const (Array Int Bool)) true) 0 true) 0))
%0 = smt.array.broadcast %true : !smt.array<[!smt.int -> !smt.bool]>
%1 = smt.array.store %0[%c], %true : !smt.array<[!smt.int -> !smt.bool]>
%2 = smt.array.select %1[%c] : !smt.array<[!smt.int -> !smt.bool]>
smt.assert %2
// CHECK: (reset)
// CHECK-INLINED: (reset)
}

177
test/Target/ExportSMTLIB/attributes.mlir
View File

@ -1,177 +0,0 @@
// RUN: circt-translate --export-smtlib %s | FileCheck %s
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
smt.solver () : () -> () {
%true = smt.constant true
// CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK: ( ! (let (([[V11:.+]] (= [[A]] [[B]])))
// CHECK: [[V11]]) :weight 2))))
// CHECK: [[V10]]))
// CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (= [[A]] [[B]]) :weight 2)))
%1 = smt.forall ["a", "b"] weight 2 {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%2 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %2 : !smt.bool
}
smt.assert %1
// CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))
// CHECK: ( ! (let (([[V15:.+]] (= [[V13]] [[V14]])))
// CHECK: [[V15]]) :weight 2))))
// CHECK: [[V12]]))
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (= [[A]] [[B]]) :weight 2)))
%2 = smt.exists weight 2 {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%3 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %3 : !smt.bool
}
smt.assert %2
// CHECK: (assert (let (([[V16:.+]] (exists (([[V17:.+]] Int) ([[V18:.+]] Int))
// CHECK: ( ! (let (([[V19:.+]] (= [[V17]] [[V18]])))
// CHECK: (let (([[V20:.+]] (=> [[V19:.+]] true)))
// CHECK: [[V20:.+]])) :weight 2))))
// CHECK: [[V16]])){{$}}
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true) :weight 2)))
%3 = smt.exists weight 2 {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
%5 = smt.implies %4, %true
smt.yield %5 : !smt.bool
}
smt.assert %3
// CHECK: (assert (let (([[V21:.+]] (exists (([[V22:.+]] Int) ([[V23:.+]] Int))
// CHECK: ( ! (let (([[V24:.+]] (= [[V22]] [[V23]])))
// CHECK: (let (([[V25:.+]] (=> [[V24]] true)))
// CHECK: [[V25]]))
// CHECK: :pattern ((let (([[V26:.+]] (= [[V22]] [[V23]])))
// CHECK: [[V26]]))))))
// CHECK: [[V21]])){{$}}
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true)
// CHECK-INLINED: :pattern ((= [[A]] [[B]])))))
%6 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
%5 = smt.implies %4, %true
smt.yield %5 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %4: !smt.bool
}
smt.assert %6
// CHECK: (assert (let (([[V27:.+]] (exists (([[V28:.+]] Int) ([[V29:.+]] Int))
// CHECK: ( ! (let (([[V30:.+]] (= [[V28]] [[V29]])))
// CHECK: (let (([[V31:.+]] (=> [[V30]] true)))
// CHECK: [[V31]])) :weight 2
// CHECK: :pattern ((let (([[V32:.+]] (= [[V28]] [[V29]])))
// CHECK: [[V32]]))))))
// CHECK: [[V27]])){{$}}
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true) :weight 2
// CHECK-INLINED: :pattern ((= [[A]] [[B]])))))
%7 = smt.exists weight 2 {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
%5 = smt.implies %4, %true
smt.yield %5 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %4: !smt.bool
}
smt.assert %7
// CHECK: (assert (let (([[V33:.+]] (exists (([[V34:.+]] Int) ([[V35:.+]] Int))
// CHECK: ( ! (let (([[V36:.+]] (= [[V35]] 4)))
// CHECK: (let (([[V37:.+]] (= [[V34]] 3)))
// CHECK: (let (([[V38:.+]] (= [[V37]] [[V36]])))
// CHECK: [[V38]])))
// CHECK: :pattern ((let (([[V39:.+]] (= [[V34]] 3)))
// CHECK: [[V39]]) (let (([[V40:.+]] (= [[V35]] 4)))
// CHECK: [[V40]]))))))
// CHECK: [[V33]])){{$}}
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (= (= [[A]] 3) (= [[B]] 4))
// CHECK-INLINED: :pattern ((= [[A]] 3) (= [[B]] 4)))))
%three = smt.int.constant 3
%four = smt.int.constant 4
%8 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
%5 = smt.eq %arg3, %four: !smt.int
%9 = smt.eq %4, %5: !smt.bool
smt.yield %9 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
smt.yield %4: !smt.bool
}, {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%5 = smt.eq %arg3, %four: !smt.int
smt.yield %5: !smt.bool
}
smt.assert %8
smt.check sat {} unknown {} unsat {}
// CHECK: (assert (let (([[V41:.+]] (exists (([[V42:.+]] Int) ([[V43:.+]] Int))
// CHECK: ( ! (let (([[V44:.+]] (= [[V43]] 4)))
// CHECK: (let (([[V45:.+]] (= [[V42]] 3)))
// CHECK: (let (([[V46:.+]] (= [[V45]] [[V44]])))
// CHECK: [[V46]])))
// CHECK: :pattern ((let (([[V47:.+]] (= [[V42]] 3)))
// CHECK: [[V47]])(let (([[V48:.+]] (= [[V43]] 4)))
// CHECK: [[V48]]))))))
// CHECK: [[V41]])){{$}}
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: ( ! (= (= [[A]] 3) (= [[B]] 4))
// CHECK-INLINED: :pattern ((= [[A]] 3)(= [[B]] 4)))))
%10 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
%5 = smt.eq %arg3, %four: !smt.int
%9 = smt.eq %4, %5: !smt.bool
smt.yield %9 : !smt.bool
} patterns {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%4 = smt.eq %arg2, %three: !smt.int
%5 = smt.eq %arg3, %four: !smt.int
smt.yield %4, %5: !smt.bool, !smt.bool
}
smt.assert %10
smt.check sat {} unknown {} unsat {}
// CHECK: (reset)
// CHECK-INLINED: (reset)
}

7
test/Target/ExportSMTLIB/bitvector-errors.mlir
View File

@ -1,7 +0,0 @@
// RUN: circt-translate --export-smtlib %s --split-input-file --verify-diagnostics
smt.solver () : () -> () {
%0 = smt.bv.constant #smt.bv<5> : !smt.bv<16>
// expected-error @below {{operation not supported for SMTLIB emission}}
%1 = smt.bv2int %0 signed : !smt.bv<16>
}

213
test/Target/ExportSMTLIB/bitvector.mlir
View File

@ -1,213 +0,0 @@
// RUN: circt-translate --export-smtlib %s | FileCheck %s
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
smt.solver () : () -> () {
%c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>
// CHECK: (assert (let (([[V0:.+]] (bvneg #x00000000)))
// CHECK: (let (([[V1:.+]] (= [[V0]] #x00000000)))
// CHECK: [[V1]])))
// CHECK-INLINED: (assert (= (bvneg #x00000000) #x00000000))
%0 = smt.bv.neg %c0_bv32 : !smt.bv<32>
%a0 = smt.eq %0, %c0_bv32 : !smt.bv<32>
smt.assert %a0
// CHECK: (assert (let (([[V2:.+]] (bvadd #x00000000 #x00000000)))
// CHECK: (let (([[V3:.+]] (= [[V2]] #x00000000)))
// CHECK: [[V3]])))
// CHECK-INLINED: (assert (= (bvadd #x00000000 #x00000000) #x00000000))
%1 = smt.bv.add %c0_bv32, %c0_bv32 : !smt.bv<32>
%a1 = smt.eq %1, %c0_bv32 : !smt.bv<32>
smt.assert %a1
// CHECK: (assert (let (([[V4:.+]] (bvmul #x00000000 #x00000000)))
// CHECK: (let (([[V5:.+]] (= [[V4]] #x00000000)))
// CHECK: [[V5]])))
// CHECK-INLINED: (assert (= (bvmul #x00000000 #x00000000) #x00000000))
%3 = smt.bv.mul %c0_bv32, %c0_bv32 : !smt.bv<32>
%a3 = smt.eq %3, %c0_bv32 : !smt.bv<32>
smt.assert %a3
// CHECK: (assert (let (([[V6:.+]] (bvurem #x00000000 #x00000000)))
// CHECK: (let (([[V7:.+]] (= [[V6]] #x00000000)))
// CHECK: [[V7]])))
// CHECK-INLINED: (assert (= (bvurem #x00000000 #x00000000) #x00000000))
%4 = smt.bv.urem %c0_bv32, %c0_bv32 : !smt.bv<32>
%a4 = smt.eq %4, %c0_bv32 : !smt.bv<32>
smt.assert %a4
// CHECK: (assert (let (([[V8:.+]] (bvsrem #x00000000 #x00000000)))
// CHECK: (let (([[V9:.+]] (= [[V8]] #x00000000)))
// CHECK: [[V9]])))
// CHECK-INLINED: (assert (= (bvsrem #x00000000 #x00000000) #x00000000))
%5 = smt.bv.srem %c0_bv32, %c0_bv32 : !smt.bv<32>
%a5 = smt.eq %5, %c0_bv32 : !smt.bv<32>
smt.assert %a5
// CHECK: (assert (let (([[V10:.+]] (bvsmod #x00000000 #x00000000)))
// CHECK: (let (([[V11:.+]] (= [[V10]] #x00000000)))
// CHECK: [[V11]])))
// CHECK-INLINED: (assert (= (bvsmod #x00000000 #x00000000) #x00000000))
%7 = smt.bv.smod %c0_bv32, %c0_bv32 : !smt.bv<32>
%a7 = smt.eq %7, %c0_bv32 : !smt.bv<32>
smt.assert %a7
// CHECK: (assert (let (([[V12:.+]] (bvshl #x00000000 #x00000000)))
// CHECK: (let (([[V13:.+]] (= [[V12]] #x00000000)))
// CHECK: [[V13]])))
// CHECK-INLINED: (assert (= (bvshl #x00000000 #x00000000) #x00000000))
%8 = smt.bv.shl %c0_bv32, %c0_bv32 : !smt.bv<32>
%a8 = smt.eq %8, %c0_bv32 : !smt.bv<32>
smt.assert %a8
// CHECK: (assert (let (([[V14:.+]] (bvlshr #x00000000 #x00000000)))
// CHECK: (let (([[V15:.+]] (= [[V14]] #x00000000)))
// CHECK: [[V15]])))
// CHECK-INLINED: (assert (= (bvlshr #x00000000 #x00000000) #x00000000))
%9 = smt.bv.lshr %c0_bv32, %c0_bv32 : !smt.bv<32>
%a9 = smt.eq %9, %c0_bv32 : !smt.bv<32>
smt.assert %a9
// CHECK: (assert (let (([[V16:.+]] (bvashr #x00000000 #x00000000)))
// CHECK: (let (([[V17:.+]] (= [[V16]] #x00000000)))
// CHECK: [[V17]])))
// CHECK-INLINED: (assert (= (bvashr #x00000000 #x00000000) #x00000000))
%10 = smt.bv.ashr %c0_bv32, %c0_bv32 : !smt.bv<32>
%a10 = smt.eq %10, %c0_bv32 : !smt.bv<32>
smt.assert %a10
// CHECK: (assert (let (([[V18:.+]] (bvudiv #x00000000 #x00000000)))
// CHECK: (let (([[V19:.+]] (= [[V18]] #x00000000)))
// CHECK: [[V19]])))
// CHECK-INLINED: (assert (= (bvudiv #x00000000 #x00000000) #x00000000))
%11 = smt.bv.udiv %c0_bv32, %c0_bv32 : !smt.bv<32>
%a11 = smt.eq %11, %c0_bv32 : !smt.bv<32>
smt.assert %a11
// CHECK: (assert (let (([[V20:.+]] (bvsdiv #x00000000 #x00000000)))
// CHECK: (let (([[V21:.+]] (= [[V20]] #x00000000)))
// CHECK: [[V21]])))
// CHECK-INLINED: (assert (= (bvsdiv #x00000000 #x00000000) #x00000000))
%12 = smt.bv.sdiv %c0_bv32, %c0_bv32 : !smt.bv<32>
%a12 = smt.eq %12, %c0_bv32 : !smt.bv<32>
smt.assert %a12
// CHECK: (assert (let (([[V22:.+]] (bvnot #x00000000)))
// CHECK: (let (([[V23:.+]] (= [[V22]] #x00000000)))
// CHECK: [[V23]])))
// CHECK-INLINED: (assert (= (bvnot #x00000000) #x00000000))
%13 = smt.bv.not %c0_bv32 : !smt.bv<32>
%a13 = smt.eq %13, %c0_bv32 : !smt.bv<32>
smt.assert %a13
// CHECK: (assert (let (([[V24:.+]] (bvand #x00000000 #x00000000)))
// CHECK: (let (([[V25:.+]] (= [[V24]] #x00000000)))
// CHECK: [[V25]])))
// CHECK-INLINED: (assert (= (bvand #x00000000 #x00000000) #x00000000))
%14 = smt.bv.and %c0_bv32, %c0_bv32 : !smt.bv<32>
%a14 = smt.eq %14, %c0_bv32 : !smt.bv<32>
smt.assert %a14
// CHECK: (assert (let (([[V26:.+]] (bvor #x00000000 #x00000000)))
// CHECK: (let (([[V27:.+]] (= [[V26]] #x00000000)))
// CHECK: [[V27]])))
// CHECK-INLINED: (assert (= (bvor #x00000000 #x00000000) #x00000000))
%15 = smt.bv.or %c0_bv32, %c0_bv32 : !smt.bv<32>
%a15 = smt.eq %15, %c0_bv32 : !smt.bv<32>
smt.assert %a15
// CHECK: (assert (let (([[V28:.+]] (bvxor #x00000000 #x00000000)))
// CHECK: (let (([[V29:.+]] (= [[V28]] #x00000000)))
// CHECK: [[V29]])))
// CHECK-INLINED: (assert (= (bvxor #x00000000 #x00000000) #x00000000))
%16 = smt.bv.xor %c0_bv32, %c0_bv32 : !smt.bv<32>
%a16 = smt.eq %16, %c0_bv32 : !smt.bv<32>
smt.assert %a16
// CHECK: (assert (let (([[V30:.+]] (bvslt #x00000000 #x00000000)))
// CHECK: [[V30]]))
// CHECK-INLINED: (assert (bvslt #x00000000 #x00000000))
%27 = smt.bv.cmp slt %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %27
// CHECK: (assert (let (([[V31:.+]] (bvsle #x00000000 #x00000000)))
// CHECK: [[V31]]))
// CHECK-INLINED: (assert (bvsle #x00000000 #x00000000))
%28 = smt.bv.cmp sle %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %28
// CHECK: (assert (let (([[V32:.+]] (bvsgt #x00000000 #x00000000)))
// CHECK: [[V32]]))
// CHECK-INLINED: (assert (bvsgt #x00000000 #x00000000))
%29 = smt.bv.cmp sgt %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %29
// CHECK: (assert (let (([[V33:.+]] (bvsge #x00000000 #x00000000)))
// CHECK: [[V33]]))
// CHECK-INLINED: (assert (bvsge #x00000000 #x00000000))
%30 = smt.bv.cmp sge %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %30
// CHECK: (assert (let (([[V34:.+]] (bvult #x00000000 #x00000000)))
// CHECK: [[V34]]))
// CHECK-INLINED: (assert (bvult #x00000000 #x00000000))
%31 = smt.bv.cmp ult %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %31
// CHECK: (assert (let (([[V35:.+]] (bvule #x00000000 #x00000000)))
// CHECK: [[V35]]))
// CHECK-INLINED: (assert (bvule #x00000000 #x00000000))
%32 = smt.bv.cmp ule %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %32
// CHECK: (assert (let (([[V36:.+]] (bvugt #x00000000 #x00000000)))
// CHECK: [[V36]]))
// CHECK-INLINED: (assert (bvugt #x00000000 #x00000000))
%33 = smt.bv.cmp ugt %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %33
// CHECK: (assert (let (([[V37:.+]] (bvuge #x00000000 #x00000000)))
// CHECK: [[V37]]))
// CHECK-INLINED: (assert (bvuge #x00000000 #x00000000))
%34 = smt.bv.cmp uge %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %34
// CHECK: (assert (let (([[V38:.+]] (concat #x00000000 #x00000000)))
// CHECK: (let (([[V39:.+]] ((_ extract 23 8) [[V38]])))
// CHECK: (let (([[V40:.+]] ((_ repeat 2) [[V39]])))
// CHECK: (let (([[V41:.+]] (= [[V40]] #x00000000)))
// CHECK: [[V41]])))))
// CHECK-INLINED: (assert (= ((_ repeat 2) ((_ extract 23 8) (concat #x00000000 #x00000000))) #x00000000))
%35 = smt.bv.concat %c0_bv32, %c0_bv32 : !smt.bv<32>, !smt.bv<32>
%36 = smt.bv.extract %35 from 8 : (!smt.bv<64>) -> !smt.bv<16>
%37 = smt.bv.repeat 2 times %36 : !smt.bv<16>
%a37 = smt.eq %37, %c0_bv32 : !smt.bv<32>
smt.assert %a37
// CHECK: (reset)
// CHECK-INLINED: (reset)
}

83
test/Target/ExportSMTLIB/core-errors.mlir
View File

@ -1,83 +0,0 @@
// RUN: circt-translate --export-smtlib %s --split-input-file --verify-diagnostics
smt.solver () : () -> () {
%0 = smt.constant true
// expected-error @below {{must not have any result values}}
%1 = smt.check sat {
smt.yield %0 : !smt.bool
} unknown {
smt.yield %0 : !smt.bool
} unsat {
smt.yield %0 : !smt.bool
} -> !smt.bool
}
// -----
smt.solver () : () -> () {
// expected-error @below {{'sat' region must be empty}}
smt.check sat {
%0 = smt.constant true
smt.yield
} unknown {
} unsat {
}
}
// -----
smt.solver () : () -> () {
// expected-error @below {{'unknown' region must be empty}}
smt.check sat {
} unknown {
%0 = smt.constant true
smt.yield
} unsat {
}
}
// -----
smt.solver () : () -> () {
// expected-error @below {{'unsat' region must be empty}}
smt.check sat {
} unknown {
} unsat {
%0 = smt.constant true
smt.yield
}
}
// -----
// expected-error @below {{solver scopes with inputs or results are not supported}}
%0 = smt.solver () : () -> (i1) {
%1 = hw.constant true
smt.yield %1 : i1
}
// -----
smt.solver () : () -> () {
// expected-error @below {{solver must not contain any non-SMT operations}}
%1 = hw.constant true
}
// -----
func.func @solver_input(%arg0: i1) {
// expected-error @below {{solver scopes with inputs or results are not supported}}
smt.solver (%arg0) : (i1) -> () {
^bb0(%arg1: i1):
smt.yield
}
return
}
// -----
smt.solver () : () -> () {
%0 = smt.declare_fun : !smt.sort<"uninterpreted0">
// expected-error @below {{uninterpreted sorts with same identifier but different arity found}}
%1 = smt.declare_fun : !smt.sort<"uninterpreted0"[!smt.bool]>
}

137
test/Target/ExportSMTLIB/core.mlir
View File

@ -1,137 +0,0 @@
// RUN: circt-translate --export-smtlib %s | FileCheck %s
// RUN: circt-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED
smt.solver () : () -> () {
%c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>
%true = smt.constant true
%false = smt.constant false
// CHECK: (declare-const b (_ BitVec 32))
// CHECK: (assert (let (([[V0:.+]] (= #x00000000 b)))
// CHECK: [[V0]]))
// CHECK-INLINED: (declare-const b (_ BitVec 32))
// CHECK-INLINED: (assert (= #x00000000 b))
%21 = smt.declare_fun "b" : !smt.bv<32>
%23 = smt.eq %c0_bv32, %21 : !smt.bv<32>
smt.assert %23
// CHECK: (assert (let (([[V1:.+]] (distinct #x00000000 #x00000000)))
// CHECK: [[V1]]))
// CHECK-INLINED: (assert (distinct #x00000000 #x00000000))
%24 = smt.distinct %c0_bv32, %c0_bv32 : !smt.bv<32>
smt.assert %24
// CHECK: (declare-const a Bool)
// CHECK: (assert (let (([[V2:.+]] (ite a #x00000000 b)))
// CHECK: (let (([[V3:.+]] (= #x00000000 [[V2]])))
// CHECK: [[V3]])))
// CHECK-INLINED: (declare-const a Bool)
// CHECK-INLINED: (assert (= #x00000000 (ite a #x00000000 b)))
%20 = smt.declare_fun "a" : !smt.bool
%38 = smt.ite %20, %c0_bv32, %21 : !smt.bv<32>
%4 = smt.eq %c0_bv32, %38 : !smt.bv<32>
smt.assert %4
// CHECK: (assert (let (([[V4:.+]] (not true)))
// CHECK: (let (([[V5:.+]] (and [[V4]] true false)))
// CHECK: (let (([[V6:.+]] (or [[V5]] [[V4]] true)))
// CHECK: (let (([[V7:.+]] (xor [[V4]] [[V6]])))
// CHECK: (let (([[V8:.+]] (=> [[V7]] false)))
// CHECK: [[V8]]))))))
// CHECK-INLINED: (assert (let (([[V15:.+]] (not true)))
// CHECK-INLINED: (=> (xor [[V15]] (or (and [[V15]] true false) [[V15]] true)) false)))
%39 = smt.not %true
%40 = smt.and %39, %true, %false
%41 = smt.or %40, %39, %true
%42 = smt.xor %39, %41
%43 = smt.implies %42, %false
smt.assert %43
// CHECK: (declare-fun func1 (Bool Bool) Bool)
// CHECK: (assert (let (([[V9:.+]] (func1 true false)))
// CHECK: [[V9]]))
// CHECK-INLINED: (declare-fun func1 (Bool Bool) Bool)
// CHECK-INLINED: (assert (func1 true false))
%44 = smt.declare_fun "func1" : !smt.func<(!smt.bool, !smt.bool) !smt.bool>
%45 = smt.apply_func %44(%true, %false) : !smt.func<(!smt.bool, !smt.bool) !smt.bool>
smt.assert %45
// CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK: (let (([[V11:.+]] (= [[A]] [[B]])))
// CHECK: [[V11]]))))
// CHECK: [[V10]]))
// CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: (= [[A]] [[B]])))
%1 = smt.forall ["a", "b"] {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%2 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %2 : !smt.bool
}
smt.assert %1
// CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))
// CHECK: (let (([[V15:.+]] (= [[V13]] [[V14]])))
// CHECK: [[V15]]))))
// CHECK: [[V12]]))
// CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))
// CHECK-INLINED: (= [[A]] [[B]])))
%2 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%3 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %3 : !smt.bool
}
smt.assert %2
// Test: make sure that open parens from outside quantifier bodies are not
// propagated into the body.
// CHECK: (assert (let (([[V15:.+]] (exists (([[V16:.+]] Int) ([[V17:.+]] Int)){{$}}
// CHECK: (let (([[V18:.+]] (= [[V16]] [[V17]]))){{$}}
// CHECK: [[V18]])))){{$}}
// CHECK: (let (([[V19:.+]] (exists (([[V20:.+]] Int) ([[V21:.+]] Int)){{$}}
// CHECK: (let (([[V22:.+]] (= [[V20]] [[V21]]))){{$}}
// CHECK: [[V22]])))){{$}}
// CHECK: (let (([[V23:.+]] (and [[V19]] [[V15]]))){{$}}
// CHECK: [[V23]])))){{$}}
%3 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%5 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %5 : !smt.bool
}
%5 = smt.exists {
^bb0(%arg2: !smt.int, %arg3: !smt.int):
%6 = smt.eq %arg2, %arg3 : !smt.int
smt.yield %6 : !smt.bool
}
%6 = smt.and %3, %5
smt.assert %6
// CHECK: (check-sat)
// CHECK-INLINED: (check-sat)
smt.check sat {} unknown {} unsat {}
// CHECK: (reset)
// CHECK-INLINED: (reset)
smt.reset
// CHECK: (push 1)
// CHECK-INLINED: (push 1)
smt.push 1
// CHECK: (pop 1)
// CHECK-INLINED: (pop 1)
smt.pop 1
// CHECK: (set-logic AUFLIA)
// CHECK-INLINED: (set-logic AUFLIA)
smt.set_logic "AUFLIA"
// CHECK: (reset)
// CHECK-INLINED: (reset)
}

7
test/Target/ExportSMTLIB/integer-errors.mlir
View File

@ -1,7 +0,0 @@
// RUN: circt-translate --export-smtlib %s --split-input-file --verify-diagnostics
smt.solver () : () -> () {
%0 = smt.int.constant 5
// expected-error @below {{operation not supported for SMTLIB emission}}
%1 = smt.int2bv %0 : !smt.bv<4>
}

82
test/Target/ExportSMTLIB/integer.mlir
View File

@ -1,82 +0,0 @@
// RUN: circt-translate --export-smtlib %s | FileCheck %s
smt.solver () : () -> () {
%0 = smt.int.constant 5
%1 = smt.int.constant 10
// CHECK: (assert (let (([[V0:.+]] (+ 5 5 5)))
// CHECK: (let (([[V1:.+]] (= [[V0]] 10)))
// CHECK: [[V1]])))
// CHECK-INLINED: (assert (= (+ 5 5 5) 10))
%2 = smt.int.add %0, %0, %0
%a2 = smt.eq %2, %1 : !smt.int
smt.assert %a2
// CHECK: (assert (let (([[V2:.+]] (* 5 5 5)))
// CHECK: (let (([[V3:.+]] (= [[V2]] 10)))
// CHECK: [[V3]])))
// CHECK-INLINED: (assert (= (* 5 5 5) 10))
%3 = smt.int.mul %0, %0, %0
%a3 = smt.eq %3, %1 : !smt.int
smt.assert %a3
// CHECK: (assert (let (([[V4:.+]] (- 5 5)))
// CHECK: (let (([[V5:.+]] (= [[V4]] 10)))
// CHECK: [[V5]])))
// CHECK-INLINED: (assert (= (- 5 5) 10))
%4 = smt.int.sub %0, %0
%a4 = smt.eq %4, %1 : !smt.int
smt.assert %a4
// CHECK: (assert (let (([[V6:.+]] (div 5 5)))
// CHECK: (let (([[V7:.+]] (= [[V6]] 10)))
// CHECK: [[V7]])))
// CHECK-INLINED: (assert (= (div 5 5) 10))
%5 = smt.int.div %0, %0
%a5 = smt.eq %5, %1 : !smt.int
smt.assert %a5
// CHECK: (assert (let (([[V8:.+]] (mod 5 5)))
// CHECK: (let (([[V9:.+]] (= [[V8]] 10)))
// CHECK: [[V9]])))
// CHECK-INLINED: (assert (= (mod 5 5) 10))
%6 = smt.int.mod %0, %0
%a6 = smt.eq %6, %1 : !smt.int
smt.assert %a6
// CHECK: (assert (let (([[V10:.+]] (<= 5 5)))
// CHECK: [[V10]]))
// CHECK-INLINED: (assert (<= 5 5))
%9 = smt.int.cmp le %0, %0
smt.assert %9
// CHECK: (assert (let (([[V11:.+]] (< 5 5)))
// CHECK: [[V11]]))
// CHECK-INLINED: (assert (< 5 5))
%10 = smt.int.cmp lt %0, %0
smt.assert %10
// CHECK: (assert (let (([[V12:.+]] (>= 5 5)))
// CHECK: [[V12]]))
// CHECK-INLINED: (assert (>= 5 5))
%11 = smt.int.cmp ge %0, %0
smt.assert %11
// CHECK: (assert (let (([[V13:.+]] (> 5 5)))
// CHECK: [[V13]]))
// CHECK-INLINED: (assert (> 5 5))
%12 = smt.int.cmp gt %0, %0
smt.assert %12
// CHECK: (reset)
// CHECK-INLINED: (reset)
}

1
tools/circt-translate/CMakeLists.txt
View File

@ -19,6 +19,7 @@ target_link_libraries(circt-translate
PRIVATE
${dialect_libs}
${translation_libs}
MLIRExportSMTLIB
MLIRIR
MLIRSupport
MLIRTranslateLib