simplify.drv 1.96 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 logic (=)  "(EQ %1 %2)"
François Bobot's avatar
François Bobot committed
35 36 37 38 39 40 41 42 43

  (* use with explicit polymorphism *)
  (* meta "enco_poly" "explicit" *)
  meta "encoding : base" type int

  (* use with encoding_decorate *)
  meta "enco_poly" "decorate"
  meta "encoding : kept" type int

44 45 46 47
end

theory int.Int

48
  prelude ";;; this is a prelude for Simplify integer arithmetic"
49 50

  syntax logic zero "0"
51
  syntax logic one  "1"
52

53 54 55 56
  syntax logic (+)  "(+ %1 %2)"
  syntax logic (-)  "(- %1 %2)"
  syntax logic (*)  "(* %1 %2)"
  syntax logic (-_) "(- 0 %1)"
57

58 59 60 61
  syntax logic (<=) "(<= %1 %2)"
  syntax logic (<)  "(< %1 %2)"
  syntax logic (>=) "(>= %1 %2)"
  syntax logic (>)  "(> %1 %2)"
62 63 64 65 66 67 68 69 70 71 72 73 74

  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
75 76
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
77

78 79 80
end

(*
81
Local Variables:
82 83
mode: why
compile-command: "make -C .. bench"
84
End:
85
*)