[Mlir-commits] [mlir] [mlir][SMT] add missing ExportSMTLIB tests (PR #136069)
Maksim Levental
llvmlistbot at llvm.org
Wed Apr 16 20:27:16 PDT 2025
https://github.com/makslevental updated https://github.com/llvm/llvm-project/pull/136069
>From 2cdb24059f199e9602c9cc03634cb2d81eccbf6a Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 16 Apr 2025 21:26:22 -0400
Subject: [PATCH 1/3] [mlir][SMT] add missing ExportSMTLIB tests
Co-authored-by: Bea Healy <beahealy22 at gmail.com>
Co-authored-by: Martin Erhart <maerhart at outlook.com>
Co-authored-by: Mike Urbach <mikeurbach at gmail.com>
Co-authored-by: Will Dietz <will.dietz at sifive.com>
Co-authored-by: fzi-hielscher <hielscher at fzi.de>
Co-authored-by: Fehr Mathieu <mathieu.fehr at gmail.com>
Co-authored-by: Clo91eaf <Clo91eaf at qq.com>
---
mlir/test/Target/ExportSMTLIB/attributes.mlir | 143 +++++++++++++
mlir/test/Target/ExportSMTLIB/basic.mlir | 192 ++++++++++++++++++
mlir/test/Target/ExportSMTLIB/lit.local.cfg | 3 +
3 files changed, 338 insertions(+)
create mode 100644 mlir/test/Target/ExportSMTLIB/attributes.mlir
create mode 100644 mlir/test/Target/ExportSMTLIB/basic.mlir
create mode 100644 mlir/test/Target/ExportSMTLIB/lit.local.cfg
diff --git a/mlir/test/Target/ExportSMTLIB/attributes.mlir b/mlir/test/Target/ExportSMTLIB/attributes.mlir
new file mode 100644
index 0000000000000..7af517e92ebf3
--- /dev/null
+++ b/mlir/test/Target/ExportSMTLIB/attributes.mlir
@@ -0,0 +1,143 @@
+// RUN: mlir-translate --export-smtlib %s | z3 -in 2>&1 | FileCheck %s
+// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 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
diff --git a/mlir/test/Target/ExportSMTLIB/basic.mlir b/mlir/test/Target/ExportSMTLIB/basic.mlir
new file mode 100644
index 0000000000000..35c1bd709fca5
--- /dev/null
+++ b/mlir/test/Target/ExportSMTLIB/basic.mlir
@@ -0,0 +1,192 @@
+// REQUIRES: z3-prover
+// RUN: mlir-translate --export-smtlib %s | z3 -in %t 2>&1 | FileCheck %s
+// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 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
diff --git a/mlir/test/Target/ExportSMTLIB/lit.local.cfg b/mlir/test/Target/ExportSMTLIB/lit.local.cfg
new file mode 100644
index 0000000000000..1df424e6667fb
--- /dev/null
+++ b/mlir/test/Target/ExportSMTLIB/lit.local.cfg
@@ -0,0 +1,3 @@
+if lit.util.which("z3", config.environment["PATH"]):
+ config.available_features.add("z3-prover")
+
>From e1bd9cceb6e4652e3822ed7a827268bf3284eed5 Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 16 Apr 2025 22:34:56 -0400
Subject: [PATCH 2/3] Update attributes.mlir
---
mlir/test/Target/ExportSMTLIB/attributes.mlir | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/mlir/test/Target/ExportSMTLIB/attributes.mlir b/mlir/test/Target/ExportSMTLIB/attributes.mlir
index 7af517e92ebf3..2ecbd145acbe3 100644
--- a/mlir/test/Target/ExportSMTLIB/attributes.mlir
+++ b/mlir/test/Target/ExportSMTLIB/attributes.mlir
@@ -1,6 +1,6 @@
+// REQUIRES: z3-prover
// RUN: mlir-translate --export-smtlib %s | z3 -in 2>&1 | FileCheck %s
// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 2>&1 | FileCheck %s
-// REQUIRES: z3
// Quantifiers Attributes
smt.solver () : () -> () {
>From dbc3ea8a111af7582ecc3c1320f98123fb09f0fe Mon Sep 17 00:00:00 2001
From: Maksim Levental <maksim.levental at gmail.com>
Date: Wed, 16 Apr 2025 22:35:25 -0400
Subject: [PATCH 3/3] Update basic.mlir
---
mlir/test/Target/ExportSMTLIB/basic.mlir | 1 -
mlir/test/Target/ExportSMTLIB/lit.local.cfg | 2 ++
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/mlir/test/Target/ExportSMTLIB/basic.mlir b/mlir/test/Target/ExportSMTLIB/basic.mlir
index 35c1bd709fca5..a52ea8b60d92c 100644
--- a/mlir/test/Target/ExportSMTLIB/basic.mlir
+++ b/mlir/test/Target/ExportSMTLIB/basic.mlir
@@ -1,7 +1,6 @@
// REQUIRES: z3-prover
// RUN: mlir-translate --export-smtlib %s | z3 -in %t 2>&1 | FileCheck %s
// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 2>&1 | FileCheck %s
-// REQUIRES: z3
// Function and constant symbol declarations, uninterpreted sorts
smt.solver () : () -> () {
diff --git a/mlir/test/Target/ExportSMTLIB/lit.local.cfg b/mlir/test/Target/ExportSMTLIB/lit.local.cfg
index 1df424e6667fb..ecc28e19f5b95 100644
--- a/mlir/test/Target/ExportSMTLIB/lit.local.cfg
+++ b/mlir/test/Target/ExportSMTLIB/lit.local.cfg
@@ -1,3 +1,5 @@
+import lit.util
+
if lit.util.which("z3", config.environment["PATH"]):
config.available_features.add("z3-prover")
More information about the Mlir-commits
mailing list