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
authorboehmes
Mon Sep 13 06:02:47 2010 +0200 (2010-09-13)
changeset 392985aefb5bc8a93
parent 39297 4f9e933a16e2
child 39300 ad79b89b4351
child 39301 e1bd8a54c40f
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
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_solver.ML
     1.1 --- a/src/HOL/SMT.thy	Fri Sep 10 23:56:35 2010 +0200
     1.2 +++ b/src/HOL/SMT.thy	Mon Sep 13 06:02:47 2010 +0200
     1.3 @@ -241,6 +241,13 @@
     1.4  
     1.5  declare [[ z3_options = "" ]]
     1.6  
     1.7 +text {*
     1.8 +The following configuration option may be used to enable mapping of
     1.9 +HOL datatypes and records to native datatypes provided by Z3.
    1.10 +*}
    1.11 +
    1.12 +declare [[ z3_datatypes = false ]]
    1.13 +
    1.14  
    1.15  
    1.16  subsection {* Schematic rules for Z3 proof reconstruction *}
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Sep 10 23:56:35 2010 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Sep 13 06:02:47 2010 +0200
     2.3 @@ -26,10 +26,12 @@
     2.4      builtin_typ: Proof.context -> typ -> string option,
     2.5      builtin_num: Proof.context -> typ -> int -> string option,
     2.6      builtin_fun: Proof.context -> string * typ -> term list ->
     2.7 -      (string * term list) option }
     2.8 +      (string * term list) option,
     2.9 +    has_datatypes: bool }
    2.10    type sign = {
    2.11      header: string list,
    2.12      sorts: string list,
    2.13 +    dtyps: (string * (string * (string * string) list) list) list list,
    2.14      funcs: (string * (string list * string)) list }
    2.15    type config = {
    2.16      prefixes: prefixes,
    2.17 @@ -79,11 +81,13 @@
    2.18    builtin_typ: Proof.context -> typ -> string option,
    2.19    builtin_num: Proof.context -> typ -> int -> string option,
    2.20    builtin_fun: Proof.context -> string * typ -> term list ->
    2.21 -    (string * term list) option }
    2.22 +    (string * term list) option,
    2.23 +  has_datatypes: bool }
    2.24  
    2.25  type sign = {
    2.26    header: string list,
    2.27    sorts: string list,
    2.28 +  dtyps: (string * (string * (string * string) list) list) list list,
    2.29    funcs: (string * (string list * string)) list }
    2.30  
    2.31  type config = {
    2.32 @@ -248,38 +252,67 @@
    2.33  
    2.34  (* translation from Isabelle terms into SMT intermediate terms *)
    2.35  
    2.36 -val empty_context = (1, Typtab.empty, 1, Termtab.empty)
    2.37 +val empty_context = (1, Typtab.empty, [], 1, Termtab.empty)
    2.38  
    2.39 -fun make_sign header (_, typs, _, terms) = {
    2.40 +fun make_sign header (_, typs, dtyps, _, terms) = {
    2.41    header = header,
    2.42 -  sorts = Typtab.fold (cons o snd) typs [],
    2.43 -  funcs = Termtab.fold (cons o snd) terms [] }
    2.44 +  sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
    2.45 +  funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [],
    2.46 +  dtyps = dtyps }
    2.47  
    2.48 -fun make_recon (unfolds, assms) (_, typs, _, terms) = {
    2.49 -  typs = Symtab.make (map swap (Typtab.dest typs)),
    2.50 +fun make_recon (unfolds, assms) (_, typs, _, _, terms) = {
    2.51 +  typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)),
    2.52 +    (*FIXME: don't drop the datatype information! *)
    2.53    terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
    2.54    unfolds = unfolds,
    2.55    assms = assms }
    2.56  
    2.57  fun string_of_index pre i = pre ^ string_of_int i
    2.58  
    2.59 -fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms)) =
    2.60 -  (case Typtab.lookup typs T of
    2.61 -    SOME s => (s, cx)
    2.62 -  | NONE =>
    2.63 -      let
    2.64 -        val s = string_of_index sort_prefix Tidx
    2.65 -        val typs' = Typtab.update (T, s) typs
    2.66 -      in (s, (Tidx+1, typs', idx, terms)) end)
    2.67 +fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
    2.68 +  let val s = string_of_index sort_prefix Tidx
    2.69 +  in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
    2.70 +
    2.71 +fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
    2.72  
    2.73 -fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms)) =
    2.74 +fun fresh_typ T f cx =
    2.75 +  (case lookup_typ cx T of
    2.76 +    SOME (s, _) => (s, cx)
    2.77 +  | NONE => f T cx)
    2.78 +
    2.79 +fun new_fun func_prefix t ss (Tidx, typs, dtyps, idx, terms) =
    2.80 +  let
    2.81 +    val f = string_of_index func_prefix idx
    2.82 +    val terms' = Termtab.update (revert_types t, (f, ss)) terms
    2.83 +  in (f, (Tidx, typs, dtyps, idx+1, terms')) end
    2.84 +
    2.85 +fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
    2.86    (case Termtab.lookup terms t of
    2.87      SOME (f, _) => (f, cx)
    2.88 -  | NONE =>
    2.89 -      let
    2.90 -        val f = string_of_index func_prefix idx
    2.91 -        val terms' = Termtab.update (revert_types t, (f, ss)) terms
    2.92 -      in (f, (Tidx, typs, idx+1, terms')) end)
    2.93 +  | NONE => new_fun func_prefix t ss cx)
    2.94 +
    2.95 +fun inst_const f Ts t =
    2.96 +  let
    2.97 +    val (n, T) = Term.dest_Const (snd (Type.varify_global [] t))
    2.98 +    val inst = map Term.dest_TVar (snd (Term.dest_Type (f T))) ~~ Ts
    2.99 +  in Const (n, Term_Subst.instantiateT inst T) end
   2.100 +
   2.101 +fun inst_constructor Ts = inst_const Term.body_type Ts
   2.102 +fun inst_selector Ts = inst_const Term.domain_type Ts
   2.103 +
   2.104 +fun lookup_datatype ctxt n Ts = (* FIXME: use Datatype/Record.get_info *)
   2.105 +  if n = @{type_name prod}
   2.106 +  then SOME [
   2.107 +    (Type (n, Ts), [
   2.108 +      (inst_constructor Ts @{term Pair},
   2.109 +        map (inst_selector Ts) [@{term fst}, @{term snd}])])]
   2.110 +  else if n = @{type_name list}
   2.111 +  then SOME [
   2.112 +    (Type (n, Ts), [
   2.113 +      (inst_constructor Ts @{term Nil}, []),
   2.114 +      (inst_constructor Ts @{term Cons},
   2.115 +        map (inst_selector Ts) [@{term hd}, @{term tl}])])]
   2.116 +  else NONE
   2.117  
   2.118  fun relaxed thms = (([], thms), map prop_of thms)
   2.119  
   2.120 @@ -291,12 +324,40 @@
   2.121  fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
   2.122    let
   2.123      val {sort_prefix, func_prefix} = prefixes
   2.124 -    val {builtin_typ, builtin_num, builtin_fun} = builtins
   2.125 +    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
   2.126 +
   2.127 +    fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
   2.128 +      | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
   2.129 +      | transT (T as Type (n, Ts)) =
   2.130 +          (case builtin_typ ctxt T of
   2.131 +            SOME n => pair n
   2.132 +          | NONE => fresh_typ T (fn _ => fn cx =>
   2.133 +              if not has_datatypes then new_typ sort_prefix true T cx
   2.134 +              else
   2.135 +                (case lookup_datatype ctxt n Ts of
   2.136 +                  NONE => new_typ sort_prefix true T cx
   2.137 +                | SOME dts =>
   2.138 +                    let val cx' = new_dtyps dts cx 
   2.139 +                    in (fst (the (lookup_typ cx' T)), cx') end)))
   2.140  
   2.141 -    fun transT T =
   2.142 -      (case builtin_typ ctxt T of
   2.143 -        SOME n => pair n
   2.144 -      | NONE => fresh_typ sort_prefix T)
   2.145 +    and new_dtyps dts cx =
   2.146 +      let
   2.147 +        fun new_decl i t =
   2.148 +          let val (Ts, T) = dest_funT i (Term.fastype_of t)
   2.149 +          in
   2.150 +            fold_map transT Ts ##>> transT T ##>>
   2.151 +            new_fun func_prefix t NONE #>> swap
   2.152 +          end
   2.153 +        fun new_dtyp_decl (con, sels) =
   2.154 +          new_decl (length sels) con ##>> fold_map (new_decl 1) sels #>>
   2.155 +          (fn ((con', _), sels') => (con', map (apsnd snd) sels'))
   2.156 +      in
   2.157 +        cx
   2.158 +        |> fold_map (new_typ sort_prefix false o fst) dts
   2.159 +        ||>> fold_map (fold_map new_dtyp_decl o snd) dts
   2.160 +        |-> (fn (ss, decls) => fn (Tidx, typs, dtyps, idx, terms) =>
   2.161 +              (Tidx, typs, (ss ~~ decls) :: dtyps, idx, terms))
   2.162 +      end
   2.163  
   2.164      fun app n ts = SApp (n, ts)
   2.165  
   2.166 @@ -327,13 +388,13 @@
   2.167                | NONE => transs h T ts))
   2.168        | (h as Free (_, T), ts) => transs h T ts
   2.169        | (Bound i, []) => pair (SVar i)
   2.170 -      | _ => raise TERM ("intermediate", [t]))
   2.171 +      | _ => raise TERM ("smt_translate", [t]))
   2.172  
   2.173      and transs t T ts =
   2.174        let val (Us, U) = dest_funT (length ts) T
   2.175        in
   2.176          fold_map transT Us ##>> transT U #-> (fn Up =>
   2.177 -        fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
   2.178 +        fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
   2.179        end
   2.180    in
   2.181      (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
     3.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 10 23:56:35 2010 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Sep 13 06:02:47 2010 +0200
     3.3 @@ -15,6 +15,7 @@
     3.4    val add_builtins: builtins -> Context.generic -> Context.generic
     3.5    val add_logic: (term list -> string option) -> Context.generic ->
     3.6      Context.generic
     3.7 +  val extra_norm: bool -> SMT_Normalize.extra_norm
     3.8    val interface: SMT_Solver.interface
     3.9  end
    3.10  
    3.11 @@ -87,9 +88,9 @@
    3.12  
    3.13  (* include additional facts *)
    3.14  
    3.15 -fun extra_norm thms ctxt =
    3.16 +fun extra_norm has_datatypes thms ctxt =
    3.17    thms
    3.18 -  |> add_pair_rules
    3.19 +  |> not has_datatypes ? add_pair_rules
    3.20    |> add_fun_upd_rules
    3.21    |> map (unfold_abs_min_max_defs ctxt)
    3.22    |> rpair ctxt
    3.23 @@ -251,13 +252,22 @@
    3.24  fun ssort sorts = sort fast_string_ord sorts
    3.25  fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
    3.26  
    3.27 -fun serialize comments {header, sorts, funcs} ts =
    3.28 +fun sdatatypes decls =
    3.29 +  let
    3.30 +    fun con (n, []) = add n
    3.31 +      | con (n, sels) = par (add n #>
    3.32 +          fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
    3.33 +    fun dtyp (n, decl) = add n #> fold (sep o con) decl
    3.34 +  in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
    3.35 +
    3.36 +fun serialize comments {header, sorts, dtyps, funcs} ts =
    3.37    Buffer.empty
    3.38    |> line (add "(benchmark Isabelle")
    3.39    |> line (add ":status unknown")
    3.40    |> fold (line o add) header
    3.41    |> length sorts > 0 ?
    3.42         line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
    3.43 +  |> fold sdatatypes dtyps
    3.44    |> length funcs > 0 ? (
    3.45         line (add ":extrafuns" #> add " (") #>
    3.46         fold (fn (f, (ss, s)) =>
    3.47 @@ -273,7 +283,7 @@
    3.48  (** interfaces **)
    3.49  
    3.50  val interface = {
    3.51 -  extra_norm = extra_norm,
    3.52 +  extra_norm = extra_norm false,
    3.53    translate = {
    3.54      prefixes = {
    3.55        sort_prefix = "S",
    3.56 @@ -286,7 +296,8 @@
    3.57      builtins = {
    3.58        builtin_typ = builtin_typ,
    3.59        builtin_num = builtin_num,
    3.60 -      builtin_fun = builtin_fun},
    3.61 +      builtin_fun = builtin_fun,
    3.62 +      has_datatypes = false},
    3.63      serialize = serialize}}
    3.64  
    3.65  end
     4.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Sep 10 23:56:35 2010 +0200
     4.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 13 06:02:47 2010 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  sig
     4.5    type builtin_fun = string * typ -> term list -> (string * term list) option
     4.6    val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
     4.7 -  val interface: SMT_Solver.interface
     4.8 +  val interface: bool -> SMT_Solver.interface
     4.9  
    4.10    datatype sym = Sym of string * sym list
    4.11    type mk_builtins = {
    4.12 @@ -68,7 +68,7 @@
    4.13    val {extra_norm, translate} = SMTLIB_Interface.interface
    4.14    val {prefixes, strict, header, builtins, serialize} = translate
    4.15    val {is_builtin_pred, ...}= the strict
    4.16 -  val {builtin_typ, builtin_num, builtin_fun} = builtins
    4.17 +  val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
    4.18  
    4.19    fun is_int_div_mod @{term "op div :: int => _"} = true
    4.20      | is_int_div_mod @{term "op mod :: int => _"} = true
    4.21 @@ -79,7 +79,8 @@
    4.22      then [@{thm div_by_z3div}, @{thm mod_by_z3mod}] @ thms
    4.23      else thms
    4.24  
    4.25 -  fun extra_norm' thms = extra_norm (add_div_mod thms)
    4.26 +  fun extra_norm' has_datatypes thms =
    4.27 +    SMTLIB_Interface.extra_norm has_datatypes (add_div_mod thms)
    4.28  
    4.29    fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
    4.30      | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
    4.31 @@ -94,8 +95,8 @@
    4.32    is_some (z3_builtin_fun' ctxt c ts) orelse 
    4.33    is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
    4.34  
    4.35 -val interface = {
    4.36 -  extra_norm = extra_norm',
    4.37 +fun interface has_datatypes = {
    4.38 +  extra_norm = extra_norm' has_datatypes,
    4.39    translate = {
    4.40      prefixes = prefixes,
    4.41      strict = strict,
    4.42 @@ -103,7 +104,8 @@
    4.43      builtins = {
    4.44        builtin_typ = builtin_typ,
    4.45        builtin_num = builtin_num,
    4.46 -      builtin_fun = z3_builtin_fun'},
    4.47 +      builtin_fun = z3_builtin_fun',
    4.48 +      has_datatypes = has_datatypes},
    4.49      serialize = serialize}}
    4.50  
    4.51  end
     5.1 --- a/src/HOL/Tools/SMT/z3_solver.ML	Fri Sep 10 23:56:35 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/z3_solver.ML	Mon Sep 13 06:02:47 2010 +0200
     5.3 @@ -8,6 +8,7 @@
     5.4  sig
     5.5    val proofs: bool Config.T
     5.6    val options: string Config.T
     5.7 +  val datatypes: bool Config.T
     5.8    val setup: theory -> theory
     5.9  end
    5.10  
    5.11 @@ -19,6 +20,7 @@
    5.12  
    5.13  val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
    5.14  val (options, options_setup) = Attrib.config_string "z3_options" (K "")
    5.15 +val (datatypes, datatypes_setup) = Attrib.config_bool "z3_datatypes" (K false)
    5.16  
    5.17  fun add xs ys = ys @ xs
    5.18  
    5.19 @@ -62,17 +64,21 @@
    5.20  val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
    5.21  
    5.22  fun solver oracle ctxt =
    5.23 -  let val with_proof = Config.get ctxt proofs
    5.24 +  let
    5.25 +    val with_datatypes = Config.get ctxt datatypes
    5.26 +    val with_proof = not with_datatypes andalso Config.get ctxt proofs
    5.27 +                     (* FIXME: implement proof reconstruction for datatypes *)
    5.28    in
    5.29     {command = {env_var=env_var, remote_name=SOME solver_name},
    5.30      arguments = cmdline_options ctxt,
    5.31 -    interface = Z3_Interface.interface,
    5.32 +    interface = Z3_Interface.interface with_datatypes,
    5.33      reconstruct = if with_proof then prover else pair o oracle}
    5.34    end
    5.35  
    5.36  val setup =
    5.37    proofs_setup #>
    5.38    options_setup #>
    5.39 +  datatypes_setup #>
    5.40    Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
    5.41    Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #>
    5.42    Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config))