144 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// Quantifiers Attributes6smt.solver () : () -> () {7 8 %true = smt.constant true9 10 %7 = smt.exists weight 2 {11 ^bb0(%arg2: !smt.int, %arg3: !smt.int):12 %4 = smt.eq %arg2, %arg3 : !smt.int13 %5 = smt.implies %4, %true14 smt.yield %5 : !smt.bool15 }16 smt.assert %717 18 smt.check sat {} unknown {} unsat {}19}20 21// CHECK-NOT: WARNING22// CHECK-NOT: warning23// CHECK-NOT: ERROR24// CHECK-NOT: error25// CHECK-NOT: unsat26// CHECK: sat27 28// Quantifiers Attributes29smt.solver () : () -> () {30 31 %true = smt.constant true32 33 %7 = smt.exists weight 2 {34 ^bb0(%arg2: !smt.int, %arg3: !smt.int):35 %4 = smt.eq %arg2, %arg3 : !smt.int36 %5 = smt.implies %4, %true37 smt.yield %5 : !smt.bool38 } patterns {39 ^bb0(%arg2: !smt.int, %arg3: !smt.int):40 %4 = smt.eq %arg2, %arg3 : !smt.int41 smt.yield %4: !smt.bool42 }43 smt.assert %744 45 smt.check sat {} unknown {} unsat {}46}47 48// CHECK-NOT: WARNING49// CHECK-NOT: warning50// CHECK-NOT: ERROR51// CHECK-NOT: error52// CHECK-NOT: unsat53// CHECK: sat54 55// Quantifiers Attributes56smt.solver () : () -> () {57 58 %true = smt.constant true59 60 %7 = smt.exists {61 ^bb0(%arg2: !smt.int, %arg3: !smt.int):62 %4 = smt.eq %arg2, %arg3 : !smt.int63 %5 = smt.implies %4, %true64 smt.yield %5 : !smt.bool65 } patterns {66 ^bb0(%arg2: !smt.int, %arg3: !smt.int):67 %4 = smt.eq %arg2, %arg3 : !smt.int68 smt.yield %4: !smt.bool69 }70 smt.assert %771 72 smt.check sat {} unknown {} unsat {}73}74 75// CHECK-NOT: WARNING76// CHECK-NOT: warning77// CHECK-NOT: ERROR78// CHECK-NOT: error79// CHECK-NOT: unsat80// CHECK: sat81 82smt.solver () : () -> () {83 84 %true = smt.constant true85 %three = smt.int.constant 386 %four = smt.int.constant 487 88 %7 = smt.exists {89 ^bb0(%arg2: !smt.int, %arg3: !smt.int):90 %4 = smt.eq %arg2, %three: !smt.int91 %5 = smt.eq %arg3, %four: !smt.int92 %6 = smt.eq %4, %5: !smt.bool93 smt.yield %6 : !smt.bool94 } patterns {95 ^bb0(%arg2: !smt.int, %arg3: !smt.int):96 %4 = smt.eq %arg2, %three: !smt.int97 smt.yield %4: !smt.bool}, {98 ^bb0(%arg2: !smt.int, %arg3: !smt.int):99 %5 = smt.eq %arg3, %four: !smt.int100 smt.yield %5: !smt.bool101 }102 smt.assert %7103 104 smt.check sat {} unknown {} unsat {}105}106 107// CHECK-NOT: WARNING108// CHECK-NOT: warning109// CHECK-NOT: ERROR110// CHECK-NOT: error111// CHECK-NOT: unsat112// CHECK: sat113 114smt.solver () : () -> () {115 116 %true = smt.constant true117 %three = smt.int.constant 3118 %four = smt.int.constant 4119 120 %10 = smt.exists {121 ^bb0(%arg2: !smt.int, %arg3: !smt.int):122 %4 = smt.eq %arg2, %three: !smt.int123 %5 = smt.eq %arg3, %four: !smt.int124 %9 = smt.eq %4, %5: !smt.bool125 smt.yield %9 : !smt.bool126 } patterns {127 ^bb0(%arg2: !smt.int, %arg3: !smt.int):128 %4 = smt.eq %arg2, %three: !smt.int129 %5 = smt.eq %arg3, %four: !smt.int130 smt.yield %4, %5: !smt.bool, !smt.bool131 }132 smt.assert %10133 134 smt.check sat {} unknown {} unsat {}135 136}137 138// CHECK-NOT: WARNING139// CHECK-NOT: warning140// CHECK-NOT: ERROR141// CHECK-NOT: error142// CHECK-NOT: unsat143// CHECK: sat144