src/HOL/Tools/SMT/smt_real.ML
changeset 41691 8f0531cf34f8
parent 41439 a31c451183e6
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Feb 02 12:34:45 2011 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Feb 02 14:01:09 2011 +0100
     1.3 @@ -58,10 +58,9 @@
     1.4  (* Z3 constructors *)
     1.5  
     1.6  local
     1.7 -  structure I = Z3_Interface
     1.8 -
     1.9 -  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
    1.10 -    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
    1.11 +  fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME @{typ real}
    1.12 +    | z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME @{typ real}
    1.13 +        (*FIXME: delete*)
    1.14      | z3_mk_builtin_typ _ = NONE
    1.15  
    1.16    fun z3_mk_builtin_num _ i T =
    1.17 @@ -76,15 +75,23 @@
    1.18    val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
    1.19    val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    1.20  
    1.21 -  fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.22 -    | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
    1.23 -    | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
    1.24 -    | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
    1.25 -    | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
    1.26 -    | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
    1.27 -    | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
    1.28 -    | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
    1.29 -    | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
    1.30 +  fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.31 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) [ct, cu] =
    1.32 +        SOME (mk_add ct cu)
    1.33 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] =
    1.34 +        SOME (mk_sub ct cu)
    1.35 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] =
    1.36 +        SOME (mk_mul ct cu)
    1.37 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] =
    1.38 +        SOME (mk_div ct cu)
    1.39 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] =
    1.40 +        SOME (mk_lt ct cu)
    1.41 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] =
    1.42 +        SOME (mk_le ct cu)
    1.43 +    | z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] =
    1.44 +        SOME (mk_lt cu ct)
    1.45 +    | z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] =
    1.46 +        SOME (mk_le cu ct)
    1.47      | z3_mk_builtin_fun _ _ = NONE
    1.48  in
    1.49