drivers/cvc3.drv

   1
   2 (* Why3 driver for CVC3 *)
   3
   4 prelude "%%% this is a prelude for CVC3 "
   5
   6 printer "cvc3"
   7 filename "%f-%t-%g.cvc"
   8
   9 (* 'fail' must be before 'valid'; otherwise it is ignored *)
  10 fail "Parse Error: \\(.*\\)" "\\1"
  11 valid "Valid\\."
  12 unknown "Unknown\\." ""
  13 outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
  14 timeout "self-timeout"
  15 time "why3cpulimit time : %s s"
  16
  17 (* Performed introductions depending on whether counterexamples are
  18    requested, as said by the meta "get_counterexmp". When this meta
  19    set, this transformation introduces the model variables that are
  20    still embedded in the goal. When it is not set, it removes all
  21    these unused-ce-related variables, even in the context.  *)
  22 transformation "counterexamples_dependent_intros"
  23
  24 transformation "inline_trivial"
  25 transformation "eliminate_builtin"
  26 transformation "eliminate_definition"
  27 transformation "eliminate_inductive"
  28 transformation "eliminate_epsilon"
  29 transformation "eliminate_algebraic"
  30 transformation "eliminate_literal"
  31
  32 transformation "simplify_formula"
  33 (*transformation "simplify_trivial_quantification"*)
  34
  35 transformation "discriminate"
  36 transformation "encoding_smt"
  37
  38 theory BuiltIn
  39   syntax type int   "INT"
  40   syntax type real  "REAL"
  41   syntax predicate (=)  "(%1 = %2)"
  42
  43   meta "encoding:kept" type int
  44 end
  45
  46 theory int.Int
  47
  48   prelude "%%% this is a prelude for CVC3 integer arithmetic"
  49
  50   syntax function zero "0"
  51   syntax function one  "1"
  52
  53   syntax function (+)  "(%1 + %2)"
  54   syntax function (-)  "(%1 - %2)"
  55   syntax function (*)  "(%1 * %2)"
  56   syntax function (-_) "(- %1)"
  57
  58   syntax predicate (<=) "(%1 <= %2)"
  59   syntax predicate (<)  "(%1 < %2)"
  60   syntax predicate (>=) "(%1 >= %2)"
  61   syntax predicate (>)  "(%1 > %2)"
  62
  63   remove prop MulComm.Comm
  64   remove prop MulAssoc.Assoc
  65   remove prop Unit_def_l
  66   remove prop Unit_def_r
  67   remove prop Inv_def_l
  68   remove prop Inv_def_r
  69   remove prop Assoc
  70   remove prop Mul_distr_l
  71   remove prop Mul_distr_r
  72   remove prop Comm
  73   remove prop Unitary
  74   remove prop Refl
  75   remove prop Trans
  76   remove prop Antisymm
  77   remove prop Total
  78   remove prop NonTrivialRing
  79   remove prop CompatOrderAdd
  80   remove prop ZeroLessOne
  81
  82 end
  83
  84
  85 theory real.Real
  86
  87   prelude "%%% this is a prelude for CVC3 real arithmetic"
  88
  89   prelude "div_by_zero: (REAL) -> REAL;"
  90
  91   syntax function zero "0"
  92   syntax function one  "1"
  93
  94   syntax function (+)  "(%1 + %2)"
  95   syntax function (-)  "(%1 - %2)"
  96   syntax function (*)  "(%1 * %2)"
  97   syntax function (/)  "(IF (%2 = 0) THEN (div_by_zero(%1)) ELSE (%1 / %2) ENDIF)"
  98   syntax function (-_) "(- %1)"
  99   syntax function inv  "(IF (%1 = 0) THEN (div_by_zero(1)) ELSE (1 / %1) ENDIF)"
 100
 101   syntax predicate (<=) "(%1 <= %2)"
 102   syntax predicate (<)  "(%1 < %2)"
 103   syntax predicate (>=) "(%1 >= %2)"
 104   syntax predicate (>)  "(%1 > %2)"
 105
 106   remove prop MulComm.Comm
 107   remove prop MulAssoc.Assoc
 108   remove prop Unit_def_l
 109   remove prop Unit_def_r
 110   remove prop Inv_def_l
 111   remove prop Inv_def_r
 112   remove prop Assoc
 113   remove prop Mul_distr_l
 114   remove prop Mul_distr_r
 115   remove prop Comm
 116   remove prop Unitary
 117   remove prop Inverse
 118   remove prop Refl
 119   remove prop Trans
 120   remove prop Antisymm
 121   remove prop Total
 122   remove prop NonTrivialRing
 123   remove prop CompatOrderAdd
 124   remove prop ZeroLessOne
 125
 126   meta "encoding:kept" type real
 127
 128 end
 129
 130 theory real.FromInt
 131
 132   syntax function from_int "%1"
 133
 134   remove prop Zero
 135   remove prop One
 136   remove prop Add
 137   remove prop Sub
 138   remove prop Mul
 139   remove prop Neg
 140
 141 end
 142
 143 theory Bool
 144   syntax type     bool  "BITVECTOR(1)"
 145   syntax function True  "0bin1"
 146   syntax function False "0bin0"
 147
 148   meta "encoding:kept" type bool
 149 end
 150
 151 theory bool.Bool
 152   syntax function andb  "(%1 & %2)"
 153   syntax function orb   "(%1 | %2)"
 154   syntax function xorb  "(BVXOR(%1,%2))"
 155   syntax function notb  "(~ %1)"
 156 end
 157
 158 theory HighOrd
 159   syntax type (->) "(ARRAY %1 OF %2)"
 160   syntax function (@) "(%1[%2])"
 161
 162   meta "encoding:lskept" function (@)
 163 end
 164
 165 theory map.Map
 166   syntax function get "(%1[%2])"
 167   syntax function set "(%1 WITH [%2] := %3)"
 168
 169   meta "encoding:lskept" function get
 170   meta "encoding:lskept" function set
 171 end
 172
 173 import "discrimination.gen"