cvc3.drv 3.75 KB
Newer Older
1

2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 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 74 75 76 77 78 79 80 81 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 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
(* Why3 driver for CVC3 *)

prelude "%%% this is a prelude for CVC3 "

printer "cvc3"
filename "%f-%t-%g.cvc"

(* 'fail' must be before 'valid'; otherwise it is ignored *)
fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid\\."
unknown "Unknown\\." ""
outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
timeout "self-timeout"
time "why3cpulimit time : %s s"

(* À discuter *)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)

transformation "discriminate"
transformation "encoding_smt"

theory BuiltIn
  syntax type int   "INT"
  syntax type real  "REAL"
  syntax predicate (=)  "(%1 = %2)"

  meta "encoding : kept" type int
end

theory int.Int

  prelude "%%% this is a prelude for CVC3 integer arithmetic"

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

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

  prelude "%%% this is a prelude for CVC3 real arithmetic"

  prelude "div_by_zero: (REAL) -> REAL;"

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

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (/)  "(IF (%2 = 0) THEN (div_by_zero(%1)) ELSE (%1 / %2) ENDIF)"
  syntax function (-_) "(- %1)"
  syntax function inv  "(IF (%1 = 0) THEN (div_by_zero(1)) ELSE (1 / %1) ENDIF)"

  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 real.FromInt

  syntax function from_int "%1"

  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg

end

theory Bool
   syntax type     bool  "BITVECTOR(1)"
   syntax function True  "0bin1"
   syntax function False "0bin0"
   meta "encoding : kept" type bool
end

theory bool.Bool
   syntax function andb  "(%1 & %2)"
   syntax function orb   "(%1 | %2)"
   syntax function xorb  "(BVXOR(%1,%2))"
   syntax function notb  "(~ %1)"
end


theory map.Map
  syntax type map "(ARRAY %1 OF %2)"
  meta "encoding : lskept" function get
  meta "encoding : lskept" function set

  syntax function get "(%1[%2])"
  syntax function set "(%1 WITH [%2] := %3)"
end

import "discrimination.gen"