keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
authorboehmes
Tue Oct 26 11:39:26 2010 +0200 (2010-10-26)
changeset 40161539d07b00e5f
parent 40160 539351451286
child 40162 7f58a9a843c2
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
src/HOL/Tools/SMT/cvc3_solver.ML
src/HOL/Tools/SMT/smt_monomorph.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/yices_solver.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_solver.ML
     1.1 --- a/src/HOL/Tools/SMT/cvc3_solver.ML	Tue Oct 26 11:31:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/cvc3_solver.ML	Tue Oct 26 11:39:26 2010 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    command = {env_var=env_var, remote_name=SOME solver_name},
     1.5    arguments = options,
     1.6    interface = SMTLIB_Interface.interface,
     1.7 -  reconstruct = pair o oracle }
     1.8 +  reconstruct = pair o pair [] o oracle }
     1.9  
    1.10  val setup =
    1.11    Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
     2.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Tue Oct 26 11:31:03 2010 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Tue Oct 26 11:39:26 2010 +0200
     2.3 @@ -6,7 +6,8 @@
     2.4  
     2.5  signature SMT_MONOMORPH =
     2.6  sig
     2.7 -  val monomorph: thm list -> Proof.context -> thm list * Proof.context
     2.8 +  val monomorph: (int * thm) list -> Proof.context ->
     2.9 +    (int * thm) list * Proof.context
    2.10  end
    2.11  
    2.12  structure SMT_Monomorph: SMT_MONOMORPH =
    2.13 @@ -33,9 +34,11 @@
    2.14  fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
    2.15  
    2.16  
    2.17 -fun incr_indexes thms =
    2.18 -  let fun inc thm idx = (Thm.incr_indexes idx thm, Thm.maxidx_of thm + idx + 1)
    2.19 -  in fst (fold_map inc thms 0) end
    2.20 +fun incr_indexes irules =
    2.21 +  let
    2.22 +    fun inc (i, thm) idx =
    2.23 +      ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1)
    2.24 +  in fst (fold_map inc irules 0) end
    2.25  
    2.26  
    2.27  (* Compute all substitutions from the types "Ts" to all relevant
    2.28 @@ -71,7 +74,7 @@
    2.29     (without schematic types) which do not occur in any of the
    2.30     previous rounds. Note that thus no schematic type variables are
    2.31     shared among theorems. *)
    2.32 -fun specialize thy all_grounds new_grounds (thm, scs) =
    2.33 +fun specialize thy all_grounds new_grounds (irule, scs) =
    2.34    let
    2.35      fun spec (subst, consts) next_grounds =
    2.36        [subst]
    2.37 @@ -80,7 +83,7 @@
    2.38        |-> fold_map (apply_subst all_grounds consts)
    2.39    in
    2.40      fold_map spec scs #>> (fn scss =>
    2.41 -    (thm, fold (fold (insert (eq_snd (op =)))) scss []))
    2.42 +    (irule, fold (fold (insert (eq_snd (op =)))) scss []))
    2.43    end
    2.44  
    2.45  
    2.46 @@ -89,16 +92,16 @@
    2.47     computation uses only the constants occurring with schematic type
    2.48     variables in the propositions. To ease comparisons, such sets of
    2.49     costants are always kept in their initial order. *)
    2.50 -fun incremental_monomorph thy limit all_grounds new_grounds ths =
    2.51 +fun incremental_monomorph thy limit all_grounds new_grounds irules =
    2.52    let
    2.53      val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
    2.54      val spec = specialize thy all_grounds' new_grounds
    2.55 -    val (ths', new_grounds') = fold_map spec ths Symtab.empty
    2.56 +    val (irs, new_grounds') = fold_map spec irules Symtab.empty
    2.57    in
    2.58 -    if Symtab.is_empty new_grounds' then ths'
    2.59 +    if Symtab.is_empty new_grounds' then irs
    2.60      else if limit > 0
    2.61 -    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' ths'
    2.62 -    else (warning "SMT: monomorphization limit reached"; ths')
    2.63 +    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' irs
    2.64 +    else (warning "SMT: monomorphization limit reached"; irs)
    2.65    end
    2.66  
    2.67  
    2.68 @@ -137,9 +140,9 @@
    2.69  
    2.70      fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
    2.71  
    2.72 -    fun inst thm subst =
    2.73 +    fun inst (i, thm) subst =
    2.74        let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
    2.75 -      in Thm.instantiate (cTs, []) thm end
    2.76 +      in (i, Thm.instantiate (cTs, []) thm) end
    2.77  
    2.78    in uncurry (map o inst) end
    2.79  
    2.80 @@ -147,7 +150,7 @@
    2.81  fun mono_all ctxt _ [] monos = (monos, ctxt)
    2.82    | mono_all ctxt limit polys monos =
    2.83        let
    2.84 -        fun invent_types thm ctxt =
    2.85 +        fun invent_types (_, thm) ctxt =
    2.86            let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
    2.87            in
    2.88              ctxt
    2.89 @@ -159,7 +162,7 @@
    2.90          val thy = ProofContext.theory_of ctxt'
    2.91  
    2.92          val ths = polys
    2.93 -          |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
    2.94 +          |> map (fn (_, thm) => (thm, [(Vartab.empty, tvar_consts_of thm)]))
    2.95  
    2.96          (* all constant names occurring with schematic types *)
    2.97          val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths []
    2.98 @@ -167,11 +170,11 @@
    2.99          (* all known instances with non-schematic types *)
   2.100          val grounds =
   2.101            Symtab.make (map (rpair []) ns)
   2.102 -          |> fold (add_consts (K true)) monos
   2.103 -          |> fold (add_consts (not o typ_has_tvars)) polys
   2.104 +          |> fold (add_consts (K true) o snd) monos
   2.105 +          |> fold (add_consts (not o typ_has_tvars) o snd) polys
   2.106        in
   2.107          polys
   2.108 -        |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
   2.109 +        |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
   2.110          |> incremental_monomorph thy limit Symtab.empty grounds
   2.111          |> map (apsnd (filter_most_specific thy))
   2.112          |> flat o map2 (instantiate thy) Tenvs
   2.113 @@ -192,9 +195,9 @@
   2.114       The initial set of theorems must not contain any schematic term
   2.115     variables, and the final list of theorems does not contain any
   2.116     schematic type variables anymore. *)
   2.117 -fun monomorph thms ctxt =
   2.118 -  thms
   2.119 -  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of)
   2.120 +fun monomorph irules ctxt =
   2.121 +  irules
   2.122 +  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
   2.123    |>> incr_indexes
   2.124    |-> mono_all ctxt monomorph_limit
   2.125  
     3.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:31:03 2010 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:39:26 2010 +0200
     3.3 @@ -17,9 +17,10 @@
     3.4  
     3.5  signature SMT_NORMALIZE =
     3.6  sig
     3.7 -  type extra_norm = thm list -> Proof.context -> thm list * Proof.context
     3.8 -  val normalize: extra_norm -> bool -> thm list -> Proof.context ->
     3.9 -    thm list * Proof.context
    3.10 +  type extra_norm = (int * thm) list -> Proof.context ->
    3.11 +    (int * thm) list * Proof.context
    3.12 +  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
    3.13 +    (int * thm) list * Proof.context
    3.14    val atomize_conv: Proof.context -> conv
    3.15    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    3.16  end
    3.17 @@ -52,8 +53,8 @@
    3.18      if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    3.19  in
    3.20  fun trivial_distinct ctxt =
    3.21 -  map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    3.22 -    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
    3.23 +  map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    3.24 +    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt)))
    3.25  end
    3.26  
    3.27  
    3.28 @@ -72,8 +73,8 @@
    3.29    val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
    3.30  in
    3.31  fun rewrite_bool_cases ctxt =
    3.32 -  map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    3.33 -    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
    3.34 +  map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    3.35 +    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
    3.36  end
    3.37  
    3.38  
    3.39 @@ -108,8 +109,8 @@
    3.40      Conv.no_conv
    3.41  in
    3.42  fun normalize_numerals ctxt =
    3.43 -  map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
    3.44 -    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
    3.45 +  map (apsnd ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
    3.46 +    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt)))
    3.47  end
    3.48  
    3.49  
    3.50 @@ -117,7 +118,7 @@
    3.51  (* embedding of standard natural number operations into integer operations *)
    3.52  
    3.53  local
    3.54 -  val nat_embedding = @{lemma
    3.55 +  val nat_embedding = map (pair ~1) @{lemma
    3.56      "nat (int n) = n"
    3.57      "i >= 0 --> int (nat i) = i"
    3.58      "i < 0 --> int (nat i) = 0"
    3.59 @@ -179,8 +180,8 @@
    3.60      Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
    3.61  in
    3.62  fun nat_as_int ctxt =
    3.63 -  map ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt)) #>
    3.64 -  exists (uses_nat_int o Thm.prop_of) ?? append nat_embedding
    3.65 +  map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
    3.66 +  exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
    3.67  end
    3.68  
    3.69  
    3.70 @@ -362,12 +363,13 @@
    3.71      if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx)
    3.72      else cx |> f (Thm.cprop_of thm) |>> (fn thm' => Thm.equal_elim thm' thm)
    3.73  in
    3.74 -fun lift_lambdas thms ctxt =
    3.75 +fun lift_lambdas irules ctxt =
    3.76    let
    3.77      val cx = (ctxt, Termtab.empty)
    3.78 +    val (idxs, thms) = split_list irules
    3.79      val (thms', (ctxt', defs)) = fold_map (lift_lm (traverse [])) thms cx
    3.80      val eqs = Termtab.fold (cons o normalize_rule ctxt' o snd) defs []
    3.81 -  in (eqs @ thms', ctxt') end
    3.82 +  in (map (pair ~1) eqs @ (idxs ~~ thms'), ctxt') end
    3.83  end
    3.84  
    3.85  
    3.86 @@ -384,8 +386,8 @@
    3.87      | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts
    3.88      | (Abs (_, _, u), ts) => fold traverse (u :: ts)
    3.89      | (_, ts) => fold traverse ts)
    3.90 -  val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I)
    3.91 -  fun prune_tab tab = Symtab.fold prune tab Symtab.empty
    3.92 +  fun prune tab = Symtab.fold (fn (n, (true, i)) =>
    3.93 +    Symtab.update (n, i) | _ => I) tab Symtab.empty
    3.94  
    3.95    fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    3.96    fun nary_conv conv1 conv2 ct =
    3.97 @@ -395,7 +397,7 @@
    3.98      in conv (Symtab.update (free n, 0) tb) cx end)
    3.99    val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
   3.100  in
   3.101 -fun explicit_application ctxt thms =
   3.102 +fun explicit_application ctxt irules =
   3.103    let
   3.104      fun sub_conv tb ctxt ct =
   3.105        (case Term.strip_comb (Thm.term_of ct) of
   3.106 @@ -423,8 +425,8 @@
   3.107        if not (needs_exp_app tab (Thm.prop_of thm)) then thm
   3.108        else Conv.fconv_rule (sub_conv tab ctxt) thm
   3.109  
   3.110 -    val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty)
   3.111 -  in map (rewrite tab ctxt) thms end
   3.112 +    val tab = prune (fold (traverse o Thm.prop_of o snd) irules Symtab.empty)
   3.113 +  in map (apsnd (rewrite tab ctxt)) irules end
   3.114  end
   3.115  
   3.116  
   3.117 @@ -465,11 +467,11 @@
   3.118          end)
   3.119  in
   3.120  
   3.121 -fun datatype_selectors thms ctxt =
   3.122 +fun datatype_selectors irules ctxt =
   3.123    let
   3.124 -    val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty)
   3.125 +    val ns = Symtab.keys (fold (collect o Thm.prop_of o snd) irules Symtab.empty)
   3.126      val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
   3.127 -  in (thms, fold add_selector cs ctxt) end
   3.128 +  in (irules, fold add_selector cs ctxt) end
   3.129      (* FIXME: also generate hypothetical definitions for the selectors *)
   3.130  
   3.131  end
   3.132 @@ -478,19 +480,20 @@
   3.133  
   3.134  (* combined normalization *)
   3.135  
   3.136 -type extra_norm = thm list -> Proof.context -> thm list * Proof.context
   3.137 +type extra_norm = (int * thm) list -> Proof.context ->
   3.138 +  (int * thm) list * Proof.context
   3.139  
   3.140 -fun with_context f thms ctxt = (f ctxt thms, ctxt)
   3.141 +fun with_context f irules ctxt = (f ctxt irules, ctxt)
   3.142  
   3.143 -fun normalize extra_norm with_datatypes thms ctxt =
   3.144 -  thms
   3.145 +fun normalize extra_norm with_datatypes irules ctxt =
   3.146 +  irules
   3.147    |> trivial_distinct ctxt
   3.148    |> rewrite_bool_cases ctxt
   3.149    |> normalize_numerals ctxt
   3.150    |> nat_as_int ctxt
   3.151    |> rpair ctxt
   3.152    |-> extra_norm
   3.153 -  |-> with_context (fn cx => map (normalize_rule cx))
   3.154 +  |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
   3.155    |-> SMT_Monomorph.monomorph
   3.156    |-> lift_lambdas
   3.157    |-> with_context explicit_application
     4.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:31:03 2010 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:39:26 2010 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4      arguments: string list,
     4.5      interface: interface,
     4.6      reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
     4.7 -      thm * Proof.context }
     4.8 +      (int list * thm) * Proof.context }
     4.9  
    4.10    (*options*)
    4.11    val timeout: int Config.T
    4.12 @@ -30,7 +30,7 @@
    4.13    val select_certificates: string -> Context.generic -> Context.generic
    4.14  
    4.15    (*solvers*)
    4.16 -  type solver = Proof.context -> thm list -> thm
    4.17 +  type solver = Proof.context -> (int * thm) list -> int list * thm
    4.18    type solver_info = Context.generic -> Pretty.T list
    4.19    val add_solver: string * (Proof.context -> solver_config) ->
    4.20      Context.generic -> Context.generic
    4.21 @@ -41,6 +41,10 @@
    4.22    val select_solver: string -> Context.generic -> Context.generic
    4.23    val solver_of: Context.generic -> solver
    4.24  
    4.25 +  (*solver*)
    4.26 +  val smt_solver: Proof.context -> ('a * thm) list -> 'a list * thm
    4.27 +  val smt_filter: Proof.context -> ('a * thm) list -> 'a list * string
    4.28 +
    4.29    (*tactic*)
    4.30    val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
    4.31    val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
    4.32 @@ -66,7 +70,7 @@
    4.33    arguments: string list,
    4.34    interface: interface,
    4.35    reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
    4.36 -    thm * Proof.context }
    4.37 +    (int list * thm) * Proof.context }
    4.38  
    4.39  
    4.40  
    4.41 @@ -177,8 +181,8 @@
    4.42        Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
    4.43    end
    4.44  
    4.45 -fun invoke translate_config comments command arguments thms ctxt =
    4.46 -  thms
    4.47 +fun invoke translate_config comments command arguments irules ctxt =
    4.48 +  irules
    4.49    |> SMT_Translate.translate translate_config ctxt comments
    4.50    ||> tap (trace_recon_data ctxt)
    4.51    |>> run_solver ctxt command arguments
    4.52 @@ -202,16 +206,17 @@
    4.53      |-> SMT_Normalize.normalize extra_norm has_datatypes
    4.54      |-> invoke translate comments command arguments
    4.55      |-> reconstruct
    4.56 -    |-> (fn thm => fn ctxt' => thm
    4.57 +    |-> (fn (idxs, thm) => fn ctxt' => thm
    4.58      |> singleton (ProofContext.export ctxt' ctxt)
    4.59 -    |> discharge_definitions)
    4.60 +    |> discharge_definitions
    4.61 +    |> pair idxs)
    4.62    end
    4.63  
    4.64  
    4.65  
    4.66  (* solver store *)
    4.67  
    4.68 -type solver = Proof.context -> thm list -> thm
    4.69 +type solver = Proof.context -> (int * thm) list -> int list * thm
    4.70  type solver_info = Context.generic -> Pretty.T list
    4.71  
    4.72  structure Solvers = Generic_Data
    4.73 @@ -259,6 +264,29 @@
    4.74  
    4.75  
    4.76  
    4.77 +(* SMT solver *)
    4.78 +
    4.79 +val has_topsort = Term.exists_type (Term.exists_subtype (fn
    4.80 +    TFree (_, []) => true
    4.81 +  | TVar (_, []) => true
    4.82 +  | _ => false))
    4.83 +
    4.84 +fun smt_solver ctxt xrules =
    4.85 +  (* without this test, we would run into problems when atomizing the rules: *)
    4.86 +  if exists (has_topsort o Thm.prop_of o snd) xrules
    4.87 +  then raise SMT "proof state contains the universal sort {}"
    4.88 +  else
    4.89 +    split_list xrules
    4.90 +    ||>> solver_of (Context.Proof ctxt) ctxt o map_index I
    4.91 +    |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =))
    4.92 +
    4.93 +fun smt_filter ctxt xrules =
    4.94 +  (fst (smt_solver ctxt xrules), "")
    4.95 +  handle SMT msg => ([], "SMT: " ^ msg)
    4.96 +       | SMT_COUNTEREXAMPLE _ => ([], "SMT: potential counterexample")
    4.97 +
    4.98 +
    4.99 +
   4.100  (* SMT tactic *)
   4.101  
   4.102  local
   4.103 @@ -279,25 +307,13 @@
   4.104      else (tac ctxt i st
   4.105        handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st
   4.106             | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
   4.107 -
   4.108 -  fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
   4.109 -
   4.110 -  val has_topsort = Term.exists_type (Term.exists_subtype (fn
   4.111 -      TFree (_, []) => true
   4.112 -    | TVar (_, []) => true
   4.113 -    | _ => false))
   4.114  in
   4.115  fun smt_tac' pass_exns ctxt rules =
   4.116    CONVERSION (SMT_Normalize.atomize_conv ctxt)
   4.117    THEN' Tactic.rtac @{thm ccontr}
   4.118    THEN' SUBPROOF (fn {context, prems, ...} =>
   4.119 -    let val thms = rules @ prems
   4.120 -    in
   4.121 -      if exists (has_topsort o Thm.prop_of) thms
   4.122 -      then fail_tac (trace_msg context I)
   4.123 -        "SMT: proof state contains the universal sort {}"
   4.124 -      else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1
   4.125 -    end) ctxt
   4.126 +    let fun solve cx = snd (smt_solver cx (map (pair ()) (rules @ prems)))
   4.127 +    in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt
   4.128  
   4.129  val smt_tac = smt_tac' false
   4.130  end
   4.131 @@ -357,7 +373,8 @@
   4.132  
   4.133  val _ =
   4.134    Outer_Syntax.improper_command "smt_status"
   4.135 -    "show the available SMT solvers and the currently selected solver" Keyword.diag
   4.136 +    "show the available SMT solvers and the currently selected solver"
   4.137 +    Keyword.diag
   4.138      (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
   4.139        print_setup (Context.Proof (Toplevel.context_of state)))))
   4.140  
     5.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Oct 26 11:31:03 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Oct 26 11:39:26 2010 +0200
     5.3 @@ -43,9 +43,9 @@
     5.4      typs: typ Symtab.table,
     5.5      terms: term Symtab.table,
     5.6      unfolds: thm list,
     5.7 -    assms: thm list }
     5.8 +    assms: (int * thm) list }
     5.9  
    5.10 -  val translate: config -> Proof.context -> string list -> thm list ->
    5.11 +  val translate: config -> Proof.context -> string list -> (int * thm) list ->
    5.12      string * recon
    5.13  end
    5.14  
    5.15 @@ -101,7 +101,7 @@
    5.16    typs: typ Symtab.table,
    5.17    terms: term Symtab.table,
    5.18    unfolds: thm list,
    5.19 -  assms: thm list }
    5.20 +  assms: (int * thm) list }
    5.21  
    5.22  
    5.23  
    5.24 @@ -244,8 +244,9 @@
    5.25            else as_term (in_term t)
    5.26        | _ => as_term (in_term t))
    5.27    in
    5.28 -    map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms),
    5.29 -    map (in_form o prop_of) (term_bool :: thms)))
    5.30 +    map (apsnd (normalize ctxt)) #> (fn irules =>
    5.31 +    ((unfold_rules, (~1, term_bool') :: irules),
    5.32 +     map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
    5.33    end
    5.34  
    5.35  
    5.36 @@ -318,7 +319,7 @@
    5.37               (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
    5.38           end)
    5.39  
    5.40 -fun relaxed thms = (([], thms), map prop_of thms)
    5.41 +fun relaxed irules = (([], irules), map (prop_of o snd) irules)
    5.42  
    5.43  fun with_context header f (ths, ts) =
    5.44    let val (us, context) = fold_map f ts empty_context
     6.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:31:03 2010 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:39:26 2010 +0200
     6.3 @@ -30,7 +30,7 @@
     6.4  (** facts about uninterpreted constants **)
     6.5  
     6.6  infix 2 ??
     6.7 -fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms
     6.8 +fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
     6.9  
    6.10  
    6.11  (* pairs *)
    6.12 @@ -40,7 +40,7 @@
    6.13  val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false)
    6.14  val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
    6.15  
    6.16 -val add_pair_rules = exists_pair_type ?? append pair_rules
    6.17 +val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
    6.18  
    6.19  
    6.20  (* function update *)
    6.21 @@ -50,7 +50,7 @@
    6.22  val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
    6.23  val exists_fun_upd = Term.exists_subterm is_fun_upd
    6.24  
    6.25 -val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules
    6.26 +val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
    6.27  
    6.28  
    6.29  (* abs/min/max *)
    6.30 @@ -88,11 +88,11 @@
    6.31  
    6.32  (* include additional facts *)
    6.33  
    6.34 -fun extra_norm has_datatypes thms ctxt =
    6.35 -  thms
    6.36 +fun extra_norm has_datatypes irules ctxt =
    6.37 +  irules
    6.38    |> not has_datatypes ? add_pair_rules
    6.39    |> add_fun_upd_rules
    6.40 -  |> map (unfold_abs_min_max_defs ctxt)
    6.41 +  |> map (apsnd (unfold_abs_min_max_defs ctxt))
    6.42    |> rpair ctxt
    6.43  
    6.44  
     7.1 --- a/src/HOL/Tools/SMT/yices_solver.ML	Tue Oct 26 11:31:03 2010 +0200
     7.2 +++ b/src/HOL/Tools/SMT/yices_solver.ML	Tue Oct 26 11:39:26 2010 +0200
     7.3 @@ -35,7 +35,7 @@
     7.4    command = {env_var=env_var, remote_name=NONE},
     7.5    arguments = options,
     7.6    interface = SMTLIB_Interface.interface,
     7.7 -  reconstruct = pair o oracle }
     7.8 +  reconstruct = pair o pair [] o oracle }
     7.9  
    7.10  val setup =
    7.11    Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
     8.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Oct 26 11:31:03 2010 +0200
     8.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Oct 26 11:39:26 2010 +0200
     8.3 @@ -74,13 +74,13 @@
     8.4      | is_int_div_mod @{term "op mod :: int => _"} = true
     8.5      | is_int_div_mod _ = false
     8.6  
     8.7 -  fun add_div_mod thms =
     8.8 -    if exists (Term.exists_subterm is_int_div_mod o Thm.prop_of) thms
     8.9 -    then [@{thm div_by_z3div}, @{thm mod_by_z3mod}] @ thms
    8.10 -    else thms
    8.11 +  fun add_div_mod irules =
    8.12 +    if exists (Term.exists_subterm is_int_div_mod o Thm.prop_of o snd) irules
    8.13 +    then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules
    8.14 +    else irules
    8.15  
    8.16 -  fun extra_norm' has_datatypes thms =
    8.17 -    SMTLIB_Interface.extra_norm has_datatypes (add_div_mod thms)
    8.18 +  fun extra_norm' has_datatypes =
    8.19 +    SMTLIB_Interface.extra_norm has_datatypes o add_div_mod
    8.20  
    8.21    fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
    8.22      | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
     9.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:31:03 2010 +0200
     9.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:39:26 2010 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4    val add_z3_rule: thm -> Context.generic -> Context.generic
     9.5    val trace_assms: bool Config.T
     9.6    val reconstruct: string list * SMT_Translate.recon -> Proof.context ->
     9.7 -    thm * Proof.context
     9.8 +    (int list * thm) * Proof.context
     9.9    val setup: theory -> theory
    9.10  end
    9.11  
    9.12 @@ -750,7 +750,7 @@
    9.13  
    9.14  fun prove ctxt unfolds assms vars =
    9.15    let
    9.16 -    val assms' = prepare_assms ctxt unfolds assms
    9.17 +    val assms' = prepare_assms ctxt unfolds (map snd assms) (* FIXME *)
    9.18      val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
    9.19  
    9.20      fun step r ps ct (cxp as (cx, ptab)) =
    9.21 @@ -821,7 +821,7 @@
    9.22        | SOME (Proved p) => (p, cxp)
    9.23        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
    9.24  
    9.25 -    fun result (p, (cx, _)) = (thm_of p, cx)
    9.26 +    fun result (p, (cx, _)) = (([], thm_of p), cx) (*FIXME*)
    9.27    in
    9.28      (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
    9.29    end
    10.1 --- a/src/HOL/Tools/SMT/z3_solver.ML	Tue Oct 26 11:31:03 2010 +0200
    10.2 +++ b/src/HOL/Tools/SMT/z3_solver.ML	Tue Oct 26 11:39:26 2010 +0200
    10.3 @@ -72,7 +72,8 @@
    10.4     {command = {env_var=env_var, remote_name=SOME solver_name},
    10.5      arguments = cmdline_options ctxt,
    10.6      interface = Z3_Interface.interface with_datatypes,
    10.7 -    reconstruct = if with_proof then prover else (fn r => `(oracle o pair r))}
    10.8 +    reconstruct =
    10.9 +      if with_proof then prover else (fn r => `(pair [] o oracle o pair r))}
   10.10    end
   10.11  
   10.12  val setup =