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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
(* Why3 driver for PolyPaver *)
(* http://michalkonecny.github.io/polypaver/_site/ *)
printer "metitarski"
filename "%f-%t-%g.tptp"
valid 0
invalid 111
timeout "Gave up on deciding conjecture: TIMED OUT"
time "why3cpulimit time : %s s"
unknown 1 "toto"
(* to be improved *)
(* Performed introductions depending on whether counterexamples are
requested, as said by the meta "get_counterexmp". When this meta
set, this transformation introduces the model variables that are
still embedded in the goal. When it is not set, it removes all
these unused-ce-related variables, even in the context. *)
transformation "counterexamples_dependent_intros"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_unknown_lsymbols"
transformation "simplify_trivial_quantification"
transformation "introduce_premises"
transformation "instantiate_predicate"
transformation "abstract_unknown_lsymbols"
transformation "discriminate"
transformation "encoding_tptp"
theory BuiltIn
meta "encoding:base" type real
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
import "discrimination.gen"
theory real.Real
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (-_) "(-%1)"
syntax function ( * ) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function inv "(1/ %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
remove allprops
end
theory real.Abs
syntax function abs "abs(%1)"
remove allprops
end
theory real.Square
syntax function sqr "(%1)^2"
syntax function sqrt "sqrt(%1)"
remove allprops
end
theory real.MinMax
syntax function min "min(%1,%2)"
syntax function max "max(%1,%2)"
remove allprops
end
theory real.ExpLog
syntax function exp "exp(%1)"
syntax function log "ln(%1)"
remove allprops
end
theory real.PowerReal
syntax function pow "pow(%1,%2)"
remove allprops
end
|
