why3session.dtd 3.58 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
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
14
<!ATTLIST file expanded CDATA #IMPLIED>
15
<!ATTLIST file verified 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
<!ATTLIST theory name CDATA #REQUIRED>
19
<!ATTLIST theory expanded CDATA #IMPLIED>
20 21
<!ATTLIST theory verified CDATA #IMPLIED>
<!ATTLIST theory sum CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25
<!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
26

27
<!ELEMENT goal (label*, proof*, transf*, metas*)>
MARCHE Claude's avatar
MARCHE Claude committed
28 29
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
30
<!ATTLIST goal sum CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
31
<!ATTLIST goal shape CDATA #IMPLIED>
32
<!ATTLIST goal proved CDATA #IMPLIED>
33
<!ATTLIST goal expanded CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
34 35 36 37
<!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
38

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

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

52
<!ELEMENT undone EMPTY>
53
<!ELEMENT unedited EMPTY>
54

55 56 57
<!ELEMENT internalfailure EMPTY>
<!ATTLIST internalfailure reason CDATA #REQUIRED>

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

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

66
<!ELEMENT metas (ts_pos*,ls_pos*,pr_pos*,meta*,goal)>
67
<!ATTLIST metas expanded CDATA #IMPLIED>
68
<!ATTLIST metas proved CDATA #IMPLIED>
69

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
81
<!ELEMENT pr_pos (ip_library*,ip_qualid+)>
82 83
<!ATTLIST pr_pos name CDATA #REQUIRED>
<!ATTLIST pr_pos id CDATA #REQUIRED>
84 85 86 87 88 89 90
<!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>
91

MARCHE Claude's avatar
MARCHE Claude committed
92 93
<!ELEMENT meta (meta_arg_ty*, meta_arg_ts*, meta_arg_ls*,
          meta_arg_pr*, meta_arg_str*, meta_arg_int*)>
94 95 96 97 98 99 100 101 102 103
<!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>

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

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

110 111
<!ELEMENT meta_arg_pr EMPTY>
<!ATTLIST meta_arg_pr id CDATA #REQUIRED>
112

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

116 117
<!ELEMENT meta_arg_int EMPTY>
<!ATTLIST meta_arg_int val CDATA #REQUIRED>