22 lines · plain
1// RUN: mlir-translate --export-smtlib %s | FileCheck %s2// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | FileCheck %s --check-prefix=CHECK-INLINED3 4smt.solver () : () -> () {5 %c = smt.int.constant 06 %true = smt.constant true7 8 // CHECK: (assert (let (([[V0:.+]] ((as const (Array Int Bool)) true)))9 // CHECK: (let (([[V1:.+]] (store [[V0]] 0 true)))10 // CHECK: (let (([[V2:.+]] (select [[V1]] 0)))11 // CHECK: [[V2]]))))12 13 // CHECK-INLINED: (assert (select (store ((as const (Array Int Bool)) true) 0 true) 0))14 %0 = smt.array.broadcast %true : !smt.array<[!smt.int -> !smt.bool]>15 %1 = smt.array.store %0[%c], %true : !smt.array<[!smt.int -> !smt.bool]>16 %2 = smt.array.select %1[%c] : !smt.array<[!smt.int -> !smt.bool]>17 smt.assert %218 19 // CHECK: (reset)20 // CHECK-INLINED: (reset)21}22