author | boehmes |
Mon, 22 Nov 2010 15:45:42 +0100 | |
changeset 40662 | 798aad2229c0 |
parent 40579 | 98ebd2300823 |
child 40681 | 872b08416fb4 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/z3_interface.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Interface to Z3 based on a relaxed version of SMT-LIB. |
|
5 |
*) |
|
6 |
||
7 |
signature Z3_INTERFACE = |
|
8 |
sig |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
9 |
type builtin_fun = string * typ -> term list -> (string * term list) option |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
10 |
val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
11 |
val interface: SMT_Solver.interface |
36898 | 12 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
13 |
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
|
14 |
type mk_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
15 |
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
|
16 |
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
|
17 |
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
|
18 |
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
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
23 |
val is_builtin_theory_term: Proof.context -> term -> bool |
36898 | 24 |
end |
25 |
||
26 |
structure Z3_Interface: Z3_INTERFACE = |
|
27 |
struct |
|
28 |
||
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
29 |
structure U = SMT_Utils |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
30 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
31 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
32 |
(** Z3-specific builtins **) |
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 |
type builtin_fun = string * typ -> term list -> (string * term list) option |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
35 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
36 |
fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
37 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
38 |
structure Builtins = Generic_Data |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
39 |
( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
40 |
type T = (int * builtin_fun) list |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
41 |
val empty = [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
42 |
val extend = I |
39687 | 43 |
fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1 |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
44 |
) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
45 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
46 |
fun add_builtin_funs b = |
39687 | 47 |
Builtins.map (Ord_List.insert fst_int_ord (serial (), b)) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
48 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
49 |
fun get_builtin_funs ctxt c ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
50 |
let |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
51 |
fun chained [] = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
52 |
| chained (b :: bs) = (case b c ts of SOME x => SOME x | _ => chained bs) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
53 |
in chained (map snd (Builtins.get (Context.Proof ctxt))) end |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
54 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
55 |
fun z3_builtin_fun builtin_fun ctxt c ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
56 |
(case builtin_fun ctxt c ts of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
57 |
SOME x => SOME x |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
58 |
| _ => get_builtin_funs ctxt c ts) |
36898 | 59 |
|
60 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
61 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
62 |
(** interface **) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
63 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
64 |
local |
40274
6486c610a549
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents:
40162
diff
changeset
|
65 |
val {translate, ...} = SMTLIB_Interface.interface |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
66 |
val {prefixes, strict, header, builtins, serialize} = translate |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
67 |
val {is_builtin_pred, ...}= the strict |
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
38864
diff
changeset
|
68 |
val {builtin_typ, builtin_num, builtin_fun, ...} = builtins |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
69 |
|
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 |
fun is_int_div_mod @{const div (int)} = true |
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 |
| is_int_div_mod @{const mod (int)} = true |
37151 | 72 |
| is_int_div_mod _ = false |
73 |
||
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
74 |
fun add_div_mod irules = |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
75 |
if exists (Term.exists_subterm is_int_div_mod o Thm.prop_of o snd) irules |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
76 |
then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
77 |
else irules |
37151 | 78 |
|
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
79 |
fun extra_norm' has_datatypes = |
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39687
diff
changeset
|
80 |
SMTLIB_Interface.extra_norm has_datatypes o add_div_mod |
37151 | 81 |
|
82 |
fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts) |
|
83 |
| z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts) |
|
84 |
| z3_builtin_fun' ctxt c ts = z3_builtin_fun builtin_fun ctxt c ts |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
85 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
86 |
val as_propT = (fn @{typ bool} => @{typ prop} | T => T) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
87 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
88 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
89 |
fun is_builtin_num ctxt (T, i) = is_some (builtin_num ctxt T i) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
90 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
91 |
fun is_builtin_fun ctxt (c as (n, T)) ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
92 |
is_some (z3_builtin_fun' ctxt c ts) orelse |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
93 |
is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->)) |
36898 | 94 |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
95 |
val interface = { |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
96 |
extra_norm = extra_norm', |
36898 | 97 |
translate = { |
98 |
prefixes = prefixes, |
|
99 |
strict = strict, |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
100 |
header = header, |
36898 | 101 |
builtins = { |
102 |
builtin_typ = builtin_typ, |
|
103 |
builtin_num = builtin_num, |
|
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
38864
diff
changeset
|
104 |
builtin_fun = z3_builtin_fun', |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
105 |
has_datatypes = true}, |
36898 | 106 |
serialize = serialize}} |
107 |
||
108 |
end |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
109 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
110 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
111 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
112 |
(** constructors **) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
113 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
114 |
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
|
115 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
116 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
117 |
(* additional constructors *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
118 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
119 |
type mk_builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
124 |
fun chained _ [] = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
125 |
| 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
|
126 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
127 |
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
|
128 |
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
|
129 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
130 |
fun chained_mk_builtin_num ctxt bs i T = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
131 |
let val thy = ProofContext.theory_of ctxt |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
132 |
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
|
133 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
134 |
fun chained_mk_builtin_fun ctxt bs s cts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
135 |
let val thy = ProofContext.theory_of ctxt |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
136 |
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
|
137 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
138 |
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
|
139 |
( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
140 |
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
|
141 |
val empty = [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
142 |
val extend = I |
39687 | 143 |
fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1 |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
144 |
) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
145 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
146 |
fun add_mk_builtins mk = |
39687 | 147 |
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
|
148 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
149 |
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
|
150 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
151 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
152 |
(* basic and additional constructors *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
153 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
154 |
fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} |
40516 | 155 |
| mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} |
156 |
| mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: delete*) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
157 |
| 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
|
158 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
159 |
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
|
160 |
| 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
|
161 |
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
|
162 |
|
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
|
163 |
val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False}) |
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
|
164 |
val mk_false = Thm.cterm_of @{theory} @{const False} |
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
|
165 |
val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not}) |
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
|
166 |
val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies}) |
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
|
167 |
val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)}) |
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
|
168 |
val conj = Thm.cterm_of @{theory} @{const HOL.conj} |
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
|
169 |
val disj = Thm.cterm_of @{theory} @{const HOL.disj} |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
170 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
171 |
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
|
172 |
| 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
|
173 |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
174 |
val eq = U.mk_const_pat @{theory} @{const_name HOL.eq} U.destT1 |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
175 |
fun mk_eq ct cu = Thm.mk_binop (U.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
|
176 |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
177 |
val if_term = U.mk_const_pat @{theory} @{const_name If} (U.destT1 o U.destT2) |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
178 |
fun mk_if cc ct cu = Thm.mk_binop (Thm.capply (U.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
|
179 |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
180 |
val nil_term = U.mk_const_pat @{theory} @{const_name Nil} U.destT1 |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
181 |
val cons_term = U.mk_const_pat @{theory} @{const_name Cons} U.destT1 |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
182 |
fun mk_list cT cts = |
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
183 |
fold_rev (Thm.mk_binop (U.instT cT cons_term)) cts (U.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
|
184 |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
185 |
val distinct = U.mk_const_pat @{theory} @{const_name SMT.distinct} |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
186 |
(U.destT1 o U.destT1) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
187 |
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
|
188 |
| mk_distinct (cts as (ct :: _)) = |
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
189 |
Thm.capply (U.instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
190 |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
191 |
val access = U.mk_const_pat @{theory} @{const_name fun_app} |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
192 |
(Thm.dest_ctyp o U.destT1) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
193 |
fun mk_access array index = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
194 |
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array) |
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
195 |
in Thm.mk_binop (U.instTs cTs access) array index end |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
196 |
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
197 |
val update = U.mk_const_pat @{theory} @{const_name fun_upd} |
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
198 |
(Thm.dest_ctyp o U.destT1) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
199 |
fun mk_update array index value = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
200 |
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array) |
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40579
diff
changeset
|
201 |
in Thm.capply (Thm.mk_binop (U.instTs cTs update) array index) value end |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
202 |
|
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
|
203 |
val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)}) |
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
|
204 |
val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)}) |
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
|
205 |
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)}) |
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
|
206 |
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)}) |
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
|
207 |
val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div}) |
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
|
208 |
val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod}) |
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
|
209 |
val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)}) |
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
|
210 |
val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{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
|
211 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
212 |
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
|
213 |
(case (sym, cts) of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
214 |
(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
|
215 |
| (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
|
216 |
| (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
|
217 |
| (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
|
218 |
| (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
|
219 |
| (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
|
220 |
| (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
|
221 |
| (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
|
222 |
| (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
223 |
| (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
224 |
| (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
|
225 |
| (Sym ("distinct", _), _) => SOME (mk_distinct cts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
226 |
| (Sym ("select", _), [ca, ck]) => SOME (mk_access ca ck) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
227 |
| (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
|
228 |
| _ => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
229 |
(case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
230 |
(Sym ("+", _), SOME @{typ int}, [ct, cu]) => SOME (mk_add ct cu) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
231 |
| (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
|
232 |
| (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
|
233 |
| (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) |
37151 | 234 |
| (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) |
235 |
| (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
|
236 |
| (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
|
237 |
| (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
|
238 |
| (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
|
239 |
| (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
|
240 |
| _ => 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
|
241 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
242 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
243 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
244 |
(** abstraction **) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
245 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
246 |
fun is_builtin_theory_term ctxt t = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
247 |
(case try HOLogic.dest_number t of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
248 |
SOME n => is_builtin_num ctxt n |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
249 |
| NONE => |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
250 |
(case Term.strip_comb t of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
251 |
(Const c, ts) => is_builtin_fun ctxt c ts |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
252 |
| _ => false)) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
253 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
254 |
end |