src/HOL/Tools/SMT/smtlib_interface.ML
author boehmes
Mon, 13 Sep 2010 06:02:47 +0200
changeset 39298 5aefb5bc8a93
parent 38864 4abe644fcea5
child 39687 4e9b6ada3a21
permissions -rw-r--r--
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smtlib_interface.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, 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
Interface to SMT solvers based on the SMT-LIB format.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature SMTLIB_INTERFACE =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
     9
  type builtins = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    10
    builtin_typ: typ -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    11
    builtin_num: typ -> int -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    12
    builtin_func: string * typ -> term list -> (string * term list) option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    13
    builtin_pred: string * typ -> term list -> (string * term list) option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    14
    is_builtin_pred: string -> typ -> bool }
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    15
  val add_builtins: builtins -> Context.generic -> Context.generic
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    16
  val add_logic: (term list -> string option) -> Context.generic ->
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    17
    Context.generic
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
    18
  val extra_norm: bool -> SMT_Normalize.extra_norm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  val interface: SMT_Solver.interface
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
structure SMTLIB_Interface: SMTLIB_INTERFACE =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
structure N = SMT_Normalize
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
structure T = SMT_Translate
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
(** facts about uninterpreted constants **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
infix 2 ??
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
(* pairs *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37155
diff changeset
    40
val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
val add_pair_rules = exists_pair_type ?? append pair_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
(* function update *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
val exists_fun_upd = Term.exists_subterm is_fun_upd
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
(* abs/min/max *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
val exists_abs_min_max = Term.exists_subterm (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
    Const (@{const_name abs}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
  | Const (@{const_name min}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
  | Const (@{const_name max}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
37786
4eb98849c5c0 fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents: 37678
diff changeset
    64
val unfold_abs_conv = Conv.rewr_conv (mk_meta_eq @{thm abs_if})
4eb98849c5c0 fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents: 37678
diff changeset
    65
val unfold_min_conv = Conv.rewr_conv (mk_meta_eq @{thm min_def})
4eb98849c5c0 fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents: 37678
diff changeset
    66
val unfold_max_conv = Conv.rewr_conv (mk_meta_eq @{thm max_def})
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
fun expand_conv cv = N.eta_expand_conv (K cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
fun unfold_def_conv ctxt ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
  (case Thm.term_of ct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
    Const (@{const_name abs}, _) $ _ => unfold_abs_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  | Const (@{const_name abs}, _) => expand_conv unfold_abs_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
  | Const (@{const_name min}, _) $ _ $ _ => unfold_min_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
  | Const (@{const_name min}, _) $ _ => expand_conv unfold_min_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
  | Const (@{const_name min}, _) => expand2_conv unfold_min_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  | Const (@{const_name max}, _) $ _ $ _ => unfold_max_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
  | Const (@{const_name max}, _) $ _ => expand_conv unfold_max_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
  | Const (@{const_name max}, _) => expand2_conv unfold_max_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
  | _ => Conv.all_conv) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
fun unfold_abs_min_max_defs ctxt thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
  if exists_abs_min_max (Thm.prop_of thm)
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
    85
  then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
  else thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
(* include additional facts *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
    91
fun extra_norm has_datatypes thms ctxt =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
  thms
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
    93
  |> not has_datatypes ? add_pair_rules
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
  |> add_fun_upd_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
  |> map (unfold_abs_min_max_defs ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
  |> rpair ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
(** builtins **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   102
(* additional builtins *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   104
type builtins = {
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   105
  builtin_typ: typ -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   106
  builtin_num: typ -> int -> string option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   107
  builtin_func: string * typ -> term list -> (string * term list) option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   108
  builtin_pred: string * typ -> term list -> (string * term list) option,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   109
  is_builtin_pred: string -> typ -> bool }
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   111
fun chained _ [] = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   112
  | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   114
fun chained' _ [] = false
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   115
  | chained' f (b :: bs) = f b orelse chained' f bs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   116
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   117
fun chained_builtin_typ bs T =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   118
  chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   120
fun chained_builtin_num bs T i =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   121
  chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   123
fun chained_builtin_func bs c ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   124
  chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   125
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   126
fun chained_builtin_pred bs c ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   127
  chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   129
fun chained_is_builtin_pred bs n T =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   130
  chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   132
fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   134
structure Builtins = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   135
(
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   136
  type T = (int * builtins) list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   137
  val empty = []
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   138
  val extend = I
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   139
  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   140
)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   142
fun add_builtins bs = Builtins.map (OrdList.insert fst_int_ord (serial (), bs))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   144
fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   145
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   146
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   147
(* basic builtins combined with additional builtins *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   148
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   149
fun builtin_typ _ @{typ int} = SOME "Int"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   150
  | builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   152
fun builtin_num _ @{typ int} i = SOME (string_of_int i)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   153
  | builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   155
fun if_int_type T n =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   156
  (case try Term.domain_type T of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   157
    SOME @{typ int} => SOME n
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   158
  | _ => NONE)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
fun conn @{const_name True} = SOME "true"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
  | conn @{const_name False} = SOME "false"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
  | conn @{const_name Not} = SOME "not"
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   163
  | conn @{const_name HOL.conj} = SOME "and"
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38786
diff changeset
   164
  | conn @{const_name HOL.disj} = SOME "or"
38786
e46e7a9cb622 formerly unnamed infix impliciation now named HOL.implies
haftmann
parents: 37786
diff changeset
   165
  | conn @{const_name HOL.implies} = SOME "implies"
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   166
  | conn @{const_name HOL.eq} = SOME "iff"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
  | conn @{const_name If} = SOME "if_then_else"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
  | conn _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
fun pred @{const_name distinct} _ = SOME "distinct"
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   171
  | pred @{const_name HOL.eq} _ = SOME "="
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
  | pred @{const_name term_eq} _ = SOME "="
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   173
  | pred @{const_name less} T = if_int_type T "<"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   174
  | pred @{const_name less_eq} T = if_int_type T "<="
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
  | pred _ _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   177
fun func @{const_name If} _ = SOME "ite"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   178
  | func @{const_name uminus} T = if_int_type T "~"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   179
  | func @{const_name plus} T = if_int_type T "+"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   180
  | func @{const_name minus} T = if_int_type T "-"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   181
  | func @{const_name times} T = if_int_type T "*"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   182
  | func _ _ = NONE
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   183
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   184
val is_propT = (fn @{typ prop} => true | _ => false)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   185
fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   186
fun is_predT T = is_propT (Term.body_type T)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   189
fun is_builtin_pred ctxt (n, T) = is_predT T andalso
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   190
  (is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   192
fun builtin_fun ctxt (c as (n, T)) ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   193
  let
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   194
    val builtin_func' = chained_builtin_func (get_builtins ctxt)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   195
    val builtin_pred' = chained_builtin_pred (get_builtins ctxt)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   196
  in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   197
    if is_connT T then conn n |> Option.map (rpair ts)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   198
    else if is_predT T then
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   199
      (case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   200
    else 
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   201
      (case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   202
  end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
(** serialization **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   208
(* header *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   209
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   210
structure Logics = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   211
(
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   212
  type T = (int * (term list -> string option)) list
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   213
  val empty = []
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   214
  val extend = I
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   215
  fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   216
)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   217
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   218
fun add_logic l = Logics.map (OrdList.insert fst_int_ord (serial (), l))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   219
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   220
fun choose_logic ctxt ts =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   221
  let
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   222
    fun choose [] = "AUFLIA"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   223
      | choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   224
  in [":logic " ^ choose (rev (Logics.get (Context.Proof ctxt)))] end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   225
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   226
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   227
(* serialization *)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   228
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
val add = Buffer.add
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
fun sep f = add " " #> f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
fun enclose l r f = sep (add l #> f #> add r)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
val par = enclose "(" ")"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
fun line f = f #> add "\n"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
fun var i = add "?v" #> add (string_of_int i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
fun sterm l (T.SVar i) = sep (var (l - i - 1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
  | sterm l (T.SQua (q, ss, ps, t)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
        val vs = map_index (apfst (Integer.add l)) ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
        fun var_decl (i, s) = par (var i #> sep (add s))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
        val sub = sterm (l + length ss)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
        fun pats (T.SPat ts) = pat ":pat" ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
          | pats (T.SNoPat ts) = pat ":nopat" ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
      in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
37155
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   252
fun ssort sorts = sort fast_string_ord sorts
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   253
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   254
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   255
fun sdatatypes decls =
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   256
  let
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   257
    fun con (n, []) = add n
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   258
      | con (n, sels) = par (add n #>
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   259
          fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   260
    fun dtyp (n, decl) = add n #> fold (sep o con) decl
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   261
  in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   262
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   263
fun serialize comments {header, sorts, dtyps, funcs} ts =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  Buffer.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  |> line (add "(benchmark Isabelle")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
  |> line (add ":status unknown")
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   267
  |> fold (line o add) header
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
  |> length sorts > 0 ?
37155
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   269
       line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   270
  |> fold sdatatypes dtyps
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
  |> length funcs > 0 ? (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
       line (add ":extrafuns" #> add " (") #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
       fold (fn (f, (ss, s)) =>
37155
e3f18cfc9829 sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents: 36936
diff changeset
   274
         line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
       line (add ")"))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
  |> line (add ":formula true)")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
  |> fold (fn str => line (add "; " #> add str)) comments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
  |> Buffer.content
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   283
(** interfaces **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
val interface = {
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   286
  extra_norm = extra_norm false,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
  translate = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
    prefixes = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
      sort_prefix = "S",
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
      func_prefix = "f"},
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   291
    header = choose_logic,
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
    strict = SOME {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
      is_builtin_conn = is_builtin_conn,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
      is_builtin_pred = is_builtin_pred,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
      is_builtin_distinct = true},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
    builtins = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
      builtin_typ = builtin_typ,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
      builtin_num = builtin_num,
39298
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   299
      builtin_fun = builtin_fun,
5aefb5bc8a93 added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents: 38864
diff changeset
   300
      has_datatypes = false},
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
    serialize = serialize}}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
end