split up Z3 models into constraints on free variables and constant definitions;
authorboehmes
Tue Nov 30 18:22:43 2010 +0100 (2010-11-30)
changeset 4082847ff261431c4
parent 40807 eeaa59fb5ad8
child 40829 edd1e0764da1
split up Z3 models into constraints on free variables and constant definitions;
reduce Z3 models by replacing unknowns with free variables and constants from the goal;
remove occurrences of the hidden constant fun_app from Z3 models
src/HOL/Tools/SMT/smt_failure.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/z3_model.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_failure.ML	Tue Nov 30 00:12:29 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_failure.ML	Tue Nov 30 18:22:43 2010 +0100
     1.3 @@ -6,12 +6,17 @@
     1.4  
     1.5  signature SMT_FAILURE =
     1.6  sig
     1.7 +  type counterexample = {
     1.8 +    is_real_cex: bool,
     1.9 +    free_constraints: term list,
    1.10 +    const_defs: term list}
    1.11    datatype failure =
    1.12 -    Counterexample of bool * term list |
    1.13 +    Counterexample of counterexample |
    1.14      Time_Out |
    1.15      Out_Of_Memory |
    1.16      Abnormal_Termination of int |
    1.17      Other_Failure of string
    1.18 +  val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
    1.19    val string_of_failure: Proof.context -> failure -> string
    1.20    exception SMT of failure
    1.21  end
    1.22 @@ -19,23 +24,32 @@
    1.23  structure SMT_Failure: SMT_FAILURE =
    1.24  struct
    1.25  
    1.26 +type counterexample = {
    1.27 +  is_real_cex: bool,
    1.28 +  free_constraints: term list,
    1.29 +  const_defs: term list}
    1.30 +
    1.31  datatype failure =
    1.32 -  Counterexample of bool * term list |
    1.33 +  Counterexample of counterexample |
    1.34    Time_Out |
    1.35    Out_Of_Memory |
    1.36    Abnormal_Termination of int |
    1.37    Other_Failure of string
    1.38  
    1.39 -fun string_of_failure ctxt (Counterexample (real, ex)) =
    1.40 -      let
    1.41 -        val msg =
    1.42 -          if real then "Counterexample found (possibly spurious)"
    1.43 -          else "Potential counterexample found"
    1.44 -      in
    1.45 -        if null ex then msg
    1.46 -        else Pretty.string_of (Pretty.big_list (msg ^ ":")
    1.47 -          (map (Syntax.pretty_term ctxt) ex))
    1.48 -      end
    1.49 +fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
    1.50 +  let
    1.51 +    val msg =
    1.52 +      if is_real_cex then "Counterexample found (possibly spurious)"
    1.53 +      else "Potential counterexample found"
    1.54 +  in
    1.55 +    if null free_constraints andalso null const_defs then Pretty.str msg
    1.56 +    else
    1.57 +      Pretty.big_list (msg ^ ":")
    1.58 +        (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
    1.59 +  end
    1.60 +
    1.61 +fun string_of_failure ctxt (Counterexample cex) =
    1.62 +      Pretty.string_of (pretty_counterexample ctxt cex)
    1.63    | string_of_failure _ Time_Out = "Timed out"
    1.64    | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    1.65    | string_of_failure _ (Abnormal_Termination err) =
     2.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 30 00:12:29 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 30 18:22:43 2010 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4      interface: interface,
     2.5      outcome: string -> string list -> outcome * string list,
     2.6      cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
     2.7 -      term list) option,
     2.8 +      term list * term list) option,
     2.9      reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    2.10        (int list * thm) * Proof.context) option }
    2.11  
    2.12 @@ -65,7 +65,7 @@
    2.13    interface: interface,
    2.14    outcome: string -> string list -> outcome * string list,
    2.15    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    2.16 -    term list) option,
    2.17 +    term list * term list) option,
    2.18    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    2.19      (int list * thm) * Proof.context) option }
    2.20  
    2.21 @@ -260,9 +260,14 @@
    2.22          then the reconstruct ctxt recon ls
    2.23          else (([], ocl ()), ctxt)
    2.24      | (result, ls) =>
    2.25 -        let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
    2.26 -        in
    2.27 -          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
    2.28 +        let
    2.29 +          val (ts, us) =
    2.30 +            (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
    2.31 +         in
    2.32 +          raise SMT_Failure.SMT (SMT_Failure.Counterexample {
    2.33 +            is_real_cex = (result = Sat),
    2.34 +            free_constraints = ts,
    2.35 +            const_defs = us})
    2.36          end)
    2.37  
    2.38    val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
    2.39 @@ -351,15 +356,14 @@
    2.40      let
    2.41        fun solve irules = snd (smt_solver NONE ctxt' irules)
    2.42        val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
    2.43 -      val str_of = SMT_Failure.string_of_failure ctxt'
    2.44 +      val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
    2.45        fun safe_solve irules =
    2.46          if pass_exns then SOME (solve irules)
    2.47          else (SOME (solve irules)
    2.48            handle
    2.49              SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
    2.50 -              (C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE)
    2.51 -          | SMT_Failure.SMT fail =>
    2.52 -              (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
    2.53 +              (C.verbose_msg ctxt' str_of fail; NONE)
    2.54 +          | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
    2.55      in
    2.56        safe_solve (map (pair ~1) (rules @ prems))
    2.57        |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
     3.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Tue Nov 30 00:12:29 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Tue Nov 30 18:22:43 2010 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  signature Z3_MODEL =
     3.5  sig
     3.6    val parse_counterex: Proof.context -> SMT_Translate.recon -> string list ->
     3.7 -    term list
     3.8 +    term list * term list
     3.9  end
    3.10  
    3.11  structure Z3_Model: Z3_MODEL =
    3.12 @@ -70,117 +70,51 @@
    3.13  val cex = space |--
    3.14    Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
    3.15  
    3.16 -fun read_cex ls =
    3.17 +fun resolve terms ((n, k), cases) =
    3.18 +  (case Symtab.lookup terms n of
    3.19 +    NONE => NONE
    3.20 +  | SOME t => SOME ((t, k), cases))
    3.21 +
    3.22 +fun annotate _ (_, []) = NONE
    3.23 +  | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, []))
    3.24 +  | annotate _ (_, [_]) = NONE
    3.25 +  | annotate terms (n, cases as (args, _) :: _) =
    3.26 +      let val (cases', (_, else_case)) = split_last cases
    3.27 +      in resolve terms ((n, length args), (else_case, cases')) end
    3.28 +
    3.29 +fun read_cex terms ls =
    3.30    maps (cons "\n" o raw_explode) ls
    3.31    |> try (fst o Scan.finite Symbol.stopper cex)
    3.32    |> the_default []
    3.33 -
    3.34 -
    3.35 -(* normalization *)
    3.36 -
    3.37 -local
    3.38 -  fun matches terms f n =
    3.39 -    (case Symtab.lookup terms n of
    3.40 -      NONE => false
    3.41 -    | SOME t => f t)
    3.42 -
    3.43 -  fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases)
    3.44 -in
    3.45 -
    3.46 -fun reduce_function (n, [c]) = SOME ((n, 0), [c])
    3.47 -  | reduce_function (n, cases) =
    3.48 -      let val (patterns, else_case as (_, e)) = split_last cases
    3.49 -      in
    3.50 -        (case patterns of
    3.51 -          [] => NONE
    3.52 -        | (args, _) :: _ => SOME ((n, length args),
    3.53 -            filter_out (equal e o snd) patterns @ [else_case]))
    3.54 -      end
    3.55 -
    3.56 -fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst)
    3.57 -
    3.58 -fun substitute_constants terms =
    3.59 -  let
    3.60 -    fun check vs1 [] = rev vs1
    3.61 -      | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) =
    3.62 -          if matches terms (fn Free _ => true | _ => false) n orelse k > 0
    3.63 -          then check (v :: vs1) vs2
    3.64 -          else
    3.65 -            let
    3.66 -              fun sub (e as Value j) = if i = j then App (n, []) else e
    3.67 -                | sub e = e
    3.68 -            in check (map (subst sub) vs1) (map (subst sub) vs2) end
    3.69 -      | check vs1 (v :: vs2) = check (v :: vs1) vs2
    3.70 -  in check [] end
    3.71 -
    3.72 -fun remove_int_nat_coercions terms vs =
    3.73 -  let
    3.74 -    fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
    3.75 -
    3.76 -    val (default_int, ints) =
    3.77 -      (case find_first (match [@{const of_nat (int)}]) vs of
    3.78 -        NONE => (NONE, [])
    3.79 -      | SOME (_, cases) =>
    3.80 -          let val (cs, (_, e)) = split_last cases
    3.81 -          in (SOME e, map (apfst hd) cs) end)
    3.82 -
    3.83 -    fun nat_of @{typ nat} (v as Value _) =
    3.84 -          AList.lookup (op =) ints v |> the_default (the_default v default_int)
    3.85 -      | nat_of _ e = e
    3.86 -
    3.87 -    fun subst_nat T k ([], e) =
    3.88 -          let fun app f i = if i <= 0 then I else app f (i-1) o f
    3.89 -          in ([], nat_of (app Term.range_type k T) e) end
    3.90 -      | subst_nat T k (arg :: args, e) =
    3.91 -          subst_nat (Term.range_type T) (k-1) (args, e)
    3.92 -          |> apfst (cons (nat_of (Term.domain_type T) arg))
    3.93 -
    3.94 -    fun subst_nats (v as ((n, k), cases)) =
    3.95 -      (case Symtab.lookup terms n of
    3.96 -        NONE => v
    3.97 -      | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
    3.98 -  in
    3.99 -    map subst_nats vs
   3.100 -    |> filter_out (match [@{const of_nat (int)}, @{const nat}])
   3.101 -  end
   3.102 -
   3.103 -fun filter_valid_valuations terms = map_filter (fn
   3.104 -    (_, []) => NONE
   3.105 -  | ((n, i), cases) =>
   3.106 -      let
   3.107 -        fun valid_expr (Array a) = valid_array a
   3.108 -          | valid_expr (App (n, es)) =
   3.109 -              Symtab.defined terms n andalso forall valid_expr es
   3.110 -          | valid_expr _ = true
   3.111 -        and valid_array (Fresh e) = valid_expr e
   3.112 -          | valid_array (Store ((a, e1), e2)) =
   3.113 -              valid_array a andalso valid_expr e1 andalso valid_expr e2
   3.114 -        fun valid_case (es, e) = forall valid_expr (e :: es)
   3.115 -      in
   3.116 -        if not (forall valid_case cases) then NONE
   3.117 -        else Option.map (rpair cases o rpair i) (Symtab.lookup terms n)
   3.118 -      end)
   3.119 -
   3.120 -end
   3.121 +  |> map_filter (annotate terms)
   3.122  
   3.123  
   3.124  (* translation into terms *)
   3.125  
   3.126 -fun with_context ctxt terms f vs =
   3.127 -  fst (fold_map f vs (ctxt, terms, Inttab.empty))
   3.128 +fun max_value vs =
   3.129 +  let
   3.130 +    fun max_val_expr (Value i) = Integer.max i
   3.131 +      | max_val_expr (App (_, es)) = fold max_val_expr es
   3.132 +      | max_val_expr (Array a) = max_val_array a
   3.133 +      | max_val_expr _ = I
   3.134  
   3.135 -fun fresh_term T (ctxt, terms, values) =
   3.136 -  let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
   3.137 -  in (Free (n, T), (ctxt', terms, values)) end
   3.138 +    and max_val_array (Fresh e) = max_val_expr e
   3.139 +      | max_val_array (Store ((a, e1), e2)) =
   3.140 +          max_val_array a #> max_val_expr e1 #> max_val_expr e2
   3.141  
   3.142 -fun term_of_value T i (cx as (_, _, values)) =
   3.143 -  (case Inttab.lookup values i of
   3.144 -    SOME t => (t, cx)
   3.145 +    fun max_val (_, (ec, cs)) =
   3.146 +      max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs
   3.147 +
   3.148 +  in fold max_val vs ~1 end
   3.149 +
   3.150 +fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1))
   3.151 +
   3.152 +fun get_term n T es (cx as (terms, next_val)) =
   3.153 +  (case Symtab.lookup terms n of
   3.154 +    SOME t => ((t, es), cx)
   3.155    | NONE =>
   3.156 -      let val (t, (ctxt', terms', values')) = fresh_term T cx
   3.157 -      in (t, (ctxt', terms', Inttab.update (i, t) values')) end)
   3.158 -
   3.159 -fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
   3.160 +      let val t = Var (("fresh", next_val), T)
   3.161 +      in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
   3.162  
   3.163  fun trans_expr _ True = pair @{const True}
   3.164    | trans_expr _ False = pair @{const False}
   3.165 @@ -188,18 +122,16 @@
   3.166    | trans_expr T (Number (i, SOME j)) =
   3.167        pair (Const (@{const_name divide}, [T, T] ---> T) $
   3.168          HOLogic.mk_number T i $ HOLogic.mk_number T j)
   3.169 -  | trans_expr T (Value i) = term_of_value T i
   3.170 +  | trans_expr T (Value i) = pair (Var (("value", i), T))
   3.171    | trans_expr T (Array a) = trans_array T a
   3.172 -  | trans_expr _ (App (n, es)) =
   3.173 -      let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of
   3.174 +  | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
   3.175 +      let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t))
   3.176        in
   3.177 -        get_term n #-> (fn t =>
   3.178 -        fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>>
   3.179 -        Term.list_comb o pair t)
   3.180 -      end
   3.181 +        fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
   3.182 +      end)
   3.183  
   3.184  and trans_array T a =
   3.185 -  let val dT = Term.domain_type T and rT = Term.range_type T
   3.186 +  let val (dT, rT) = U.split_type T
   3.187    in
   3.188      (case a of
   3.189        Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
   3.190 @@ -232,35 +164,131 @@
   3.191  fun mk_lambda Ts (t, pats) =
   3.192    fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
   3.193  
   3.194 -fun translate' T i [([], e)] =
   3.195 -      if i = 0 then trans_expr T e
   3.196 -      else 
   3.197 -        let val ((Us1, Us2), U) = Term.strip_type T |>> chop i
   3.198 -        in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end
   3.199 -  | translate' T i cases =
   3.200 -      let
   3.201 -        val (pat_cases, def) = split_last cases |> apsnd snd
   3.202 -        val ((Us1, Us2), U) = Term.strip_type T |>> chop i
   3.203 -      in
   3.204 -        trans_expr (Us2 ---> U) def ##>>
   3.205 -        fold_map (trans_pattern T) pat_cases #>>
   3.206 -        mk_lambda Us1
   3.207 -      end
   3.208 +fun translate ((t, k), (e, cs)) =
   3.209 +  let
   3.210 +    val T = Term.fastype_of t
   3.211 +    val (Us, U) = U.dest_funT k (Term.fastype_of t)
   3.212 +
   3.213 +    fun mk_full_def u' pats =
   3.214 +      pats
   3.215 +      |> filter_out (fn (_, u) => u aconv u')
   3.216 +      |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u'
   3.217 +
   3.218 +    fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u)
   3.219 +    fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')]
   3.220 +      | mk_eqs _ pats = map mk_eq pats
   3.221 +  in
   3.222 +    trans_expr U e ##>>
   3.223 +    (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>>
   3.224 +    (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats))
   3.225 +  end
   3.226 +
   3.227 +
   3.228 +(* normalization *)
   3.229 +
   3.230 +fun partition_eqs f =
   3.231 +  let
   3.232 +    fun part t (xs, ts) =
   3.233 +      (case try HOLogic.dest_eq t of
   3.234 +        SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts))
   3.235 +      | NONE => (xs, t :: ts))
   3.236 +  in (fn ts => fold part ts ([], [])) end
   3.237 +
   3.238 +fun replace_vars tab =
   3.239 +  let
   3.240 +    fun replace (v as Var _) = the_default v (AList.lookup (op aconv) tab v)
   3.241 +      | replace t = t
   3.242 +  in map (Term.map_aterms replace) end
   3.243 +
   3.244 +fun remove_int_nat_coercions (eqs, defs) =
   3.245 +  let
   3.246 +    fun mk_nat_num t i =
   3.247 +      (case try HOLogic.dest_number i of
   3.248 +        SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n)
   3.249 +      | NONE => NONE)
   3.250 +    fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i
   3.251 +      | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i
   3.252 +      | nat_of _ _ = NONE
   3.253 +    val (nats, eqs') = partition_eqs nat_of eqs
   3.254  
   3.255 -fun translate ((t, i), cases) =
   3.256 -  translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t
   3.257 +    fun is_coercion t =
   3.258 +      (case try HOLogic.dest_eq t of
   3.259 +        SOME (@{const of_nat (int)}, _) => true
   3.260 +      | SOME (@{const nat}, _) => true
   3.261 +      | _ => false)
   3.262 +  in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end
   3.263 +
   3.264 +fun unfold_funapp (eqs, defs) =
   3.265 +  let
   3.266 +    fun unfold_app (Const (@{const_name SMT.fun_app}, _) $ f $ t) = f $ t
   3.267 +      | unfold_app t = t
   3.268 +    fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =
   3.269 +          eq $ unfold_app t $ u
   3.270 +      | unfold_eq t = t
   3.271 +
   3.272 +    fun is_fun_app t =
   3.273 +      (case try HOLogic.dest_eq t of
   3.274 +        SOME (Const (@{const_name SMT.fun_app}, _), _) => true
   3.275 +      | _ => false)
   3.276 +
   3.277 +  in (map unfold_eq eqs, filter_out is_fun_app defs) end
   3.278 +
   3.279 +fun unfold_simple_eqs (eqs, defs) =
   3.280 +  let
   3.281 +    fun add_rewr (l as Const _) (r as Var _) = SOME (r, l)
   3.282 +      | add_rewr (l as Free _) (r as Var _) = SOME (r, l)
   3.283 +      | add_rewr _ _ = NONE
   3.284 +    val (rs, eqs') = partition_eqs add_rewr eqs
   3.285 +
   3.286 +    fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
   3.287 +      | is_trivial _ = false
   3.288 +  in pairself (replace_vars rs #> filter_out is_trivial) (eqs', defs) end
   3.289 +
   3.290 +fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
   3.291 +      eq $ u $ t
   3.292 +  | swap_free t = t
   3.293 +
   3.294 +fun frees_for_vars ctxt (eqs, defs) =
   3.295 +  let
   3.296 +    fun fresh_free i T (cx as (frees, ctxt)) =
   3.297 +      (case Inttab.lookup frees i of
   3.298 +        SOME t => (t, cx)
   3.299 +      | NONE =>
   3.300 +          let
   3.301 +            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
   3.302 +            val t = Free (n, T)
   3.303 +          in (t, (Inttab.update (i, t) frees, ctxt')) end)
   3.304 +
   3.305 +    fun repl_var (Var ((_, i), T)) = fresh_free i T
   3.306 +      | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $
   3.307 +      | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t'))
   3.308 +      | repl_var t = pair t
   3.309 +  in
   3.310 +    (Inttab.empty, ctxt)
   3.311 +    |> fold_map repl_var eqs
   3.312 +    ||>> fold_map repl_var defs
   3.313 +    |> fst
   3.314 +  end
   3.315  
   3.316  
   3.317  (* overall procedure *)
   3.318  
   3.319 +val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
   3.320 +
   3.321 +fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
   3.322 +  | is_const_def _ = false
   3.323 +
   3.324  fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
   3.325 -  read_cex ls
   3.326 -  |> map_filter reduce_function
   3.327 -  |> drop_skolem_constants terms
   3.328 -  |> substitute_constants terms
   3.329 -  |> remove_int_nat_coercions terms
   3.330 -  |> filter_valid_valuations terms
   3.331 -  |> with_context ctxt terms translate
   3.332 +  read_cex terms ls
   3.333 +  |> with_context terms translate
   3.334 +  |> apfst flat o split_list
   3.335 +  |> remove_int_nat_coercions
   3.336 +  |> unfold_funapp
   3.337 +  |> unfold_simple_eqs
   3.338 +  |>> map swap_free
   3.339 +  |>> filter is_free_constraint
   3.340 +  |> frees_for_vars ctxt
   3.341 +  ||> filter is_const_def
   3.342  
   3.343  end
   3.344