| author | boehmes |
| Wed, 12 May 2010 23:53:57 +0200 | |
| changeset 36893 | 48cf03469dc6 |
| permissions | -rw-r--r-- |
|
36893
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/SMT/Tools/z3_interface.ML |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
3 |
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
4 |
Interface to Z3 based on a relaxed version of SMT-LIB. |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
5 |
*) |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
6 |
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
7 |
signature Z3_INTERFACE = |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
8 |
sig |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
9 |
val interface: string list -> SMT_Translate.config |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
10 |
end |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
11 |
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
12 |
structure Z3_Interface: Z3_INTERFACE = |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
13 |
struct |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
14 |
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
15 |
fun z3_builtin_fun bf c ts = |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
16 |
(case Const c of |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
17 |
@{term "op / :: real => _"} => SOME ("/", ts)
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
18 |
| _ => bf c ts) |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
19 |
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
20 |
fun interface comments = |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
21 |
let |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
22 |
val {prefixes, strict, builtins, serialize} =
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
23 |
SMTLIB_Interface.interface comments |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
24 |
val {builtin_typ, builtin_num, builtin_fun} = builtins
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
25 |
in |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
26 |
{prefixes = prefixes,
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
27 |
strict = strict, |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
28 |
builtins = {
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
29 |
builtin_typ = builtin_typ, |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
30 |
builtin_num = builtin_num, |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
31 |
builtin_fun = z3_builtin_fun builtin_fun}, |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
32 |
serialize = serialize} |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
33 |
end |
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
34 |
|
|
48cf03469dc6
added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
boehmes
parents:
diff
changeset
|
35 |
end |