201 lines · plain
1// RUN: mlir-opt %s --verify-roundtrip | FileCheck %s2 3// CHECK-LABEL: func @types4// CHECK-SAME: (%{{.*}}: !smt.bool, %{{.*}}: !smt.bv<32>, %{{.*}}: !smt.int, %{{.*}}: !smt.sort<"uninterpreted_sort">, %{{.*}}: !smt.sort<"uninterpreted_sort"[!smt.bool, !smt.int]>, %{{.*}}: !smt.func<(!smt.bool, !smt.bool) !smt.bool>)5func.func @types(%arg0: !smt.bool, %arg1: !smt.bv<32>, %arg2: !smt.int, %arg3: !smt.sort<"uninterpreted_sort">, %arg4: !smt.sort<"uninterpreted_sort"[!smt.bool, !smt.int]>, %arg5: !smt.func<(!smt.bool, !smt.bool) !smt.bool>) {6 return7}8 9func.func @core(%in: i8) {10 // CHECK: %a = smt.declare_fun "a" {smt.some_attr} : !smt.bool11 %a = smt.declare_fun "a" {smt.some_attr} : !smt.bool12 // CHECK: smt.declare_fun {smt.some_attr} : !smt.bv<32>13 %b = smt.declare_fun {smt.some_attr} : !smt.bv<32>14 // CHECK: smt.declare_fun {smt.some_attr} : !smt.int15 %c = smt.declare_fun {smt.some_attr} : !smt.int16 // CHECK: smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">17 %d = smt.declare_fun {smt.some_attr} : !smt.sort<"uninterpreted_sort">18 // CHECK: smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>19 %e = smt.declare_fun {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>20 21 // CHECK: smt.constant true {smt.some_attr}22 %true = smt.constant true {smt.some_attr}23 // CHECK: smt.constant false {smt.some_attr}24 %false = smt.constant false {smt.some_attr}25 26 // CHECK: smt.assert %a {smt.some_attr}27 smt.assert %a {smt.some_attr}28 29 // CHECK: smt.reset {smt.some_attr}30 smt.reset {smt.some_attr}31 32 // CHECK: smt.push 1 {smt.some_attr}33 smt.push 1 {smt.some_attr}34 35 // CHECK: smt.pop 1 {smt.some_attr}36 smt.pop 1 {smt.some_attr}37 38 // CHECK: %{{.*}} = smt.solver(%{{.*}}) {smt.some_attr} : (i8) -> (i8, i32) {39 // CHECK: ^bb0(%{{.*}}: i8)40 // CHECK: %{{.*}} = smt.check {smt.some_attr} sat {41 // CHECK: smt.yield %{{.*}} : i3242 // CHECK: } unknown {43 // CHECK: smt.yield %{{.*}} : i3244 // CHECK: } unsat {45 // CHECK: smt.yield %{{.*}} : i3246 // CHECK: } -> i3247 // CHECK: smt.yield %{{.*}}, %{{.*}} : i8, i3248 // CHECK: }49 %0:2 = smt.solver(%in) {smt.some_attr} : (i8) -> (i8, i32) {50 ^bb0(%arg0: i8):51 %1 = smt.check {smt.some_attr} sat {52 %c1_i32 = arith.constant 1 : i3253 smt.yield %c1_i32 : i3254 } unknown {55 %c0_i32 = arith.constant 0 : i3256 smt.yield %c0_i32 : i3257 } unsat {58 %c-1_i32 = arith.constant -1 : i3259 smt.yield %c-1_i32 : i3260 } -> i3261 smt.yield %arg0, %1 : i8, i3262 }63 64 // CHECK: smt.solver() : () -> () {65 // CHECK-NEXT: }66 smt.solver() : () -> () { }67 68 // CHECK: smt.solver() : () -> () {69 // CHECK-NEXT: smt.set_logic "AUFLIA"70 // CHECK-NEXT: }71 smt.solver() : () -> () {72 smt.set_logic "AUFLIA"73 }74 75 // CHECK: smt.check sat {76 // CHECK-NEXT: } unknown {77 // CHECK-NEXT: } unsat {78 // CHECK-NEXT: }79 smt.check sat { } unknown { } unsat { }80 81 // CHECK: %{{.*}} = smt.eq %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>82 %1 = smt.eq %b, %b {smt.some_attr} : !smt.bv<32>83 // CHECK: %{{.*}} = smt.distinct %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>84 %2 = smt.distinct %b, %b {smt.some_attr} : !smt.bv<32>85 86 // CHECK: %{{.*}} = smt.eq %{{.*}}, %{{.*}}, %{{.*}} : !smt.bool87 %3 = smt.eq %a, %a, %a : !smt.bool88 // CHECK: %{{.*}} = smt.distinct %{{.*}}, %{{.*}}, %{{.*}} : !smt.bool89 %4 = smt.distinct %a, %a, %a : !smt.bool90 91 // CHECK: %{{.*}} = smt.ite %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr} : !smt.bv<32>92 %5 = smt.ite %a, %b, %b {smt.some_attr} : !smt.bv<32>93 94 // CHECK: %{{.*}} = smt.not %{{.*}} {smt.some_attr}95 %6 = smt.not %a {smt.some_attr}96 // CHECK: %{{.*}} = smt.and %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}97 %7 = smt.and %a, %a, %a {smt.some_attr}98 // CHECK: %{{.*}} = smt.or %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}99 %8 = smt.or %a, %a, %a {smt.some_attr}100 // CHECK: %{{.*}} = smt.xor %{{.*}}, %{{.*}}, %{{.*}} {smt.some_attr}101 %9 = smt.xor %a, %a, %a {smt.some_attr}102 // CHECK: %{{.*}} = smt.implies %{{.*}}, %{{.*}} {smt.some_attr}103 %10 = smt.implies %a, %a {smt.some_attr}104 105 // CHECK: smt.apply_func %{{.*}}(%{{.*}}, %{{.*}}) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>106 %11 = smt.apply_func %e(%c, %a) {smt.some_attr} : !smt.func<(!smt.int, !smt.bool) !smt.bool>107 108 return109}110 111// CHECK-LABEL: func @quantifiers112func.func @quantifiers() {113 // CHECK-NEXT: smt.forall ["a", "b"] weight 2 attributes {smt.some_attr} {114 // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):115 // CHECK-NEXT: smt.eq116 // CHECK-NEXT: smt.yield %{{.*}}117 // CHECK-NEXT: } patterns {118 // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool, %{{.*}}: !smt.bool):119 // CHECK-NEXT: smt.yield %{{.*}}120 // CHECK-NEXT: }, {121 // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool):122 // CHECK-NEXT: smt.yield %{{.*}}123 // CHECK-NEXT: }124 %0 = smt.forall ["a", "b"] weight 2 attributes {smt.some_attr} {125 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):126 %1 = smt.eq %arg2, %arg3 : !smt.bool127 smt.yield %1 : !smt.bool128 } patterns {129 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):130 smt.yield %arg2, %arg3 : !smt.bool, !smt.bool131 }, {132 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):133 smt.yield %arg2, %arg3 : !smt.bool, !smt.bool134 }135 136 // CHECK-NEXT: smt.forall ["a", "b"] no_pattern attributes {smt.some_attr} {137 // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):138 // CHECK-NEXT: smt.eq139 // CHECK-NEXT: smt.yield %{{.*}}140 // CHECK-NEXT: }141 %1 = smt.forall ["a", "b"] no_pattern attributes {smt.some_attr} {142 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):143 %2 = smt.eq %arg2, %arg3 : !smt.bool144 smt.yield %2 : !smt.bool145 }146 147 // CHECK-NEXT: smt.forall {148 // CHECK-NEXT: smt.constant149 // CHECK-NEXT: smt.yield %{{.*}}150 // CHECK-NEXT: }151 %2 = smt.forall {152 %3 = smt.constant true153 smt.yield %3 : !smt.bool154 }155 156 // CHECK-NEXT: smt.exists ["a", "b"] weight 2 attributes {smt.some_attr} {157 // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):158 // CHECK-NEXT: smt.eq159 // CHECK-NEXT: smt.yield %{{.*}}160 // CHECK-NEXT: } patterns {161 // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool, %{{.*}}: !smt.bool):162 // CHECK-NEXT: smt.yield %{{.*}}163 // CHECK-NEXT: }, {164 // CHECK-NEXT: ^bb0(%{{.*}}: !smt.bool):165 // CHECK-NEXT: smt.yield %{{.*}}166 // CHECK-NEXT: }167 %3 = smt.exists ["a", "b"] weight 2 attributes {smt.some_attr} {168 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):169 %4 = smt.eq %arg2, %arg3 : !smt.bool170 smt.yield %4 : !smt.bool {smt.some_attr}171 } patterns {172 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):173 smt.yield %arg2, %arg3 : !smt.bool, !smt.bool174 }, {175 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):176 smt.yield %arg2, %arg3 : !smt.bool, !smt.bool177 }178 179 // CHECK-NEXT: smt.exists no_pattern attributes {smt.some_attr} {180 // CHECK-NEXT: ^bb0({{.*}}: !smt.bool, {{.*}}: !smt.bool):181 // CHECK-NEXT: smt.eq182 // CHECK-NEXT: smt.yield %{{.*}}183 // CHECK-NEXT: }184 %4 = smt.exists no_pattern attributes {smt.some_attr} {185 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):186 %5 = smt.eq %arg2, %arg3 : !smt.bool187 smt.yield %5 : !smt.bool {smt.some_attr}188 }189 190 // CHECK-NEXT: smt.exists [] {191 // CHECK-NEXT: smt.constant192 // CHECK-NEXT: smt.yield %{{.*}}193 // CHECK-NEXT: }194 %5 = smt.exists [] {195 %6 = smt.constant true196 smt.yield %6 : !smt.bool197 }198 199 return200}201