src/HOL/Tools/SMT/z3_model.ML
changeset 41058 42e0a0bfef73
parent 40840 2f97215e79bf
child 41122 72176ec5e031
equal deleted inserted replaced
41057:8dbc951a291c 41058:42e0a0bfef73
   111 
   111 
   112 fun get_term n T es (cx as (terms, next_val)) =
   112 fun get_term n T es (cx as (terms, next_val)) =
   113   (case Symtab.lookup terms n of
   113   (case Symtab.lookup terms n of
   114     SOME t => ((t, es), cx)
   114     SOME t => ((t, es), cx)
   115   | NONE =>
   115   | NONE =>
   116       let val t = Var (("fresh", next_val), T)
   116       let val t = Var (("skolem", next_val), T)
   117       in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
   117       in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
   118 
   118 
   119 fun trans_expr _ True = pair @{const True}
   119 fun trans_expr _ True = pair @{const True}
   120   | trans_expr _ False = pair @{const False}
   120   | trans_expr _ False = pair @{const False}
   121   | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
   121   | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
   231         SOME (Const (@{const_name SMT.fun_app}, _), _) => true
   231         SOME (Const (@{const_name SMT.fun_app}, _), _) => true
   232       | _ => false)
   232       | _ => false)
   233 
   233 
   234   in (map unfold_eq eqs, filter_out is_fun_app defs) end
   234   in (map unfold_eq eqs, filter_out is_fun_app defs) end
   235 
   235 
   236 fun unfold_simple_eqs (eqs, defs) =
   236 fun unfold_eqs (eqs, defs) =
   237   let
   237   let
   238     fun add_rewr (l as Const _) (r as Var _) = SOME (r, l)
   238     val is_ground = not o Term.exists_subterm (fn Var _ => true | _ => false)
   239       | add_rewr (l as Free _) (r as Var _) = SOME (r, l)
   239     fun add_rewr l (r as Var _) = if is_ground l then SOME (r, l) else NONE
   240       | add_rewr _ _ = NONE
   240       | add_rewr _ _ = NONE
   241     val (rs, eqs') = partition_eqs add_rewr eqs
       
   242 
   241 
   243     fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
   242     fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
   244       | is_trivial _ = false
   243       | is_trivial _ = false
   245   in pairself (replace_vars rs #> filter_out is_trivial) (eqs', defs) end
   244 
       
   245     fun replace rs = replace_vars rs #> filter_out is_trivial
       
   246 
       
   247     fun unfold (es, ds) =
       
   248       (case partition_eqs add_rewr es of
       
   249         ([], _) => (es, ds)
       
   250       | (rs, es') => unfold (pairself (replace rs) (es', ds)))
       
   251 
       
   252   in unfold (eqs, defs) end
   246 
   253 
   247 fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
   254 fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
   248       eq $ u $ t
   255       eq $ u $ t
   249   | swap_free t = t
   256   | swap_free t = t
   250 
   257 
   282   read_cex terms ls
   289   read_cex terms ls
   283   |> with_context terms translate
   290   |> with_context terms translate
   284   |> apfst flat o split_list
   291   |> apfst flat o split_list
   285   |> remove_int_nat_coercions
   292   |> remove_int_nat_coercions
   286   |> unfold_funapp
   293   |> unfold_funapp
   287   |> unfold_simple_eqs
   294   |> unfold_eqs
   288   |>> map swap_free
   295   |>> map swap_free
   289   |>> filter is_free_constraint
   296   |>> filter is_free_constraint
   290   |> frees_for_vars ctxt
   297   |> frees_for_vars ctxt
   291   ||> filter is_const_def
   298   ||> filter is_const_def
   292 
   299