[mlir][SMT] add missing ExportSMTLIB tests #136069
Merged
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
|
@llvm/pr-subscribers-mlir Author: Maksim Levental (makslevental) ChangesWhoops forgot these -export-smtlib tests. Full diff: https://github.com/llvm/llvm-project/pull/136069.diff 2 Files Affected:
diff --git a/mlir/test/Target/ExportSMTLIB/attributes.mlir b/mlir/test/Target/ExportSMTLIB/attributes.mlir
new file mode 100644
index 0000000000000..05e8d04803e28
--- /dev/null
+++ b/mlir/test/Target/ExportSMTLIB/attributes.mlir
@@ -0,0 +1,143 @@
+// RUN: mlir-translate --export-smtlib %s > %t && z3 %t 2>&1 | FileCheck %s
+// RUN: mlir-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
diff --git a/mlir/test/Target/ExportSMTLIB/basic.mlir b/mlir/test/Target/ExportSMTLIB/basic.mlir
new file mode 100644
index 0000000000000..2dc090bbb1051
--- /dev/null
+++ b/mlir/test/Target/ExportSMTLIB/basic.mlir
@@ -0,0 +1,191 @@
+// RUN: mlir-translate --export-smtlib %s > %t && z3 %t 2>&1 | FileCheck %s
+// RUN: mlir-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
|
math-fehr
approved these changes
Apr 17, 2025
| @@ -0,0 +1,143 @@ | |||
| // RUN: mlir-translate --export-smtlib %s > %t && z3 %t 2>&1 | FileCheck %s | |||
There was a problem hiding this comment.
Another way of doing that is to pipe it to z3 -in rather than creating a new file.
Just mentionning this, not sure what is usually preferred
There was a problem hiding this comment.
ah you know i didn't even notice that z3 was in that pipeline. anyway you're saying do this instead?
mlir-translate --export-smtlib %s | z3 -in 2>&1 | FileCheck %s
?
There was a problem hiding this comment.
Lemme just try it locally..............
There was a problem hiding this comment.
yea that works but i need to gate this test behind something that checks whether is on the system
There was a problem hiding this comment.
Yep! That's usually what I use in our filecheck tests.
Co-authored-by: Bea Healy <[email protected]> Co-authored-by: Martin Erhart <[email protected]> Co-authored-by: Mike Urbach <[email protected]> Co-authored-by: Will Dietz <[email protected]> Co-authored-by: fzi-hielscher <[email protected]> Co-authored-by: Fehr Mathieu <[email protected]> Co-authored-by: Clo91eaf <[email protected]>
makslevental
force-pushed
the
makslevental/add-exportlib-tests
branch
from
18137f9 to
2cdb240
Compare
math-fehr
reviewed
Apr 17, 2025
Comment on lines
1
to
4
| // 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 |
There was a problem hiding this comment.
You have both z3-prover and z3 here?
makslevental
force-pushed
the
makslevental/add-exportlib-tests
branch
from
2c81dbc to
dbc3ea8
Compare
makslevental
force-pushed
the
makslevental/add-exportlib-tests
branch
from
dbc3ea8 to
27abda9
Compare
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/24/builds/7455 Here is the relevant piece of the build log for the reference |
var-const
pushed a commit
to ldionne/llvm-project
that referenced
this pull request
Apr 17, 2025
Whoops forgot these -export-smtlib tests. --------- Co-authored-by: Bea Healy <[email protected]> Co-authored-by: Martin Erhart <[email protected]> Co-authored-by: Mike Urbach <[email protected]> Co-authored-by: Will Dietz <[email protected]> Co-authored-by: fzi-hielscher <[email protected]> Co-authored-by: Fehr Mathieu <[email protected]> Co-authored-by: Clo91eaf <[email protected]>
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.
Whoops forgot these -export-smtlib tests.