simplify.drv 2.04 KB
Newer Older
1 2 3 4 5 6 7 8
(* Why driver for Simplify *)

prelude ";;; this is a prelude for Simplify"

printer "simplify"
filename "%f-%t-%g.sx"

valid "\\bValid\\b"
9
unknown "\\bInvalid\\b" ""
10
time "why3cpulimit time : %s s"
11 12 13 14

transformation "inline_trivial"

transformation "eliminate_builtin"
15
transformation "eliminate_definition" (*_func*)
16
transformation "eliminate_inductive"
17
transformation "eliminate_algebraic"
18 19
transformation "eliminate_if"
transformation "eliminate_let"
20

21
transformation "simplify_formula"
22
(*transformation "simplify_trivial_quantification"*)
23

24 25
transformation "remove_triggers"
(*transformation "filter_trigger_no_predicate"*)
26 27 28 29
(* predicate are *currently* translated to P(\x) = true, thus in a
trigger they can't appear since = can't appear *)
(*transformation "filter_trigger_builtin"*)

30
(* this is sound as long as int is the only kept type *)
31
transformation "encoding_tptp"
32 33

theory BuiltIn
34
  syntax predicate (=)  "(EQ %1 %2)"
François Bobot's avatar
François Bobot committed
35

36
  meta "encoding : base" type int
37 38 39 40
end

theory int.Int

41
  prelude ";;; this is a prelude for Simplify integer arithmetic"
42

43 44
  syntax function zero "0"
  syntax function one  "1"
45

46 47 48 49
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
  syntax function (-_) "(- 0 %1)"
50

51 52 53 54
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
55 56

  remove prop CommutativeGroup.Comm.Comm
57 58 59 60 61
  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
62
  remove prop Assoc.Assoc
63 64
  remove prop Mul_distr_l
  remove prop Mul_distr_r
65 66 67 68 69 70
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
71 72
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
73
  remove prop ZeroLessOne
74

75 76
end

MARCHE Claude's avatar
MARCHE Claude committed
77 78 79 80 81 82 83 84
theory real.Real

  remove prop ZeroLessOne
  remove prop NonTrivialRing

end


85
(*
86
Local Variables:
87 88
mode: why
compile-command: "make -C .. bench"
89
End:
90
*)