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
*)