added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
--- a/src/HOL/IsaMakefile Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/IsaMakefile Wed May 12 23:53:57 2010 +0200
@@ -1245,11 +1245,11 @@
$(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/ROOT.ML SMT/SMT_Base.thy SMT/Z3.thy \
SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \
SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \
+ SMT/Tools/z3_interface.ML SMT/Tools/smt_additional_facts.ML \
SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \
SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \
SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \
- SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML \
- SMT/Tools/smt_additional_facts.ML
+ SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
--- a/src/HOL/SMT/SMT_Base.thy Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy Wed May 12 23:53:57 2010 +0200
@@ -106,26 +106,13 @@
text {*
Some SMT solver formats require a strict separation between formulas and terms.
-The following marker symbols are used internally to separate those categories:
+During normalization, all uninterpreted constants are treated as function
+symbols, and atoms (with uninterpreted head symbol) are turned into terms by
+equating them with true using the following term-level equation symbol:
*}
-definition formula :: "bool \<Rightarrow> bool" where "formula x = x"
-definition "term" where "term x = x"
-
-text {*
-Predicate symbols also occurring as function symbols are turned into function
-symbols by translating atomic formulas into terms:
-*}
-
-abbreviation holds :: "bool \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)"
-
-text {*
-The following constant represents equivalence, to be treated differently than
-the (polymorphic) equality predicate:
-*}
-
-definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
- "(x iff y) = (x = y)"
+definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
+ where "(x term_eq y) = (x = y)"
--- a/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Wed May 12 23:53:57 2010 +0200
@@ -9,9 +9,9 @@
numerals),
* embed natural numbers into integers,
* add extra rules specifying types and constants which occur frequently,
+ * fully translate into object logic, add universal closure,
* lift lambda terms,
- * make applications explicit for functions with varying number of arguments,
- * fully translate into object logic, add universal closure.
+ * make applications explicit for functions with varying number of arguments.
*)
signature SMT_NORMALIZE =
@@ -45,28 +45,6 @@
-(* simplification of trivial let expressions (whose bound variables occur at
- most once) *)
-
-local
- fun count i (Bound j) = if j = i then 1 else 0
- | count i (t $ u) = count i t + count i u
- | count i (Abs (_, _, t)) = count (i + 1) t
- | count _ _ = 0
-
- fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) =
- (count 0 t <= 1)
- | is_trivial_let _ = false
-
- fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def})
-in
-fun trivial_let ctxt =
- map ((Term.exists_subterm is_trivial_let o Thm.prop_of) ??
- Conv.fconv_rule (More_Conv.top_conv let_conv ctxt))
-end
-
-
-
(* simplification of trivial distincts (distinct should have at least
three elements in the argument list) *)
@@ -507,7 +485,6 @@
fun normalize ctxt thms =
thms
- |> trivial_let ctxt
|> trivial_distinct ctxt
|> rewrite_bool_cases ctxt
|> normalize_numerals ctxt
--- a/src/HOL/SMT/Tools/smt_solver.ML Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML Wed May 12 23:53:57 2010 +0200
@@ -12,8 +12,7 @@
type proof_data = {
context: Proof.context,
output: string list,
- recon: SMT_Translate.recon,
- assms: thm list option }
+ recon: SMT_Translate.recon }
type solver_config = {
command: {env_var: string, remote_name: string option},
arguments: string list,
@@ -60,8 +59,7 @@
type proof_data = {
context: Proof.context,
output: string list,
- recon: SMT_Translate.recon,
- assms: thm list option }
+ recon: SMT_Translate.recon }
type solver_config = {
command: {env_var: string, remote_name: string option},
@@ -164,8 +162,11 @@
end
-fun make_proof_data ctxt (ls, (recon, thms)) =
- {context=ctxt, output=ls, recon=recon, assms=SOME thms}
+fun invoke translate_config command arguments ctxt thms =
+ thms
+ |> SMT_Translate.translate translate_config ctxt
+ |>> run_solver ctxt command arguments
+ |> (fn (ls, recon) => {context=ctxt, output=ls, recon=recon})
fun gen_solver name solver ctxt prems =
let
@@ -173,14 +174,11 @@
val comments = ("solver: " ^ name) ::
("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
"arguments:" :: arguments
- val tc = interface comments
- val thy = ProofContext.theory_of ctxt
in
SMT_Additional_Facts.add_facts prems
|> SMT_Normalize.normalize ctxt
- ||> SMT_Translate.translate tc thy
- ||> apfst (run_solver ctxt command arguments)
- ||> reconstruct o make_proof_data ctxt
+ ||> invoke (interface comments) command arguments ctxt
+ ||> reconstruct
|-> fold SMT_Normalize.discharge_definition
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/smt_translate.ML Wed May 12 23:53:57 2010 +0200
@@ -0,0 +1,355 @@
+(* Title: HOL/SMT/Tools/smt_translate.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Translate theorems into an SMT intermediate format and serialize them.
+*)
+
+signature SMT_TRANSLATE =
+sig
+ (* intermediate term structure *)
+ datatype squant = SForall | SExists
+ datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
+ datatype sterm =
+ SVar of int |
+ SApp of string * sterm list |
+ SLet of string * sterm * sterm |
+ SQua of squant * string list * sterm spattern list * sterm
+
+ (* configuration options *)
+ type prefixes = {sort_prefix: string, func_prefix: string}
+ type strict = {
+ is_builtin_conn: string * typ -> bool,
+ is_builtin_pred: string * typ -> bool,
+ is_builtin_distinct: bool}
+ type builtins = {
+ builtin_typ: typ -> string option,
+ builtin_num: typ -> int -> string option,
+ builtin_fun: string * typ -> term list -> (string * term list) option }
+ datatype smt_theory = Integer | Real | Bitvector
+ type sign = {
+ theories: smt_theory list,
+ sorts: string list,
+ funcs: (string * (string list * string)) list }
+ type config = {
+ prefixes: prefixes,
+ strict: strict option,
+ builtins: builtins,
+ serialize: sign -> sterm list -> string }
+ type recon = {
+ typs: typ Symtab.table,
+ terms: term Symtab.table,
+ unfolds: thm list,
+ assms: thm list option }
+
+ val translate: config -> Proof.context -> thm list -> string * recon
+end
+
+structure SMT_Translate: SMT_TRANSLATE =
+struct
+
+(* intermediate term structure *)
+
+datatype squant = SForall | SExists
+
+datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
+
+datatype sterm =
+ SVar of int |
+ SApp of string * sterm list |
+ SLet of string * sterm * sterm |
+ SQua of squant * string list * sterm spattern list * sterm
+
+
+
+(* configuration options *)
+
+type prefixes = {sort_prefix: string, func_prefix: string}
+
+type strict = {
+ is_builtin_conn: string * typ -> bool,
+ is_builtin_pred: string * typ -> bool,
+ is_builtin_distinct: bool}
+
+type builtins = {
+ builtin_typ: typ -> string option,
+ builtin_num: typ -> int -> string option,
+ builtin_fun: string * typ -> term list -> (string * term list) option }
+
+datatype smt_theory = Integer | Real | Bitvector
+
+type sign = {
+ theories: smt_theory list,
+ sorts: string list,
+ funcs: (string * (string list * string)) list }
+
+type config = {
+ prefixes: prefixes,
+ strict: strict option,
+ builtins: builtins,
+ serialize: sign -> sterm list -> string }
+
+type recon = {
+ typs: typ Symtab.table,
+ terms: term Symtab.table,
+ unfolds: thm list,
+ assms: thm list option }
+
+
+
+(* utility functions *)
+
+val dest_funT =
+ let
+ fun dest Ts 0 T = (rev Ts, T)
+ | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
+ | dest _ _ T = raise TYPE ("dest_funT", [T], [])
+ in dest [] end
+
+val quantifier = (fn
+ @{const_name All} => SOME SForall
+ | @{const_name Ex} => SOME SExists
+ | _ => NONE)
+
+fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) =
+ if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
+ | group_quant _ Ts t = (Ts, t)
+
+fun dest_pat ts (Const (@{const_name pat}, _) $ t) = SPat (rev (t :: ts))
+ | dest_pat ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (t :: ts))
+ | dest_pat ts (Const (@{const_name andpat}, _) $ p $ t) = dest_pat (t::ts) p
+ | dest_pat _ t = raise TERM ("dest_pat", [t])
+
+fun dest_trigger (@{term trigger} $ tl $ t) =
+ (map (dest_pat []) (HOLogic.dest_list tl), t)
+ | dest_trigger t = ([], t)
+
+fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
+ let
+ val (Ts, u) = group_quant qn [T] t
+ val (ps, b) = dest_trigger u
+ in (q, rev Ts, ps, b) end)
+
+fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
+ | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
+
+fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm)
+
+
+
+(* enforce a strict separation between formulas and terms *)
+
+val term_eq_rewr = @{lemma "x term_eq y == x = y" by (simp add: term_eq_def)}
+
+val term_bool = @{lemma "~(True term_eq False)" by (simp add: term_eq_def)}
+val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
+
+
+val is_let = (fn Const (@{const_name Let}, _) $ _ $ Abs _ => true | _ => false)
+
+val is_true_eq = (fn
+ @{term "op = :: bool => _"} $ _ $ @{term True} => true
+ | _ => false)
+
+val true_eq_rewr = @{lemma "P = True == P" by simp}
+
+val is_trivial_if = (fn
+ Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+ | _ => false)
+
+val trivial_if_rewr = @{lemma "(if P then True else False) == P"
+ by (atomize(full)) simp}
+
+fun rewrite _ ct =
+ if is_trivial_if (Thm.term_of ct) then Conv.rewr_conv trivial_if_rewr ct
+ else if is_true_eq (Thm.term_of ct) then Conv.rewr_conv true_eq_rewr ct
+ else if is_let (Thm.term_of ct) then Conv.rewr_conv @{thm Let_def} ct
+ else Conv.all_conv ct
+
+val needs_rewrite =
+ Term.exists_subterm (is_trivial_if orf is_true_eq orf is_let)
+
+fun normalize ctxt thm =
+ if needs_rewrite (Thm.prop_of thm)
+ then Conv.fconv_rule (More_Conv.top_conv rewrite ctxt) thm
+ else thm
+
+val unfold_rules = [term_eq_rewr, Let_def, trivial_if_rewr, true_eq_rewr]
+
+
+val revert_types =
+ let
+ fun revert @{typ prop} = @{typ bool}
+ | revert (Type (n, Ts)) = Type (n, map revert Ts)
+ | revert T = T
+ in Term.map_types revert end
+
+
+fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
+ let
+
+ fun is_builtin_conn' (@{const_name True}, _) = false
+ | is_builtin_conn' (@{const_name False}, _) = false
+ | is_builtin_conn' c = is_builtin_conn c
+
+ val propT = @{typ prop} and boolT = @{typ bool}
+ val as_propT = (fn @{typ bool} => propT | T => T)
+ fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
+ fun conn (n, T) = (n, mapTs as_propT as_propT T)
+ fun pred (n, T) = (n, mapTs I as_propT T)
+
+ val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
+ fun as_term t = Const term_eq $ t $ @{term True}
+
+ val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
+ fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
+
+ fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
+
+ fun in_term t =
+ (case Term.strip_comb t of
+ (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
+ c $ in_form t1 $ in_term t2 $ in_term t3
+ | (h as Const c, ts) =>
+ if is_builtin_conn' (conn c) orelse is_builtin_pred (pred c)
+ then wrap_in_if (in_form t)
+ else Term.list_comb (h, map in_term ts)
+ | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
+ | _ => t)
+
+ and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
+ | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
+ | in_pat ((c as Const (@{const_name andpat}, _)) $ p $ t) =
+ c $ in_pat p $ in_term t
+ | in_pat t = raise TERM ("in_pat", [t])
+
+ and in_pats p = in_list @{typ pattern} in_pat p
+
+ and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
+ | in_trig t = in_form t
+
+ and in_form t =
+ (case Term.strip_comb t of
+ (q as Const (qn, _), [Abs (n, T, t')]) =>
+ if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
+ else as_term (in_term t)
+ | (Const (c as (@{const_name distinct}, T)), [t']) =>
+ if is_builtin_distinct then Const (pred c) $ in_list T in_term t'
+ else as_term (in_term t)
+ | (Const c, ts) =>
+ if is_builtin_conn (conn c)
+ then Term.list_comb (Const (conn c), map in_form ts)
+ else if is_builtin_pred (pred c)
+ then Term.list_comb (Const (pred c), map in_term ts)
+ else as_term (in_term t)
+ | _ => as_term (in_term t))
+ in
+ map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms),
+ map (in_form o prop_of) (term_bool :: thms)))
+ end
+
+
+
+(* translation from Isabelle terms into SMT intermediate terms *)
+
+val empty_context = (1, Typtab.empty, 1, Termtab.empty, [])
+
+fun make_sign (_, typs, _, terms, thys) = {
+ theories = thys,
+ sorts = Typtab.fold (cons o snd) typs [],
+ funcs = Termtab.fold (cons o snd) terms [] }
+
+fun make_recon (unfolds, assms) (_, typs, _, terms, _) = {
+ typs = Symtab.make (map swap (Typtab.dest typs)),
+ terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
+ unfolds = unfolds,
+ assms = SOME assms }
+
+fun string_of_index pre i = pre ^ string_of_int i
+
+fun add_theory T (Tidx, typs, idx, terms, thys) =
+ let
+ fun add @{typ int} = insert (op =) Integer
+ | add @{typ real} = insert (op =) Real
+ | add (Type (@{type_name word}, _)) = insert (op =) Bitvector
+ | add (Type (_, Ts)) = fold add Ts
+ | add _ = I
+ in (Tidx, typs, idx, terms, add T thys) end
+
+fun fresh_typ sort_prefix T (cx as (Tidx, typs, idx, terms, thys)) =
+ (case Typtab.lookup typs T of
+ SOME s => (s, cx)
+ | NONE =>
+ let
+ val s = string_of_index sort_prefix Tidx
+ val typs' = Typtab.update (T, s) typs
+ in (s, (Tidx+1, typs', idx, terms, thys)) end)
+
+fun fresh_fun func_prefix t ss (cx as (Tidx, typs, idx, terms, thys)) =
+ (case Termtab.lookup terms t of
+ SOME (f, _) => (f, cx)
+ | NONE =>
+ let
+ val f = string_of_index func_prefix idx
+ val terms' = Termtab.update (revert_types t, (f, ss)) terms
+ in (f, (Tidx, typs, idx+1, terms', thys)) end)
+
+fun relaxed thms = (([], thms), map prop_of thms)
+
+fun with_context f (ths, ts) =
+ let val (us, context) = fold_map f ts empty_context
+ in ((make_sign context, us), make_recon ths context) end
+
+
+fun translate {prefixes, strict, builtins, serialize} ctxt =
+ let
+ val {sort_prefix, func_prefix} = prefixes
+ val {builtin_typ, builtin_num, builtin_fun} = builtins
+
+ fun transT T = add_theory T #>
+ (case builtin_typ T of
+ SOME n => pair n
+ | NONE => fresh_typ sort_prefix T)
+
+ fun app n ts = SApp (n, ts)
+
+ fun trans t =
+ (case Term.strip_comb t of
+ (Const (qn, _), [Abs (_, T, t1)]) =>
+ (case dest_quant qn T t1 of
+ SOME (q, Ts, ps, b) =>
+ fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
+ trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
+ | NONE => raise TERM ("intermediate", [t]))
+ | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
+ transT T ##>> trans t1 ##>> trans t2 #>>
+ (fn ((U, u1), u2) => SLet (U, u1, u2))
+ | (h as Const (c as (@{const_name distinct}, T)), [t1]) =>
+ (case builtin_fun c (HOLogic.dest_list t1) of
+ SOME (n, ts) => add_theory T #> fold_map trans ts #>> app n
+ | NONE => transs h T [t1])
+ | (h as Const (c as (_, T)), ts) =>
+ (case try HOLogic.dest_number t of
+ SOME (T, i) =>
+ (case builtin_num T i of
+ SOME n => add_theory T #> pair (SApp (n, []))
+ | NONE => transs t T [])
+ | NONE =>
+ (case builtin_fun c ts of
+ SOME (n, ts') => add_theory T #> fold_map trans ts' #>> app n
+ | NONE => transs h T ts))
+ | (h as Free (_, T), ts) => transs h T ts
+ | (Bound i, []) => pair (SVar i)
+ | _ => raise TERM ("intermediate", [t]))
+
+ and transs t T ts =
+ let val (Us, U) = dest_funT (length ts) T
+ in
+ fold_map transT Us ##>> transT U #-> (fn Up =>
+ fresh_fun func_prefix t Up ##>> fold_map trans ts #>> SApp)
+ end
+ in
+ (if is_some strict then strictify (the strict) ctxt else relaxed) #>
+ with_context trans #>> uncurry serialize
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML Wed May 12 23:53:57 2010 +0200
@@ -0,0 +1,214 @@
+(* Title: HOL/SMT/Tools/smtlib_interface.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Interface to SMT solvers based on the SMT-LIB format.
+*)
+
+signature SMTLIB_INTERFACE =
+sig
+ val interface: string list -> SMT_Translate.config
+end
+
+structure SMTLIB_Interface: SMTLIB_INTERFACE =
+struct
+
+structure T = SMT_Translate
+
+fun dest_binT T =
+ (case T of
+ Type (@{type_name "Numeral_Type.num0"}, _) => 0
+ | Type (@{type_name "Numeral_Type.num1"}, _) => 1
+ | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
+ | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
+ | _ => raise TYPE ("dest_binT", [T], []))
+
+fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
+ | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
+
+
+
+(* builtins *)
+
+fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
+fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
+
+fun builtin_typ @{typ int} = SOME "Int"
+ | builtin_typ @{typ real} = SOME "Real"
+ | builtin_typ (Type (@{type_name word}, [T])) =
+ Option.map (index1 "BitVec") (try dest_binT T)
+ | builtin_typ _ = NONE
+
+fun builtin_num @{typ int} i = SOME (string_of_int i)
+ | builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
+ | builtin_num (Type (@{type_name word}, [T])) i =
+ Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
+ | builtin_num _ _ = NONE
+
+val is_propT = (fn @{typ prop} => true | _ => false)
+fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
+fun is_predT T = is_propT (Term.body_type T)
+
+fun just c ts = SOME (c, ts)
+
+val is_arith_type = member (op =) [@{typ int}, @{typ real}] o Term.domain_type
+
+fun fixed_bvT (Ts, T) x =
+ if forall (can dest_wordT) (T :: Ts) then SOME x else NONE
+
+fun if_fixed_bvT' T = fixed_bvT ([], Term.domain_type T)
+fun if_fixed_bvT T = curry (fixed_bvT ([], Term.domain_type T))
+fun if_full_fixed_bvT T = curry (fixed_bvT (Term.strip_type T))
+
+fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
+ | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
+fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
+ | dest_nat ts = raise TERM ("dest_nat", ts)
+fun dest_nat_word_funT (T, ts) =
+ (dest_word_funT (Term.range_type T), dest_nat ts)
+
+fun bv_extend n T ts =
+ (case try dest_word_funT T of
+ SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
+ | _ => NONE)
+
+fun bv_rotate n T ts =
+ try dest_nat ts
+ |> Option.map (fn (i, ts') => (index1 n i, ts'))
+
+fun bv_extract n T ts =
+ try dest_nat_word_funT (T, ts)
+ |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
+
+
+fun conn @{const_name True} = SOME "true"
+ | conn @{const_name False} = SOME "false"
+ | conn @{const_name Not} = SOME "not"
+ | conn @{const_name "op &"} = SOME "and"
+ | conn @{const_name "op |"} = SOME "or"
+ | conn @{const_name "op -->"} = SOME "implies"
+ | conn @{const_name "op ="} = SOME "iff"
+ | conn @{const_name If} = SOME "if_then_else"
+ | conn _ = NONE
+
+fun pred @{const_name distinct} _ = SOME "distinct"
+ | pred @{const_name "op ="} _ = SOME "="
+ | pred @{const_name term_eq} _ = SOME "="
+ | pred @{const_name less} T =
+ if is_arith_type T then SOME "<"
+ else if_fixed_bvT' T "bvult"
+ | pred @{const_name less_eq} T =
+ if is_arith_type T then SOME "<="
+ else if_fixed_bvT' T "bvule"
+ | pred @{const_name word_sless} T = if_fixed_bvT' T "bvslt"
+ | pred @{const_name word_sle} T = if_fixed_bvT' T "bvsle"
+ | pred _ _ = NONE
+
+fun func @{const_name If} _ = just "ite"
+ | func @{const_name uminus} T =
+ if is_arith_type T then just "~"
+ else if_fixed_bvT T "bvneg"
+ | func @{const_name plus} T =
+ if is_arith_type T then just "+"
+ else if_fixed_bvT T "bvadd"
+ | func @{const_name minus} T =
+ if is_arith_type T then just "-"
+ else if_fixed_bvT T "bvsub"
+ | func @{const_name times} T =
+ if is_arith_type T then just "*"
+ else if_fixed_bvT T "bvmul"
+ | func @{const_name bitNOT} T = if_fixed_bvT T "bvnot"
+ | func @{const_name bitAND} T = if_fixed_bvT T "bvand"
+ | func @{const_name bitOR} T = if_fixed_bvT T "bvor"
+ | func @{const_name bitXOR} T = if_fixed_bvT T "bvxor"
+ | func @{const_name div} T = if_fixed_bvT T "bvudiv"
+ | func @{const_name mod} T = if_fixed_bvT T "bvurem"
+ | func @{const_name sdiv} T = if_fixed_bvT T "bvsdiv"
+ | func @{const_name smod} T = if_fixed_bvT T "bvsmod"
+ | func @{const_name srem} T = if_fixed_bvT T "bvsrem"
+ | func @{const_name word_cat} T = if_full_fixed_bvT T "concat"
+ | func @{const_name bv_shl} T = if_full_fixed_bvT T "bvshl"
+ | func @{const_name bv_lshr} T = if_full_fixed_bvT T "bvlshr"
+ | func @{const_name bv_ashr} T = if_full_fixed_bvT T "bvashr"
+ | func @{const_name slice} T = bv_extract "extract" T
+ | func @{const_name ucast} T = bv_extend "zero_extend" T
+ | func @{const_name scast} T = bv_extend "sign_extend" T
+ | func @{const_name word_rotl} T = bv_rotate "rotate_left" T
+ | func @{const_name word_rotr} T = bv_rotate "rotate_right" T
+ | func _ _ = K NONE
+
+fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
+fun is_builtin_pred (n, T) = is_predT T andalso is_some (pred n T)
+
+fun builtin_fun (n, T) ts =
+ if is_connT T then conn n |> Option.map (rpair ts)
+ else if is_predT T then pred n T |> Option.map (rpair ts)
+ else func n T ts
+
+
+
+(* serialization *)
+
+val add = Buffer.add
+fun sep f = add " " #> f
+fun enclose l r f = sep (add l #> f #> add r)
+val par = enclose "(" ")"
+fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
+fun line f = f #> add "\n"
+
+fun var i = add "?v" #> add (string_of_int i)
+
+fun sterm l (T.SVar i) = sep (var (l - i - 1))
+ | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
+ | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
+ | sterm l (T.SQua (q, ss, ps, t)) =
+ let
+ val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
+ val vs = map_index (apfst (Integer.add l)) ss
+ fun var_decl (i, s) = par (var i #> sep (add s))
+ val sub = sterm (l + length ss)
+ fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
+ fun pats (T.SPat ts) = pat ":pat" ts
+ | pats (T.SNoPat ts) = pat ":nopat" ts
+ in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
+
+fun choose_logic theories =
+ if member (op =) theories T.Bitvector then "QF_AUFBV"
+ else if member (op =) theories T.Real then "AUFLIRA"
+ else "AUFLIA"
+
+fun serialize comments {theories, sorts, funcs} ts =
+ Buffer.empty
+ |> line (add "(benchmark Isabelle")
+ |> line (add ":status unknown")
+ |> line (add ":logic " #> add (choose_logic theories))
+ |> length sorts > 0 ?
+ line (add ":extrasorts" #> par (fold (sep o add) sorts))
+ |> length funcs > 0 ? (
+ line (add ":extrafuns" #> add " (") #>
+ fold (fn (f, (ss, s)) =>
+ line (sep (app f (sep o add) (ss @ [s])))) funcs #>
+ line (add ")"))
+ |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
+ |> line (add ":formula true)")
+ |> fold (fn str => line (add "; " #> add str)) comments
+ |> Buffer.content
+
+
+
+(* interface *)
+
+fun interface comments = {
+ prefixes = {
+ sort_prefix = "S",
+ func_prefix = "f"},
+ strict = SOME {
+ is_builtin_conn = is_builtin_conn,
+ is_builtin_pred = is_builtin_pred,
+ is_builtin_distinct = true},
+ builtins = {
+ builtin_typ = builtin_typ,
+ builtin_num = builtin_num,
+ builtin_fun = builtin_fun},
+ serialize = serialize comments}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/z3_interface.ML Wed May 12 23:53:57 2010 +0200
@@ -0,0 +1,35 @@
+(* Title: HOL/SMT/Tools/z3_interface.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Interface to Z3 based on a relaxed version of SMT-LIB.
+*)
+
+signature Z3_INTERFACE =
+sig
+ val interface: string list -> SMT_Translate.config
+end
+
+structure Z3_Interface: Z3_INTERFACE =
+struct
+
+fun z3_builtin_fun bf c ts =
+ (case Const c of
+ @{term "op / :: real => _"} => SOME ("/", ts)
+ | _ => bf c ts)
+
+fun interface comments =
+ let
+ val {prefixes, strict, builtins, serialize} =
+ SMTLIB_Interface.interface comments
+ val {builtin_typ, builtin_num, builtin_fun} = builtins
+ in
+ {prefixes = prefixes,
+ strict = strict,
+ builtins = {
+ builtin_typ = builtin_typ,
+ builtin_num = builtin_num,
+ builtin_fun = z3_builtin_fun builtin_fun},
+ serialize = serialize}
+ end
+
+end
--- a/src/HOL/SMT/Tools/z3_proof.ML Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_proof.ML Wed May 12 23:53:57 2010 +0200
@@ -6,8 +6,7 @@
signature Z3_PROOF =
sig
- val reconstruct: Proof.context -> thm list option -> SMT_Translate.recon ->
- string list -> thm
+ val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> thm
end
structure Z3_Proof: Z3_PROOF =
@@ -56,13 +55,13 @@
fun make_context (Ttab, ttab, etab, ptab, nctxt) =
Context {Ttab=Ttab, ttab=ttab, etab=etab, ptab=ptab, nctxt=nctxt}
-fun empty_context thy ({typs, terms=ttab} : SMT_Translate.recon) =
+fun empty_context thy ({typs, terms, ...} : SMT_Translate.recon) =
let
- val ttab' = Symtab.map (fn @{term True} => @{term "~False"} | t => t) ttab
- val ns = Symtab.fold (Term.add_free_names o snd) ttab' []
+ val ttab = Symtab.map (fn @{term True} => @{term "~False"} | t => t) terms
+ val ns = Symtab.fold (Term.add_free_names o snd) ttab []
val nctxt = Name.make_context ns
- val tt = Symtab.map (Thm.cterm_of thy) ttab'
- in make_context (typs, tt, Inttab.empty, Inttab.empty, nctxt) end
+ val ttab' = Symtab.map (Thm.cterm_of thy) ttab
+ in make_context (typs, ttab', Inttab.empty, Inttab.empty, nctxt) end
fun map_context f (Context {Ttab, ttab, etab, ptab, nctxt}) =
make_context (f (Ttab, ttab, etab, ptab, nctxt))
@@ -237,14 +236,15 @@
|> handle_errors line_no (Scan.finite' Symbol.stopper (node thy))
|> (fn (stop', (cx', _)) => (stop', line_no + 1, cx'))
-fun reconstruct ctxt assms recon output =
+fun reconstruct ctxt recon output =
let
val _ = T.var_prefix <> free_prefix orelse error "Same prefixes"
val thy = ProofContext.theory_of ctxt
+ val {unfolds, assms, ...} = recon
in
(case fold (parse_line thy) output (NONE, 1, empty_context thy recon) of
- (SOME p, _, Context {ptab, ...}) => R.prove ctxt assms ptab p
+ (SOME p, _, Context {ptab, ...}) => R.prove ctxt unfolds assms ptab p
| _ => z3_exn "bad proof")
end
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Wed May 12 23:53:57 2010 +0200
@@ -14,8 +14,8 @@
(*proof reconstruction*)
type proof
val make_proof: rule -> int list -> cterm * cterm list -> proof
- val prove: Proof.context -> thm list option -> proof Inttab.table -> int ->
- thm
+ val prove: Proof.context -> thm list -> thm list option ->
+ proof Inttab.table -> int -> thm
(*setup*)
val trace_assms: bool Config.T
@@ -479,19 +479,16 @@
Attrib.config_bool "z3_trace_assms" (K false)
local
- val TT_eq = @{lemma "(P = (~False)) == P" by simp}
val remove_trigger = @{lemma "trigger t p == p"
by (rule eq_reflection, rule trigger_def)}
- val remove_iff = @{lemma "p iff q == p = q"
- by (rule eq_reflection, rule iff_def)}
fun with_context simpset ctxt = Simplifier.context ctxt simpset
val prep_ss = with_context (Simplifier.empty_ss addsimps
- [@{thm Let_def}, remove_trigger, remove_iff, true_false, TT_eq])
+ [@{thm Let_def}, remove_trigger, true_false])
- val TT_eq_conv = Conv.rewr_conv TT_eq
- val norm_conv = More_Conv.bottom_conv (K (Conv.try_conv TT_eq_conv))
+ fun norm_conv ctxt unfolds = More_Conv.top_conv
+ (K (Conv.try_conv (More_Conv.rewrs_conv unfolds))) ctxt
val threshold = 10
@@ -513,9 +510,10 @@
val thms = map rewrite assms
in if length assms < threshold then Some thms else Many (thm_net_of thms) end
-fun asserted _ NONE ct = Thm (Thm.assume (T.mk_prop ct))
- | asserted ctxt (SOME assms) ct =
- Thm (with_conv (norm_conv ctxt) (lookup_assm ctxt assms) (T.mk_prop ct))
+fun asserted _ _ NONE ct = Thm (Thm.assume (T.mk_prop ct))
+ | asserted ctxt unfolds (SOME assms) ct =
+ Thm (with_conv (norm_conv ctxt unfolds) (lookup_assm ctxt assms)
+ (T.mk_prop ct))
end
@@ -1326,7 +1324,7 @@
fun not_supported r =
z3_exn ("proof rule not implemented: " ^ quote (string_of_rule r))
-fun prove ctxt assms =
+fun prove ctxt unfolds assms =
let
val prems = Option.map (prepare_assms ctxt) assms
@@ -1334,8 +1332,8 @@
(case (r, ps) of
(* core rules *)
(TrueAxiom, _) => (([], Thm true_thm), ptab)
- | (Asserted, _) => (([], asserted ctxt prems ct), ptab)
- | (Goal, _) => (([], asserted ctxt prems ct), ptab)
+ | (Asserted, _) => (([], asserted ctxt unfolds prems ct), ptab)
+ | (Goal, _) => (([], asserted ctxt unfolds prems ct), ptab)
| (ModusPonens, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
| (ModusPonensOeq, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
| (AndElim, [(p, (_, i))]) => apfst (pair []) (and_elim (p, i) ct ptab)
--- a/src/HOL/SMT/Tools/z3_solver.ML Wed May 12 23:53:56 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_solver.ML Wed May 12 23:53:57 2010 +0200
@@ -61,9 +61,9 @@
check_unsat recon output
|> K @{cprop False}
-fun prover ({context, output, recon, assms} : SMT_Solver.proof_data) =
+fun prover ({context, output, recon} : SMT_Solver.proof_data) =
check_unsat recon output
- |> Z3_Proof.reconstruct context assms recon
+ |> Z3_Proof.reconstruct context recon
fun solver oracle ctxt =
let val with_proof = Config.get ctxt proofs