why3session.dtd 3.46 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
<!ELEMENT why3session (prover*, file*)>
MARCHE Claude's avatar
MARCHE Claude committed
2
<!ATTLIST why3session shape_version CDATA #IMPLIED>
3

MARCHE Claude's avatar
MARCHE Claude committed
4 5 6 7
<!ELEMENT prover EMPTY>
<!ATTLIST prover id CDATA #REQUIRED>
<!ATTLIST prover name CDATA #REQUIRED>
<!ATTLIST prover version CDATA #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
8
<!ATTLIST prover alternative CDATA #IMPLIED>
9 10
<!ATTLIST prover timelimit CDATA #IMPLIED>
<!ATTLIST prover memlimit CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
11

MARCHE Claude's avatar
MARCHE Claude committed
12 13 14
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ATTLIST file verified CDATA #REQUIRED>
15
<!ATTLIST file expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
16

MARCHE Claude's avatar
MARCHE Claude committed
17
<!ELEMENT theory (label*,goal*)>
MARCHE Claude's avatar
MARCHE Claude committed
18 19
<!ATTLIST theory name CDATA #REQUIRED>
<!ATTLIST theory verified CDATA #REQUIRED>
20
<!ATTLIST theory expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24
<!ATTLIST theory locfile CDATA #IMPLIED>
<!ATTLIST theory loclnum CDATA #IMPLIED>
<!ATTLIST theory loccnumb CDATA #IMPLIED>
<!ATTLIST theory loccnume CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
25

26
<!ELEMENT goal (label*, proof*, transf*, metas*)>
MARCHE Claude's avatar
MARCHE Claude committed
27 28 29
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
<!ATTLIST goal proved CDATA #REQUIRED>
30
<!ATTLIST goal sum CDATA #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
31
<!ATTLIST goal shape CDATA #IMPLIED>
32
<!ATTLIST goal expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
33 34 35 36
<!ATTLIST goal locfile CDATA #IMPLIED>
<!ATTLIST goal loclnum CDATA #IMPLIED>
<!ATTLIST goal loccnumb CDATA #IMPLIED>
<!ATTLIST goal loccnume CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
37

38
<!ELEMENT proof (result|undone|internalfailure)>
MARCHE Claude's avatar
MARCHE Claude committed
39
<!ATTLIST proof prover CDATA #REQUIRED>
40 41
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
42 43
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
44
<!ATTLIST proof archived CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
45 46

<!ELEMENT result EMPTY>
47
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|failure|highfailure) #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
48 49
<!ATTLIST result time CDATA #IMPLIED>

50 51
<!ELEMENT undone EMPTY>

52 53 54
<!ELEMENT internalfailure EMPTY>
<!ATTLIST internalfailure reason CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
55 56 57
<!ELEMENT transf (goal*)>
<!ATTLIST transf name CDATA #REQUIRED>
<!ATTLIST transf proved CDATA #REQUIRED>
58
<!ATTLIST transf expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61

<!ELEMENT label EMPTY>
<!ATTLIST label name CDATA #REQUIRED>
62

63
<!ELEMENT metas (ts_pos*,ls_pos*,pr_pos*,meta*,goal)>
64 65 66
<!ATTLIST metas proved CDATA #REQUIRED>
<!ATTLIST metas expanded CDATA #IMPLIED>

Andrei Paskevich's avatar
Andrei Paskevich committed
67
<!ELEMENT ts_pos (ip_library*,ip_qualid+)>
68 69 70
<!ATTLIST ts_pos name CDATA #REQUIRED>
<!ATTLIST ts_pos arity CDATA #REQUIRED>
<!ATTLIST ts_pos id CDATA #REQUIRED>
71
<!ATTLIST ts_pos ip_theory CDATA #REQUIRED>
72

Andrei Paskevich's avatar
Andrei Paskevich committed
73
<!ELEMENT ls_pos (ip_library*,ip_qualid+)>
74 75
<!ATTLIST ls_pos name CDATA #REQUIRED>
<!ATTLIST ls_pos id CDATA #REQUIRED>
76
<!ATTLIST ls_pos ip_theory CDATA #REQUIRED>
77

Andrei Paskevich's avatar
Andrei Paskevich committed
78
<!ELEMENT pr_pos (ip_library*,ip_qualid+)>
79 80
<!ATTLIST pr_pos name CDATA #REQUIRED>
<!ATTLIST pr_pos id CDATA #REQUIRED>
81 82 83 84 85 86 87
<!ATTLIST pr_pos ip_theory CDATA #REQUIRED>

<!ELEMENT ip_library EMPTY>
<!ATTLIST ip_library name CDATA #REQUIRED>

<!ELEMENT ip_qualid EMPTY>
<!ATTLIST ip_qualid name CDATA #REQUIRED>
88

MARCHE Claude's avatar
MARCHE Claude committed
89 90
<!ELEMENT meta (meta_arg_ty*, meta_arg_ts*, meta_arg_ls*,
          meta_arg_pr*, meta_arg_str*, meta_arg_int*)>
91 92 93 94 95 96 97 98 99 100
<!ATTLIST meta name CDATA #REQUIRED>

<!ELEMENT meta_args_ty (ty_var|ty_app)>

<!ELEMENT ty_var EMPTY>
<!ATTLIST ty_var id CDATA #REQUIRED>

<!ELEMENT ty_app (ty_var*,ty_app*)>
<!ATTLIST ty_app id CDATA #REQUIRED>

101 102
<!ELEMENT meta_arg_ts EMPTY>
<!ATTLIST meta_arg_ts id CDATA #REQUIRED>
103

104 105
<!ELEMENT meta_arg_ls EMPTY>
<!ATTLIST meta_arg_ls id CDATA #REQUIRED>
106

107 108
<!ELEMENT meta_arg_pr EMPTY>
<!ATTLIST meta_arg_pr id CDATA #REQUIRED>
109

110 111
<!ELEMENT meta_arg_str EMPTY>
<!ATTLIST meta_arg_str val CDATA #REQUIRED>
112

113 114
<!ELEMENT meta_arg_int EMPTY>
<!ATTLIST meta_arg_int val CDATA #REQUIRED>