smt-libv2.drv 4.02 KB
Newer Older
1
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
2

3
4
5
6
7
8
9
10
11
12
prelude ";;; generated by SMT-LIB2 driver"

(*

Note: we do not insert any command "set-logic" because its
interpretation is specific to provers

prelude "(set-logic AUFNIRA)"

    A  : Array
13
14
15
    UF : Uninterpreted Function
    DT : Datatypes (not needed at the end ...)
    NIRA : NonLinear Integer Reals Arithmetic
16

17
18
19
20
*)

printer "smtv2"
filename "%f-%t-%g.smt2"
21
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
22
time "why3cpulimit time : %s s"
23
valid "^unsat$"
24
25
26
27
28
29


theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
  syntax predicate (=)  "(= %1 %2)"
30
  meta "encoding:ignore_polymorphism_ls" predicate (=)
31
32
33
34
35
  meta "encoding : kept" type int
end

theory int.Int

36
  prelude ";;; SMT-LIB2: integer arithmetic"
37
38
39
40
41
42

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
43
  syntax function ( * )  "(* %1 %2)"
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
  syntax function (-_) "(- %1)"

  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
  remove prop Assoc.Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

end

theory real.Real

74
  prelude ";;; SMT-LIB2: real arithmetic"
75
76
77
78
79
80

  syntax function zero "0.0"
  syntax function one  "1.0"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
81
  syntax function ( * )  "(* %1 %2)"
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
  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 prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
  remove prop Assoc.Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Inverse
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

  meta "encoding : kept" type real

end

theory Bool
   syntax type     bool  "Bool"
   syntax function True  "true"
   syntax function False "false"
   meta "encoding : kept" type bool
end

theory bool.Bool
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function xorb  "(xor %1 %2)"
   syntax function notb  "(not %1)"
   syntax function implb "(=> %1 %2)"
end

theory bool.Ite
  syntax function ite "(ite %1 %2 %3)"
  meta "encoding : lskept" function ite
end

135
(* not uniformly interpreted by provers
136
137
138
139
140
141
142
143
144
theory real.Truncate
  syntax function floor "(to_int %1)"
  remove prop Floor_down
  remove prop Floor_monotonic
end
*)

theory map.Map
  syntax type map "(Array %1 %2)"
145
  meta "encoding:ignore_polymorphism_ts" type map
146
147
148

  syntax function get   "(select %1 %2)"
  syntax function set   "(store %1 %2 %3)"
149
150
151
152
153
154
155
156
157
158
159
  meta "encoding : lskept" function get
  meta "encoding : lskept" function set
  meta "encoding:ignore_polymorphism_ls" function get
  meta "encoding:ignore_polymorphism_ls" function ([])
  meta "encoding:ignore_polymorphism_ls" function set
  meta "encoding:ignore_polymorphism_ls" function ([<-])

  meta "encoding:ignore_polymorphism_pr" prop Select_eq
  meta "encoding:ignore_polymorphism_pr" prop Select_neq
  remove prop Select_eq
  remove prop Select_neq
MARCHE Claude's avatar
MARCHE Claude committed
160
161
162
163
end

theory map.Const
  meta "encoding : lskept" function const
164
165
(*  syntax function const "(const[%t0] %1)" *)
end