alt_ergo.drv 3.39 KB
Newer Older
1 2 3 4 5
(* Why driver for Alt-Ergo *)

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

printer "alt-ergo"
6
filename "%f-%t-%g.why"
7 8 9 10 11

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

(* À discuter *)
16
(*transformation "simplify_recursive_definition"*)
17 18
transformation "inline_trivial"

19
transformation "eliminate_builtin"
Andrei Paskevich's avatar
Andrei Paskevich committed
20
transformation "eliminate_recursion"
21
transformation "eliminate_inductive"
22
transformation "eliminate_algebraic_smt"
23
transformation "eliminate_if"
24
transformation "eliminate_let"
25

26
transformation "split_premise"
27
transformation "simplify_formula"
28
(*transformation "simplify_trivial_quantification_in_goal"*)
29 30

theory BuiltIn
31 32
  syntax type int   "int"
  syntax type real  "real"
33 34

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

37
theory int.Int
38

39
  prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
40

41 42
  syntax function zero "0"
  syntax function one  "1"
43

44 45 46 47
  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (-_) "(-%1)"
48

49 50 51 52
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"
53

54 55 56 57 58
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
59
  remove prop Mul_distr
60 61
  remove prop Comm.Comm
  remove prop Unitary
62 63 64 65
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
66 67
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
68 69 70

end

MARCHE Claude's avatar
MARCHE Claude committed
71 72
theory int.EuclideanDivision

73 74
  syntax function div "(%1 / %2)"
  syntax function mod "(%1 % %2)"
MARCHE Claude's avatar
MARCHE Claude committed
75 76 77 78

end


79 80 81 82
theory real.Real

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

83 84
  syntax function zero "0.0"
  syntax function one  "1.0"
85

86 87 88 89 90 91
  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)"
92

93 94 95 96
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 <  %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 >  %2)"
97 98 99 100 101 102 103 104 105 106 107 108 109 110

  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
111 112
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
113 114 115

end

MARCHE Claude's avatar
MARCHE Claude committed
116 117
theory real.RealInfix

118 119 120 121 122
  syntax function (+.)  "(%1 + %2)"
  syntax function (-.)  "(%1 - %2)"
  syntax function ( *.) "(%1 * %2)"
  syntax function (/.)  "(%1 / %2)"
  syntax function (-._) "(-%1)"
MARCHE Claude's avatar
MARCHE Claude committed
123

124 125 126 127
  syntax predicate (<=.) "(%1 <= %2)"
  syntax predicate (<.)  "(%1 <  %2)"
  syntax predicate (>=.) "(%1 >= %2)"
  syntax predicate (>.)  "(%1 >  %2)"
MARCHE Claude's avatar
MARCHE Claude committed
128 129 130

end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131
theory bool.Bool
132 133 134
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135 136
end

137
theory Tuple0
138 139
  syntax type     tuple0 "unit"
  syntax function Tuple0 "void"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
140 141
end

142
theory algebra.AC
143
  meta cloned AC function op
144 145
  remove cloned prop Comm.Comm
  remove cloned prop Assoc.Assoc
146 147 148
end

(*
149
Local Variables:
150
mode: why
151
compile-command: "make -C .. bench"
152
End:
153
*)