simplify.drv 1.89 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
transformation "eliminate_epsilon"
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
(* this is sound as long as int is the only kept type *)
32
transformation "encoding_tptp"
33 34

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

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

theory int.Int

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
57 58 59 60 61 62 63
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
64 65
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
66
  remove prop Comm
67 68 69 70 71
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
72 73
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
74
  remove prop ZeroLessOne
75

76 77
end

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

  remove prop ZeroLessOne
  remove prop NonTrivialRing

end