smt-libv2.drv 3.85 KB
Newer Older
1
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
2

3 4 5 6 7 8 9 10 11 12
prelude ";;; generated by SMT-LIB2 driver"

(*

Note: we do not insert any command "set-logic" because its
interpretation is specific to provers

prelude "(set-logic AUFNIRA)"

    A  : Array
13 14 15
    UF : Uninterpreted Function
    DT : Datatypes (not needed at the end ...)
    NIRA : NonLinear Integer Reals Arithmetic
16

17 18 19 20
*)

printer "smtv2"
filename "%f-%t-%g.smt2"
21
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
22
time "why3cpulimit time : %s s"
23
valid "^unsat$"
24 25 26 27 28

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
  syntax predicate (=)  "(= %1 %2)"
Andrei Paskevich's avatar
Andrei Paskevich committed
29

30
  meta "encoding:kept" type int
Andrei Paskevich's avatar
Andrei Paskevich committed
31
  meta "encoding:ignore_polymorphism_ls" predicate (=)
32 33 34 35
end

theory int.Int

36
  prelude ";;; SMT-LIB2: integer arithmetic"
37 38 39 40 41 42

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
Andrei Paskevich's avatar
Andrei Paskevich committed
43
  syntax function (*)  "(* %1 %2)"
44 45 46 47 48 49 50
  syntax function (-_) "(- %1)"

  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"

Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
60
  remove prop Comm
61 62 63 64 65 66 67 68 69 70 71 72 73
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

end

theory real.Real

74
  prelude ";;; SMT-LIB2: real arithmetic"
75 76 77 78 79 80

  syntax function zero "0.0"
  syntax function one  "1.0"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  syntax function (*)  "(* %1 %2)"
82 83 84 85 86 87 88 89 90
  syntax function (/)  "(/ %1 %2)"
  syntax function (-_) "(- %1)"
  syntax function inv  "(/ 1.0 %1)"

  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"

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

111
  meta "encoding:kept" type real
112 113 114 115

end

theory Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
116 117 118 119 120
  syntax type     bool  "Bool"
  syntax function True  "true"
  syntax function False "false"

  meta "encoding:kept" type bool
121 122 123
end

theory bool.Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
124 125 126 127 128
  syntax function andb  "(and %1 %2)"
  syntax function orb   "(or %1 %2)"
  syntax function xorb  "(xor %1 %2)"
  syntax function notb  "(not %1)"
  syntax function implb "(=> %1 %2)"
129 130 131 132
end

theory bool.Ite
  syntax function ite "(ite %1 %2 %3)"
133
  meta "encoding:lskept" function ite
134
  meta "encoding:ignore_polymorphism_ls" function ite
135 136
end

137
(* not uniformly interpreted by provers
138 139 140 141 142 143 144
theory real.Truncate
  syntax function floor "(to_int %1)"
  remove prop Floor_down
  remove prop Floor_monotonic
end
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
145 146 147
theory HighOrd
  syntax type     (->) "(Array %1 %2)"
  syntax function (@)  "(select %1 %2)"
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149
  meta "encoding:lskept" function (@)
150
  meta "encoding:ignore_polymorphism_ts" type (->)
Andrei Paskevich's avatar
Andrei Paskevich committed
151
  meta "encoding:ignore_polymorphism_ls" function (@)
Andrei Paskevich's avatar
Andrei Paskevich committed
152 153
end

154
theory map.Map
155 156
  syntax function get "(select %1 %2)"
  syntax function set "(store %1 %2 %3)"
Andrei Paskevich's avatar
Andrei Paskevich committed
157

158 159
  meta "encoding:lskept" function get
  meta "encoding:lskept" function set
160 161 162 163
  meta "encoding:ignore_polymorphism_ls" function get
  meta "encoding:ignore_polymorphism_ls" function ([])
  meta "encoding:ignore_polymorphism_ls" function set
  meta "encoding:ignore_polymorphism_ls" function ([<-])
MARCHE Claude's avatar
MARCHE Claude committed
164
end
165

MARCHE Claude's avatar
MARCHE Claude committed
166
theory map.Const
167
  meta "encoding:lskept" function const
168 169
(*  syntax function const "(const[%t0] %1)" *)
end