src/HolSmt/Yices.sml

171   fun translate_type (acc, ty) =
173       fun uninterpreted_type (acc as (ty_dict, fresh, defs), ty) =
175           SOME s => (acc, s)
194       fun data_type tyinfo (acc as (ty_dict, fresh, defs), ty) =
196           SOME s => (acc, s)
199                       val acc = (ty_dict', fresh + 1, defs)
202                       val ((acc, _), constructors) = Lib.foldl_map
203                         (fn ((acc, i), c) =>
208                             val ((acc, _), doms) = Lib.foldl_map
209                               (fn ((acc, j), dom) =>
215                                   val (acc, atype) = translate_type (acc, dom)
217                                 ((acc, j + 1), aname ^ "::" ^ atype)
218                               end) ((acc, 0), doms)
221                           ((acc, i + 1), (cname, doms))
222                         end) ((acc, 0), TypeBasePure.constructors_of tyinfo)
230                       val (ty_dict, fresh, defs) = acc
241           (acc, "(bitvector " ^ Arbnum.toString dim ^ ")")
253                   translate_type (acc, Args)
266                 data_type tyinfo (acc, ty)
268                 uninterpreted_type (acc, ty))
270       else uninterpreted_type (acc, ty)
278   fun translate_term (acc, tm) =
283         (acc, Arbnum.toString n)
289         (acc, String.substring (s, 0, String.size s - 1))
295         (acc, String.substring (s, 0, String.size s - 1))
301           val (acc, s1) = translate_term (acc, t1)
302           val (acc, s2) = translate_term (acc, t2)
303           val (acc, s3) = translate_term (acc, t3)
305         (acc, "(ite " ^ s3 ^ " " ^ s1 ^ " " ^ s2 ^ ")")
311           val (acc, s1) = translate_term (acc, t1)
313         (acc, "(select " ^ s1 ^ " 1)")
319           val (acc, s1) = translate_term (acc, t1)
321         (acc, "(select " ^ s1 ^ " 2)")
332         (acc, "(mk-bv " ^ Arbnum.toString dim ^ " " ^ Arbnum.toString n ^ ")")
339           val (acc, s1) = translate_term (acc, t1)
346         (acc, "(= (bv-extract " ^ sn ^ " " ^ sn ^ " " ^ s1 ^ ") 0b1)")
369           val (acc, s1) = translate_term (acc, w)
383           (acc, s1)
385           (acc, "(bv-extract " ^ Arbnum.toString (Arbnum.- (dim, Arbnum.one)) ^
388           (acc, "(bv-concat (mk-bv " ^ Arbnum.toString
403           val (acc, s1) = translate_term (acc, t1)
406           (acc, "(bv-extract " ^ Arbnum.toString (Arbnum.- (dim, Arbnum.one)) ^
409           (acc, "(bv-concat (mk-bv " ^ Arbnum.toString
424           val (acc, s1) = translate_term (acc, t1)
427           (acc, "(bv-extract " ^ Arbnum.toString (Arbnum.- (dim, Arbnum.one)) ^
430           (acc, "(bv-sign-extend " ^ s1 ^ " " ^ Arbnum.toString
442           val (acc, s1) = translate_term (acc, t1)
444         (acc, "(= (bv-extract " ^ sn ^ " " ^ sn ^ " " ^ s1 ^ ") 0b1)")
458               val (dict, fresh, ty_dict, ty_fresh, defs) = acc
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
497           let val (acc', yices_rands) = Lib.foldl_map
498                 translate_term (acc, rands)
499               val (dict, fresh, ty_dict, ty_fresh, defs) = acc'
519                     val (dict, fresh, ty_dict, ty_fresh, defs) = acc
525                     val (acc, yices_rands) = Lib.foldl_map translate_term
531                   (acc, name)
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
597                     (acc, cascaded_ite yices_cases cs)
623               val (acc, yices_x) = translate_term (acc, x)
624               val (_, _, ty_dict, _, _) = acc
628             (acc, "(select " ^ yices_x ^ " " ^ yices_field ^ ")")
657               val (acc, yices_x) = translate_term (acc, x)
658               val (acc, yices_val) = translate_term (acc, new_val)
659               val (_, _, ty_dict, _, _) = acc
663             (acc, "(update " ^ yices_x ^ " " ^ fname ^ " " ^ yices_val ^ ")")
672                 val (acc, s1) = translate_term (acc, t1)
673                 val (acc, s2) = translate_term (acc, t2)
675               (acc, "(" ^ s1 ^ " " ^ s2 ^ ")")
681             let val (dict, fresh, ty_dict, ty_fresh, defs) = acc
684                 SOME s => (acc, s)