author | blanchet |
Thu, 28 Aug 2014 00:40:37 +0200 | |
changeset 58055 | 625bdd5c70b2 |
parent 47155 | src/HOL/Tools/SMT/smtlib_interface.ML@ade3fc826af3 |
permissions | -rw-r--r-- |
58055 | 1 |
(* Title: HOL/Library/SMT/smtlib_interface.ML |
36898 | 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 |
|
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41072
diff
changeset
|
9 |
val smtlibC: SMT_Utils.class |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
10 |
val add_logic: int * (term list -> string option) -> Context.generic -> |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
11 |
Context.generic |
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
|
12 |
val translate_config: Proof.context -> SMT_Translate.config |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
13 |
val setup: theory -> theory |
36898 | 14 |
end |
15 |
||
16 |
structure SMTLIB_Interface: SMTLIB_INTERFACE = |
|
17 |
struct |
|
18 |
||
19 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
20 |
val smtlibC = ["smtlib"] |
36898 | 21 |
|
22 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
23 |
(* builtins *) |
36898 | 24 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
25 |
local |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
26 |
fun int_num _ i = SOME (string_of_int i) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
27 |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
28 |
fun is_linear [t] = SMT_Utils.is_number t |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
29 |
| is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u |
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset
|
30 |
| is_linear _ = 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
|
31 |
|
41281
679118e35378
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset
|
32 |
fun times _ _ ts = |
679118e35378
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset
|
33 |
let val mk = Term.list_comb o pair @{const times (int)} |
679118e35378
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset
|
34 |
in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
35 |
in |
36898 | 36 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
37 |
val setup_builtins = |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
38 |
SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #> |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
39 |
fold (SMT_Builtin.add_builtin_fun' smtlibC) [ |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
40 |
(@{const True}, "true"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
41 |
(@{const False}, "false"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
42 |
(@{const Not}, "not"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
43 |
(@{const HOL.conj}, "and"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
44 |
(@{const HOL.disj}, "or"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
45 |
(@{const HOL.implies}, "implies"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
46 |
(@{const HOL.eq (bool)}, "iff"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
47 |
(@{const HOL.eq ('a)}, "="), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
48 |
(@{const If (bool)}, "if_then_else"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
49 |
(@{const If ('a)}, "ite"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
50 |
(@{const less (int)}, "<"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
51 |
(@{const less_eq (int)}, "<="), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
52 |
(@{const uminus (int)}, "~"), |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
53 |
(@{const plus (int)}, "+"), |
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
|
54 |
(@{const minus (int)}, "-") ] #> |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
55 |
SMT_Builtin.add_builtin_fun smtlibC |
47155
ade3fc826af3
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
boehmes
parents:
41473
diff
changeset
|
56 |
(Term.dest_Const @{const times (int)}, times) |
36898 | 57 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
58 |
end |
36898 | 59 |
|
60 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
61 |
(* serialization *) |
36898 | 62 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
63 |
(** header **) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
64 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
65 |
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
66 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
67 |
structure Logics = Generic_Data |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
68 |
( |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
69 |
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
|
70 |
val empty = [] |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
71 |
val extend = I |
41473 | 72 |
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
|
73 |
) |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
74 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
75 |
fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
76 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
77 |
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
|
78 |
let |
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
79 |
fun choose [] = "AUFLIA" |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
80 |
| choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
41057
diff
changeset
|
81 |
in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
82 |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
83 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
84 |
(** serialization **) |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
85 |
|
36898 | 86 |
val add = Buffer.add |
87 |
fun sep f = add " " #> f |
|
88 |
fun enclose l r f = sep (add l #> f #> add r) |
|
89 |
val par = enclose "(" ")" |
|
90 |
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs)) |
|
91 |
fun line f = f #> add "\n" |
|
92 |
||
93 |
fun var i = add "?v" #> add (string_of_int i) |
|
94 |
||
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
95 |
fun sterm l (SMT_Translate.SVar i) = sep (var (l - i - 1)) |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
96 |
| sterm l (SMT_Translate.SApp (n, ts)) = app n (sterm l) ts |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
97 |
| sterm _ (SMT_Translate.SLet _) = |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
98 |
raise Fail "SMT-LIB: unsupported let expression" |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
99 |
| sterm l (SMT_Translate.SQua (q, ss, ps, w, t)) = |
36898 | 100 |
let |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
101 |
fun quant SMT_Translate.SForall = add "forall" |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
102 |
| quant SMT_Translate.SExists = add "exists" |
36898 | 103 |
val vs = map_index (apfst (Integer.add l)) ss |
104 |
fun var_decl (i, s) = par (var i #> sep (add s)) |
|
105 |
val sub = sterm (l + length ss) |
|
106 |
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts)) |
|
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
107 |
fun pats (SMT_Translate.SPat ts) = pat ":pat" ts |
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
108 |
| pats (SMT_Translate.SNoPat ts) = pat ":nopat" ts |
40664 | 109 |
fun weight NONE = I |
110 |
| weight (SOME i) = |
|
111 |
sep (add ":weight { " #> add (string_of_int i) #> add " }") |
|
112 |
in |
|
113 |
par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w) |
|
114 |
end |
|
36898 | 115 |
|
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
|
116 |
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
|
117 |
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
|
118 |
|
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
|
119 |
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
|
120 |
let |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset
|
121 |
fun con (n, []) = sep (add n) |
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
|
122 |
| con (n, sels) = par (add n #> |
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset
|
123 |
fold (fn (n, s) => par (add n #> sep (add s))) sels) |
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset
|
124 |
fun dtyp (n, decl) = add n #> fold con decl |
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
|
125 |
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
|
126 |
|
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
|
127 |
fun serialize comments {header, sorts, dtyps, funcs} ts = |
36898 | 128 |
Buffer.empty |
129 |
|> line (add "(benchmark Isabelle") |
|
130 |
|> 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
|
131 |
|> fold (line o add) header |
36898 | 132 |
|> 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
|
133 |
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
|
134 |
|> fold sdatatypes dtyps |
36898 | 135 |
|> length funcs > 0 ? ( |
136 |
line (add ":extrafuns" #> add " (") #> |
|
137 |
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
|
138 |
line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #> |
36898 | 139 |
line (add ")")) |
140 |
|> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts |
|
141 |
|> line (add ":formula true)") |
|
142 |
|> fold (fn str => line (add "; " #> add str)) comments |
|
143 |
|> Buffer.content |
|
144 |
||
145 |
||
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
146 |
(* interface *) |
36898 | 147 |
|
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
|
148 |
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
|
149 |
prefixes = { |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
150 |
sort_prefix = "S", |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
151 |
func_prefix = "f"}, |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
152 |
header = choose_logic 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
|
153 |
is_fol = 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
|
154 |
has_datatypes = false, |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
155 |
serialize = serialize} |
36898 | 156 |
|
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
|
157 |
val setup = Context.theory_map ( |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
158 |
setup_builtins #> |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41281
diff
changeset
|
159 |
SMT_Translate.add_config (smtlibC, translate_config)) |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
160 |
|
36898 | 161 |
end |