alt_ergo_bare.drv 3.43 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
(* Why driver for Alt-Ergo *)

prelude "(* this is a prelude for Alt-Ergo*)"

printer "alt-ergo"
filename "%f-%t-%g.why"

valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "why3cpulimit time : %s s"

(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "eliminate_if"
transformation "eliminate_let"

transformation "split_premise"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)

theory BuiltIn
  syntax type int   "int"
  syntax type real  "real"

  syntax predicate (=)  "(%1 = %2)"
end

theory int.Int

  prelude "(* this is a prelude for Alt-Ergo 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.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
68
  remove prop ZeroLessOne
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

end

theory int.EuclideanDivision

  syntax function div "(%1 / %2)"
  syntax function mod "(%1 % %2)"

end


theory real.Real

  prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"

  syntax function zero "0.0"
  syntax function one  "1.0"

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

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
114
  remove prop ZeroLessOne
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132

end

theory real.RealInfix

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

end

133
theory Bool
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
end

theory Tuple0
  syntax type     tuple0 "unit"
  syntax function Tuple0 "void"
end

theory algebra.AC
  meta cloned AC function op
  remove cloned prop Comm.Comm
  remove cloned prop Assoc.Assoc
end

(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)