This PR upstreams the `SMT` dialect from the CIRCT project. Here we only check in the dialect/op/types/attributes and lit tests. Follow up PRs will add conversions in and out and etc. Co-authored-by: Bea Healy <beahealy22@gmail.com> Co-authored-by: Martin Erhart <maerhart@outlook.com> Co-authored-by: Mike Urbach <mikeurbach@gmail.com> Co-authored-by: Will Dietz <will.dietz@sifive.com> Co-authored-by: fzi-hielscher <hielscher@fzi.de> Co-authored-by: Fehr Mathieu <mathieu.fehr@gmail.com>
14 lines
372 B
MLIR
14 lines
372 B
MLIR
// RUN: mlir-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
|
|
}
|