138 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 %c0_bv32 = smt.bv.constant #smt.bv<0> : !smt.bv<32>6 %true = smt.constant true7 %false = smt.constant false8 9 // CHECK: (declare-const b (_ BitVec 32))10 // CHECK: (assert (let (([[V0:.+]] (= #x00000000 b)))11 // CHECK: [[V0]]))12 13 // CHECK-INLINED: (declare-const b (_ BitVec 32))14 // CHECK-INLINED: (assert (= #x00000000 b))15 %21 = smt.declare_fun "b" : !smt.bv<32>16 %23 = smt.eq %c0_bv32, %21 : !smt.bv<32>17 smt.assert %2318 19 // CHECK: (assert (let (([[V1:.+]] (distinct #x00000000 #x00000000)))20 // CHECK: [[V1]]))21 22 // CHECK-INLINED: (assert (distinct #x00000000 #x00000000))23 %24 = smt.distinct %c0_bv32, %c0_bv32 : !smt.bv<32>24 smt.assert %2425 26 // CHECK: (declare-const a Bool)27 // CHECK: (assert (let (([[V2:.+]] (ite a #x00000000 b)))28 // CHECK: (let (([[V3:.+]] (= #x00000000 [[V2]])))29 // CHECK: [[V3]])))30 31 // CHECK-INLINED: (declare-const a Bool)32 // CHECK-INLINED: (assert (= #x00000000 (ite a #x00000000 b)))33 %20 = smt.declare_fun "a" : !smt.bool34 %38 = smt.ite %20, %c0_bv32, %21 : !smt.bv<32>35 %4 = smt.eq %c0_bv32, %38 : !smt.bv<32>36 smt.assert %437 38 // CHECK: (assert (let (([[V4:.+]] (not true)))39 // CHECK: (let (([[V5:.+]] (and [[V4]] true false)))40 // CHECK: (let (([[V6:.+]] (or [[V5]] [[V4]] true)))41 // CHECK: (let (([[V7:.+]] (xor [[V4]] [[V6]])))42 // CHECK: (let (([[V8:.+]] (=> [[V7]] false)))43 // CHECK: [[V8]]))))))44 45 // CHECK-INLINED: (assert (let (([[V15:.+]] (not true)))46 // CHECK-INLINED: (=> (xor [[V15]] (or (and [[V15]] true false) [[V15]] true)) false)))47 %39 = smt.not %true48 %40 = smt.and %39, %true, %false49 %41 = smt.or %40, %39, %true50 %42 = smt.xor %39, %4151 %43 = smt.implies %42, %false52 smt.assert %4353 54 // CHECK: (declare-fun func1 (Bool Bool) Bool)55 // CHECK: (assert (let (([[V9:.+]] (func1 true false)))56 // CHECK: [[V9]]))57 58 // CHECK-INLINED: (declare-fun func1 (Bool Bool) Bool)59 // CHECK-INLINED: (assert (func1 true false))60 %44 = smt.declare_fun "func1" : !smt.func<(!smt.bool, !smt.bool) !smt.bool>61 %45 = smt.apply_func %44(%true, %false) : !smt.func<(!smt.bool, !smt.bool) !smt.bool>62 smt.assert %4563 64 // CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))65 // CHECK: (let (([[V11:.+]] (= [[A]] [[B]])))66 // CHECK: [[V11]]))))67 // CHECK: [[V10]]))68 69 // CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))70 // CHECK-INLINED: (= [[A]] [[B]])))71 %1 = smt.forall ["a", "b"] {72 ^bb0(%arg2: !smt.int, %arg3: !smt.int):73 %2 = smt.eq %arg2, %arg3 : !smt.int74 smt.yield %2 : !smt.bool75 }76 smt.assert %177 78 // CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))79 // CHECK: (let (([[V15:.+]] (= [[V13]] [[V14]])))80 // CHECK: [[V15]]))))81 // CHECK: [[V12]]))82 83 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))84 // CHECK-INLINED: (= [[A]] [[B]])))85 %2 = smt.exists {86 ^bb0(%arg2: !smt.int, %arg3: !smt.int):87 %3 = smt.eq %arg2, %arg3 : !smt.int88 smt.yield %3 : !smt.bool89 }90 smt.assert %291 92 // Test: make sure that open parens from outside quantifier bodies are not93 // propagated into the body.94 // CHECK: (assert (let (([[V15:.+]] (exists (([[V16:.+]] Int) ([[V17:.+]] Int)){{$}}95 // CHECK: (let (([[V18:.+]] (= [[V16]] [[V17]]))){{$}}96 // CHECK: [[V18]])))){{$}}97 // CHECK: (let (([[V19:.+]] (exists (([[V20:.+]] Int) ([[V21:.+]] Int)){{$}}98 // CHECK: (let (([[V22:.+]] (= [[V20]] [[V21]]))){{$}}99 // CHECK: [[V22]])))){{$}}100 // CHECK: (let (([[V23:.+]] (and [[V19]] [[V15]]))){{$}}101 // CHECK: [[V23]])))){{$}}102 %3 = smt.exists {103 ^bb0(%arg2: !smt.int, %arg3: !smt.int):104 %5 = smt.eq %arg2, %arg3 : !smt.int105 smt.yield %5 : !smt.bool106 }107 %5 = smt.exists {108 ^bb0(%arg2: !smt.int, %arg3: !smt.int):109 %6 = smt.eq %arg2, %arg3 : !smt.int110 smt.yield %6 : !smt.bool111 }112 %6 = smt.and %3, %5113 smt.assert %6114 115 // CHECK: (check-sat)116 // CHECK-INLINED: (check-sat)117 smt.check sat {} unknown {} unsat {}118 119 // CHECK: (reset)120 // CHECK-INLINED: (reset)121 smt.reset122 123 // CHECK: (push 1)124 // CHECK-INLINED: (push 1)125 smt.push 1126 127 // CHECK: (pop 1)128 // CHECK-INLINED: (pop 1)129 smt.pop 1130 131 // CHECK: (set-logic AUFLIA)132 // CHECK-INLINED: (set-logic AUFLIA)133 smt.set_logic "AUFLIA"134 135 // CHECK: (reset)136 // CHECK-INLINED: (reset)137}138