author | blanchet |
Fri, 04 Dec 2015 14:15:16 +0100 | |
changeset 61782 | 7d754aca6a75 |
parent 61609 | 77b453bd616f |
child 69204 | d5ab1636660b |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/z3_real.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Z3 setup for reals. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
|
58061 | 7 |
structure Z3_Real: sig end = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
|
58061 | 10 |
fun real_type_parser (SMTLIB.Sym "Real", []) = SOME @{typ Real.real} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
| real_type_parser _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
|
58061 | 13 |
fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i) |
14 |
| real_term_parser (SMTLIB.Sym "/", [t1, t2]) = |
|
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
58061
diff
changeset
|
15 |
SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2) |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60352
diff
changeset
|
16 |
| real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Int.of_int :: int => _"} $ t) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
| real_term_parser _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
fun abstract abs t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
(case t of |
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
58061
diff
changeset
|
21 |
(c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2)) |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60352
diff
changeset
|
23 |
| (c as @{term "Int.of_int :: int => _"}) $ t => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
abs t #>> (fn u => SOME (c $ u)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
| _ => pair NONE) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
val _ = Theory.setup (Context.theory_map ( |
58061 | 28 |
SMTLIB_Proof.add_type_parser real_type_parser #> |
29 |
SMTLIB_Proof.add_term_parser real_term_parser #> |
|
30 |
Z3_Replay_Methods.add_arith_abstracter abstract)) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
|
57229 | 32 |
end; |