simplify.drv 1.86 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_smt"
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
72

73 74 75
end

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