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
|
(** Why3 driver for Z3 >= 4.3.2 *)
(* Do not set any logic, let z3 choose by itself
prelude "(set-logic AUFNIRA)"
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.gen"
filename "%f-%t-%g.smt2"
printer "smtv2"
import "smt-libv2-bv.gen"
import "z3_bv.gen"
import "smt-libv2-floats.gen"
import "discrimination.gen"
(* 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"
import "common-transformations.gen"
transformation "detect_polymorphism"
transformation "eliminate_definition_conditionally"
transformation "eliminate_inductive"
transformation "eliminate_epsilon"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")"
outofmemory "Failed to verify: pthread_create"
outofmemory "std::bad_alloc"
outofmemory "Resource temporarily unavailable"
outofmemory "Cannot allocate memory"
(* not convenient: is more a problem of fork
outofmemory "error while loading shared libraries:.*failed to map segment from shared object"
*)
timeout "^timeout$"
timeout "interrupted by timeout"
steps ":rlimit-count +\\([0-9]+\\)" 1
steplimitexceeded "Maximal allocation counts [0-9]+ have been exceeded"
(** Z3 needs "(push)" to provide models *)
theory BuiltIn
meta "counterexample_need_smtlib_push" ""
end
(** Extra theories supported by Z3 *)
(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory int.MinMax
remove allprops
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
(* does not work: Z3 segfaults
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function pi "pi"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
end
*)
theory ieee_float.Float64
(* check the sign bit; if pos |%1| else |%1| - 2^1025 *)
syntax function to_int
"(ite (= ((_ extract 1024 1024) ((_ fp.to_sbv 1025) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 1025) %1 %2)) (- (bv2int ((_ fp.to_sbv 1025) %1 %2)) (bv2int (bvshl (_ bv1 1026) (_ bv1025 1026)))))"
(* we do not define of_int since z3 will not prove anything if it
appears (05/01/2017) *)
end
theory ieee_float.Float32
(* check the sign bit; if pos |%1| else |%1| - 2^129 *)
syntax function to_int
"(ite (= ((_ extract 128 128) ((_ fp.to_sbv 129) %1 %2)) #b0) (bv2int ((_ fp.to_sbv 129) %1 %2)) (- (bv2int ((_ fp.to_sbv 129) %1 %2)) (bv2int (bvshl (_ bv1 130) (_ bv129 130)))))"
end
theory real.Square
remove allprops
end
|
