author | haftmann |
Mon, 01 Jun 2015 18:59:21 +0200 | |
changeset 60352 | d46de31a50c4 |
parent 59634 | 4b94cc030ba0 |
child 63950 | cdc1e59aa513 |
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_z3_interface.ML |
36898 | 2 |
Author: Sascha Boehme, TU Muenchen |
3 |
||
4 |
Interface to Z3 based on a relaxed version of SMT-LIB. |
|
5 |
*) |
|
6 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
7 |
signature OLD_Z3_INTERFACE = |
36898 | 8 |
sig |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
9 |
val smtlib_z3C: Old_SMT_Utils.class |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
10 |
val setup: theory -> theory |
36898 | 11 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
12 |
datatype sym = Sym of string * sym list |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
13 |
type mk_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
14 |
mk_builtin_typ: sym -> typ option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
15 |
mk_builtin_num: theory -> int -> typ -> cterm option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
16 |
mk_builtin_fun: theory -> sym -> cterm list -> cterm option } |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
17 |
val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
18 |
val mk_builtin_typ: Proof.context -> sym -> typ option |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
19 |
val mk_builtin_num: Proof.context -> int -> typ -> cterm option |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
20 |
val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
21 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
22 |
val is_builtin_theory_term: Proof.context -> term -> bool |
36898 | 23 |
end |
24 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
25 |
structure Old_Z3_Interface: OLD_Z3_INTERFACE = |
36898 | 26 |
struct |
27 |
||
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
28 |
val smtlib_z3C = Old_SMTLIB_Interface.smtlibC @ ["z3"] |
36898 | 29 |
|
30 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
31 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
32 |
(* interface *) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
33 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
34 |
local |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
35 |
fun translate_config ctxt = |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
36 |
let |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
37 |
val {prefixes, header, is_fol, serialize, ...} = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
38 |
Old_SMTLIB_Interface.translate_config ctxt |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
39 |
in |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
40 |
{prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize, |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
41 |
has_datatypes=true} |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
42 |
end |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
43 |
|
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59634
diff
changeset
|
44 |
fun is_div_mod @{const divide (int)} = true |
41302
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
45 |
| is_div_mod @{const mod (int)} = true |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
46 |
| is_div_mod _ = false |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
47 |
|
41302
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
48 |
val div_by_z3div = @{lemma |
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
49 |
"ALL k l. k div l = ( |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
50 |
if k = 0 | l = 0 then 0 |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
51 |
else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
52 |
else z3div (-k) (-l))" |
58057 | 53 |
by (simp add: z3div_def)} |
37151 | 54 |
|
41302
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
55 |
val mod_by_z3mod = @{lemma |
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
56 |
"ALL k l. k mod l = ( |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
57 |
if l = 0 then k |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
58 |
else if k = 0 then 0 |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
59 |
else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
60 |
else - z3mod (-k) (-l))" |
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
61 |
by (simp add: z3mod_def)} |
37151 | 62 |
|
41302
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
63 |
val have_int_div_mod = |
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
64 |
exists (Term.exists_subterm is_div_mod o Thm.prop_of) |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
65 |
|
41302
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
66 |
fun add_div_mod _ (thms, extra_thms) = |
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
67 |
if have_int_div_mod thms orelse have_int_div_mod extra_thms then |
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
68 |
(thms, div_by_z3div :: mod_by_z3mod :: extra_thms) |
0485186839a7
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
boehmes
parents:
41280
diff
changeset
|
69 |
else (thms, extra_thms) |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
70 |
|
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
71 |
val setup_builtins = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
72 |
Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #> |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
73 |
Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
74 |
Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
75 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
76 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
77 |
val setup = Context.theory_map ( |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
78 |
setup_builtins #> |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
79 |
Old_SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #> |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
80 |
Old_SMT_Translate.add_config (smtlib_z3C, translate_config)) |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
81 |
|
36898 | 82 |
end |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
83 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
84 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
85 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
86 |
(* constructors *) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
87 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
88 |
datatype sym = Sym of string * sym list |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
89 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
90 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
91 |
(** additional constructors **) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
92 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
93 |
type mk_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
94 |
mk_builtin_typ: sym -> typ option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
95 |
mk_builtin_num: theory -> int -> typ -> cterm option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
96 |
mk_builtin_fun: theory -> sym -> cterm list -> cterm option } |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
97 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
98 |
fun chained _ [] = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
99 |
| chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
100 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
101 |
fun chained_mk_builtin_typ bs sym = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
102 |
chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
103 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
104 |
fun chained_mk_builtin_num ctxt bs i T = |
42361 | 105 |
let val thy = Proof_Context.theory_of ctxt |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
106 |
in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
107 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
108 |
fun chained_mk_builtin_fun ctxt bs s cts = |
42361 | 109 |
let val thy = Proof_Context.theory_of ctxt |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
110 |
in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
111 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
112 |
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
113 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
114 |
structure Mk_Builtins = Generic_Data |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
115 |
( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
116 |
type T = (int * mk_builtins) list |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
117 |
val empty = [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
118 |
val extend = I |
41473 | 119 |
fun merge data = Ord_List.merge fst_int_ord data |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
120 |
) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
121 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
122 |
fun add_mk_builtins mk = |
39687 | 123 |
Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
124 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
125 |
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
126 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
127 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
128 |
(** basic and additional constructors **) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
129 |
|
49720 | 130 |
fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool} |
40516 | 131 |
| mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} |
49720 | 132 |
| mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*) |
133 |
| mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
134 |
| mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
135 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
136 |
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
137 |
| mk_builtin_num ctxt i T = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
138 |
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
139 |
|
59634 | 140 |
val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False}) |
141 |
val mk_false = Thm.cterm_of @{context} @{const False} |
|
142 |
val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not}) |
|
143 |
val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies}) |
|
144 |
val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)}) |
|
145 |
val conj = Thm.cterm_of @{context} @{const HOL.conj} |
|
146 |
val disj = Thm.cterm_of @{context} @{const HOL.disj} |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
147 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
148 |
fun mk_nary _ cu [] = cu |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
149 |
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
150 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
151 |
val eq = Old_SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} Old_SMT_Utils.destT1 |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
152 |
fun mk_eq ct cu = Thm.mk_binop (Old_SMT_Utils.instT' ct eq) ct cu |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
153 |
|
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
154 |
val if_term = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
155 |
Old_SMT_Utils.mk_const_pat @{theory} @{const_name If} |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
156 |
(Old_SMT_Utils.destT1 o Old_SMT_Utils.destT2) |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
157 |
fun mk_if cc ct cu = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
158 |
Thm.mk_binop (Thm.apply (Old_SMT_Utils.instT' ct if_term) cc) ct cu |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
159 |
|
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
160 |
val nil_term = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
161 |
Old_SMT_Utils.mk_const_pat @{theory} @{const_name Nil} Old_SMT_Utils.destT1 |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
162 |
val cons_term = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
163 |
Old_SMT_Utils.mk_const_pat @{theory} @{const_name Cons} Old_SMT_Utils.destT1 |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
164 |
fun mk_list cT cts = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
165 |
fold_rev (Thm.mk_binop (Old_SMT_Utils.instT cT cons_term)) cts |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
166 |
(Old_SMT_Utils.instT cT nil_term) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
167 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
168 |
val distinct = Old_SMT_Utils.mk_const_pat @{theory} @{const_name distinct} |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
169 |
(Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
170 |
fun mk_distinct [] = mk_true |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
171 |
| mk_distinct (cts as (ct :: _)) = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
172 |
Thm.apply (Old_SMT_Utils.instT' ct distinct) |
59586 | 173 |
(mk_list (Thm.ctyp_of_cterm ct) cts) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
174 |
|
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
175 |
val access = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
176 |
Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1 |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
177 |
fun mk_access array = Thm.apply (Old_SMT_Utils.instT' array access) array |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
178 |
|
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
179 |
val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd} |
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
180 |
(Thm.dest_ctyp o Old_SMT_Utils.destT1) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
181 |
fun mk_update array index value = |
59586 | 182 |
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array) |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
183 |
in |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
184 |
Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value |
41691
8f0531cf34f8
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41473
diff
changeset
|
185 |
end |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
186 |
|
59634 | 187 |
val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)}) |
188 |
val add = Thm.cterm_of @{context} @{const plus (int)} |
|
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
|
189 |
val int0 = Numeral.mk_cnumber @{ctyp int} 0 |
59634 | 190 |
val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)}) |
191 |
val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)}) |
|
192 |
val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div}) |
|
193 |
val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod}) |
|
194 |
val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)}) |
|
195 |
val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)}) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
196 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
197 |
fun mk_builtin_fun ctxt sym cts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
198 |
(case (sym, cts) of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
199 |
(Sym ("true", _), []) => SOME mk_true |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
200 |
| (Sym ("false", _), []) => SOME mk_false |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
201 |
| (Sym ("not", _), [ct]) => SOME (mk_not ct) |
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
|
202 |
| (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts) |
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
|
203 |
| (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
204 |
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
205 |
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
206 |
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
207 |
| (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) |
41761
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41691
diff
changeset
|
208 |
| (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) |
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41691
diff
changeset
|
209 |
| (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
210 |
| (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
211 |
| (Sym ("distinct", _), _) => SOME (mk_distinct cts) |
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:
42361
diff
changeset
|
212 |
| (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
213 |
| (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
214 |
| _ => |
59586 | 215 |
(case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of |
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
|
216 |
(Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
217 |
| (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
218 |
| (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
219 |
| (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) |
37151 | 220 |
| (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) |
221 |
| (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
222 |
| (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
223 |
| (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
224 |
| (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
225 |
| (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
226 |
| _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts)) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
227 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
228 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
229 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
230 |
(* abstraction *) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
231 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
232 |
fun is_builtin_theory_term ctxt t = |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
233 |
if Old_SMT_Builtin.is_builtin_num ctxt t then true |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
234 |
else |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
235 |
(case Term.strip_comb t of |
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset
|
236 |
(Const c, ts) => Old_SMT_Builtin.is_builtin_fun ctxt c ts |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40681
diff
changeset
|
237 |
| _ => false) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
238 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
239 |
end |