author | boehmes |
Fri, 12 Nov 2010 15:56:11 +0100 | |
changeset 40516 | 516a367eb38c |
parent 38715 | 6513ea67d95d |
child 40579 | 98ebd2300823 |
permissions | -rw-r--r-- |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/smt_real.ML |
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 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
7 |
signature SMT_REAL = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
8 |
sig |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
9 |
val setup: theory -> theory |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
10 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
11 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
12 |
structure SMT_Real: SMT_REAL = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
13 |
struct |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
14 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
15 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
16 |
(* SMT-LIB logic *) |
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 |
fun smtlib_logic ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
19 |
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
|
20 |
then SOME "AUFLIRA" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
21 |
else NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
22 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
23 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
24 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
25 |
(* SMT-LIB builtins *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
26 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
27 |
local |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
28 |
fun smtlib_builtin_typ @{typ real} = SOME "Real" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
29 |
| smtlib_builtin_typ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
30 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
31 |
fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0") |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
32 |
| smtlib_builtin_num _ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
33 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
34 |
fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
35 |
| smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
36 |
| smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
37 |
| smtlib_builtin_func @{const_name times} ts = SOME ("*", ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
38 |
| smtlib_builtin_func _ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
39 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
40 |
fun smtlib_builtin_pred @{const_name less} = SOME "<" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
41 |
| smtlib_builtin_pred @{const_name less_eq} = SOME "<=" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
42 |
| smtlib_builtin_pred _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
43 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
44 |
fun real_fun T y f x = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
45 |
(case try Term.domain_type T of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
46 |
SOME @{typ real} => f x |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
47 |
| _ => y) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
48 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
49 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
50 |
val smtlib_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
51 |
builtin_typ = smtlib_builtin_typ, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
52 |
builtin_num = smtlib_builtin_num, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
53 |
builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)), |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
54 |
builtin_pred = (fn (n, T) => fn ts => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
55 |
real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)), |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
56 |
is_builtin_pred = (fn n => fn T => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
57 |
real_fun T false (is_some o smtlib_builtin_pred) n) } |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
58 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
59 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
60 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
61 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
62 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
63 |
(* Z3 builtins *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
64 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
65 |
local |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
66 |
fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
67 |
| z3_builtin_fun _ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
68 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
69 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
70 |
val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
71 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
72 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
73 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
74 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
75 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
76 |
(* Z3 constructors *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
77 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
78 |
local |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
79 |
structure I = Z3_Interface |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
80 |
|
40516 | 81 |
fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real} |
82 |
| z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
83 |
| z3_mk_builtin_typ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
84 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
85 |
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
|
86 |
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
|
87 |
else NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
88 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
89 |
val mk_uminus = Thm.capply @{cterm "uminus :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
90 |
val mk_add = Thm.mk_binop @{cterm "op + :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
91 |
val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
92 |
val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
93 |
val mk_div = Thm.mk_binop @{cterm "op / :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
94 |
val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
95 |
val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
96 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
97 |
fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
98 |
| z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
99 |
| z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
100 |
| z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
101 |
| z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
102 |
| z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
103 |
| z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
104 |
| z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
105 |
| z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
106 |
| z3_mk_builtin_fun _ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
107 |
in |
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 z3_mk_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
110 |
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
|
111 |
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
|
112 |
mk_builtin_fun = (fn _ => fn sym => fn cts => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
113 |
(case try (#T o Thm.rep_cterm o hd) cts of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
114 |
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
|
115 |
| _ => NONE)) } |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
116 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
117 |
end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
118 |
|
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 |
(* Z3 proof reconstruction *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
122 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
123 |
val real_rules = @{lemma |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
124 |
"0 + (x::real) = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
125 |
"x + 0 = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
126 |
"0 * x = 0" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
127 |
"1 * x = x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
128 |
"x + y = y + x" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
129 |
by auto} |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
130 |
|
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
|
131 |
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
132 |
"(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
133 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
134 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
135 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
136 |
(* setup *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
137 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
138 |
val setup = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
139 |
Context.theory_map ( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
140 |
SMTLIB_Interface.add_logic smtlib_logic #> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
141 |
SMTLIB_Interface.add_builtins smtlib_builtins #> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
142 |
Z3_Interface.add_builtin_funs z3_builtins #> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
143 |
Z3_Interface.add_mk_builtins z3_mk_builtins #> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
144 |
fold Z3_Proof_Reconstruction.add_z3_rule real_rules #> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
145 |
Z3_Proof_Tools.add_simproc real_linarith_proc) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
146 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset
|
147 |
end |