equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/SMT2/z3_new_real.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Z3 setup for reals. |
|
5 *) |
|
6 |
|
7 structure Z3_New_Real: sig end = |
|
8 struct |
|
9 |
|
10 fun real_type_parser (SMTLIB2.Sym "Real", []) = SOME @{typ Real.real} |
|
11 | real_type_parser _ = NONE |
|
12 |
|
13 fun real_term_parser (SMTLIB2.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i) |
|
14 | real_term_parser (SMTLIB2.Sym "/", [t1, t2]) = |
|
15 SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2) |
|
16 | real_term_parser (SMTLIB2.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t) |
|
17 | real_term_parser _ = NONE |
|
18 |
|
19 fun abstract abs t = |
|
20 (case t of |
|
21 (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 => |
|
22 abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2)) |
|
23 | (c as @{term "Real.real :: int => _"}) $ t => |
|
24 abs t #>> (fn u => SOME (c $ u)) |
|
25 | _ => pair NONE) |
|
26 |
|
27 val _ = Theory.setup (Context.theory_map ( |
|
28 SMTLIB2_Proof.add_type_parser real_type_parser #> |
|
29 SMTLIB2_Proof.add_term_parser real_term_parser #> |
|
30 Z3_New_Replay_Methods.add_arith_abstracter abstract)) |
|
31 |
|
32 end; |
|