removed unused file smt_builtin.ML,
authorboehmes
Tue Oct 27 18:09:11 2009 +0100 (2009-10-27)
changeset 332492b65e9ed2e6e
parent 33248 95478a5b4c05
child 33262 b8d3b7196fe7
removed unused file smt_builtin.ML,
made negative pattern polymorphic (similar to positve pattern)
src/HOL/IsaMakefile
src/HOL/SMT/SMT_Base.thy
src/HOL/SMT/Tools/smt_builtin.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 27 18:01:50 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 27 18:09:11 2009 +0100
     1.3 @@ -1187,12 +1187,11 @@
     1.4  
     1.5  $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy		\
     1.6    SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML	\
     1.7 -  SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML			\
     1.8 -  SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML			\
     1.9 -  SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML			\
    1.10 -  SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML		\
    1.11 -  SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML				\
    1.12 -  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
    1.13 +  SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML              \
    1.14 +  SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML                      \
    1.15 +  SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML                 \
    1.16 +  SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML                     \
    1.17 +  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
    1.18  	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
    1.19  
    1.20  
     2.1 --- a/src/HOL/SMT/SMT_Base.thy	Tue Oct 27 18:01:50 2009 +0100
     2.2 +++ b/src/HOL/SMT/SMT_Base.thy	Tue Oct 27 18:09:11 2009 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4  definition pat :: "'a \<Rightarrow> pattern"
     2.5  where "pat _ = Pattern"
     2.6  
     2.7 -definition nopat :: "bool \<Rightarrow> pattern"
     2.8 +definition nopat :: "'a \<Rightarrow> pattern"
     2.9  where "nopat _ = Pattern"
    2.10  
    2.11  definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
     3.1 --- a/src/HOL/SMT/Tools/smt_builtin.ML	Tue Oct 27 18:01:50 2009 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,78 +0,0 @@
     3.4 -(*  Title:      HOL/SMT/Tools/smt_builtin.ML
     3.5 -    Author:     Sascha Boehme, TU Muenchen
     3.6 -
     3.7 -Tables for built-in symbols.
     3.8 -*)
     3.9 -
    3.10 -signature SMT_BUILTIN =
    3.11 -sig
    3.12 -  type sterm = (SMT_Translate.sym, typ) sterm
    3.13 -  type builtin_fun = typ -> sterm list -> (string * sterm list) option
    3.14 -  type table = (typ * builtin_fun) list Symtab.table
    3.15 -
    3.16 -  val make: (term * string) list -> table
    3.17 -  val add: term * builtin_fun -> table -> table
    3.18 -  val lookup: table -> theory -> string * typ -> sterm list ->
    3.19 -    (string * sterm list) option
    3.20 -
    3.21 -  val bv_rotate: (int -> string) -> builtin_fun
    3.22 -  val bv_extend: (int -> string) -> builtin_fun
    3.23 -  val bv_extract: (int -> int -> string) -> builtin_fun
    3.24 -end
    3.25 -
    3.26 -structure SMT_Builtin: SMT_BUILTIN =
    3.27 -struct
    3.28 -
    3.29 -structure T = SMT_Translate
    3.30 -
    3.31 -type sterm = (SMT_Translate.sym, typ) sterm
    3.32 -type builtin_fun = typ -> sterm list -> (string * sterm list) option
    3.33 -type table = (typ * builtin_fun) list Symtab.table
    3.34 -
    3.35 -fun make entries =
    3.36 -  let
    3.37 -    fun dest (t, bn) =
    3.38 -      let val (n, T) = Term.dest_Const t
    3.39 -      in (n, (Logic.varifyT T, K (pair bn))) end
    3.40 -  in Symtab.make (AList.group (op =) (map dest entries)) end
    3.41 -
    3.42 -fun add (t, f) tab =
    3.43 -  let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
    3.44 -  in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
    3.45 -
    3.46 -fun lookup tab thy (n, T) =
    3.47 -  AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T
    3.48 -
    3.49 -
    3.50 -fun dest_binT T =
    3.51 -  (case T of
    3.52 -    Type (@{type_name "Numeral_Type.num0"}, _) => 0
    3.53 -  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
    3.54 -  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
    3.55 -  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
    3.56 -  | _ => raise TYPE ("dest_binT", [T], []))
    3.57 -
    3.58 -fun dest_wordT T =
    3.59 -  (case T of
    3.60 -    Type (@{type_name "word"}, [T]) => dest_binT T
    3.61 -  | _ => raise TYPE ("dest_wordT", [T], []))
    3.62 -
    3.63 -
    3.64 -val dest_nat = (fn
    3.65 -    SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
    3.66 -  | _ => NONE)
    3.67 -
    3.68 -fun bv_rotate mk_name T ts =
    3.69 -  dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
    3.70 -
    3.71 -fun bv_extend mk_name T ts =
    3.72 -  (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
    3.73 -    (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
    3.74 -  | _ => NONE)
    3.75 -
    3.76 -fun bv_extract mk_name T ts =
    3.77 -  (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
    3.78 -    (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
    3.79 -  | _ => NONE)
    3.80 -
    3.81 -end