178 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 6 %true = smt.constant true7 8 9 // CHECK: (assert (let (([[V10:.+]] (forall (([[A:.+]] Int) ([[B:.+]] Int))10 // CHECK: ( ! (let (([[V11:.+]] (= [[A]] [[B]])))11 // CHECK: [[V11]]) :weight 2))))12 // CHECK: [[V10]]))13 14 // CHECK-INLINED: (assert (forall (([[A:.+]] Int) ([[B:.+]] Int))15 // CHECK-INLINED: ( ! (= [[A]] [[B]]) :weight 2)))16 %1 = smt.forall ["a", "b"] weight 2 {17 ^bb0(%arg2: !smt.int, %arg3: !smt.int):18 %2 = smt.eq %arg2, %arg3 : !smt.int19 smt.yield %2 : !smt.bool20 }21 smt.assert %122 23 24 // CHECK: (assert (let (([[V12:.+]] (exists (([[V13:.+]] Int) ([[V14:.+]] Int))25 // CHECK: ( ! (let (([[V15:.+]] (= [[V13]] [[V14]])))26 // CHECK: [[V15]]) :weight 2))))27 // CHECK: [[V12]]))28 29 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))30 // CHECK-INLINED: ( ! (= [[A]] [[B]]) :weight 2)))31 32 %2 = smt.exists weight 2 {33 ^bb0(%arg2: !smt.int, %arg3: !smt.int):34 %3 = smt.eq %arg2, %arg3 : !smt.int35 smt.yield %3 : !smt.bool36 }37 smt.assert %238 39 40 41 // CHECK: (assert (let (([[V16:.+]] (exists (([[V17:.+]] Int) ([[V18:.+]] Int))42 // CHECK: ( ! (let (([[V19:.+]] (= [[V17]] [[V18]])))43 // CHECK: (let (([[V20:.+]] (=> [[V19:.+]] true)))44 // CHECK: [[V20:.+]])) :weight 2))))45 // CHECK: [[V16]])){{$}}46 47 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))48 // CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true) :weight 2)))49 50 %3 = smt.exists weight 2 {51 ^bb0(%arg2: !smt.int, %arg3: !smt.int):52 %4 = smt.eq %arg2, %arg3 : !smt.int53 %5 = smt.implies %4, %true54 smt.yield %5 : !smt.bool55 }56 smt.assert %357 58 59 // CHECK: (assert (let (([[V21:.+]] (exists (([[V22:.+]] Int) ([[V23:.+]] Int))60 // CHECK: ( ! (let (([[V24:.+]] (= [[V22]] [[V23]])))61 // CHECK: (let (([[V25:.+]] (=> [[V24]] true)))62 // CHECK: [[V25]])) 63 // CHECK: :pattern ((let (([[V26:.+]] (= [[V22]] [[V23]])))64 // CHECK: [[V26]]))))))65 // CHECK: [[V21]])){{$}}66 67 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))68 // CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true)69 // CHECK-INLINED: :pattern ((= [[A]] [[B]])))))70 71 %6 = smt.exists {72 ^bb0(%arg2: !smt.int, %arg3: !smt.int):73 %4 = smt.eq %arg2, %arg3 : !smt.int74 %5 = smt.implies %4, %true75 smt.yield %5 : !smt.bool76 } patterns {77 ^bb0(%arg2: !smt.int, %arg3: !smt.int):78 %4 = smt.eq %arg2, %arg3 : !smt.int79 smt.yield %4: !smt.bool80 }81 smt.assert %682 83 // CHECK: (assert (let (([[V27:.+]] (exists (([[V28:.+]] Int) ([[V29:.+]] Int))84 // CHECK: ( ! (let (([[V30:.+]] (= [[V28]] [[V29]])))85 // CHECK: (let (([[V31:.+]] (=> [[V30]] true)))86 // CHECK: [[V31]])) :weight 287 // CHECK: :pattern ((let (([[V32:.+]] (= [[V28]] [[V29]])))88 // CHECK: [[V32]]))))))89 // CHECK: [[V27]])){{$}}90 91 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))92 // CHECK-INLINED: ( ! (=> (= [[A]] [[B]]) true) :weight 293 // CHECK-INLINED: :pattern ((= [[A]] [[B]])))))94 95 %7 = smt.exists weight 2 {96 ^bb0(%arg2: !smt.int, %arg3: !smt.int):97 %4 = smt.eq %arg2, %arg3 : !smt.int98 %5 = smt.implies %4, %true99 smt.yield %5 : !smt.bool100 } patterns {101 ^bb0(%arg2: !smt.int, %arg3: !smt.int):102 %4 = smt.eq %arg2, %arg3 : !smt.int103 smt.yield %4: !smt.bool104 }105 smt.assert %7106 107 // CHECK: (assert (let (([[V33:.+]] (exists (([[V34:.+]] Int) ([[V35:.+]] Int))108 // CHECK: ( ! (let (([[V36:.+]] (= [[V35]] 4)))109 // CHECK: (let (([[V37:.+]] (= [[V34]] 3)))110 // CHECK: (let (([[V38:.+]] (= [[V37]] [[V36]])))111 // CHECK: [[V38]])))112 // CHECK: :pattern ((let (([[V39:.+]] (= [[V34]] 3)))113 // CHECK: [[V39]]) (let (([[V40:.+]] (= [[V35]] 4)))114 // CHECK: [[V40]]))))))115 // CHECK: [[V33]])){{$}}116 117 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))118 // CHECK-INLINED: ( ! (= (= [[A]] 3) (= [[B]] 4))119 // CHECK-INLINED: :pattern ((= [[A]] 3) (= [[B]] 4)))))120 121 122 %three = smt.int.constant 3123 %four = smt.int.constant 4124 125 %8 = smt.exists {126 ^bb0(%arg2: !smt.int, %arg3: !smt.int):127 %4 = smt.eq %arg2, %three: !smt.int128 %5 = smt.eq %arg3, %four: !smt.int129 %9 = smt.eq %4, %5: !smt.bool130 smt.yield %9 : !smt.bool131 } patterns {132 ^bb0(%arg2: !smt.int, %arg3: !smt.int):133 %4 = smt.eq %arg2, %three: !smt.int134 smt.yield %4: !smt.bool135 }, {136 ^bb0(%arg2: !smt.int, %arg3: !smt.int):137 %5 = smt.eq %arg3, %four: !smt.int138 smt.yield %5: !smt.bool139 }140 smt.assert %8141 142 smt.check sat {} unknown {} unsat {}143 144 // CHECK: (assert (let (([[V41:.+]] (exists (([[V42:.+]] Int) ([[V43:.+]] Int))145 // CHECK: ( ! (let (([[V44:.+]] (= [[V43]] 4)))146 // CHECK: (let (([[V45:.+]] (= [[V42]] 3)))147 // CHECK: (let (([[V46:.+]] (= [[V45]] [[V44]])))148 // CHECK: [[V46]])))149 // CHECK: :pattern ((let (([[V47:.+]] (= [[V42]] 3)))150 // CHECK: [[V47]])(let (([[V48:.+]] (= [[V43]] 4)))151 // CHECK: [[V48]]))))))152 // CHECK: [[V41]])){{$}}153 154 // CHECK-INLINED: (assert (exists (([[A:.+]] Int) ([[B:.+]] Int))155 // CHECK-INLINED: ( ! (= (= [[A]] 3) (= [[B]] 4))156 // CHECK-INLINED: :pattern ((= [[A]] 3)(= [[B]] 4)))))157 158 %10 = smt.exists {159 ^bb0(%arg2: !smt.int, %arg3: !smt.int):160 %4 = smt.eq %arg2, %three: !smt.int161 %5 = smt.eq %arg3, %four: !smt.int162 %9 = smt.eq %4, %5: !smt.bool163 smt.yield %9 : !smt.bool164 } patterns {165 ^bb0(%arg2: !smt.int, %arg3: !smt.int):166 %4 = smt.eq %arg2, %three: !smt.int167 %5 = smt.eq %arg3, %four: !smt.int168 smt.yield %4, %5: !smt.bool, !smt.bool169 }170 smt.assert %10171 172 smt.check sat {} unknown {} unsat {}173 174 // CHECK: (reset)175 // CHECK-INLINED: (reset)176 177}178