/usr/share/why3/drivers/smt-libv2.drv is in why3 0.88.3-1ubuntu4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 | (* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
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
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
printer "smtv2"
filename "%f-%t-%g.smt2"
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
time "why3cpulimit time : %s s"
valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
end
theory int.Int
prelude ";;; SMT-LIB2: integer arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function ( * ) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
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
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
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
remove prop ZeroLessOne
end
theory real.Real
prelude ";;; SMT-LIB2: real arithmetic"
syntax function zero "0.0"
syntax function one "1.0"
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)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
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
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
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
meta "encoding : kept" type real
end
theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
end
theory bool.Bool
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)"
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
end
(* not uniformly interpreted by provers
theory real.Truncate
syntax function floor "(to_int %1)"
remove prop Floor_down
remove prop Floor_monotonic
end
*)
theory map.Map
syntax type map "(Array %1 %2)"
meta "encoding:ignore_polymorphism_ts" type map
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
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 ([<-])
meta "encoding:ignore_polymorphism_pr" prop Select_eq
meta "encoding:ignore_polymorphism_pr" prop Select_neq
remove prop Select_eq
remove prop Select_neq
end
theory map.Const
meta "encoding : lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
|