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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
(** Why3 driver for dreal 21.4.06.2* *)
prelude ";; produced by dreal.drv ;;"
printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "delta-sat with delta = .*" ""
time "why3cpulimit time : %s s"
valid "^unsat$"
(* 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_definition"
transformation "eliminate_builtin"
transformation "eliminate_inductive"
transformation "eliminate_epsilon"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_smt"
transformation "simplify_computations"
transformation "introduce_premises"
transformation "instantiate_predicate"
transformation "keep_only_arithmetic"
transformation "abstract_unknown_lsymbols"
transformation "eliminate_unknown_lsymbols"
transformation "eliminate_unknown_types"
transformation "eliminate_big_constants"
prelude "(set-logic QF_NRA)"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:kept" type int
meta "encoding:ignore_polymorphism_ls" predicate (=)
end
theory int.Int
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove allprops
end
theory int.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.Real
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1.0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove allprops
meta "encoding:kept" type real
end
theory real.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.MinMax
syntax function min "(min %1 %2)"
syntax function max "(max %1 %2)"
remove allprops
end
theory real.FromInt
remove allprops
end
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0) \
(to_int %1) \
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- (to_int (- %1)))"
remove allprops
end
theory real.Square
syntax function sqrt "(sqrt %1)"
syntax function sqr "(pow %1 2)"
remove allprops
end
theory real.ExpLog
syntax function exp "(exp %1)"
syntax function log "(log %1)"
remove allprops
end
theory real.PowerReal
syntax function pow "(^ %1 %2)"
remove allprops
end
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_neg
remove prop Sin_neg
remove prop Cos_sum
remove prop Sin_sum
remove prop Tan_atan
end
theory real.Hyperbolic
syntax function cosh "(cosh %1)"
syntax function sinh "(sinh %1)"
syntax function tanh "(tanh %1)"
end
theory ieee_float.GenericFloat
remove allprops
end
|
