simplify.drv 1.95 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 "cpulimit_time : %s s"
11

12
transformation "simplify_recursive_definition"
13
14
15
transformation "inline_trivial"

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

22
23
24
transformation "simplify_formula"
transformation "simplify_trivial_quantification"

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)"
35
36
37
38
end

theory int.Int

39
  prelude ";;; this is a prelude for Simplify integer arithmetic"
40
41

  syntax logic zero "0"
42
  syntax logic one  "1"
43

44
45
46
47
  syntax logic (+)  "(+ %1 %2)"
  syntax logic (-)  "(- %1 %2)"
  syntax logic (*)  "(* %1 %2)"
  syntax logic (-_) "(- 0 %1)"
48

49
50
51
52
  syntax logic (<=) "(<= %1 %2)"
  syntax logic (<)  "(< %1 %2)"
  syntax logic (>=) "(>= %1 %2)"
  syntax logic (>)  "(> %1 %2)"
53
54
55
56
57
58
59
60
61
62
63
64
65

  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
66
67
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
68

69
  (* use with explicit polymorphism *)
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
70
  meta "enco_poly" "explicit"
71
72
73
  meta "encoding : base" type int

  (* use with encoding_decorate *)
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
74
  (* meta "enco_poly" "decorate" *)
75
76
  (* meta "encoding : kept" type int *)

77
78
79
end

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