author | boehmes |
Wed, 07 Apr 2010 20:40:42 +0200 | |
changeset 36085 | 0eaa6905590f |
parent 36084 | 3176ec2244ad |
child 36087 | 37a5735783c5 |
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/smtlib_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 SMT solvers based on the SMT-LIB format. |
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 SMTLIB_INTERFACE = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
8 |
sig |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
9 |
val basic_builtins: SMT_Translate.builtins |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
10 |
val default_attributes: string list |
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
11 |
val gen_interface: SMT_Translate.builtins -> string list -> string list -> |
36085
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
12 |
SMT_Translate.config |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
13 |
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
|
14 |
end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
15 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
16 |
structure SMTLIB_Interface: SMTLIB_INTERFACE = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
17 |
struct |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
18 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
19 |
structure T = SMT_Translate |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
20 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
21 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
22 |
(* built-in types, functions and predicates *) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
23 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
24 |
val builtin_typ = (fn |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
25 |
@{typ int} => SOME "Int" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
26 |
| @{typ real} => SOME "Real" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
27 |
| _ => NONE) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
28 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
29 |
val builtin_num = (fn |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
30 |
(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
|
31 |
| (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
|
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 "uminus :: real => _"}, "~"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
41 |
(@{term "plus :: real => _"}, "+"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
42 |
(@{term "minus :: real => _"}, "-"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
43 |
(@{term "times :: real => _"}, "*") ] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
44 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
45 |
val builtin_preds = T.builtin_make [ |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
46 |
(@{term True}, "true"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
47 |
(@{term False}, "false"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
48 |
(@{term Not}, "not"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
49 |
(@{term "op &"}, "and"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
50 |
(@{term "op |"}, "or"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
51 |
(@{term "op -->"}, "implies"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
52 |
(@{term "op iff"}, "iff"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
53 |
(@{term If}, "if_then_else"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
54 |
(@{term distinct}, "distinct"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
55 |
(@{term "op ="}, "="), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
56 |
(@{term "op < :: int => _"}, "<"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
57 |
(@{term "op <= :: int => _"}, "<="), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
58 |
(@{term "op < :: real => _"}, "<"), |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
59 |
(@{term "op <= :: real => _"}, "<=") ] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
60 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
61 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
62 |
(* serialization *) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
63 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
64 |
fun wr s stream = (TextIO.output (stream, s); stream) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
65 |
fun wr_line f = f #> wr "\n" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
66 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
67 |
fun sep f = wr " " #> f |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
68 |
fun par f = sep (wr "(" #> f #> wr ")") |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
69 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
70 |
fun wr1 s = sep (wr s) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
71 |
fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts)) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
72 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
73 |
val term_marker = "__term" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
74 |
val formula_marker = "__form" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
75 |
fun dest_marker (T.SApp ("__term", [t])) = SOME (true, t) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
76 |
| dest_marker (T.SApp ("__form", [t])) = SOME (false, t) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
77 |
| dest_marker _ = NONE |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
78 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
79 |
val tvar = prefix "?" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
80 |
val fvar = prefix "$" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
81 |
|
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
82 |
datatype lexpr = |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
83 |
LVar of string | |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
84 |
LTerm of lexpr list * (string, string) T.sterm |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
85 |
|
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
86 |
fun wr_expr loc env t = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
87 |
(case t of |
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
88 |
T.SVar i => |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
89 |
(case nth env i of |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
90 |
LVar name => wr1 name |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
91 |
| LTerm (env', t') => wr_expr loc env' t') |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
92 |
| T.SApp (n, ts) => |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
93 |
(case dest_marker t of |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
94 |
SOME (loc', t') => wr_expr loc' env t' |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
95 |
| NONE => wrn (wr_expr loc env) n ts) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
96 |
| T.SLet ((v, _), t1, t2) => |
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
97 |
if loc |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
98 |
then |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
99 |
let val (_, t1') = the (dest_marker t1) |
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
100 |
in wr_expr loc (LTerm (env, t1') :: env) t2 end |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
101 |
else |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
102 |
let |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
103 |
val (loc', t1') = the (dest_marker t1) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
104 |
val (kind, v') = if loc' then ("let", tvar v) else ("flet", fvar v) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
105 |
in |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
106 |
par (wr kind #> par (wr v' #> wr_expr loc' env t1') #> |
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
107 |
wr_expr loc (LVar v' :: env) t2) |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
108 |
end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
109 |
| T.SQuant (q, vs, ps, b) => |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
110 |
let |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
111 |
val wr_quant = wr o (fn T.SForall => "forall" | T.SExists => "exists") |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
112 |
fun wr_var (n, s) = par (wr (tvar n) #> wr1 s) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
113 |
|
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
33418
diff
changeset
|
114 |
val wre = wr_expr loc (map (LVar o tvar o fst) (rev vs) @ env) |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
115 |
|
33353 | 116 |
fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}" |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
117 |
fun wr_pat (T.SPat ts) = wrp "pat" ts |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
118 |
| wr_pat (T.SNoPat ts) = wrp "nopat" ts |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
119 |
in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
120 |
|
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
121 |
fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream = |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
122 |
let |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
123 |
fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts))) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
124 |
in |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
125 |
stream |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
126 |
|> wr_line (wr "(benchmark Isabelle") |
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
127 |
|> wr_line (wr ":status unknown") |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
128 |
|> fold (wr_line o wr) attributes |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
129 |
|> length typs > 0 ? |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
130 |
wr_line (wr ":extrasorts" #> par (fold wr1 typs)) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
131 |
|> length funs > 0 ? ( |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
132 |
wr_line (wr ":extrafuns (") #> |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
133 |
fold (wr_decl o apsnd (fn (Ts, T) => Ts @ [T])) funs #> |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
134 |
wr_line (wr " )")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
135 |
|> length preds > 0 ? ( |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
136 |
wr_line (wr ":extrapreds (") #> |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
137 |
fold wr_decl preds #> |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
138 |
wr_line (wr " )")) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
139 |
|> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
140 |
|> wr_line (wr ":formula true") |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
141 |
|> wr_line (wr ")") |
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
142 |
|> fold (fn comment => wr_line (wr ("; " ^ comment))) comments |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
143 |
|> K () |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
144 |
end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
145 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
146 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
147 |
(* SMT solver interface using the SMT-LIB input format *) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
148 |
|
33017
4fb8a33f74d6
eliminated extraneous wrapping of public records,
boehmes
parents:
32618
diff
changeset
|
149 |
val basic_builtins = { |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
150 |
builtin_typ = builtin_typ, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
151 |
builtin_num = builtin_num, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
152 |
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
|
153 |
|
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
154 |
val default_attributes = [":logic AUFLIRA"] |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
155 |
|
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
156 |
fun gen_interface builtins attributes comments = { |
36085
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
157 |
strict = true, |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
158 |
prefixes = { |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
159 |
var_prefix = "x", |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
160 |
typ_prefix = "T", |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
161 |
fun_prefix = "uf_", |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
162 |
pred_prefix = "up_" }, |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
163 |
markers = { |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
164 |
term_marker = term_marker, |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
165 |
formula_marker = formula_marker }, |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
166 |
builtins = builtins, |
0eaa6905590f
shortened interface (do not export unused options and functions)
boehmes
parents:
36084
diff
changeset
|
167 |
serialize = serialize attributes comments } |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
168 |
|
35153
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
169 |
fun interface comments = |
5e8935678ee4
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
boehmes
parents:
33446
diff
changeset
|
170 |
gen_interface basic_builtins default_attributes comments |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
171 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
172 |
end |