src/HOL/Library/Old_SMT/old_z3_model.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 59058 a78612c67ec0
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_z3_model.ML
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme and Philipp Meyer, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Parser for counterexamples generated by Z3.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_Z3_MODEL =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     9
  val parse_counterex: Proof.context -> Old_SMT_Translate.recon -> string list ->
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    10
    term list * term list
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    13
structure Old_Z3_Model: OLD_Z3_MODEL =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40627
diff changeset
    16
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
(* counterexample expressions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
datatype expr = True | False | Number of int * int option | Value of int |
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    20
  Array of array | App of string * expr list
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
and array = Fresh of expr | Store of (array * expr) * expr
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
(* parsing *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
val space = Scan.many Symbol.is_ascii_blank
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    27
fun spaced p = p --| space
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    28
fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")")
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    29
fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
val digit = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    36
val nat_num = spaced (Scan.repeat1 (Scan.some digit) >>
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    37
  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0))
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    38
val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    39
  (fn sign => nat_num >> sign))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 40579
diff changeset
    42
  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    43
val name = spaced (Scan.many1 is_char >> implode)
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    44
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    45
fun $$$ s = spaced (Scan.this_string s)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    47
fun array_expr st = st |> in_parens (
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    48
  $$$ "const" |-- expr >> Fresh ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    49
  $$$ "store" |-- array_expr -- expr -- expr >> Store)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    51
and expr st = st |> (
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    52
  $$$ "true" >> K True ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    53
  $$$ "false" >> K False ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    54
  int_num -- Scan.option ($$$ "/" |-- int_num) >> Number ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    55
  $$$ "val!" |-- nat_num >> Value ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    56
  name >> (App o rpair []) ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    57
  array_expr >> Array ||
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    58
  in_parens (name -- Scan.repeat1 expr) >> App)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    60
fun args st = ($$$ "->" >> K [] || expr ::: args) st
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    61
val args_case = args -- expr
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    62
val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
val func =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  let fun cases st = (else_case >> single || args_case ::: cases) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  in in_braces cases end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    68
val cex = space |--
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    69
  Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    71
fun resolve terms ((n, k), cases) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    72
  (case Symtab.lookup terms n of
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    73
    NONE => NONE
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    74
  | SOME t => SOME ((t, k), cases))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    75
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    76
fun annotate _ (_, []) = NONE
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    77
  | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, []))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    78
  | annotate _ (_, [_]) = NONE
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    79
  | annotate terms (n, cases as (args, _) :: _) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    80
      let val (cases', (_, else_case)) = split_last cases
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    81
      in resolve terms ((n, length args), (else_case, cases')) end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    82
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    83
fun read_cex terms ls =
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 40579
diff changeset
    84
  maps (cons "\n" o raw_explode) ls
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
  |> try (fst o Scan.finite Symbol.stopper cex)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
  |> the_default []
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    87
  |> map_filter (annotate terms)
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    88
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
    89
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
(* translation into terms *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    92
fun max_value vs =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    93
  let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    94
    fun max_val_expr (Value i) = Integer.max i
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    95
      | max_val_expr (App (_, es)) = fold max_val_expr es
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    96
      | max_val_expr (Array a) = max_val_array a
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    97
      | max_val_expr _ = I
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
    99
    and max_val_array (Fresh e) = max_val_expr e
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   100
      | max_val_array (Store ((a, e1), e2)) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   101
          max_val_array a #> max_val_expr e1 #> max_val_expr e2
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   103
    fun max_val (_, (ec, cs)) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   104
      max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   105
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   106
  in fold max_val vs ~1 end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   107
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   108
fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   109
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   110
fun get_term n T es (cx as (terms, next_val)) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   111
  (case Symtab.lookup terms n of
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   112
    SOME t => ((t, es), cx)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
  | NONE =>
41058
42e0a0bfef73 more aggressive unfolding of unknowns in Z3 models
boehmes
parents: 40840
diff changeset
   114
      let val t = Var (("skolem", next_val), T)
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   115
      in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40551
diff changeset
   117
fun trans_expr _ True = pair @{const True}
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40551
diff changeset
   118
  | trans_expr _ False = pair @{const False}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
  | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
  | trans_expr T (Number (i, SOME j)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
      pair (Const (@{const_name divide}, [T, T] ---> T) $
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
        HOLogic.mk_number T i $ HOLogic.mk_number T j)
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   123
  | trans_expr T (Value i) = pair (Var (("value", i), T))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
  | trans_expr T (Array a) = trans_array T a
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   125
  | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   126
      let val Ts = fst (Old_SMT_Utils.dest_funT (length es') (Term.fastype_of t))
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   127
      in
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   128
        fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   129
      end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
and trans_array T a =
40840
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40828
diff changeset
   132
  let val (dT, rT) = Term.dest_funT T
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
    (case a of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
      Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
    | Store ((a', e1), e2) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
        trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
        (fn ((m, k), v) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
          Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   142
fun trans_pattern T ([], e) = trans_expr T e #>> pair []
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   143
  | trans_pattern T (arg :: args, e) =
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   144
      trans_expr (Term.domain_type T) arg ##>>
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   145
      trans_pattern (Term.range_type T) (args, e) #>>
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   146
      (fn (arg', (args', e')) => (arg' :: args', e'))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   148
fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   149
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   150
fun mk_update ([], u) _ = u
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   151
  | mk_update ([t], u) f =
40840
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40828
diff changeset
   152
      uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   153
  | mk_update (t :: ts, u) f =
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   154
      let
40840
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40828
diff changeset
   155
        val (dT, rT) = Term.dest_funT (Term.fastype_of f)
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40828
diff changeset
   156
        val (dT', rT') = Term.dest_funT rT
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   157
      in
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   158
        mk_fun_upd dT rT $ f $ t $
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41570
diff changeset
   159
          mk_update (ts, u) (absdummy dT' (Const ("_", rT')))
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   160
      end
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   161
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   162
fun mk_lambda Ts (t, pats) =
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41570
diff changeset
   163
  fold_rev absdummy Ts t |> fold mk_update pats
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   165
fun translate ((t, k), (e, cs)) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   166
  let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   167
    val T = Term.fastype_of t
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   168
    val (Us, U) = Old_SMT_Utils.dest_funT k (Term.fastype_of t)
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   169
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   170
    fun mk_full_def u' pats =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   171
      pats
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   172
      |> filter_out (fn (_, u) => u aconv u')
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   173
      |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u'
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   174
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   175
    fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   176
    fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')]
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   177
      | mk_eqs _ pats = map mk_eq pats
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   178
  in
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   179
    trans_expr U e ##>>
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   180
    (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>>
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   181
    (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   182
  end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   183
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   184
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   185
(* normalization *)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   186
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   187
fun partition_eqs f =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   188
  let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   189
    fun part t (xs, ts) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   190
      (case try HOLogic.dest_eq t of
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   191
        SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   192
      | NONE => (xs, t :: ts))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   193
  in (fn ts => fold part ts ([], [])) end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   194
41122
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   195
fun first_eq pred =
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   196
  let
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   197
    fun part _ [] = NONE
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   198
      | part us (t :: ts) =
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   199
          (case try (pred o HOLogic.dest_eq) t of
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   200
            SOME (SOME lr) => SOME (lr, fold cons us ts)
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   201
          | _ => part (t :: us) ts)
41122
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   202
  in (fn ts => part [] ts) end
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   203
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   204
fun replace_vars tab =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   205
  let
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   206
    fun repl v = the_default v (AList.lookup (op aconv) tab v)
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   207
    fun replace (v as Var _) = repl v
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   208
      | replace (v as Free _) = repl v
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   209
      | replace t = t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   210
  in map (Term.map_aterms replace) end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   211
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   212
fun remove_int_nat_coercions (eqs, defs) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   213
  let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   214
    fun mk_nat_num t i =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   215
      (case try HOLogic.dest_number i of
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   216
        SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   217
      | NONE => NONE)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   218
    fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   219
      | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   220
      | nat_of _ _ = NONE
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   221
    val (nats, eqs') = partition_eqs nat_of eqs
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   222
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   223
    fun is_coercion t =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   224
      (case try HOLogic.dest_eq t of
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   225
        SOME (@{const of_nat (int)}, _) => true
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   226
      | SOME (@{const nat}, _) => true
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   227
      | _ => false)
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58058
diff changeset
   228
  in apply2 (replace_vars nats) (eqs', filter_out is_coercion defs) end
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   229
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   230
fun unfold_funapp (eqs, defs) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   231
  let
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   232
    fun unfold_app (Const (@{const_name fun_app}, _) $ f $ t) = f $ t
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   233
      | unfold_app t = t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   234
    fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   235
          eq $ unfold_app t $ u
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   236
      | unfold_eq t = t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   237
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   238
    fun is_fun_app t =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   239
      (case try HOLogic.dest_eq t of
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   240
        SOME (Const (@{const_name fun_app}, _), _) => true
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   241
      | _ => false)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   242
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   243
  in (map unfold_eq eqs, filter_out is_fun_app defs) end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   244
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   245
val unfold_eqs =
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   246
  let
41122
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   247
    val is_ground = not o Term.exists_subterm Term.is_Var
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   248
    fun is_non_rec (v, t) = not (Term.exists_subterm (equal v) t)
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   249
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   250
    fun rewr_var (l as Var _, r) = if is_ground r then SOME (l, r) else NONE
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   251
      | rewr_var (r, l as Var _) = if is_ground r then SOME (l, r) else NONE
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   252
      | rewr_var _ = NONE
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   253
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   254
    fun rewr_free' e = if is_non_rec e then SOME e else NONE
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   255
    fun rewr_free (e as (Free _, _)) = rewr_free' e
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   256
      | rewr_free (e as (_, Free _)) = rewr_free' (swap e)
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   257
      | rewr_free _ = NONE
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   258
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   259
    fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   260
      | is_trivial _ = false
41058
42e0a0bfef73 more aggressive unfolding of unknowns in Z3 models
boehmes
parents: 40840
diff changeset
   261
41122
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   262
    fun replace r = replace_vars [r] #> filter_out is_trivial
41058
42e0a0bfef73 more aggressive unfolding of unknowns in Z3 models
boehmes
parents: 40840
diff changeset
   263
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   264
    fun unfold_vars (es, ds) =
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   265
      (case first_eq rewr_var es of
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58058
diff changeset
   266
        SOME (lr, es') => unfold_vars (apply2 (replace lr) (es', ds))
41122
72176ec5e031 rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents: 41058
diff changeset
   267
      | NONE => (es, ds))
41058
42e0a0bfef73 more aggressive unfolding of unknowns in Z3 models
boehmes
parents: 40840
diff changeset
   268
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   269
    fun unfold_frees ues (es, ds) =
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   270
      (case first_eq rewr_free es of
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   271
        SOME (lr, es') =>
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58058
diff changeset
   272
          apply2 (replace lr) (es', ds)
41570
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   273
          |> unfold_frees (HOLogic.mk_eq lr :: replace lr ues)
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   274
      | NONE => (ues @ es, ds))
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   275
80c7622a7ff3 normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents: 41328
diff changeset
   276
  in unfold_vars #> unfold_frees [] end
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   277
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   278
fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   279
      eq $ u $ t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   280
  | swap_free t = t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   281
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   282
fun frees_for_vars ctxt (eqs, defs) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   283
  let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   284
    fun fresh_free i T (cx as (frees, ctxt)) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   285
      (case Inttab.lookup frees i of
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   286
        SOME t => (t, cx)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   287
      | NONE =>
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   288
          let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   289
            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   290
            val t = Free (n, T)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   291
          in (t, (Inttab.update (i, t) frees, ctxt')) end)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   292
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   293
    fun repl_var (Var ((_, i), T)) = fresh_free i T
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   294
      | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   295
      | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t'))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   296
      | repl_var t = pair t
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   297
  in
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   298
    (Inttab.empty, ctxt)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   299
    |> fold_map repl_var eqs
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   300
    ||>> fold_map repl_var defs
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   301
    |> fst
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   302
  end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
(* overall procedure *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   307
val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   308
41129
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   309
fun is_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   310
  | is_free_def _ = false
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   311
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   312
fun defined tp =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58058
diff changeset
   313
  try (apply2 (fst o HOLogic.dest_eq)) tp
41129
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   314
  |> the_default false o Option.map (op aconv)
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   315
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   316
fun add_free_defs free_cs defs =
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   317
  let val (free_defs, defs') = List.partition is_free_def defs
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   318
  in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   319
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   320
fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   321
  | is_const_def _ = false
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   322
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   323
fun parse_counterex ctxt ({terms, ...} : Old_SMT_Translate.recon) ls =
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   324
  read_cex terms ls
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   325
  |> with_context terms translate
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   326
  |> apfst flat o split_list
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   327
  |> remove_int_nat_coercions
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   328
  |> unfold_funapp
41058
42e0a0bfef73 more aggressive unfolding of unknowns in Z3 models
boehmes
parents: 40840
diff changeset
   329
  |> unfold_eqs
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   330
  |>> map swap_free
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   331
  |>> filter is_free_constraint
41129
b88cfc0f7456 also show function definitions for higher-order free variables in Z3 models
boehmes
parents: 41122
diff changeset
   332
  |-> add_free_defs
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   333
  |> frees_for_vars ctxt
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40663
diff changeset
   334
  ||> filter is_const_def
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
end
39536
c62359dd253d properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents: 37153
diff changeset
   337