blob: 691b4380da4d9b109203c06f409b81b2ca87f3cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics
smt.solver () : () -> () {
%0 = smt.constant true
// expected-error @below {{must not have any result values}}
%1 = smt.check sat {
smt.yield %0 : !smt.bool
} unknown {
smt.yield %0 : !smt.bool
} unsat {
smt.yield %0 : !smt.bool
} -> !smt.bool
}
// -----
smt.solver () : () -> () {
// expected-error @below {{'sat' region must be empty}}
smt.check sat {
%0 = smt.constant true
smt.yield
} unknown {
} unsat {
}
}
// -----
smt.solver () : () -> () {
// expected-error @below {{'unknown' region must be empty}}
smt.check sat {
} unknown {
%0 = smt.constant true
smt.yield
} unsat {
}
}
// -----
smt.solver () : () -> () {
// expected-error @below {{'unsat' region must be empty}}
smt.check sat {
} unknown {
} unsat {
%0 = smt.constant true
smt.yield
}
}
// -----
// expected-error @below {{solver scopes with inputs or results are not supported}}
%0 = smt.solver () : () -> (i1) {
%1 = arith.constant true
smt.yield %1 : i1
}
// -----
smt.solver () : () -> () {
// expected-error @below {{solver must not contain any non-SMT operations}}
%1 = arith.constant true
}
// -----
func.func @solver_input(%arg0: i1) {
// expected-error @below {{solver scopes with inputs or results are not supported}}
smt.solver (%arg0) : (i1) -> () {
^bb0(%arg1: i1):
smt.yield
}
return
}
// -----
smt.solver () : () -> () {
%0 = smt.declare_fun : !smt.sort<"uninterpreted0">
// expected-error @below {{uninterpreted sorts with same identifier but different arity found}}
%1 = smt.declare_fun : !smt.sort<"uninterpreted0"[!smt.bool]>
}
|
