author | wenzelm |
Wed, 04 Mar 2015 22:05:01 +0100 | |
changeset 59586 | ddf6deaadfe8 |
parent 58825 | 2065f49da190 |
child 59621 | 291934bac95e |
permissions | -rw-r--r-- |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
1 |
(* Title: HOL/Library/Old_SMT/old_smt_real.ML |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
3 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
4 |
SMT setup for reals. |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
5 |
*) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
6 |
|
58825 | 7 |
structure Old_SMT_Real: sig end = |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
8 |
struct |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
9 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
10 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
11 |
(* SMT-LIB logic *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
12 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
13 |
fun smtlib_logic ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
14 |
if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
15 |
then SOME "AUFLIRA" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
16 |
else NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
17 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
18 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40579
diff
changeset
|
19 |
(* SMT-LIB and Z3 built-ins *) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
20 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
21 |
local |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40579
diff
changeset
|
22 |
fun real_num _ i = SOME (string_of_int i ^ ".0") |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
23 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
24 |
fun is_linear [t] = Old_SMT_Utils.is_number t |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
25 |
| is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
26 |
| is_linear _ = false |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
27 |
|
41281
679118e35378
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset
|
28 |
fun mk_times ts = Term.list_comb (@{const times (real)}, ts) |
679118e35378
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset
|
29 |
|
58057 | 30 |
fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
31 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
32 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40579
diff
changeset
|
33 |
val setup_builtins = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
34 |
Old_SMT_Builtin.add_builtin_typ Old_SMTLIB_Interface.smtlibC |
41439
a31c451183e6
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41302
diff
changeset
|
35 |
(@{typ real}, K (SOME "Real"), real_num) #> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
36 |
fold (Old_SMT_Builtin.add_builtin_fun' Old_SMTLIB_Interface.smtlibC) [ |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
37 |
(@{const less (real)}, "<"), |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
38 |
(@{const less_eq (real)}, "<="), |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40579
diff
changeset
|
39 |
(@{const uminus (real)}, "~"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40579
diff
changeset
|
40 |
(@{const plus (real)}, "+"), |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
41 |
(@{const minus (real)}, "-") ] #> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
42 |
Old_SMT_Builtin.add_builtin_fun Old_SMTLIB_Interface.smtlibC |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset
|
43 |
(Term.dest_Const @{const times (real)}, times) #> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
44 |
Old_SMT_Builtin.add_builtin_fun' Old_Z3_Interface.smtlib_z3C |
41439
a31c451183e6
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41302
diff
changeset
|
45 |
(@{const times (real)}, "*") #> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
46 |
Old_SMT_Builtin.add_builtin_fun' Old_Z3_Interface.smtlib_z3C |
41439
a31c451183e6
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41302
diff
changeset
|
47 |
(@{const divide (real)}, "/") |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
48 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
49 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
50 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
51 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
52 |
(* Z3 constructors *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
53 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
54 |
local |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
55 |
fun z3_mk_builtin_typ (Old_Z3_Interface.Sym ("Real", _)) = SOME @{typ real} |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
56 |
| z3_mk_builtin_typ (Old_Z3_Interface.Sym ("real", _)) = SOME @{typ real} |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
57 |
(*FIXME: delete*) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
58 |
| z3_mk_builtin_typ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
59 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
60 |
fun z3_mk_builtin_num _ i T = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
61 |
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
62 |
else NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
63 |
|
47965
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset
|
64 |
fun mk_nary _ cu [] = cu |
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset
|
65 |
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset
|
66 |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
41691
diff
changeset
|
67 |
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) |
47965
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset
|
68 |
val add = Thm.cterm_of @{theory} @{const plus (real)} |
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset
|
69 |
val real0 = Numeral.mk_cnumber @{ctyp real} 0 |
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
70 |
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
71 |
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
72 |
val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
73 |
val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset
|
74 |
val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
75 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
76 |
fun z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
77 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("+", _)) cts = |
47965
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset
|
78 |
SOME (mk_nary add real0 cts) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
79 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
80 |
SOME (mk_sub ct cu) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
81 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("*", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
82 |
SOME (mk_mul ct cu) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
83 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("/", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
84 |
SOME (mk_div ct cu) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
85 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("<", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
86 |
SOME (mk_lt ct cu) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
87 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym ("<=", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
88 |
SOME (mk_le ct cu) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
89 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym (">", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
90 |
SOME (mk_lt cu ct) |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
91 |
| z3_mk_builtin_fun (Old_Z3_Interface.Sym (">=", _)) [ct, cu] = |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41439
diff
changeset
|
92 |
SOME (mk_le cu ct) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
93 |
| z3_mk_builtin_fun _ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
94 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
95 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
96 |
val z3_mk_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
97 |
mk_builtin_typ = z3_mk_builtin_typ, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
98 |
mk_builtin_num = z3_mk_builtin_num, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
99 |
mk_builtin_fun = (fn _ => fn sym => fn cts => |
59586 | 100 |
(case try (Thm.typ_of_cterm o hd) cts of |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
101 |
SOME @{typ real} => z3_mk_builtin_fun sym cts |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
102 |
| _ => NONE)) } |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
103 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
104 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
105 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
106 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
107 |
(* Z3 proof reconstruction *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
108 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
109 |
val real_rules = @{lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
110 |
"0 + (x::real) = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
111 |
"x + 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
112 |
"0 * x = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
113 |
"1 * x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
114 |
"x + y = y + x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
115 |
by auto} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
116 |
|
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
36899
diff
changeset
|
117 |
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47965
diff
changeset
|
118 |
"(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
119 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
120 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
121 |
(* setup *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
122 |
|
58825 | 123 |
val _ = |
124 |
Theory.setup |
|
125 |
(Context.theory_map ( |
|
126 |
Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #> |
|
127 |
setup_builtins #> |
|
128 |
Old_Z3_Interface.add_mk_builtins z3_mk_builtins #> |
|
129 |
fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #> |
|
130 |
Old_Z3_Proof_Tools.add_simproc real_linarith_proc)) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
131 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
132 |
end |