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

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

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
time "why3cpulimit time : %s s"


transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
17
transformation "eliminate_algebraic"
18
transformation "eliminate_literal"
19
transformation "eliminate_epsilon"
20 21 22

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
23

24
transformation "encoding_smt"
25 26 27 28

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

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

theory int.Int

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

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

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

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

51 52 53 54 55 56 57
  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
58 59
  remove prop Mul_distr_l
  remove prop Mul_distr_r
60
  remove prop Comm
61 62 63 64 65 66 67
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
68
  remove prop ZeroLessOne
69 70 71 72 73 74 75 76

end


theory real.Real

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

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

80 81 82 83 84 85
  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)"
86

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

92 93 94 95 96 97 98
  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
99 100
  remove prop Mul_distr_l
  remove prop Mul_distr_r
101
  remove prop Comm
102
  remove prop Unitary
103
  remove prop Inverse
104 105 106 107 108 109
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
110
  remove prop ZeroLessOne
111

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

end

(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
118

119
theory Bool
120 121 122 123 124
  syntax type bool   "bool"
  syntax function True  "true"
  syntax function False "false"

  meta "encoding_decorate:kept" type bool
125
end
126

127
theory bool.Bool
128 129 130 131
  syntax function andb  "(and %1 %2)"
  syntax function orb   "(or %1 %2)"
  syntax function xorb  "(xor %1 %2)"
  syntax function notb  "(not %1)"
132 133
end
*)