drivers/smt-libv2.gen

   1 (* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
   2
   3 prelude ";;; generated by SMT-LIB2 driver"
   4
   5 (*
   6
   7 Note: we do not insert any command "set-logic" because its
   8 interpretation is specific to provers
   9
  10 prelude "(set-logic AUFNIRA)"
  11
  12     A  : Array
  13     UF : Uninterpreted Function
  14     DT : Datatypes (not needed at the end ...)
  15     NIRA : NonLinear Integer Reals Arithmetic
  16
  17 *)
  18
  19 (* cannot be here because case of psmt2 files: filename "%f-%t-%g.smt2" *)
  20
  21 unknown "^\\(unknown\\|sat\\|Fail\\)$" "\\1"
  22 unknown "^(:reason-unknown \\([^)]*\\))$" "\\1"
  23 time "why3cpulimit time : %s s"
  24 valid "^unsat$"
  25
  26 theory BuiltIn
  27   syntax type int   "Int"
  28   syntax type real  "Real"
  29   syntax predicate (=)  "(= %1 %2)"
  30
  31   meta "encoding:kept" type int
  32   meta "encoding:ignore_polymorphism_ls" predicate (=)
  33 end
  34
  35 theory Ignore
  36   syntax predicate ignore'term  "true"
  37   meta "encoding:ignore_polymorphism_ls" predicate ignore'term
  38 end
  39
  40 theory int.Int
  41
  42   prelude ";;; SMT-LIB2: integer arithmetic"
  43
  44   syntax function zero "0"
  45   syntax function one  "1"
  46
  47   syntax function (+)  "(+ %1 %2)"
  48   syntax function (-)  "(- %1 %2)"
  49   syntax function (*)  "(* %1 %2)"
  50   syntax function (-_) "(- %1)"
  51
  52   syntax predicate (<=) "(<= %1 %2)"
  53   syntax predicate (<)  "(< %1 %2)"
  54   syntax predicate (>=) "(>= %1 %2)"
  55   syntax predicate (>)  "(> %1 %2)"
  56
  57   remove prop MulComm.Comm
  58   remove prop MulAssoc.Assoc
  59   remove prop Unit_def_l
  60   remove prop Unit_def_r
  61   remove prop Inv_def_l
  62   remove prop Inv_def_r
  63   remove prop Assoc
  64   remove prop Mul_distr_l
  65   remove prop Mul_distr_r
  66   remove prop Comm
  67   remove prop Unitary
  68   remove prop Refl
  69   remove prop Trans
  70   remove prop Antisymm
  71   remove prop Total
  72   remove prop NonTrivialRing
  73   remove prop CompatOrderAdd
  74   remove prop ZeroLessOne
  75
  76 end
  77
  78 theory real.Real
  79
  80   prelude ";;; SMT-LIB2: real arithmetic"
  81
  82   syntax function zero "0.0"
  83   syntax function one  "1.0"
  84
  85   syntax function (+)  "(+ %1 %2)"
  86   syntax function (-)  "(- %1 %2)"
  87   syntax function (*)  "(* %1 %2)"
  88   syntax function (/)  "(/ %1 %2)"
  89   syntax function (-_) "(- %1)"
  90   syntax function inv  "(/ 1.0 %1)"
  91
  92   syntax predicate (<=) "(<= %1 %2)"
  93   syntax predicate (<)  "(< %1 %2)"
  94   syntax predicate (>=) "(>= %1 %2)"
  95   syntax predicate (>)  "(> %1 %2)"
  96
  97   remove prop MulComm.Comm
  98   remove prop MulAssoc.Assoc
  99   remove prop Unit_def_l
 100   remove prop Unit_def_r
 101   remove prop Inv_def_l
 102   remove prop Inv_def_r
 103   remove prop Assoc
 104   remove prop Mul_distr_l
 105   remove prop Mul_distr_r
 106   remove prop Comm
 107   remove prop Unitary
 108   remove prop Inverse
 109   remove prop Refl
 110   remove prop Trans
 111   remove prop Antisymm
 112   remove prop Total
 113   remove prop NonTrivialRing
 114   remove prop CompatOrderAdd
 115   remove prop ZeroLessOne
 116
 117   meta "encoding:kept" type real
 118
 119 end
 120
 121 theory real.Abs
 122   syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
 123
 124   remove allprops
 125 end
 126
 127 theory real.MinMax
 128
 129   remove allprops
 130 end
 131
 132 theory real.FromInt
 133   syntax function from_int "(to_real %1)"
 134
 135   remove allprops
 136 end
 137
 138 theory real.Truncate
 139   syntax function truncate "(ite (>= %1 0.0) \
 140                                  (to_int %1) \
 141                                  (- (to_int (- %1))))"
 142   syntax function floor "(to_int %1)"
 143   syntax function ceil "(- (to_int (- %1)))"
 144
 145   remove allprops
 146 end
 147
 148 theory Bool
 149   syntax type     bool  "Bool"
 150   syntax function True  "true"
 151   syntax function False "false"
 152
 153   meta "algebraic:kept" type bool
 154 end
 155
 156 theory bool.Bool
 157   syntax function andb  "(and %1 %2)"
 158   syntax function orb   "(or %1 %2)"
 159   syntax function xorb  "(xor %1 %2)"
 160   syntax function notb  "(not %1)"
 161   syntax function implb "(=> %1 %2)"
 162 end
 163
 164 theory bool.Ite
 165   syntax function ite "(ite %1 %2 %3)"
 166   meta "encoding:lskept" function ite
 167   meta "encoding:ignore_polymorphism_ls" function ite
 168 end
 169
 170 (* not uniformly interpreted by provers
 171 theory real.Truncate
 172   syntax function floor "(to_int %1)"
 173   remove prop Floor_down
 174   remove prop Floor_monotonic
 175 end
 176 *)
 177
 178 theory HighOrd
 179   syntax type     (->) "(Array %1 %2)"
 180   syntax function (@)  "(select %1 %2)"
 181
 182   meta "encoding:lskept" function (@)
 183   meta "encoding:ignore_polymorphism_ts" type (->)
 184   meta "encoding:ignore_polymorphism_ls" function (@)
 185 end
 186
 187
 188 theory bv.BV_Gen
 189
 190   (* removing well-founded properties, they cannot be useful
 191      for SMT solvers, and they imply polymorphism *)
 192   remove prop ult_wf
 193   remove prop ugt_wf
 194   remove prop slt_wf
 195   remove prop sgt_wf
 196
 197 end
 198
 199
 200 theory map.Map
 201   syntax function get "(select %1 %2)"
 202   syntax function set "(store %1 %2 %3)"
 203
 204   meta "encoding:lskept" function get
 205   meta "encoding:lskept" function set
 206   meta "encoding:ignore_polymorphism_ls" function get
 207   meta "encoding:ignore_polymorphism_ls" function ([])
 208   meta "encoding:ignore_polymorphism_ls" function set
 209   meta "encoding:ignore_polymorphism_ls" function ([<-])
 210 end
 211
 212 theory map.Const
 213   meta "encoding:lskept" function const
 214 (*  syntax function const "(const[%t0] %1)" *)
 215 end