--- 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
--- 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
--- 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
--- 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 =