MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

simplify.drv 1.82 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

(* 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"

transformation "simplify_recursive_definition"      
transformation "inline_trivial"

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

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

30
(*transformation "encoding_decorate_mono"*)
31
32

theory BuiltIn
33
34
35
36
  syntax type int   "Int"
  syntax type real  "Real"
  syntax logic (=)  "(EQ %1 %2)"
  syntax logic (<>) "(NEQ %1 %2)"
37
38
39
40
41
42
43
44
end

theory int.Int

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

  syntax logic zero "0"

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

50
51
52
53
  syntax logic (<=) "(<= %1 %2)"
  syntax logic (<)  "(< %1 %2)"
  syntax logic (>=) "(>= %1 %2)"
  syntax logic (>)  "(> %1 %2)"
54
55
56
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
end

theory transform.encoding_decorate.Kept
70
  meta cloned "encoding_decorate : kept" type t
71
72
73
74
75
76
77
78
end

(*
Local Variables: 
mode: why
compile-command: "make -C .. bench"
End: 
*)