Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
08e10dd9
Commit
08e10dd9
authored
Feb 18, 2015
by
MARCHE Claude
Browse files
Fix stmv2 printer for algebraic data types: CVC4 requires a strict syntax
parent
b62e0ffd
Changes
5
Hide whitespace changes
Inline
Side-by-side
drivers/cvc4_bare.drv
View file @
08e10dd9
prelude "(set-logic ALL_SUPPORTED)"
(*
prelude "(set-logic AUFNIRA)" (* how come bv is supported by cvc4 in this logic ?!? *)
*)
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
...
...
drivers/smt-libv2.drv
View file @
08e10dd9
...
...
@@ -24,7 +24,7 @@ transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_algebraic
_if_poly
"
transformation "eliminate_epsilon"
transformation "simplify_formula"
...
...
examples/logic/genealogy/why3session.xml
View file @
08e10dd9
...
...
@@ -2,187 +2,187 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"C
oq
"
version=
"
8.4pl4
"
timelimit=
"
5
"
memlimit=
"
4
000"
/>
<prover
id=
"1"
name=
"C
VC4
"
version=
"
1.2
"
timelimit=
"
60
"
memlimit=
"
1
000"
/>
<prover
id=
"2"
name=
"
Alt-Ergo
"
version=
"
0.95.1
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"0"
name=
"C
VC4
"
version=
"
1.2
"
timelimit=
"
60
"
memlimit=
"
1
000"
/>
<prover
id=
"1"
name=
"C
oq
"
version=
"
8.4pl4
"
timelimit=
"
5
"
memlimit=
"
4
000"
/>
<prover
id=
"2"
name=
"
Eprover
"
version=
"
1.6
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"3"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"4"
name=
"
Eprover
"
version=
"
1.6
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"5"
name=
"
Z3
"
version=
"
2.19
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"6"
name=
"
CVC4
"
version=
"
1.4
"
timelimit=
"
3
"
memlimit=
"
100
0"
/>
<prover
id=
"7"
name=
"
CVC
3"
version=
"
2.2
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"8"
name=
"
Eprover
"
version=
"
1.4
"
timelimit=
"
3
"
memlimit=
"
100
0"
/>
<prover
id=
"9"
name=
"
Spass
"
version=
"
3.7
"
timelimit=
"
5
"
memlimit=
"0"
/>
<prover
id=
"10"
name=
"
Z
3"
version=
"
4.3.1
"
timelimit=
"5"
memlimit=
"
400
0"
/>
<prover
id=
"4"
name=
"
Alt-Ergo
"
version=
"
0.95.1
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"5"
name=
"
CVC4
"
version=
"
1.4
"
timelimit=
"5"
memlimit=
"
100
0"
/>
<prover
id=
"6"
name=
"
Z3
"
version=
"
2.19
"
timelimit=
"
5
"
memlimit=
"0"
/>
<prover
id=
"7"
name=
"
Z
3"
version=
"
4.3.1
"
timelimit=
"5"
memlimit=
"
400
0"
/>
<prover
id=
"8"
name=
"
Spass
"
version=
"
3.7
"
timelimit=
"
5
"
memlimit=
"0"
/>
<prover
id=
"9"
name=
"
Eprover
"
version=
"
1.4
"
timelimit=
"
3
"
memlimit=
"
100
0"
/>
<prover
id=
"10"
name=
"
CVC
3"
version=
"
2.2
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"11"
name=
"Simplify"
version=
"1.5.4"
timelimit=
"3"
memlimit=
"1000"
/>
<prover
id=
"12"
name=
"
Yices
"
version=
"
1.0.38
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"12"
name=
"
Isabelle
"
version=
"
2014
"
timelimit=
"5"
memlimit=
"
400
0"
/>
<prover
id=
"13"
name=
"Zenon"
version=
"0.7.1"
timelimit=
"5"
memlimit=
"4000"
/>
<prover
id=
"14"
name=
"
Isabelle
"
version=
"
2014
"
timelimit=
"5"
memlimit=
"
400
0"
/>
<prover
id=
"15"
name=
"
Metis
"
version=
"
2.3
"
timelimit=
"5"
memlimit=
"
100
0"
/>
<prover
id=
"16"
name=
"
Z3
"
version=
"
3.2
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"14"
name=
"
Yices
"
version=
"
1.0.38
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"15"
name=
"
Z3
"
version=
"
3.2
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"16"
name=
"
Metis
"
version=
"
2.3
"
timelimit=
"5"
memlimit=
"
100
0"
/>
<prover
id=
"17"
name=
"Z3"
version=
"4.3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"18"
name=
"
Alt-Ergo
"
version=
"
0.95.2
"
timelimit=
"
60
"
memlimit=
"
1
000"
/>
<prover
id=
"18"
name=
"
veriT
"
version=
"
201310
"
timelimit=
"
5
"
memlimit=
"
4
000"
/>
<prover
id=
"19"
name=
"PVS"
version=
"6.0"
timelimit=
"5"
memlimit=
"4000"
/>
<prover
id=
"20"
name=
"
veriT
"
version=
"
201310
"
timelimit=
"
5
"
memlimit=
"
4
000"
/>
<prover
id=
"20"
name=
"
Alt-Ergo
"
version=
"
0.95.2
"
timelimit=
"
60
"
memlimit=
"
1
000"
/>
<prover
id=
"21"
name=
"CVC4"
version=
"1.3"
timelimit=
"3"
memlimit=
"1000"
/>
<prover
id=
"22"
name=
"Vampire"
version=
"0.6"
timelimit=
"3"
memlimit=
"1000"
/>
<file
name=
"../genealogy.why"
expanded=
"true"
>
<theory
name=
"Genealogy"
sum=
"35e1439432a79e05534b2c5cf39ad9dc"
expanded=
"true"
>
<goal
name=
"Child_is_son_or_daughter"
expanded=
"true"
>
<proof
prover=
"0"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.v"
><result
status=
"
valid
"
time=
"
1.58
"
/></proof>
<proof
prover=
"1"
><result
status=
"
unknown
"
time=
"
0.00
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.0
1"
steps=
"12
"
/></proof>
<proof
prover=
"0"
><result
status=
"
unknown
"
time=
"
0.00
"
/></proof>
<proof
prover=
"1"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.v"
><result
status=
"
valid
"
time=
"
1.58
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"6"
><result
status=
"
unknown
"
time=
"0.0
0
"
/></proof>
<proof
prover=
"7"
><result
status=
"
valid
"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"10"
><result
status=
"
unknown
"
time=
"
2.28
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
1"
steps=
"12
"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"6"
><result
status=
"
valid
"
time=
"0.0
1
"
/></proof>
<proof
prover=
"7"
memlimit=
"1000"
><result
status=
"
unknown
"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"10"
><result
status=
"
valid
"
time=
"
0.00
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"
unknown
"
time=
"
0.01
"
/></proof>
<proof
prover=
"12"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
><result
status=
"
valid
"
time=
"
7.22
"
/></proof>
<proof
prover=
"13"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.xml"
><result
status=
"
valid
"
time=
"
7.22
"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"14"
><result
status=
"
unknown
"
time=
"
0.01
"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
1"
steps=
"12
"
/></proof>
<proof
prover=
"18"
timelimit=
"60"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"19"
edited=
"genealogy_Genealogy_Child_is_son_or_daughter_1.pvs"
><result
status=
"valid"
time=
"0.24"
/></proof>
<proof
prover=
"20"
timelimit=
"60"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
1"
steps=
"12
"
/></proof>
<proof
prover=
"21"
><result
status=
"unknown"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Sibling_sym"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.00"
steps=
"5"
/></proof>
<proof
prover=
"
0
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
steps=
"5"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"
0.0
0"
/></proof>
<proof
prover=
"12"
edited=
"genealogy_Genealogy_Sibling_sym_1.xml"
><result
status=
"valid"
time=
"
6.9
0"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.23"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Sibling_sym_1.xml"
><result
status=
"valid"
time=
"
6.9
0"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.1
2
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.
0
1"
/></proof>
<proof
prover=
"14"
><result
status=
"valid"
time=
"
0.0
0"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.
0
1"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.1
2
"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
2"
steps=
"5
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
2"
steps=
"5
"
/></proof>
<proof
prover=
"21"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Sibling_is_brother_or_sister"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"unknown"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.00"
steps=
"9"
/></proof>
<proof
prover=
"
0
"
><result
status=
"unknown"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"6"
><result
status=
"
unknown
"
time=
"0.0
0
"
/></proof>
<proof
prover=
"7"
><result
status=
"
valid
"
time=
"
0.00
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.00"
steps=
"9"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"6"
><result
status=
"
valid
"
time=
"0.0
1
"
/></proof>
<proof
prover=
"7"
><result
status=
"
unknown
"
time=
"
2.25
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"10"
><result
status=
"
unknown
"
time=
"
2.25
"
/></proof>
<proof
prover=
"10"
><result
status=
"
valid
"
time=
"
0.00
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"
unknown
"
time=
"
0.02
"
/></proof>
<proof
prover=
"12"
edited=
"genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"
><result
status=
"
valid
"
time=
"
7.50
"
/></proof>
<proof
prover=
"13"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"
><result
status=
"
valid
"
time=
"
7.50
"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.0
4
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"14"
><result
status=
"
unknown
"
time=
"
0.02
"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.0
4
"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
2"
steps=
"9
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
2"
steps=
"9
"
/></proof>
<proof
prover=
"21"
><result
status=
"unknown"
time=
"0.01"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Grandparent_is_grandfather_or_grandmother"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
steps=
"32"
/></proof>
<proof
prover=
"
0
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
8
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"32"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"
9
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"
0.04
"
/></proof>
<proof
prover=
"12"
edited=
"genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
><result
status=
"valid"
time=
"
7.57
"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.26"
/></proof>
<proof
prover=
"14"
edited=
"genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"
><result
status=
"valid"
time=
"
7.57
"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.0
7
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"14"
><result
status=
"valid"
time=
"
0.04
"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.0
7
"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
2"
steps=
"32
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
2"
steps=
"32
"
/></proof>
<proof
prover=
"21"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"Grandfather_male"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.0
1"
steps=
"6
"
/></proof>
<proof
prover=
"
0
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
1"
steps=
"6
"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.77"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"14"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
1"
steps=
"6
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
1"
steps=
"6
"
/></proof>
<proof
prover=
"21"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"Grandmother_female"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.0
1"
steps=
"5
"
/></proof>
<proof
prover=
"
0
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.0
1"
steps=
"5
"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.27"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"14"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
1"
steps=
"5
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
1"
steps=
"5
"
/></proof>
<proof
prover=
"21"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"Only_two_grandfathers"
expanded=
"true"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
<proof
prover=
"
0
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.0
3
"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.0
2
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"11"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"12"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"13"
><result
status=
"timeout"
time=
"5.99"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"14"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"15"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"16"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"17"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.0
1"
steps=
"1
0"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"18"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"20"
><result
status=
"valid"
time=
"0.0
1"
steps=
"1
0"
/></proof>
<proof
prover=
"21"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"22"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
...
...
src/printer/smtv2.ml
View file @
08e10dd9
...
...
@@ -256,11 +256,20 @@ let print_prop_decl info fmt k pr f = match k with
let
print_constructor_decl
info
fmt
(
ls
,
args
)
=
match
args
with
|
[]
->
print_ident
fmt
ls
.
ls_name
|
[]
->
fprintf
fmt
"(%a)"
print_ident
ls
.
ls_name
|
_
->
fprintf
fmt
"@[(%a@ %a)@]"
print_ident
ls
.
ls_name
(
print_list
space
(
print_type
info
))
ls
.
ls_args
fprintf
fmt
"@[(%a@ "
print_ident
ls
.
ls_name
;
let
_
=
List
.
fold_left2
(
fun
i
ty
pr
->
begin
match
pr
with
|
Some
pr
->
fprintf
fmt
"(%a"
print_ident
pr
.
ls_name
|
None
->
fprintf
fmt
"(%a_proj_%d"
print_ident
ls
.
ls_name
i
end
;
fprintf
fmt
" %a)"
(
print_type
info
)
ty
;
succ
i
)
1
ls
.
ls_args
args
in
fprintf
fmt
")@]"
let
print_data_decl
info
fmt
(
ts
,
cl
)
=
fprintf
fmt
"@[(%a@ %a)@]"
...
...
src/transform/eliminate_algebraic.ml
View file @
08e10dd9
...
...
@@ -493,3 +493,17 @@ let () =
~
desc
:
"Replace@ algebraic@ data@ types@ by@ first-order@ definitions."
;
Trans
.
register_transform
"eliminate_projections"
eliminate_projections
~
desc
:
"Define@ algebraic@ projection@ symbols@ separately."
(** conditional transformations, only applied when polymorphic types occur *)
let
eliminate_algebraic_if_poly
=
Trans
.
on_meta
Detect_polymorphism
.
meta_monomorphic_types_only
(
function
|
[]
->
eliminate_algebraic
|
_
->
Trans
.
identity
)
let
()
=
Trans
.
register_transform
"eliminate_algebraic_if_poly"
eliminate_algebraic_if_poly
~
desc
:
"Same@ as@ eliminate_algebraic@ but@ only@ if@ polymorphism@ appear."
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment