yices_bare.drv 3.59 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
valid "\\bunsat\\b"
9 10
unknown "\\bunknown\\b\\|\\bsat\\b" ""
unknown "feature not supported: non linear problem" "non linear arith"
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 "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

  meta "encoding : kept" type int
Jean-Christophe's avatar
Jean-Christophe committed
33 34 35

  (* could we do this? *)
  (* meta "eliminate_algebraic" "keep_enums" *)
36 37 38 39
end

theory int.Int

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

42 43
  syntax function zero "0"
  syntax function one  "1"
44

45 46 47
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
48
  syntax function (-_) "(- 0 %1)"
49

50 51 52 53
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
54 55

  remove prop CommutativeGroup.Comm.Comm
56 57 58 59 60
  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
61
  remove prop Assoc.Assoc
62 63
  remove prop Mul_distr_l
  remove prop Mul_distr_r
64 65 66 67 68 69 70 71
  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
72
  remove prop ZeroLessOne
73 74 75 76 77 78

end


theory real.Real

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

81 82
  syntax function zero "0"
  syntax function one  "1"
83

84 85 86
  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
  syntax function (*)  "(* %1 %2)"
87 88 89
  (* 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)" *)
90
  syntax function (-_) "(- 0 %1)"
91
  (* syntax function inv  "(/ 1 %1)" *)
92

93 94 95 96
  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"
97 98

  remove prop CommutativeGroup.Comm.Comm
99 100 101 102 103
  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
104
  remove prop Assoc.Assoc
105 106
  remove prop Mul_distr_l
  remove prop Mul_distr_r
107 108
  remove prop Comm.Comm
  remove prop Unitary
109
  remove prop Inverse
110 111 112 113 114 115
  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
116
  remove prop ZeroLessOne
117 118 119 120 121

  meta "encoding : kept" type real

end

122
theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
123
   syntax type     bool  "bool"
124 125
   syntax function True  "true"
   syntax function False "false"
126 127 128
   meta "encoding : kept" type bool
end
theory bool.Bool
129 130 131
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function notb  "(not %1)"
132 133
end

François Bobot's avatar
François Bobot committed
134 135 136 137 138 139 140 141 142 143 144 145

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


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