# HG changeset patch
# User boehmes
# Date 1270665642 -7200
# Node ID 0eaa6905590f21b5e7c37f2d2330c030e73ed583
# Parent  3176ec2244adac58ec69ffb23aa71372fda3a6d6
shortened interface (do not export unused options and functions)

diff -r 3176ec2244ad -r 0eaa6905590f src/HOL/SMT/Tools/smt_normalize.ML
--- a/src/HOL/SMT/Tools/smt_normalize.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -13,25 +13,10 @@
 
 signature SMT_NORMALIZE =
 sig
-  val normalize_rule: Proof.context -> thm -> thm
   val instantiate_free: cterm * cterm -> thm -> thm
   val discharge_definition: cterm -> thm -> thm
 
-  val trivial_let: Proof.context -> thm list -> thm list
-  val positive_numerals: Proof.context -> thm list -> thm list
-  val nat_as_int: Proof.context -> thm list -> thm list
-  val add_pair_rules: Proof.context -> thm list -> thm list
-  val add_fun_upd_rules: Proof.context -> thm list -> thm list
-
-  datatype config =
-    RewriteTrivialLets |
-    RewriteNegativeNumerals |
-    RewriteNaturalNumbers |
-    AddPairRules |
-    AddFunUpdRules
-
-  val normalize: config list -> Proof.context -> thm list ->
-    cterm list * thm list
+  val normalize: Proof.context -> thm list -> cterm list * thm list
 end
 
 structure SMT_Normalize: SMT_NORMALIZE =
@@ -485,25 +470,15 @@
 
 (* combined normalization *)
 
-datatype config =
-  RewriteTrivialLets |
-  RewriteNegativeNumerals |
-  RewriteNaturalNumbers |
-  AddPairRules |
-  AddFunUpdRules
-
-fun normalize config ctxt thms =
-  let fun if_enabled c f = member (op =) config c ? f ctxt
-  in
-    thms
-    |> if_enabled RewriteTrivialLets trivial_let
-    |> if_enabled RewriteNegativeNumerals positive_numerals
-    |> if_enabled RewriteNaturalNumbers nat_as_int
-    |> if_enabled AddPairRules add_pair_rules
-    |> if_enabled AddFunUpdRules add_fun_upd_rules
-    |> map (unfold_defs ctxt #> normalize_rule ctxt)
-    |> lift_lambdas ctxt
-    |> apsnd (explicit_application ctxt)
-  end
+fun normalize ctxt thms =
+  thms
+  |> trivial_let ctxt
+  |> positive_numerals ctxt
+  |> nat_as_int ctxt
+  |> add_pair_rules ctxt
+  |> add_fun_upd_rules ctxt
+  |> map (unfold_defs ctxt #> normalize_rule ctxt)
+  |> lift_lambdas ctxt
+  |> apsnd (explicit_application ctxt)
 
 end
diff -r 3176ec2244ad -r 0eaa6905590f src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -9,9 +9,6 @@
   exception SMT of string
   exception SMT_COUNTEREXAMPLE of bool * term list
 
-  type interface = {
-    normalize: SMT_Normalize.config list,
-    translate: SMT_Translate.config }
   type proof_data = {
     context: Proof.context,
     output: string list,
@@ -20,7 +17,7 @@
   type solver_config = {
     command: {env_var: string, remote_name: string option},
     arguments: string list,
-    interface: string list -> interface,
+    interface: string list -> SMT_Translate.config,
     reconstruct: proof_data -> thm }
 
   (*options*)
@@ -60,10 +57,6 @@
 exception SMT_COUNTEREXAMPLE of bool * term list
 
 
-type interface = {
-  normalize: SMT_Normalize.config list,
-  translate: SMT_Translate.config }
-
 type proof_data = {
   context: Proof.context,
   output: string list,
@@ -73,7 +66,7 @@
 type solver_config = {
   command: {env_var: string, remote_name: string option},
   arguments: string list,
-  interface: string list -> interface,
+  interface: string list -> SMT_Translate.config,
   reconstruct: proof_data -> thm }
 
 
@@ -182,10 +175,10 @@
     val comments = ("solver: " ^ name) ::
       ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
       "arguments:" :: arguments
-    val {normalize=nc, translate=tc} = interface comments
+    val tc = interface comments
     val thy = ProofContext.theory_of ctxt
   in
-    SMT_Normalize.normalize nc ctxt prems
+    SMT_Normalize.normalize ctxt prems
     ||> run_solver ctxt command arguments o SMT_Translate.translate tc thy
     ||> reconstruct o make_proof_data ctxt
     |-> fold SMT_Normalize.discharge_definition
diff -r 3176ec2244ad -r 0eaa6905590f src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -9,8 +9,8 @@
   val basic_builtins: SMT_Translate.builtins
   val default_attributes: string list
   val gen_interface: SMT_Translate.builtins -> string list -> string list ->
-    SMT_Solver.interface
-  val interface: string list -> SMT_Solver.interface
+    SMT_Translate.config
+  val interface: string list -> SMT_Translate.config
 end
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -154,24 +154,17 @@
 val default_attributes = [":logic AUFLIRA"]
 
 fun gen_interface builtins attributes comments = {
-  normalize = [
-    SMT_Normalize.RewriteTrivialLets,
-    SMT_Normalize.RewriteNegativeNumerals,
-    SMT_Normalize.RewriteNaturalNumbers,
-    SMT_Normalize.AddPairRules,
-    SMT_Normalize.AddFunUpdRules ],
-  translate = {
-    strict = true,
-    prefixes = {
-      var_prefix = "x",
-      typ_prefix = "T",
-      fun_prefix = "uf_",
-      pred_prefix = "up_" },
-    markers = {
-      term_marker = term_marker,
-      formula_marker = formula_marker },
-    builtins = builtins,
-    serialize = serialize attributes comments }}
+  strict = true,
+  prefixes = {
+    var_prefix = "x",
+    typ_prefix = "T",
+    fun_prefix = "uf_",
+    pred_prefix = "up_" },
+  markers = {
+    term_marker = term_marker,
+    formula_marker = formula_marker },
+  builtins = builtins,
+  serialize = serialize attributes comments }
 
 fun interface comments =
   gen_interface basic_builtins default_attributes comments
diff -r 3176ec2244ad -r 0eaa6905590f src/HOL/SMT/Tools/z3_interface.ML
--- a/src/HOL/SMT/Tools/z3_interface.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_interface.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -6,7 +6,7 @@
 
 signature Z3_INTERFACE =
 sig
-  val interface: string list -> SMT_Solver.interface
+  val interface: string list -> SMT_Translate.config
 end
 
 structure Z3_Interface: Z3_INTERFACE =