author | boehmes |
Wed, 07 Apr 2010 20:40:42 +0200 | |
changeset 36085 | 0eaa6905590f |
parent 35153 | 5e8935678ee4 |
permissions | -rw-r--r-- |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/SMT/Tools/z3_interface.ML |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
3 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
4 |
Interface to Z3 based on a relaxed version of SMT-LIB. |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
5 |
*) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
6 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
7 |
signature Z3_INTERFACE = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
8 |
sig |
36085
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
35153
diff
changeset
|
9 |
val interface: string list -> SMT_Translate.config |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
10 |
end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
11 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
12 |
structure Z3_Interface: Z3_INTERFACE = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
13 |
struct |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
14 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
15 |
structure T = SMT_Translate |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
16 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
17 |
fun mk_name1 n i = n ^ "[" ^ string_of_int i ^ "]" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
18 |
fun mk_name2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
19 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
20 |
val builtin_typ = (fn |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
21 |
@{typ int} => SOME "Int" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
22 |
| @{typ real} => SOME "Real" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
23 |
| Type (@{type_name word}, [T]) => |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
24 |
Option.map (mk_name1 "BitVec") (try T.dest_binT T) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
25 |
| _ => NONE) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
26 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
27 |
val builtin_num = (fn |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
28 |
(i, @{typ int}) => SOME (string_of_int i) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
29 |
| (i, @{typ real}) => SOME (string_of_int i ^ ".0") |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
30 |
| (i, Type (@{type_name word}, [T])) => |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
31 |
Option.map (mk_name1 ("bv" ^ string_of_int i)) (try T.dest_binT T) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
32 |
| _ => NONE) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
33 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
34 |
val builtin_funcs = T.builtin_make [ |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
35 |
(@{term If}, "ite"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
36 |
(@{term "uminus :: int => _"}, "~"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
37 |
(@{term "plus :: int => _"}, "+"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
38 |
(@{term "minus :: int => _"}, "-"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
39 |
(@{term "times :: int => _"}, "*"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
40 |
(@{term "op div :: int => _"}, "div"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
41 |
(@{term "op mod :: int => _"}, "mod"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
42 |
(@{term "op rem"}, "rem"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
43 |
(@{term "uminus :: real => _"}, "~"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
44 |
(@{term "plus :: real => _"}, "+"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
45 |
(@{term "minus :: real => _"}, "-"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
46 |
(@{term "times :: real => _"}, "*"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
47 |
(@{term "op / :: real => _"}, "/"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
48 |
(@{term "bitNOT :: 'a::len0 word => _"}, "bvnot"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
49 |
(@{term "op AND :: 'a::len0 word => _"}, "bvand"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
50 |
(@{term "op OR :: 'a::len0 word => _"}, "bvor"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
51 |
(@{term "op XOR :: 'a::len0 word => _"}, "bvxor"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
52 |
(@{term "uminus :: 'a::len0 word => _"}, "bvneg"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
53 |
(@{term "op + :: 'a::len0 word => _"}, "bvadd"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
54 |
(@{term "op - :: 'a::len0 word => _"}, "bvsub"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
55 |
(@{term "op * :: 'a::len0 word => _"}, "bvmul"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
56 |
(@{term "op div :: 'a::len0 word => _"}, "bvudiv"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
57 |
(@{term "op mod :: 'a::len0 word => _"}, "bvurem"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
58 |
(@{term "op sdiv"}, "bvsdiv"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
59 |
(@{term "op smod"}, "bvsmod"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
60 |
(@{term "op srem"}, "bvsrem"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
61 |
(@{term word_cat}, "concat"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
62 |
(@{term bv_shl}, "bvshl"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
63 |
(@{term bv_lshr}, "bvlshr"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
64 |
(@{term bv_ashr}, "bvashr")] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
65 |
|> T.builtin_add (@{term slice}, T.bv_extract (mk_name2 "extract")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
66 |
|> T.builtin_add (@{term ucast}, T.bv_extend (mk_name1 "zero_extend")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
67 |
|> T.builtin_add (@{term scast}, T.bv_extend (mk_name1 "sign_extend")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
68 |
|> T.builtin_add (@{term word_rotl}, T.bv_rotate (mk_name1 "rotate_left")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
69 |
|> T.builtin_add (@{term word_rotr}, T.bv_rotate (mk_name1 "rotate_right")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
70 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
71 |
val builtin_preds = T.builtin_make [ |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
72 |
(@{term True}, "true"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
73 |
(@{term False}, "false"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
74 |
(@{term Not}, "not"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
75 |
(@{term "op &"}, "and"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
76 |
(@{term "op |"}, "or"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
77 |
(@{term "op -->"}, "implies"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
78 |
(@{term "op iff"}, "iff"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
79 |
(@{term If}, "if_then_else"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
80 |
(@{term distinct}, "distinct"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
81 |
(@{term "op ="}, "="), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
82 |
(@{term "op < :: int => _"}, "<"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
83 |
(@{term "op <= :: int => _"}, "<="), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
84 |
(@{term "op < :: real => _"}, "<"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
85 |
(@{term "op <= :: real => _"}, "<="), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
86 |
(@{term "op < :: 'a::len0 word => _"}, "bvult"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
87 |
(@{term "op <= :: 'a::len0 word => _"}, "bvule"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
88 |
(@{term word_sless}, "bvslt"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
89 |
(@{term word_sle}, "bvsle")] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
90 |
|
33017
4fb8a33f74d6
eliminated extraneous wrapping of public records,
boehmes
parents:
32618
diff
changeset
|
91 |
val builtins = { |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
92 |
builtin_typ = builtin_typ, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
93 |
builtin_num = builtin_num, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
94 |
builtin_fun = (fn true => builtin_funcs | false => builtin_preds) } |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
95 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
96 |
val interface = SMTLIB_Interface.gen_interface builtins [] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
97 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
98 |
end |