drivers/colibri2.drv

   1 (** Why3 driver for Colibri (with floating point support) *)
   2
   3 prelude ";; produced by local colibri2.drv ;;"
   4 prelude "(set-logic ALL)"
   5 prelude "(set-info :smt-lib-version 2.6)"
   6
   7 filename "%f-%t-%g.psmt2"
   8 unknown "^\\(unknown\\|sat\\|Fail\\)$" "\\1"
   9 unknown "^(:reason-unknown \\([^)]*\\))$" "\\1"
  10 time "why3cpulimit time : %s s"
  11 valid "^unsat$"
  12 steplimitexceeded "steplimitreached"
  13 steps "^(steps \\([0-9]+.?[0-9]*\\))" 1
  14
  15 printer "smtv2.6par"
  16
  17
  18 (* Performed introductions depending on whether counterexamples are
  19    requested, as said by the meta "get_counterexmp". When this meta
  20    set, this transformation introduces the model variables that are
  21    still embedded in the goal. When it is not set, it removes all
  22    these unused-ce-related variables, even in the context.  *)
  23 transformation "counterexamples_dependent_intros"
  24
  25 transformation "monomorphise_goal"
  26 transformation "eliminate_builtin"
  27 transformation "compile_match"
  28 (* transformation "inline_trivial" *)
  29 transformation "simplify_formula"
  30 transformation "eliminate_inductive"
  31 transformation "eliminate_literal"
  32 transformation "eliminate_epsilon"
  33
  34
  35 theory BuiltIn
  36   syntax type int   "Int"
  37   syntax type real  "Real"
  38   syntax predicate (=)  "(= %1 %2)"
  39 end
  40
  41 theory Ignore
  42   syntax predicate ignore'term  "true"
  43 end
  44
  45 theory int.Int
  46
  47   prelude ";;; SMT-LIB2: integer arithmetic"
  48
  49   syntax function zero "0"
  50   syntax function one  "1"
  51
  52   syntax function (+)  "(+ %1 %2)"
  53   syntax function (-)  "(- %1 %2)"
  54   syntax function (*)  "(* %1 %2)"
  55   syntax function (-_) "(- %1)"
  56
  57   syntax predicate (<=) "(<= %1 %2)"
  58   syntax predicate (<)  "(< %1 %2)"
  59   syntax predicate (>=) "(>= %1 %2)"
  60   syntax predicate (>)  "(> %1 %2)"
  61
  62   remove prop MulComm.Comm
  63   remove prop MulAssoc.Assoc
  64   remove prop Unit_def_l
  65   remove prop Unit_def_r
  66   remove prop Inv_def_l
  67   remove prop Inv_def_r
  68   remove prop Assoc
  69   remove prop Mul_distr_l
  70   remove prop Mul_distr_r
  71   remove prop Comm
  72   remove prop Unitary
  73   remove prop Refl
  74   remove prop Trans
  75   remove prop Antisymm
  76   remove prop Total
  77   remove prop NonTrivialRing
  78   remove prop CompatOrderAdd
  79   remove prop CompatOrderMult
  80   remove prop ZeroLessOne
  81
  82 end
  83
  84 theory real.Real
  85
  86   prelude ";;; SMT-LIB2: real arithmetic"
  87
  88   syntax function zero "0.0"
  89   syntax function one  "1.0"
  90
  91   syntax function (+)  "(+ %1 %2)"
  92   syntax function (-)  "(- %1 %2)"
  93   syntax function (*)  "(* %1 %2)"
  94   syntax function (/)  "(/ %1 %2)"
  95   syntax function (-_) "(- %1)"
  96   syntax function inv  "(/ 1.0 %1)"
  97
  98   syntax predicate (<=) "(<= %1 %2)"
  99   syntax predicate (<)  "(< %1 %2)"
 100   syntax predicate (>=) "(>= %1 %2)"
 101   syntax predicate (>)  "(> %1 %2)"
 102
 103   remove prop MulComm.Comm
 104   remove prop MulAssoc.Assoc
 105   remove prop Unit_def_l
 106   remove prop Unit_def_r
 107   remove prop Inv_def_l
 108   remove prop Inv_def_r
 109   remove prop Assoc
 110   remove prop Mul_distr_l
 111   remove prop Mul_distr_r
 112   remove prop Comm
 113   remove prop Unitary
 114   remove prop Inverse
 115   remove prop Refl
 116   remove prop Trans
 117   remove prop Antisymm
 118   remove prop Total
 119   remove prop NonTrivialRing
 120   remove prop CompatOrderAdd
 121   remove prop CompatOrderMult
 122   remove prop ZeroLessOne
 123
 124 end
 125
 126 theory real.Square
 127   syntax function sqrt "(colibri_sqrt %1)"
 128
 129 end
 130
 131 theory real.FromInt
 132   syntax function from_int "(to_real %1)"
 133
 134   (* remove allprops *)
 135 end
 136
 137 theory real.Abs
 138   syntax function abs "(colibri_abs_real %1)"
 139 end
 140
 141 theory int.Abs
 142   syntax function abs "(colibri_abs_int %1)"
 143 end
 144
 145 theory int.EuclideanDivision
 146   syntax function div "(div %1 %2)"
 147   syntax function mod "(mod %1 %2)"
 148 end
 149
 150 theory int.ComputerDivision
 151   syntax function div "(colibri_cdiv %1 %2)"
 152   syntax function mod "(colibri_crem %1 %2)"
 153 end
 154
 155
 156 (*
 157 theory real.MinMax
 158
 159   remove allprops
 160 end
 161 *)
 162
 163 theory real.Truncate
 164   syntax function floor "(to_int %1)"
 165   syntax function ceil "(- (to_int (- %1)))"
 166
 167   (* remove allprops *)
 168 end
 169
 170
 171 theory Bool
 172   syntax type     bool  "Bool"
 173   syntax function True  "true"
 174   syntax function False "false"
 175 end
 176
 177 theory bool.Bool
 178   syntax function andb  "(and %1 %2)"
 179   syntax function orb   "(or %1 %2)"
 180   syntax function xorb  "(xor %1 %2)"
 181   syntax function notb  "(not %1)"
 182   syntax function implb "(=> %1 %2)"
 183 end
 184
 185 theory bool.Ite
 186   syntax function ite "(ite %1 %2 %3)"
 187 end