192 lines · plain
1// REQUIRES: z3-prover2// RUN: mlir-translate --export-smtlib %s | z3 -in 2>&1 | FileCheck %s3// RUN: mlir-translate --export-smtlib --smtlibexport-inline-single-use-values %s | z3 -in 2>&1 | FileCheck %s4 5// Function and constant symbol declarations, uninterpreted sorts6smt.solver () : () -> () {7 %0 = smt.declare_fun "b" : !smt.bv<32>8 %1 = smt.declare_fun : !smt.int9 %2 = smt.declare_fun : !smt.func<(!smt.int, !smt.bv<32>) !smt.bool>10 %3 = smt.apply_func %2(%1, %0) : !smt.func<(!smt.int, !smt.bv<32>) !smt.bool>11 smt.assert %312 13 %4 = smt.declare_fun : !smt.sort<"uninterpreted">14 %5 = smt.declare_fun : !smt.sort<"other"[!smt.sort<"uninterpreted">]>15 %6 = smt.declare_fun : !smt.func<(!smt.sort<"other"[!smt.sort<"uninterpreted">]>, !smt.sort<"uninterpreted">) !smt.bool>16 %7 = smt.apply_func %6(%5, %4) : !smt.func<(!smt.sort<"other"[!smt.sort<"uninterpreted">]>, !smt.sort<"uninterpreted">) !smt.bool>17 smt.assert %718 19 smt.check sat {} unknown {} unsat {}20}21 22// CHECK-NOT: WARNING23// CHECK-NOT: warning24// CHECK-NOT: ERROR25// CHECK-NOT: error26// CHECK-NOT: unsat27// CHECK: sat28 29// Big expression30smt.solver () : () -> () {31 %true = smt.constant true32 %false = smt.constant false33 %0 = smt.not %true34 %1 = smt.and %0, %true, %false35 %2 = smt.or %1, %0, %true36 %3 = smt.xor %0, %237 %4 = smt.implies %3, %false38 %5 = smt.implies %4, %true39 smt.assert %540 41 smt.check sat {} unknown {} unsat {}42}43 44// CHECK-NOT: WARNING45// CHECK-NOT: warning46// CHECK-NOT: ERROR47// CHECK-NOT: error48// CHECK-NOT: unsat49// CHECK: sat50 51// Constant array52smt.solver () : () -> () {53 %true = smt.constant true54 %false = smt.constant false55 %c = smt.int.constant 056 %0 = smt.array.broadcast %true : !smt.array<[!smt.int -> !smt.bool]>57 %1 = smt.array.store %0[%c], %false : !smt.array<[!smt.int -> !smt.bool]>58 %2 = smt.array.select %1[%c] : !smt.array<[!smt.int -> !smt.bool]>59 smt.assert %260 61 smt.check sat {} unknown {} unsat {}62}63 64// CHECK-NOT: WARNING65// CHECK-NOT: warning66// CHECK-NOT: ERROR67// CHECK-NOT: error68// CHECK: unsat69 70// BitVector extract and concat, and constants71smt.solver () : () -> () {72 %xf = smt.bv.constant #smt.bv<0xf> : !smt.bv<4>73 %x0 = smt.bv.constant #smt.bv<0> : !smt.bv<4>74 %xff = smt.bv.constant #smt.bv<0xff> : !smt.bv<8>75 76 %0 = smt.bv.concat %xf, %x0 : !smt.bv<4>, !smt.bv<4>77 %1 = smt.bv.extract %0 from 4 : (!smt.bv<8>) -> !smt.bv<4>78 %2 = smt.bv.repeat 2 times %1 : !smt.bv<4>79 %3 = smt.eq %2, %xff : !smt.bv<8>80 smt.assert %381 82 smt.check sat {} unknown {} unsat {}83}84 85// CHECK-NOT: WARNING86// CHECK-NOT: warning87// CHECK-NOT: ERROR88// CHECK-NOT: error89// CHECK-NOT: unsat90// CHECK: sat91 92// Quantifiers93smt.solver () : () -> () {94 %1 = smt.forall ["a"] {95 ^bb0(%arg2: !smt.int):96 %c2_1 = smt.int.constant 297 %2 = smt.int.mul %arg2, %c2_198 99 %3 = smt.exists {100 ^bb0(%arg1: !smt.int):101 %c2 = smt.int.constant 2102 %4 = smt.int.mul %c2, %arg1103 %5 = smt.eq %4, %2 : !smt.int104 smt.yield %5 : !smt.bool105 }106 107 smt.yield %3 : !smt.bool108 }109 smt.assert %1110 111 smt.check sat {} unknown {} unsat {}112}113 114// CHECK-NOT: WARNING115// CHECK-NOT: warning116// CHECK-NOT: ERROR117// CHECK-NOT: error118// CHECK-NOT: unsat119// CHECK: sat120 121// Push and pop122smt.solver () : () -> () {123 %three = smt.int.constant 3124 %four = smt.int.constant 4125 %unsat_eq = smt.eq %three, %four : !smt.int126 %sat_eq = smt.eq %three, %three : !smt.int127 128 smt.push 1129 smt.assert %unsat_eq130 smt.check sat {} unknown {} unsat {}131 smt.pop 1132 smt.assert %sat_eq133 smt.check sat {} unknown {} unsat {}134}135 136// CHECK-NOT: WARNING137// CHECK-NOT: warning138// CHECK-NOT: ERROR139// CHECK-NOT: error140// CHECK-NOT: sat141// CHECK: unsat142// CHECK-NOT: WARNING143// CHECK-NOT: warning144// CHECK-NOT: ERROR145// CHECK-NOT: error146// CHECK-NOT: unsat147// CHECK: sat148 149// Reset150smt.solver () : () -> () {151 %three = smt.int.constant 3152 %four = smt.int.constant 4153 %unsat_eq = smt.eq %three, %four : !smt.int154 %sat_eq = smt.eq %three, %three : !smt.int155 156 smt.assert %unsat_eq157 smt.check sat {} unknown {} unsat {}158 smt.reset159 smt.assert %sat_eq160 smt.check sat {} unknown {} unsat {}161}162 163// CHECK-NOT: WARNING164// CHECK-NOT: warning165// CHECK-NOT: ERROR166// CHECK-NOT: error167// CHECK-NOT: sat168// CHECK: unsat169// CHECK-NOT: WARNING170// CHECK-NOT: warning171// CHECK-NOT: ERROR172// CHECK-NOT: error173// CHECK-NOT: unsat174// CHECK: sat175 176smt.solver () : () -> () {177 smt.set_logic "HORN"178 %c = smt.declare_fun : !smt.int179 %c4 = smt.int.constant 4180 %eq = smt.eq %c, %c4 : !smt.int181 smt.assert %eq182 smt.check sat {} unknown {} unsat {}183}184 185// CHECK-NOT: WARNING186// CHECK-NOT: warning187// CHECK-NOT: ERROR188// CHECK-NOT: error189// CHECK-NOT: unsat190// CHECK-NOT: sat191// CHECK: unknown192