z3.drv 3.23 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
time "cpulimit_time : \\([0-9]+.[0-9]*\\) s" "0:0:\\1"
11 12

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

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

21
transformation "simplify_formula"
22
transformation "simplify_trivial_quantification"
23

24 25
transformation "encoding_array"

26
transformation "encoding_smt"
27
transformation "encoding_sort"
28 29

theory BuiltIn
30 31 32
  syntax type int   "Int"
  syntax type real  "Real"
  syntax logic (=)  "(= %1 %2)"
33 34 35 36
end

theory int.Int

37 38
  prelude ";;; this is a prelude for Z3 integer arithmetic"

39
  syntax logic zero "0"
40
  syntax logic one  "1"
41

42 43 44 45
  syntax logic (+)  "(+ %1 %2)"
  syntax logic (-)  "(- %1 %2)"
  syntax logic (*)  "(* %1 %2)"
  syntax logic (-_) "(- %1)"
46

47 48 49 50
  syntax logic (<=) "(<= %1 %2)"
  syntax logic (<)  "(< %1 %2)"
  syntax logic (>=) "(>= %1 %2)"
  syntax logic (>)  "(> %1 %2)"
51 52 53 54 55 56 57 58 59

  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
60 61 62 63
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
64 65
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
66

67 68
  meta "encoding : kept" type int

69 70
end

71 72 73

theory real.Real

74
  prelude ";;; this is a prelude for Z3 real arithmetic"
75

76 77
  syntax logic zero "0.0"
  syntax logic one  "1.0"
78

79 80 81 82 83
  syntax logic (+)  "(+ %1 %2)"
  syntax logic (-)  "(- %1 %2)"
  syntax logic (*)  "(* %1 %2)"
  syntax logic (/)  "(/ %1 %2)"
  syntax logic (-_) "(- %1)"
84 85
  syntax logic inv  "(/ 1.0 %1)"

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

  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
104 105
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
106

107 108
  meta "encoding : kept" type real

109 110 111 112 113
end

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


Francois Bobot's avatar
Francois Bobot committed
126 127 128 129 130 131 132 133
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
134

135
theory transform.array.Array
François Bobot's avatar
François Bobot committed
136 137 138 139 140
  syntax logic get "(select %1 %2)"
  syntax logic set "(store %1 %2)"
  remove prop Select_eq
  remove prop Select_neq

141 142
end

143
(*
144
Local Variables:
145
mode: why
146
compile-command: "unset LANG; make -C .. bench"
147
End:
148
*)