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

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

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

valid "\\bValid\\b"
unknown "\\bInvalid\\b" "Unknown"
10
time "why3cpulimit time : %s s"
11

12
(*transformation "simplify_recursive_definition"*)
13
14
15
transformation "inline_trivial"

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

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

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

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
37
38

  meta "enco_poly" "decorate"
  meta "encoding : kept" type int

39
40
41
42
end

theory int.Int

43
  prelude ";;; this is a prelude for Simplify integer arithmetic"
44

45
46
  syntax function zero "0"
  syntax function one  "1"
47

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

53
54
55
56
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
57
58
59
60
61
62
63
64
65
66
67
68
69

  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 Antisymm
  remove prop Total
70
71
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
72
  remove prop ZeroLessOne
73

74
75
76
end

(*
77
Local Variables:
78
79
mode: why
compile-command: "make -C .. bench"
80
End:
81
*)