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

prelude ";;; this is a prelude for Z3"

Andrei Paskevich's avatar
Andrei Paskevich committed
5
printer "smtv1"
6 7 8
filename "%f-%t-%g.smt"

valid "^unsat"
9
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
10 11 12 13 14 15 16 17 18
time "why3cpulimit time : %s s"


(* À discuter *)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
19
transformation "eliminate_algebraic"
20
transformation "eliminate_epsilon"
21 22 23

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
Andrei Paskevich's avatar
Andrei Paskevich committed
24

25
transformation "encoding_smt"
26 27 28 29

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
30
  syntax predicate (=)  "(= %1 %2)"
31

32
  meta "encoding:kept" type int
33 34 35 36 37 38
end

theory int.Int

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

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

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

47 48 49 50
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52 53 54 55 56 57 58
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
59 60
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
61
  remove prop Comm
62 63 64 65 66 67 68
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
69
  remove prop ZeroLessOne
70 71 72 73 74 75 76 77

end


theory real.Real

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

78 79
  syntax function zero "0.0"
  syntax function one  "1.0"
80

81 82 83 84 85 86
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
  syntax function (/)  "(/ %1 %2)"
  syntax function (-_) "(- %1)"
  syntax function inv  "(/ 1.0 %1)"
87

88 89 90 91
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
92

Andrei Paskevich's avatar
Andrei Paskevich committed
93 94 95 96 97 98 99
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
100 101
  remove prop Mul_distr_l
  remove prop Mul_distr_r
Andrei Paskevich's avatar
Andrei Paskevich committed
102
  remove prop Comm
103
  remove prop Unitary
104
  remove prop Inverse
105 106 107 108 109 110
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
111
  remove prop ZeroLessOne
112

113
  meta "encoding:kept" type real
114 115 116 117 118

end

(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
Andrei Paskevich's avatar
Andrei Paskevich committed
119

120
theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
121 122 123 124 125
  syntax type bool   "bool"
  syntax function True  "true"
  syntax function False "false"

  meta "encoding_decorate:kept" type bool
126
end
Andrei Paskevich's avatar
Andrei Paskevich committed
127

128
theory bool.Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131 132
  syntax function andb  "(and %1 %2)"
  syntax function orb   "(or %1 %2)"
  syntax function xorb  "(xor %1 %2)"
  syntax function notb  "(not %1)"
133 134
end
*)