yices_bare.drv 3.53 KB
Newer Older
1 2
(* Why driver for SMT syntax *)

Andrei Paskevich's avatar
Andrei Paskevich committed
3
prelude ";;; this is a prelude for Yices "
4

François Bobot's avatar
François Bobot committed
5 6
printer "yices"
filename "%f-%t-%g.ycs"
7

Andrei Paskevich's avatar
Andrei Paskevich committed
8 9
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
10 11 12
time "why3cpulimit time : %s s"

(* À discuter *)
13
(*transformation "simplify_recursive_definition"*)
14 15 16 17 18 19 20 21 22
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"

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

24
transformation "discriminate"
25
transformation "encoding_smt"
26 27

theory BuiltIn
François Bobot's avatar
François Bobot committed
28 29
  syntax type int   "int"
  syntax type real  "real"
30
  syntax predicate (=)  "(= %1 %2)"
31 32 33 34 35 36

  meta "encoding : kept" type int
end

theory int.Int

Andrei Paskevich's avatar
Andrei Paskevich committed
37
  prelude ";;; this is a prelude for Yices integer arithmetic"
38

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

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

47 48 49 50
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65

  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
  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
66
  remove prop ZeroLessOne
67 68 69 70 71 72

end


theory real.Real

Andrei Paskevich's avatar
Andrei Paskevich committed
73
  prelude ";;; this is a prelude for Yices real arithmetic"
74

75 76
  syntax function zero "0"
  syntax function one  "1"
77

78 79 80
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
François Bobot's avatar
François Bobot committed
81 82 83
  (* Yices division doesn't accept anything else than constant on
  denominator so we don't use it (except for constant cf printer) *)
  (* syntax function (/)  "(/ %1 %2)" *)
84
  syntax function (-_) "(- 0 %1)"
François Bobot's avatar
François Bobot committed
85
  (* syntax function inv  "(/ 1 %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 99 100 101 102 103 104 105 106

  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
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
Andrei Paskevich's avatar
Andrei Paskevich committed
107
  remove prop ZeroLessOne
108 109 110 111 112

  meta "encoding : kept" type real

end

113
theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
114
   syntax type     bool  "bool"
115 116
   syntax function True  "true"
   syntax function False "false"
117 118 119
   meta "encoding : kept" type bool
end
theory bool.Bool
120 121 122
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function notb  "(not %1)"
123 124
end

François Bobot's avatar
François Bobot committed
125

126
theory int.EuclideanDivision
127 128
   syntax function div "(div %1 %2)"
   syntax function mod "(mod %1 %2)"
129 130 131 132 133
   remove prop Mod_bound
   remove prop Div_mod
   remove prop Mod_1
   remove prop Div_1
end
François Bobot's avatar
François Bobot committed
134 135 136 137 138 139 140 141 142 143 144 145 146 147



theory map.Map
  syntax type map "(-> %1 %2)"
  meta "encoding : lskept" function get
  meta "encoding : lskept" function set
  meta "encoding : lskept" function const

  syntax function get   "(%1 %2)"
  syntax function set   "(update %1 (%2) %3)"
end


148 149 150 151 152 153
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)