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/smtlib_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 SMT solvers based on the SMT-LIB format. |
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 SMTLIB_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 SMTLIB_Interface: SMTLIB_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 |
structure T = SMT_Translate |
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 |
|
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 |
fun dest_binT T = |
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 |
(case T 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
|
19 |
Type (@{type_name "Numeral_Type.num0"}, _) => 0 |
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 |
| Type (@{type_name "Numeral_Type.num1"}, _) => 1 |
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 |
| Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T |
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 |
| Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T |
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 |
| _ => raise TYPE ("dest_binT", [T], [])) |
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 |
|
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 |
fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T |
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 |
| dest_wordT T = raise TYPE ("dest_wordT", [T], []) |
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 |
|
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 |
|
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 |
|
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 |
(* 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
|
31 |
|
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 |
fun index1 n i = n ^ "[" ^ string_of_int i ^ "]" |
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 |
fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]" |
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 |
fun builtin_typ @{typ int} = SOME "Int" |
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
|
36 |
| builtin_typ @{typ real} = SOME "Real" |
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
|
37 |
| builtin_typ (Type (@{type_name word}, [T])) = |
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
|
38 |
Option.map (index1 "BitVec") (try dest_binT T) |
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
|
39 |
| builtin_typ _ = NONE |
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
|
40 |
|
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
|
41 |
fun builtin_num @{typ int} i = SOME (string_of_int i) |
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
|
42 |
| builtin_num @{typ real} i = SOME (string_of_int i ^ ".0") |
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
|
43 |
| builtin_num (Type (@{type_name word}, [T])) i = |
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
|
44 |
Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T) |
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
|
45 |
| builtin_num _ _ = NONE |
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
|
46 |
|
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
|
47 |
val is_propT = (fn @{typ prop} => true | _ => false) |
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
|
48 |
fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us)) |
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
|
49 |
fun is_predT T = is_propT (Term.body_type T) |
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
|
50 |
|
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
|
51 |
fun just c ts = SOME (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
|
52 |
|
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
|
53 |
val is_arith_type = member (op =) [@{typ int}, @{typ real}] o Term.domain_type |
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
|
54 |
|
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
|
55 |
fun fixed_bvT (Ts, T) x = |
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
|
56 |
if forall (can dest_wordT) (T :: Ts) then SOME x else NONE |
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
|
57 |
|
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
|
58 |
fun if_fixed_bvT' T = fixed_bvT ([], Term.domain_type T) |
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
|
59 |
fun if_fixed_bvT T = curry (fixed_bvT ([], Term.domain_type T)) |
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
|
60 |
fun if_full_fixed_bvT T = curry (fixed_bvT (Term.strip_type T)) |
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
|
61 |
|
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
|
62 |
fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U) |
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
|
63 |
| dest_word_funT T = raise TYPE ("dest_word_funT", [T], []) |
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
|
64 |
fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), 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
|
65 |
| dest_nat ts = raise TERM ("dest_nat", 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
|
66 |
fun dest_nat_word_funT (T, 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
|
67 |
(dest_word_funT (Term.range_type T), dest_nat 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
|
68 |
|
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
|
69 |
fun bv_extend n T 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
|
70 |
(case try dest_word_funT T 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
|
71 |
SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE |
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
|
72 |
| _ => NONE) |
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
|
73 |
|
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
|
74 |
fun bv_rotate n T 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
|
75 |
try dest_nat 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
|
76 |
|> Option.map (fn (i, ts') => (index1 n i, 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
|
77 |
|
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
|
78 |
fun bv_extract n T 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
|
79 |
try dest_nat_word_funT (T, 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
|
80 |
|> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, 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
|
81 |
|
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
|
82 |
|
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
|
83 |
fun conn @{const_name True} = SOME "true" |
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
|
84 |
| conn @{const_name False} = SOME "false" |
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
|
85 |
| conn @{const_name Not} = SOME "not" |
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
|
86 |
| conn @{const_name "op &"} = SOME "and" |
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
|
87 |
| conn @{const_name "op |"} = SOME "or" |
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
|
88 |
| conn @{const_name "op -->"} = SOME "implies" |
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
|
89 |
| conn @{const_name "op ="} = SOME "iff" |
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
|
90 |
| conn @{const_name If} = SOME "if_then_else" |
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
|
91 |
| conn _ = NONE |
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
|
92 |
|
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
|
93 |
fun pred @{const_name distinct} _ = SOME "distinct" |
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
|
94 |
| pred @{const_name "op ="} _ = SOME "=" |
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
|
95 |
| pred @{const_name term_eq} _ = SOME "=" |
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
|
96 |
| pred @{const_name less} T = |
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
|
97 |
if is_arith_type T then SOME "<" |
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
|
98 |
else if_fixed_bvT' T "bvult" |
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
|
99 |
| pred @{const_name less_eq} T = |
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
|
100 |
if is_arith_type T then SOME "<=" |
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
|
101 |
else if_fixed_bvT' T "bvule" |
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
|
102 |
| pred @{const_name word_sless} T = if_fixed_bvT' T "bvslt" |
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
|
103 |
| pred @{const_name word_sle} T = if_fixed_bvT' T "bvsle" |
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
|
104 |
| pred _ _ = NONE |
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
|
105 |
|
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
|
106 |
fun func @{const_name If} _ = just "ite" |
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
|
107 |
| func @{const_name uminus} T = |
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
|
108 |
if is_arith_type T then just "~" |
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
|
109 |
else if_fixed_bvT T "bvneg" |
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
|
110 |
| func @{const_name plus} T = |
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
|
111 |
if is_arith_type T then just "+" |
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
|
112 |
else if_fixed_bvT T "bvadd" |
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
|
113 |
| func @{const_name minus} T = |
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
|
114 |
if is_arith_type T then just "-" |
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
|
115 |
else if_fixed_bvT T "bvsub" |
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
|
116 |
| func @{const_name times} T = |
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
|
117 |
if is_arith_type T then just "*" |
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
|
118 |
else if_fixed_bvT T "bvmul" |
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
|
119 |
| func @{const_name bitNOT} T = if_fixed_bvT T "bvnot" |
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
|
120 |
| func @{const_name bitAND} T = if_fixed_bvT T "bvand" |
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
|
121 |
| func @{const_name bitOR} T = if_fixed_bvT T "bvor" |
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
|
122 |
| func @{const_name bitXOR} T = if_fixed_bvT T "bvxor" |
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
|
123 |
| func @{const_name div} T = if_fixed_bvT T "bvudiv" |
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
|
124 |
| func @{const_name mod} T = if_fixed_bvT T "bvurem" |
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
|
125 |
| func @{const_name sdiv} T = if_fixed_bvT T "bvsdiv" |
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
|
126 |
| func @{const_name smod} T = if_fixed_bvT T "bvsmod" |
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
|
127 |
| func @{const_name srem} T = if_fixed_bvT T "bvsrem" |
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
|
128 |
| func @{const_name word_cat} T = if_full_fixed_bvT T "concat" |
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
|
129 |
| func @{const_name bv_shl} T = if_full_fixed_bvT T "bvshl" |
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
|
130 |
| func @{const_name bv_lshr} T = if_full_fixed_bvT T "bvlshr" |
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
|
131 |
| func @{const_name bv_ashr} T = if_full_fixed_bvT T "bvashr" |
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
|
132 |
| func @{const_name slice} T = bv_extract "extract" T |
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
|
133 |
| func @{const_name ucast} T = bv_extend "zero_extend" T |
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
|
134 |
| func @{const_name scast} T = bv_extend "sign_extend" T |
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
|
135 |
| func @{const_name word_rotl} T = bv_rotate "rotate_left" T |
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
|
136 |
| func @{const_name word_rotr} T = bv_rotate "rotate_right" T |
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
|
137 |
| func _ _ = K NONE |
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
|
138 |
|
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
|
139 |
fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n) |
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
|
140 |
fun is_builtin_pred (n, T) = is_predT T andalso is_some (pred n T) |
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
|
141 |
|
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
|
142 |
fun builtin_fun (n, T) 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
|
143 |
if is_connT T then conn n |> Option.map (rpair 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
|
144 |
else if is_predT T then pred n T |> Option.map (rpair 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
|
145 |
else func n T 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
|
146 |
|
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
|
147 |
|
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
|
148 |
|
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
|
149 |
(* serialization *) |
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
|
150 |
|
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
|
151 |
val add = Buffer.add |
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
|
152 |
fun sep f = add " " #> f |
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
|
153 |
fun enclose l r f = sep (add l #> f #> add r) |
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
|
154 |
val par = enclose "(" ")" |
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
|
155 |
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs)) |
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
|
156 |
fun line f = f #> add "\n" |
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
|
157 |
|
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
|
158 |
fun var i = add "?v" #> add (string_of_int i) |
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
|
159 |
|
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
|
160 |
fun sterm l (T.SVar i) = sep (var (l - i - 1)) |
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
|
161 |
| sterm l (T.SApp (n, ts)) = app n (sterm l) 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
|
162 |
| sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression" |
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
|
163 |
| sterm l (T.SQua (q, ss, ps, t)) = |
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
|
164 |
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
|
165 |
val quant = add o (fn T.SForall => "forall" | T.SExists => "exists") |
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
|
166 |
val vs = map_index (apfst (Integer.add l)) ss |
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
|
167 |
fun var_decl (i, s) = par (var i #> sep (add s)) |
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
|
168 |
val sub = sterm (l + length ss) |
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
|
169 |
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub 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
|
170 |
fun pats (T.SPat ts) = pat ":pat" 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
|
171 |
| pats (T.SNoPat ts) = pat ":nopat" 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
|
172 |
in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) 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
|
173 |
|
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
|
174 |
fun choose_logic theories = |
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
|
175 |
if member (op =) theories T.Bitvector then "QF_AUFBV" |
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
|
176 |
else if member (op =) theories T.Real then "AUFLIRA" |
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
|
177 |
else "AUFLIA" |
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
|
178 |
|
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
|
179 |
fun serialize comments {theories, sorts, funcs} 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
|
180 |
Buffer.empty |
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
|
181 |
|> line (add "(benchmark Isabelle") |
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
|
182 |
|> line (add ":status unknown") |
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
|
183 |
|> line (add ":logic " #> add (choose_logic theories)) |
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
|
184 |
|> length sorts > 0 ? |
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
|
185 |
line (add ":extrasorts" #> par (fold (sep o add) sorts)) |
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
|
186 |
|> length funcs > 0 ? ( |
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
|
187 |
line (add ":extrafuns" #> add " (") #> |
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
|
188 |
fold (fn (f, (ss, s)) => |
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
|
189 |
line (sep (app f (sep o add) (ss @ [s])))) funcs #> |
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
|
190 |
line (add ")")) |
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
|
191 |
|> fold (fn t => line (add ":assumption" #> sterm 0 t)) 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
|
192 |
|> line (add ":formula true)") |
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
|
193 |
|> fold (fn str => line (add "; " #> add str)) 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
|
194 |
|> Buffer.content |
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
|
195 |
|
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
|
196 |
|
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
|
197 |
|
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
|
198 |
(* 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
|
199 |
|
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
|
200 |
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
|
201 |
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
|
202 |
sort_prefix = "S", |
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
|
203 |
func_prefix = "f"}, |
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
|
204 |
strict = SOME { |
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
|
205 |
is_builtin_conn = is_builtin_conn, |
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
|
206 |
is_builtin_pred = is_builtin_pred, |
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
|
207 |
is_builtin_distinct = true}, |
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
|
208 |
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
|
209 |
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
|
210 |
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
|
211 |
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
|
212 |
serialize = serialize 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
|
213 |
|
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
|
214 |
end |