why3session.dtd 1.86 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>
11
<!ATTLIST prover steplimit CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
12

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

MARCHE Claude's avatar
MARCHE Claude committed
18
<!ELEMENT theory (label*,goal*)>
MARCHE Claude's avatar
MARCHE Claude committed
19
<!ATTLIST theory name CDATA #REQUIRED>
20
<!ATTLIST theory verified CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
21
<!ATTLIST theory proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
22

MARCHE Claude's avatar
MARCHE Claude committed
23
<!ELEMENT goal (label*, proof*, transf*)>
MARCHE Claude's avatar
MARCHE Claude committed
24 25
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
26
<!ATTLIST goal sum CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
27
<!ATTLIST goal shape CDATA #IMPLIED>
28
<!ATTLIST goal proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
29

30
<!ELEMENT proof (result|undone|internalfailure|unedited)>
MARCHE Claude's avatar
MARCHE Claude committed
31
<!ATTLIST proof prover CDATA #REQUIRED>
32 33
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
34
<!ATTLIST proof steplimit CDATA #IMPLIED>
35 36
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
37 38

<!ELEMENT result EMPTY>
39
<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|steplimitexceeded|failure|highfailure) #REQUIRED>
MARCHE Claude's avatar
MARCHE Claude committed
40
<!ATTLIST result time CDATA #IMPLIED>
41
<!ATTLIST result steps CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
42

43
<!ELEMENT undone EMPTY>
44
<!ELEMENT unedited EMPTY>
45

46 47 48
<!ELEMENT internalfailure EMPTY>
<!ATTLIST internalfailure reason CDATA #REQUIRED>

MARCHE Claude's avatar
MARCHE Claude committed
49 50
<!ELEMENT transf (goal*)>
<!ATTLIST transf name CDATA #REQUIRED>
51
<!ATTLIST transf proved CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
52 53 54 55
<!ATTLIST transf arg1 CDATA #IMPLIED>
<!ATTLIST transf arg2 CDATA #IMPLIED>
<!ATTLIST transf arg3 CDATA #IMPLIED>
<!ATTLIST transf arg4 CDATA #IMPLIED>
MARCHE Claude's avatar
MARCHE Claude committed
56 57 58

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