smt-libv2.gen 4.45 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
*)

filename "%f-%t-%g.smt2"
20 21
unknown "^\\(unknown\\|sat\\|Fail\\)$" "\\1"
unknown "^(:reason-unknown \\([^)]*\\))$" "\\1"
22
time "why3cpulimit time : %s s"
23
valid "^unsat$"
24 25 26 27 28

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
  syntax predicate (=)  "(= %1 %2)"
29

30
  meta "encoding:kept" type int
31
  meta "encoding:ignore_polymorphism_ls" predicate (=)
32 33 34 35
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
  syntax function (-_) "(- %1)"

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

51 52 53 54 55 56 57
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
58 59
  remove prop Mul_distr_l
  remove prop Mul_distr_r
60
  remove prop Comm
61 62 63 64 65 66 67 68 69 70 71 72 73
  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
  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)"

91 92 93 94 95 96 97
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
98 99
  remove prop Mul_distr_l
  remove prop Mul_distr_r
100
  remove prop Comm
101 102 103 104 105 106 107 108 109 110
  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

111
  meta "encoding:kept" type real
112 113 114

end

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
theory real.Abs
  syntax function abs "(ite (>= %1 0.0) %1 (- %1))"

  remove allprops
end

theory real.MinMax
  syntax function min "(ite (< %1 %2) %1 %2)"
  syntax function max "(ite (< %1 %2) %2 %1)"

  remove allprops
end

theory real.FromInt
  syntax function from_int "(to_real %1)"

  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

144
theory Bool
145 146 147 148 149
  syntax type     bool  "Bool"
  syntax function True  "true"
  syntax function False "false"

  meta "encoding:kept" type bool
150 151 152
end

theory bool.Bool
153 154 155 156 157
  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)"
158 159 160 161
end

theory bool.Ite
  syntax function ite "(ite %1 %2 %3)"
162
  meta "encoding:lskept" function ite
163
  meta "encoding:ignore_polymorphism_ls" function ite
164 165
end

166
(* not uniformly interpreted by provers
167 168 169 170 171 172 173
theory real.Truncate
  syntax function floor "(to_int %1)"
  remove prop Floor_down
  remove prop Floor_monotonic
end
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
174 175 176
theory HighOrd
  syntax type     (->) "(Array %1 %2)"
  syntax function (@)  "(select %1 %2)"
177

178
  meta "encoding:lskept" function (@)
179
  meta "encoding:ignore_polymorphism_ts" type (->)
180
  meta "encoding:ignore_polymorphism_ls" function (@)
Andrei Paskevich's avatar
Andrei Paskevich committed
181 182
end

183
theory map.Map
184 185
  syntax function get "(select %1 %2)"
  syntax function set "(store %1 %2 %3)"
186

187 188
  meta "encoding:lskept" function get
  meta "encoding:lskept" function set
189 190 191 192
  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 ([<-])
MARCHE Claude's avatar
MARCHE Claude committed
193
end
194

MARCHE Claude's avatar
MARCHE Claude committed
195
theory map.Const
196
  meta "encoding:lskept" function const
197 198
(*  syntax function const "(const[%t0] %1)" *)
end