z3.drv 3 KB
Newer Older
1
2
(* Why driver for SMT syntax *)

3
prelude ";;; this is a prelude for Z3"
4
5

printer "smtv1"
6
filename "%f-%t-%g.smt"
7

8
9
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
10
11

(* À discuter *)
12
transformation "simplify_recursive_definition"
Francois Bobot's avatar
sorry    
Francois Bobot committed
13
transformation "inline_trivial"
14

15
transformation "eliminate_builtin"
16
17
18
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
19

20
transformation "simplify_formula"
21
transformation "simplify_trivial_quantification"
22

23
transformation "encoding_smt"
24
transformation "encoding_simple2"
25
26

theory BuiltIn
27
28
29
  syntax type int   "Int"
  syntax type real  "Real"
  syntax logic (=)  "(= %1 %2)"
30
31
32
33
end

theory int.Int

34
35
  prelude ";;; this is a prelude for Z3 integer arithmetic"

36
  syntax logic zero "0"
37
  syntax logic one  "1"
38

39
40
41
42
  syntax logic (+)  "(+ %1 %2)"
  syntax logic (-)  "(- %1 %2)"
  syntax logic (*)  "(* %1 %2)"
  syntax logic (-_) "(- %1)"
43

44
45
46
47
  syntax logic (<=) "(<= %1 %2)"
  syntax logic (<)  "(< %1 %2)"
  syntax logic (>=) "(>= %1 %2)"
  syntax logic (>)  "(> %1 %2)"
48
49
50
51
52
53
54
55
56

  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
57
58
59
60
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
61
62
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
63

64
65
  meta "encoding : kept" type int

66
67
end

68
69
70

theory real.Real

71
  prelude ";;; this is a prelude for Z3 real arithmetic"
72

73
74
  syntax logic zero "0.0"
  syntax logic one  "1.0"
75

76
77
78
79
80
  syntax logic (+)  "(+ %1 %2)"
  syntax logic (-)  "(- %1 %2)"
  syntax logic (*)  "(* %1 %2)"
  syntax logic (/)  "(/ %1 %2)"
  syntax logic (-_) "(- %1)"
81
82
  syntax logic inv  "(/ 1.0 %1)"

83
84
85
86
  syntax logic (<=) "(<= %1 %2)"
  syntax logic (<)  "(< %1 %2)"
  syntax logic (>=) "(>= %1 %2)"
  syntax logic (>)  "(> %1 %2)"
87
88
89
90
91
92
93
94
95
96
97
98
99
100

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Inverse
  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
101
102
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
103

104
105
  meta "encoding : kept" type real

106
107
108
109
110
end

(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
111
112
   syntax type bool   "bool"
   syntax logic True  "true"
113
   syntax logic False "false"
114
115
116
   syntax logic andb  "(and %1 %2)"
   syntax logic orb   "(or %1 %2)"
   syntax logic xorb  "(xor %1 %2)"
117
   syntax logic notb  "(not %1)"
118
   meta cloned "encoding_decorate : kept" type bool
119
120
121
122
end
*)


Francois Bobot's avatar
Francois Bobot committed
123
124
125
126
127
128
129
130
theory int.EuclideanDivision
   syntax logic div "(div %1 %2)"
   syntax logic mod "(mod %1 %2)"
   remove prop Mod_bound
   remove prop Div_mod
   remove prop Mod_1
   remove prop Div_1
end
131
132

(*
133
Local Variables:
134
mode: why
135
compile-command: "unset LANG; make -C .. bench"
136
End:
137
*)