498 lines · plain
1// RUN: mlir-opt %s --split-input-file --verify-diagnostics2 3func.func @solver_isolated_from_above(%arg0: !smt.bool) {4 // expected-note @below {{required by region isolation constraints}}5 smt.solver() : () -> () {6 // expected-error @below {{using value defined outside the region}}7 smt.assert %arg08 }9 return10}11 12// -----13 14func.func @no_smt_value_enters_solver(%arg0: !smt.bool) {15 // expected-error @below {{operand #0 must be variadic of any non-smt type, but got '!smt.bool'}}16 smt.solver(%arg0) : (!smt.bool) -> () {17 ^bb0(%arg1: !smt.bool):18 smt.assert %arg119 }20 return21}22 23// -----24 25func.func @no_smt_value_exits_solver() {26 // expected-error @below {{result #0 must be variadic of any non-smt type, but got '!smt.bool'}}27 %0 = smt.solver() : () -> !smt.bool {28 %a = smt.declare_fun "a" : !smt.bool29 smt.yield %a : !smt.bool30 }31 return32}33 34// -----35 36func.func @block_args_and_inputs_match() {37 // expected-error @below {{block argument types must match the types of the 'inputs'}}38 smt.solver() : () -> () {39 ^bb0(%arg0: i32):40 }41 return42}43 44// -----45 46func.func @solver_yield_operands_and_results_match() {47 // expected-error @below {{types of yielded values must match return values}}48 smt.solver() : () -> () {49 %1 = arith.constant 0 : i3250 smt.yield %1 : i3251 }52 return53}54 55// -----56 57func.func @check_yield_operands_and_results_match() {58 // expected-error @below {{types of yielded values in 'unsat' region must match return values}}59 %0 = smt.check sat {60 %1 = arith.constant 0 : i3261 smt.yield %1 : i3262 } unknown {63 %1 = arith.constant 0 : i3264 smt.yield %1 : i3265 } unsat { } -> i3266 return67}68 69// -----70 71func.func @check_yield_operands_and_results_match() {72 // expected-error @below {{types of yielded values in 'unknown' region must match return values}}73 %0 = smt.check sat {74 %1 = arith.constant 0 : i3275 smt.yield %1 : i3276 } unknown {77 } unsat {78 %1 = arith.constant 0 : i3279 smt.yield %1 : i3280 } -> i3281 return82}83 84// -----85 86func.func @check_yield_operands_and_results_match() {87 // expected-error @below {{types of yielded values in 'sat' region must match return values}}88 %0 = smt.check sat {89 } unknown {90 %1 = arith.constant 0 : i3291 smt.yield %1 : i3292 } unsat {93 %1 = arith.constant 0 : i3294 smt.yield %1 : i3295 } -> i3296 return97}98 99// -----100 101func.func @check_no_block_arguments() {102 // expected-error @below {{region #0 should have no arguments}}103 smt.check sat {104 ^bb0(%arg0: i32):105 } unknown {106 } unsat {107 }108 return109}110 111// -----112 113func.func @check_no_block_arguments() {114 // expected-error @below {{region #1 should have no arguments}}115 smt.check sat {116 } unknown {117 ^bb0(%arg0: i32):118 } unsat {119 }120 return121}122 123// -----124 125func.func @check_no_block_arguments() {126 // expected-error @below {{region #2 should have no arguments}}127 smt.check sat {128 } unknown {129 } unsat {130 ^bb0(%arg0: i32):131 }132 return133}134 135// -----136 137func.func @too_few_operands() {138 // expected-error @below {{'inputs' must have at least size 2, but got 0}}139 smt.eq : !smt.bool140 return141}142 143// -----144 145func.func @too_few_operands(%a: !smt.bool) {146 // expected-error @below {{'inputs' must have at least size 2, but got 1}}147 smt.distinct %a : !smt.bool148 return149}150 151// -----152 153func.func @ite_type_mismatch(%a: !smt.bool, %b: !smt.bv<32>) {154 // expected-error @below {{failed to verify that all of {thenValue, elseValue, result} have same type}}155 "smt.ite"(%a, %a, %b) {} : (!smt.bool, !smt.bool, !smt.bv<32>) -> !smt.bool156 return157}158 159// -----160 161func.func @forall_number_of_decl_names_must_match_num_args() {162 // expected-error @below {{number of bound variable names must match number of block arguments}}163 %1 = smt.forall ["a"] {164 ^bb0(%arg2: !smt.int, %arg3: !smt.int):165 %2 = smt.eq %arg2, %arg3 : !smt.int166 smt.yield %2 : !smt.bool167 }168 return169}170 171// -----172 173func.func @exists_number_of_decl_names_must_match_num_args() {174 // expected-error @below {{number of bound variable names must match number of block arguments}}175 %1 = smt.exists ["a"] {176 ^bb0(%arg2: !smt.int, %arg3: !smt.int):177 %2 = smt.eq %arg2, %arg3 : !smt.int178 smt.yield %2 : !smt.bool179 }180 return181}182 183// -----184 185func.func @forall_yield_must_have_exactly_one_bool_value() {186 // expected-error @below {{yielded value must be of '!smt.bool' type}}187 %1 = smt.forall ["a", "b"] {188 ^bb0(%arg2: !smt.int, %arg3: !smt.int):189 %2 = smt.int.add %arg2, %arg3190 smt.yield %2 : !smt.int191 }192 return193}194 195// -----196 197func.func @forall_yield_must_have_exactly_one_bool_value() {198 // expected-error @below {{must have exactly one yielded value}}199 %1 = smt.forall ["a", "b"] {200 ^bb0(%arg2: !smt.int, %arg3: !smt.int):201 smt.yield202 }203 return204}205 206// -----207 208func.func @exists_yield_must_have_exactly_one_bool_value() {209 // expected-error @below {{yielded value must be of '!smt.bool' type}}210 %1 = smt.exists ["a", "b"] {211 ^bb0(%arg2: !smt.int, %arg3: !smt.int):212 %2 = smt.int.add %arg2, %arg3213 smt.yield %2 : !smt.int214 }215 return216}217 218// -----219 220func.func @exists_yield_must_have_exactly_one_bool_value() {221 // expected-error @below {{must have exactly one yielded value}}222 %1 = smt.exists ["a", "b"] {223 ^bb0(%arg2: !smt.int, %arg3: !smt.int):224 smt.yield225 }226 return227}228 229// -----230 231func.func @exists_patterns_region_and_no_patterns_attr_are_mutually_exclusive() {232 // expected-error @below {{patterns and the no_pattern attribute must not be specified at the same time}}233 %1 = smt.exists ["a"] no_pattern {234 ^bb0(%arg2: !smt.bool):235 smt.yield %arg2 : !smt.bool236 } patterns {237 ^bb0(%arg2: !smt.bool):238 smt.yield %arg2 : !smt.bool239 }240 return241}242 243// -----244 245func.func @forall_patterns_region_and_no_patterns_attr_are_mutually_exclusive() {246 // expected-error @below {{patterns and the no_pattern attribute must not be specified at the same time}}247 %1 = smt.forall ["a"] no_pattern {248 ^bb0(%arg2: !smt.bool):249 smt.yield %arg2 : !smt.bool250 } patterns {251 ^bb0(%arg2: !smt.bool):252 smt.yield %arg2 : !smt.bool253 }254 return255}256 257// -----258 259func.func @exists_patterns_region_num_args() {260 // expected-error @below {{block argument number and types of the 'body' and 'patterns' region #0 must match}}261 %1 = smt.exists ["a"] {262 ^bb0(%arg2: !smt.bool):263 smt.yield %arg2 : !smt.bool264 } patterns {265 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):266 smt.yield %arg2, %arg3 : !smt.bool, !smt.bool267 }268 return269}270 271// -----272 273func.func @forall_patterns_region_num_args() {274 // expected-error @below {{block argument number and types of the 'body' and 'patterns' region #0 must match}}275 %1 = smt.forall ["a"] {276 ^bb0(%arg2: !smt.bool):277 smt.yield %arg2 : !smt.bool278 } patterns {279 ^bb0(%arg2: !smt.bool, %arg3: !smt.bool):280 smt.yield %arg2, %arg3 : !smt.bool, !smt.bool281 }282 return283}284 285// -----286 287func.func @exists_patterns_region_at_least_one_yielded_value() {288 // expected-error @below {{'patterns' region #0 must have at least one yielded value}}289 %1 = smt.exists ["a"] {290 ^bb0(%arg2: !smt.bool):291 smt.yield %arg2 : !smt.bool292 } patterns {293 ^bb0(%arg2: !smt.bool):294 smt.yield295 }296 return297}298 299// -----300 301func.func @forall_patterns_region_at_least_one_yielded_value() {302 // expected-error @below {{'patterns' region #0 must have at least one yielded value}}303 %1 = smt.forall ["a"] {304 ^bb0(%arg2: !smt.bool):305 smt.yield %arg2 : !smt.bool306 } patterns {307 ^bb0(%arg2: !smt.bool):308 smt.yield309 }310 return311}312 313// -----314 315func.func @exists_all_pattern_regions_tested() {316 // expected-error @below {{'patterns' region #1 must have at least one yielded value}}317 %1 = smt.exists ["a"] {318 ^bb0(%arg2: !smt.bool):319 smt.yield %arg2 : !smt.bool320 } patterns {321 ^bb0(%arg2: !smt.bool):322 smt.yield %arg2 : !smt.bool323 }, {324 ^bb0(%arg2: !smt.bool):325 smt.yield326 }327 return328}329 330// -----331 332func.func @forall_all_pattern_regions_tested() {333 // expected-error @below {{'patterns' region #1 must have at least one yielded value}}334 %1 = smt.forall ["a"] {335 ^bb0(%arg2: !smt.bool):336 smt.yield %arg2 : !smt.bool337 } patterns {338 ^bb0(%arg2: !smt.bool):339 smt.yield %arg2 : !smt.bool340 }, {341 ^bb0(%arg2: !smt.bool):342 smt.yield343 }344 return345}346 347// -----348 349func.func @exists_patterns_region_no_non_smt_operations() {350 // expected-error @below {{'patterns' region #0 may only contain SMT dialect operations}}351 %1 = smt.exists ["a"] {352 ^bb0(%arg2: !smt.bool):353 smt.yield %arg2 : !smt.bool354 } patterns {355 ^bb0(%arg2: !smt.bool):356 // expected-note @below {{first non-SMT operation here}}357 arith.constant 0 : i32358 smt.yield %arg2 : !smt.bool359 }360 return361}362 363// -----364 365func.func @forall_patterns_region_no_non_smt_operations() {366 // expected-error @below {{'patterns' region #0 may only contain SMT dialect operations}}367 %1 = smt.forall ["a"] {368 ^bb0(%arg2: !smt.bool):369 smt.yield %arg2 : !smt.bool370 } patterns {371 ^bb0(%arg2: !smt.bool):372 // expected-note @below {{first non-SMT operation here}}373 arith.constant 0 : i32374 smt.yield %arg2 : !smt.bool375 }376 return377}378 379// -----380 381func.func @exists_patterns_region_no_var_binding_operations() {382 // expected-error @below {{'patterns' region #0 must not contain any variable binding operations}}383 %1 = smt.exists ["a"] {384 ^bb0(%arg2: !smt.bool):385 smt.yield %arg2 : !smt.bool386 } patterns {387 ^bb0(%arg2: !smt.bool):388 // expected-note @below {{first violating operation here}}389 smt.exists ["b"] {390 ^bb0(%arg3: !smt.bool):391 smt.yield %arg3 : !smt.bool392 }393 smt.yield %arg2 : !smt.bool394 }395 return396}397 398// -----399 400func.func @forall_patterns_region_no_var_binding_operations() {401 // expected-error @below {{'patterns' region #0 must not contain any variable binding operations}}402 %1 = smt.forall ["a"] {403 ^bb0(%arg2: !smt.bool):404 smt.yield %arg2 : !smt.bool405 } patterns {406 ^bb0(%arg2: !smt.bool):407 // expected-note @below {{first violating operation here}}408 smt.forall ["b"] {409 ^bb0(%arg3: !smt.bool):410 smt.yield %arg3 : !smt.bool411 }412 smt.yield %arg2 : !smt.bool413 }414 return415}416 417// -----418 419func.func @exists_bound_variable_type_invalid() {420 // expected-error @below {{bound variables must by any non-function SMT value}}421 %1 = smt.exists ["a", "b"] {422 ^bb0(%arg2: !smt.func<(!smt.int) !smt.int>, %arg3: !smt.bool):423 smt.yield %arg3 : !smt.bool424 }425 return426}427 428// -----429 430func.func @forall_bound_variable_type_invalid() {431 // expected-error @below {{bound variables must by any non-function SMT value}}432 %1 = smt.forall ["a", "b"] {433 ^bb0(%arg2: !smt.func<(!smt.int) !smt.int>, %arg3: !smt.bool):434 smt.yield %arg3 : !smt.bool435 }436 return437}438 439// -----440 441// expected-error @below {{domain types must be any non-function SMT type}}442func.func @func_domain_no_smt_type(%arg0: !smt.func<(i32) !smt.bool>) {443 return444}445 446// -----447 448// expected-error @below {{range type must be any non-function SMT type}}449func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) i32>) {450 return451}452 453// -----454 455// expected-error @below {{range type must be any non-function SMT type}}456func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) !smt.func<(!smt.bool) !smt.bool>>) {457 return458}459 460// -----461 462func.func @func_range_no_smt_type(%arg0: !smt.func<(!smt.bool) !smt.bool>) {463 // expected-error @below {{got 0 operands and 1 types}}464 smt.apply_func %arg0() : !smt.func<(!smt.bool) !smt.bool>465 return466}467 468// -----469 470// expected-error @below {{sort parameter types must be any non-function SMT type}}471func.func @sort_type_no_smt_type(%arg0: !smt.sort<"sortname"[i32]>) {472 return473}474 475// -----476 477func.func @negative_push() {478 // expected-error @below {{smt.push' op attribute 'count' failed to satisfy constraint: 32-bit signless integer attribute whose value is non-negative}}479 smt.push -1480 return481}482 483// -----484 485func.func @negative_pop() {486 // expected-error @below {{smt.pop' op attribute 'count' failed to satisfy constraint: 32-bit signless integer attribute whose value is non-negative}}487 smt.pop -1488 return489}490 491// -----492 493func.func @set_logic_outside_solver() {494 // expected-error @below {{'smt.set_logic' op expects parent op 'smt.solver'}}495 smt.set_logic "AUFLIA"496 return497}498