1(* Copyright (c) 2009-2012 Tjark Weber. All rights reserved. *) 2 3(* Functions to invoke the Yices SMT solver *) 4 5structure Yices = struct 6 7 (* FIXME: Yices 1.0.29 only supports linear arithmetic, bit-vector shifts by 8 a numeric constant, etc. We do not check these side conditions on 9 arguments at the moment, therefore possibly producing invalid Yices 10 input. *) 11 12 (* translation of HOL terms into Yices' input syntax -- currently, all types 13 and terms except the following are treated as uninterpreted: 14 - types: 'bool', 'num', 'int', 'real', 'fun', 'prod', word types, data 15 types, record types 16 - terms: Boolean connectives (T, F, ==>, /\, \/, ~, if-then-else, 17 bool-case), quantifiers (!, ?), numeric literals, arithmetic 18 operators (SUC, +, -, *, /, ~, DIV, MOD, ABS, MIN, MAX), function 19 application, lambda abstraction, tuple selectors FST and SND, 20 various word operations, data type constructors, data type case 21 constants, record field selectors, record updates *) 22 23 val Yices_types = [ 24 (("min", "bool"), "bool", ""), 25 (("num", "num"), "nat", ""), 26 (("integer", "int"), "int", ""), 27 (("realax", "real"), "real", ""), 28 (* Yices considers "-> X Y Z" and "-> X (-> Y Z)" different types. We use 29 the latter only. *) 30 (("min", "fun"), "->", ""), 31 (* Likewise, we only use tuples of arity 2. *) 32 (("pair", "prod"), "tuple", "") 33 ] 34 35 (* many HOL operators can be translated by simply mapping them to the 36 corresponding Yices operator, or to a function that we define in Yices 37 ourselves (the last component of each tuple is the function's 38 definition) *) 39 val Yices_operator_terms = [ 40 (boolSyntax.T, "true", ""), 41 (boolSyntax.F, "false", ""), 42 (boolSyntax.equality, "=", ""), 43 (boolSyntax.implication, "=>", ""), 44 (boolSyntax.conjunction, "and", ""), 45 (boolSyntax.disjunction, "or", ""), 46 (boolSyntax.negation, "not", ""), 47 (boolSyntax.conditional, "ite", ""), 48 (numSyntax.suc_tm, "+ 1", ""), 49 (numSyntax.plus_tm, "+", ""), 50 (* in HOL, 's1 < s2' implies 's1 - s2 = 0' for naturals; Yices however 51 would consider 's1 - s2' a negative integer *) 52 (numSyntax.minus_tm, "hol_num_minus", 53 "(define hol_num_minus::(-> nat nat nat) " ^ 54 "(lambda (x::nat y::nat) (ite (< x y) 0 (- x y))))"), 55 (numSyntax.mult_tm, "*", ""), 56 (* 'x div 0' and 'x mod 0' are unspecified in HOL, but not type-correct in 57 Yices and, therefore, treated quite weirdly: Yices claims that, e.g., 58 'x = 42 div 0' is unsatisfiable. Similar for div/mod on integers. *) 59 (numSyntax.div_tm, "hol_num_div", 60 "(define hol_num_div0::(-> nat nat))\n" ^ 61 "(define hol_num_div::(-> nat nat nat) (lambda (x::nat y::nat) " ^ 62 "(ite (= y 0) (hol_num_div0 x) (div x y))))"), 63 (numSyntax.mod_tm, "hol_num_mod", 64 "(define hol_num_mod0::(-> nat nat))\n" ^ 65 "(define hol_num_mod::(-> nat nat nat) (lambda (x::nat y::nat) " ^ 66 "(ite (= y 0) (hol_num_mod0 x) (mod x y))))"), 67 (numSyntax.min_tm, "hol_num_min", 68 "(define hol_num_min::(-> nat nat nat) (lambda (x::nat y::nat) " ^ 69 "(ite (< x y) x y)))"), 70 (numSyntax.max_tm, "hol_num_max", 71 "(define hol_num_max::(-> nat nat nat) (lambda (x::nat y::nat) " ^ 72 "(ite (< x y) y x)))"), 73 (numSyntax.less_tm, "<", ""), 74 (numSyntax.leq_tm, "<=", ""), 75 (numSyntax.greater_tm, ">", ""), 76 (numSyntax.geq_tm, ">=", ""), 77 (intSyntax.negate_tm, "- 0", ""), 78 (intSyntax.absval_tm, "hol_int_abs", 79 "(define hol_int_abs::(-> int int) (lambda (x::int) " ^ 80 "(ite (< x 0) (- 0 x) x)))"), 81 (intSyntax.plus_tm, "+", ""), 82 (intSyntax.minus_tm, "-", ""), 83 (intSyntax.mult_tm, "*", ""), 84 (intSyntax.div_tm, "hol_int_div", 85 "(define hol_int_div0::(-> int int))\n" ^ 86 "(define hol_int_div::(-> int int int) (lambda (x::int y::int) " ^ 87 "(ite (= y 0) (hol_int_div0 x) (div x y))))"), 88 (intSyntax.mod_tm, "hol_int_mod", 89 "(define hol_int_mod0::(-> int int))\n" ^ 90 "(define hol_int_mod::(-> int int int) (lambda (x::int y::int) " ^ 91 "(ite (= y 0) (hol_int_mod0 x) (mod x y))))"), 92 (intSyntax.min_tm, "hol_int_min", 93 "(define hol_int_min::(-> int int int) (lambda (x::int y::int) " ^ 94 "(ite (< x y) x y)))"), 95 (intSyntax.max_tm, "hol_int_max", 96 "(define hol_int_max::(-> int int int) (lambda (x::int y::int) " ^ 97 "(ite (< x y) y x)))"), 98 (intSyntax.less_tm, "<", ""), 99 (intSyntax.leq_tm, "<=", ""), 100 (intSyntax.great_tm, ">", ""), 101 (intSyntax.geq_tm, ">=", ""), 102 (realSyntax.negate_tm, "- 0", ""), 103 (realSyntax.absval_tm, "hol_real_abs", 104 "(define hol_real_abs::(-> real real) (lambda (x::real) " ^ 105 "(ite (< x 0) (- 0 x) x)))"), 106 (realSyntax.plus_tm, "+", ""), 107 (realSyntax.minus_tm, "-", ""), 108 (realSyntax.mult_tm, "*", ""), 109 (* note that Yices uses '/' for division on reals, not 'div'; Yices will 110 fail if the second argument is 0 or not a numeral *) 111 (realSyntax.div_tm, "/", ""), 112 (realSyntax.min_tm, "hol_real_min", 113 "(define hol_real_min::(-> real real real) (lambda (x::real y::real) " ^ 114 "(ite (< x y) x y)))"), 115 (realSyntax.max_tm, "hol_real_max", 116 "(define hol_real_max::(-> real real real) (lambda (x::real y::real) " ^ 117 "(ite (< x y) y x)))"), 118 (realSyntax.less_tm, "<", ""), 119 (realSyntax.leq_tm, "<=", ""), 120 (realSyntax.great_tm, ">", ""), 121 (realSyntax.geq_tm, ">=", ""), 122 (pairSyntax.comma_tm, "mk-tuple", ""), 123 (wordsSyntax.word_and_tm, "bv-and", ""), 124 (wordsSyntax.word_or_tm, "bv-or", ""), 125 (wordsSyntax.word_xor_tm, "bv-xor", ""), 126 (wordsSyntax.word_1comp_tm, "bv-not", ""), 127 (wordsSyntax.word_lsl_tm, "bv-shift-left0", ""), 128 (wordsSyntax.word_lsr_tm, "bv-shift-right0", ""), 129 (* bv-shl is an undocumented Yices feature (as of version 1.0.29) *) 130 (wordsSyntax.word_lsl_bv_tm, "bv-shl", ""), 131 (* FIXME: The following functions have no built-in counterparts in Yices, 132 as far as I know. We could try to provide our own definitions. 133 (wordsSyntax.word_asr_tm, ...), 134 (wordsSyntax.word_ror_tm, ...), 135 (wordsSyntax.word_rol_tm, ...), 136 (wordsSyntax.word_asr_bv_tm, ...), 137 (wordsSyntax.word_ror_bv_tm, ...), 138 (wordsSyntax.word_rol_bv_tm, ...), *) 139 (* word_concat in HOL has a more general type than bv-concat in Yices *) 140 (wordsSyntax.word_concat_tm, "bv-concat", ""), 141 (wordsSyntax.word_add_tm, "bv-add", ""), 142 (wordsSyntax.word_sub_tm, "bv-sub", ""), 143 (wordsSyntax.word_mul_tm, "bv-mul", ""), 144 (wordsSyntax.word_2comp_tm, "bv-neg", ""), 145 (wordsSyntax.word_lt_tm, "bv-slt", ""), 146 (wordsSyntax.word_le_tm, "bv-sle", ""), 147 (wordsSyntax.word_gt_tm, "bv-sgt", ""), 148 (wordsSyntax.word_ge_tm, "bv-sge", ""), 149 (wordsSyntax.word_lo_tm, "bv-lt", ""), 150 (wordsSyntax.word_ls_tm, "bv-le", ""), 151 (wordsSyntax.word_hi_tm, "bv-gt", ""), 152 (wordsSyntax.word_hs_tm, "bv-ge", "") 153 ] 154 155 (* binders need to be treated differently from the operators in 156 'Yices_operator_terms' *) 157 val Yices_binder_terms = [ 158 (boolSyntax.strip_forall, "forall"), 159 (boolSyntax.strip_exists, "exists"), 160 (* Yices considers "-> X Y Z" and "-> X (-> Y Z)" different types. We use 161 the latter only. *) 162 (fn t => let val (var, body) = Term.dest_abs t 163 in 164 ([var], body) 165 end handle Feedback.HOL_ERR _ => ([], t), "lambda") 166 ] 167 168 (* ty_dict: dictionary that maps types to names 169 fresh: next fresh index to generate a new type name 170 defs: list of auxiliary Yices definitions *) 171 fun translate_type (acc, ty) = 172 let 173 fun uninterpreted_type (acc as (ty_dict, fresh, defs), ty) = 174 case Redblackmap.peek (ty_dict, ty) of 175 SOME s => (acc, s) 176 | NONE => let val name = "t" ^ Int.toString fresh 177 val ty_dict' = Redblackmap.insert (ty_dict, ty, name) 178 val defs' = "(define-type " ^ name ^ ")" :: defs 179 in 180 if !Library.trace > 0 andalso Type.is_type ty then 181 Feedback.HOL_WARNING "Yices" "translate_type" 182 ("uninterpreted type " ^ Hol_pp.type_to_string ty) 183 else 184 (); 185 if !Library.trace > 2 then 186 Feedback.HOL_MESG 187 ("HolSmtLib (Yices): inventing name '" ^ name ^ 188 "' for HOL type '" ^ Hol_pp.type_to_string ty ^ "'") 189 else 190 (); 191 ((ty_dict', fresh + 1, defs'), name) 192 end 193 (* data types, record types *) 194 fun data_type tyinfo (acc as (ty_dict, fresh, defs), ty) = 195 case Redblackmap.peek (ty_dict, ty) of 196 SOME s => (acc, s) 197 | NONE => let val name = "t" ^ Int.toString fresh 198 val ty_dict' = Redblackmap.insert (ty_dict, ty, name) 199 val acc = (ty_dict', fresh + 1, defs) 200 val is_record = not (List.null (TypeBasePure.fields_of 201 tyinfo)) 202 val ((acc, _), constructors) = Lib.foldl_map 203 (fn ((acc, i), c) => 204 let val cname = "c_" ^ name ^ "_" ^ Int.toString i 205 val c = TypeBasePure.cinst ty c 206 val (doms, _) = boolSyntax.strip_fun 207 (Term.type_of c) 208 val ((acc, _), doms) = Lib.foldl_map 209 (fn ((acc, j), dom) => 210 let val aname = if is_record then 211 "f_" ^ name ^ "_" ^ Int.toString j 212 else 213 "a_" ^ name ^ "_" ^ Int.toString i ^ "_" ^ 214 Int.toString j 215 val (acc, atype) = translate_type (acc, dom) 216 in 217 ((acc, j + 1), aname ^ "::" ^ atype) 218 end) ((acc, 0), doms) 219 val doms = String.concatWith " " doms 220 in 221 ((acc, i + 1), (cname, doms)) 222 end) ((acc, 0), TypeBasePure.constructors_of tyinfo) 223 val datatype_def = if is_record then 224 "(record " ^ Lib.snd (List.hd constructors) ^ ")" 225 else 226 "(datatype " ^ String.concatWith " " (List.map 227 (fn (cname, doms) => if doms = "" then cname else 228 "(" ^ cname ^ " " ^ doms ^ ")") constructors) ^ 229 ")" 230 val (ty_dict, fresh, defs) = acc 231 val defs' = "(define-type " ^ name ^ " " ^ datatype_def ^ 232 ")" :: defs 233 in 234 ((ty_dict, fresh, defs'), name) 235 end 236 in 237 if wordsSyntax.is_word_type ty then 238 (* bit-vector types *) 239 let val dim = fcpLib.index_to_num (wordsSyntax.dest_word_type ty) 240 in 241 (acc, "(bitvector " ^ Arbnum.toString dim ^ ")") 242 end handle Feedback.HOL_ERR _ => (* index_to_num can fail *) 243 raise (Feedback.mk_HOL_ERR "Yices" "translate_type" 244 "bit-vector type of unknown size") 245 else if Type.is_type ty then 246 (* check table of types *) 247 let val {Thy, Tyop, Args} = Type.dest_thy_type ty 248 in 249 case List.find (fn ((thy, tyop), _, _) => 250 thy = Thy andalso tyop = Tyop) Yices_types of 251 SOME (_, name, def) => 252 let val ((ty_dict, fresh, defs), yices_Args) = Lib.foldl_map 253 translate_type (acc, Args) 254 val defs' = if def = "" orelse Lib.mem def defs then defs else 255 def :: defs 256 val yices_Args = String.concatWith " " yices_Args 257 in 258 ((ty_dict, fresh, defs'), 259 if yices_Args = "" then name 260 else "(" ^ name ^ " " ^ yices_Args ^ ")") 261 end 262 | NONE => 263 (* perhaps a data type? *) 264 (case TypeBase.fetch ty of 265 SOME tyinfo => 266 data_type tyinfo (acc, ty) 267 | NONE => 268 uninterpreted_type (acc, ty)) 269 end 270 else uninterpreted_type (acc, ty) 271 end 272 273 (* dict: dictionary that maps terms to names 274 fresh: next fresh index to generate a new name 275 ty_dict: cf. translate_type 276 ty_fresh: cf. translate_type 277 defs: list of auxiliary Yices definitions *) 278 fun translate_term (acc, tm) = 279 (* numerals *) 280 if numSyntax.is_numeral tm then 281 let val n = numSyntax.dest_numeral tm 282 in 283 (acc, Arbnum.toString n) 284 end 285 else if intSyntax.is_int_literal tm then 286 let val i = intSyntax.int_of_term tm 287 val s = Arbint.toString i 288 in 289 (acc, String.substring (s, 0, String.size s - 1)) 290 end 291 else if realSyntax.is_real_literal tm then 292 let val i = realSyntax.int_of_term tm 293 val s = Arbint.toString i 294 in 295 (acc, String.substring (s, 0, String.size s - 1)) 296 end 297 (* bool_case *) 298 (* cannot be defined as a function in Yices because it is polymorphic *) 299 else if boolSyntax.is_bool_case tm then 300 let val (t1, t2, t3) = boolSyntax.dest_bool_case tm 301 val (acc, s1) = translate_term (acc, t1) 302 val (acc, s2) = translate_term (acc, t2) 303 val (acc, s3) = translate_term (acc, t3) 304 in 305 (acc, "(ite " ^ s3 ^ " " ^ s1 ^ " " ^ s2 ^ ")") 306 end 307 (* FST *) 308 (* cannot be defined as a function in Yices because it is polymorphic *) 309 else if pairSyntax.is_fst tm then 310 let val t1 = pairSyntax.dest_fst tm 311 val (acc, s1) = translate_term (acc, t1) 312 in 313 (acc, "(select " ^ s1 ^ " 1)") 314 end 315 (* SND *) 316 (* cannot be defined as a function in Yices because it is polymorphic *) 317 else if pairSyntax.is_snd tm then 318 let val t1 = pairSyntax.dest_snd tm 319 val (acc, s1) = translate_term (acc, t1) 320 in 321 (acc, "(select " ^ s1 ^ " 2)") 322 end 323 (* word literals *) 324 else if wordsSyntax.is_word_literal tm then 325 let val (num, dim_ty) = wordsSyntax.dest_n2w tm 326 val dim = fcpLib.index_to_num dim_ty 327 handle Feedback.HOL_ERR _ => 328 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 329 "word literal: bit-vector type of unknown size") 330 val n = numSyntax.dest_numeral num 331 in 332 (acc, "(mk-bv " ^ Arbnum.toString dim ^ " " ^ Arbnum.toString n ^ ")") 333 end 334 (* fcp_index *) 335 (* Hopefully used as index into a bit vector, but we don't check -- Yices 336 should. *) 337 else if wordsSyntax.is_index tm then 338 let val (t1, num) = wordsSyntax.dest_index tm 339 val (acc, s1) = translate_term (acc, t1) 340 val n = numSyntax.dest_numeral num 341 handle Feedback.HOL_ERR _ => 342 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 343 "index into bit-vector is not a numeral") 344 val sn = Arbnum.toString n 345 in 346 (acc, "(= (bv-extract " ^ sn ^ " " ^ sn ^ " " ^ s1 ^ ") 0b1)") 347 end 348 (* word_extract -- applies w2w after extraction to adjust the dimension of 349 the result in HOL *) 350 else if wordsSyntax.is_word_extract tm then 351 let val (n1, n2, w, dim_ty) = wordsSyntax.dest_word_extract tm 352 val n1 = numSyntax.dest_numeral n1 353 handle Feedback.HOL_ERR _ => 354 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 355 "word_extract: upper index is not a numeral") 356 val n2 = numSyntax.dest_numeral n2 357 handle Feedback.HOL_ERR _ => 358 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 359 "word_extract: lower index is not a numeral") 360 val dim = fcpLib.index_to_num dim_ty 361 handle Feedback.HOL_ERR _ => 362 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 363 "word_extract: result bit-vector type of unknown size") 364 val extract_dim = Arbnum.+ (Arbnum.- (n1, n2), Arbnum.one) 365 val old_dim = fcpLib.index_to_num (wordsSyntax.dim_of w) 366 handle Feedback.HOL_ERR _ => 367 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 368 "word_extract: argument bit-vector type of unknown size") 369 val (acc, s1) = translate_term (acc, w) 370 val s1 = if Arbnum.< (n1, n2) then 371 (* Yices does not support bit-vector extraction with n1 < n2 *) 372 "(mk-bv 1 0)" 373 else 374 "(bv-extract " ^ Arbnum.toString n1 ^ " " ^ Arbnum.toString n2 ^ 375 " " ^ (if Arbnum.< (n1, old_dim) then s1 else 376 (* n1 >= old_dim: we need to prepend 0s to 'w' to make 377 Yices happy *) 378 "(bv-concat (mk-bv " ^ Arbnum.toString (Arbnum.+ 379 (Arbnum.- (n1, old_dim), Arbnum.one)) ^ " 0) " ^ s1 ^ ")") 380 ^ ")" 381 in 382 if dim = extract_dim then 383 (acc, s1) 384 else if Arbnum.< (dim, extract_dim) then 385 (acc, "(bv-extract " ^ Arbnum.toString (Arbnum.- (dim, Arbnum.one)) ^ 386 " 0 " ^ s1 ^ ")") 387 else (* dim > extract_dim *) 388 (acc, "(bv-concat (mk-bv " ^ Arbnum.toString 389 (Arbnum.- (dim, extract_dim)) ^ " 0) " ^ s1 ^ ")") 390 end 391 (* w2w *) 392 else if wordsSyntax.is_w2w tm then 393 let val (t1, dim_ty) = wordsSyntax.dest_w2w tm 394 val dim = fcpLib.index_to_num dim_ty 395 handle Feedback.HOL_ERR _ => 396 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 397 "w2w: result bit-vector type of unknown size") 398 val old_dim_ty = wordsSyntax.dim_of t1 399 val old_dim = fcpLib.index_to_num old_dim_ty 400 handle Feedback.HOL_ERR _ => 401 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 402 "w2w: argument bit-vector type of unknown size") 403 val (acc, s1) = translate_term (acc, t1) 404 in 405 if Arbnum.<= (dim, old_dim) then 406 (acc, "(bv-extract " ^ Arbnum.toString (Arbnum.- (dim, Arbnum.one)) ^ 407 " 0 " ^ s1 ^ ")") 408 else 409 (acc, "(bv-concat (mk-bv " ^ Arbnum.toString 410 (Arbnum.- (dim, old_dim)) ^ " 0) " ^ s1 ^ ")") 411 end 412 (* sw2sw *) 413 else if wordsSyntax.is_sw2sw tm then 414 let val (t1, dim_ty) = wordsSyntax.dest_sw2sw tm 415 val dim = fcpLib.index_to_num dim_ty 416 handle Feedback.HOL_ERR _ => 417 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 418 "sw2sw: result bit-vector type of unknown size") 419 val old_dim_ty = wordsSyntax.dim_of t1 420 val old_dim = fcpLib.index_to_num old_dim_ty 421 handle Feedback.HOL_ERR _ => 422 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 423 "sw2sw: argument bit-vector type of unknown size") 424 val (acc, s1) = translate_term (acc, t1) 425 in 426 if Arbnum.< (dim, old_dim) then 427 (acc, "(bv-extract " ^ Arbnum.toString (Arbnum.- (dim, Arbnum.one)) ^ 428 " 0 " ^ s1 ^ ")") 429 else 430 (acc, "(bv-sign-extend " ^ s1 ^ " " ^ Arbnum.toString 431 (Arbnum.- (dim, old_dim)) ^ ")") 432 end 433 (* word_msb *) 434 else if wordsSyntax.is_word_msb tm then 435 let val t1 = wordsSyntax.dest_word_msb tm 436 val dim_ty = wordsSyntax.dim_of t1 437 val n = fcpLib.index_to_num dim_ty 438 handle Feedback.HOL_ERR _ => 439 raise (Feedback.mk_HOL_ERR "Yices" "translate_term" 440 "word_msb: argument bit-vector type of unknown size") 441 val sn = Arbnum.toString (Arbnum.- (n, Arbnum.one)) 442 val (acc, s1) = translate_term (acc, t1) 443 in 444 (acc, "(= (bv-extract " ^ sn ^ " " ^ sn ^ " " ^ s1 ^ ") 0b1)") 445 end 446 (* binders *) 447 else 448 case Lib.get_first (fn (strip_fn, name) => 449 case strip_fn tm of 450 ([], _) => NONE (* not this binder *) 451 | (vars, body) => 452 let val typs = List.map Term.type_of vars 453 (* We must gather Yices definitions for all types, and for all 454 terms in the body with the exception of bound vars. Still, 455 bound vars must not be mapped to names used elsewhere (to 456 avoid accidental capture). Also note that not all bound vars 457 need to occur in the body. *) 458 val (dict, fresh, ty_dict, ty_fresh, defs) = acc 459 (* translate types of bound variables separately, because we 460 don't want to discard their definitions *) 461 val (ty_acc, yices_typs) = Lib.foldl_map translate_type 462 ((ty_dict, ty_fresh, defs), typs) 463 val (ty_dict, ty_fresh, defs) = ty_acc 464 (* translate bound variables; make sure they are mapped to fresh 465 names; their types have just been translated already *) 466 val empty_dict = Redblackmap.mkDict Term.compare 467 val (bound_acc, yices_vars) = Lib.foldl_map translate_term 468 ((empty_dict, fresh, ty_dict, ty_fresh, []), vars) 469 val (bound_dict, fresh, _, _, _) = bound_acc 470 (* translate the body, with bound variables mapped properly *) 471 fun union dict1 dict2 = 472 Redblackmap.foldl (fn (t, s, d) => Redblackmap.insert (d, t, s)) 473 dict1 dict2 474 val acc = (union dict bound_dict, fresh, ty_dict, ty_fresh, defs) 475 val (acc, yices_body) = translate_term (acc, body) 476 val (body_dict, fresh, ty_dict, ty_fresh, defs) = acc 477 (* discard the mapping of bound variables, but keep other term 478 mappings that result from translation of the body *) 479 fun diff dict1 dict2 = 480 Redblackmap.foldl (fn (t, _, d) => 481 (Lib.fst o Redblackmap.remove) (d, t)) dict1 dict2 482 val dict = union dict (diff body_dict bound_dict) 483 val yices_bounds = String.concatWith " " (List.map (fn (v, t) => 484 v ^ "::" ^ t) (Lib.zip yices_vars yices_typs)) 485 in 486 SOME ((dict, fresh, ty_dict, ty_fresh, defs), 487 "(" ^ name ^ " (" ^ yices_bounds ^ ") " ^ yices_body ^ ")") 488 end) Yices_binder_terms of 489 SOME result => result 490 | NONE => 491 (* operators + arguments *) 492 let val (rator, rands) = boolSyntax.strip_comb tm 493 in 494 case List.find (fn (t, _, _) => Term.same_const t rator) 495 Yices_operator_terms of 496 SOME (_, name, def) => 497 let val (acc', yices_rands) = Lib.foldl_map 498 translate_term (acc, rands) 499 val (dict, fresh, ty_dict, ty_fresh, defs) = acc' 500 val defs' = if def = "" orelse Lib.mem def defs then defs else 501 def :: defs 502 val yices_rands' = String.concatWith " " yices_rands 503 in 504 ((dict, fresh, ty_dict, ty_fresh, defs'), 505 if yices_rands = [] then name 506 else "(" ^ name ^ " " ^ yices_rands' ^ ")") 507 end 508 | NONE => 509 510 (* data type constructors + arguments *) 511 let val ty = Term.type_of rator 512 val (_, data_ty) = boolSyntax.strip_fun ty 513 in 514 case TypeBase.fetch data_ty of 515 SOME tyinfo => 516 let val i = Lib.index (Term.same_const rator) 517 (TypeBasePure.constructors_of tyinfo) (* may fail *) 518 (* also collect type definitions *) 519 val (dict, fresh, ty_dict, ty_fresh, defs) = acc 520 val ((ty_dict, ty_fresh, defs), _) = translate_type 521 ((ty_dict, ty_fresh, defs), ty) 522 val ty_name = Redblackmap.find (ty_dict, data_ty) 523 val cname = "c_" ^ ty_name ^ "_" ^ Int.toString i 524 (* translate argument terms *) 525 val (acc, yices_rands) = Lib.foldl_map translate_term 526 ((dict, fresh, ty_dict, ty_fresh, defs), rands) 527 val name = String.concatWith " " (cname :: yices_rands) 528 val name = if List.null yices_rands then name 529 else "(" ^ name ^ ")" 530 in 531 (acc, name) 532 end 533 | NONE => 534 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 535 "not a data type constructor (range type is not a data type)" 536 end 537 handle Feedback.HOL_ERR _ => (* not a data type constructor *) 538 539 (* FIXME: There's a problem with the use of data type constructors 540 (which are not curried in Yices, e.g., of type "-> X Y Z") as 541 arguments to case constants, which expect curried functions (of 542 type, e.g., "-> X (-> Y Z)"). Perhaps eta-expansion currently 543 prevents this problem from showing up, but a good (clean) solution 544 is still missing. *) 545 546 (* case constants for data types (+ arguments) *) 547 let val (cases, elem) = 548 case rands of 549 [] => 550 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 551 "not a case constant (no operands)" 552 | (h::t) => (t,h) 553 val data_ty = Term.type_of elem 554 in 555 case TypeBase.fetch data_ty of 556 SOME tyinfo => 557 if Term.same_const rator (TypeBasePure.case_const_of tyinfo) 558 then 559 let (* constructors *) 560 val cs = TypeBasePure.constructors_of tyinfo 561 val _ = if List.length cs = List.length cases then () 562 else 563 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 564 "not a case constant (wrong number of cases)" 565 (* translate argument terms *) 566 val (acc, yices_cases) = Lib.foldl_map translate_term 567 (acc, cases) 568 val (acc, yices_elem) = translate_term (acc, elem) 569 val (_, _, ty_dict, _, _) = acc 570 val ty_name = Redblackmap.find (ty_dict, data_ty) 571 (* recognizers, accessors *) 572 val cs = List.map (List.length o Lib.fst o 573 boolSyntax.strip_fun o Term.type_of) cs 574 val (_, cs) = Lib.foldl_map (fn (i, n) => 575 let val cname = "c_" ^ ty_name ^ "_" ^ Int.toString i 576 fun aname j = 577 "a_" ^ ty_name ^ "_" ^ Int.toString i ^ "_" ^ 578 Int.toString j 579 val anames = List.tabulate (n, aname) 580 in 581 (i + 1, (cname, anames)) 582 end) (0, cs) 583 (* build the cascaded ite expression *) 584 val mk_case = List.foldl (fn (aname, yices_case) => 585 "(" ^ yices_case ^ " (" ^ aname ^ " " ^ yices_elem ^ 586 "))") 587 fun cascaded_ite [ycase] [(_, anames)] = 588 mk_case ycase anames 589 | cascaded_ite (ycase::ys) ((cname, anames)::cs) = 590 "(ite (" ^ cname ^ "? " ^ yices_elem ^ ") " ^ 591 mk_case ycase anames ^ " " ^ cascaded_ite ys cs ^ 592 ")" 593 | cascaded_ite _ _ = 594 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 595 "not a case constant (error in cascaded_ite)" 596 in 597 (acc, cascaded_ite yices_cases cs) 598 end 599 else 600 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 601 "not a case constant (different constant)" 602 | NONE => 603 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 604 "not a case constant (last argument is not a data type)" 605 end 606 handle Feedback.HOL_ERR _ => (* not a case constant *) 607 608 (* record field selectors *) 609 let val (select, x) = Term.dest_comb tm 610 val (select_name, select_ty) = Term.dest_const select 611 val (record_ty, rng_ty) = Type.dom_rng select_ty 612 val (record_name, _) = Type.dest_type record_ty 613 (* FIXME: This check for matching types may be too liberal, as it 614 does not take the record type into account. On the other hand, 615 it may not be needed at all: ensuring that the constant name 616 is identical to the field selector name may already be 617 sufficient. *) 618 val j = Lib.index (fn (field_name, field_ty) => 619 select_name = record_name ^ "_" ^ field_name andalso 620 Lib.can (Type.match_type field_ty) rng_ty) 621 (TypeBase.fields_of record_ty) 622 (* translate argument *) 623 val (acc, yices_x) = translate_term (acc, x) 624 val (_, _, ty_dict, _, _) = acc 625 val ty_name = Redblackmap.find (ty_dict, record_ty) 626 val yices_field = "f_" ^ ty_name ^ "_" ^ Int.toString j 627 in 628 (acc, "(select " ^ yices_x ^ " " ^ yices_field ^ ")") 629 end 630 handle Feedback.HOL_ERR _ => (* not a record field selector *) 631 632 (* record field updates *) 633 let 634 val (update_f, x) = Term.dest_comb tm 635 val (update, f) = Term.dest_comb update_f 636 (* FIXME: Only field updates using the K combinator (in eta-long 637 form) are supported at the moment. *) 638 val (var1, body) = Term.dest_abs f 639 val (f, var2) = Term.dest_comb body 640 val _ = (var1 = var2) orelse 641 raise Feedback.mk_HOL_ERR "Yices" "translate_term" 642 "not a field selector (update function not in eta-long form)" 643 val new_val = combinSyntax.dest_K_1 f 644 val (update_name, _) = Term.dest_const update 645 val record_ty = Term.type_of x 646 val (record_name, _) = Type.dest_type record_ty 647 val val_ty = Term.type_of new_val 648 (* FIXME: This check for matching types may be too liberal, as it 649 does not take the record type into account. On the other hand, 650 it may not be needed at all: ensuring that the constant name 651 is identical to the field update function's name may already be 652 sufficient. *) 653 val j = Lib.index (fn (field_name, field_ty) => 654 update_name = record_name ^ "_" ^ field_name ^ "_fupd" andalso 655 Lib.can (Type.match_type field_ty) val_ty) 656 (TypeBase.fields_of record_ty) 657 val (acc, yices_x) = translate_term (acc, x) 658 val (acc, yices_val) = translate_term (acc, new_val) 659 val (_, _, ty_dict, _, _) = acc 660 val ty_name = Redblackmap.find (ty_dict, record_ty) 661 val fname = "f_" ^ ty_name ^ "_" ^ Int.toString j 662 in 663 (acc, "(update " ^ yices_x ^ " " ^ fname ^ " " ^ yices_val ^ ")") 664 end 665 handle Feedback.HOL_ERR _ => (* not a record field selector *) 666 667 (* function application *) 668 if Term.is_comb tm then 669 (* Yices considers "-> X Y Z" and "-> X (-> Y Z)" different types. We 670 use the latter only. *) 671 let val (t1, t2) = Term.dest_comb tm 672 val (acc, s1) = translate_term (acc, t1) 673 val (acc, s2) = translate_term (acc, t2) 674 in 675 (acc, "(" ^ s1 ^ " " ^ s2 ^ ")") 676 end 677 else (* replace all other terms with a variable *) 678 (* we even replace variables, to make sure there are no name clashes 679 with either (i) variables generated by us, or (ii) reserved Yices 680 names *) 681 let val (dict, fresh, ty_dict, ty_fresh, defs) = acc 682 in 683 case Redblackmap.peek (dict, tm) of 684 SOME s => (acc, s) 685 | NONE => 686 let val name = "v" ^ Int.toString fresh 687 val dict = Redblackmap.insert (dict, tm, name) 688 (* also collect type definitions *) 689 val ((ty_dict, ty_fresh, defs), ty_name) = translate_type 690 ((ty_dict, ty_fresh, defs), Term.type_of tm) 691 val defs = "(define " ^ name ^ "::" ^ ty_name ^ ")" :: defs 692 in 693 if !Library.trace > 0 andalso Term.is_const rator then 694 Feedback.HOL_WARNING "Yices" "translate_term" 695 ("uninterpreted constant " ^ Hol_pp.term_to_string tm) 696 else 697 (); 698 if !Library.trace > 2 then 699 Feedback.HOL_MESG 700 ("HolSmtLib (Yices): inventing name '" ^ name ^ 701 "' for HOL term '" ^ Hol_pp.term_to_string tm ^ "'") 702 else 703 (); 704 ((dict, fresh + 1, ty_dict, ty_fresh, defs), name) 705 end 706 end 707 end 708 709 (* returns the eta-long form of a term, i.e., every variable/constant is 710 applied to the correct number of arguments, as determined by its type *) 711 fun full_eta_long_conv tm = 712 if Term.is_abs tm then 713 let val (v, body) = Term.dest_abs tm 714 in 715 Term.mk_abs (v, full_eta_long_conv body) 716 end 717 else 718 let val (rand, args) = boolSyntax.strip_comb tm 719 in 720 if Term.is_abs rand then 721 Term.list_mk_comb 722 (full_eta_long_conv rand, map full_eta_long_conv args) 723 else (* 'rand' is a variable/constant *) 724 let val T = Term.type_of tm 725 in 726 if (Lib.can Type.dom_rng) T then 727 (* eta expansion (by one argument) *) 728 let val v = Term.mk_var ("x", Lib.fst (Type.dom_rng T)) 729 val fresh = Term.variant (Term.free_vars tm) v 730 in 731 full_eta_long_conv (Term.mk_abs 732 (fresh, Term.list_mk_comb (rand, args @ [fresh]))) 733 end 734 else 735 Term.list_mk_comb (rand, map full_eta_long_conv args) 736 end 737 end 738 739 fun goal_to_Yices goal = 740 let 741 (* simplification: eliminates some HOL terms that are not supported by the 742 Yices translation *) 743 val SIMP_TAC = Tactical.THENL (Tactical.REPEAT Tactic.GEN_TAC, 744 [Tactical.THEN (Library.LET_SIMP_TAC, 745 Tactical.THEN 746 (Tactic.CONV_TAC (Conv.DEPTH_CONV wordsLib.EXPAND_REDUCE_CONV), 747 Tactical.THEN (simpLib.SIMP_TAC (simpLib.++ (simpLib.++ 748 (pureSimps.pure_ss, numSimps.REDUCE_ss), wordsLib.SIZES_ss)) 749 [wordsTheory.word_lsr_bv_def, wordsTheory.w2n_n2w, 750 wordsTheory.word_lsb_def, wordsTheory.word_msb_def, 751 wordsTheory.WORD_SLICE_THM, wordsTheory.WORD_BITS_EXTRACT], 752 Tactical.THEN (Library.SET_SIMP_TAC, Tactic.BETA_TAC))))]) 753 val ((asl, g), _) = SolverSpec.simplify SIMP_TAC goal 754 val (asl, g) = (List.map full_eta_long_conv asl, full_eta_long_conv g) 755 val empty = Redblackmap.mkDict Term.compare 756 val empty_ty = Redblackmap.mkDict Type.compare 757 val ((_, _, _, _, defs), yices_asl_g) = Lib.foldl_map translate_term 758 ((empty, 0, empty_ty, 0, []), asl @ [boolSyntax.mk_neg g]) 759 val defs = List.map (fn s => s ^ "\n") (List.rev defs) 760 val yices_asl_g = List.map (fn s => "(assert " ^ s ^ ")\n") yices_asl_g 761 in 762 defs @ yices_asl_g @ ["(check)\n"] 763 end 764 765 (* returns SAT if Yices reported "sat", UNSAT if Yices reported "unsat" *) 766 fun result_fn path = 767 let val instream = TextIO.openIn path 768 val line = TextIO.inputLine instream 769 in 770 TextIO.closeIn instream; 771 if line = SOME "sat\n" then 772 SolverSpec.SAT NONE 773 else if line = SOME "unsat\n" then 774 SolverSpec.UNSAT NONE 775 else 776 SolverSpec.UNKNOWN NONE 777 end 778 779 fun is_configured () = 780 Option.isSome (OS.Process.getEnv "HOL4_YICES_EXECUTABLE") 781 782 (* Yices 1.0.29, native file format *) 783 fun Yices_Oracle goal = 784 case OS.Process.getEnv "HOL4_YICES_EXECUTABLE" of 785 SOME file => 786 SolverSpec.make_solver 787 (Lib.pair () o goal_to_Yices) 788 (file ^ " -tc ") 789 (Lib.K result_fn) 790 goal 791 | NONE => 792 raise Feedback.mk_HOL_ERR "Yices" "Yices_Oracle" 793 "Yices not configured: set the HOL4_YICES_EXECUTABLE environment variable to point to the Yices executable file." 794 795end 796