93 lines · plain
1// RUN: mlir-opt %s --split-input-file | FileCheck %s2 3// CHECK-LABEL: @schedule_with_constrained_param4module attributes {transform.with_named_sequence} {5 transform.named_sequence @schedule_with_constrained_param(%arg0: !transform.any_op {transform.readonly}) {6 // CHECK: %[[PARAM_AS_PARAM:.*]] = transform.param.constant7 %param_as_param = transform.param.constant 42 -> !transform.param<i64>8 9 // CHECK: transform.smt.constrain_params(%[[PARAM_AS_PARAM]])10 transform.smt.constrain_params(%param_as_param) : (!transform.param<i64>) -> () {11 // CHECK: ^bb{{.*}}(%[[PARAM_AS_SMT_SYMB:.*]]: !smt.int):12 ^bb0(%param_as_smt_var: !smt.int):13 // CHECK: %[[C0:.*]] = smt.int.constant 014 %c0 = smt.int.constant 015 // CHECK: %[[C43:.*]] = smt.int.constant 4316 %c43 = smt.int.constant 4317 // CHECK: %[[LOWER_BOUND:.*]] = smt.int.cmp le %[[C0]], %[[PARAM_AS_SMT_SYMB]]18 %lower_bound = smt.int.cmp le %c0, %param_as_smt_var19 // CHECK: smt.assert %[[LOWER_BOUND]]20 smt.assert %lower_bound21 // CHECK: %[[UPPER_BOUND:.*]] = smt.int.cmp le %[[PARAM_AS_SMT_SYMB]], %[[C43]]22 %upper_bound = smt.int.cmp le %param_as_smt_var, %c4323 // CHECK: smt.assert %[[UPPER_BOUND]]24 smt.assert %upper_bound25 }26 // NB: from here can rely on that 0 <= %param_as_param <= 43, even if its27 // definition changes.28 transform.yield29 }30}31 32// -----33 34// CHECK-LABEL: @schedule_with_constraint_on_multiple_params_returning_computed_value35module attributes {transform.with_named_sequence} {36 transform.named_sequence @schedule_with_constraint_on_multiple_params_returning_computed_value(%arg0: !transform.any_op {transform.readonly}) {37 // CHECK: %[[PARAM_A:.*]] = transform.param.constant38 %param_a = transform.param.constant 4 -> !transform.param<i64>39 // CHECK: %[[PARAM_B:.*]] = transform.param.constant40 %param_b = transform.param.constant 32 -> !transform.param<i64>41 42 // CHECK: transform.smt.constrain_params(%[[PARAM_A]], %[[PARAM_B]])43 %divisor = transform.smt.constrain_params(%param_a, %param_b) : (!transform.param<i64>, !transform.param<i64>) -> (!transform.param<i64>) {44 // CHECK: ^bb{{.*}}(%[[VAR_A:.*]]: !smt.int, %[[VAR_B:.*]]: !smt.int):45 ^bb0(%var_a: !smt.int, %var_b: !smt.int):46 // CHECK: %[[DIV:.*]] = smt.int.div %[[VAR_B]], %[[VAR_A]]47 %divisor = smt.int.div %var_b, %var_a48 // CHECK: %[[C0:.*]] = smt.int.constant 049 %c0 = smt.int.constant 050 // CHECK: %[[REMAINDER:.*]] = smt.int.mod %[[VAR_B]], %[[VAR_A]]51 %remainder = smt.int.mod %var_b, %var_a52 // CHECK: %[[EQ:.*]] = smt.eq %[[REMAINDER]], %[[C0]]53 %eq = smt.eq %remainder, %c0 : !smt.int54 // CHECK: smt.assert %[[EQ]]55 smt.assert %eq56 // CHECK: smt.yield %[[DIV]]57 smt.yield %divisor : !smt.int58 }59 // NB: from here can rely on that %param_a is a divisor of %param_b and60 // that the relevant factor, 8, got associated to %divisor.61 transform.yield62 }63}64 65// -----66 67// CHECK-LABEL: @schedule_with_param_as_a_bool68module attributes {transform.with_named_sequence} {69 transform.named_sequence @schedule_with_param_as_a_bool(%arg0: !transform.any_op {transform.readonly}) {70 // CHECK: %[[PARAM_AS_PARAM:.*]] = transform.param.constant71 %param_as_param = transform.param.constant true -> !transform.param<i1>72 73 // CHECK: transform.smt.constrain_params(%[[PARAM_AS_PARAM]])74 transform.smt.constrain_params(%param_as_param) : (!transform.param<i1>) -> () {75 // CHECK: ^bb{{.*}}(%[[PARAM_AS_SMT_VAR:.*]]: !smt.bool):76 ^bb0(%param_as_smt_var: !smt.bool):77 // CHECK: %[[C0:.*]] = smt.int.constant 078 %c0 = smt.int.constant 079 // CHECK: %[[C1:.*]] = smt.int.constant 180 %c1 = smt.int.constant 181 // CHECK: %[[FALSEHOOD:.*]] = smt.eq %[[C0]], %[[C1]]82 %falsehood = smt.eq %c0, %c1 : !smt.int83 // CHECK: %[[TRUE_IFF_PARAM_IS:.*]] = smt.or %[[PARAM_AS_SMT_VAR]], %[[FALSEHOOD]]84 %true_iff_param_is = smt.or %param_as_smt_var, %falsehood85 // CHECK: smt.assert %[[TRUE_IFF_PARAM_IS]]86 smt.assert %true_iff_param_is87 }88 // NB: from here can rely on that %param_as_param holds true, even if its89 // definition changes.90 transform.yield91 }92}93