1(* Copyright (c) 2010-2011 Tjark Weber. All rights reserved. *) 2 3(* SMT-LIB 2 theories *) 4 5structure SmtLib_Theories = 6struct 7 8local 9 10 local open HolSmtTheory in end 11 12 val ERR = Feedback.mk_HOL_ERR "SmtLib_Theories" 13 14in 15 16 fun zero_args x xs = 17 if List.null xs then 18 x 19 else 20 raise ERR "zero_args" "no arguments expected" 21 22 fun one_arg f xs = 23 f (Lib.singleton_of_list xs handle Feedback.HOL_ERR _ => 24 raise ERR "one_arg" "one argument expected") 25 26 fun two_args f xs = 27 f (Lib.pair_of_list xs handle Feedback.HOL_ERR _ => 28 raise ERR "two_args" "two arguments expected") 29 30 fun three_args f xs = 31 f (Lib.triple_of_list xs handle Feedback.HOL_ERR _ => 32 raise ERR "three_args" "three arguments expected") 33 34 fun list_args f xs = 35 if List.null xs then 36 raise ERR "list_args" "non-empty argument list expected" 37 else 38 f xs 39 40 fun zero_zero f x = zero_args (zero_args (f x)) 41 fun zero_one f x = zero_args (one_arg (f x)) 42 fun zero_two f x = zero_args (two_args (f x)) 43 44 fun one_zero f x = zero_args o (one_arg (f x)) 45 fun one_one f x = one_arg o (one_arg (f x)) 46 47 fun K_zero_zero x = Lib.K (zero_args (zero_args x)) 48 fun K_zero_one f = Lib.K (zero_args (one_arg f)) 49 fun K_zero_two f = Lib.K (zero_args (two_args f)) 50 fun K_zero_three f = Lib.K (zero_args (three_args f)) 51 fun K_zero_list f = Lib.K (zero_args (list_args f)) 52 53 fun K_one_zero f = Lib.K (zero_args o one_arg f) 54 fun K_one_one f = Lib.K (one_arg o one_arg f) 55 56 fun K_two_one f = Lib.K (one_arg o two_args f) 57 58 fun chainable f = 59 let 60 fun aux t [] = raise Match (* should never happen *) 61 | aux t [_] = t 62 | aux t (x::y::zs) = aux (boolSyntax.mk_conj (t, f (x, y))) (y::zs) 63 in 64 Lib.K (zero_args (list_args 65 (fn x::y::zs => aux (f (x, y)) (y::zs) 66 | _ => raise ERR "chainable" "at least two arguments expected"))) 67 end 68 69 fun leftassoc f = 70 let 71 fun aux t [] = t 72 | aux t (y::zs) = aux (f (t, y)) zs 73 in 74 Lib.K (zero_args (list_args 75 (fn x::y::zs => aux x (y::zs) 76 | _ => raise ERR "leftassoc" "at least two arguments expected"))) 77 end 78 79 fun rightassoc f = 80 let 81 fun aux _ [] = raise Match (* should never happen *) 82 | aux cont [y] = cont y 83 | aux cont (x::y::zs) = aux (fn t => cont (f (x, t))) (y::zs) 84 in 85 Lib.K (zero_args (list_args 86 (fn x::y::zs => aux Lib.I (x::y::zs) 87 | _ => raise ERR "rightassoc" "at least two arguments expected"))) 88 end 89 90 (* A <numeral> is the digit 0 or a non-empty sequence of digits not 91 starting with 0. *) 92 fun is_numeral token = 93 let 94 val cs = String.explode token 95 in 96 cs = [#"0"] orelse 97 (not (List.null cs) andalso List.all Char.isDigit cs andalso 98 List.hd cs <> #"0") 99 end 100 101 (* A <decimal> is a token of the form <numeral>.0*<numeral>. *) 102 fun real_of_decimal token = 103 let 104 val (left, right) = Lib.pair_of_list (String.fields (Lib.equal #".") token) 105 val _ = is_numeral left orelse 106 raise ERR "real_of_decimal" "not a decimal" 107 val right = String.explode right 108 fun is_zerostar_numeral (#"0" :: c :: cs) = is_zerostar_numeral (c :: cs) 109 | is_zerostar_numeral cs = is_numeral (String.implode cs) 110 val _ = is_zerostar_numeral right orelse 111 raise ERR "real_of_decimal" "not a decimal" 112 (* drop trailing 0's *) 113 fun drop_zeros (#"0" :: cs) = drop_zeros cs 114 | drop_zeros cs = cs 115 val right = String.implode (List.rev (drop_zeros (List.rev right))) 116 val numerator = Arbint.fromString (left ^ right) 117 val ten = Arbint.fromInt 10 118 val denominator = Lib.funpow (String.size right) 119 (fn i => Arbint.* (ten, i)) Arbint.one 120 in 121 if denominator = Arbint.one then 122 realSyntax.term_of_int numerator 123 else 124 realSyntax.mk_div (realSyntax.term_of_int numerator, 125 realSyntax.term_of_int denominator) 126 end 127 handle Feedback.HOL_ERR _ => 128 raise ERR "real_of_decimal" "not a decimal" 129 130 (* ArraysEx *) 131 132 structure ArraysEx = 133 struct 134 135 val tydict = Library.dict_from_list [ 136 (* arrays are translated as functions *) 137 ("Array", K_zero_two Type.-->) 138 ] 139 140 val tmdict = Library.dict_from_list [ 141 (* array lookup is translated as function application *) 142 ("select", K_zero_two Term.mk_comb), 143 (* array update is translated as function update *) 144 ("store", K_zero_three (fn (array, index, value) => 145 Term.mk_comb (combinSyntax.mk_update (index, value), array))) 146 ] 147 148 end 149 150 (* Fixed_Size_BitVectors *) 151 152 structure Fixed_Size_BitVectors = 153 struct 154 155 val tydict = Library.dict_from_list [ 156 ("BitVec", K_one_zero (wordsSyntax.mk_word_type o fcpLib.index_type)) 157 ] 158 159 val tmdict = Library.dict_from_list [ 160 (* bit-vector constants *) 161 ("_", zero_zero (fn token => 162 if String.isPrefix "#b" token then 163 let 164 val binary = String.extract (token, 2, NONE) 165 val value = Arbnum.fromBinString binary 166 val size = Arbnum.fromInt (String.size binary) 167 in 168 wordsSyntax.mk_word (value, size) 169 end 170 else if String.isPrefix "#x" token then 171 let 172 val hex = String.extract (token, 2, NONE) 173 val value = Arbnum.fromHexString hex 174 val size = Arbnum.times2 (Arbnum.times2 (Arbnum.fromInt 175 (String.size hex))) 176 in 177 wordsSyntax.mk_word (value, size) 178 end 179 else 180 raise ERR "<Fixed_Size_BitVectors.tmdict._>" 181 "not a bit-vector constant")), 182 ("concat", K_zero_two wordsSyntax.mk_word_concat), 183 ("extract", K_two_one (fn (m, n) => 184 let 185 val index_type = fcpLib.index_type (Arbnum.plus1 (Arbnum.- (m, n))) 186 val m = numSyntax.mk_numeral m 187 val n = numSyntax.mk_numeral n 188 in 189 fn t => wordsSyntax.mk_word_extract (m, n, t, index_type) 190 end)), 191 ("bvnot", K_zero_one wordsSyntax.mk_word_1comp), 192 ("bvneg", K_zero_one wordsSyntax.mk_word_2comp), 193 ("bvand", K_zero_two wordsSyntax.mk_word_and), 194 ("bvor", K_zero_two wordsSyntax.mk_word_or), 195 ("bvadd", K_zero_two wordsSyntax.mk_word_add), 196 ("bvmul", K_zero_two wordsSyntax.mk_word_mul), 197 (* SMT-LIB states that division by 0w is unspecified. Thus, any 198 proof (of unsatisfiability) should also be valid in HOL, 199 regardless of how division by 0w is defined in HOL. *) 200 ("bvudiv", K_zero_two wordsSyntax.mk_word_div), 201 ("bvurem", K_zero_two wordsSyntax.mk_word_mod), 202 ("bvshl", K_zero_two wordsSyntax.mk_word_lsl_bv), 203 ("bvlshr", K_zero_two wordsSyntax.mk_word_lsr_bv), 204 ("bvult", K_zero_two wordsSyntax.mk_word_lo) 205 ] 206 207 end 208 209 (* Core *) 210 211 structure Core = 212 struct 213 214 val tydict = Library.dict_from_list [ 215 ("Bool", K_zero_zero Type.bool) 216 ] 217 218 val tmdict = Library.dict_from_list [ 219 ("true", K_zero_zero boolSyntax.T), 220 ("false", K_zero_zero boolSyntax.F), 221 ("not", K_zero_one boolSyntax.mk_neg), 222 ("=>", rightassoc boolSyntax.mk_imp), 223 (* FIXME: SMT-LIB declares "and" and "or" as left-assoc. This 224 interacts badly with HOL4, where they are right-assoc. In 225 particular, it breaks our proof reconstruction implementation 226 (Z3_ProofReplay.sml) in a few places that are not prepared to 227 handle the additional parentheses. For now, we parse "and" 228 and "or" as rightassoc. Since conjunction and disjunction are 229 associative, this does not change the meaning of formulas. *) 230 ("and", rightassoc boolSyntax.mk_conj), 231 ("or", rightassoc boolSyntax.mk_disj), 232 ("xor", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb 233 (Term.prim_mk_const {Thy="HolSmt", Name="xor"}, t1), t2))), 234 ("=", chainable boolSyntax.mk_eq), 235 (* "distinct" is declared as :pairwise in SMT-LIB, but rather 236 than unfolding the definition of :pairwise, we use 237 'mk_all_distinct' *) 238 ("distinct", K_zero_list (fn ts => listSyntax.mk_all_distinct 239 (listSyntax.mk_list (ts, Term.type_of (List.hd ts))))), 240 ("ite", K_zero_three boolSyntax.mk_cond) 241 ] 242 243 end 244 245 (* Ints *) 246 247 structure Ints = 248 struct 249 250 val tydict = Library.dict_from_list [ 251 ("Int", K_zero_zero intSyntax.int_ty) 252 ] 253 254 val tmdict = Library.dict_from_list [ 255 (* numerals *) 256 ("_", zero_zero (fn token => 257 if is_numeral token then 258 intSyntax.term_of_int (Arbint.fromString token) 259 else 260 raise ERR "<Ints.tmdict._>" "not a numeral")), 261 ("-", K_zero_one intSyntax.mk_negated), 262 ("-", leftassoc intSyntax.mk_minus), 263 ("+", leftassoc intSyntax.mk_plus), 264 ("*", leftassoc intSyntax.mk_mult), 265 (* FIXME: add parsing of div and mod *) 266 ("abs", K_zero_one intSyntax.mk_absval), 267 ("<=", chainable intSyntax.mk_leq), 268 ("<", chainable intSyntax.mk_less), 269 (">=", chainable intSyntax.mk_geq), 270 (">", chainable intSyntax.mk_great) 271 ] 272 273 end 274 275 (* Reals *) 276 277 structure Reals = 278 struct 279 280 val tydict = Library.dict_from_list [ 281 ("Real", K_zero_zero realSyntax.real_ty) 282 ] 283 284 val tmdict = Library.dict_from_list [ 285 (* numerals *) 286 ("_", zero_zero (fn token => 287 if is_numeral token then 288 realSyntax.term_of_int (Arbint.fromString token) 289 else 290 raise ERR "<Reals.tmdict._>" "not a numeral")), 291 (* decimals *) 292 ("_", zero_zero real_of_decimal), 293 ("-", K_zero_one realSyntax.mk_negated), 294 ("-", leftassoc realSyntax.mk_minus), 295 ("+", leftassoc realSyntax.mk_plus), 296 ("*", leftassoc realSyntax.mk_mult), 297 ("/", leftassoc realSyntax.mk_div), 298 ("<=", chainable realSyntax.mk_leq), 299 ("<", chainable realSyntax.mk_less), 300 (">=", chainable realSyntax.mk_geq), 301 (">", chainable realSyntax.mk_great) 302 ] 303 304 end 305 306 (* Reals_Ints *) 307 308 structure Reals_Ints = 309 struct 310 311 val tydict = Library.dict_from_list [ 312 ("Int", K_zero_zero intSyntax.int_ty), 313 ("Real", K_zero_zero realSyntax.real_ty) 314 ] 315 316 val tmdict = Library.dict_from_list [ 317 (* numerals *) 318 ("_", zero_zero (fn token => 319 if is_numeral token then 320 intSyntax.term_of_int (Arbint.fromString token) 321 else 322 raise ERR "<Reals_Ints.tmdict._>" "not a numeral")), 323 ("-", K_zero_one intSyntax.mk_negated), 324 ("-", leftassoc intSyntax.mk_minus), 325 ("+", leftassoc intSyntax.mk_plus), 326 ("*", leftassoc intSyntax.mk_mult), 327 (* FIXME: add parsing of div and mod *) 328 ("abs", K_zero_one intSyntax.mk_absval), 329 ("<=", chainable intSyntax.mk_leq), 330 ("<", chainable intSyntax.mk_less), 331 (">=", chainable intSyntax.mk_geq), 332 (">", chainable intSyntax.mk_great), 333 (* decimals *) 334 ("_", zero_zero real_of_decimal), 335 ("-", K_zero_one realSyntax.mk_negated), 336 ("-", leftassoc realSyntax.mk_minus), 337 ("+", leftassoc realSyntax.mk_plus), 338 ("*", leftassoc realSyntax.mk_mult), 339 ("/", leftassoc realSyntax.mk_div), 340 ("<=", chainable realSyntax.mk_leq), 341 ("<", chainable realSyntax.mk_less), 342 (">=", chainable realSyntax.mk_geq), 343 (">", chainable realSyntax.mk_great), 344 ("to_real", K_zero_one intrealSyntax.mk_real_of_int), 345 ("to_int", K_zero_one intrealSyntax.mk_INT_FLOOR), 346 ("is_int", K_zero_one intrealSyntax.mk_is_int) 347 ] 348 349 end 350 351end (* local *) 352 353end 354