author | wenzelm |
Tue, 28 Sep 2021 22:14:02 +0200 | |
changeset 74382 | 8d0294d877bd |
parent 72458 | b44e894796d5 |
child 74561 | 8e6c973003c8 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smtlib_proof.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
3 |
Author: Mathias Fleury, ENS Rennes |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
6 |
SMT-LIB-2-style proofs: parsing and abstract syntax tree. |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
7 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
|
58061 | 9 |
signature SMTLIB_PROOF = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
sig |
58061 | 11 |
datatype 'b shared = Tree of SMTLIB.tree | Term of term | Proof of 'b | None |
57221 | 12 |
type ('a, 'b) context |
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
13 |
|
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
14 |
val mk_context: Proof.context -> int -> 'b shared Symtab.table -> typ Symtab.table -> |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
15 |
term Symtab.table -> 'a -> ('a, 'b) context |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
16 |
val empty_context: Proof.context -> typ Symtab.table -> term Symtab.table -> ('a list, 'b) context |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
17 |
val ctxt_of: ('a, 'b) context -> Proof.context |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
18 |
val lookup_binding: ('a, 'b) context -> string -> 'b shared |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
19 |
val update_binding: string * 'b shared -> ('a, 'b) context -> ('a, 'b) context |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
20 |
val with_bindings: (string * 'b shared) list -> (('a, 'b) context -> 'c * ('d, 'b) context) -> |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
21 |
('a, 'b) context -> 'c * ('d, 'b) context |
57222 | 22 |
val next_id: ('a, 'b) context -> int * ('a, 'b) context |
23 |
val with_fresh_names: (('a list, 'b) context -> |
|
57747 | 24 |
term * ((string * (string * typ)) list, 'b) context) -> ('c, 'b) context -> (term * string list) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
(*type and term parsers*) |
58061 | 27 |
type type_parser = SMTLIB.tree * typ list -> typ option |
28 |
type term_parser = SMTLIB.tree * term list -> term option |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
val add_type_parser: type_parser -> Context.generic -> Context.generic |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
val add_term_parser: term_parser -> Context.generic -> Context.generic |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
|
58061 | 32 |
exception SMTLIB_PARSE of string * SMTLIB.tree |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
34 |
val declare_fun: string -> typ -> ((string * typ) list, 'a) context -> |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
35 |
((string * typ) list, 'a) context |
58061 | 36 |
val dest_binding: SMTLIB.tree -> string * 'a shared |
37 |
val type_of: ('a, 'b) context -> SMTLIB.tree -> typ |
|
38 |
val term_of: SMTLIB.tree -> ((string * (string * typ)) list, 'a) context -> |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
39 |
term * ((string * (string * typ)) list, 'a) context |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
40 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
41 |
(*name bindings*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
42 |
type name_bindings |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
43 |
val empty_name_binding: name_bindings |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
44 |
val update_name_binding: Symtab.key * SMTLIB.tree -> name_bindings -> name_bindings |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
45 |
val extract_name_bindings: SMTLIB.tree -> name_bindings -> name_bindings * string list |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
46 |
val expand_name_bindings: SMTLIB.tree -> name_bindings -> SMTLIB.tree * name_bindings |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
47 |
val extract_and_update_name_bindings: SMTLIB.tree -> name_bindings -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
48 |
(SMTLIB.tree * name_bindings) * string list |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
49 |
val remove_name_bindings: SMTLIB.tree -> SMTLIB.tree |
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
50 |
end; |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
51 |
|
58061 | 52 |
structure SMTLIB_Proof: SMTLIB_PROOF = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
54 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
55 |
(* proof parser context *) |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
56 |
|
58061 | 57 |
datatype 'b shared = Tree of SMTLIB.tree | Term of term | Proof of 'b | None |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
59 |
type ('a, 'b) context = { |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
60 |
ctxt: Proof.context, |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
61 |
id: int, |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
62 |
syms: 'b shared Symtab.table, |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
63 |
typs: typ Symtab.table, |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
64 |
funs: term Symtab.table, |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
65 |
extra: 'a} |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
66 |
|
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
67 |
fun mk_context ctxt id syms typs funs extra: ('a, 'b) context = |
57747 | 68 |
{ctxt = ctxt, id = id, syms = syms, typs = typs, funs = funs, extra = extra} |
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
69 |
|
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
70 |
fun empty_context ctxt typs funs = mk_context ctxt 1 Symtab.empty typs funs [] |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
71 |
|
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
72 |
fun ctxt_of ({ctxt, ...}: ('a, 'b) context) = ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
73 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
74 |
fun lookup_binding ({syms, ...}: ('a, 'b) context) = |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
75 |
the_default None o Symtab.lookup syms |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
76 |
|
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
77 |
fun map_syms f ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) = |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
78 |
mk_context ctxt id (f syms) typs funs extra |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
79 |
|
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
80 |
fun update_binding b = map_syms (Symtab.update b) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
81 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
82 |
fun with_bindings bs f cx = |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
83 |
let val bs' = map (lookup_binding cx o fst) bs |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
84 |
in |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
85 |
cx |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
86 |
|> fold update_binding bs |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
87 |
|> f |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
88 |
||> fold2 (fn (name, _) => update_binding o pair name) bs bs' |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
89 |
end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
90 |
|
57221 | 91 |
fun next_id ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) = |
92 |
(id, mk_context ctxt (id + 1) syms typs funs extra) |
|
93 |
||
57748 | 94 |
fun with_fresh_names f ({ctxt, id, syms, typs, funs, ...}: ('a, 'b) context) = |
57221 | 95 |
let |
96 |
fun bind (_, v as (_, T)) t = Logic.all_const T $ Term.absfree v t |
|
97 |
||
98 |
val needs_inferT = equal Term.dummyT orf Term.is_TVar |
|
99 |
val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT) |
|
100 |
fun infer_types ctxt = |
|
101 |
singleton (Type_Infer_Context.infer_types ctxt) #> |
|
102 |
singleton (Proof_Context.standard_term_check_finish ctxt) |
|
103 |
fun infer ctxt t = if needs_infer t then infer_types ctxt t else t |
|
104 |
||
57747 | 105 |
val (t, {ctxt = ctxt', extra = names, ...}: ((string * (string * typ)) list, 'b) context) = |
57221 | 106 |
f (mk_context ctxt id syms typs funs []) |
107 |
val t' = infer ctxt' (fold_rev bind names (HOLogic.mk_Trueprop t)) |
|
108 |
in |
|
57747 | 109 |
(t', map fst names) |
57221 | 110 |
end |
111 |
||
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
112 |
fun lookup_typ ({typs, ...}: ('a, 'b) context) = Symtab.lookup typs |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
113 |
fun lookup_fun ({funs, ...}: ('a, 'b) context) = Symtab.lookup funs |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
115 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
(* core type and term parser *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
|
69593 | 118 |
fun core_type_parser (SMTLIB.Sym "Bool", []) = SOME \<^typ>\<open>HOL.bool\<close> |
119 |
| core_type_parser (SMTLIB.Sym "Int", []) = SOME \<^typ>\<open>Int.int\<close> |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
| core_type_parser _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
fun mk_unary n t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
let val T = fastype_of t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
124 |
in Const (n, T --> T) $ t end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
fun mk_binary' n T U t1 t2 = Const (n, [T, T] ---> U) $ t1 $ t2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
fun mk_binary n t1 t2 = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
let val T = fastype_of t1 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
in mk_binary' n T T t1 t2 end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
132 |
fun mk_rassoc f t ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
let val us = rev (t :: ts) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
in fold f (tl us) (hd us) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
136 |
fun mk_lassoc f t ts = fold (fn u1 => fn u2 => f u2 u1) ts t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
fun mk_lassoc' n = mk_lassoc (mk_binary n) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
139 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
140 |
fun mk_binary_pred n S t1 t2 = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
141 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
142 |
val T1 = fastype_of t1 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
val T2 = fastype_of t2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
val T = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
145 |
if T1 <> Term.dummyT then T1 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
else if T2 <> Term.dummyT then T2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
147 |
else TVar (("?a", serial ()), S) |
69593 | 148 |
in mk_binary' n T \<^typ>\<open>HOL.bool\<close> t1 t2 end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
|
69593 | 150 |
fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2 |
151 |
fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
|
74382 | 153 |
fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^Const>\<open>True\<close> |
154 |
| core_term_parser (SMTLIB.Sym "false", _) = SOME \<^Const>\<open>False\<close> |
|
58061 | 155 |
| core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t) |
156 |
| core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts) |
|
157 |
| core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts) |
|
158 |
| core_term_parser (SMTLIB.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) |
|
159 |
| core_term_parser (SMTLIB.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) |
|
160 |
| core_term_parser (SMTLIB.Sym "=", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2)) |
|
161 |
| core_term_parser (SMTLIB.Sym "~", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2)) |
|
162 |
| core_term_parser (SMTLIB.Sym "ite", [t1, t2, t3]) = |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
163 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
164 |
val T = fastype_of t2 |
69593 | 165 |
val c = Const (\<^const_name>\<open>HOL.If\<close>, [\<^typ>\<open>HOL.bool\<close>, T, T] ---> T) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
166 |
in SOME (c $ t1 $ t2 $ t3) end |
69593 | 167 |
| core_term_parser (SMTLIB.Num i, []) = SOME (HOLogic.mk_number \<^typ>\<open>Int.int\<close> i) |
168 |
| core_term_parser (SMTLIB.Sym "-", [t]) = SOME (mk_unary \<^const_name>\<open>uminus_class.uminus\<close> t) |
|
169 |
| core_term_parser (SMTLIB.Sym "~", [t]) = SOME (mk_unary \<^const_name>\<open>uminus_class.uminus\<close> t) |
|
58061 | 170 |
| core_term_parser (SMTLIB.Sym "+", t :: ts) = |
69593 | 171 |
SOME (mk_lassoc' \<^const_name>\<open>plus_class.plus\<close> t ts) |
58061 | 172 |
| core_term_parser (SMTLIB.Sym "-", t :: ts) = |
69593 | 173 |
SOME (mk_lassoc' \<^const_name>\<open>minus_class.minus\<close> t ts) |
58061 | 174 |
| core_term_parser (SMTLIB.Sym "*", t :: ts) = |
69593 | 175 |
SOME (mk_lassoc' \<^const_name>\<open>times_class.times\<close> t ts) |
176 |
| core_term_parser (SMTLIB.Sym "div", [t1, t2]) = SOME (mk_binary \<^const_name>\<open>z3div\<close> t1 t2) |
|
177 |
| core_term_parser (SMTLIB.Sym "mod", [t1, t2]) = SOME (mk_binary \<^const_name>\<open>z3mod\<close> t1 t2) |
|
58061 | 178 |
| core_term_parser (SMTLIB.Sym "<", [t1, t2]) = SOME (mk_less t1 t2) |
179 |
| core_term_parser (SMTLIB.Sym ">", [t1, t2]) = SOME (mk_less t2 t1) |
|
180 |
| core_term_parser (SMTLIB.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2) |
|
181 |
| core_term_parser (SMTLIB.Sym ">=", [t1, t2]) = SOME (mk_less_eq t2 t1) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
182 |
| core_term_parser _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
184 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
185 |
(* custom type and term parsers *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
186 |
|
58061 | 187 |
type type_parser = SMTLIB.tree * typ list -> typ option |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
188 |
|
58061 | 189 |
type term_parser = SMTLIB.tree * term list -> term option |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
190 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
191 |
fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
192 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
193 |
structure Parsers = Generic_Data |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
194 |
( |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
195 |
type T = (int * type_parser) list * (int * term_parser) list |
56122 | 196 |
val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)]) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
197 |
val extend = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
198 |
fun merge ((tys1, ts1), (tys2, ts2)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
199 |
(Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
200 |
) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
201 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
202 |
fun add_type_parser type_parser = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
203 |
Parsers.map (apfst (Ord_List.insert id_ord (serial (), type_parser))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
204 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
205 |
fun add_term_parser term_parser = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
206 |
Parsers.map (apsnd (Ord_List.insert id_ord (serial (), term_parser))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
207 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
208 |
fun get_type_parsers ctxt = map snd (fst (Parsers.get (Context.Proof ctxt))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
209 |
fun get_term_parsers ctxt = map snd (snd (Parsers.get (Context.Proof ctxt))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
210 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
211 |
fun apply_parsers parsers x = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
212 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
213 |
fun apply [] = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
214 |
| apply (parser :: parsers) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
215 |
(case parser x of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
216 |
SOME y => SOME y |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
217 |
| NONE => apply parsers) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
218 |
in apply parsers end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
219 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
220 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
221 |
(* type and term parsing *) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
222 |
|
58061 | 223 |
exception SMTLIB_PARSE of string * SMTLIB.tree |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
224 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
225 |
val desymbolize = Name.desymbolize (SOME false) o perhaps (try (unprefix "?")) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
226 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
227 |
fun fresh_fun add name n T ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
228 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
229 |
val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
230 |
val t = Free (n', T) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
231 |
val funs' = Symtab.update (name, t) funs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
232 |
in (t, mk_context ctxt' id syms typs funs' (add (n', T) extra)) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
233 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
234 |
fun declare_fun name = snd oo fresh_fun cons name (desymbolize name) |
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
235 |
fun declare_free name = fresh_fun (cons o pair name) name (desymbolize name) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
236 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
237 |
fun parse_type cx ty Ts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
238 |
(case apply_parsers (get_type_parsers (ctxt_of cx)) (ty, Ts) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
239 |
SOME T => T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
240 |
| NONE => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
241 |
(case ty of |
58061 | 242 |
SMTLIB.Sym name => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
243 |
(case lookup_typ cx name of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
244 |
SOME T => T |
58061 | 245 |
| NONE => raise SMTLIB_PARSE ("unknown SMT type", ty)) |
246 |
| _ => raise SMTLIB_PARSE ("bad SMT type format", ty))) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
247 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
248 |
fun parse_term t ts cx = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
249 |
(case apply_parsers (get_term_parsers (ctxt_of cx)) (t, ts) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
250 |
SOME u => (u, cx) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
251 |
| NONE => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
252 |
(case t of |
58061 | 253 |
SMTLIB.Sym name => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
254 |
(case lookup_fun cx name of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
255 |
SOME u => (Term.list_comb (u, ts), cx) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
256 |
| NONE => |
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
257 |
if null ts then declare_free name Term.dummyT cx |
58061 | 258 |
else raise SMTLIB_PARSE ("bad SMT term", t)) |
259 |
| _ => raise SMTLIB_PARSE ("bad SMT term format", t))) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
260 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
261 |
fun type_of cx ty = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
262 |
(case try (parse_type cx ty) [] of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
263 |
SOME T => T |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
264 |
| NONE => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
265 |
(case ty of |
58061 | 266 |
SMTLIB.S (ty' :: tys) => parse_type cx ty' (map (type_of cx) tys) |
267 |
| _ => raise SMTLIB_PARSE ("bad SMT type", ty))) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
268 |
|
58061 | 269 |
fun dest_var cx (SMTLIB.S [SMTLIB.Sym name, ty]) = (name, (desymbolize name, type_of cx ty)) |
270 |
| dest_var _ v = raise SMTLIB_PARSE ("bad SMT quantifier variable format", v) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
271 |
|
58061 | 272 |
fun dest_body (SMTLIB.S (SMTLIB.Sym "!" :: body :: _)) = dest_body body |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
273 |
| dest_body body = body |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
274 |
|
58061 | 275 |
fun dest_binding (SMTLIB.S [SMTLIB.Sym name, t]) = (name, Tree t) |
276 |
| dest_binding b = raise SMTLIB_PARSE ("bad SMT let binding format", b) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
277 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
278 |
fun mk_choice (x, T, P) = HOLogic.choice_const T $ absfree (x, T) P |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
58061
diff
changeset
|
279 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
280 |
fun term_of t cx = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
281 |
(case t of |
58061 | 282 |
SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx |
283 |
| SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
58061
diff
changeset
|
284 |
| SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx |
58061 | 285 |
| SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
286 |
with_bindings (map dest_binding bindings) (term_of body) cx |
58061 | 287 |
| SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx |
288 |
| SMTLIB.S (f :: args) => |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
289 |
cx |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
290 |
|> fold_map term_of args |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
291 |
|-> parse_term f |
58061 | 292 |
| SMTLIB.Sym name => |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
293 |
(case lookup_binding cx name of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
294 |
Tree u => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
295 |
cx |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
296 |
|> term_of u |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
297 |
|-> (fn u' => pair u' o update_binding (name, Term u')) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
298 |
| Term u => (u, cx) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
299 |
| None => parse_term t [] cx |
58061 | 300 |
| _ => raise SMTLIB_PARSE ("bad SMT term format", t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
301 |
| _ => parse_term t [] cx) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
302 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
303 |
and quant q vars body cx = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
304 |
let val vs = map (dest_var cx) vars |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
305 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
306 |
cx |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
307 |
|> with_bindings (map (apsnd (Term o Free)) vs) (term_of (dest_body body)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
308 |
|>> fold_rev (fn (_, (n, T)) => fn t => q (n, T, t)) vs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
309 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
310 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
311 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
312 |
(* Sharing of terms via "! _ :named name"*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
313 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
314 |
type name_bindings = SMTLIB.tree Symtab.table * SMTLIB.tree Symtab.table |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
315 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
316 |
val empty_name_binding = (Symtab.empty, Symtab.empty) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
317 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
318 |
fun update_name_binding (name, t) (tab, exp_tab) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
319 |
(tab, Symtab.update (name, t) exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
320 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
321 |
fun remove_name_bindings (SMTLIB.S (SMTLIB.Sym "!" :: body :: _)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
322 |
remove_name_bindings body |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
323 |
| remove_name_bindings (SMTLIB.S body) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
324 |
SMTLIB.S (map remove_name_bindings body) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
325 |
| remove_name_bindings t = t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
326 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
327 |
fun extract_name_bindings t (tab, exp_tab) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
328 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
329 |
fun extract t (tab, new) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
330 |
(case t of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
331 |
SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S _, body] => extract body (tab, new) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
332 |
| SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S _, body] => extract body (tab, new) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
333 |
| SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S _, body] => extract body (tab, new) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
334 |
| SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
335 |
raise (Fail "unsupported let construction in name extraction") |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
336 |
| SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name]) => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
337 |
extract t (tab, new) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
338 |
|>> Symtab.update (name, remove_name_bindings t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
339 |
||> curry (op :: ) name |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
340 |
| SMTLIB.S args => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
341 |
fold extract args (tab, new) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
342 |
| _ => ((tab, new))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
343 |
val (tab, new) = extract t (tab, []) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
344 |
in ((tab, exp_tab), new) end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
345 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
346 |
fun expand_name_bindings t (tab, exp_tab) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
347 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
348 |
fun expand_update (SMTLIB.Sym sym) exp_tab = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
349 |
(case Symtab.lookup exp_tab sym of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
350 |
SOME t => (t, exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
351 |
| NONE => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
352 |
(case (Symtab.lookup tab sym) of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
353 |
NONE => (SMTLIB.Sym sym, exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
354 |
| SOME u => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
355 |
let val (u2, exp_tab) = expand_update u exp_tab |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
356 |
in (u2, Symtab.update (sym, u2) exp_tab) end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
357 |
) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
358 |
) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
359 |
| expand_update (t as SMTLIB.Key _) exp_tab = (t, exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
360 |
| expand_update (t as SMTLIB.Num _) exp_tab = (t, exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
361 |
| expand_update (t as SMTLIB.Dec _) exp_tab = (t, exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
362 |
| expand_update (t as SMTLIB.Str _) exp_tab = (t, exp_tab) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
363 |
| expand_update (SMTLIB.S s) (exp_tab : SMTLIB.tree Symtab.table) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
364 |
fold_map expand_update s exp_tab |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
365 |
|>> (fn s => SMTLIB.S s) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
366 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
367 |
expand_update t exp_tab |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
368 |
|> (fn (t, exp_tab) => (remove_name_bindings t, (tab, exp_tab))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
369 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
370 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
371 |
fun extract_and_update_name_bindings t tab = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
372 |
extract_name_bindings t tab |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
373 |
|>> expand_name_bindings (remove_name_bindings t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
374 |
|
57219
34018603e0d0
factor out SMT-LIB 2 type/term parsing from Z3-specific code
blanchet
parents:
56811
diff
changeset
|
375 |
end; |