[mlir][SMT] add export smtlib #131492
Merged
[mlir][SMT] add export smtlib #131492
+1,822
−0
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
makslevental
requested review from
maerhart,
fabianschuiki,
jpienaar,
ftynse and
math-fehr
|
@llvm/pr-subscribers-mlir Author: Maksim Levental (makslevental) Changessee #131480 TODO: add C APIs here after C APIs are added for smt dialect. Patch is 194.37 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/131492.diff 47 Files Affected:
diff --git a/mlir/include/mlir/Dialect/CMakeLists.txt b/mlir/include/mlir/Dialect/CMakeLists.txt
index f710235197334..9d1a840d6644b 100644
--- a/mlir/include/mlir/Dialect/CMakeLists.txt
+++ b/mlir/include/mlir/Dialect/CMakeLists.txt
@@ -33,6 +33,7 @@ add_subdirectory(Ptr)
add_subdirectory(Quant)
add_subdirectory(SCF)
add_subdirectory(Shape)
+add_subdirectory(SMT)
add_subdirectory(SparseTensor)
add_subdirectory(SPIRV)
add_subdirectory(Tensor)
diff --git a/mlir/include/mlir/Dialect/SMT/CMakeLists.txt b/mlir/include/mlir/Dialect/SMT/CMakeLists.txt
new file mode 100644
index 0000000000000..f33061b2d87cf
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(IR)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt b/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
new file mode 100644
index 0000000000000..bd743ed510a9e
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/CMakeLists.txt
@@ -0,0 +1,16 @@
+add_mlir_dialect(SMT smt)
+add_mlir_doc(SMT SMT Dialects/SMTOps -gen-op-doc)
+# TODO(maX)
+#add_mlir_doc(SMT SMT Dialects/SMTTypes -gen-typedef-doc -dialect smt)
+
+set(LLVM_TARGET_DEFINITIONS SMT.td)
+
+mlir_tablegen(SMTAttributes.h.inc -gen-attrdef-decls)
+mlir_tablegen(SMTAttributes.cpp.inc -gen-attrdef-defs)
+add_public_tablegen_target(MLIRSMTAttrIncGen)
+add_dependencies(mlir-headers MLIRSMTAttrIncGen)
+
+mlir_tablegen(SMTEnums.h.inc -gen-enum-decls)
+mlir_tablegen(SMTEnums.cpp.inc -gen-enum-defs)
+add_public_tablegen_target(MLIRSMTEnumsIncGen)
+add_dependencies(mlir-headers MLIRSMTEnumsIncGen)
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMT.td b/mlir/include/mlir/Dialect/SMT/IR/SMT.td
new file mode 100644
index 0000000000000..dd7bd033c9fa5
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMT.td
@@ -0,0 +1,22 @@
+//===- SMT.td - SMT dialect definition ---------------------*- tablegen -*-===//
+//
+// 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 MLIR_DIALECT_SMT_SMT_TD
+#define MLIR_DIALECT_SMT_SMT_TD
+
+include "mlir/IR/OpBase.td"
+
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/Dialect/SMT/IR/SMTOps.td"
+include "mlir/Dialect/SMT/IR/SMTArrayOps.td"
+include "mlir/Dialect/SMT/IR/SMTBitVectorOps.td"
+include "mlir/Dialect/SMT/IR/SMTIntOps.td"
+
+#endif // MLIR_DIALECT_SMT_SMT_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
new file mode 100644
index 0000000000000..05b5398b6a7f9
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTArrayOps.td
@@ -0,0 +1,99 @@
+//===- SMTArrayOps.td - SMT array operations ---------------*- tablegen -*-===//
+//
+// 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 MLIR_DIALECT_SMT_SMTARRAYOPS_TD
+#define MLIR_DIALECT_SMT_SMTARRAYOPS_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class SMTArrayOp<string mnemonic, list<Trait> traits = []> :
+ SMTOp<"array." # mnemonic, traits>;
+
+def ArrayStoreOp : SMTArrayOp<"store", [
+ Pure,
+ TypesMatchWith<"summary", "array", "index",
+ "cast<ArrayType>($_self).getDomainType()">,
+ TypesMatchWith<"summary", "array", "value",
+ "cast<ArrayType>($_self).getRangeType()">,
+ AllTypesMatch<["array", "result"]>,
+]> {
+ let summary = "stores a value at a given index and returns the new array";
+ let description = [{
+ This operation returns a new array which is the same as the 'array' operand
+ except that the value at the given 'index' is changed to the given 'value'.
+ The semantics are equivalent to the 'store' operator described in the
+ [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
+ the SMT-LIB standard 2.6.
+ }];
+
+ let arguments = (ins ArrayType:$array, AnySMTType:$index, AnySMTType:$value);
+ let results = (outs ArrayType:$result);
+
+ let assemblyFormat = [{
+ $array `[` $index `]` `,` $value attr-dict `:` qualified(type($array))
+ }];
+}
+
+def ArraySelectOp : SMTArrayOp<"select", [
+ Pure,
+ TypesMatchWith<"summary", "array", "index",
+ "cast<ArrayType>($_self).getDomainType()">,
+ TypesMatchWith<"summary", "array", "result",
+ "cast<ArrayType>($_self).getRangeType()">,
+]> {
+ let summary = "get the value stored in the array at the given index";
+ let description = [{
+ This operation is retuns the value stored in the given array at the given
+ index. The semantics are equivalent to the `select` operator defined in the
+ [SMT ArrayEx theory](https://smtlib.cs.uiowa.edu/Theories/ArraysEx.smt2) of
+ the SMT-LIB standard 2.6.
+ }];
+
+ let arguments = (ins ArrayType:$array, AnySMTType:$index);
+ let results = (outs AnySMTType:$result);
+
+ let assemblyFormat = [{
+ $array `[` $index `]` attr-dict `:` qualified(type($array))
+ }];
+}
+
+def ArrayBroadcastOp : SMTArrayOp<"broadcast", [
+ Pure,
+ TypesMatchWith<"summary", "result", "value",
+ "cast<ArrayType>($_self).getRangeType()">,
+]> {
+ let summary = "construct an array with the given value stored at every index";
+ let description = [{
+ This operation represents a broadcast of the 'value' operand to all indices
+ of the array. It is equivalent to
+ ```
+ %0 = smt.declare "array" : !smt.array<[!smt.int -> !smt.bool]>
+ %1 = smt.forall ["idx"] {
+ ^bb0(%idx: !smt.int):
+ %2 = smt.array.select %0[%idx] : !smt.array<[!smt.int -> !smt.bool]>
+ %3 = smt.eq %value, %2 : !smt.bool
+ smt.yield %3 : !smt.bool
+ }
+ smt.assert %1
+ // return %0
+ ```
+
+ In SMT-LIB, this is frequently written as
+ `((as const (Array Int Bool)) value)`.
+ }];
+
+ let arguments = (ins AnySMTType:$value);
+ let results = (outs ArrayType:$result);
+
+ let assemblyFormat = "$value attr-dict `:` qualified(type($result))";
+}
+
+#endif // MLIR_DIALECT_SMT_SMTARRAYOPS_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
new file mode 100644
index 0000000000000..590364d572699
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.h
@@ -0,0 +1,29 @@
+//===- SMTAttributes.h - Declare SMT dialect attributes ----------*- 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 MLIR_DIALECT_SMT_SMTATTRIBUTES_H
+#define MLIR_DIALECT_SMT_SMTATTRIBUTES_H
+
+#include "mlir/IR/Attributes.h"
+#include "mlir/IR/BuiltinAttributeInterfaces.h"
+#include "mlir/IR/BuiltinAttributes.h"
+
+namespace mlir {
+namespace smt {
+namespace detail {
+
+struct BitVectorAttrStorage;
+
+} // namespace detail
+} // namespace smt
+} // namespace mlir
+
+#define GET_ATTRDEF_CLASSES
+#include "mlir/Dialect/SMT/IR/SMTAttributes.h.inc"
+
+#endif // MLIR_DIALECT_SMT_SMTATTRIBUTES_H
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
new file mode 100644
index 0000000000000..4231363fdf05b
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTAttributes.td
@@ -0,0 +1,74 @@
+//===- SMTAttributes.td - Attributes for SMT dialect -------*- tablegen -*-===//
+//
+// 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 file defines SMT dialect specific attributes.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
+#define MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/BuiltinAttributeInterfaces.td"
+
+def BitVectorAttr : AttrDef<SMTDialect, "BitVector", [
+ DeclareAttrInterfaceMethods<TypedAttrInterface>
+]> {
+ let mnemonic = "bv";
+ let description = [{
+ This attribute represents a constant value of the `(_ BitVec width)` sort as
+ described in the [SMT bit-vector
+ theory](https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml).
+
+ The constant is as #bX (binary) or #xX (hexadecimal) in SMT-LIB
+ where X is the value in the corresponding format without any further
+ prefixing. Here, the bit-vector constant is given as a regular integer
+ literal and the associated bit-vector type indicating the bit-width.
+
+ Examples:
+ ```mlir
+ #smt.bv<5> : !smt.bv<4>
+ #smt.bv<92> : !smt.bv<8>
+ ```
+
+ The explicit type-suffix is mandatory to uniquely represent the attribute,
+ i.e., this attribute should always be used in the extended form (using the
+ `quantified` keyword in the operation assembly format string).
+
+ The bit-width must be greater than zero (i.e., at least one digit has to be
+ present).
+ }];
+
+ let parameters = (ins "llvm::APInt":$value);
+
+ let hasCustomAssemblyFormat = true;
+ let genVerifyDecl = true;
+
+ // We need to manually define the storage class because the generated one is
+ // buggy (because the APInt asserts matching bitwidth in the `==` operator and
+ // the generated storage uses that directly.
+ // Alternatively: add a type parameter to redundantly store the bitwidth of
+ // of the attribute type, it it's in the order before the 'value' it will be
+ // checked before the APInt equality (this is the reason it works for the
+ // builtin integer attribute), but would be more fragile (and we'd store
+ // duplicate data).
+ let genStorageClass = false;
+
+ let builders = [
+ AttrBuilder<(ins "llvm::StringRef":$value)>,
+ AttrBuilder<(ins "uint64_t":$value, "unsigned":$width)>,
+ ];
+
+ let extraClassDeclaration = [{
+ /// Return the bit-vector constant as a SMT-LIB formatted string.
+ std::string getValueAsString(bool prefix = true) const;
+ }];
+}
+
+#endif // MLIR_DIALECT_SMT_SMTATTRIBUTES_TD
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
new file mode 100644
index 0000000000000..b6ca34e142d82
--- /dev/null
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTBitVectorOps.td
@@ -0,0 +1,255 @@
+//===- SMTBitVectorOps.td - SMT bit-vector dialect ops -----*- tablegen -*-===//
+//
+// 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 MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
+#define MLIR_DIALECT_SMT_SMTBITVECTOROPS_TD
+
+include "mlir/Dialect/SMT/IR/SMTDialect.td"
+include "mlir/Dialect/SMT/IR/SMTAttributes.td"
+include "mlir/Dialect/SMT/IR/SMTTypes.td"
+include "mlir/IR/EnumAttr.td"
+include "mlir/IR/OpAsmInterface.td"
+include "mlir/Interfaces/InferTypeOpInterface.td"
+include "mlir/Interfaces/SideEffectInterfaces.td"
+
+class SMTBVOp<string mnemonic, list<Trait> traits = []> :
+ Op<SMTDialect, "bv." # mnemonic, traits>;
+
+def BVConstantOp : SMTBVOp<"constant", [
+ Pure,
+ ConstantLike,
+ FirstAttrDerivedResultType,
+ DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>,
+ DeclareOpInterfaceMethods<OpAsmOpInterface, ["getAsmResultNames"]>
+]> {
+ let summary = "produce a constant bit-vector";
+ let description = [{
+ This operation produces an SSA value equal to the bit-vector constant
+ specified by the 'value' attribute.
+ Refer to the `BitVectorAttr` documentation for more information about
+ the semantics of bit-vector constants, their format, and associated sort.
+ The result type always matches the attribute's type.
+
+ Examples:
+ ```mlir
+ %c92_bv8 = smt.bv.constant #smt.bv<92> : !smt.bv<8>
+ %c5_bv4 = smt.bv.constant #smt.bv<5> : !smt.bv<4>
+ ```
+ }];
+
+ let arguments = (ins BitVectorAttr:$value);
+ let results = (outs BitVectorType:$result);
+
+ let assemblyFormat = "qualified($value) attr-dict";
+
+ let builders = [
+ OpBuilder<(ins "const llvm::APInt &":$value), [{
+ build($_builder, $_state,
+ BitVectorAttr::get($_builder.getContext(), value));
+ }]>,
+ OpBuilder<(ins "uint64_t":$value, "unsigned":$width), [{
+ build($_builder, $_state,
+ BitVectorAttr::get($_builder.getContext(), value, width));
+ }]>,
+ ];
+
+ let hasFolder = true;
+}
+
+class BVArithmeticOrBitwiseOp<string mnemonic, string desc> :
+ SMTBVOp<mnemonic, [Pure, SameOperandsAndResultType]> {
+ let summary = "equivalent to bv" # mnemonic # " in SMT-LIB";
+ let description = "This operation performs " # desc # [{. The semantics are
+ equivalent to the `bv}] # mnemonic # [{` operator defined in the SMT-LIB 2.6
+ standard. More precisely in the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+ }];
+
+ let results = (outs BitVectorType:$result);
+}
+
+class BinaryBVOp<string mnemonic, string desc> :
+ BVArithmeticOrBitwiseOp<mnemonic, desc> {
+ let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs);
+ let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type($result))";
+}
+
+class UnaryBVOp<string mnemonic, string desc> :
+ BVArithmeticOrBitwiseOp<mnemonic, desc> {
+ let arguments = (ins BitVectorType:$input);
+ let assemblyFormat = "$input attr-dict `:` qualified(type($result))";
+}
+
+def BVNotOp : UnaryBVOp<"not", "bitwise negation">;
+def BVNegOp : UnaryBVOp<"neg", "two's complement unary minus">;
+
+def BVAndOp : BinaryBVOp<"and", "bitwise AND">;
+def BVOrOp : BinaryBVOp<"or", "bitwise OR">;
+def BVXOrOp : BinaryBVOp<"xor", "bitwise exclusive OR">;
+
+def BVAddOp : BinaryBVOp<"add", "addition">;
+def BVMulOp : BinaryBVOp<"mul", "multiplication">;
+def BVUDivOp : BinaryBVOp<"udiv", "unsigned division (rounded towards zero)">;
+def BVSDivOp : BinaryBVOp<"sdiv", "two's complement signed division">;
+def BVURemOp : BinaryBVOp<"urem", "unsigned remainder">;
+def BVSRemOp : BinaryBVOp<"srem",
+ "two's complement signed remainder (sign follows dividend)">;
+def BVSModOp : BinaryBVOp<"smod",
+ "two's complement signed remainder (sign follows divisor)">;
+def BVShlOp : BinaryBVOp<"shl", "shift left">;
+def BVLShrOp : BinaryBVOp<"lshr", "logical shift right">;
+def BVAShrOp : BinaryBVOp<"ashr", "arithmetic shift right">;
+
+def PredicateSLT : I64EnumAttrCase<"slt", 0>;
+def PredicateSLE : I64EnumAttrCase<"sle", 1>;
+def PredicateSGT : I64EnumAttrCase<"sgt", 2>;
+def PredicateSGE : I64EnumAttrCase<"sge", 3>;
+def PredicateULT : I64EnumAttrCase<"ult", 4>;
+def PredicateULE : I64EnumAttrCase<"ule", 5>;
+def PredicateUGT : I64EnumAttrCase<"ugt", 6>;
+def PredicateUGE : I64EnumAttrCase<"uge", 7>;
+let cppNamespace = "mlir::smt" in
+def BVCmpPredicate : I64EnumAttr<
+ "BVCmpPredicate",
+ "smt bit-vector comparison predicate",
+ [PredicateSLT, PredicateSLE, PredicateSGT, PredicateSGE,
+ PredicateULT, PredicateULE, PredicateUGT, PredicateUGE]>;
+
+def BVCmpOp : SMTBVOp<"cmp", [Pure, SameTypeOperands]> {
+ let summary = "compare bit-vectors interpreted as signed or unsigned";
+ let description = [{
+ This operation compares bit-vector values, interpreting them as signed or
+ unsigned values depending on the predicate. The semantics are equivalent to
+ the `bvslt`, `bvsle`, `bvsgt`, `bvsge`, `bvult`, `bvule`, `bvugt`, or
+ `bvuge` operator defined in the SMT-LIB 2.6 standard depending on the
+ specified predicate. More precisely in the
+ [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+ }];
+
+ let arguments = (ins BVCmpPredicate:$pred,
+ BitVectorType:$lhs,
+ BitVectorType:$rhs);
+ let results = (outs BoolType:$result);
+
+ let assemblyFormat = [{
+ $pred $lhs `,` $rhs attr-dict `:` qualified(type($lhs))
+ }];
+}
+
+def ConcatOp : SMTBVOp<"concat", [
+ Pure,
+ DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>
+]> {
+ let summary = "bit-vector concatenation";
+ let description = [{
+ This operation concatenates bit-vector values with semantics equivalent to
+ the `concat` operator defined in the SMT-LIB 2.6 standard. More precisely in
+ the [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+
+ Note that the following equivalences hold:
+ * `smt.bv.concat %a, %b : !smt.bv<4>, !smt.bv<4>` is equivalent to
+ `(concat a b)` in SMT-LIB
+ * `(= (concat #xf #x0) #xf0)`
+ }];
+
+ let arguments = (ins BitVectorType:$lhs, BitVectorType:$rhs);
+ let results = (outs BitVectorType:$result);
+
+ let assemblyFormat = "$lhs `,` $rhs attr-dict `:` qualified(type(operands))";
+}
+
+def ExtractOp : SMTBVOp<"extract", [Pure]> {
+ let summary = "bit-vector extraction";
+ let description = [{
+ This operation extracts the range of bits starting at the 'lowBit' index
+ (inclusive) up to the 'lowBit' + result-width index (exclusive). The
+ semantics are equivalent to the `extract` operator defined in the SMT-LIB
+ 2.6 standard. More precisely in the
+ [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+
+ Note that `smt.bv.extract %bv from 2 : (!smt.bv<32>) -> !smt.bv<16>` is
+ equivalent to `((_ extract 17 2) bv)`, i.e., the SMT-LIB operator takes the
+ low and high indices where both are inclusive. The following equivalence
+ holds: `(= ((_ extract 3 0) #x0f) #xf)`
+ }];
+
+ let arguments = (ins I32Attr:$lowBit, BitVectorType:$input);
+ let results = (outs BitVectorType:$result);
+
+ let assemblyFormat = [{
+ $input `from` $lowBit attr-dict `:` functional-type($input, $result)
+ }];
+
+ let hasVerifier = true;
+}
+
+def RepeatOp : SMTBVOp<"repeat", [Pure]> {
+ let summary = "repeated bit-vector concatenation of one value";
+ let description = [{
+ This operation is a shorthand for repeated concatenation of the same
+ bit-vector value, i.e.,
+ ```mlir
+ smt.bv.repeat 5 times %a : !smt.bv<4>
+ // is the same as
+ %0 = smt.bv.repeat 4 times %a : !smt.bv<4>
+ smt.bv.concat %a, %0 : !smt.bv<4>, !smt.bv<16>
+ // or also
+ %0 = smt.bv.repeat 4 times %a : !smt.bv<4>
+ smt.bv.concat %0, %a : !smt.bv<16>, !smt.bv<4>
+ ```
+
+ The semantics are equivalent to the `repeat` operator defined in the SMT-LIB
+ 2.6 standard. More precisely in the
+ [theory of FixedSizeBitVectors](https://smtlib.cs.uiowa.edu/Theories/FixedSizeBitVectors.smt2)
+ and the [QF_BV logic](https://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2)
+ describing closed quantifier-free formulas over the theory of fixed-size
+ bit-vectors.
+ }];
+
+ let arguments = (ins BitVectorType:$input);
+ let results = (outs BitVectorType:$result)...
[truncated]
|
makslevental
changed the title
makslevental
force-pushed
the
makslevental/export-smtlib
branch
from
86a8cc6 to
bcbfdfd
Compare
|
ping - this one is ready now that #131480 is merged. |
math-fehr
approved these changes
Apr 12, 2025
Comment on lines
+508
to
+527
| 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(); | ||
| } |
There was a problem hiding this comment.
Why are these here and not in the ExpressionVisitor?
There was a problem hiding this comment.
i mean i think expressionvisitor is basically for binary/unary ops? maybe not? i can move
There was a problem hiding this comment.
hmm didn't work for some reason (some logic somewhere in the visitor dispatch 🤷) - gonna leave for now (we can revisit later if it's an issue
There was a problem hiding this comment.
it was the easiest way to always inline constants instead of assigning them to a temporary. We'd need to special case them in the dispatch method of the expression visitor if we wanted to move them there.
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/203/builds/7465 Here is the relevant piece of the build log for the reference |
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/205/builds/6256 Here is the relevant piece of the build log for the reference |
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/204/builds/6278 Here is the relevant piece of the build log for the reference |
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/130/builds/12296 Here is the relevant piece of the build log for the reference |
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/80/builds/12485 Here is the relevant piece of the build log for the reference |
jplehr
added a commit
to jplehr/llvm-project
that referenced
this pull request
Apr 12, 2025
After llvm#131492 is appears that linking MLIRAritDialect was missing.
jplehr
added a commit
that referenced
this pull request
Apr 12, 2025
var-const
pushed a commit
to ldionne/llvm-project
that referenced
this pull request
Apr 17, 2025
This PR adds the `ExportSMTLIB` translation/egress pass for `SMT` dialect.
var-const
pushed a commit
to ldionne/llvm-project
that referenced
this pull request
Apr 17, 2025
After llvm#131492 is appears that linking MLIRAritDialect was missing.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the
ExportSMTLIBtranslation/egress pass forSMTdialect.