author | boehmes |
Mon, 22 Nov 2010 15:45:42 +0100 | |
changeset 40662 | 798aad2229c0 |
parent 40274 | 6486c610a549 |
child 40664 | e023788a91a1 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/smtlib_interface.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Interface to SMT solvers based on the SMT-LIB format. |
|
5 |
*) |
|
6 |
||
7 |
signature SMTLIB_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 builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
10 |
builtin_typ: typ -> string option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
11 |
builtin_num: typ -> int -> string option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
12 |
builtin_func: 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
|
13 |
builtin_pred: 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
|
14 |
is_builtin_pred: string -> typ -> bool } |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
15 |
val add_builtins: 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
|
16 |
val add_logic: (term list -> string option) -> Context.generic -> |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
17 |
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
|
18 |
val extra_norm: SMT_Normalize.extra_norm |
36898 | 19 |
val interface: SMT_Solver.interface |
20 |
end |
|
21 |
||
22 |
structure SMTLIB_Interface: SMTLIB_INTERFACE = |
|
23 |
struct |
|
24 |
||
25 |
structure N = SMT_Normalize |
|
26 |
structure T = SMT_Translate |
|
27 |
||
28 |
||
29 |
||
30 |
(** facts about uninterpreted constants **) |
|
31 |
||
32 |
infix 2 ?? |
|
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
|
33 |
fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f |
36898 | 34 |
|
35 |
||
36 |
(* pairs *) |
|
37 |
||
38 |
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] |
|
39 |
||
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37155
diff
changeset
|
40 |
val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false) |
36898 | 41 |
val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type) |
42 |
||
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
|
43 |
val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules) |
36898 | 44 |
|
45 |
||
46 |
(* function update *) |
|
47 |
||
48 |
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}] |
|
49 |
||
50 |
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false) |
|
51 |
val exists_fun_upd = Term.exists_subterm is_fun_upd |
|
52 |
||
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
|
53 |
val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules) |
36898 | 54 |
|
55 |
||
56 |
(* abs/min/max *) |
|
57 |
||
58 |
val exists_abs_min_max = Term.exists_subterm (fn |
|
59 |
Const (@{const_name abs}, _) => true |
|
60 |
| Const (@{const_name min}, _) => true |
|
61 |
| Const (@{const_name max}, _) => true |
|
62 |
| _ => false) |
|
63 |
||
37786
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37678
diff
changeset
|
64 |
val unfold_abs_conv = Conv.rewr_conv (mk_meta_eq @{thm abs_if}) |
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37678
diff
changeset
|
65 |
val unfold_min_conv = Conv.rewr_conv (mk_meta_eq @{thm min_def}) |
4eb98849c5c0
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
boehmes
parents:
37678
diff
changeset
|
66 |
val unfold_max_conv = Conv.rewr_conv (mk_meta_eq @{thm max_def}) |
36898 | 67 |
|
68 |
fun expand_conv cv = N.eta_expand_conv (K cv) |
|
69 |
fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv)) |
|
70 |
||
71 |
fun unfold_def_conv ctxt ct = |
|
72 |
(case Thm.term_of ct of |
|
73 |
Const (@{const_name abs}, _) $ _ => unfold_abs_conv |
|
74 |
| Const (@{const_name abs}, _) => expand_conv unfold_abs_conv ctxt |
|
75 |
| Const (@{const_name min}, _) $ _ $ _ => unfold_min_conv |
|
76 |
| Const (@{const_name min}, _) $ _ => expand_conv unfold_min_conv ctxt |
|
77 |
| Const (@{const_name min}, _) => expand2_conv unfold_min_conv ctxt |
|
78 |
| Const (@{const_name max}, _) $ _ $ _ => unfold_max_conv |
|
79 |
| Const (@{const_name max}, _) $ _ => expand_conv unfold_max_conv ctxt |
|
80 |
| Const (@{const_name max}, _) => expand2_conv unfold_max_conv ctxt |
|
81 |
| _ => Conv.all_conv) ct |
|
82 |
||
83 |
fun unfold_abs_min_max_defs ctxt thm = |
|
84 |
if exists_abs_min_max (Thm.prop_of thm) |
|
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36899
diff
changeset
|
85 |
then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm |
36898 | 86 |
else thm |
87 |
||
88 |
||
89 |
(* include additional facts *) |
|
90 |
||
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
|
91 |
fun extra_norm has_datatypes irules ctxt = |
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
|
92 |
irules |
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
|
93 |
|> not has_datatypes ? add_pair_rules |
36898 | 94 |
|> add_fun_upd_rules |
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
|
95 |
|> map (apsnd (unfold_abs_min_max_defs ctxt)) |
36898 | 96 |
|> rpair ctxt |
97 |
||
98 |
||
99 |
||
100 |
(** builtins **) |
|
101 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
102 |
(* additional builtins *) |
36898 | 103 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
104 |
type builtins = { |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
105 |
builtin_typ: typ -> string option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
106 |
builtin_num: typ -> int -> string option, |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
107 |
builtin_func: 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
|
108 |
builtin_pred: 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
|
109 |
is_builtin_pred: string -> typ -> bool } |
36898 | 110 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
111 |
fun chained _ [] = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
112 |
| chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs) |
36898 | 113 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
114 |
fun chained' _ [] = false |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
115 |
| chained' f (b :: bs) = f b orelse chained' f bs |
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 |
fun chained_builtin_typ bs T = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
118 |
chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs |
36898 | 119 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
120 |
fun chained_builtin_num bs T i = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
121 |
chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs |
36898 | 122 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
123 |
fun chained_builtin_func bs c ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
124 |
chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
125 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
126 |
fun chained_builtin_pred bs c ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
127 |
chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs |
36898 | 128 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
129 |
fun chained_is_builtin_pred bs n T = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
130 |
chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs |
36898 | 131 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
132 |
fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2) |
36898 | 133 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
134 |
structure Builtins = Generic_Data |
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 |
type T = (int * builtins) list |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
137 |
val empty = [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
138 |
val extend = I |
39687 | 139 |
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
|
140 |
) |
36898 | 141 |
|
39687 | 142 |
fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs)) |
36898 | 143 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
144 |
fun get_builtins ctxt = map snd (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
|
145 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
146 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
147 |
(* basic builtins combined with additional builtins *) |
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 builtin_typ _ @{typ int} = SOME "Int" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
150 |
| builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T |
36898 | 151 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
152 |
fun builtin_num _ @{typ int} i = SOME (string_of_int i) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
153 |
| builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i |
36898 | 154 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
155 |
fun if_int_type T n = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
156 |
(case try Term.domain_type T of |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
157 |
SOME @{typ int} => SOME n |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
158 |
| _ => NONE) |
36898 | 159 |
|
160 |
fun conn @{const_name True} = SOME "true" |
|
161 |
| conn @{const_name False} = SOME "false" |
|
162 |
| conn @{const_name Not} = SOME "not" |
|
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
163 |
| conn @{const_name HOL.conj} = SOME "and" |
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
164 |
| conn @{const_name HOL.disj} = SOME "or" |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
37786
diff
changeset
|
165 |
| conn @{const_name HOL.implies} = SOME "implies" |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
166 |
| conn @{const_name HOL.eq} = SOME "iff" |
36898 | 167 |
| conn @{const_name If} = SOME "if_then_else" |
168 |
| conn _ = NONE |
|
169 |
||
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
|
170 |
fun pred @{const_name SMT.distinct} _ = SOME "distinct" |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
171 |
| pred @{const_name HOL.eq} _ = SOME "=" |
36898 | 172 |
| pred @{const_name term_eq} _ = SOME "=" |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
173 |
| pred @{const_name less} T = if_int_type T "<" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
174 |
| pred @{const_name less_eq} T = if_int_type T "<=" |
36898 | 175 |
| pred _ _ = NONE |
176 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
177 |
fun func @{const_name If} _ = SOME "ite" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
178 |
| func @{const_name uminus} T = if_int_type T "~" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
179 |
| func @{const_name plus} T = if_int_type T "+" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
180 |
| func @{const_name minus} T = if_int_type T "-" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
181 |
| func @{const_name times} T = if_int_type T "*" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
182 |
| func _ _ = NONE |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
183 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
184 |
val is_propT = (fn @{typ prop} => true | _ => false) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
185 |
fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us)) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
186 |
fun is_predT T = is_propT (Term.body_type T) |
36898 | 187 |
|
188 |
fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n) |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
189 |
fun is_builtin_pred ctxt (n, T) = is_predT T andalso |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
190 |
(is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T) |
36898 | 191 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
192 |
fun 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
|
193 |
let |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
194 |
val builtin_func' = chained_builtin_func (get_builtins ctxt) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
195 |
val builtin_pred' = chained_builtin_pred (get_builtins ctxt) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
196 |
in |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
197 |
if is_connT T then conn n |> Option.map (rpair ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
198 |
else if is_predT T then |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
199 |
(case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
200 |
else |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
201 |
(case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
202 |
end |
36898 | 203 |
|
204 |
||
205 |
||
206 |
(** serialization **) |
|
207 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
208 |
(* header *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
209 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
210 |
structure Logics = Generic_Data |
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 |
type T = (int * (term list -> string option)) list |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
213 |
val empty = [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
214 |
val extend = I |
39687 | 215 |
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
|
216 |
) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
217 |
|
39687 | 218 |
fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l)) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
219 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
220 |
fun choose_logic ctxt ts = |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
221 |
let |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
222 |
fun choose [] = "AUFLIA" |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
223 |
| choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
224 |
in [":logic " ^ choose (rev (Logics.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
|
225 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
226 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
227 |
(* serialization *) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
228 |
|
36898 | 229 |
val add = Buffer.add |
230 |
fun sep f = add " " #> f |
|
231 |
fun enclose l r f = sep (add l #> f #> add r) |
|
232 |
val par = enclose "(" ")" |
|
233 |
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs)) |
|
234 |
fun line f = f #> add "\n" |
|
235 |
||
236 |
fun var i = add "?v" #> add (string_of_int i) |
|
237 |
||
238 |
fun sterm l (T.SVar i) = sep (var (l - i - 1)) |
|
239 |
| sterm l (T.SApp (n, ts)) = app n (sterm l) ts |
|
240 |
| sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression" |
|
241 |
| sterm l (T.SQua (q, ss, ps, t)) = |
|
242 |
let |
|
243 |
val quant = add o (fn T.SForall => "forall" | T.SExists => "exists") |
|
244 |
val vs = map_index (apfst (Integer.add l)) ss |
|
245 |
fun var_decl (i, s) = par (var i #> sep (add s)) |
|
246 |
val sub = sterm (l + length ss) |
|
247 |
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts)) |
|
248 |
fun pats (T.SPat ts) = pat ":pat" ts |
|
249 |
| pats (T.SNoPat ts) = pat ":nopat" ts |
|
250 |
in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end |
|
251 |
||
37155
e3f18cfc9829
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents:
36936
diff
changeset
|
252 |
fun ssort sorts = sort fast_string_ord sorts |
e3f18cfc9829
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents:
36936
diff
changeset
|
253 |
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs |
e3f18cfc9829
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents:
36936
diff
changeset
|
254 |
|
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
|
255 |
fun sdatatypes decls = |
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
|
256 |
let |
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
|
257 |
fun con (n, []) = add n |
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
|
258 |
| con (n, sels) = par (add n #> |
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
|
259 |
fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels) |
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
|
260 |
fun dtyp (n, decl) = add n #> fold (sep o con) decl |
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
|
261 |
in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end |
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
|
262 |
|
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
|
263 |
fun serialize comments {header, sorts, dtyps, funcs} ts = |
36898 | 264 |
Buffer.empty |
265 |
|> line (add "(benchmark Isabelle") |
|
266 |
|> line (add ":status unknown") |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
267 |
|> fold (line o add) header |
36898 | 268 |
|> length sorts > 0 ? |
37155
e3f18cfc9829
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents:
36936
diff
changeset
|
269 |
line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts))) |
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
|
270 |
|> fold sdatatypes dtyps |
36898 | 271 |
|> length funcs > 0 ? ( |
272 |
line (add ":extrafuns" #> add " (") #> |
|
273 |
fold (fn (f, (ss, s)) => |
|
37155
e3f18cfc9829
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
boehmes
parents:
36936
diff
changeset
|
274 |
line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #> |
36898 | 275 |
line (add ")")) |
276 |
|> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts |
|
277 |
|> line (add ":formula true)") |
|
278 |
|> fold (fn str => line (add "; " #> add str)) comments |
|
279 |
|> Buffer.content |
|
280 |
||
281 |
||
282 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
283 |
(** interfaces **) |
36898 | 284 |
|
285 |
val interface = { |
|
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
|
286 |
extra_norm = extra_norm, |
36898 | 287 |
translate = { |
288 |
prefixes = { |
|
289 |
sort_prefix = "S", |
|
290 |
func_prefix = "f"}, |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
291 |
header = choose_logic, |
36898 | 292 |
strict = SOME { |
293 |
is_builtin_conn = is_builtin_conn, |
|
294 |
is_builtin_pred = is_builtin_pred, |
|
295 |
is_builtin_distinct = true}, |
|
296 |
builtins = { |
|
297 |
builtin_typ = builtin_typ, |
|
298 |
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
|
299 |
builtin_fun = builtin_fun, |
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
|
300 |
has_datatypes = false}, |
36898 | 301 |
serialize = serialize}} |
302 |
||
303 |
end |