From 2cdb24059f199e9602c9cc03634cb2d81eccbf6a Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Wed, 16 Apr 2025 21:26:22 -0400 Subject: [PATCH 1/3] [mlir][SMT] add missing ExportSMTLIB tests Co-authored-by: Bea Healy Co-authored-by: Martin Erhart Co-authored-by: Mike Urbach Co-authored-by: Will Dietz Co-authored-by: fzi-hielscher Co-authored-by: Fehr Mathieu Co-authored-by: Clo91eaf --- 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 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 27abda9e14048bff5d67cdefeaef27d029db8500 Mon Sep 17 00:00:00 2001 From: Maksim Levental Date: Wed, 16 Apr 2025 22:35:25 -0400 Subject: [PATCH 3/3] Update basic.mlir --- mlir/test/Target/ExportSMTLIB/basic.mlir | 3 +-- mlir/test/Target/ExportSMTLIB/lit.local.cfg | 2 ++ 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/mlir/test/Target/ExportSMTLIB/basic.mlir b/mlir/test/Target/ExportSMTLIB/basic.mlir index 35c1bd709fca5..81c23cde0f9fd 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 %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 // 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")