z3_smtv1.drv 3.16 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 21 22

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

24
transformation "encoding_smt"
Andrei Paskevich's avatar
Andrei Paskevich committed
25
transformation "encoding_sort"
26 27 28 29

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

  meta "encoding : kept" type int
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 52

  remove prop CommutativeGroup.Comm.Comm
53 54 55 56 57
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
58
  remove prop Assoc.Assoc
59 60
  remove prop Mul_distr_l
  remove prop Mul_distr_r
61 62 63 64 65 66 67 68
  remove prop Comm.Comm
  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 93

  remove prop CommutativeGroup.Comm.Comm
94 95 96 97 98
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
99
  remove prop Assoc.Assoc
100 101
  remove prop Mul_distr_l
  remove prop Mul_distr_r
102 103
  remove prop Comm.Comm
  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 114 115 116 117 118

  meta "encoding : kept" type real

end

(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
119
theory Bool
120
   syntax type bool   "bool"
121 122
   syntax function True  "true"
   syntax function False "false"
123
   meta "encoding_decorate : kept" type bool
124 125
end
theory bool.Bool
126 127 128 129
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function xorb  "(xor %1 %2)"
   syntax function notb  "(not %1)"
130 131 132 133 134 135 136 137 138 139
end
*)


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